IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
and functionality wrt implies P1,P2,Q1,Q2:Prop. (P1P2) (Q1Q2) P1 & Q1P2 & Q2
By:
Unfold `guard` 0 THEN HypBackchain
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html