(5steps total) PrintForm Definitions Lemmas rel 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: trans rel func wrt sym self
  T:Type, R:(TTProp).
  (Trans x,y:T. R(x,y))
  
  (a,a',b,b':T.
  (Symmetrize(x,y.R(x,y);a;b)
  (
  (Symmetrize(x,y.R(x,y);a';b')  (R(a,a')  R(b,b')))
By: (Unfolds [`symmetrize`;`guard`] 0) THEN GenRepD

Generated subgoals:

1 1. T : Type
2. R : TTProp
3. Trans x,y:T. R(x,y)
4. a : T
5. a' : T
6. b : T
7. b' : T
8. R(a,b)
9. R(b,a)
10. R(a',b')
11. R(b',a')
12. R(a,a')
  R(b,b')
2 steps
2 1. T : Type
2. R : TTProp
3. Trans x,y:T. R(x,y)
4. a : T
5. a' : T
6. b : T
7. b' : T
8. R(a,b)
9. R(b,a)
10. R(a',b')
11. R(b',a')
12. R(b,b')
  R(a,a')
2 steps

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

(5steps total) PrintForm Definitions Lemmas rel 1 Sections StandardLIB Doc