module poly where

open import Data.Nat
open import Function
open import Relation.Binary.PropositionalEquality

infixr 5 _⇒_

-- type
data typ[_] (tvar : Set) : Set where
  TVar : tvar → typ[ tvar ]
  Nat : typ[ tvar ]
  _⇒_ : typ[ tvar ] → typ[ tvar ] → typ[ tvar ]

-- type scheme
data ts[_] (tvar : Set) : Set where
  Typ : typ[ tvar ] → ts[ tvar ]
  Forall : (ts : tvar → ts[ tvar ]) → ts[ tvar ]

-- substitution relation on types
data SubstTyp {tvar : Set} :
    (tvar → typ[ tvar ]) → typ[ tvar ] → typ[ tvar ] → Set where
  sTVar= : {τ : typ[ tvar ]} →
           SubstTyp (λ α → TVar α) τ τ
  sTVar≠ : {τ : typ[ tvar ]} → {α : tvar} →
           SubstTyp (λ β → TVar α) τ (TVar α)
  sNat   : {τ : typ[ tvar ]} →
           SubstTyp (λ β → Nat) τ Nat
  sArrow : {τ₁ : tvar → typ[ tvar ]} →
           {τ₂ : tvar → typ[ tvar ]} →
           {τ : typ[ tvar ]} →
           {τ₁′ : typ[ tvar ]} →
           {τ₂′ : typ[ tvar ]} →
           SubstTyp τ₁ τ τ₁′ → SubstTyp τ₂ τ τ₂′ →
           SubstTyp (λ β → τ₁ β ⇒ τ₂ β) τ (τ₁′ ⇒ τ₂′)

-- substitution relation on type schemes
data SubstTs {tvar : Set} :
    (tvar → ts[ tvar ]) → typ[ tvar ] → ts[ tvar ] → Set where
  sTyp : {τ₁ : tvar → typ[ tvar ]} →
         {τ : typ[ tvar ]} →
         {τ₁′ : typ[ tvar ]} →
         SubstTyp τ₁ τ τ₁′ →
         SubstTs (λ β → Typ (τ₁ β)) τ (Typ τ₁′)
  sForall :
         {σ₁ : tvar → tvar → ts[ tvar ]} →
         {τ : typ[ tvar ]} →
         {σ₁′ : tvar → ts[ tvar ]} →
         ((α : tvar) → SubstTs (λ β → (σ₁ β) α) τ (σ₁′ α)) →
         SubstTs (λ β → Forall (σ₁ β)) τ (Forall σ₁′)

-- instance
data inst {tvar : Set} : ts[ tvar ] → typ[ tvar ] → Set where
  instTyp : {τ : typ[ tvar ]} → inst (Typ τ) τ
  instForall : {σ : tvar → ts[ tvar ]} → {σ′ : ts[ tvar ]} →
               {τ τ′ : typ[ tvar ]} →
               SubstTs σ τ′ σ′ →
               inst σ′ τ →
               inst (Forall σ) τ

-- source term
mutual
  data value[_]_ {tvar : Set} (var : ts[ tvar ] → Set) :
                 typ[ tvar ] → Set where
    Var : {σ₁ : ts[ tvar ]} →
          (x : var σ₁) → {τ₁ : typ[ tvar ]} →
          (p : inst σ₁ τ₁) → value[ var ] τ₁
    Num : (n : ℕ) → value[ var ] Nat
    Fun : {τ₁ τ₂ : typ[ tvar ]} →
          (e₁ : var (Typ τ₂) → term[ var ] τ₁) → value[ var ] (τ₂ ⇒ τ₁)

  data term[_]_ {tvar : Set} (var : ts[ tvar ] → Set) :
       typ[ tvar ] → Set where
    Val : {τ₁ : typ[ tvar ]} → value[ var ] τ₁ → term[ var ] τ₁
    App : {τ₁ τ₂ : typ[ tvar ]} →
          (e₁ : term[ var ] (τ₂ ⇒ τ₁)) → (e₂ : term[ var ] τ₂) →
          term[ var ] τ₁
    Let : (σ₁ : ts[ tvar ]) → {τ₂ : typ[ tvar ]} →
          (v₁ : {τ₁ : typ[ tvar ]} → inst σ₁ τ₁ → value[ var ] τ₁) →
          (e₂ : var σ₁ → term[ var ] τ₂) →
          term[ var ] τ₂

-- substitution relation on terms
mutual
  data SubstVal {tvar : Set} {var : ts[ tvar ] → Set} :
      {σ₁ : ts[ tvar ]} → {τ₂ : typ[ tvar ]} →
      (var σ₁ → value[ var ] τ₂) →
      ({τ₁ : typ[ tvar ]} → inst σ₁ τ₁ → value[ var ] τ₁) →
      value[ var ] τ₂ → Set where
    sVar= : {τ : typ[ tvar ]} → {σ : ts[ tvar ]} →
            {p : inst σ τ} →
            {v : {τ₁ : typ[ tvar ]} → inst σ τ₁ → value[ var ] τ₁} →
            SubstVal (λ x → Var x p) v (v p)
    sVar≠ : {τ₁ : typ[ tvar ]} → {σ₁ σ₂ : ts[ tvar ]} →
            {x : var σ₂} →
            {p : inst σ₂ τ₁} →
            {v : {τ₂ : typ[ tvar ]} → inst σ₁ τ₂ → value[ var ] τ₂} →
            SubstVal (λ y → Var x p) v (Var x p)
    sNum : {τ : typ[ tvar ]} → {σ : ts[ tvar ]} →
           {n : ℕ} →
           {v : {τ₁ : typ[ tvar ]} → inst σ τ₁ → value[ var ] τ₁} →
           SubstVal (λ y → Num n) v (Num n)
    sFun : {τ₁ τ₂ : typ[ tvar ]} → {σ : ts[ tvar ]} →
           {e₁ : var σ → var (Typ τ₂) → term[ var ] τ₁} →
           {v : {τ : typ[ tvar ]} → inst σ τ → value[ var ] τ} →
           {e₁′ : var (Typ τ₂) → term[ var ] τ₁} →
           ((x : var (Typ τ₂)) → Subst (λ y → (e₁ y) x) v (e₁′ x)) →
           SubstVal (λ y → Fun (e₁ y)) v (Fun e₁′)

  data Subst {tvar : Set} {var : ts[ tvar ] → Set} :
      {σ₁ : ts[ tvar ]} → {τ₂ : typ[ tvar ]} →
      (var σ₁ → term[ var ] τ₂) →
      ({τ₁ : typ[ tvar ]} → inst σ₁ τ₁ → value[ var ] τ₁) →
      term[ var ] τ₂ → Set where
    sVal : {τ₁ : typ[ tvar ]} → {σ : ts[ tvar ]} →
           {v₁ : var σ → value[ var ] τ₁} →
           {v : {τ : typ[ tvar ]} → inst σ τ → value[ var ] τ} →
           {v₁′ : value[ var ] τ₁} →
           SubstVal v₁ v v₁′ →
           Subst (λ y → Val (v₁ y)) v (Val v₁′)
    sApp : {τ₁ τ₂ : typ[ tvar ]} → {σ : ts[ tvar ]} →
           {e₁ : var σ → term[ var ] (τ₂ ⇒ τ₁)} →
           {e₂ : var σ → term[ var ] τ₂} →
           {v : {τ : typ[ tvar ]} → inst σ τ → value[ var ] τ} →
           {e₁′ : term[ var ] (τ₂ ⇒ τ₁)} →
           {e₂′ : term[ var ] τ₂} →
           Subst e₁ v e₁′ → Subst e₂ v e₂′ →
           Subst (λ y → App (e₁ y) (e₂ y)) v (App e₁′ e₂′)
    sLet : {τ₂ : typ[ tvar ]} → {σ σ₁ : ts[ tvar ]} →
           {v₁ : var σ →
                 {τ₁ : typ[ tvar ]} → inst σ₁ τ₁ → value[ var ] τ₁} →
           {e₁ : var σ → var σ₁ → term[ var ] τ₂} →
           {v : {τ : typ[ tvar ]} → inst σ τ → value[ var ] τ} →
           {v₁′ : {τ₁ : typ[ tvar ]} → inst σ₁ τ₁ → value[ var ] τ₁} →
           {e₁′ : var σ₁ → term[ var ] τ₂} →
           ({x : typ[ tvar ]} → (y : inst σ₁ x) →
            SubstVal (λ z → (v₁ z) y) v (v₁′ y)) →
           ((x : var σ₁) → Subst (λ y → (e₁ y) x) v (e₁′ x)) →
           Subst (λ y → Let σ₁ (v₁ y) (e₁ y)) v (Let σ₁ v₁′ e₁′)

data frame[_,_] {tvar : Set} (var : ts[ tvar ] → Set)
     : typ[ tvar ] → typ[ tvar ] → Set where
  App₁ : {τ₁ τ₂ : typ[ tvar ]} →
         (e₂ : term[ var ] τ₂) →
         frame[ var , τ₂ ⇒ τ₁ ] τ₁
  App₂ : {τ₁ τ₂ : typ[ tvar ]} →
         (v₁ : value[ var ] (τ₂ ⇒ τ₁)) →
         frame[ var , τ₂ ] τ₁

frame-plug : {tvar : Set} → {var : ts[ tvar ] → Set} →
             {τ₁ τ₂ : typ[ tvar ]} →
             frame[ var , τ₂ ] τ₁ → term[ var ] τ₂ → term[ var ] τ₁
frame-plug (App₁ e₂) e₁ = App e₁ e₂
frame-plug (App₂ v₁) e₂ = App (Val v₁) e₂

-- reduction relation (= preservation)
data Reduce {tvar : Set} {var : ts[ tvar ] → Set}
     : {τ₁ : typ[ tvar ]} → term[ var ] τ₁ → term[ var ] τ₁ → Set where
  RBeta : {τ₁ τ₂ : typ[ tvar ]} →
          (e : var (Typ τ₂) → term[ var ] τ₁) →
          (v₂ : {τ : typ[ tvar ]} → inst (Typ τ₂) τ → value[ var ] τ) →
          {e′ : term[ var ] τ₁} →
          Subst e v₂ e′ →
          Reduce (App (Val (Fun e)) (Val (v₂ instTyp))) e′
  RFrame : {τ₁ τ₂ : typ[ tvar ]} →
           (e : term[ var ] τ₁) →
           (e′ : term[ var ] τ₁) →
           (f : frame[ var , τ₁ ] τ₂) →
           Reduce e e′ →
           Reduce (frame-plug f e) (frame-plug f e′)
  RLet : {σ₁ : ts[ tvar ]} → {τ₂ : typ[ tvar ]} →
         (v₁ : {τ₁ : typ[ tvar ]} → inst σ₁ τ₁ → value[ var ] τ₁) →
         (e₂ : var σ₁ → term[ var ] τ₂) →
         (e₂′ : term[ var ] τ₂) →
         Subst e₂ v₁ e₂′ →
         Reduce (Let σ₁ v₁ e₂) e₂′

data Reduce* {tvar : Set} {var : ts[ tvar ] → Set}
     : {τ₁ : typ[ tvar ]} →
       term[ var ] τ₁ →
       term[ var ] τ₁ → Set where
  R*Id : {τ₁ : typ[ tvar ]} →
         (e : term[ var ] τ₁) →
         Reduce* e e
  R*Trans : {τ₁ : typ[ tvar ]} →
            (e₁ e₂ e₃ : term[ var ] τ₁) →
            Reduce e₁ e₂ →
            Reduce* e₂ e₃ →
            Reduce* e₁ e₃

-- CPS source term
mutual
  data cpscont[_]_⇒Nat {tvar : Set} (var : ts[ tvar ] → Set)
                        : typ[ tvar ] → Set where
    Var : {τ₁ : typ[ tvar ]} → (k : var (Typ (τ₁ ⇒ Nat))) →
          cpscont[ var ] τ₁ ⇒Nat
    Fun : {τ₁ : typ[ tvar ]} →
          (e₁ : var (Typ τ₁) → cpsterm[ var ]Nat) →
          cpscont[ var ] τ₁ ⇒Nat

  data cpsvalue[_]_ {tvar : Set} (var : ts[ tvar ] → Set)
                    : typ[ tvar ] → Set where
    Var : {σ₁ : ts[ tvar ]} → (x : var σ₁) →
          {τ₁ : typ[ tvar ]} → inst σ₁ τ₁ → cpsvalue[ var ] τ₁
    Num : (n : ℕ) → cpsvalue[ var ] Nat
    Fun : {τ₁ τ₂ : typ[ tvar ]} →
          (e₁ : var (Typ τ₂) → var (Typ (τ₁ ⇒ Nat)) →
                cpsterm[ var ]Nat) →
          cpsvalue[ var ] (τ₂ ⇒ τ₁)

  data cpsterm[_]Nat {tvar : Set} (var : ts[ tvar ] → Set)
                     : Set where -- typ is always Nat
    App : {τ₁ τ₂ : typ[ tvar ]} →
          (v₁ : cpsvalue[ var ] (τ₂ ⇒ τ₁)) →
          (v₂ : cpsvalue[ var ] τ₂) →
          (c : cpscont[ var ] τ₁ ⇒Nat) →
          cpsterm[ var ]Nat
    Ret : {τ₁ : typ[ tvar ]} →
          (c : cpscont[ var ] τ₁ ⇒Nat) →
          (v : cpsvalue[ var ] τ₁) → cpsterm[ var ]Nat
    Let : (σ₁ : ts[ tvar ]) →
          (v₁ : {τ₁ : typ[ tvar ]} → inst σ₁ τ₁ →
                cpsvalue[ var ] τ₁) →
          (e₂ : var σ₁ → cpsterm[ var ]Nat) →
          cpsterm[ var ]Nat

-- substitution relation on CPS terms
mutual
  data cpsSubstCont {tvar : Set} {var : ts[ tvar ] → Set} :
                    {σ : ts[ tvar ]} → {τ τ₁ : typ[ tvar ]} →
                    (c₁ : var σ → var (Typ (τ ⇒ Nat)) →
                          cpscont[ var ] τ₁ ⇒Nat) →
                    (v : {τ : typ[ tvar ]} →
                         inst σ τ → cpsvalue[ var ] τ) →
                    (c : cpscont[ var ] τ ⇒Nat) →
                    (c₁′ : cpscont[ var ] τ₁ ⇒Nat) → Set where
    sVar= : {σ : ts[ tvar ]} → {τ : typ[ tvar ]} →
            {v : {τ₁ : typ[ tvar ]} → inst σ τ₁ → cpsvalue[ var ] τ₁} →
            {c : cpscont[ var ] τ ⇒Nat} →
            cpsSubstCont (λ _ k → Var k) v c c
    sVar≠ : {σ : ts[ tvar ]} → {τ τ₁ : typ[ tvar ]} →
            {v : {τ₁ : typ[ tvar ]} → inst σ τ₁ → cpsvalue[ var ] τ₁} →
            {c : cpscont[ var ] τ ⇒Nat} → {k′ : var (Typ (τ₁ ⇒ Nat))} →
            cpsSubstCont (λ _ k → Var k′) v c (Var k′)
    sFun  : {σ : ts[ tvar ]} → {τ τ₁ : typ[ tvar ]} →
            {e₁ : var σ → var (Typ (τ ⇒ Nat)) →
                  var (Typ τ₁) → cpsterm[ var ]Nat} →
            {v : {τ₁ : typ[ tvar ]} → inst σ τ₁ → cpsvalue[ var ] τ₁} →
            {c : cpscont[ var ] τ ⇒Nat} →
            {e₁′ : var (Typ τ₁) → cpsterm[ var ]Nat} →
            ((x : var (Typ τ₁)) →
                cpsSubst (λ x′ k′ → (e₁ x′ k′) x) v c (e₁′ x)) →
            cpsSubstCont (λ x k → Fun (e₁ x k)) v c (Fun e₁′)
                   
  data cpsSubstVal {tvar : Set} {var : ts[ tvar ] → Set} :
                   {σ : ts[ tvar ]} {τ τ₁ : typ[ tvar ]} →
                   (v₁ : var σ → var (Typ (τ ⇒ Nat)) →
                         cpsvalue[ var ] τ₁) →
                   (v : {τ : typ[ tvar ]} →
                        inst σ τ → cpsvalue[ var ] τ) →
                   (c : cpscont[ var ] τ ⇒Nat) →
                   (v₁′ : cpsvalue[ var ] τ₁) → Set where
    sVar= : {σ : ts[ tvar ]} → {τ τ₁ : typ[ tvar ]} → 
            {p : inst σ τ} →
            {v : {τ₁ : typ[ tvar ]} → inst σ τ₁ → cpsvalue[ var ] τ₁} →
            {c : cpscont[ var ] τ₁ ⇒Nat} →
            cpsSubstVal (λ x _ → Var x p) v c (v p)
    sVar≠ : {σ σ₁ : ts[ tvar ]} → {τ τ₁ : typ[ tvar ]} →
            {p : inst σ₁ τ} →
            {v : {τ₁ : typ[ tvar ]} → inst σ τ₁ → cpsvalue[ var ] τ₁} →
            {c : cpscont[ var ] τ₁ ⇒Nat} → {y : var σ₁} →
            cpsSubstVal (λ x _ → Var y p) v c (Var y p)
    sNum  : {σ : ts[ tvar ]} → {τ : typ[ tvar ]} →
            {v : {τ₁ : typ[ tvar ]} → inst σ τ₁ → cpsvalue[ var ] τ₁} →
            {c : cpscont[ var ] τ ⇒Nat} → {n : ℕ} →
            cpsSubstVal (λ _ _ → Num n) v c (Num n)
    sFun  : {σ : ts[ tvar ]} → {τ τ₁ τ₂ : typ[ tvar ]} →
            {e₁ : var σ → var (Typ (τ ⇒ Nat)) →
                  var (Typ τ₂) → var (Typ (τ₁ ⇒ Nat)) →
                  cpsterm[ var ]Nat} →
            {v : {τ₁ : typ[ tvar ]} → inst σ τ₁ → cpsvalue[ var ] τ₁} →
            {c : cpscont[ var ] τ ⇒Nat} →
            {e₁′ : var (Typ τ₂) → var (Typ (τ₁ ⇒ Nat)) →
                   cpsterm[ var ]Nat} →
            ((x : var (Typ τ₂)) → (k : var (Typ (τ₁ ⇒ Nat))) →
                cpsSubst (λ x′ k′ → (e₁ x′ k′) x k) v c (e₁′ x k)) →
            cpsSubstVal (λ x k → Fun (e₁ x k)) v c (Fun e₁′)

  data cpsSubst {tvar : Set} {var : ts[ tvar ] → Set} :
                {σ : ts[ tvar ]} → {τ : typ[ tvar ]} →
                (e : var σ → var (Typ (τ ⇒ Nat)) →
                     cpsterm[ var ]Nat) →
                (v : {τ : typ[ tvar ]} → inst σ τ → cpsvalue[ var ] τ) →
                (c : cpscont[ var ] τ ⇒Nat) →
                (e′ : cpsterm[ var ]Nat) → Set where
    sApp : {σ : ts[ tvar ]} → {τ τ₁ τ₂ : typ[ tvar ]} →
           {v₁ : var σ → var (Typ (τ ⇒ Nat)) →
                 cpsvalue[ var ] (τ₂ ⇒ τ₁)} →
           {v₂ : var σ → var (Typ (τ ⇒ Nat)) →
                 cpsvalue[ var ] τ₂} →
           {c₃ : var σ → var (Typ (τ ⇒ Nat)) →
                 cpscont[ var ] τ₁ ⇒Nat} →
           {v : {τ₁ : typ[ tvar ]} → inst σ τ₁ → cpsvalue[ var ] τ₁} →
           {c : cpscont[ var ] τ ⇒Nat} →
           {v₁′ : cpsvalue[ var ] (τ₂ ⇒ τ₁)} →
           {v₂′ : cpsvalue[ var ] τ₂} →
           {c₃′ : cpscont[ var ] τ₁ ⇒Nat} →
           cpsSubstVal v₁ v c v₁′ → cpsSubstVal v₂ v c v₂′ →
           cpsSubstCont c₃ v c c₃′ →
           cpsSubst (λ x k → App (v₁ x k) (v₂ x k) (c₃ x k)) v c
                             (App v₁′ v₂′ c₃′)
    sRet : {σ : ts[ tvar ]} → {τ τ₁ : typ[ tvar ]} →
           {c₁ : var σ → var (Typ (τ ⇒ Nat)) →
                 cpscont[ var ] τ₁ ⇒Nat} →
           {v₂ : var σ → var (Typ (τ ⇒ Nat)) →
                 cpsvalue[ var ] τ₁} →
           {v : {τ₁ : typ[ tvar ]} → inst σ τ₁ → cpsvalue[ var ] τ₁} →
           {c : cpscont[ var ] τ ⇒Nat} →
           {c₁′ : cpscont[ var ] τ₁ ⇒Nat} →
           {v₂′ : cpsvalue[ var ] τ₁} →
           cpsSubstCont c₁ v c c₁′ →
           cpsSubstVal v₂ v c v₂′ →
           cpsSubst (λ x k → Ret (c₁ x k) (v₂ x k)) v c (Ret c₁′ v₂′)
    sLet : {σ σ₁ : ts[ tvar ]} → {τ : typ[ tvar ]} →
           {v₁ : var σ → var (Typ (τ ⇒ Nat)) →
                 {τ₁ : typ[ tvar ]} → inst σ₁ τ₁ → cpsvalue[ var ] τ₁} →
           {e₁ : var σ → var (Typ (τ ⇒ Nat)) →
                 var σ₁ → cpsterm[ var ]Nat} →
           {v : {τ₁ : typ[ tvar ]} → inst σ τ₁ → cpsvalue[ var ] τ₁} →
           {c : cpscont[ var ] τ ⇒Nat} →
           {v₁′ : {τ₁ : typ[ tvar ]} → inst σ₁ τ₁ → cpsvalue[ var ] τ₁} →
           {e₁′ : var σ₁ → cpsterm[ var ]Nat} →
           ({τ₁ : typ[ tvar ]} → (p : inst σ₁ τ₁) →
            cpsSubstVal (λ x k → (v₁ x k) p) v c (v₁′ p)) →
           ((x : var σ₁) →
            cpsSubst (λ x′ k′ → (e₁ x′ k′) x) v c (e₁′ x)) →
           cpsSubst (λ x k → Let σ₁ (v₁ x k) (e₁ x k)) v c
                             (Let σ₁ v₁′ e₁′)

mutual
  data cpsSubstContK {tvar : Set} {var : ts[ tvar ] → Set} :
                     {σ : ts[ tvar ]} → {τ₁ : typ[ tvar ]} →
                     (c₁ : var σ → cpscont[ var ] τ₁ ⇒Nat) →
                     (v : {τ : typ[ tvar ]} →
                          inst σ τ → cpsvalue[ var ] τ) →
                     (c₁′ : cpscont[ var ] τ₁ ⇒Nat) → Set where
    sVar≠ : {σ : ts[ tvar ]} → {τ : typ[ tvar ]} →
            {v : {τ₁ : typ[ tvar ]} → inst σ τ₁ → cpsvalue[ var ] τ₁} →
            {k′ : var (Typ (τ ⇒ Nat))} →
            cpsSubstContK (λ _ → Var k′) v (Var k′)
    sFun  : {σ : ts[ tvar ]} → {τ₁ : typ[ tvar ]} →
            {e₁ : var σ →
                  var (Typ τ₁) → cpsterm[ var ]Nat} →
            {v : {τ₁ : typ[ tvar ]} → inst σ τ₁ → cpsvalue[ var ] τ₁} →
            {e₁′ : var (Typ τ₁) → cpsterm[ var ]Nat} →
            ((x : var (Typ τ₁)) →
                cpsSubstK (λ x′ → (e₁ x′) x) v (e₁′ x)) →
            cpsSubstContK (λ x → Fun (e₁ x)) v (Fun e₁′)
                   
  data cpsSubstValK {tvar : Set} {var : ts[ tvar ] → Set} :
                    {σ : ts[ tvar ]} → {τ₁ : typ[ tvar ]} →
                    (v₁ : var σ → cpsvalue[ var ] τ₁) →
                    (v : {τ : typ[ tvar ]} →
                         inst σ τ → cpsvalue[ var ] τ) →
                    (v₁′ : cpsvalue[ var ] τ₁) → Set where
    sVar= : {σ : ts[ tvar ]} → {τ : typ[ tvar ]} →
            {p : inst σ τ} →
            {v : {τ₁ : typ[ tvar ]} → inst σ τ₁ → cpsvalue[ var ] τ₁} →
            cpsSubstValK (λ x → Var x p) v (v p)
    sVar≠ : {σ σ₁ : ts[ tvar ]} → {τ : typ[ tvar ]} →
            {p : inst σ₁ τ} →
            {v : {τ₁ : typ[ tvar ]} → inst σ τ₁ → cpsvalue[ var ] τ₁} →
            {y : var σ₁} →
            cpsSubstValK (λ _ → Var y p) v (Var y p)
    sNum  : {σ : ts[ tvar ]} →
            {v : {τ₁ : typ[ tvar ]} → inst σ τ₁ → cpsvalue[ var ] τ₁} →
            {n : ℕ} →
            cpsSubstValK (λ x → Num n) v (Num n)
    sFun  : {σ : ts[ tvar ]} → {τ₁ τ₂ : typ[ tvar ]} →
            {e₁ : var σ →
                  var (Typ τ₂) → var (Typ (τ₁ ⇒ Nat)) →
                  cpsterm[ var ]Nat} →
            {v : {τ₁ : typ[ tvar ]} → inst σ τ₁ → cpsvalue[ var ] τ₁} →
            {e₁′ : var (Typ τ₂) → var (Typ (τ₁ ⇒ Nat)) →
                   cpsterm[ var ]Nat} →
            ((x : var (Typ τ₂)) → (k : var (Typ (τ₁ ⇒ Nat))) →
                cpsSubstK (λ x′ → (e₁ x′) x k) v (e₁′ x k)) →
            cpsSubstValK (λ x → Fun (e₁ x)) v (Fun e₁′)

  data cpsSubstK {tvar : Set} {var : ts[ tvar ] → Set} :
                 {σ : ts[ tvar ]} →
                 (e : var σ → cpsterm[ var ]Nat) →
                 (v : {τ : typ[ tvar ]} → inst σ τ → cpsvalue[ var ] τ) →
                 (e′ : cpsterm[ var ]Nat) → Set where
    sApp : {σ : ts[ tvar ]} → {τ₁ τ₂ : typ[ tvar ]} →
           {v₁ : var σ → cpsvalue[ var ] (τ₂ ⇒ τ₁)} →
           {v₂ : var σ → cpsvalue[ var ] τ₂} →
           {c₃ : var σ → cpscont[ var ] τ₁ ⇒Nat} →
           {v : {τ₁ : typ[ tvar ]} → inst σ τ₁ → cpsvalue[ var ] τ₁} →
           {v₁′ : cpsvalue[ var ] (τ₂ ⇒ τ₁)} →
           {v₂′ : cpsvalue[ var ] τ₂} →
           {c₃′ : cpscont[ var ] τ₁ ⇒Nat} →
           cpsSubstValK v₁ v v₁′ → cpsSubstValK v₂ v v₂′ →
           cpsSubstContK c₃ v c₃′ →
           cpsSubstK (λ x → App (v₁ x) (v₂ x) (c₃ x)) v (App v₁′ v₂′ c₃′)
    sRet : {σ : ts[ tvar ]} → {τ₁ : typ[ tvar ]} →
           {c₁ : var σ → cpscont[ var ] τ₁ ⇒Nat} →
           {v₂ : var σ → cpsvalue[ var ] τ₁} →
           {v : {τ₁ : typ[ tvar ]} → inst σ τ₁ → cpsvalue[ var ] τ₁} →
           {c₁′ : cpscont[ var ] τ₁ ⇒Nat} →
           {v₂′ : cpsvalue[ var ] τ₁} →
           cpsSubstContK c₁ v c₁′ →
           cpsSubstValK v₂ v v₂′ →
           cpsSubstK (λ x → Ret (c₁ x) (v₂ x)) v (Ret c₁′ v₂′)
    sLet : {σ σ₁ : ts[ tvar ]}
           {v₁ : var σ →
                 {τ₁ : typ[ tvar ]} → inst σ₁ τ₁ → cpsvalue[ var ] τ₁} →
           {e₁ : var σ →
                 var σ₁ → cpsterm[ var ]Nat} →
           {v : {τ₁ : typ[ tvar ]} → inst σ τ₁ → cpsvalue[ var ] τ₁} →
           {v₁′ : {τ₁ : typ[ tvar ]} → inst σ₁ τ₁ → cpsvalue[ var ] τ₁} →
           {e₁′ : var σ₁ → cpsterm[ var ]Nat} →
           ({τ₁ : typ[ tvar ]} → (p : inst σ₁ τ₁) →
            cpsSubstValK (λ x → (v₁ x) p) v (v₁′ p)) →
           ((x : var σ₁) →
            cpsSubstK (λ x′ → (e₁ x′) x) v (e₁′ x)) →
           cpsSubstK (λ x → Let σ₁ (v₁ x) (e₁ x)) v
                             (Let σ₁ v₁′ e₁′)

-- cps reduction relation (= preservation)
data cpsReduce {tvar : Set} {var : ts[ tvar ] → Set} :
     cpsterm[ var ]Nat → cpsterm[ var ]Nat → Set where
  RBeta  : {τ₁ τ₂ : typ[ tvar ]} →
           {e : var (Typ τ₂) → var (Typ (τ₁ ⇒ Nat)) →
                cpsterm[ var ]Nat} →
           {v₂ : {τ : typ[ tvar ]} →
                 inst (Typ τ₂) τ → cpsvalue[ var ] τ} →
           {c : cpscont[ var ] τ₁ ⇒Nat} →
           {e′ : cpsterm[ var ]Nat} →
           cpsSubst e v₂ c e′ →
           cpsReduce (App (Fun e) (v₂ instTyp) c) e′
  RCont  : {τ₁ : typ[ tvar ]} →
           {e : var (Typ τ₁) → cpsterm[ var ]Nat} →
           {v₂ : cpsvalue[ var ] τ₁} →
           {e′ : cpsterm[ var ]Nat} →
           cpsSubstK e (λ {instTyp → v₂}) e′ →
           cpsReduce (Ret (Fun e) v₂) e′
  RLet   : {σ₁ : ts[ tvar ]} →
           {v₁ : {τ₁ : typ[ tvar ]} → inst σ₁ τ₁ → cpsvalue[ var ] τ₁} →
           {e₂ : var σ₁ → cpsterm[ var ]Nat} →
           {e₂′ : cpsterm[ var ]Nat} →
           cpsSubstK e₂ v₁ e₂′ →
           cpsReduce (Let σ₁ v₁ e₂) e₂′

data cpsEqual {tvar : Set} {var : ts[ tvar ] → Set} :
     cpsterm[ var ]Nat → cpsterm[ var ]Nat → Set where
  R*Id  : (e : cpsterm[ var ]Nat) →
          cpsEqual e e
  R*Trans : (e₁ e₂ e₃ : cpsterm[ var ]Nat) →
            cpsReduce e₁ e₂ →
            cpsEqual e₂ e₃ →
            cpsEqual e₁ e₃
  R*Trans′ : (e₁ e₂ e₃ : cpsterm[ var ]Nat) →
             cpsReduce e₂ e₁ → 
             cpsEqual e₂ e₃ →
             cpsEqual e₁ e₃

-- equational reasoning
-- see ≡-Reasoning in Relation.Binary.PropositionalEquality.agda

infix  3 _∎
infixr 2 _⟶⟨_⟩_　_⟵⟨_⟩_ _⟷⟨_⟩_ _≡⟨_⟩_
infix  1 begin_

begin_ : {tvar : Set} → {var : ts[ tvar ] → Set} →
         {e₁ e₂ : cpsterm[ var ]Nat} → cpsEqual e₁ e₂ → cpsEqual e₁ e₂
begin_ red = red

_⟶⟨_⟩_ : {tvar : Set} → {var : ts[ tvar ] → Set} →
           (e₁ {e₂ e₃} : cpsterm[ var ]Nat) →
           cpsReduce e₁ e₂ → cpsEqual e₂ e₃ → cpsEqual e₁ e₃
_⟶⟨_⟩_ e₁ {e₂} {e₃} e₁-red-e₂ e₂-eq-e₃ =
  R*Trans e₁ e₂ e₃ e₁-red-e₂ e₂-eq-e₃

_⟵⟨_⟩_ : {tvar : Set} → {var : ts[ tvar ] → Set} →
           (e₁ {e₂ e₃} : cpsterm[ var ]Nat) →
           cpsReduce e₂ e₁ → cpsEqual e₂ e₃ → cpsEqual e₁ e₃
_⟵⟨_⟩_ e₁ {e₂} {e₃} e₂-red-e₁ e₂-eq-e₃ =
  R*Trans′ e₁ e₂ e₃ e₂-red-e₁ e₂-eq-e₃

_⟷⟨_⟩_ : {tvar : Set} → {var : ts[ tvar ] → Set} →
            (e₁ {e₂ e₃} : cpsterm[ var ]Nat) →
            cpsEqual e₁ e₂ → cpsEqual e₂ e₃ → cpsEqual e₁ e₃
_⟷⟨_⟩_ e₁ {.e₁} {e₃} (R*Id .e₁) e₁-eq-e₃ = e₁-eq-e₃
_⟷⟨_⟩_ e₁ {.e₂} {e₃} (R*Trans .e₁ e₁′ e₂ e₁-red-e₁′ e₁′-eq-e₂) e₂-eq-e₃ =
  R*Trans e₁ e₁′ e₃ e₁-red-e₁′
          (e₁′ ⟷⟨ e₁′-eq-e₂ ⟩ e₂-eq-e₃)
_⟷⟨_⟩_ e₁ {.e₂} {e₃} (R*Trans′ .e₁ e₁′ e₂ e₁′-red-e₁ e₁′-eq-e₂) e₂-eq-e₃ =
  R*Trans′ e₁ e₁′ e₃ e₁′-red-e₁ (e₁′ ⟷⟨ e₁′-eq-e₂ ⟩ e₂-eq-e₃)

_≡⟨_⟩_ : {tvar : Set} → {var : ts[ tvar ] → Set} →
         (e₁ {e₂ e₃} : cpsterm[ var ]Nat) → e₁ ≡ e₂ → cpsEqual e₂ e₃ →
           cpsEqual e₁ e₃
_≡⟨_⟩_ e₁ {e₂} {e₃} refl e₂-eq-e₃ = e₂-eq-e₃

_∎ : {tvar : Set} → {var : ts[ tvar ] → Set} →
     (e : cpsterm[ var ]Nat) → cpsEqual e e
_∎ e = R*Id e

-- CPS transformation
mutual
  cpsV : {tvar : Set} → {var : ts[ tvar ] → Set} → {τ₁ : typ[ tvar ]} →
         value[ var ] τ₁ → cpsvalue[ var ] τ₁
  cpsV (Var x p) = Var x p
  cpsV (Num n) = Num n
  cpsV (Fun e₁) = Fun (λ x k → cps (e₁ x) (λ v₁ → Ret (Var k) v₁))

  cps : {tvar : Set} → {var : ts[ tvar ] → Set} → {τ₁ : typ[ tvar ]} →
        term[ var ] τ₁ →
        (cpsvalue[ var ] τ₁ → cpsterm[ var ]Nat) →
        cpsterm[ var ]Nat
  cps (Val v) k = k (cpsV v)
  cps (App e₁ e₂) k =
    cps e₁ (λ v₁ → cps e₂ (λ v₂ →
      App v₁ v₂ (Fun (λ v → k (Var v instTyp)))))
  cps (Let σ₁ v₁ e₂) k =
    Let σ₁ (λ p → cpsV (v₁ p)) (λ x → cps (e₂ x) k)

-- CPS transformation (that produces no eta-redex)
mutual
  cpsEtaV : {tvar : Set} → {var : ts[ tvar ] → Set} → {τ₁ : typ[ tvar ]} →
            value[ var ] τ₁ → cpsvalue[ var ] τ₁
  cpsEtaV (Var x p) = Var x p
  cpsEtaV (Num n) = Num n
  cpsEtaV (Fun e₁) = Fun (λ x k → cpsEta′ (e₁ x) (Var k))

  cpsEta : {tvar : Set} → {var : ts[ tvar ] → Set} → {τ₁ : typ[ tvar ]} →
           term[ var ] τ₁ →
           (cpsvalue[ var ] τ₁ → cpsterm[ var ]Nat) →
           cpsterm[ var ]Nat
  cpsEta (Val v) κ = κ (cpsEtaV v)
  cpsEta (App e₁ e₂) κ =
    cpsEta e₁ (λ v₁ → cpsEta e₂ (λ v₂ →
      App v₁ v₂ (Fun (λ v → κ (Var v instTyp)))))
  cpsEta (Let σ₁ v₁ e₂) κ =
    Let σ₁ (λ p → cpsEtaV (v₁ p)) (λ x → cpsEta (e₂ x) κ)

  cpsEta′ : {tvar : Set} → {var : ts[ tvar ] → Set} → {τ₁ : typ[ tvar ]} →
            term[ var ] τ₁ →
            cpscont[ var ] τ₁ ⇒Nat →
            cpsterm[ var ]Nat
  cpsEta′ (Val v) k = Ret k (cpsEtaV v)
  cpsEta′ (App e₁ e₂) k =
    cpsEta e₁ (λ v₁ → cpsEta e₂ (λ v₂ →
      App v₁ v₂ k))
  cpsEta′ (Let σ₁ v₁ e₂) k =
    Let σ₁ (λ p → cpsEtaV (v₁ p)) (λ x → cpsEta′ (e₂ x) k)

-- schematic
schematic : {tvar : Set} {var : ts[ tvar ] → Set} {τ : typ[ tvar ]} →
            (κ : cpsvalue[ var ] τ → cpsterm[ var ]Nat) → Set
schematic {tvar} {var} {τ} κ =
  {σ₁ : ts[ tvar ]} →
  {v₁ : var σ₁ → cpsvalue[ var ] τ} →
  {v₁′ : cpsvalue[ var ] τ} →
  {v : {τ₁ : typ[ tvar ]} → inst σ₁ τ₁ → cpsvalue[ var ] τ₁} →
  cpsSubstValK v₁ v v₁′ → 
  cpsSubstK (λ x₁ → κ (v₁ x₁)) v (κ v₁′)

-- disappears afterward
schematic′ : {tvar : Set} {var : ts[ tvar ] → Set} →
             {τ₁ τ₂ : typ[ tvar ]} →
             (κ : cpsvalue[ var ] τ₂ →
                  cpsvalue[ var ] τ₁ → cpsterm[ var ]Nat) → Set
schematic′ {tvar} {var} {τ₁} {τ₂} κ =
  {σ₁ : ts[ tvar ]} →
  {v₁ : var σ₁ → cpsvalue[ var ] τ₂} →
  {v₁′ : cpsvalue[ var ] τ₂} →
  {v : {τ : typ[ tvar ]} → inst σ₁ τ → cpsvalue[ var ] τ} →
  cpsSubstValK v₁ v v₁′ →
  (x : cpsvalue[ var ] τ₁) →
  cpsSubstK (λ y → κ (v₁ y) x) v (κ v₁′ x)

-- disappears afterward
cont-equal : {tvar : Set} {var : ts[ tvar ] → Set} {σ₁ : ts[ tvar ]}
             {τ₁ τ₃ : typ[ tvar ]} →
             (κ₁ : var σ₁ → var (Typ (τ₃ ⇒ Nat)) →
                   cpsvalue[ var ] τ₁ → cpsterm[ var ]Nat) →
             (v : {τ : typ[ tvar ]} → inst σ₁ τ → value[ var ] τ) →
             (c : cpscont[ var ] τ₃ ⇒Nat) →
             (κ₂ : cpsvalue[ var ] τ₁ → cpsterm[ var ]Nat) → Set
cont-equal {tvar} {var} {σ₁} {τ₁} {τ₃} κ₁ v c κ₂ =
  {v₁ : var σ₁ → var (Typ (τ₃ ⇒ Nat)) → cpsvalue[ var ] τ₁} →
  {v₁′ : cpsvalue[ var ] τ₁} →
  cpsSubstVal v₁ (λ p → cpsEtaV (v p)) c v₁′ →
  cpsSubst (λ x k → κ₁ x k (v₁ x k))
           (λ p → cpsEtaV (v p)) c (κ₂ v₁′)

-- disappears afterward
cont-equalK : {tvar : Set} {var : ts[ tvar ] → Set} {σ₁ : ts[ tvar ]}
              {τ₁ : typ[ tvar ]} →
              (κ₁ : var σ₁ → cpsvalue[ var ] τ₁ → cpsterm[ var ]Nat) →
              (v : {τ : typ[ tvar ]} → inst σ₁ τ → value[ var ] τ) →
              (κ₂ : cpsvalue[ var ] τ₁ → cpsterm[ var ]Nat) → Set
cont-equalK {tvar} {var} {σ₁} {τ₁} κ₁ v κ₂ =
  {v₁ : var σ₁ → cpsvalue[ var ] τ₁} →
  {v₁′ : cpsvalue[ var ] τ₁} →
  cpsSubstValK (λ x → v₁ x) (λ {τ₂} p → cpsEtaV (v p)) v₁′ →
  cpsSubstK (λ x → κ₁ x (v₁ x)) (λ {τ₂} p → cpsEtaV (v p)) (κ₂ v₁′)

mutual
  SubstEtaVK≠ : {tvar : Set} {var : ts[ tvar ] → Set} {σ₁ : ts[ tvar ]}
                {τ : typ[ tvar ]}
                {v₁ : cpsvalue[ var ] τ} →
                {v : {τ₁ : typ[ tvar ]} →
                     inst σ₁ τ₁ → cpsvalue[ var ] τ₁} →
                cpsSubstValK (λ _ → v₁) v v₁
  SubstEtaVK≠ {v₁ = Var x p} = sVar≠
  SubstEtaVK≠ {v₁ = Num n} = sNum
  SubstEtaVK≠ {v₁ = Fun e₁} = sFun (λ _ _ → SubstEtaK≠)

  SubstEtaK≠ : {tvar : Set} {var : ts[ tvar ] → Set} {σ₁ : ts[ tvar ]}
               {e₁ : cpsterm[ var ]Nat} →
               {v : {τ : typ[ tvar ]} → inst σ₁ τ → cpsvalue[ var ] τ} →
            cpsSubstK (λ _ → e₁) v e₁
  SubstEtaK≠ {e₁ = App v₁ v₂ c} = sApp SubstEtaVK≠ SubstEtaVK≠ SubstEtaCK≠
  SubstEtaK≠ {e₁ = Ret c v} = sRet SubstEtaCK≠ SubstEtaVK≠
  SubstEtaK≠ {e₁ = Let σ₂ v₁ e₂} =
    sLet (λ _ → SubstEtaVK≠) (λ _ → SubstEtaK≠)

  SubstEtaCK≠ : {tvar : Set} {var : ts[ tvar ] → Set} {σ₁ : ts[ tvar ]}
                {τ₁ : typ[ tvar ]}
                {c : cpscont[ var ] τ₁ ⇒Nat} →
                {v : {τ : typ[ tvar ]} → inst σ₁ τ → cpsvalue[ var ] τ} →
                cpsSubstContK (λ _ → c) v c
  SubstEtaCK≠ {c = Var k} = sVar≠
  SubstEtaCK≠ {c = Fun e₁} = sFun (λ _ → SubstEtaK≠)

mutual
  ekSubstEtaV : {tvar : Set} {var : ts[ tvar ] → Set} {σ₁ : ts[ tvar ]}
                {τ₁ τ₂ : typ[ tvar ]} →
                {v₁ : var σ₁ → value[ var ] τ₁} →
                {v₁′ : value[ var ] τ₁} →
                {v : {τ : typ[ tvar ]} → inst σ₁ τ → value[ var ] τ} →
                {c : cpscont[ var ] τ₂ ⇒Nat} →
                SubstVal v₁ v v₁′ →
                cpsSubstVal (λ x _ → cpsEtaV (v₁ x)) (λ p → cpsEtaV (v p))
                            c (cpsEtaV v₁′)
  ekSubstEtaV sVar= = sVar=
  ekSubstEtaV sVar≠ = sVar≠
  ekSubstEtaV sNum = sNum
  ekSubstEtaV (sFun x) = sFun (λ x₁ k → ekSubstEta′ (x x₁) k)

  ekSubstEta : {tvar : Set} {var : ts[ tvar ] → Set} {σ₁ : ts[ tvar ]}
               {τ₁ τ₂ : typ[ tvar ]} → 
               {e : var σ₁ → term[ var ] τ₁} →
               {e′ : term[ var ] τ₁} →
               {v : {τ : typ[ tvar ]} → inst σ₁ τ → value[ var ] τ} →
               {c : cpscont[ var ] τ₂ ⇒Nat} →
               Subst e v e′ →
               (κ₁ : var σ₁ → var (Typ (τ₂ ⇒ Nat)) →
                     cpsvalue[ var ] τ₁ → cpsterm[ var ]Nat) →
               {κ₂ : cpsvalue[ var ] τ₁ → cpsterm[ var ]Nat} →
               cont-equal κ₁ v c κ₂ →
               cpsSubst (λ x k → cpsEta (e x) (κ₁ x k))
                        (λ p → cpsEtaV (v p)) c (cpsEta e′ κ₂)
  ekSubstEta (sVal x) κ₁ eq = eq (ekSubstEtaV x)
  ekSubstEta (sApp {e₁ = e₁} {e₂} s s₁) κ₁ eq =
    ekSubstEta s (λ x k v₁ →
      cpsEta (e₂ x) (λ v₂ →
        App v₁ v₂ (Fun (λ v → κ₁ x k (Var v instTyp))))) (λ {v₁} sub₁ →
    ekSubstEta s₁ (λ x k v₂ →
      App (v₁ x k) v₂ (Fun (λ v → κ₁ x k (Var v instTyp)))) (λ sub₂ →
        sApp sub₁ sub₂ (sFun (λ x → eq sVar≠))))
  ekSubstEta (sLet x x₁) κ₁ eq =
    sLet (λ p → ekSubstEtaV (x p)) (λ v₁ → ekSubstEta (x₁ v₁) κ₁ eq)

  ekSubstEta′ : {tvar : Set} {var : ts[ tvar ] → Set} {σ₁ : ts[ tvar ]}
                {τ₁ τ₂ : typ[ tvar ]} →
                {e : var σ₁ → term[ var ] τ₁} →
                {e′ : term[ var ] τ₁} →
                {v : {τ : typ[ tvar ]} → inst σ₁ τ → value[ var ] τ} →
                Subst e v e′ →
                {c : cpscont[ var ] τ₂ ⇒Nat} →
                (k : var (Typ (τ₁ ⇒ Nat))) → 
                cpsSubst (λ x k₁ → cpsEta′ (e x) (Var k))
                         (λ p → cpsEtaV (v p)) c (cpsEta′ e′ (Var k))
  ekSubstEta′ (sVal x) k = sRet sVar≠ (ekSubstEtaV x)
  ekSubstEta′ (sApp {e₂ = e₂} x x₁) k =
    ekSubstEta x (λ x _ v₁ →
      cpsEta (e₂ x) (λ v₂ →
        App v₁ v₂ (Var k))) (λ {v₁} sub₁ →
    ekSubstEta x₁ (λ x k₁ v₂ →
      App (v₁ x k₁) v₂ (Var k)) (λ sub₂ → sApp sub₁ sub₂ sVar≠))
  ekSubstEta′ (sLet x x₁) k =
    sLet (λ p → ekSubstEtaV (x p)) (λ v₁ → ekSubstEta′ (x₁ v₁) k)

mutual
  ekSubstEtaKV : {tvar : Set} {var : ts[ tvar ] → Set} {σ₁ : ts[ tvar ]}
                 {τ₁ : typ[ tvar ]} →
                 {v₁ : var σ₁ → value[ var ] τ₁} →
                 {v₁′ : value[ var ] τ₁} →
                 {v : {τ : typ[ tvar ]} → inst σ₁ τ → value[ var ] τ} →
                 SubstVal v₁ v v₁′ →
                 cpsSubstValK (λ x → cpsEtaV (v₁ x))
                              (λ p → cpsEtaV (v p)) (cpsEtaV v₁′)
  ekSubstEtaKV sVar= = sVar=
  ekSubstEtaKV sVar≠ = sVar≠
  ekSubstEtaKV sNum = sNum
  ekSubstEtaKV (sFun x) = sFun (λ x₁ k → ekSubstEtaK′ (x x₁) (Var k))

  ekSubstEtaK′ : {tvar : Set}{var : ts[ tvar ] → Set}
                 {σ₁ : ts[ tvar ]}{τ₁ : typ[ tvar ]} →
                 {e : var σ₁ → term[ var ] τ₁} →
                 {e′ : term[ var ] τ₁} →
                 {v : {τ : typ[ tvar ]} → inst σ₁ τ → value[ var ] τ} →
                 Subst e v e′ →
                 (c : cpscont[ var ] τ₁ ⇒Nat) →
                 cpsSubstK (λ x → cpsEta′ (e x) c) (λ p → cpsEtaV (v p))
                           (cpsEta′ e′ c)
  ekSubstEtaK′ (sVal x) (Var k) = sRet sVar≠ (ekSubstEtaKV x)
  ekSubstEtaK′ (sVal x) (Fun e₁) =
    sRet (sFun (λ x₁ → SubstEtaK≠)) (ekSubstEtaKV x)
  ekSubstEtaK′ (sApp {e₁ = e₁} {e₂} {e₂′} s s₁) (Var k) =
    ekSubstEtaK (λ x v₁ → cpsEta (e₂ x) (λ v₂ → App v₁ v₂ (Var k)))
                s
                (λ {v₁} subk₁ →
                  ekSubstEtaK (λ x v₂ → App (v₁ x) v₂ (Var k))
                              s₁
                              (λ subk₂ → sApp subk₁ subk₂ sVar≠))
  ekSubstEtaK′ (sApp {e₁ = e₁} {e₂} s s₁) (Fun e₃) =
    ekSubstEtaK (λ x v₁ → cpsEta (e₂ x) (λ v₂ → App v₁ v₂ (Fun e₃)))
                s
                (λ {v₁} subk₁ →
                  ekSubstEtaK (λ x v₂ → App (v₁ x) v₂ (Fun e₃))
                              s₁
                              (λ subk₂ → sApp subk₁ subk₂ SubstEtaCK≠))
  ekSubstEtaK′ (sLet v₂ e₂) (Var k) =
    sLet (λ p → ekSubstEtaKV (v₂ p))
         (λ var₂ → ekSubstEtaK′ (e₂ var₂) (Var k))
  ekSubstEtaK′ (sLet v₂ e₂) (Fun e₃) =
    sLet (λ p → ekSubstEtaKV (v₂ p))
         (λ var₂ → ekSubstEtaK′ (e₂ var₂) (Fun e₃))
        
  ekSubstEtaK : {tvar : Set} {var : ts[ tvar ] → Set} {σ₁ : ts[ tvar ]}
                {τ : typ[ tvar ]} →
                {e₁ : var σ₁ → term[ var ] τ} →
                {e₁′ : term[ var ] τ} →
                {v : {τ₁ : typ[ tvar ]} → inst σ₁ τ₁ → value[ var ] τ₁} →
                (κ₁ : var σ₁ → cpsvalue[ var ] τ → cpsterm[ var ]Nat) →
                {κ₂ : cpsvalue[ var ] τ → cpsterm[ var ]Nat} →
                Subst e₁ v e₁′ →
                cont-equalK κ₁ v κ₂ → 
                cpsSubstK (λ x₁ → cpsEta (e₁ x₁) (κ₁ x₁))
                          (λ p → cpsEtaV (v p)) (cpsEta e₁′ κ₂)
  ekSubstEtaK κ₁ {κ₂} (sVal x) eq = eq (ekSubstEtaKV x)
  ekSubstEtaK {τ = τ} κ₁ {κ₂} (sApp {e₁ = e₁} {e₂} s s₁) eq =
    ekSubstEtaK (λ x v₁ →
      cpsEta (e₂ x) (λ v₂ →
        App v₁ v₂ (Fun (λ v → κ₁ x (Var v instTyp))))) s (λ {v₁} sub₁ →
    ekSubstEtaK (λ x v₂ →
      App (v₁ x) v₂ (Fun (λ x₁ → κ₁ x (Var x₁ instTyp)))) s₁
          (λ {v₁} sub₂ → sApp sub₁ sub₂ (sFun (λ x → eq sVar≠))))
  ekSubstEtaK κ₁ (sLet x x₁) eq =
    sLet (λ p → ekSubstEtaKV (x p))
         (λ v₂ → ekSubstEtaK κ₁ (x₁ v₂) (λ sub → eq sub))

ekSubstEta′₂ : {tvar : Set} {var : ts[ tvar ] → Set}
               {τ τ₂ : typ[ tvar ]} →
               {e : var (Typ τ₂) → term[ var ] τ} →
               {e′ : term[ var ] τ} →
               {v : {τ₁ : typ[ tvar ]} →
                    inst (Typ τ₂) τ₁ → value[ var ] τ₁} →
               Subst e v e′ →
               (κ : cpsvalue[ var ] τ → cpsterm[ var ]Nat) →
               schematic κ →
               cpsSubst (λ x₁ k₁ → cpsEta′ (e x₁) (Var k₁))
                        (λ p → cpsEtaV (v p))
                        (Fun (λ v → κ (Var v instTyp)))
                        (cpsEta′ e′ (Fun (λ x₁ → κ (Var x₁ instTyp))))
ekSubstEta′₂ (sVal x) κ sche = sRet sVar= (ekSubstEtaV x)
ekSubstEta′₂ (sApp {e₂ = e₂} x x₁) κ sche =
  ekSubstEta x
    (λ x₂ k₁ v₁ → cpsEta (e₂ x₂) (λ v₂ → App v₁ v₂ (Var k₁)))
    (λ {v₁′} sval₁ → ekSubstEta x₁
                      (λ x₂ k₁ v₁ → App (v₁′ x₂ k₁) v₁ (Var k₁))
                      (λ sval₂ → sApp sval₁ sval₂ sVar=))
ekSubstEta′₂ (sLet x x₁) κ sche = 
  sLet (λ p → ekSubstEtaV (x p))
       (λ v₁ → ekSubstEta′₂ (x₁ v₁) κ sche)

kSubstEta : {tvar : Set} {var : ts[ tvar ] → Set} {σ₁ : ts[ tvar ]}
            {τ₂ τ₃ : typ[ tvar ]} →
            (e : term[ var ] τ₂) →
            {v : {τ₁ : typ[ tvar ]} → inst σ₁ τ₁ → cpsvalue[ var ] τ₁} →
            {v₁ : var σ₁ → cpsvalue[ var ] τ₃} →
            {v₁′ : cpsvalue[ var ] τ₃} →
            (κ : cpsvalue[ var ] τ₃ →
                 cpsvalue[ var ] τ₂ → cpsterm[ var ]Nat) →
            schematic′ κ →
            cpsSubstValK v₁ v v₁′ →
            cpsSubstK (λ y → cpsEta e (κ (v₁ y))) v (cpsEta e (κ v₁′))
kSubstEta (Val x) κ sche s = sche s (cpsEtaV x)
kSubstEta (App e e₁) κ sche s =
  kSubstEta e (λ v′ v₁ →
    cpsEta e₁ (λ v₂ →
      App v₁ v₂ (Fun (λ x → κ v′ (Var x instTyp))))) (λ sub₁ v₁ →
  kSubstEta e₁ (λ v′ v₂ →
    App v₁ v₂ (Fun (λ x → κ v′ (Var x instTyp)))) (λ sub₂ v₂ →
      sApp SubstEtaVK≠ SubstEtaVK≠
           (sFun (λ v′ → sche sub₂ (Var v′ instTyp)))) sub₁) s
kSubstEta (Let σ₂ v₁ e₂) κ sche s =
  sLet (λ p → SubstEtaVK≠) (λ x → kSubstEta (e₂ x) κ sche s)

-- postulate
lemma : {tvar : Set} {var : ts[ tvar ] → Set} {σ₁ : ts[ tvar ]} →
        {e₁ e₂ : var σ₁ → cpsterm[ var ]Nat} →
        {v : {τ₁ : typ[ tvar ]} → inst σ₁ τ₁ → cpsvalue[ var ] τ₁} →
        ((x : var σ₁) → cpsEqual (e₁ x) (e₂ x)) →
        cpsEqual (Let σ₁ v e₁) (Let σ₁ v e₂)
lemma eq = {!!}

-- the last step in correctEta*
cpsEtaEta′ : {tvar : Set} {var : ts[ tvar ] → Set} {τ : typ[ tvar ]} →
             (e : term[ var ] τ) →
             (κ : cpsvalue[ var ] τ → cpsterm[ var ]Nat) →
             schematic κ →
             cpsEqual (cpsEta′ e (Fun (λ x₁ → κ (Var x₁ instTyp))))
                      (cpsEta e κ)
cpsEtaEta′ (Val x) κ sche =
  begin
    cpsEta′ (Val x) (Fun (λ x₁ → κ (Var x₁ instTyp)))
  ≡⟨ refl ⟩
    Ret (Fun (λ x₁ → κ (Var x₁ instTyp))) (cpsEtaV x)
  ⟶⟨ RCont (sche sVar=) ⟩
    cpsEta (Val x) κ 
  ∎
cpsEtaEta′ (App e e₁) κ sche = 
  begin
    cpsEta e
       (λ v₁ →
          cpsEta e₁ (λ v₂ → App v₁ v₂ (Fun (λ v → κ (Var v instTyp)))))
  ∎
cpsEtaEta′ (Let σ₁ v₁ e₂) κ sche =
  begin
    cpsEta′ (Let σ₁ v₁ e₂)
            (Fun (λ x₁ → κ (Var x₁ instTyp)))
  ⟷⟨ lemma (λ x → cpsEtaEta′ (e₂ x) κ sche) ⟩
    cpsEta (Let σ₁ v₁ e₂) κ
  ∎

-- main
correctEta : {tvar : Set} → {var : ts[ tvar ] → Set} → {τ : typ[ tvar ]} →
             {e e′ : term[ var ] τ} →
             (κ : cpsvalue[ var ] τ → cpsterm[ var ]Nat) →
             Reduce e e′ →
             schematic κ →
             cpsEqual (cpsEta e κ) (cpsEta e′ κ)
correctEta {e′ = e′} κ (RBeta e v₂ x) sche =
  begin
    cpsEta (App (Val (Fun e)) (Val (v₂ instTyp))) κ
  ≡⟨ refl ⟩
    App (Fun (λ x₁ k₁ → cpsEta′ (e x₁) (Var k₁)))
        (cpsEtaV (v₂ instTyp)) (Fun (λ v → κ (Var v instTyp)))
  ⟶⟨ RBeta {v₂ = λ p → cpsEtaV (v₂ p)} (ekSubstEta′₂ x κ sche) ⟩
    cpsEta′ e′ (Fun (λ x → κ (Var x instTyp)))
  ⟷⟨ cpsEtaEta′ e′ κ sche ⟩
    cpsEta e′ κ
  ∎
correctEta κ (RFrame e e′ (App₁ e₂) r) sche =
  begin
    cpsEta (frame-plug (App₁ e₂) e) κ
  ≡⟨ refl ⟩
    cpsEta e
       (λ v₁ →
          cpsEta e₂ (λ v₂ → App v₁ v₂ (Fun (λ v → κ (Var v instTyp))))) 
  ⟷⟨ correctEta (λ v₁ →
         cpsEta e₂ (λ v₂ → App v₁ v₂ (Fun (λ v → κ (Var v instTyp))))) r
         (λ sub → kSubstEta e₂ (λ y v₂ →
            App y v₂ (Fun (λ x → κ (Var x instTyp)))) (λ sub′ v′ →
              sApp sub′ SubstEtaVK≠ SubstEtaCK≠) sub) ⟩
    cpsEta e′
       (λ v₁ →
          cpsEta e₂ (λ v₂ → App v₁ v₂ (Fun (λ v → κ (Var v instTyp)))))
  ≡⟨ refl ⟩
    cpsEta (frame-plug (App₁ e₂) e′) κ
  ∎
correctEta κ (RFrame e e′ (App₂ v₁) r) sche =
  begin
    cpsEta (frame-plug (App₂ v₁) e) κ
  ≡⟨ refl ⟩
    cpsEta e
       (λ v₂ → App (cpsEtaV v₁) v₂ (Fun (λ v → κ (Var v instTyp))))
  ⟷⟨ correctEta
          (λ v₂ → App (cpsEtaV v₁) v₂ (Fun (λ v → κ (Var v instTyp)))) r
          (λ sub → sApp SubstEtaVK≠ sub SubstEtaCK≠) ⟩
    cpsEta e′
       (λ v₂ → App (cpsEtaV v₁) v₂ (Fun (λ v → κ (Var v instTyp))))
  ≡⟨ refl ⟩
    cpsEta (frame-plug (App₂ v₁) e′) κ
  ∎
correctEta κ (RLet {σ₁} v₁ e₂ e₂′ x) sche =
  begin
    cpsEta (Let σ₁ v₁ e₂) κ
  ≡⟨ refl ⟩
    Let σ₁ (λ {τ₂} p → cpsEtaV (v₁ p)) (λ x₁ → cpsEta (e₂ x₁) κ)
  ⟶⟨ RLet (ekSubstEtaK (λ _ v₂ → κ v₂) x sche) ⟩
    cpsEta e₂′ κ
  ∎