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