PA008
Premises:
(forall ?X (= (+ 0 ?X) ?X))
Conclusion:
(= (+ 0 (succ a)) (succ a))
Proof Trace