the_es:ES. Trans x,y:E. x  y 

By:	Unfolds [`trans`;`es-le`] 0 THEN Inst Thm* the_es:ES. Trans x,y:E. (x <loc y) [the_es]

1

1. the_es : ES 2. a : E 3. b : E 4. c : E 5. (a <loc b)  a = b 6. (b <loc c)  b = c 7. Trans x,y:E. (x <loc y)   (a <loc c)  a = c

1 step

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html