proposition: Lemma map_singleton_subseteq {A} i j (x y : A) : {[i := x]} ⊆@{M A} {[j := y]} ↔ i = j ∧ x = y.
proof: Proof. rewrite map_subseteq_spec. setoid_rewrite lookup_singleton_Some. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)