proposition: Lemma filter_NoDup : forall (A : Set)(ls : list A)(P : A -> bool), NoDup ls -> NoDup (filter P ls).
proof: Proof. induction ls; simpl in *; intuition. inversion H; clear H; subst. destruct (P a). econstructor; eauto. intuition. eapply filter_In in H. intuition. eapply IHls; eauto. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia