proposition: Lemma map_img_union_inv `{!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. intros Hsep Himg. exists (filter (λ '(_,x), x ∈ X) m), (filter (λ '(_,x), x ∉ X) m). assert (filter (λ '(_,x), x ∈ X) m ##ₘ filter (λ '(_,x), x ∉ X) m). { apply map_disjoint_filter_complement. } split_and!. - symmetry. apply map_filter_union_complement. - done. - apply map_img_filter; intros x. split; [|naive_solver]. intros. destruct (elem_of_map_img_1 m x); set_solver. - apply map_img_filter; intros x; split. + intros. destruct (elem_of_map_img_1 m x); set_solver. + intros (i & ?%elem_of_map_img_2 & ?). set_solver. Qed.
imports: Coq(Permutation) stdpp(options)