proposition: Lemma Finite_dec {A:Type}: Finite A /\ decidable_eq A <-> Finite' A.
proof: Proof. split. - intros ((l, Hfull) & Hdec). destruct (uniquify Hdec l) as (l' & H_nodup & H_inc). exists l'. split; trivial. intros a. apply H_inc. apply Hfull. - intros (l & Hlist). apply Listing_decidable_eq in Hlist as Heqdec. destruct Hlist as (Hnodup & Hfull). split; [ exists l | ]; assumption. Qed.
imports: List PeanoNat Compare_dec EqNat Decidable ListDec