proposition: Lemma Permutation_nodup A ( l l' : list A) : Permutation l l' -> NoDup l -> NoDup l'.
proof: Proof. induction 1; eauto; rewrite !nodup_cons in *; ins; desf; intuition. eby symmetry in H; eapply H0; eapply Permutation_in. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation