Forms of types in the calculus of constructions
On the face of it, the result you're asking for is a normalization result, as it asserts that every well-typed term of a certain form has a head-normal form (of a certain shape).

However it is legitimate to ask whether your statement is equivalent to normalization of the CC, since you are only asking for head normal forms of a certain sub-class of terms.

In general, it doesn't make sense to ask whether two true statements are equivalent, since the answer is always (trivially) yes. However in this specific case, normalization of CC must rely on powerful meta-theory, since it implies consistency of some strong form of higher-order logic! So it makes sense to ask:


  In some weak meta-theory (say $\mathrm{PRA}$ or $\mathrm{PA}$) can we prove "CC is normalizing" $\Longleftrightarrow$ "Every closed term of type $*$ or $\square$ reduces to a product"?


The answer, I believe, is no.

Certainly, direction $\Longrightarrow$ holds, as you noted. But in the other direction, we have some counter-examples: in system $\mathrm{F_\omega}$, the fact that "type level" computations are normalizing is a consequence of the normalization of the simply-typed $\lambda$-calculus, and in Girard's system $U^-$, type level normalization holds, whereas it does not at the term level!

Things are a bit more complicated in the CC though, since type level terms can contain arbitrary term-level terms. The trick is that to compute head-normal forms, you don't actually need to dip into those terms to do reductions.

In PTS lingo, you only need to reduce $(*,\square, \square)$ and $(\square, \square, \square)$ redexes. But normalization of those only relies on the normalization of some variant of the simply typed $\lambda$-calculus (though I won't detail that argument right now). The hard part is showing that reducing the 2 types of redexes above must result in a head-normal form for terms of type $*$ or $\square$. You can do this by contradiction by supposing there is a head redex at that level, and showing that it must be of one of the two forms above.