proposition: Lemma map_not_disjoint {A} (m1 m2 : M A) : ¬m1 ##ₘ m2 ↔ ∃ i x1 x2, m1 !! i = Some x1 ∧ m2 !! i = Some x2.
proof: Proof. unfold disjoint, map_disjoint. rewrite map_not_Forall2 by solve_decision. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)