proposition: Lemma NoDup_filter_in_map : forall (A B: Type) (f: A -> bool) (m: A -> B) (l: list A), NoDup (map m l) -> NoDup (map m (filter f l)).
proof: Proof. intros; induction l. - intuition. - simpl in *. destruct (f a). + simpl; apply NoDup_cons. * apply NoDup_remove_2 with (l:=[]) in H; simpl in H. unfold not; intros. apply in_map_iff in H0; destruct H0; destruct H0. apply filter_In in H1; destruct H1. apply in_map with (f:=m) in H1. rewrite -> H0 in H1. contradiction. * apply IHl; apply NoDup_remove_1 with (l:=[]) (a:=m a); intuition. + apply IHl; apply NoDup_remove_1 with (l:=[]) (a:=m a); intuition. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.Program.Program Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.CountingListBags Fiat.QueryStructure.Implementation.DataStructures.Bags.TreeBags Fiat.QueryStructure.Specification.Representation.Tuple Fiat.QueryStructure.Specification.Representation.Heading Fiat.Common.ilist Coq.Bool.Bool Coq.Strings.String Coq.Arith.Arith Coq.Structures.OrderedTypeEx Fiat.Common.String_as_OT Fiat.Common.i2list Fiat.Common.DecideableEnsembles Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.Ensembles.EnsembleListEquivalence Fiat.ADTRefinement.GeneralBuildADTTactics Fiat.Common.List.PermutationFacts Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsOfTuples Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.QueryStructure.Implementation.DataStructures.BagADT.BagADT Fiat.Common.List.ListFacts TransparentAbstract