proposition: Lemma map_agree_alt {A} (m1 m2 : M A) : map_agree m1 m2 ↔ ∀ i, m1 !! i = None ∨ m2 !! i = None ∨ m1 !! i = m2 !! i.
proof: Proof. apply forall_proper; intros i; destruct (m1 !! i), (m2 !! i); naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)