IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
The proof here illustrates how the evaluation of the extract of one theorem
Thm* 
a,b:
. Dec(a | b)
can help to prove another theorem.
For neatness, the pattern of proof here could easily be incorporated into a tactic.
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
