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