T308
(=> (= x y) (<=> (f x) (f y)))
Proof Trace