Why Church-encoded types aren't sufficient to express inductive proofs? I've heard some claims that the calculus of constructions without inductive types isn't powerful enough to express proofs by induction. Is that correct? If so, why isn't the Church-encoding sufficient for that?
How would you prove inside the pure CoC that the induction principle holds of the Church numerals? See Thomas Streicher's, Independence of the induction
principle and the axiom of
choice in the pure calculus
of constructions.