proposition: Theorem map_NoDup_gen : forall (ls : list A), NoDup_gen ea ls -> NoDup_gen eb (map f ls).
proof: Proof. induction ls; intuition; simpl in *. econstructor. inversion H; clear H; subst. econstructor. intuition. eapply H2. eapply In_gen_map_iff in H. destruct H. intuition. eapply In_gen_equiv_compat; [ eauto | eauto | idtac | idtac]. eapply eb_func. eauto. trivial. eauto. Qed.
imports: List FCF.Fold