forall a: forall b:
forall Q:a->b:
forall R:a->b:
I:a&(Q&R);(Q&R)^
= I:a&R;Q^