proposition: Lemma insert_mono {A} (m1 m2 : M A) i x : m1 ⊆ m2 → <[i:=x]> m1 ⊆ <[i:=x]>m2.
proof: Proof. rewrite !map_subseteq_spec. intros Hm j y. rewrite !lookup_insert_Some. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)