proposition: Lemma update_find_l : ∀ k elt (m1 m2 : M.t elt), ~ M.In k m2 → M.find k (P.update m1 m2) = M.find k m1.
proof: Proof. intros. unfold P.update. apply P.fold_rec_bis; intros; auto. destruct (E.eq_dec k0 k). rewrite e0 in H0. contradiction H. exists e. assumption. rewrite !F.add_neq_o; trivial. Qed.
imports: Coq.Unicode.Utf8 Coq.FSets.FMapFacts