proposition: Lemma NoDup_Permutation_rewrite {A} : forall (l l' : list A), Permutation l l' -> NoDup l -> NoDup l'.
proof: Proof. intros; induction H. + econstructor. + inversion H0; subst; econstructor; eauto. unfold not; intros; apply H3; apply Permutation_sym in H; eapply Permutation_in; eauto. + inversion H0; subst; inversion H3; subst; repeat econstructor; eauto. * unfold not; intros; destruct H; eauto. apply H2; econstructor; eauto. * unfold not; intros; apply H2; econstructor 2; eauto. + eauto. Qed.
imports: Coq.Sorting.Permutation Fiat.Common Coq.Lists.List Fiat.Common.List.ListFacts