proposition: Lemma map_eq_app A B (f : A -> B) l l1' l2' : map f l = l1' ++ l2' <-> exists l1 l2, l = l1 ++ l2 /\ map f l1 = l1' /\ map f l2 = l2'.
proof: Proof. split; ins; desf; auto using map_app. revert dependent l1'; induction l; destruct l1'; ins; desf. - exists nil, nil; ins. - eexists nil, (_ :: _); ins. - apply IHl in H; desf; eexists (_ :: _), _; ins. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation