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