proposition: Lemma map_singleton_subseteq_l {A} i (x : A) (m : M A) : {[i := x]} ⊆ m ↔ m !! i = Some x.
proof: Proof. rewrite map_subseteq_spec. setoid_rewrite lookup_singleton_Some. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)