a,z:, n:, s:({a...z}{1...n}Peg), n':.
  nn'
  
  (h:({n+1...n'}Peg). (s(?) {to n}  h {to n'})  {a...z}{1...n'}Peg)

By:	Def of <fun>(?) {to <nat>}  <fun> {to <nat>}

None

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