T309
(<=> (f x) (forall ?Y (=> (= ?Y x) (f ?Y))))
Proof Trace