proposition: Lemma flatten_NoDup_gen : forall (A : Set)(ls : list (list A)), NoDup_gen (fun a b => a <> nil /\ a = b) ls -> (forall x, In x ls -> NoDup x) -> (forall x1 x2, In x1 ls -> In x2 ls -> x1 <> x2 -> NoDup (x1 ++ x2)) -> NoDup (flatten ls).
proof: Proof. induction ls; intuition; simpl in *. econstructor. inversion H; clear H; subst. eapply app_NoDup; intuition. eapply in_flatten in H3. destruct H3. intuition. eapply app_NoDup_inv. eapply H1. right. eapply H6. left. reflexivity. intuition. subst. eapply H4. eapply In_gen_weaken. exact H6. intuition. subst. subst. simpl in *. intuition. eauto. eauto. eapply in_flatten in H2. destruct H2. intuition. eapply app_NoDup_inv. eapply H1. right. eapply H6. left. reflexivity. intuition. subst. eapply H4. eapply In_gen_weaken. exact H6. intuition. subst. subst. simpl in *. intuition. eauto. eauto. Qed.
imports: List FCF.Fold FCF.RepeatCore