proposition: Lemma nodup_list_of_finite P (P_fin : finite P) : nodup (list_of_finite P_fin).
proof: Proof. unfold list_of_finite. destruct (cid (iff_impl_subrelation (finite P) (exists l : list A, P [=] of_list l /\ nodup l) (finite_eq_nodup P) P_fin)). tauto. Qed.
imports: Coq(Basics Morphisms Setoid) CoLoR(ClassicUtil IotaUtil EpsilonUtil LogicUtil NatUtil FunUtil ListUtil ListNodup SetUtil BoundNat)