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