(16steps total) PrintForm Definitions mb event system 2 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: rel plus implies 2 1 1 1 1 1
1. T : Type
2. R : TTProp
3. n : 
4. 0<n
5. n = 1
6. 0<n
7. x : T
8. y : T
9. n = 0
10. z : T
11. x R z
12. z R^n-1 y
13. x,y:T. (x R^n-1 y)  (x R y)  (z:T. (x R^+ z) & (z R y))
14. z R y
  x R^+ z
By: Unfold `rel_plus` 0 THEN Reduce 0 THEN InstConcl [1] THEN Reduce 0

Generated subgoal:

1   x R^1 z
1 step

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

(16steps total) PrintForm Definitions mb event system 2 Sections EventSystems Doc