(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 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


By: MoveToConcl -1 THEN MoveToConcl 4 THEN MoveToConcl 3 THEN MoveToConcl -1
THEN
InductionOnNat


Generated subgoals:

1 3. EquivRel(T)(_1 E _2)
  x,y:T. (x E^0 y (x E y)

2 steps
2 3. EquivRel(T)(_1 E _2)
4. n : 
5. 0<n
6. x,y:T. (x E^n-1 y (x E y)
  x,y:T. (x E^n y (x E y)

5 steps

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

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