proposition: Lemma omap_insert_Some {A B} (f : A → option B) (m : M A) i x y : f x = Some y → omap f (<[i:=x]>m) = <[i:=y]>(omap f m).
proof: Proof. intros Hx. by rewrite omap_insert, Hx. Qed.
imports: Coq(Permutation) stdpp(options)