proposition: Lemma permutation_NoDup : forall (A : Type)(ls1 ls2 : list A), Permutation ls1 ls2 -> NoDup ls1 -> NoDup ls2.
proof: Proof. induction 1; intuition. inversion H0; clear H0; subst. econstructor. intuition. eapply H3. eapply Permutation_in. eapply Permutation_sym. eapply H. eauto. eauto. inversion H; clear H; subst. inversion H3; clear H3; subst. simpl in *. econstructor. simpl. intuition. econstructor; intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation