proposition: Lemma Finite_alt_deprecated A (d:decidable_eq A) : Finite A <-> Finite' A.
proof: Proof. split. - intros F. now apply Finite_dec. - intros (l & _ & F). now exists l. Qed.
imports: List PeanoNat Compare_dec EqNat Decidable ListDec