proposition: Lemma merge_comm m1 m2 : (∀ i, f (m1 !! i) (m2 !! i) = f (m2 !! i) (m1 !! i)) → merge f m1 m2 = merge f m2 m1.
proof: Proof. intros Hm. apply map_eq; intros i. specialize (Hm i). rewrite !lookup_merge. by destruct (m1 !! i), (m2 !! i). Qed.
imports: Coq(Permutation) stdpp(options)