Nuprl - Proof: hsimp rec wd 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. 'a : S
2. x : 'a
3. f : 'a

'a
4. n :

5. fun :

'a
6. simp_rec_rel(fun,x,f,n+1)

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

By:	Unab [`hsimp_rec_rel`] THEN Simp THEN StrongAuto

Generated subgoal:

1 6. fun(0) = x
7. m:. m<n+1 fun(m+1) = f(fun(m))
ncompose(f;n;x) = fun(n)
8 steps

About:

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