T2-335
(<=> (and (exists ?Y (= ?Y ?X)) (P)) (P))
Proof Trace