proposition: Lemma map_agree_singleton_r {A} (m : M A) i x : map_agree m {[i := x]} ↔ m !! i = Some x ∨ m !! i = None.
proof: Proof. by rewrite (symmetry_iff map_agree), map_agree_singleton_l. Qed.
imports: Coq(Permutation) stdpp(options)