Prove that
  e :: forall a. a -> a
must satisfy
  e xr = xr
(for all types AR, for all xr :: AR)
In other words, e has to be the identity function.

Below is the proof skeleton.  Fill in the TODO's to complete it.

The parametricity theorem, but use functions for relations:

for all types AL, AR, h :: AL -> AR :
  let <a> be: xl<a>xr iff h xl = xr
  e <a -> a> e

Expand the definition of <a -> a>:
(We do it slowly this time, so keep "foo <a> bar" unexpanded until next step.)

for all types AL, AR, h :: AL -> AR :
  let <a> be: xl<a>xr iff h xl = xr
  for all xl::AL, xr::AR :
    if TODO <a> TODO
    then TODO <a> TODO

Use the definition of <a>:

for all types AL, AR, h :: AL -> AR :
  for all xl::AL, xr::AR :
    if TODO = TODO
    then TODO = TODO

Choose AL=TODO, xl=TODO, h x = TODO (for all x):

for all types AR :
  for all xr::AR :
    xr = e xr