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