proposition: Lemma snoc_eq_singleton A (l : list A) a a' : l ++ a :: nil = a' :: nil <-> l = nil /\ a = a'.
proof: Proof. rewrite app_cons_eq_singleton; split; ins; desf; eauto. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation