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