proposition: Lemma map_union_comm {A} (m1 m2 : M A) : m1 ##ₘ m2 → m1 ∪ m2 = m2 ∪ m1.
proof: Proof. intros Hdisjoint. apply (merge_comm (union_with (λ x _, Some x))). intros i. specialize (Hdisjoint i). destruct (m1 !! i), (m2 !! i); compute; naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)