proposition: Lemma map_eq_singleton A B (f : A -> B) l y : map f l = y :: nil <-> exists x, l = x :: nil /\ y = f x.
proof: Proof. split; ins; desf. destruct l as [|?[|??]]; ins; desf; eauto. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation