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