forall a:
forall Q:a->a:
forall R:a->a:
(Q<I:a and R<I:a) =>
Q;R = Q&R