From Church-encoding to induction principle
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} &amp;= \forall T . T \to T \\
&amp;= \forall T . (1 \to T) \to T \\
&amp;= \forall T . (F T \to T) \to T
\end{align*}
where $F X = 1$.

Empty type

\begin{align*}
\mathsf{unit} &amp;= \forall T . T \\
&amp;= \forall T . 1 \to T \\
&amp;= \forall T . (0 \to T) \to T \\
&amp;= \forall T . (F T \to T) \to T
\end{align*}
where $F X = 0$.

Natural numbers

\begin{align*}
\mathsf{nat} &amp;= \forall T . (T \to T) \to (T \to T) \\
&amp;= \forall T . (T \to T) \times T \to T \\
&amp;= \forall T . T \times (T \to T) \to T \\
&amp;= \forall T . ((1 + T) \to T) \to T \\
&amp;= \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} &amp;= \forall T . (F T \to T) \to T \\
&amp;= \forall T . ((1 + T \times T) \to T) \to T \\
&amp;= \forall T . (T \times (T \times T \to T) \to T \\
&amp;= \forall T . T \to (T \to T \to T) \to T
\end{align*}

It all works beautifully.