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

The conclusion is "guarded" <words go here>

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