proposition: Theorem firstn_NoDup : forall (A : Type) n (ls : list A), NoDup ls -> NoDup (firstn n ls).
proof: Proof. induction n; destruct ls; intuition; simpl in *. econstructor. inversion H; clear H; subst. econstructor. intuition. eapply H2. eapply firstn_In. eauto. eapply IHn; intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation