(9steps total) PrintForm Definitions mb nat Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: rel star of equiv

  T:Type, E:(TTProp), x,y:T.
  EquivRel(T)(_1 E _2)  (x (E^*) y (x E y)


By: Unfold `rel_star` 0 THEN Reduce 0 THEN ExRepD


Generated subgoal:

1 1. T : Type
2. E : TTProp
3. x : T
4. y : T
5. EquivRel(T)(_1 E _2)
6. n : 
7. x E^n y
  x E y

8 steps

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

(9steps total) PrintForm Definitions mb nat Sections MarkB generic Doc