In this blog post, reporting on a collaboration with Li-Yao Xia, I will show an example of how some results that we traditionally think of as arising from free theorems / parametricity can be established in a purely “syntactic” way, by looking at the structure of canonical derivations. More precisely, I prove that $\newcommand{\List}[1]{\mathsf{List}~#1} \newcommand{\Fin}[1]{\mathsf{Fin}~#1} \newcommand{\Nat}[1]{\mathbb{N}} \newcommand{\rule}[2]{\frac{\displaystyle \array{#1}}{\displaystyle #2}} \newcommand{\judge}[2]{{#1} \vdash {#2}} \newcommand{\emptyrule}[1]{\begin{array}{c}\\[-1em] #1 \end{array}} ∀α. \List α → \List \alpha$ is isomorphic to $Π(n:\Nat{}). \List{(\Fin{n})}$ where $\Fin{n}$ is the type of integers smaller than $n$, corresponding to the set $\{0, 1, \dots, n-1\}$.