Nuprl - Proof: fun exp add sq 2 1 1

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

1. n :

2. 0<n
3.

, f,i:Top. (f^n-1+m(i)) ~ (f^n-1(f^m(i)))
4. m :

5. f : Top
6. i : Top

(f^n-1+m+1(i)) ~ (f^n-1+1(f^m(i)))

By:	Assert (n:, x:Top. (f^n+1(x)) ~ (f(f^n(x))))

Generated subgoals:

1 n:, x:Top. (f^n+1(x)) ~ (f(f^n(x)))
2 steps

2 7. n:, x:Top. (f^n+1(x)) ~ (f(f^n(x)))
(f^n-1+m+1(i)) ~ (f^n-1+1(f^m(i)))
2 steps

About:

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

1	n:, x:Top. (f^n+1(x)) ~ (f(f^n(x)))	2 steps
2	7. n:, x:Top. (f^n+1(x)) ~ (f(f^n(x))) (f^n-1+m+1(i)) ~ (f^n-1+1(f^m(i)))	2 steps