proposition: Lemma omap_merge {D} (g : C → option D) (m1 : M A) (m2 : M B) : omap g (merge f m1 m2) = merge (λ mx1 mx2, f mx1 mx2 ≫= g) m1 m2.
proof: Proof. apply map_eq; intros i. rewrite lookup_omap, !lookup_merge. by destruct (m1 !! i), (m2 !! i). Qed.
imports: Coq(Permutation) stdpp(options)