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