proposition: Lemma filter_NoDup : forall (A : Set)(ls : list A)(P : A -> bool), NoDup ls -> NoDup (filter P ls).
proof: Proof. induction ls; intuition; simpl in *. inversion H; clear H; subst. case_eq (P a); intuition. econstructor; intuition. eapply H2. eapply filter_In; eauto. Qed.
imports: Bvector List FCF.Blist FCF.EqDec FCF.Fold FCF.EqDec