T321
(exists ?X (= ?X y))
Proof Trace