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

1

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

7 steps

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