Nuprl - Proof: hsimp rec wd 1 1

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

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

'a
4. n :

ncompose(f;n;x) = (@

fun:

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

By:	Unab [`bchoose`] THEN ChooseDC THEN Simp THEN StrongAuto THEN HN THEN StrongAuto THEN Try (Complete (Unfold `label` 0))

Generated subgoals:

1 5. fun : 'a
6. simp_rec_rel(fun,x,f,n+1)
ncompose(f;n;x) = fun(n)
9 steps

2 fun:('a). simp_rec_rel(fun,x,f,n+1)
2 steps

About:

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

1	5. fun : 'a 6. simp_rec_rel(fun,x,f,n+1) ncompose(f;n;x) = fun(n)	9 steps
2	fun:('a). simp_rec_rel(fun,x,f,n+1)	2 steps