Description: In the Separation Scheme zfauscl , we require that y not occur in
ph (which can be generalized to "not be free in"). Here we show
special cases of A and ph that result in a contradiction if that
requirement is not met. (Contributed by NM, 8-Feb-2006)(Proof
shortened by BJ, 18-Nov-2023)