I thought this might be tough, given the fact that the proof usually goes in the other direction (Parametricity $\Rightarrow$ Normalization), and the post by Gabriel is somewhat involved, but in system F one can do a relatively straightforward induction.
I'm going to assume you're somewhat familiar with the usual statement of parametricty, e.g. from the "Theorems for free!" paper, and I'll treat only binary relations for simplicity.
I'll also be working in the "Curry-style" calculus for brevity.
Theorem: if $T(X)$ is a type in system F with (only) the free type variable $X$, then for any well-typed term
$$ \vdash t : \forall X.T(X)$$
and any relation $\cal R$ between terms that respects $\beta\eta$,
$$ t\ T({\cal R})\ t$$
where $T(\cal R)$ is the parametricity relation defined in the usual way by induction on the structure of types.
The proof requires a more general lemma, which will handle arbitrary amounts of type variables and term variables (rather than working in a closed context).
Let $\theta$ be a map from type variables to $\beta\eta$ respecting binary relations over terms, and if $\Gamma$ is a type context, then $\sigma$ is a map from variables $x$ to pairs of terms $(u_1, u_2)$ such that, if $x : U\in\Gamma$, then $u_1\ U\theta\ u_2$, i.e. $u_1$ and $u_2$ are related by the parametricity relation at the appropriate type (where $\theta$ is used to instantiate type variables).
Given this, the lemma then states:
Lemma: for any such $\theta, \Gamma, \sigma$, if $\Gamma \vdash t : T$, then $t\sigma_1\ T\theta\ t\sigma_2$. (With the obvious interpretation of $\sigma_i$ as a plain substitution).
Proof. First we note that $T\theta$ is closed under $\beta\eta$ conversion, so we may take the $\beta$-normal $\eta$-long normal form of $t$, and reason by induction on its size.
Now we reason by cases (not induction!) on the structure of $T$.
Base case: suppose $T=X$. The normal form of $t$ is also of type $X$ and the only possible form is $x\ t_1\ldots t_n$, with the $t_i$ in normal forms.
If t is just $x$, then $\sigma_1(x)\ X\theta\ \sigma_2(x)$ by construction.
Otherwise, by inversion the type of $x$ is $T'=T_1\rightarrow\ldots\rightarrow T_n\rightarrow X$. Now by construction, $\sigma_1(x)\ T'\theta\sigma_2(x)$, which means that $\sigma_1(x\ t_1\ldots t_n)\ \theta(X)\ \sigma_2(x\ t_1\ldots t_n)$ if $\sigma_1(t_i)\ T_i\theta\ \sigma_2(t_i)$. But this is exactly the induction hypothesis.
Suppose now that $T=T_1\rightarrow T_2$. We proceed similarly: take 2 arbitrary terms $u$ and $u'$ such that $u\ T_1\theta\ u'$. We need to show that $t\sigma_1\ u\ T_2\theta\ t\sigma_2\ u'$. But by inversion again, (and the definition of $\eta$-long forms), $t$ must be of the form $\lambda x.t'$, so $t'\sigma_1\ u\ =_{\beta\eta}\ t'\sigma_1'$, where $\sigma_1'$ is $\sigma_1$ extended with the mapping $x\mapsto u$, and similarly for $u'$.
The induction hypothesis applies again, using $\sigma'$ instead of $\sigma$.
Finally, if $T=\forall X.T'$, then inversion tells us that $\Gamma\vdash t:T'$, and $X$ does not appear free in $\Gamma$. This means we can take $\theta'$ to be $\theta$ extended with an arbitrary binding for $X$, which does not affect the correctness of $\sigma$, since $X$ does not appear in the types of any of the variables.
This gives $t\sigma_1\ T'\theta'\ t\sigma_2$ for an arbitrary such extension, implying $t\sigma_1\ T\theta\ t\sigma_2$, which concludes the proof.
I'm not 100% certain, but I suspect this proof can be carried out in some weak form of 2nd order arithmetic, which would show that normalization does imply parametricity in some strong sense.
let rec f x = f xandthrow new Exception ("Hello Mum"). What you have in mind is some variant of System F or F$\omega$. $\endgroup$