proposition: Lemma Permutation_elements_filter B : forall (f : B -> bool) container, Permutation (map snd (MValues.elements (MValuesProperties.filter (fun _ => f) container))) (map snd (List.filter (fun kv => f (snd kv))(MValues.elements container))).
proof: Proof. intros. intros; eapply Permutation_InA_cons. eapply NoDupA_filter; eapply MValues.elements_3w. eapply MValues.elements_3w. intros. rewrite filter_InA, <- !elements_mapsto_iff, MValuesProperties.filter_iff; eauto with typeclass_instances. unfold Proper, respectful; intros. destruct H; rewrite H0; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties Coq.Arith.Peano_dec Coq.Structures.OrdersEx Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.FSets.FMapAVL Coq.ZArith.ZArith Fiat.Common Fiat.Common.String_as_OT Fiat.Common.List.ListFacts Fiat.Common.List.FlattenList Fiat.Common.SetEqProperties Fiat.Common.FMapExtensions Fiat.Common.List.PermutationFacts Fiat.QueryStructure.Specification.SearchTerms.ListInclusion