proposition: Lemma map_disjoint_difference_l {A} (m1 m2 : M A) : m1 ⊆ m2 → m2 ∖ m1 ##ₘ m1.
proof: Proof. intros Hm i; specialize (Hm i). unfold difference, map_difference; rewrite lookup_difference_with. by destruct (m1 !! i), (m2 !! i). Qed.
imports: Coq(Permutation) stdpp(options)