proposition: Lemma Finite_eqdec {X : Type} (U : Ensemble X) : Finite U -> forall x y : X, In U x -> In U y -> x = y \/ x <> y.
proof: Proof. intros HU x y Hx Hy. induction HU. { contradiction. } destruct Hx, Hy; auto. all: repeat match goal with | H : In (Singleton _) _ |- _ => apply Singleton_inv in H end. - right. intros ?; subst; auto. - right. intros ?; subst; auto. - left. subst. auto. Qed.
imports: Coq(Classical Lia) ZornsLemma(DecidableDec EnsemblesImplicit Families FiniteImplicit FunctionPropertiesEns Powerset_facts Image InverseImage ReverseMath.AddSubtract)