T316a
(=> (= x y) (= (A x) (A y)))
Proof Trace