Rigorous statement for Sys F cannot express ∀ w/ predicates

Stream: Type theory

[nrs]

I'm trying to understand exactly why it is that https://ncatlab.org/nlab/show/computational+trilogy states that quantification requires dependent types, and why this wouldn't be possible to achieve with System F. From what I've managed to gather, System F can express quantification, but only over types, and not over elements or predicates.

I'm looking for a way to formalize this statement in order to start working on a proof. How could I express: System F lacks the expressive power to state quantification over terms? Or, lacks the expressive power to state quantification in the way made possible by dependent types?