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