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