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