proposition: Lemma elements_add_eq elt : forall k (v : elt) m, XMap.Equal (XMap.add k v m) (XMap.add k v (XMap.remove k m)).
proof: Proof. unfold XMap.Equal; intros. symmetry; case_eq (XMap.find (elt:=elt) y (XMap.add k v m)); intros. apply find_2 in H. rewrite (@add_mapsto_iff _ m k y v e) in H; intuition; subst. apply find_1; eauto. exact (XMap.is_bst _). apply add_1; eauto. apply find_1; eauto. exact (XMap.is_bst _). apply add_2; eauto. apply remove_2; eauto. exact (XMap.is_bst _). rewrite <- not_find_in_iff in *. intro; apply H. destruct H0. rewrite (@add_mapsto_iff _ (XMap.remove k m) k y v x) in H0; intuition; subst. eexists; eapply add_1; eauto. rewrite (@remove_mapsto_iff _ m k y x) in H2; intuition. eexists; eauto. apply add_2; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.FSets.FMapAVL Coq.ZArith.ZArith Fiat.Common Fiat.Common.List.ListFacts Fiat.Common.List.FlattenList Fiat.Common.SetEqProperties Fiat.Common.FMapExtensions Fiat.Common.List.PermutationFacts Fiat.QueryStructure.Specification.SearchTerms.ListPrefix