proposition: Lemma NoDup_concatD A (l: list A) ll : NoDup (concat ll) -> In l ll -> NoDup l.
proof: Proof. ins; apply in_split_perm in H0; desf. rewrite H0, concat_cons, nodup_app in H; desf. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation