Calculus of constructions: Why forall when pi exists?
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.