T318
(<=> (and (exists ?X (f ?X)) (forall ?X (forall ?Y (=> (and (f ?X) (f ?Y)) (= ?X ?Y))))) (exists ?Y (forall ?X (<=> (f ?X) (= ?X ?Y)))))
Proof Trace