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