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