proposition: Lemma NoDup_modulo_permutation : forall {A} (seq: list A), NoDup seq <-> (exists seq', NoDup seq' /\ Permutation seq seq').
proof: Proof. split; intros * H; [ exists seq; intuition | ]. destruct H as [ seq' (no_dup & perm) ]. symmetry in perm. eapply NoDup_Permutation_rewrite; eauto. Qed.
imports: Coq.Sorting.Permutation Fiat.Common Coq.Lists.List Fiat.Common.List.ListFacts