proposition: Lemma delete_mono {A} (m1 m2 : M A) i : m1 ⊆ m2 → delete i m1 ⊆ delete i m2.
proof: Proof. rewrite !map_subseteq_spec. intros ? j x. rewrite !lookup_delete_Some. intuition eauto. Qed.
imports: Coq(Permutation) stdpp(options)