PA003
Premises:
(forall ?X (= (+ ?X 0) ?X)) (forall ?X (forall ?Y (= (+ ?X (succ ?Y)) (succ (+ ?X ?Y)))))
Conclusion:
(= (succ (+ (succ 0) 0)) (succ (succ 0)))
Proof Trace