Nuprl - Proof: hsimp rec wd 1 1 1 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. '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+1

fun(m+1) = f(fun(m)))

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

. m<n+1

fun(m+1) = f(fun(m))

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

By:	InstHyp [n-1] 9 THEN StrongAuto THEN Try (Complete (Unfold `label` 0))

Generated subgoal:

1 10. fun(n-1+1) = f(fun(n-1))
f(ncompose(f;n-1;x)) = fun(n)
6 steps

About:

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