T328
(forall (?A ?B ?C) (=> (and (=> (exists ?Z (forall ?X (<=> (f ?X) (= ?X ?Z)))) (f ?A)) (=> (not (exists ?Z (forall ?X (<=> (f ?X) (= ?X ?Z))))) (= ?A ?C)) (=> (exists ?Z (forall ?Y (<=> (f ?Y) (= ?Y ?Z)))) (f ?B)) (=> (not (exists ?Z (forall ?Y (<=> (f ?Y) (= ?Y ?Z))))) (= ?B ?C))) (= ?A ?B)))
Proof Trace