proposition: Lemma merge_empty_r {A B C} (f : option A → option B → option C) (m1 : M A) : merge f m1 ∅ = omap (flip f None ∘ Some) m1.
proof: Proof. apply map_eq; intros i. rewrite lookup_merge, lookup_omap, lookup_empty. by destruct (m1 !! i). Qed.
imports: Coq(Permutation) stdpp(options)