[Agda] Proving Parametricity?

[Brandon Moore]

I've written the following code based on Adam Chlipala's paper on
"Parametric Higher Order Abstract Syntax". I'm wondering if there's
any way to prove the parammetricity assumption at the end.
It's taken as an axiom in the Coq development.

module phoas where

open import Data.List
open import Data.Product

data Exp (var : Set) : Set where
  Var : var -> Exp var
  App : Exp var -> Exp var -> Exp var
  Abs : (var -> Exp var) -> Exp var

-- an expression is an Exp parametric in the variable type
exp = ∀ var → Exp var

-- "apply"
example : exp
example var = Abs (λ x → Abs (λ y → App (Var x) (Var y)))

data In {A : Set} : A -> List A -> Set where
  InHd : ∀ x l → In x (x ∷ l)
  InTl : ∀ x x' l → In x l -> In x (x' ∷ l)

data Exp_related {var1 var2 : Set} :
  (Γ : List (var1 × var2)) → Exp var1 -> Exp var2 -> Set where
  Related : ∀ Γ v1 v2 → In (v1 , v2) Γ → Exp_related Γ (Var v1) (Var v2)
  RApp : ∀ Γ e1 e2 e1' e2' → Exp_related Γ e1 e1' → Exp_related Γ e2 e2' →
    Exp_related Γ (App e1 e2) (App e1' e2')
  RAbs : ∀ Γ f1 f2 → (∀ v1 v2 → Exp_related ((v1 , v2) ∷ Γ) (f1 v1) (f2 v2)) →
    Exp_related Γ (Abs f1) (Abs f2)

exp_param : ∀ (e : exp) var1 var2 → Exp_related [] (e var1) (e var2)
exp_param = {!!}