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′))