T316
(=> (= ?X ?Y) (= (A ?X) (A ?Y)))
Proof Trace