T311
(<=> (and (f x) (= x y)) (and (f y) (= x y)))
Proof Trace