# List of theorems

List of theorems in general/First-order_logic_with_quantifiability.gh:

(→ φ (= s t))(→ φ (= t s))
(→ φ (= s t)) , (→ φ (= t u))(→ φ (= s u))
(→ (= s0 s1) (↔ (= s0 t) (= s1 t)))
(→ (↔ (= s0 t0) (= s1 t1)) (↔ (= t0 s0) (= t1 s1)))
(→ (= s0 s1) (↔ (= t s0) (= t s1)))
(→ (∧ (= s0 s1) (= t0 t1)) (↔ (= s0 t0) (= s1 t1)))
(= s0 s1) , (= t0 t1)(↔ (= s0 t0) (= s1 t1))
(= s0 s1)(↔ (= s0 t) (= s1 t))
(= t0 t1)(↔ (= s t0) (= s t1))
(→ φ (= s0 s1)) , (→ φ (= t0 t1))(→ φ (↔ (= s0 t0) (= s1 t1)))
(→ φ (= s0 s1))(→ φ (↔ (= s0 t) (= s1 t)))
(→ φ (= t0 t1))(→ φ (↔ (= s t0) (= s t1)))
(↔ (subst s x φ) (∃ y (∧ (= y s) (∃ x (∧ (= x y) φ)))))
(→ (= s t) (↔ (subst s x φ) (subst t x φ)))
(= s t)(↔ (subst s x φ) (subst t x φ))
(→ (∀ x (→ φ ψ)) (→ (subst s x φ) (subst s x ψ)))
(→ φ ψ)(→ (subst s x φ) (subst s x ψ))
(→ (∀ x (↔ φ ψ)) (↔ (subst s x φ) (subst s x ψ)))
(↔ φ ψ)(↔ (subst s x φ) (subst s x ψ))
(→ (subst s x φ) (∃ x φ))
(subst s x φ)(∃ x φ)
(→ (∀ x φ) (subst s x φ))
(→ antecedent (∀ x φ))(→ antecedent (subst s x φ))
(→ (∀ x (→ (= x s) (↔ φ ψ))) (↔ (∀ x (→ (= x s) φ)) ψ))
(→ (= x s) (↔ φ ψ))(↔ (∀ x (→ (= x s) φ)) ψ)
(→ (∀ x (→ (= x s) (↔ φ ψ))) (↔ (∃ x (∧ (= x s) φ)) ψ))
(→ (= x s) (↔ φ ψ))(↔ (∃ x (∧ (= x s) φ)) ψ)
(→ (= x s) φ)φ
(→ (= x s) (↔ φx φs)) , φxφs
(→ (= x s) (→ φ (∀ x (→ (= x s) φ))))
(↔ (∃ x (∧ (= x s) φ)) (∀ x (→ (= x s) φ)))
(↔ (subst s x φ) (∃ x (∧ (= x s) φ)))
(↔ (subst s x φ) φ)
(↔ (∀ x (→ (= x s) (¬ φ))) (¬ (∃ x (∧ (= x s) φ))))
(↔ (subst s x (¬ φ)) (¬ (subst s x φ)))
(↔ (subst s x (∨ φ ψ)) (∨ (subst s x φ) (subst s x ψ)))
(↔ (subst s x (∧ φ ψ)) (∧ (subst s x φ) (subst s x ψ)))
(↔ (subst s x (→ φ ψ)) (→ (subst s x φ) (subst s x ψ)))
(↔ (subst s x (↔ φ ψ)) (↔ (subst s x φ) (subst s x ψ)))
(↔ (subst s x (∃ y φ)) (∃ y (subst s x φ)))
(↔ (subst s y (subst y x φ)) (subst s x φ))
φ(subst s x φ)
(→ (= x s) (↔ φ ψ))(↔ (subst s x φ) ψ)
(→ (= x s) (→ φ (subst s x φ)))
(→ (= x s) (→ (subst s x φ) φ))
(→ (= x s) (↔ φ (subst s x φ)))
(↔ (subst x x φ) φ)
(→ (= x s) (↔ φ (subst s x φ)))
(↔ (∃ x φ) (∃ y (subst y x φ)))
(↔ (∀ x φ) (∀ y (subst y x φ)))
(→ (= x y) (↔ φx φy))(↔ (subst s x φx) (subst s y φy))