# List of theorems

List of theorems in general/Triangle_congruence.gh:

(→ (∧ (= x z) (between x y z)) (= x y))
(→ (= x z) (→ (∧ (∧ (∧ (∧ (∧ (between x y z) (between x′ y′ z′)) (≡ x z x′ z′)) (≡ y z y′ z′)) (≡ x u x′ u′)) (≡ z u z′ u′)) (≡ y u y′ u′)))
(→ (∧ (∧ (between x z w) (¬ (= z w))) (∧ (∧ (between x′ z′ w′) (≡ z′ w′ z w)) (∧ (¬ (= x z)) (∧ (∧ (∧ (∧ (∧ (between x y z) (between x′ y′ z′)) (≡ x z x′ z′)) (≡ y z y′ z′)) (≡ x u x′ u′)) (≡ z u z′ u′))))) (≡ w u w′ u′))
(→ (∧ (∧ (between x z w) (¬ (= z w))) (∧ (∧ (between x′ z′ w′) (≡ z′ w′ z w)) (∧ (¬ (= x z)) (∧ (∧ (∧ (∧ (∧ (between x y z) (between x′ y′ z′)) (≡ x z x′ z′)) (≡ y z y′ z′)) (≡ x u x′ u′)) (≡ z u z′ u′))))) (≡ y u y′ u′))
(→ (¬ (= x z)) (→ (∧ (∧ (∧ (∧ (∧ (between x y z) (between x′ y′ z′)) (≡ x z x′ z′)) (≡ y z y′ z′)) (≡ x u x′ u′)) (≡ z u z′ u′)) (≡ y u y′ u′)))
(→ (∧ (∧ (∧ (∧ (∧ (between x y z) (between x′ y′ z′)) (≡ x z x′ z′)) (≡ y z y′ z′)) (≡ x u x′ u′)) (≡ z u z′ u′)) (≡ y u y′ u′))
(→ (∧ (∧ (∧ (between x y z) (between x′ y′ z′)) (≡ x z x′ z′)) (≡ y z y′ z′)) (≡ x y x′ y′))
(↔ (≅ x y z x′ y′ z′) (∧ (∧ (≡ x y x′ y′) (≡ x z x′ z′)) (≡ y z y′ z′)))
(→ (≅ A B C A′ B′ C′) (≡ A B A′ B′))
(→ (≅ A B C A′ B′ C′) (≡ B C B′ C′))
(→ (≅ A B C A′ B′ C′) (≡ A C A′ C′))
(↔ (≅ A B C A′ B′ C′) (≅ B C A B′ C′ A′))
(≅ A B C A B C)
(→ (∧ (between A B C) (≡ A C A′ C′)) (∃ d′ (∃ b′ (∃ c″ (∧ (∧ (∧ (∧ (between C′ A′ d′) (¬ (= A′ d′))) (∧ (between d′ A′ b′) (≡ A′ b′ A B))) (∧ (between d′ b′ c″) (≡ b′ c″ B C))) (∧ (between A B C) (≡ A C A′ C′)))))))
(→ (∧ (∧ (∧ (∧ (between C′ A′ D′) (¬ (= A′ D′))) (∧ (between D′ A′ B′) (≡ A′ B′ A B))) (∧ (between D′ B′ C″) (≡ B′ C″ B C))) (∧ (between A B C) (≡ A C A′ C′))) (between A′ B′ C″))
(→ (∧ (∧ (∧ (∧ (between C′ A′ D′) (¬ (= A′ D′))) (∧ (between D′ A′ B′) (≡ A′ B′ A B))) (∧ (between D′ B′ C″) (≡ B′ C″ B C))) (∧ (between A B C) (≡ A C A′ C′))) (≡ A C A′ C″))
(→ (∧ (∧ (∧ (∧ (between C′ A′ D′) (¬ (= A′ D′))) (∧ (between D′ A′ B′) (≡ A′ B′ A B))) (∧ (between D′ B′ C″) (≡ B′ C″ B C))) (∧ (between A B C) (≡ A C A′ C′))) (between D′ A′ C″))
(→ (∧ (∧ (∧ (∧ (between C′ A′ D′) (¬ (= A′ D′))) (∧ (between D′ A′ B′) (≡ A′ B′ A B))) (∧ (between D′ B′ C″) (≡ B′ C″ B C))) (∧ (between A B C) (≡ A C A′ C′))) (= C′ C″))
(→ (∧ (= C′ C″) (≡ B′ C″ B C)) (≡ B′ C′ B C))
(→ (∧ (∧ (∧ (∧ (between C′ A′ D′) (¬ (= A′ D′))) (∧ (between D′ A′ B′) (≡ A′ B′ A B))) (∧ (between D′ B′ C″) (≡ B′ C″ B C))) (∧ (between A B C) (≡ A C A′ C′))) (≅ A B C A′ B′ C′))
(→ (∧ (= C′ C″) (between A′ B′ C″)) (between A′ B′ C′))
(→ (∧ (∧ (∧ (∧ (between C′ A′ D′) (¬ (= A′ D′))) (∧ (between D′ A′ B′) (≡ A′ B′ A B))) (∧ (between D′ B′ C″) (≡ B′ C″ B C))) (∧ (between A B C) (≡ A C A′ C′))) (between A′ B′ C′))
(→ (∧ (between A B C) (≡ A C A′ C′)) (∃ b′ (∧ (between A′ b′ C′) (≅ A B C A′ b′ C′))))
(→ (∧ (between A B C) (≅ A B C A′ B′ C′)) (∃ b″ (∧ (∧ (between A′ b″ C′) (≅ A B C A′ b″ C′)) (∧ (between A B C) (≅ A B C A′ B′ C′)))))
(→ (∧ (∧ (between A′ B″ C′) (≅ A B C A′ B″ C′)) (∧ (between A B C) (≅ A B C A′ B′ C′))) (≡ A′ B″ A′ B′))
(→ (∧ (∧ (between A′ B″ C′) (≅ A B C A′ B″ C′)) (∧ (between A B C) (≅ A B C A′ B′ C′))) (≡ C′ B″ C′ B′))
(→ (∧ (∧ (between A′ B″ C′) (≅ A B C A′ B″ C′)) (∧ (between A B C) (≅ A B C A′ B′ C′))) (= B″ B′))
(→ (∧ (∧ (between A′ B″ C′) (≅ A B C A′ B″ C′)) (∧ (between A B C) (≅ A B C A′ B′ C′))) (between A′ B′ C′))
(→ (∧ (between A B C) (≅ A B C A′ B′ C′)) (between A′ B′ C′))