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