It is not possible to derive induction for Church-encoded datatypes on the Calculus of Constructions (source). Moreover, according to the accepted answer to another question, it is also not possible to derive induction for Church-encoded datatypes on CoIC, despite the presence of inductive datatypes. As such, I wonder if we assume induction for Church-encoded Nat,
cnat_ind; that is:
cnat_ind : (n : CNat) -> (P : CNat -> Type) -> (S : ∀ (n : CNat) -> P n -> P (csucc n)) -> (Z : P czero) -> P n
czero are the usual Church-encoded Nat type and constructors, would that allow us to inhabit the empty type
∀ (P : *) -> P?