Is there a formalization of normalization of impredicative system F?

Coq without Prop is not strong enough, because it's basically Martin-Lf type theory with universes.

Coq with Prop is strong enough, because you can encode sets of normalizing terms via predicates $S : \mathrm{Term} \to \mathrm{Prop}$, and impredicative universal quantification lets you express arbitrary intersections.