proposition: Lemma kmap_merge {A B C} (g : option A → option B → option C) (m1 : M1 A) (m2 : M1 B) : kmap f (merge g m1 m2) = merge g (kmap f m1) (kmap f m2).
proof: Proof. apply map_eq; intros j. apply option_eq; intros y. rewrite lookup_merge, lookup_kmap_Some. setoid_rewrite lookup_merge. split. { intros [i [-> ?]]. by rewrite !lookup_kmap. } intros Hg. destruct (kmap f m1 !! j) as [x1|] eqn:Hm1. { apply lookup_kmap_Some in Hm1 as (i&->&Hm1i). exists i. split; [done|]. by rewrite Hm1i, <-lookup_kmap. } destruct (kmap f m2 !! j) as [x2|] eqn:Hm2; [|naive_solver]. apply lookup_kmap_Some in Hm2 as (i&->&Hm2i). exists i. split; [done|]. by rewrite Hm2i, <-lookup_kmap, Hm1. Qed.
imports: Coq(Permutation) stdpp(options)