proposition: Lemma NoDupA_filter : forall (A : Type) (eqA : A -> A -> Prop) (f : A -> bool) (ls : list A), NoDupA eqA ls -> NoDupA eqA (List.filter f ls).
proof: Proof. intros. induction ls. - constructor. - simpl. inversion H. subst. destruct (f a). + eapply NoDupA_cons; eauto. clear IHls H H3. intro. apply H2. clear H2. induction ls. inversion H. simpl in *. destruct (f a0). inversion H; clear H; subst. apply InA_cons_hd; eauto. apply InA_cons_tl; eapply IHls; eauto. apply InA_cons_tl; eauto. + eauto. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties Coq.Arith.PeanoNat Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.FSets.FMapAVL Fiat.Common Fiat.Common.List.ListFacts Fiat.Common.List.FlattenList Fiat.Common.SetEqProperties Fiat.Common.FMapExtensions Fiat.Common.List.PermutationFacts