The way I understand these types is by thinking of what functions I can build that satisfy the signature.
Booleans
For booleans, we have the type $\Pi\alpha . \alpha \rightarrow \alpha \rightarrow \alpha$. All members of this type will take in two abstract values (that is, values of type $\alpha$, where $\alpha$ can be anything) and return an abstract value (an $\alpha$).
In System F, there are exactly two functions that match this signature: $(\lambda x . \lambda y . x)$ and $(\lambda x . \lambda y . y)$. We can name them true and false and properly claim "all booleans are either true or false".
Integers
Integers have the type $\Pi\alpha . \alpha \rightarrow (\alpha \rightarrow \alpha) \rightarrow \alpha$. All members of this type need to be functions that take in two things: an abstract value and a function on abstract values, and return an abstract value.
(Again, we don't know anything about what type $\alpha$ actually is, nor do we know what the function of type $(\alpha \rightarrow \alpha)$ does. It could be the identity, it could be the successor function, it could accept a list and return the empty list.)
One function that matches this signature is $(\lambda x . \lambda f . x)$. Another is $(\lambda x . \lambda f . f x)$. Yet another is $(\lambda x . \lambda f . f (f x))$. There are countably many of these functions, so we can put them in one-to-one correspondence with the natural numbers and name them 0, 1, 2, ... . The only difference between these and Church numerals is that you can only apply them to values $x$ and $f$ with the right type.
Lists & Trees
After integers, lists and trees are easy. The type for lists, like you said, is $\Pi \alpha . \alpha \rightarrow (U \rightarrow \alpha \rightarrow \alpha) \rightarrow \alpha$. Again, members of this type take in two arguments, an abstract value and a function that can manipulate abstract values, and returns an abstract value. The interesting part is the type $U$, which Girard uses to denote the type of elements in the list. A List Boolean has type $\Pi \alpha . \alpha \rightarrow (Boolean \rightarrow \alpha \rightarrow \alpha) \rightarrow \alpha$.
We can easily define a function nil as $(\lambda x . \lambda f . x)$. That's one way to return a list given the arguments $x$ and $f$. The only other thing we can do to return a list is to apply the function $f$; given a value $u$ of type $U$, we could make the function $(\lambda x . \lambda f . f u x)$. If we parameterize over the value $u$, we get a more familiar cons function: $(\lambda u . \lambda x . \lambda f . f u x)$. Its type is $\Pi U . \Pi \alpha . \alpha \rightarrow (U \rightarrow \alpha \rightarrow \alpha) \rightarrow \alpha$.
Trees have the type $\Pi \alpha . \alpha \rightarrow (U \rightarrow \alpha \rightarrow \alpha \rightarrow \alpha) \rightarrow \alpha$. You just add another branch!
Example: Lists in other Programming Languages
A list is one of two things:
- Empty
- Non empty, so we can think of it as one element attached to a smaller list
Let's stick to lists of integers, which Girard would describe with the type $\Pi \alpha . \alpha \rightarrow (Integer \rightarrow \alpha \rightarrow \alpha) \rightarrow \alpha$. His empty list is $\alpha$, the first argument, and his non-empty list is the second argument (which is a function expecting one element and another list).
In Java, we could represent these two alternatives by making an interface and a pair of classes.
interface IntList {}
class Empty implements IntList {}
class Cons implements IntList { int head; IntList tail; }
The Cons class has fields representing the two parts of any non-empty list.
In OCaml, things look a little more like System F.
type int_list = Empty | Cons of int * int_list
Again, there are two alternatives. A list can be Empty, or it can be a pair like Cons(2, Empty) made of an element and another list.
Girard's type is difficult to read because he expresses these ideas with one $\Pi$-type, but the idea's the same.
Best Answer
To understand the meaning of a family of terms defined by induction, my suggestion is to take some concrete examples. So, let us see what are $F_0'$, $F_1'$, $F_2'$, $F_3'$, and $F_0$, $F_1$, $F_2$, $F_3$ (for every $n \in \mathbb{N}$, the Church numeral representing $n$ is denoted by $\underline{n}$)
\begin{align} F_0' &= m & F_0 &= \lambda c. \lambda m. m \\ F_1' &= c \underline{1} F_0' = c \, \underline{1} \, m & F_1 &= \lambda c. \lambda m. c \, \underline{1} \, F_0' = \lambda c. \lambda m. c \, \underline{1} \, m \\ F_2' &= c \, \underline{2} \, F_1' = c \,\underline{2} (c \,\underline{1} \, m ) & F_2 &= \lambda c. \lambda m. c \,\underline{2} \, F_1' = \lambda c. \lambda m. c \, \underline{2} (c \, \underline{1} \, m ) \\ F_3' &= c \, \underline{3} \, F_2' = c \, \underline{3} (c \, \underline{2} (c \, \underline{1} \, m )) & F_3 &= \lambda c. \lambda m. c \, \underline{3} \, F_2' = \lambda c. \lambda m. c \, \underline{3} (c \, \underline{2} (c \, \underline{1} \, m )) \\ \dots & & \dots \\ F_n' &= c \, \underline{n} \, F_{n-1}' = c \, \underline{n} (c \,\underline{n\!-\!1} \dots(c \, \underline{1} \, m )) & F_n &= \lambda c. \lambda m. c \, \underline{n} \, F_{n-1}' = \lambda c. \lambda m. c \, \underline{n} (c \,\underline{n\!-\!1} \dots(c \, \underline{1} \, m )) \end{align}
Now, as explained here and here, a list $[M_1, \dots, M_n]$ of $n \in \mathbb{N}$ "objects" can be represented in the $\lambda$-calculus by the term $$\tag{$*$} \lambda c.\lambda m.c M_1 (c M_2 (\dots(c M_n m)...)) $$ Comparing $(*)$ and $F_n$, it is clear that $F_n$ is nothing but the instance of $(*)$ where $M_1$ is replaced by $\underline{n}$, and $M_2$ is replaced by $\underline{n-1}$, and so on (in general, $M_k$ is replaced by $\underline{n-k+1}$, for all $1 \leq k \leq n$). Therefore, for every $n \in \mathbb{N}$, the term $$F_n = \lambda c. \lambda m. c \, \underline{n} (c \,\underline{n\!-\!1} \dots(c \, \underline{1} \, m ))$$ represents $$[\,\underline{n}, \underline{n-1}, \dots, \underline{1}\,]$$ the decreasing list of natural numbers from $n$ to $1$.