proposition: Lemma map_agree_singleton_l {A} (m: M A) i x : map_agree {[i:=x]} m ↔ m !! i = Some x ∨ m !! i = None.
proof: Proof. rewrite map_agree_spec. setoid_rewrite lookup_singleton_Some. destruct (m !! i) eqn:?; naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)