Calculus of constructions: Why forall when pi exists? I'm studying the calculus of constructions from ATAPL, Chapter 2. I'm trying to understand the Type Equivalence rule, which describes the meaning of the new type family Prf a. The rule states:
Γ ⊢ T :: *         Γ, x:T ⊢ t: Prop
---------------------------------------[QT-ALL]
Γ ⊢ Prf (all x:T.t) ≡ Πx:T. Prf t :: *

This rule seems to state that types of the form of Prf(all ...) is equivalent to Π types. Combining this with the information that:

Prf: Πx:Prop.* [Prof needs Prop as input]
The only constructor of Prop is of the form all ...

implies that the only well-typed occurrence of Prf we can have is of the form Prf (all ...), which is equivalent to the Pi-type encoding (as given by QT-ALL).
Thus, I see no benefit gained by adding the Prf/Prop mechanism. I believe we gain something to do with impredicativity, as we can use all x:T.t : Prop to quantify over Prop itself. I don't know enough theory to judge whether this is possible or impossible just using Pi types.
Clearly, I am missing something. Could I please have an explanation of what we gain by introducing Prf/Prop that we did not already have with Pi types?
I've added a picture of the full definition here:
It is false that the only well-typed occurrence of Prf has to be of the form Prf(all ...). For example, in the context with a variable p : Prop we can form the type Prf(p) which is not of the stated form. Another possibility is that we have a Prf(t) for some closed term t : Prop which is not of the form all ... but it normalizes to it.
The purpose of Prf is to decode, or coerce, the elements of Prop to types. That is, the elements of Prop are not actual types, so if we want to use them as if they were types, they first have to be coerced to types, which is what Prf does. The rule QT-All states that all decodes to Π.
To put it differently, Prop is a Tarski universe and Prf is the type family that decodes its elements as types.