1. a : 
2. b:, P:({a..b}Prop). ba  ((i:{a..b}. P(i))  (Or i:{a..b}. P(i)))
3. k : 
4. 0<k
5. b:. 
5. b-a = k-1  (P:({a..b}Prop). (i:{a..b}. P(i))  (Or i:{a..b}. P(i)))
6. b : 
7. b-a = k
8. P : {a..b}Prop
  (i:{a..b}. P(i))  (Or i:{a..b}. P(i))

By:	Rewrite by Thm*  a,b:, P:({a..b}Prop). Thm*  a<b  ((i:{a..b}. P(i))  (i:{a..(b-1)}. P(i))  P(b-1)) THEN Rewrite by Thm*  f:(AAA), u:A, a,b:, e:({a..b}A). Thm*  a<b Thm*   Thm*  (Iter(f;u) i:{a..b}. e(i)) = f((Iter(f;u) i:{a..b-1}. e(i)),e(b-1)) THEN Reduce Concl

1

(i:{a..(b-1)}. P(i))  P(b-1)  (Or i:{a..b-1}. P(i))  P(b-1)

1 step

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