proposition: Lemma delete_insert_subseteq {A} (m1 m2 : M A) i x : m1 !! i = Some x → delete i m1 ⊆ m2 → m1 ⊆ <[i:=x]> m2.
proof: Proof. rewrite !map_subseteq_spec. intros Hix Hi j y Hj. destruct (decide (i = j)) as [->|?]. - rewrite lookup_insert. congruence. - rewrite lookup_insert_ne by done. apply Hi. by rewrite lookup_delete_ne. Qed.
imports: Coq(Permutation) stdpp(options)