forall a:
I:a^ = I:a