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