forall a: forall b:
forall Q:a->b:
Q = (I:a&Q;Q^);Q