proposition: Lemma nodup_append_commut A (a b : list A) : NoDup (a ++ b) -> NoDup (b ++ a).
proof: Proof. ins; rewrite nodup_app in *; unfold disjoint in *. desf; splits; ins; eauto. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation