proposition: Lemma nodup_app: forall (A: Type) (l1 l2: list A), NoDup (l1 ++ l2) <-> NoDup l1 /\ NoDup l2 /\ disjoint l1 l2.
proof: Proof. induction l1; ins. by split; ins; desf; vauto. rewrite !nodup_cons, IHl1, in_app_iff; unfold disjoint. ins; intuition (subst; eauto). Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation