PA007b
Premises:
(= (+ 0 a) a) (= (+ 0 (succ a)) (succ (+ 0 a))) (forall ?X (forall ?Y (=> (= ?X ?Y) (= (succ ?X) (succ ?Y)))))
Conclusion:
(= (+ 0 (succ a)) (succ a))
Proof Trace