Is there a formalization of normalization of impredicative system F?

In particular Agda seems not strong enough to prove that.

Is the predicative Calculus of Inductive Constructions universes (Coq without Prop) sufficient?

How about with the impredicative Prop?

• 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.

• Is there an existing Coq formalization? – Łukasz Lew Jun 8 '18 at 16:37
• @ŁukaszLew I couldn't find anything compelling online, but there is a Lego formalization by Altenkirch (1993!) described here: cs.nott.ac.uk/~psztxa/publ/tlca93.pdf – cody Jun 8 '18 at 19:12
• – Łukasz Lew Jun 9 '18 at 0:49