T313
(<= (= x y) (exists ?Z (and (= ?Z x) (= ?Z y))))
Proof Trace