proposition: Lemma map_not_agree {A} (m1 m2 : M A) `{!EqDecision A}: ¬map_agree m1 m2 ↔ ∃ i x1 x2, m1 !! i = Some x1 ∧ m2 !! i = Some x2 ∧ x1 ≠ x2.
proof: Proof. unfold map_agree. rewrite map_not_Forall2 by solve_decision. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)