proposition: Lemma merge_Some (m1 : M A) (m2 : M B) (m : M C) : f None None = None → (∀ i, m !! i = f (m1 !! i) (m2 !! i)) ↔ merge f m1 m2 = m.
proof: Proof. intros. rewrite map_eq_iff. apply forall_proper; intros i. rewrite lookup_merge. destruct (m1 !! i), (m2 !! i); naive_solver congruence. Qed.
imports: Coq(Permutation) stdpp(options)