i:, E:({...i}Prop).
  E(i)  (k:{...i-1}. E(k+1)  E(k))  (k:{...i}. E(k))

1

1. i :  2. E : {...i}Prop 3. E(i) 4. k:{...i-1}. E(k+1)  E(k)   k:{...i}. E(k)

6 steps

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