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