IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
set inc wrt imp A:Type, B,B':(AProp).
(x:A. B(x) B'(x)) {x:A| B(x) } {x:A| B'(x) }
By:
UnivCD THEN Analyze THEN Analyze-1 THEN Analyze THEN BackThru: Hyp:-3
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
A:Type, B,B':(A
Prop).
(
B'(x)) 
{x:A| B'(x) }
