proposition: Lemma insert_delete_subset {A} (m1 m2 : M A) i x : m1 !! i = None → <[i:=x]> m1 ⊂ m2 → m1 ⊂ delete i m2.
proof: Proof. intros ? [Hm12 Hm21]; split; [eauto using insert_delete_subseteq|]. contradict Hm21. apply delete_insert_subseteq; auto. eapply lookup_weaken, Hm12. by rewrite lookup_insert. Qed.
imports: Coq(Permutation) stdpp(options)