proposition: Lemma map_disjoint_delete_l {A} (m1 m2 : M A) i : m1 ##ₘ m2 → delete i m1 ##ₘ m2.
proof: Proof. rewrite !map_disjoint_alt. intros Hdisjoint j. destruct (Hdisjoint j); auto. rewrite lookup_delete_None. tauto. Qed.
imports: Coq(Permutation) stdpp(options)