proposition: Lemma NoDup_concat_simpl A (a : A) l1 l2 ll (ND: NoDup (concat ll)) (K: In l1 ll) (K' : In a l1) (L: In l2 ll) (L' : In a l2) : l1 = l2.
proof: Proof. apply in_split_perm in K; desc; rewrite K, concat_cons, nodup_app in *; ins; desf. edestruct ND1; eauto using in_concat. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation