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

By:	Inst:  Thm*  P:(Prop), a:. Thm*  (b:{...a}. P(a,b)) Thm*   Thm*  (b:{a+1...}. (c:{a..b}. P(a,c))  P(a,b))  (b:. P(a,b)) Using:[P | a]

1	5. b : {...a}   P(a,b)	1 step
2	5. b : {a+1...} 6. c:{a..b}. P(a,c)   P(a,b)	1 step

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