`MIEnvIsEmpty` and `MIEnvTransform` have inconsistent behaviors
In an affine logic, MIEnvTransform will clear the hypotheses that fail to be transformed, while MIEnvIsEmpty would fail if the environment is not empty. This is inconsistent.
The same remark applies to MIEnvForall.