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