Is there a formalization of normalization of impredicative system F?
Coq without Prop is not strong enough, because it's basically Martin-Löf 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.