proposition: Lemma dom_union_inv_L `{!RelDecision (∈@{D})} {A} (m : M A) (X1 X2 : D) : X1 ## X2 → dom m = X1 ∪ X2 → ∃ m1 m2, m = m1 ∪ m2 ∧ m1 ##ₘ m2 ∧ dom m1 = X1 ∧ dom m2 = X2.
proof: Proof. unfold_leibniz. apply dom_union_inv. Qed.
imports: stdpp(options)