T312
(<=> (= x y) (forall ?Z (=> (= ?Z x) (= ?Z y))))
Proof Trace