T328a
(=> (and (exists ?Y (forall ?X (<=> (F ?X) (= ?X ?Y)))) (F a) (F b)) (= a b))
Proof Trace