Nuprl - Proof: es-le-trans 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: es-le-trans 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

By:	SplitOrHyps THENL [OrLeft THEN (UseTrans b) ;OrLeft THEN (HypSubst -3 0) ;OrLeft THEN (HypSubst -2 -3) ;OrRight]

Generated subgoals:

None

About:

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