(4steps total) PrintForm Definitions rel 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: trans imp sp trans 2

1. T : Type
2. R : TTProp
3. a,b,c:TR(a,b R(b,c R(a,c)
4. a : T
5. b : T
6. c : T
7. R(a,b)
8. R(b,a)
9. R(b,c)
10. R(c,b)
  R(c,a)


By: (Analyze 0) THEN (Analyze 10)


Generated subgoal:

1 10. R(c,a)
  R(c,b)

1 step

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

(4steps total) PrintForm Definitions rel 1 Sections StandardLIB Doc