forall a: forall b:
forall Q:a->b:
forall R:a->b:
forall S:b->a:
Q<R => S;Q < S;R