T311b
(<= (and (f x) (= x y)) (and (f y) (= x y)))
Proof Trace