a,b,c:. imin(a;imin(b;c)) = imin(imin(a;b);c)

By:	Auto THEN Rewrite by a,b:. imin(a;b) = -imax(-a;-b) THEN Rewrite by Thm* a,b:. -imin(a;b) = imax(-a;-b)

1

1. a :  2. b :  3. c :    -imax(-a;imax(-b;-c)) = -imax(imax(-a;-b);-c)

1 step

About: IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html