This paper presents generic derivations of induction for
impredicatively typed lambda-encoded datatypes, in the Cedille
type theory. Cedille is a pure type theory extending the
Curry-style Calculus of Constructions with implicit products,
primitive heterogeneous equality, and dependent intersections.
All data erase to pure lambda terms, and there is no built-in
notion of datatype. The derivations are generic in the sense
that we derive induction for any datatype which arises as the
least fixed point of a signature functor. We consider
Church-style and Mendler-style lambda-encodings. Moreover, the
isomorphism of these encodings is proved. Also, we formalize
Lambek's lemma as a consequence of expected laws of cancellation,
reflection, and fusion.