forall a:
forall Q:a->a:
Q<I:a => Q^ = Q