Nuprl - Proof: fun exp add1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: fun exp add1 1 1

1. T : Type
2. f : T

T
3. n :

4. T
5. f^1+n = f^1 o f^n

f^n+1 = f o f^n

By:	Subst' (n+1 = 1+n) 0 THEN HypSubst -1 0

Generated subgoal:

1 f^1 o f^n = f o f^n
1 step

About:

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