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