Is case analysis on normal forms of lambda terms sufficient to prove parametricity results? There are many closed terms of a given type. For instance, both of these terms:

$$ \lambda x . x $$
$$ \lambda x . (\lambda y . y) x $$

have a type of a polymorphic identity function:

$$ \forall X . X \rightarrow X$$

On the other hand, there is only one normalized term of that type i.e: $\lambda x . x$.
Similarly, given the type of Church natural numbers:

$$ \mathtt{Nat} = \forall X . (X \rightarrow X) \rightarrow X \rightarrow X $$ 

one can argue that all the normal form terms of type $\mathtt{Nat}$ are in the form:

$$\lambda s . \lambda z . s (\ldots (s\; z)) $$

Is there any research that goes along these lines and perhaps formalizes this intuition?  

Is this idea correct and strong enough to prove (by case analysis on the normal forms of the terms) 'free theorems' or more general parametricity results?

Clarification: The type system in question is System F
I'd like to offer some pointers.


  Is there any research that goes along these lines and perhaps formalizes this intuition?


Parametricity by analysis of the shape of (simply-typed) normal forms preceded by a normalisation argument was proposed by Girard, Scedrov, and Scott [1]. This connects parametricity, cut-elimination in logic, and a proof technique for coherence in category theory. Here, parametricity is understood as a property of dinaturality, originally proposed for system F in [2]. 


  Is this idea correct and strong enough to prove (by case analysis on the normal forms of the terms) 'free theorems' or more general parametricity results?


In [1], it is noted that this includes the so-called "free theorems" as a special case. But the argument does not extend to all of system F, and dinaturality fails to capture relational parametricity (see e.g. [3]). On the other hand, a work by Paolo Pistone shows that one indeed thus obtains a syntactic characterisation of parametricity for a class of types a bit larger than the simple types including your examples [4]:


  Our results imply that, for positive second order types, realizability, parametricity, dinaturality and typability are equivalent properties of closed normal lambda-terms. 


So there is indeed an elementary technique based on looking at shapes of normal forms, which provides a syntactic characterisation of some parametricity results including the "free theorems", that also hints at a connection with categorical coherence.

[1]: Girard, J.-Y.; Scedrov, A. &amp; Scott, P. J. Normal Forms and Cut-Free Proofs as Natural Transformations. Logic From Computer Science, Mathematical Science Research Institute Publications 21, Springer-Verlag, 1992, 217-241.
http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.811

[2]: Bainbridge, E. S.; Freyd, P. J.; Scedrov, A. &amp; Scott, P. J. Functorial polymorphism. Theoretical computer science, Elsevier, 1990, 70, 35-64.
https://core.ac.uk/display/82270459

[3]: De Lataillade, J. Dinatural Terms in System F. Logic in Computer Science, 24th Annual IEEE Symposium, 267-276, 2009. https://www.irif.fr/~delatail/dinat.pdf

[4]: Pistone, P. On completeness and parametricity in the realizability semantics of System F. https://arxiv.org/abs/1802.05143