proposition: Lemma omap_singleton {A B} (f : A → option B) i x : omap f {[ i := x ]} =@{M B} match f x with Some y => {[ i:=y ]} | None => ∅ end.
proof: Proof. rewrite <-insert_empty, omap_insert, omap_empty. destruct (f x) as [y|]; simpl. - by rewrite insert_empty. - by rewrite delete_empty. Qed.
imports: Coq(Permutation) stdpp(options)