proposition: Lemma finite_eq_dec: forall X:Type, FiniteT X -> forall x y:X, x = y \/ x <> y.
proof: Proof. intros. induction H. { destruct x. } { destruct x, y. 4: left; reflexivity. 2, 3: right; congruence. specialize (IHFiniteT t t0) as [|]; [left|right]; congruence. } destruct H0. specialize (IHFiniteT (g x) (g y)) as [|]. - left. rewrite <- H1. rewrite <- H1 with x. rewrite H2. reflexivity. - right. contradict H2. rewrite H2. reflexivity. Qed.
imports: Coq(Arith Description FunctionalExtensionality Lia) ZornsLemma(DecidableDec Finite_sets FunctionProperties Image IndexedFamilies Powerset_facts) Coq(ProofIrrelevance)