Nuprl - Proof: hsimp rec wd 1 1 2 1

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

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

'a
4. n :

5. m :

6. m<n+1

ncompose(f;m+1;x) = f(ncompose(f;m;x))

By:	Assert (0<m+1) THEN Simp THEN StrongAuto

Generated subgoals:

None

About:

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