PA007a
Premises:
(= (+ 0 a) a) (= (+ 0 (succ a)) (succ (+ 0 a)))
Conclusion:
(= (+ 0 (succ a)) (succ a))
Proof Trace