proposition: Lemma omap_insert {A B} (f : A → option B) (m : M A) i x : omap f (<[i:=x]>m) = (match f x with Some y => <[i:=y]> | None => delete i end) (omap f m).
proof: Proof. intros; apply map_eq; intros i'; destruct (decide (i' = i)) as [->|]. - rewrite lookup_omap, !lookup_insert. destruct (f x) as [y|] eqn:Hx; simpl. + by rewrite lookup_insert. + by rewrite lookup_delete, Hx. - rewrite lookup_omap, !lookup_insert_ne by done. destruct (f x) as [y|] eqn:Hx; simpl. + by rewrite lookup_insert_ne, lookup_omap by done. + by rewrite lookup_delete_ne, lookup_omap by done. Qed.
imports: Coq(Permutation) stdpp(options)