Hmm. It seems the way to plug the whole is some more stringent requirement on the A when we judge Gamma |- x / A.
