proposition: Theorem NoDup_gen_zip_fst : forall (A B : Set)(ea : A -> A -> Prop)(lsa : list A)(lsb : list B), NoDup_gen ea lsa -> NoDup_gen (fun a b => ea (fst a) (fst b)) (zip lsa lsb).
proof: Proof. induction lsa; intuition; simpl in *. econstructor. inversion H; clear H; subst. destruct lsb; intuition; simpl in *. econstructor. econstructor. intuition. eapply H2. eapply In_gen_zip_fst. eauto. eauto. Qed.
imports: List FCF.Fold FCF.RepeatCore