T302
(=> (= x y) (= y x))
Proof Trace