Let $F : \mathsf{Type} \to \mathsf{Type}$ be a type constructor and let $W_F$ be the inductive type defined by $W_F = F W_F$. Not every $F$ has such an inductive types, but this is not important for this discussion.
The starting point of Church's encodings is the observation that $W_F$ ought to be
$$\forall T : \mathsf{Type} \,.\, (F T \to T) \to T.$$
Thus, to get an induction principle out of a Church encoding, we take the following steps:
- Rewrite the Church encoding in the form $\forall T : \mathsf{Type} \,.\, (F T \to T) \to T$ for a suitable $F$.
- Derive an induction principle for $F$, as in your own answer to your own question.
Let us try a couple of examples.
Unit type
\begin{align*}
\mathsf{unit} &= \forall T . T \to T \\
&= \forall T . (1 \to T) \to T \\
&= \forall T . (F T \to T) \to T
\end{align*}
where $F X = 1$.
Empty type
\begin{align*}
\mathsf{unit} &= \forall T . T \\
&= \forall T . 1 \to T \\
&= \forall T . (0 \to T) \to T \\
&= \forall T . (F T \to T) \to T
\end{align*}
where $F X = 0$.
Natural numbers
\begin{align*}
\mathsf{nat} &= \forall T . (T \to T) \to (T \to T) \\
&= \forall T . (T \to T) \times T \to T \\
&= \forall T . T \times (T \to T) \to T \\
&= \forall T . ((1 + T) \to T) \to T \\
&= \forall T . (F T \to T) \to T
\end{align*}
where $F X = 1 + X$.
Binary trees
We can also go backwards. The binary trees are the inductive type for $F X = 1 + X \times X$, thus their Church encoding is
\begin{align*}
\mathsf{tree} &= \forall T . (F T \to T) \to T \\
&= \forall T . ((1 + T \times T) \to T) \to T \\
&= \forall T . (T \times (T \times T \to T) \to T \\
&= \forall T . T \to (T \to T \to T) \to T
\end{align*}
It all works beautifully.
