Lack of atomic propositions in the Calculus of Constructions from ATTAPL textbook
I have no thoughts on whether this is on-topic for TCS and if need be I can repost my answer elsewhere. But I think the question is a good opportunity to demonstrate how to think about the CoC pending some consensus to move it.


The rule BETA-ALL, which says we can beta-reduce terms underneath the all binder (but not the type of the argument), is not part of the typing or equivalence rules of $\mathsf{CC}$. Pierce is extending his definition of $\beta$-reduction first seen in Section 2.3 (section "Strong Normalization"), which itself is defined "As an auxiliary device for the soundness and completeness of algorithmic typechecking." Specifically the fact that this reduction is strongly normalizing can be used to show that typechecking halts.
Pierce mentions on page 51 that "We may use type and term variables declared in a fixed initial context to simulate the built-in types and operators of a programming language."

Also see Figure 2-1 (First-order dependent types), in which one of the context formation rules (labelled "term variable binding") is that if $\Gamma$ is a well-formed context and $T$ is a well-formed type, we can pick a variable name $x$ and and then $\Gamma, x :: T$ is a well-formed context. (It seems to be implicit that $x$ should be a fresh name, i.e. does not conflict with the rest of $\Gamma$, and that $T$ is well-formed in context $\Gamma$.).

Now combine this with rule of Figure 2-7 which states that $T ::= \ldots \mathsf{Prop}\ldots$, meaning $\mathsf{Prop}$ is a type. Therefore we can add $\mathsf{True} :: \mathsf{Prop}$ to the context. Likewise with $\mathsf{False}$.

To add a proof of $\mathsf{True}$, use rule K-App to deduce that $\mathsf{Prf} \:\mathsf{True}$ has kind $\ast$, i.e. is a type, and apply term variable binding again to add some proof $\mathsf{Unit} :: \mathsf{Prf} \,\mathsf{True}$ to the context.
When introducing $\mathsf{Prop}$, we also introduce this new binder called forall, which seems reasonable. Now we have to give this a semantics---how do we prove some forall x, P? The rule merely states that a proof of forall x, P is the same thing as offering "a proof of $P$ for every $x$" where the latter is defined as a dependent product (something our system already had). In a sense, the rules just say "by using the operator $\mathsf{Prf}$, $\mathsf{Prop}$ acts like $\ast$."

Perhaps you're wondering why this is interesting. We know that a proposition $p:\mathsf{Prop}$ can be coerced to a type $\mathsf{Prf} p : \ast$, and the equivalence says the binder forall acts like a dependent product, so what is gained?. But notice that by using T-ALL and QT-ALL, $\mathsf{Prop}$ can effectively play the role of $T$ when forming the dependent product, so we can quantify over $\mathsf{Prop}$ and still have a $\mathsf{Prop}$. This is the "impredicativity"  Pierce refers to, and it makes the system drastically more expressive. If we tried to get rid of the coercion just take $\mathsf{Prop} \equiv \ast$, we would have $\ast : \ast$, which is known to be inconsistent by a theorem of Girard.
To exhibit a natural number per Pierce's definition, you must be able to satisfy this criterion: If I give you any type $a$, term $z : a$, and successor function $s : a \to a$, you must be able to offer me some term of type $a$. Since you don't know the type $a$ in advance, the only thing you can do is apply $s$ to $z$ some number of times, and that is effectively the same thing as having a natural number. Pierce is showing that $\mathsf{CC}$ is expressive enough to type Church's encoding of the natural numbers , which is good because that encoding becomes impossible when you move from untyped lambda calculus to STLC. See these course notes. See also the Wikipedia page on System F for more information---System F is less expressive than $\mathsf{CC}$ but still good enough to play this game.