T310
(<=> (f x) (exists ?Y (and (= ?Y x) (f ?Y))))
Proof Trace