P:(Prop). 
  (a:, b:{...a}. P(a,b))
  
  (a:, b:{a+1...}. (c:{a..b}. P(a,c))  P(a,b))  (a,b:. P(a,b))

1

1. P : Prop 2. a:, b:{...a}. P(a,b) 3. a:, b:{a+1...}. (c:{a..b}. P(a,c))  P(a,b)   a,b:. P(a,b)

4 steps

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