IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
and preserved by T:Type, P,Q:(TProp), R:(TTProp).
R preserves PR preserves QR preserves PQ
By:
Unfolds [`prop_and`;`preserved_by`] 0 THEN Reduce 0 THEN EasyHyp
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
T:Type, P,Q:(T
Prop), R:(T
R preserves P 
R preserves Q 
Q
