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