1. i : 
2. j : 
3. F : {i..j}Prop
4. k:{i..j}. Dec(F(k))
5. Dec(k:{i..j}. F(k))
6. Dec((k:{i..j}. F(k)))
  Dec(k:{i..j}. F(k))

By:	Rewrite-1 by Thm* Q:(TProp). (x:T. Q(x))  (x:T. Q(x))

1

7. Dec(k:{i..j}. F(k))   Dec(k:{i..j}. F(k))

1 step

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