proposition: Lemma finite_countable s (F: set_finite s) : countable s.
proof: Proof. destruct F as [l H]; red. destruct (classic (inhabited A)) as [[a]|]; auto. right; exists (fun i => nth i (undup (filterP s l)) a). right; exists (length (undup (filterP s l))); splits; unnw; ins. - apply nth_In with (d:=a) in LTi. rewrite in_undup_iff, in_filterP_iff in LTi; desf. - eapply NoDup_nth; eauto. - apply In_nth, in_undup_iff, in_filterP_iff; eauto. Qed.
imports: Arith micromega.Lia Setoid IndefiniteDescription ClassicalChoice HahnBase HahnList HahnEquational HahnRewrite HahnRelationsBasic HahnSets HahnNatExtra HahnListBefore HahnWf HahnSorted HahnTotalExt