theorem InfModel.Finite.Equation374794_implies_Equation2 (G : Type u_1) [Magma G] [Finite G] (h : Equation374794 G) : Equation2 G

In a finite model Equation374794 implies Equation2, that the model is a subsingleton.

theorem InfModel.Equation374794_not_implies_Equation2 : ∃ (G : Type) (x : Magma G), Equation374794 G ∧ ¬Equation2 G

However, Equation374794 doesn't imply Equation2.

theorem InfModel.Finite.Equation5105_implies_Equation2 (G : Type u_1) [Magma G] [Finite G] (h : Equation5105 G) : Equation2 G

theorem InfModel.Finite.Equation28770_implies_Equation2 (G : Type u_1) [Magma G] [Finite G] (h : Equation28770 G) : Equation2 G

theorem InfModel.Equation28770_not_implies_Equation2 : ∃ (G : Type) (x : Magma G), Equation28770 G ∧ ¬Equation2 G

theorem InfModel.Finite.Equation3994_implies_Equation3588 (G : Type u_1) [Magma G] [Finite G] (h : Equation3994 G) : Equation3588 G

theorem InfModel.Equation3994_not_implies_Equation3588 : ∃ (G : Type) (x : Magma G), Equation3994 G ∧ ¬Equation3588 G

theorem InfModel.Equation3588_not_implies_Equation3944 : ∃ (G : Type) (x : Magma G), Equation3588 G ∧ ¬Equation3994 G

Dual of the above, obtained by swapping x and y in the proof. TODO: find a way to avoid this kind of code duplication.