Nuprl - Proof: hsimp rec wd 1 1 1 1 1 1 2 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hsimp rec wd 1 1 1 1 1 1 2 1 1

1. 'a : S
2. x : 'a
3. f : 'a

'a
4. fun :

'a
5. fun(0) = x
6. n :

7. 0<n
8.

. m<n+1

fun(m+1) = f(fun(m))
9. fun(n) = f(fun(-1+n))
10. ncompose(f;-1+n;x) = fun(-1+n)

f(ncompose(f;-1+n;x)) = f(fun(-1+n))

By:	Analyze THEN StrongAuto THEN Try (Complete (Unfold `label` 0))

Generated subgoal:

1 ncompose(f;-1+n;x) = fun(-1+n)
1 step

About:

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