proposition: Lemma Permutation_elements_update B : forall m1 m2, (forall x, InA (@MValues.eq_key _) x (MValues.elements m1) -> ~ InA (@MValues.eq_key _) x (MValues.elements m2)) -> Permutation (map snd (MValues.elements (MValuesProperties.update (elt := B) m1 m2))) (map snd (MValues.elements m1) ++ map snd (MValues.elements m2)).
proof: Proof. intros; rewrite <- map_app; apply Permutation_InA_cons. eapply NoDupA_app; eauto using MValues.elements_3w with typeclass_instances. eapply MValues.elements_3w. intros. rewrite InA_app_iff, <- !elements_mapsto_iff by (eauto with typeclass_instances). rewrite MValuesProperties.update_mapsto_iff; intuition. right; intuition. rewrite elements_mapsto_iff in H1; eapply H with (x := (k, v)); eauto. revert H1; clear; induction (MValues.elements m1); intros; inversion H1; subst; eauto. destruct H0; constructor; eauto. destruct H0; rewrite elements_mapsto_iff in H0; revert H0; clear; induction (MValues.elements m2); intros; inversion H0; subst; eauto. destruct H1; simpl in *; constructor; 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