module WellTypedLam2 where

data TyCode : Set where
  ι : TyCode
  _⇒_ : TyCode → TyCode → TyCode

data Con : Set where
  ε : Con
  _<_ : Con → TyCode → Con

data Lam : Con → TyCode → Set where
  z : ∀{Γ σ} → Lam (Γ < σ) σ
  w : ∀{Γ σ τ} → Lam Γ τ → Lam (Γ < σ) τ
  _$_ : ∀{Γ σ τ} → Lam Γ (σ ⇒ τ) → Lam Γ σ → Lam Γ τ
  lam : ∀{Γ σ τ} → Lam (Γ < σ) τ → Lam Γ (σ ⇒ τ)

data Var : Con → TyCode → Set where
  z : ∀{Γ σ} → Var (Γ < σ) σ
  s : ∀{Γ σ τ} → Var Γ τ → Var (Γ < σ) τ

var2lam : ∀{Γ σ} → Var Γ σ → Lam Γ σ
var2lam z     = z
var2lam (s i) = w (var2lam i)