proposition: Lemma update_find_r : ∀ k elt (m1 m2 : M.t elt), ~ M.In k m1 → M.find k (P.update m1 m2) = M.find k m2.
proof: Proof. intros. unfold P.update. apply P.fold_rec_bis; intros. - rewrite <- H0; assumption. - rewrite F.empty_o. apply F.not_find_in_iff; assumption. - destruct (E.eq_dec k0 k). rewrite !F.add_eq_o; trivial. rewrite !F.add_neq_o; trivial. Qed.
imports: Coq.Unicode.Utf8 Coq.FSets.FMapFacts