1. 'a : S
2. x : 'a
3. f : 'a  'a
4. n : 
  fun:('a). simp_rec_rel(fun,x,f,n+1)

By:	((DTerm (m:. ncompose(f;m;x)) 0) THEN (Unab [`hsimp_rec_rel`])) THEN Simp THEN StrongAuto THEN HN THEN StrongAuto THEN Try (Complete (Unfold `label` 0))

1

5. m :  6. m<n+1   ncompose(f;m+1;x) = f(ncompose(f;m;x))

1 step

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