T312c
(<=> (= ?X ?Y) (forall ?Z (=> (= ?Z ?X) (= ?Z ?Y))))
Proof Trace