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

1

2. k :  3. k1:.  3. k1<k 3.  3. (a:, z:{a...}. 3. (z-ak1 3. ( 3. ((f:({a...z}Peg).  3. ((f(a) = p & f(z)  p 3. (( 3. (((x:{a...z-1}. (u:{a...x}. f(u) = p) & f(x+1)  p))) 4. a :  5. z : {a...} 6. z-ak 7. f : {a...z}Peg 8. f(a) = p 9. f(z)  p   x:{a...z-1}. (u:{a...x}. f(u) = p) & f(x+1)  p

10 steps

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