(6steps total) PrintForm Definitions rel 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: symmetrized preorder
  T:Type, R:(TTProp).
  Preorder(T;x,y.R(x,y))  (EquivRel a,b:T. Symmetrize(x,y.R(x,y);a;b))
By: Unfolds [`preorder`;`equiv_rel`;`symmetrize`] 0

Generated subgoals:

1 1. T : Type
2. R : TTProp
3. Refl(T;x,y.R(x,y))
4. Trans x,y:T. R(x,y)
  Refl(T;a,b.R(a,b) & R(b,a))
1 step
2 1. T : Type
2. R : TTProp
3. Refl(T;x,y.R(x,y))
4. Trans x,y:T. R(x,y)
  Sym a,b:T. R(a,b) & R(b,a)
1 step
3 1. T : Type
2. R : TTProp
3. Refl(T;x,y.R(x,y))
4. Trans x,y:T. R(x,y)
  Trans a,b:T. R(a,b) & R(b,a)
3 steps

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

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