def Trm.multi_subst (L : Finset ℕ) (f : { x : ℕ // x ∈ L } → Trm) : Trm → Trm

Equations

• Trm.multi_subst L f (€i) = €i
• Trm.multi_subst L f ($y) = if h : y ∈ L then f ⟨y, h⟩ else $y
• Trm.multi_subst L f (λu) = λTrm.multi_subst L f u
• Trm.multi_subst L f (u1 @ u2) = Trm.multi_subst L f u1 @ Trm.multi_subst L f u2

def Trm.context_type (Γ : context) (x : { x : ℕ // x ∈ context_terms Γ }) : Typ

Equations

• Trm.context_type [] ⟨val, h⟩ = ⋯.elim
• Trm.context_type ((x_2, b) :: Γ_2) ⟨x', h⟩ = if ha : x' = x_2 then b else Trm.context_type Γ_2 ⟨x', ⋯⟩

theorem Trm.multi_subst_over_empty_context (t : Trm) (f : { x : ℕ // x ∈ context_terms [] } → Trm) : Trm.multi_subst (context_terms []) f t = t

theorem Trm.multi_subst_at_singleton (t : Trm) (x : ℕ) (T : Typ) (f : { x_1 : ℕ // x_1 ∈ context_terms [(x, T)] } → Trm) : Trm.multi_subst (context_terms [(x, T)]) f t = [x // f ⟨x, ⋯⟩] t

def Trm.add_term (Γ : context) (f : { x : ℕ // x ∈ context_terms Γ } → Trm) (u : Trm) (y : ℕ) (T : Typ) (x : { x : ℕ // x ∈ context_terms ((y, T) :: Γ) }) : Trm

Equations

• Trm.add_term Γ f u y T x = Subtype.casesOn x fun (x' : ℕ) (h : x' ∈ context_terms ((y, T) :: Γ)) => if p : x' = y then u else f ⟨x', ⋯⟩

theorem Trm.multi_subst_fresh (Γ : context) (t : Trm) (u : Trm) (y : ℕ) (T : Typ) (h : y ∉ t.fv) (f : { x : ℕ // x ∈ context_terms Γ } → Trm) : Trm.multi_subst (context_terms ((y, T) :: Γ)) (Trm.add_term Γ f u y T) t = Trm.multi_subst (context_terms Γ) f t

theorem Trm.multi_subst_open_lemma_1 (e1 : Trm) (e2 : Trm) (Γ : context) (f : { x : ℕ // x ∈ context_terms Γ } → Trm) : (∀ (x : ℕ) (h : x ∈ context_terms Γ), (f ⟨x, h⟩).lc) → ∀ (j : ℕ), Trm.multi_subst (context_terms Γ) f ( {j ~> e2} e1) = {j ~> Trm.multi_subst (context_terms Γ) f e2} Trm.multi_subst (context_terms Γ) f e1

theorem Trm.multi_subst_open_lemma_2 (Γ : context) (t : Trm) (u : Trm) (y : ℕ) (T : Typ) : u.lc → y ∉ t.fv → ∀ (f : { x : ℕ // x ∈ context_terms Γ } → Trm), (∀ (x : ℕ) (h : x ∈ context_terms Γ), (f ⟨x, h⟩).lc) → Trm.multi_subst (context_terms ((y, T) :: Γ)) (Trm.add_term Γ f u y T) (t.open₀ ($y)) = (Trm.multi_subst (context_terms Γ) f t).open₀ u

theorem Trm.multi_subst_open (Γ : context) (t : Trm) (y : ℕ) : y ∉ context_terms Γ → ∀ (f : { x : ℕ // x ∈ context_terms Γ } → Trm), (∀ (x : ℕ) (h : x ∈ context_terms Γ), (f ⟨x, h⟩).lc) → Trm.multi_subst (context_terms Γ) f (t.open₀ ($y)) = (Trm.multi_subst (context_terms Γ) f t).open₀ ($y)

theorem Trm.context_type_eq_bind (Γ : context) (x : { x : ℕ // x ∈ context_terms Γ }) (T : Typ) : valid_ctx Γ → binds (↑x) T Γ → Trm.context_type Γ x = T

theorem Trm.multi_subst_lc (t : Trm) (Γ : context) : t.lc → ∀ (f : { x : ℕ // x ∈ context_terms Γ } → Trm), (∀ (x : ℕ) (h : x ∈ context_terms Γ), (f ⟨x, h⟩).lc) → (Trm.multi_subst (context_terms Γ) f t).lc