proposition: Lemma app_eq_prefix A (l : list A) l' : l ++ l' = l <-> l' = nil.
proof: Proof. split; ins; desf; auto using app_nil_r. induction l; ins; desf; eauto. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation