How does one prove weakening for a simple language in agda?

Question

I'm trying to prove a weakening lemma analagous to Harper's from chapter 4 of PFPL. Namely, weakening : {x : String} {Γ : Context} {e : Expr} {τ τ' : Type} → x ∉dom Γ → Γ ⊢ e ؛ τ' → (Γ , x ؛ τ) ⊢ e ؛ τ'

I've adapted some of Wadler's code, where he proves weaken below, but still don't know how to prove this general weakening lemma, either using the rename function or by induction as harper does. (for example, Harper seems to implicitly assume exchange for a let constructor, not included in this language). I thought introducing the _∉dom_ would help, but I just see it bloating the amoung of work I have to do in somehow making a bunch of correspondance lemmas with _؛_∈_.

How does one prove weakening, either as stated or modified, with either via induction or rename?

module basic where

open import Data.List using (List; _∷_; []; map)
open import Data.Empty
open import Data.String using (_++_; _==_; _≟_; String)
open import Data.Nat using (ℕ)
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; trans; sym; cong; cong-app; subst)

data Type : Set where
  nat : Type
  bool : Type

data Expr : Set where
  var : String → Expr
  lit : (n : ℕ) → Expr
  tt : Expr
  ff : Expr
  _+'_ : Expr → Expr → Expr
  _*'_ : Expr → Expr → Expr
  _<'_ : Expr → Expr → Expr
  if : Expr → Expr → Expr → Expr

Id : Set
Id = String

infixl 5  _,_؛_
data Context : Set where
  ∅     : Context
  _,_؛_ : Context → Id → Type → Context


data _؛_∈_ : Id → Type → Context → Set where
  Z : ∀ {Γ x A} → x ؛ A ∈ (Γ , x ؛ A)
  S : ∀ {Γ x y A B} → (x ≡ y → ⊥) → x ؛ A ∈ Γ → x ؛ A ∈ (Γ , y ؛ B)

-- not in wadler
data _∉dom_ : Id → Context → Set where
  em :  ∀ {x} → x ∉dom ∅
  notcons  : ∀ {x y τ Γ} → x ∉dom Γ → (x ≡ y → ⊥) → x ∉dom (Γ , y ؛ τ )

-- hypothetical judgement
data _⊢_؛_ : Context → Expr → Type → Set where 
  varR   : ∀ {a τ Γ} → (a ؛ τ ∈ Γ) → (Γ ⊢ (var a) ؛ τ)
  natR : ∀ {Γ} {n : ℕ}  → Γ ⊢ (lit n) ؛ nat
  trueR :  ∀ {Γ} → Γ ⊢ tt ؛ bool
  falseR :  ∀ {Γ} → Γ ⊢ ff ؛ bool
  plus-i :  ∀ {Γ} {e1 e2 : Expr} → Γ ⊢ e1 ؛ nat → Γ ⊢ e2 ؛ nat → Γ ⊢ e1 +' e2 ؛ nat
  times-i :  ∀ {Γ} {e1 e2 : Expr} → Γ ⊢ e1 ؛ nat → Γ ⊢ e2 ؛ nat → Γ ⊢ e1 *' e2 ؛ nat
  le-i :  ∀ {Γ} {e1 e2 : Expr} → Γ ⊢ e1 ؛ nat → Γ ⊢ e2 ؛ nat → Γ ⊢ e1 <' e2 ؛ bool
  if-i :  ∀ {Γ} {τ} {e1 e2 e3 : Expr}  → Γ ⊢ e1 ؛ bool → Γ ⊢ e2 ؛ τ → Γ ⊢ e3 ؛ τ → Γ ⊢ if e1 e2 e3 ؛ τ 

-- adapted from wadler
rename : ∀ {Γ Δ} → (∀ {x A} → x ؛ A ∈ Γ → x ؛ A ∈ Δ) → (∀ {M A} → Γ ⊢ M ؛ A → Δ ⊢ M ؛ A)
rename f (varR x) = varR (f x)
rename f natR = natR
rename f trueR = trueR
rename f falseR = falseR
rename f (plus-i h h₁) = plus-i (rename f h) (rename f h₁)
rename f (times-i h h₁) = times-i (rename f h) (rename f h₁)
rename f (le-i h h₁) = le-i (rename f h) (rename f h₁)
rename f (if-i h h₁ h₂) = if-i (rename f h) (rename f h₁) (rename f h₂)

-- wadler's weaken lemma
weaken : ∀ {Γ M A} → ∅ ⊢ M ؛ A → Γ ⊢ M ؛ A
weaken x = rename (λ ()) x

-- my attempt
weakening : {x : String} {Γ : Context} {e : Expr} {τ τ' : Type} → x ∉dom Γ → Γ ⊢ e ؛ τ' → (Γ , x ؛ τ)  ⊢ e ؛ τ' 
-- induction, dunno how to account for the variable
weakening x (varR y) = {!!}
weakening x natR = natR
weakening x trueR = trueR
weakening x falseR = falseR
weakening x (plus-i y₁ y₂) = plus-i (weakening x y₁) (weakening x y₂)
weakening x (times-i y₁ y₂) = times-i (weakening x y₁) (weakening x y₂)
weakening x (le-i y₁ y₂) = le-i (weakening x y₁) (weakening x y₂)
weakening x (if-i y₁ y₂ y₃) = if-i (weakening x y₁) (weakening x y₂) (weakening x y₃)

-- otherwise, i don't know how to addapt this rename
weakening' : {x : String} {Γ : Context} {e : Expr} {τ τ' : Type} → x ∉dom Γ → Γ ⊢ e ؛ τ' → (Γ , x ؛ τ)  ⊢ e ؛ τ' 
weakening' {x} {τ = τ} em y = rename help y
  where
    help : {x = x₁ : Id} {A : Type} → x₁ ؛ A ∈ ∅ → x₁ ؛ A ∈ (∅ , x ؛ τ)
    help {x = x₁} ()
weakening' (notcons α β) y = rename (λ z → S (λ x₃ → {!!}) z) y

Answer 1

A possible idea is to add a lemma which states that, if a value x is not in a context Γ and if a value a is of type τ in the same context Γ then a and x cannot be equal.

open import Relation.Nullary

-- If a,τ'∈Γ and x∉Γ then ¬a≡x
prop : ∀ {x Γ τ a} → x ∉dom Γ → a ؛ τ ∈ Γ → ¬ a ≡ x
prop (notcons _ ¬x≡x) Z refl = ¬x≡x refl
prop (notcons x∉Γ _) (S _ aτ∈Γ) = prop x∉Γ aτ∈Γ

Then the missing case in your version of weakening simple becomes

weakening x (varR y) = varR (S (prop x y) y)