T305
(=> (and (= x y) (= z y)) (= x z))
Proof Trace