Succ00
Premises:
(forall ?X (not (= 0 (succ ?X)))) (forall (?X ?Y) (=> (= (succ ?X) (succ ?Y)) (= ?X ?Y))) (forall (?X ?Y) (<=> (= (succ ?X) (succ ?Y)) (= ?X ?Y)))
Conclusion:
(forall (?X ?Y) (=> (= ?X ?Y) (= (succ ?X) (succ ?Y))))
Proof Trace