proposition: Lemma map_eq_snoc A B (f : A -> B) l y ys : map f l = ys ++ y :: nil <-> exists x l', l = l' ++ x :: nil /\ y = f x /\ map f l' = ys.
proof: Proof. rewrite map_eq_app; split; ins; desf; eauto. rewrite map_eq_singleton in *; desf; eauto. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation