You need parametricity to to show induction is derivable. Without it, you can only show that Church encodings give rise to weak inductive types. Derek Dreyer and I have a new CSL paper Internalizing Parametricity in the Extensional Calculus of Constructions that talks about how to do it.
