proposition: Theorem In_gen_map_iff : forall (l : list A) (y : B), (In_gen eb y (map f l) <-> (exists x : A, eb (f x) y /\ In_gen ea x l)).
proof: Proof. induction l; intuition; simpl in *. intuition. destruct H. intuition. intuition. econstructor. intuition. eapply eb_symm. eauto. left. eapply ea_refl. eapply eb_symm. eauto. specialize (IHl y). intuition. destruct H2. intuition. econstructor. split. eauto. intuition. destruct H. intuition. left. eapply eb_trans. eapply eb_symm. eauto. eapply ea_func. trivial. right. specialize (IHl y). intuition. eapply H2. econstructor. intuition. eauto. trivial. Qed.
imports: List FCF.Fold