proposition: Lemma nodup_append A (l1 l2: list A) : NoDup l1 -> NoDup l2 -> disjoint l1 l2 -> NoDup (l1 ++ l2).
proof: Proof. generalize nodup_app; firstorder. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation