Nuprl - Proof: hsimp rec wd 1 1 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 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-1+1) = f(fun(n-1))
10. m :

11. m<n-1+1

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

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

Generated subgoals:

None

About:

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