List of theorems

List of theorems in general/Basic_arithmetic_implies_Peano_axioms.gh:

(= (succ a) (+ a (1)))
(↔ (= (succ a) (succ b)) (= a b))
(= (+ a (0)) a)
(= (+ a (succ b)) (succ (+ a b)))
(= (· a (0)) (0))
(= (· a (succ b)) (+ a (· a b)))
(→ (∧ (subst (0) n φ) (∀ k (→ (subst k n φ) (subst (succ k) n φ)))) (∀ n φ))
(¬ (= (0) (succ a)))