(6steps 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 exp add 2 1 1
1. T : Type
2. R : TTProp
3. m : 
4. 0<m
5. n:, x,y,z:T. (x R^m-1 y)  (y R^n z)  (x R^m-1+n z)
6. n : 
7. T
8. y : T
9. z : T
10. y R^n z
11. m=0
12. m+n=0
13. z1 : T
14. z1 R^m-1 y
  z1 R^m+n-1 z
By: AllHyps (InstHyp [n;z1;y;z]) THEN NthHypSq -1
THEN
RepeatFor 2 (Analyze THEN Try Trivial)

Generated subgoal:

1 15. z1 R^m-1+n z
  (m+n-1) ~ (m-1+n)
Auto

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

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