proposition: Lemma update_empty_r : ∀ elt (m : M.t elt), M.Equal (P.update m (M.empty _)) m.
proof: Proof. intros. apply F.Equal_mapsto_iff; split; intros. simplify_maps. simplify_maps. right; intuition. apply F.empty_in_iff in H0. assumption. Qed.
imports: Coq.Unicode.Utf8 Coq.FSets.FMapFacts