proposition: Theorem nth_NoDup : forall (A : Set)(ls : list (list A)) i, (forall e, In e ls -> NoDup e) -> NoDup (nth i ls nil).
proof: Proof. induction ls; destruct i; intuition; simpl in *. econstructor. econstructor. eauto. Qed.
imports: FCF.FCF Permutation