proposition: Lemma update_add : ∀ k elt e (m1 m2 : M.t elt), M.Equal (P.update m1 (M.add k e m2)) (M.add k e (P.update m1 m2)).
proof: Proof. intros. apply F.Equal_mapsto_iff; split; intros. apply P.update_mapsto_iff in H. destruct H. simplify_maps. simplify_maps. simplify_maps. right; intuition. apply P.update_mapsto_iff. left; assumption. destruct H. simplify_maps. destruct (E.eq_dec k k0) eqn:Heqe. left; intuition; subst. contradiction H0. apply F.in_find_iff. rewrite F.add_eq_o; trivial. unfold not; intros. discriminate. right; intuition. apply P.update_mapsto_iff. right; intuition. apply H0. apply F.in_find_iff. rewrite F.add_neq_o; trivial. apply F.in_find_iff; trivial. simplify_maps; apply P.update_mapsto_iff. left. simplify_maps. apply P.update_mapsto_iff in H4. destruct H4. left. simplify_maps. destruct H. right; intuition. destruct (proj1 (in_mapsto_iff _ _ _) H1). simplify_maps. apply H0. apply in_mapsto_iff. exists x. assumption. Qed.
imports: Coq.Unicode.Utf8 Coq.FSets.FMapFacts