proposition: Lemma merge_diag {A C} (f : option A → option A → option C) (m : M A) : merge f m m = omap (λ x, f (Some x) (Some x)) m.
proof: Proof. apply map_eq. intros i. rewrite lookup_merge, lookup_omap. by destruct (m !! i). Qed.
imports: Coq(Permutation) stdpp(options)