proposition: Theorem NoDup_flatten_subset : forall (A : Set)(ls1 ls2 : list (list A)), list_pred (fun x y => exists n, y = firstn n x) ls1 ls2 -> NoDup (flatten ls1) -> NoDup (flatten ls2).
proof: Proof. induction 1; intuition; simpl in *. destruct H. subst. eapply NoDup_app in H1. intuition. eapply app_NoDup; intuition. eapply firstn_NoDup. trivial. eapply H3. eapply firstn_In. eauto. eapply pred_firstn_In. eauto. eauto. intuition. eapply H3. eapply firstn_In. eauto. eapply pred_firstn_In. eauto. eauto. intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation