(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 b
  T:Type, R:(TTProp).
  (Trans a,b:T. R(a,b))
  
  (a,b,c:T.
  (strict_part(x,y.R(x,y);a;b)  R(b,c)  strict_part(x,y.R(x,y);a;c))
By: Unfolds [`trans`;`strict_part`;`guard`] 0 THEN GenRepD

Generated subgoals:

1 1. T : Type
2. R : TTProp
3. a,b,c:T. R(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)
  R(a,c)
1 step
2 1. T : Type
2. R : TTProp
3. a,b,c:T. R(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)
  R(c,a)
2 steps

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