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