proposition: Lemma destruct_end A (l : list A) : l = nil \/ exists l' a, l = l' ++ a :: nil.
proof: Proof. induction l; ins; desf; eauto. - right; exists nil; ins; eauto. - right; eexists (_ :: _); ins; eauto. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation