Prove that if
  e :: forall a. a -> a
then
  for all types AR, for all xr :: AR:
    xr = e xr
(So e has to be the identity function.)

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

Apply the parametricity theorem and expand:

for all types AL, AR, relation (~) between AL and AR:
  let <a> = (~) in
  for all xl::AL, xr::AR :
    if TODO <a> TODO
    then TODO <a> TODO

Choose

AL = TODO, xl = TODO
(~) be TODO

xl<a>xr is true because TODO

Therefore

for all type AR:
  for all xr::AR:
    xr = e xr