p:Peg, a:, z:{a...}, f:({a...z}Peg).
  f(a) = p & f(z)  p  (x:{a...z-1}. (u:{a...x}. f(u) = p) & f(x+1)  p)

By:	Guarding (a:<type>. <prop>) Auto

1

1. p : Peg   a:, z:{a...}, f:({a...z}Peg).   f(a) = p & f(z)  p  (x:{a...z-1}. (u:{a...x}. f(u) = p) & f(x+1)  p)

13 steps

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