proposition: Lemma map_union_cancel_l {A} (m1 m2 m3 : M A) : m1 ##ₘ m3 → m2 ##ₘ m3 → m3 ∪ m1 = m3 ∪ m2 → m1 = m2.
proof: Proof. intros. apply (anti_symm (⊆)); apply map_union_reflecting_l with m3; by try apply reflexive_eq. Qed.
imports: Coq(Permutation) stdpp(options)