Nuprl - Proof: ncompose wf 1 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: ncompose wf 1 2

1. 'a : Type
2. f : 'a

'a
3. n :

4. 0<n
5.

x:'a. ncompose(f;n-1;x)

'a
6. x : 'a

ncompose(f;n;x)

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

Generated subgoal:

1 7. n=0
ncompose(f;n-1;x) 'a
1 step

About:

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