proposition: Lemma map_img_union_inv_L `{!RelDecision (∈@{SA})} X Y m : X ## Y → map_img m = X ∪ Y → ∃ m1 m2, m = m1 ∪ m2 ∧ m1 ##ₘ m2 ∧ map_img m1 = X ∧ map_img m2 = Y.
proof: Proof. unfold_leibniz. apply map_img_union_inv. Qed.
imports: Coq(Permutation) stdpp(options)