proposition: Lemma Permutation_elements_map B C : forall (f : B -> C) container, Permutation (map snd (MValues.elements (MValues.map f container))) (map snd (List.map (fun kv => (fst kv, f (snd kv))) (MValues.elements container))).
proof: Proof. intros. intros; eapply Permutation_InA_cons. - generalize (MValues.elements_3w container). induction (MValues.elements container); simpl; constructor. + inversion H; subst; intro; apply H2. revert H0; clear; induction l; simpl; intros; inversion H0; subst. * econstructor; eapply H1. * econstructor 2; eauto. + inversion H; subst; eauto. - eapply MValues.elements_3w. - intros. rewrite <- !elements_mapsto_iff, map_mapsto_iff. setoid_rewrite elements_mapsto_iff. induction (MValues.elements container); simpl; intuition. + destruct_ex; intuition; inversion H1. + inversion H. + destruct_ex; intuition; subst; inversion H3; subst. * simpl; econstructor 1. destruct H2; split; simpl in *; f_equal; eauto. * econstructor 2; eauto. + simpl in *; inversion H1; subst. * eexists b; split. eapply H3. econstructor; destruct H3; split; simpl in *; eauto. * apply H0 in H3; destruct_ex; intuition; eexists; eauto. 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