proposition: Lemma omap_delete {A B} (f: A → option B) (m : M A) i : omap f (delete i m) = delete i (omap f m).
proof: Proof. apply map_eq; intros i'; destruct (decide (i' = i)) as [->|]. - by rewrite lookup_omap, !lookup_delete. - by rewrite lookup_omap, !lookup_delete_ne, lookup_omap by done. Qed.
imports: Coq(Permutation) stdpp(options)