proposition: Lemma map_disjoint_singleton_l {A} (m: M A) i x : {[i:=x]} ##ₘ m ↔ m !! i = None.
proof: Proof. rewrite !map_disjoint_spec. setoid_rewrite lookup_singleton_Some. destruct (m !! i) eqn:?; naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)