Rigorous proof that parametric polymorphism implies naturality using parametricity?
The missing part is the &quot;identity extension lemma&quot;, which is mentioned in Reynolds' original paper but not in Wadler's.
For $F : \text{Type} \to \text{Type}$, this says that if the relational interpretation of $F$ is instantiated with a type $A$ and the identity relation
on $A$, we get the identity relation on $F\,A$.
For System F, identity extension can be proven for types-in-contexts, but note that there is no $F : \text{Type} \to \text{Type}$ in System F. To gracefully handle identity extension for type operators in general, it's better to switch to reflexive graph models, where identity extension is given mutually with the rest of the model.
Let's use the reflexive graph model of some type theory. This means that for every closed $F : \text{Type} \to \text{Type}$, we get a semantic $F^S : \text{Set} \to \text{Set}$, together with $F^R : (A, B : \text{Set}) \to \text{Rel}\,A\,B \to \text{Rel}\,(F\,A)\,(F\,B)$ where $\text{Rel}\,A\,B$ denotes a set of proof-irrelevant relations. We also get identity extension: $F^R\,A\,A\,(\text{Id}\,A) = \text{Id}\,(F\,A)$, where $\text{Id}\,A$ is the identity relation. In the following, let's omit all $^S$-es and don't talk about syntactic things, only about semantic things, so that we may write $F : \text{Set} \to \text{Set}$.
Assume $F, G : \text{Set} \to \text{Set}$ are functors, and $\eta : (A : \text{Set}) \to F\,A \to G\,A$. Let's write $\text{map}$ for functorial mapping.
We assume that everything is parametric. This means that we get $F^R$, $G^R$, $\eta^R$ and ${\text{map}_F}^R$ and ${\text{map}_G}^R$. Assume $f : A \to B$ and $x : F\,A$.
To show:
$$ \text{map}_G\,f\,(\eta_A\,x) = \eta_B\,(\text{map}_F\,f\,x) $$
By identity extension for $G$, this is equivalent to
$$ G^R\,B\,B\,(\text{Id}\,B)\,(\text{map}_G\,f\,(\eta_A\,x))\,(\eta_B\,(\text{map}_F\,f\,x)) $$
Category law:
$$ G^R\,B\,B\,(\text{Id}\,B)\,(\text{map}_G\,f\,(\eta_A\,x))\,(\text{map}_G\,id\,(\eta_B\,(\text{map}_F\,f\,x))) $$
To show the above, we use ${\text{map}_G}^R$, i.e. that $\text{map}_G$ preserves all relations. We have to pick two relations, one in $\text{Rel}\,A\,B$ and one in $\text{Rel}\,B\,B$ and show that $f : A \to B$ and $id : B \to B$ are pointwise related. We pick the graph of $f$ and $\text{Id}\,B$, and the functions are clearly pointwise related. It remains to show:
$$ G^R\,A\,B\,(\text{Graph}\,f)\,(\eta_A\,x)\,(\eta_B\,(\text{map}_F\,f\,x)) $$
We know that $\eta$ preserves all relations, so it's enough to show:
$$ F^R\,A\,B\,(\text{Graph}\,f)\,x\,(\text{map}_F\,f\,x) $$
Category law:
$$ F^R\,A\,B\,(\text{Graph}\,f)\,(\text{map}_F\,id\,x)\,(\text{map}_F\,f\,x)$$
We instantiate ${\text{map}_F}^R$ with $\text{Id}\,A$ and $\text{Graph}\,f$ and it remains to show:
$$ F^R\,A\,A\,(\text{Id}\,A)\,x\,x $$
By identity extension for $F$, this is equivalent to:
$$ x = x $$

The same thing in Agda:
-- Agda 2.6.1, stdlib 1.5

open import Relation.Binary.PropositionalEquality
  renaming (sym to infix 6 _⁻¹; cong to ap; trans to infixr 5 _◾_; subst to tr)
open import Function

coe : ∀{i}{A B : Set i} → A ≡ B → A → B
coe refl a = a

Rel : Set → Set → Set₁
Rel A B = A → B → Set

Id : (A : Set) → Rel A A
Id A x y = x ≡ y

Graph : {A B : Set} → (A → B) → Rel A B
Graph f a b = f a ≡ b

happly : ∀{i j}{A : Set i}{B : Set j}{f g : A → B} → f ≡ g → ∀ x → f x ≡ g x
happly refl x = refl

record Functor : Set₁ where
  field
    !      : Set → Set
    map    : {A B : Set} → (A → B) → ! A → ! B
    map-id : ∀ {A} → map {A} id ≡ id
    map-∘  : ∀ {A B C}(f : B → C)(g : A → B) → map (f ∘ g) ≡ map f ∘ map g

record Functorᴿ (F : Functor) : Set₁ where
  private module F = Functor F
  field
    !     : ∀{A₀ A₁} → Rel A₀ A₁ → Rel (F.! A₀) (F.! A₁)
    map   : ∀ {A₀ A₁}(Aᴿ : Rel A₀ A₁){B₀ B₁}(Bᴿ : Rel B₀ B₁)
            (f₀ : A₀ → B₀)(f₁ : A₁ → B₁)(fᴿ : ∀ {a₀ a₁} → Aᴿ a₀ a₁ → Bᴿ (f₀ a₀) (f₁ a₁))
            {fa₀ fa₁} → ! Aᴿ fa₀ fa₁ → ! Bᴿ (F.map f₀ fa₀) (F.map f₁ fa₁)

    idext : ∀ {A} → ! (Id A) ≡ Id (F.! A)

  reflexive : ∀ {A x} → ! (Id A) x x
  reflexive {A} {x} = tr (λ f →  f x x) (idext ⁻¹) refl

module _
  (F G : Functor) (Fᴿ : Functorᴿ F) (Gᴿ : Functorᴿ G) where

  module F  = Functor F   ; module G  = Functor G
  module Fᴿ = Functorᴿ Fᴿ ; module Gᴿ = Functorᴿ Gᴿ

  module _ (η  : ∀ {A} → F.! A → G.! A)
           (ηᴿ : ∀ {A₀ A₁}(Aᴿ : Rel A₀ A₁){fa₀ fa₁}
                 → Fᴿ.! Aᴿ fa₀ fa₁ → Gᴿ.! Aᴿ (η fa₀) (η fa₁)) where

    η-is-natural : ∀ {A B}(f : A → B) x → G.map f (η x) ≡ η (F.map f x)
    η-is-natural {A} {B} f x =
      let lem1 : Fᴿ.! (Graph f) (F.map id x) (F.map f x)
          lem1 = Fᴿ.map (Id A) (Graph f) id f (ap f) {x} {x} Fᴿ.reflexive

          lem2 : Fᴿ.! (Graph f) x (F.map f x)
          lem2 = tr (λ y → Fᴿ.! (Graph f) y (F.map f x)) (happly F.map-id x) lem1

          lem3 : Gᴿ.! (Graph f) (η x) (η (F.map f x))
          lem3 = ηᴿ (Graph f) lem2

          lem4 : Gᴿ.! (Id B) (G.map f (η x)) (G.map id (η (F.map f x)))
          lem4 = Gᴿ.map (Graph f) (Id B) f id id lem3

          lem5 : Gᴿ.! (Id B) (G.map f (η x)) (η (F.map f x))
          lem5 = tr (λ y → Gᴿ.! (Id B) (G.map f (η x)) y) (happly G.map-id _) lem4

      in coe (happly (happly Gᴿ.idext (G.map f (η x))) (η (F.map f x))) lem5