6. StlcProp: Properties of STLC🔗

In this chapter, we develop the fundamental theory of the Simply Typed Lambda Calculus — in particular, the type safety theorem.

We pick up where the Stlc chapter left off, so everything below lives in the same namespace as the definitions it is about.

namespace Stlc

open scoped MyGetElem
open scoped Elab

6.1. Canonical Forms🔗

As we saw for the very simple language in the Types chapter, the first step in establishing basic properties of reduction and types is to identify the possible canonical forms (i.e., well-typed values) belonging to each type. For Bool, these are again the boolean values true and false; for arrow types, they are lambda-abstractions.

Formally, we will need these lemmas only for terms that are not only well typed but closed — i.e., well typed in the empty context.

theorem canonical_forms_bool (t : Tm) (hτ : <{ ∅ ⊢ t ⦂ Bool }>) (hv : t.IsValue) :
    t = <{ true }> ∨ t = <{ false }> := byt:Tmhτ:<{ ∅ ⊢ t ⦂ Bool }>hv:t.IsValue⊢ t = <{ true }> ∨ t = <{ false }>
  cases hv with
  | abs x τ t₁ =>absx:Stringτ:Tyt₁:Tmhτ:<{ ∅ ⊢ λ ~x : τ . t₁ ⦂ Bool }>⊢ <{ λ ~x : τ . t₁ }> = <{ true }> ∨ <{ λ ~x : τ . t₁ }> = <{ false }> cases hτAll goals completed! 🐙
  | tru =>truhτ:<{ ∅ ⊢ true ⦂ Bool }>⊢ <{ true }> = <{ true }> ∨ <{ true }> = <{ false }> lefttruhτ:<{ ∅ ⊢ true ⦂ Bool }>⊢ <{ true }> = <{ true }>; rflAll goals completed! 🐙
  | fls =>flshτ:<{ ∅ ⊢ false ⦂ Bool }>⊢ <{ false }> = <{ true }> ∨ <{ false }> = <{ false }> rightflshτ:<{ ∅ ⊢ false ⦂ Bool }>⊢ <{ false }> = <{ false }>; rflAll goals completed! 🐙

theorem canonical_forms_fun (t : Tm) (τ₁ τ₂ : Ty)
    (hτ : <{ ∅ ⊢ t ⦂ τ₁ → τ₂ }>) (hv : t.IsValue) :
    ∃ x u, t = <{ λ x : τ₁ . u }> := byt:Tmτ₁:Tyτ₂:Tyhτ:<{ ∅ ⊢ t ⦂ τ₁ → τ₂ }>hv:t.IsValue⊢ ∃ x u, t = <{ λ ~x : τ₁ . u }>
  cases hv with
  | abs x τ t₁ =>absτ₁:Tyτ₂:Tyx:Stringτ:Tyt₁:Tmhτ:<{ ∅ ⊢ λ ~x : τ . t₁ ⦂ τ₁ → τ₂ }>⊢ ∃ x_1 u, <{ λ ~x : τ . t₁ }> = <{ λ ~x_1 : τ₁ . u }> cases hτ with | abs _ _ _ _ _ _ =>abs.absτ₁:Tyτ₂:Tyx:Stringt₁:Tmh✝:<{ ~(x →ₚ τ₁) ⊢ t₁ ⦂ τ₂ }>⊢ ∃ x_1 u, <{ λ ~x : τ₁ . t₁ }> = <{ λ ~x_1 : τ₁ . u }>
    exists x, t₁All goals completed! 🐙
  | tru =>truτ₁:Tyτ₂:Tyhτ:<{ ∅ ⊢ true ⦂ τ₁ → τ₂ }>⊢ ∃ x u, <{ true }> = <{ λ ~x : τ₁ . u }> cases hτAll goals completed! 🐙
  | fls =>flsτ₁:Tyτ₂:Tyhτ:<{ ∅ ⊢ false ⦂ τ₁ → τ₂ }>⊢ ∃ x u, <{ false }> = <{ λ ~x : τ₁ . u }> cases hτAll goals completed! 🐙

6.2. Progress🔗

The progress theorem tells us that closed, well-typed terms are not stuck: either a well-typed term is a value, or it can take a reduction step. The proof is a relatively straightforward extension of the progress proof we saw in the Types chapter. We give the proof in English first, then the formal version.

Proof: By induction on the derivation of ∅ ⊢ t ⦂ τ.

The last rule of the derivation cannot be HasType.var, since a variable is never well typed in an empty context.
The HasType.tru, HasType.fls, and HasType.abs cases are trivial, since in each of these cases we can see by inspecting the rule that t is a value.
If the last rule of the derivation is HasType.app, then t has the form t₁ t₂ for some t₁ and t₂, where ∅ ⊢ t₁ ⦂ τ₂ → τ and ∅ ⊢ t₂ ⦂ τ₂ for some type τ₂. The induction hypothesis for the first subderivation says that either t₁ is a value or else it can take a reduction step.
- If t₁ is a value, then consider t₂, which by the induction hypothesis for the second subderivation must also either be a value or take a step.
  - Suppose t₂ is a value. Since t₁ is a value with an arrow type, it must be a lambda abstraction; hence t₁ t₂ can take a step by Step.appAbs.
  - Otherwise, t₂ can take a step, and hence so can t₁ t₂ by Step.app2.
- If t₁ can take a step, then so can t₁ t₂ by Step.app1.
If the last rule of the derivation is HasType.ite, then t = if t₁ then t₂ else t₃, where t₁ has type Bool. The first IH says that t₁ either is a value or takes a step.
- If t₁ is a value, then since it has type Bool it must be either true or false. If it is true, then t steps to t₂; otherwise it steps to t₃.
- Otherwise, t₁ takes a step, and therefore so does t (by Step.ifStep).

theorem progress (t : Tm) (τ : Ty) (hτ : <{ ∅ ⊢ t ⦂ τ }>) :
    t.IsValue ∨ ∃ t', t ⟶ t' := byt:Tmτ:Tyhτ:<{ ∅ ⊢ t ⦂ τ }>⊢ t.IsValue ∨ ∃ t', t ⟶ t'
  generalize hΓ : (∅ : Context) = Γ at hτt:Tmτ:TyΓ:ContexthΓ:∅ = Γhτ:<{ Γ ⊢ t ⦂ τ }>⊢ t.IsValue ∨ ∃ t', t ⟶ t'
  induction hτ with
  | var Γ x τ₁ h =>vart:Tmτ:TyΓ✝:ContextΓ:Contextx:Stringτ₁:Tyh:Γ[x] = some τ₁hΓ:∅ = Γ⊢ (Stlc.Tm.var x).IsValue ∨ ∃ t', Stlc.Tm.var x ⟶ t'
    subst hΓvart:Tmτ:TyΓ:Contextx:Stringτ₁:Tyh:∅[x] = some τ₁⊢ (Stlc.Tm.var x).IsValue ∨ ∃ t', Stlc.Tm.var x ⟶ t'
    -- Contradictory: variables cannot be typed in an empty context.
    rw [PartialMap.getElem_emptyvart:Tmτ:TyΓ:Contextx:Stringτ₁:Tyh:none = some τ₁⊢ (Stlc.Tm.var x).IsValue ∨ ∃ t', Stlc.Tm.var x ⟶ t'] at hvart:Tmτ:TyΓ:Contextx:Stringτ₁:Tyh:none = some τ₁⊢ (Stlc.Tm.var x).IsValue ∨ ∃ t', Stlc.Tm.var x ⟶ t'
    cases hAll goals completed! 🐙
  | abs =>abst:Tmτ:TyΓ:ContextΓ✝:Contextx✝:Stringτ₁✝:Tyτ₂✝:Tyt₁✝:Tmh✝:<{ ~(x✝ →ₚ τ₂✝ ; Γ✝) ⊢ t₁✝ ⦂ τ₁✝ }>h_ih✝:∅ = x✝ →ₚ τ₂✝ ; Γ✝ → t₁✝.IsValue ∨ ∃ t', t₁✝ ⟶ t'hΓ:∅ = Γ✝⊢ <{ λ ~x✝ : τ₂✝ . t₁✝ }>.IsValue ∨ ∃ t', <{ λ ~x✝ : τ₂✝ . t₁✝ }> ⟶ t' leftabst:Tmτ:TyΓ:ContextΓ✝:Contextx✝:Stringτ₁✝:Tyτ₂✝:Tyt₁✝:Tmh✝:<{ ~(x✝ →ₚ τ₂✝ ; Γ✝) ⊢ t₁✝ ⦂ τ₁✝ }>h_ih✝:∅ = x✝ →ₚ τ₂✝ ; Γ✝ → t₁✝.IsValue ∨ ∃ t', t₁✝ ⟶ t'hΓ:∅ = Γ✝⊢ <{ λ ~x✝ : τ₂✝ . t₁✝ }>.IsValue; constructorAll goals completed! 🐙
  | tru =>trut:Tmτ:TyΓ:ContextΓ✝:ContexthΓ:∅ = Γ✝⊢ <{ true }>.IsValue ∨ ∃ t', <{ true }> ⟶ t' lefttrut:Tmτ:TyΓ:ContextΓ✝:ContexthΓ:∅ = Γ✝⊢ <{ true }>.IsValue; constructorAll goals completed! 🐙
  | fls =>flst:Tmτ:TyΓ:ContextΓ✝:ContexthΓ:∅ = Γ✝⊢ <{ false }>.IsValue ∨ ∃ t', <{ false }> ⟶ t' leftflst:Tmτ:TyΓ:ContextΓ✝:ContexthΓ:∅ = Γ✝⊢ <{ false }>.IsValue; constructorAll goals completed! 🐙
  | app Γ τ₁ τ₂ t₁ t₂ h₁ h₂ ih₁ ih₂ =>appt:Tmτ:TyΓ✝:ContextΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ Γ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ Γ ⊢ t₂ ⦂ τ₂ }>ih₁:∅ = Γ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = Γ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'hΓ:∅ = Γ⊢ <{ t₁ t₂ }>.IsValue ∨ ∃ t', <{ t₁ t₂ }> ⟶ t'
    -- `t = t₁ t₂`.  Proceed by cases on whether `t₁` is a value or steps.
    subst hΓappt:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'⊢ <{ t₁ t₂ }>.IsValue ∨ ∃ t', <{ t₁ t₂ }> ⟶ t'
    rightappt:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'⊢ ∃ t', <{ t₁ t₂ }> ⟶ t'
    cases ih₁ rfl with
    | inl hv₁ =>app.inlt:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'hv₁:t₁.IsValue⊢ ∃ t', <{ t₁ t₂ }> ⟶ t'
      cases ih₂ rfl with
      | inl hv₂ =>app.inl.inlt:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'hv₁:t₁.IsValuehv₂:t₂.IsValue⊢ ∃ t', <{ t₁ t₂ }> ⟶ t'
        obtain ⟨x, u, rfl⟩ := canonical_forms_fun t₁ _ _ h₁ hv₁app.inl.inlt:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₂:Tmh₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'hv₂:t₂.IsValuex:Stringu:Tmh₁:<{ ∅ ⊢ λ ~x : τ₂ . u ⦂ τ₂ → τ₁ }>ih₁:∅ = ∅ → <{ λ ~x : τ₂ . u }>.IsValue ∨ ∃ t', <{ λ ~x : τ₂ . u }> ⟶ t'hv₁:<{ λ ~x : τ₂ . u }>.IsValue⊢ ∃ t', <{ (λ ~x : τ₂ . u) t₂ }> ⟶ t'
        exists <{ [x := t₂] u }>app.inl.inlt:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₂:Tmh₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'hv₂:t₂.IsValuex:Stringu:Tmh₁:<{ ∅ ⊢ λ ~x : τ₂ . u ⦂ τ₂ → τ₁ }>ih₁:∅ = ∅ → <{ λ ~x : τ₂ . u }>.IsValue ∨ ∃ t', <{ λ ~x : τ₂ . u }> ⟶ t'hv₁:<{ λ ~x : τ₂ . u }>.IsValue⊢ <{ (λ ~x : τ₂ . u) t₂ }> ⟶ <{ [~x := t₂] u }>
        constructorapp.inl.inlt:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₂:Tmh₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'hv₂:t₂.IsValuex:Stringu:Tmh₁:<{ ∅ ⊢ λ ~x : τ₂ . u ⦂ τ₂ → τ₁ }>ih₁:∅ = ∅ → <{ λ ~x : τ₂ . u }>.IsValue ∨ ∃ t', <{ λ ~x : τ₂ . u }> ⟶ t'hv₁:<{ λ ~x : τ₂ . u }>.IsValue⊢ t₂.IsValue
        assumptionAll goals completed! 🐙
      | inr hs₂ =>app.inl.inrt:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'hv₁:t₁.IsValuehs₂:∃ t', t₂ ⟶ t'⊢ ∃ t', <{ t₁ t₂ }> ⟶ t'
        obtain ⟨t₂', h⟩ := hs₂app.inl.inrt:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'hv₁:t₁.IsValuet₂':Tmh:t₂ ⟶ t₂'⊢ ∃ t', <{ t₁ t₂ }> ⟶ t'
        exists <{ t₁ t₂' }>app.inl.inrt:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'hv₁:t₁.IsValuet₂':Tmh:t₂ ⟶ t₂'⊢ <{ t₁ t₂ }> ⟶ <{ t₁ t₂' }>
        constructorapp.inl.inr.hvt:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'hv₁:t₁.IsValuet₂':Tmh:t₂ ⟶ t₂'⊢ t₁.IsValueapp.inl.inr.ht:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'hv₁:t₁.IsValuet₂':Tmh:t₂ ⟶ t₂'⊢ t₂ ⟶ t₂' <;>app.inl.inr.hvt:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'hv₁:t₁.IsValuet₂':Tmh:t₂ ⟶ t₂'⊢ t₁.IsValueapp.inl.inr.ht:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'hv₁:t₁.IsValuet₂':Tmh:t₂ ⟶ t₂'⊢ t₂ ⟶ t₂' assumptionAll goals completed! 🐙
    | inr hs₁ =>app.inrt:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'hs₁:∃ t', t₁ ⟶ t'⊢ ∃ t', <{ t₁ t₂ }> ⟶ t'
      obtain ⟨t₁', h⟩ := hs₁app.inrt:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t't₁':Tmh:t₁ ⟶ t₁'⊢ ∃ t', <{ t₁ t₂ }> ⟶ t'
      exists <{ t₁' t₂ }>app.inrt:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t't₁':Tmh:t₁ ⟶ t₁'⊢ <{ t₁ t₂ }> ⟶ <{ t₁' t₂ }>
      constructorapp.inrt:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t't₁':Tmh:t₁ ⟶ t₁'⊢ t₁ ⟶ t₁' <;>app.inrt:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t't₁':Tmh:t₁ ⟶ t₁'⊢ t₁ ⟶ t₁' assumptionAll goals completed! 🐙
  | ite Γ t₁ t₂ t₃ τ₁ h₁ h₂ h₃ ih₁ ih₂ ih₃ =>itet:Tmτ:TyΓ✝:ContextΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ Γ ⊢ t₁ ⦂ Bool }>h₂:<{ Γ ⊢ t₂ ⦂ τ₁ }>h₃:<{ Γ ⊢ t₃ ⦂ τ₁ }>ih₁:∅ = Γ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = Γ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'ih₃:∅ = Γ → t₃.IsValue ∨ ∃ t', t₃ ⟶ t'hΓ:∅ = Γ⊢ <{ if t₁ then t₂ else t₃ }>.IsValue ∨ ∃ t', <{ if t₁ then t₂ else t₃ }> ⟶ t'
    subst hΓitet:Tmτ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'ih₃:∅ = ∅ → t₃.IsValue ∨ ∃ t', t₃ ⟶ t'⊢ <{ if t₁ then t₂ else t₃ }>.IsValue ∨ ∃ t', <{ if t₁ then t₂ else t₃ }> ⟶ t'
    rightitet:Tmτ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'ih₃:∅ = ∅ → t₃.IsValue ∨ ∃ t', t₃ ⟶ t'⊢ ∃ t', <{ if t₁ then t₂ else t₃ }> ⟶ t'
    cases ih₁ rfl with
    | inl hv₁ =>ite.inlt:Tmτ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'ih₃:∅ = ∅ → t₃.IsValue ∨ ∃ t', t₃ ⟶ t'hv₁:t₁.IsValue⊢ ∃ t', <{ if t₁ then t₂ else t₃ }> ⟶ t'
      cases canonical_forms_bool t₁ h₁ hv₁ with
      | inl he =>ite.inl.inlt:Tmτ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'ih₃:∅ = ∅ → t₃.IsValue ∨ ∃ t', t₃ ⟶ t'hv₁:t₁.IsValuehe:t₁ = <{ true }>⊢ ∃ t', <{ if t₁ then t₂ else t₃ }> ⟶ t'
        subst heite.inl.inlt:Tmτ:TyΓ:Contextt₂:Tmt₃:Tmτ₁:Tyh₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'ih₃:∅ = ∅ → t₃.IsValue ∨ ∃ t', t₃ ⟶ t'h₁:<{ ∅ ⊢ true ⦂ Bool }>ih₁:∅ = ∅ → <{ true }>.IsValue ∨ ∃ t', <{ true }> ⟶ t'hv₁:<{ true }>.IsValue⊢ ∃ t', <{ if true then t₂ else t₃ }> ⟶ t'
        exists t₂ite.inl.inlt:Tmτ:TyΓ:Contextt₂:Tmt₃:Tmτ₁:Tyh₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'ih₃:∅ = ∅ → t₃.IsValue ∨ ∃ t', t₃ ⟶ t'h₁:<{ ∅ ⊢ true ⦂ Bool }>ih₁:∅ = ∅ → <{ true }>.IsValue ∨ ∃ t', <{ true }> ⟶ t'hv₁:<{ true }>.IsValue⊢ <{ if true then t₂ else t₃ }> ⟶ t₂
        constructorAll goals completed! 🐙
      | inr he =>ite.inl.inrt:Tmτ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'ih₃:∅ = ∅ → t₃.IsValue ∨ ∃ t', t₃ ⟶ t'hv₁:t₁.IsValuehe:t₁ = <{ false }>⊢ ∃ t', <{ if t₁ then t₂ else t₃ }> ⟶ t'
        subst heite.inl.inrt:Tmτ:TyΓ:Contextt₂:Tmt₃:Tmτ₁:Tyh₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'ih₃:∅ = ∅ → t₃.IsValue ∨ ∃ t', t₃ ⟶ t'h₁:<{ ∅ ⊢ false ⦂ Bool }>ih₁:∅ = ∅ → <{ false }>.IsValue ∨ ∃ t', <{ false }> ⟶ t'hv₁:<{ false }>.IsValue⊢ ∃ t', <{ if false then t₂ else t₃ }> ⟶ t'
        exists t₃ite.inl.inrt:Tmτ:TyΓ:Contextt₂:Tmt₃:Tmτ₁:Tyh₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'ih₃:∅ = ∅ → t₃.IsValue ∨ ∃ t', t₃ ⟶ t'h₁:<{ ∅ ⊢ false ⦂ Bool }>ih₁:∅ = ∅ → <{ false }>.IsValue ∨ ∃ t', <{ false }> ⟶ t'hv₁:<{ false }>.IsValue⊢ <{ if false then t₂ else t₃ }> ⟶ t₃
        constructorAll goals completed! 🐙
    | inr hs₁ =>ite.inrt:Tmτ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'ih₃:∅ = ∅ → t₃.IsValue ∨ ∃ t', t₃ ⟶ t'hs₁:∃ t', t₁ ⟶ t'⊢ ∃ t', <{ if t₁ then t₂ else t₃ }> ⟶ t'
      obtain ⟨t₁', h⟩ := hs₁ite.inrt:Tmτ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'ih₃:∅ = ∅ → t₃.IsValue ∨ ∃ t', t₃ ⟶ t't₁':Tmh:t₁ ⟶ t₁'⊢ ∃ t', <{ if t₁ then t₂ else t₃ }> ⟶ t'
      exists <{ if t₁' then t₂ else t₃ }>ite.inrt:Tmτ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'ih₃:∅ = ∅ → t₃.IsValue ∨ ∃ t', t₃ ⟶ t't₁':Tmh:t₁ ⟶ t₁'⊢ <{ if t₁ then t₂ else t₃ }> ⟶ <{ if t₁' then t₂ else t₃ }>
      constructorite.inrt:Tmτ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₁:∅ = ∅ → t₁.IsValue ∨ ∃ t', t₁ ⟶ t'ih₂:∅ = ∅ → t₂.IsValue ∨ ∃ t', t₂ ⟶ t'ih₃:∅ = ∅ → t₃.IsValue ∨ ∃ t', t₃ ⟶ t't₁':Tmh:t₁ ⟶ t₁'⊢ t₁ ⟶ t₁'
      assumptionAll goals completed! 🐙

Exercise★★★(progress_from_term_ind) (Advanced)

Show that progress can also be proved by induction on terms instead of induction on typing derivations.

theorem declaration uses `sorry`progress' (t : Tm) (τ : Ty) (hτ : <{ ∅ ⊢ t ⦂ τ }>) :
    t.IsValue ∨ ∃ t', t ⟶ t' := byt:Tmτ:Tyhτ:<{ ∅ ⊢ t ⦂ τ }>⊢ t.IsValue ∨ ∃ t', t ⟶ t'
  sorryAll goals completed! 🐙

6.3. Preservation🔗

The other half of the type soundness property is the preservation of types during reduction. For this part, we'll need to develop some technical machinery for reasoning about variables and substitution. Working from top to bottom (from the high-level property we are actually interested in to the lowest-level technical lemmas that are needed by various cases of the more interesting proofs), the story goes like this:

The preservation theorem is proved by induction on a typing derivation and case analysis on the step relation, pretty much as we did in the Types chapter. The one case that is significantly different is the one for the Step.appAbs rule, whose definition uses the substitution operation. To see that this step preserves typing, we need to know that the substitution itself does. So we prove a...
substitution lemma, stating that substituting a (closed, well-typed) term s for a variable x in a term t preserves the type of t. The proof goes by induction on the form of t and requires looking at all the different cases in the definition of substitution. This time, for the variables case, we discover that we need to deduce from the fact that a term s has type σ in the empty context the fact that s has type σ in every context. For this we prove a...
weakening lemma, showing that typing is preserved under "extensions" to the context Γ.

To make Lean happy, though, we need to formalize the story in the opposite order, starting with weakening...

6.3.1. The Weakening Lemma🔗

First, we show that typing is preserved under "extensions" to the context Γ. (Recall map inclusion, Γ ⊆ Γ', from the Typeclasses chapter.)

theorem weakening {Γ Γ' : Context} {t : Tm} {τ : Ty}
    (hi : Γ ⊆ Γ') (ht : <{ Γ ⊢ t ⦂ τ }>) : <{ Γ' ⊢ t ⦂ τ }> := byΓ:ContextΓ':Contextt:Tmτ:Tyhi:Γ ⊆ Γ'ht:<{ Γ ⊢ t ⦂ τ }>⊢ <{ Γ' ⊢ t ⦂ τ }>
  induction ht generalizing Γ' with
  | var _ x _ h =>varΓ:Contextt:Tmτ:TyΓ✝:Contextx:Stringτ₁✝:Tyh:Γ✝[x] = some τ₁✝Γ':Contexthi:Γ✝ ⊆ Γ'⊢ <{ Γ' ⊢ ~(Stlc.Tm.var x) ⦂ τ₁✝ }>
    constructorvarΓ:Contextt:Tmτ:TyΓ✝:Contextx:Stringτ₁✝:Tyh:Γ✝[x] = some τ₁✝Γ':Contexthi:Γ✝ ⊆ Γ'⊢ Γ'[x] = some τ₁✝
    exact hi hAll goals completed! 🐙
  | abs _ x _ _ _ _ ih =>absΓ:Contextt:Tmτ:TyΓ✝:Contextx:Stringτ₁✝:Tyτ₂✝:Tyt₁✝:Tmh✝:<{ ~(x →ₚ τ₂✝ ; Γ✝) ⊢ t₁✝ ⦂ τ₁✝ }>ih:∀ {Γ' : Context}, x →ₚ τ₂✝ ; Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ τ₁✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ <{ Γ' ⊢ λ ~x : τ₂✝ . t₁✝ ⦂ τ₂✝ → τ₁✝ }>
    constructorabsΓ:Contextt:Tmτ:TyΓ✝:Contextx:Stringτ₁✝:Tyτ₂✝:Tyt₁✝:Tmh✝:<{ ~(x →ₚ τ₂✝ ; Γ✝) ⊢ t₁✝ ⦂ τ₁✝ }>ih:∀ {Γ' : Context}, x →ₚ τ₂✝ ; Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ τ₁✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ <{ ~(x →ₚ τ₂✝ ; Γ') ⊢ t₁✝ ⦂ τ₁✝ }>
    apply ihabsΓ:Contextt:Tmτ:TyΓ✝:Contextx:Stringτ₁✝:Tyτ₂✝:Tyt₁✝:Tmh✝:<{ ~(x →ₚ τ₂✝ ; Γ✝) ⊢ t₁✝ ⦂ τ₁✝ }>ih:∀ {Γ' : Context}, x →ₚ τ₂✝ ; Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ τ₁✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ x →ₚ τ₂✝ ; Γ✝ ⊆ x →ₚ τ₂✝ ; Γ'
    apply PartialMap.update_subsetabsΓ:Contextt:Tmτ:TyΓ✝:Contextx:Stringτ₁✝:Tyτ₂✝:Tyt₁✝:Tmh✝:<{ ~(x →ₚ τ₂✝ ; Γ✝) ⊢ t₁✝ ⦂ τ₁✝ }>ih:∀ {Γ' : Context}, x →ₚ τ₂✝ ; Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ τ₁✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ Γ✝ ⊆ Γ'
    assumptionAll goals completed! 🐙
  | app _ _ _ _ _ _ _ ih₁ ih₂ =>appΓ:Contextt:Tmτ:TyΓ✝:Contextτ₁✝:Tyτ₂✝:Tyt₁✝:Tmt₂✝:Tmh₁✝:<{ Γ✝ ⊢ t₁✝ ⦂ τ₂✝ → τ₁✝ }>h₂✝:<{ Γ✝ ⊢ t₂✝ ⦂ τ₂✝ }>ih₁:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ τ₂✝ → τ₁✝ }>ih₂:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₂✝ ⦂ τ₂✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ <{ Γ' ⊢ t₁✝ t₂✝ ⦂ τ₁✝ }>
    constructorapp.h₁Γ:Contextt:Tmτ:TyΓ✝:Contextτ₁✝:Tyτ₂✝:Tyt₁✝:Tmt₂✝:Tmh₁✝:<{ Γ✝ ⊢ t₁✝ ⦂ τ₂✝ → τ₁✝ }>h₂✝:<{ Γ✝ ⊢ t₂✝ ⦂ τ₂✝ }>ih₁:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ τ₂✝ → τ₁✝ }>ih₂:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₂✝ ⦂ τ₂✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ <{ Γ' ⊢ t₁✝ ⦂ ~?app.τ₂ → τ₁✝ }>app.h₂Γ:Contextt:Tmτ:TyΓ✝:Contextτ₁✝:Tyτ₂✝:Tyt₁✝:Tmt₂✝:Tmh₁✝:<{ Γ✝ ⊢ t₁✝ ⦂ τ₂✝ → τ₁✝ }>h₂✝:<{ Γ✝ ⊢ t₂✝ ⦂ τ₂✝ }>ih₁:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ τ₂✝ → τ₁✝ }>ih₂:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₂✝ ⦂ τ₂✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ <{ Γ' ⊢ t₂✝ ⦂ ~?app.τ₂ }>app.τ₂Γ:Contextt:Tmτ:TyΓ✝:Contextτ₁✝:Tyτ₂✝:Tyt₁✝:Tmt₂✝:Tmh₁✝:<{ Γ✝ ⊢ t₁✝ ⦂ τ₂✝ → τ₁✝ }>h₂✝:<{ Γ✝ ⊢ t₂✝ ⦂ τ₂✝ }>ih₁:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ τ₂✝ → τ₁✝ }>ih₂:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₂✝ ⦂ τ₂✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ Ty
    ·app.h₁Γ:Contextt:Tmτ:TyΓ✝:Contextτ₁✝:Tyτ₂✝:Tyt₁✝:Tmt₂✝:Tmh₁✝:<{ Γ✝ ⊢ t₁✝ ⦂ τ₂✝ → τ₁✝ }>h₂✝:<{ Γ✝ ⊢ t₂✝ ⦂ τ₂✝ }>ih₁:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ τ₂✝ → τ₁✝ }>ih₂:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₂✝ ⦂ τ₂✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ <{ Γ' ⊢ t₁✝ ⦂ ~?app.τ₂ → τ₁✝ }> apply ih₁app.h₁Γ:Contextt:Tmτ:TyΓ✝:Contextτ₁✝:Tyτ₂✝:Tyt₁✝:Tmt₂✝:Tmh₁✝:<{ Γ✝ ⊢ t₁✝ ⦂ τ₂✝ → τ₁✝ }>h₂✝:<{ Γ✝ ⊢ t₂✝ ⦂ τ₂✝ }>ih₁:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ τ₂✝ → τ₁✝ }>ih₂:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₂✝ ⦂ τ₂✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ Γ✝ ⊆ Γ'
      exact hiAll goals completed! 🐙
    ·app.h₂Γ:Contextt:Tmτ:TyΓ✝:Contextτ₁✝:Tyτ₂✝:Tyt₁✝:Tmt₂✝:Tmh₁✝:<{ Γ✝ ⊢ t₁✝ ⦂ τ₂✝ → τ₁✝ }>h₂✝:<{ Γ✝ ⊢ t₂✝ ⦂ τ₂✝ }>ih₁:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ τ₂✝ → τ₁✝ }>ih₂:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₂✝ ⦂ τ₂✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ <{ Γ' ⊢ t₂✝ ⦂ τ₂✝ }> apply ih₂app.h₂Γ:Contextt:Tmτ:TyΓ✝:Contextτ₁✝:Tyτ₂✝:Tyt₁✝:Tmt₂✝:Tmh₁✝:<{ Γ✝ ⊢ t₁✝ ⦂ τ₂✝ → τ₁✝ }>h₂✝:<{ Γ✝ ⊢ t₂✝ ⦂ τ₂✝ }>ih₁:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ τ₂✝ → τ₁✝ }>ih₂:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₂✝ ⦂ τ₂✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ Γ✝ ⊆ Γ'
      exact hiAll goals completed! 🐙
  | tru =>truΓ:Contextt:Tmτ:TyΓ✝:ContextΓ':Contexthi:Γ✝ ⊆ Γ'⊢ <{ Γ' ⊢ true ⦂ Bool }> constructorAll goals completed! 🐙
  | fls =>flsΓ:Contextt:Tmτ:TyΓ✝:ContextΓ':Contexthi:Γ✝ ⊆ Γ'⊢ <{ Γ' ⊢ false ⦂ Bool }> constructorAll goals completed! 🐙
  | ite _ _ _ _ _ _ _ _ ih₁ ih₂ ih₃ =>iteΓ:Contextt:Tmτ:TyΓ✝:Contextt₁✝:Tmt₂✝:Tmt₃✝:Tmτ₁✝:Tyh₁✝:<{ Γ✝ ⊢ t₁✝ ⦂ Bool }>h₂✝:<{ Γ✝ ⊢ t₂✝ ⦂ τ₁✝ }>h₃✝:<{ Γ✝ ⊢ t₃✝ ⦂ τ₁✝ }>ih₁:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ Bool }>ih₂:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₂✝ ⦂ τ₁✝ }>ih₃:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₃✝ ⦂ τ₁✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ <{ Γ' ⊢ if t₁✝ then t₂✝ else t₃✝ ⦂ τ₁✝ }>
    constructorite.h₁Γ:Contextt:Tmτ:TyΓ✝:Contextt₁✝:Tmt₂✝:Tmt₃✝:Tmτ₁✝:Tyh₁✝:<{ Γ✝ ⊢ t₁✝ ⦂ Bool }>h₂✝:<{ Γ✝ ⊢ t₂✝ ⦂ τ₁✝ }>h₃✝:<{ Γ✝ ⊢ t₃✝ ⦂ τ₁✝ }>ih₁:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ Bool }>ih₂:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₂✝ ⦂ τ₁✝ }>ih₃:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₃✝ ⦂ τ₁✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ <{ Γ' ⊢ t₁✝ ⦂ Bool }>ite.h₂Γ:Contextt:Tmτ:TyΓ✝:Contextt₁✝:Tmt₂✝:Tmt₃✝:Tmτ₁✝:Tyh₁✝:<{ Γ✝ ⊢ t₁✝ ⦂ Bool }>h₂✝:<{ Γ✝ ⊢ t₂✝ ⦂ τ₁✝ }>h₃✝:<{ Γ✝ ⊢ t₃✝ ⦂ τ₁✝ }>ih₁:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ Bool }>ih₂:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₂✝ ⦂ τ₁✝ }>ih₃:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₃✝ ⦂ τ₁✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ <{ Γ' ⊢ t₂✝ ⦂ τ₁✝ }>ite.h₃Γ:Contextt:Tmτ:TyΓ✝:Contextt₁✝:Tmt₂✝:Tmt₃✝:Tmτ₁✝:Tyh₁✝:<{ Γ✝ ⊢ t₁✝ ⦂ Bool }>h₂✝:<{ Γ✝ ⊢ t₂✝ ⦂ τ₁✝ }>h₃✝:<{ Γ✝ ⊢ t₃✝ ⦂ τ₁✝ }>ih₁:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ Bool }>ih₂:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₂✝ ⦂ τ₁✝ }>ih₃:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₃✝ ⦂ τ₁✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ <{ Γ' ⊢ t₃✝ ⦂ τ₁✝ }>
    ·ite.h₁Γ:Contextt:Tmτ:TyΓ✝:Contextt₁✝:Tmt₂✝:Tmt₃✝:Tmτ₁✝:Tyh₁✝:<{ Γ✝ ⊢ t₁✝ ⦂ Bool }>h₂✝:<{ Γ✝ ⊢ t₂✝ ⦂ τ₁✝ }>h₃✝:<{ Γ✝ ⊢ t₃✝ ⦂ τ₁✝ }>ih₁:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ Bool }>ih₂:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₂✝ ⦂ τ₁✝ }>ih₃:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₃✝ ⦂ τ₁✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ <{ Γ' ⊢ t₁✝ ⦂ Bool }> apply ih₁ite.h₁Γ:Contextt:Tmτ:TyΓ✝:Contextt₁✝:Tmt₂✝:Tmt₃✝:Tmτ₁✝:Tyh₁✝:<{ Γ✝ ⊢ t₁✝ ⦂ Bool }>h₂✝:<{ Γ✝ ⊢ t₂✝ ⦂ τ₁✝ }>h₃✝:<{ Γ✝ ⊢ t₃✝ ⦂ τ₁✝ }>ih₁:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ Bool }>ih₂:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₂✝ ⦂ τ₁✝ }>ih₃:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₃✝ ⦂ τ₁✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ Γ✝ ⊆ Γ'
      exact hiAll goals completed! 🐙
    ·ite.h₂Γ:Contextt:Tmτ:TyΓ✝:Contextt₁✝:Tmt₂✝:Tmt₃✝:Tmτ₁✝:Tyh₁✝:<{ Γ✝ ⊢ t₁✝ ⦂ Bool }>h₂✝:<{ Γ✝ ⊢ t₂✝ ⦂ τ₁✝ }>h₃✝:<{ Γ✝ ⊢ t₃✝ ⦂ τ₁✝ }>ih₁:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ Bool }>ih₂:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₂✝ ⦂ τ₁✝ }>ih₃:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₃✝ ⦂ τ₁✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ <{ Γ' ⊢ t₂✝ ⦂ τ₁✝ }> apply ih₂ite.h₂Γ:Contextt:Tmτ:TyΓ✝:Contextt₁✝:Tmt₂✝:Tmt₃✝:Tmτ₁✝:Tyh₁✝:<{ Γ✝ ⊢ t₁✝ ⦂ Bool }>h₂✝:<{ Γ✝ ⊢ t₂✝ ⦂ τ₁✝ }>h₃✝:<{ Γ✝ ⊢ t₃✝ ⦂ τ₁✝ }>ih₁:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ Bool }>ih₂:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₂✝ ⦂ τ₁✝ }>ih₃:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₃✝ ⦂ τ₁✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ Γ✝ ⊆ Γ'
      exact hiAll goals completed! 🐙
    ·ite.h₃Γ:Contextt:Tmτ:TyΓ✝:Contextt₁✝:Tmt₂✝:Tmt₃✝:Tmτ₁✝:Tyh₁✝:<{ Γ✝ ⊢ t₁✝ ⦂ Bool }>h₂✝:<{ Γ✝ ⊢ t₂✝ ⦂ τ₁✝ }>h₃✝:<{ Γ✝ ⊢ t₃✝ ⦂ τ₁✝ }>ih₁:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ Bool }>ih₂:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₂✝ ⦂ τ₁✝ }>ih₃:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₃✝ ⦂ τ₁✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ <{ Γ' ⊢ t₃✝ ⦂ τ₁✝ }> apply ih₃ite.h₃Γ:Contextt:Tmτ:TyΓ✝:Contextt₁✝:Tmt₂✝:Tmt₃✝:Tmτ₁✝:Tyh₁✝:<{ Γ✝ ⊢ t₁✝ ⦂ Bool }>h₂✝:<{ Γ✝ ⊢ t₂✝ ⦂ τ₁✝ }>h₃✝:<{ Γ✝ ⊢ t₃✝ ⦂ τ₁✝ }>ih₁:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₁✝ ⦂ Bool }>ih₂:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₂✝ ⦂ τ₁✝ }>ih₃:∀ {Γ' : Context}, Γ✝ ⊆ Γ' → <{ Γ' ⊢ t₃✝ ⦂ τ₁✝ }>Γ':Contexthi:Γ✝ ⊆ Γ'⊢ Γ✝ ⊆ Γ'
      exact hiAll goals completed! 🐙

Through judicious use of apply_rules, we can heavily automate this proof. The tactic after with is applied to every case of the induction and handles all the cases using apply_rules's automation. We must give the tactic access to all the HasType constructors and the PartialMap.update_subset lemma for this to work:

theorem weakening' {Γ Γ' : Context} {t : Tm} {τ : Ty}
    (hi : Γ ⊆ Γ') (ht : <{ Γ ⊢ t ⦂ τ }>) : <{ Γ' ⊢ t ⦂ τ }> := byΓ:ContextΓ':Contextt:Tmτ:Tyhi:Γ ⊆ Γ'ht:<{ Γ ⊢ t ⦂ τ }>⊢ <{ Γ' ⊢ t ⦂ τ }>
  induction ht generalizing Γ' with (apply_rules [PartialMap.update_subset] using StlcTypingAll goals completed! 🐙)

The following simple corollary is what we actually need below.

theorem weakening_empty {Γ : Context} {t : Tm} {τ : Ty} (ht : <{ ∅ ⊢ t ⦂ τ }>) :
    <{ Γ ⊢ t ⦂ τ }> := byΓ:Contextt:Tmτ:Tyht:<{ ∅ ⊢ t ⦂ τ }>⊢ <{ Γ ⊢ t ⦂ τ }>
  apply weakening (Γ := ∅)hiΓ:Contextt:Tmτ:Tyht:<{ ∅ ⊢ t ⦂ τ }>⊢ ∅ ⊆ ΓhtΓ:Contextt:Tmτ:Tyht:<{ ∅ ⊢ t ⦂ τ }>⊢ <{ ∅ ⊢ t ⦂ τ }>
  -- this is the "manual" way to show that the empty context is a subset of any context:
  -- show that a 'lookup' in it is impossible.
  ·hiΓ:Contextt:Tmτ:Tyht:<{ ∅ ⊢ t ⦂ τ }>⊢ ∅ ⊆ Γ intros x b contrahiΓ:Contextt:Tmτ:Tyht:<{ ∅ ⊢ t ⦂ τ }>x:Stringb:Tycontra:∅[x] = some b⊢ Γ[x] = some b
    contradictionAll goals completed! 🐙
  ·htΓ:Contextt:Tmτ:Tyht:<{ ∅ ⊢ t ⦂ τ }>⊢ <{ ∅ ⊢ t ⦂ τ }> assumptionAll goals completed! 🐙

6.3.2. The Substitution Lemma🔗

Now we come to the conceptual heart of the proof that reduction preserves types — namely, the observation that substitution preserves types.

Formally, the so-called substitution lemma says this: Suppose we have a term t with a free variable x, and suppose we've assigned a type τ to t under the assumption that x has some type τ'. Also, suppose that we have some other term v and that we've shown that v has type τ'. Then, since v satisfies the assumption we made about x when typing t, we can substitute v for each of the occurrences of x in t and obtain a new term that still has type τ.

theorem substitution_preserves_typing (Γ : Context) (x : String) (τ' : Ty)
    (t v : Tm) (τ : Ty)
    (hτ : <{ x ↦ τ' ; Γ ⊢ t ⦂ τ }>) (hv : <{ ∅ ⊢ v ⦂ τ' }>) :
    <{ Γ ⊢ [x := v] t ⦂ τ }> := byΓ:Contextx:Stringτ':Tyt:Tmv:Tmτ:Tyhτ:<{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }>hv:<{ ∅ ⊢ v ⦂ τ' }>⊢ <{ Γ ⊢ [~x := v] t ⦂ τ }>
  -- By induction on `t`; in each case we get at the derivation of `hτ`.
  induction t generalizing Γ τ with
  | var y =>varx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:StringΓ:Contextτ:Tyhτ:<{ ~(x →ₚ τ' ; Γ) ⊢ ~(Stlc.Tm.var y) ⦂ τ }>⊢ <{ Γ ⊢ [~x := v] ~(Stlc.Tm.var y) ⦂ τ }>
    cases hτ with
    | var _ _ _ h =>var.varx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:StringΓ:Contextτ:Tyh:(x →ₚ τ' ; Γ)[y] = some τ⊢ <{ Γ ⊢ [~x := v] ~(Stlc.Tm.var y) ⦂ τ }>
      by_cases hxy : x = yposx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:StringΓ:Contextτ:Tyh:(x →ₚ τ' ; Γ)[y] = some τhxy:x = y⊢ <{ Γ ⊢ [~x := v] ~(Stlc.Tm.var y) ⦂ τ }>negx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:StringΓ:Contextτ:Tyh:(x →ₚ τ' ; Γ)[y] = some τhxy:¬x = y⊢ <{ Γ ⊢ [~x := v] ~(Stlc.Tm.var y) ⦂ τ }>
      ·posx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:StringΓ:Contextτ:Tyh:(x →ₚ τ' ; Γ)[y] = some τhxy:x = y⊢ <{ Γ ⊢ [~x := v] ~(Stlc.Tm.var y) ⦂ τ }> subst hxyposx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>Γ:Contextτ:Tyh:(x →ₚ τ' ; Γ)[x] = some τ⊢ <{ Γ ⊢ [~x := v] ~(Stlc.Tm.var x) ⦂ τ }>
        rw [PartialMap.update_eqposx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>Γ:Contextτ:Tyh:some τ' = some τ⊢ <{ Γ ⊢ [~x := v] ~(Stlc.Tm.var x) ⦂ τ }>] at hposx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>Γ:Contextτ:Tyh:some τ' = some τ⊢ <{ Γ ⊢ [~x := v] ~(Stlc.Tm.var x) ⦂ τ }>
        rw [subst_var_eqposx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>Γ:Contextτ:Tyh:some τ' = some τ⊢ <{ Γ ⊢ v ⦂ τ }>]posx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>Γ:Contextτ:Tyh:some τ' = some τ⊢ <{ Γ ⊢ v ⦂ τ }>
        have hτ'τ : τ' = τ := byΓ:Contextx:Stringτ':Tyt:Tmv:Tmτ:Tyhτ:<{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }>hv:<{ ∅ ⊢ v ⦂ τ' }>⊢ <{ Γ ⊢ [~x := v] t ⦂ τ }>
          apply Option.some.injx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>Γ:Contextτ:Tyh:some τ' = some τ⊢ some τ' = some τ
          exact hposx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>Γ:Contextτ:Tyh:some τ' = some τhτ'τ:τ' = τ⊢ <{ Γ ⊢ v ⦂ τ }>
        subst hτ'τposx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>Γ:Contexth:some τ' = some τ'⊢ <{ Γ ⊢ v ⦂ τ' }>
        apply weakening_emptyposx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>Γ:Contexth:some τ' = some τ'⊢ <{ ∅ ⊢ v ⦂ τ' }>
        exact hvAll goals completed! 🐙
      ·negx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:StringΓ:Contextτ:Tyh:(x →ₚ τ' ; Γ)[y] = some τhxy:¬x = y⊢ <{ Γ ⊢ [~x := v] ~(Stlc.Tm.var y) ⦂ τ }> rw [PartialMap.update_neq hxynegx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:StringΓ:Contextτ:Tyh:Γ[y] = some τhxy:¬x = y⊢ <{ Γ ⊢ [~x := v] ~(Stlc.Tm.var y) ⦂ τ }>] at hnegx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:StringΓ:Contextτ:Tyh:Γ[y] = some τhxy:¬x = y⊢ <{ Γ ⊢ [~x := v] ~(Stlc.Tm.var y) ⦂ τ }>
        rw [subst_var_ne _ _ _ hxynegx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:StringΓ:Contextτ:Tyh:Γ[y] = some τhxy:¬x = y⊢ <{ Γ ⊢ ~(Stlc.Tm.var y) ⦂ τ }>]negx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:StringΓ:Contextτ:Tyh:Γ[y] = some τhxy:¬x = y⊢ <{ Γ ⊢ ~(Stlc.Tm.var y) ⦂ τ }>
        constructornegx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:StringΓ:Contextτ:Tyh:Γ[y] = some τhxy:¬x = y⊢ Γ[y] = some τ
        exact hAll goals completed! 🐙
  | app t₁ t₂ ih₁ ih₂ =>appx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>t₁:Tmt₂:Tmih₁:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>ih₂:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₂ ⦂ τ }>Γ:Contextτ:Tyhτ:<{ ~(x →ₚ τ' ; Γ) ⊢ t₁ t₂ ⦂ τ }>⊢ <{ Γ ⊢ [~x := v] (t₁ t₂) ⦂ τ }>
    cases hτ with
    | app _ _ _ _ _ h₁ h₂ =>app.appx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>t₁:Tmt₂:Tmih₁:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>ih₂:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₂ ⦂ τ }>Γ:Contextτ:Tyτ₂✝:Tyh₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ₂✝ }>h₁:<{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ₂✝ → τ }>⊢ <{ Γ ⊢ [~x := v] (t₁ t₂) ⦂ τ }>
      rw [subst_appapp.appx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>t₁:Tmt₂:Tmih₁:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>ih₂:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₂ ⦂ τ }>Γ:Contextτ:Tyτ₂✝:Tyh₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ₂✝ }>h₁:<{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ₂✝ → τ }>⊢ <{ Γ ⊢ [~x := v] t₁ [~x := v] t₂ ⦂ τ }>]app.appx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>t₁:Tmt₂:Tmih₁:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>ih₂:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₂ ⦂ τ }>Γ:Contextτ:Tyτ₂✝:Tyh₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ₂✝ }>h₁:<{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ₂✝ → τ }>⊢ <{ Γ ⊢ [~x := v] t₁ [~x := v] t₂ ⦂ τ }>
      constructorapp.app.h₁x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>t₁:Tmt₂:Tmih₁:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>ih₂:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₂ ⦂ τ }>Γ:Contextτ:Tyτ₂✝:Tyh₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ₂✝ }>h₁:<{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ₂✝ → τ }>⊢ <{ Γ ⊢ [~x := v] t₁ ⦂ ~?app.app.τ₂ → τ }>app.app.h₂x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>t₁:Tmt₂:Tmih₁:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>ih₂:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₂ ⦂ τ }>Γ:Contextτ:Tyτ₂✝:Tyh₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ₂✝ }>h₁:<{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ₂✝ → τ }>⊢ <{ Γ ⊢ [~x := v] t₂ ⦂ ~?app.app.τ₂ }>app.app.τ₂x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>t₁:Tmt₂:Tmih₁:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>ih₂:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₂ ⦂ τ }>Γ:Contextτ:Tyτ₂✝:Tyh₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ₂✝ }>h₁:<{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ₂✝ → τ }>⊢ Ty
      ·app.app.h₁x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>t₁:Tmt₂:Tmih₁:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>ih₂:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₂ ⦂ τ }>Γ:Contextτ:Tyτ₂✝:Tyh₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ₂✝ }>h₁:<{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ₂✝ → τ }>⊢ <{ Γ ⊢ [~x := v] t₁ ⦂ ~?app.app.τ₂ → τ }> apply ih₁app.app.h₁x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>t₁:Tmt₂:Tmih₁:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>ih₂:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₂ ⦂ τ }>Γ:Contextτ:Tyτ₂✝:Tyh₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ₂✝ }>h₁:<{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ₂✝ → τ }>⊢ <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ ~?app.app.τ₂ → τ }>
        exact h₁All goals completed! 🐙
      ·app.app.h₂x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>t₁:Tmt₂:Tmih₁:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>ih₂:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₂ ⦂ τ }>Γ:Contextτ:Tyτ₂✝:Tyh₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ₂✝ }>h₁:<{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ₂✝ → τ }>⊢ <{ Γ ⊢ [~x := v] t₂ ⦂ τ₂✝ }> apply ih₂app.app.h₂x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>t₁:Tmt₂:Tmih₁:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>ih₂:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₂ ⦂ τ }>Γ:Contextτ:Tyτ₂✝:Tyh₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ₂✝ }>h₁:<{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ₂✝ → τ }>⊢ <{ ~(x →ₚ τ' ; Γ) ⊢ t₂ ⦂ τ₂✝ }>
        exact h₂All goals completed! 🐙
  | abs y σ t₁ ih =>absx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:Stringσ:Tyt₁:Tmih:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>Γ:Contextτ:Tyhτ:<{ ~(x →ₚ τ' ; Γ) ⊢ λ ~y : σ . t₁ ⦂ τ }>⊢ <{ Γ ⊢ [~x := v] (λ ~y : σ . t₁) ⦂ τ }>
    cases hτ with
    | abs _ _ _ _ _ h =>abs.absx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:Stringσ:Tyt₁:Tmih:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>Γ:Contextτ₁✝:Tyh:<{ ~(y →ₚ σ ; x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ₁✝ }>⊢ <{ Γ ⊢ [~x := v] (λ ~y : σ . t₁) ⦂ σ → τ₁✝ }>
      by_cases hxy : x = yposx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:Stringσ:Tyt₁:Tmih:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>Γ:Contextτ₁✝:Tyh:<{ ~(y →ₚ σ ; x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ₁✝ }>hxy:x = y⊢ <{ Γ ⊢ [~x := v] (λ ~y : σ . t₁) ⦂ σ → τ₁✝ }>negx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:Stringσ:Tyt₁:Tmih:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>Γ:Contextτ₁✝:Tyh:<{ ~(y →ₚ σ ; x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ₁✝ }>hxy:¬x = y⊢ <{ Γ ⊢ [~x := v] (λ ~y : σ . t₁) ⦂ σ → τ₁✝ }>
      ·posx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:Stringσ:Tyt₁:Tmih:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>Γ:Contextτ₁✝:Tyh:<{ ~(y →ₚ σ ; x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ₁✝ }>hxy:x = y⊢ <{ Γ ⊢ [~x := v] (λ ~y : σ . t₁) ⦂ σ → τ₁✝ }> subst hxyposx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>σ:Tyt₁:Tmih:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>Γ:Contextτ₁✝:Tyh:<{ ~(x →ₚ σ ; x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ₁✝ }>⊢ <{ Γ ⊢ [~x := v] (λ ~x : σ . t₁) ⦂ σ → τ₁✝ }>
        rw [subst_abs_eqposx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>σ:Tyt₁:Tmih:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>Γ:Contextτ₁✝:Tyh:<{ ~(x →ₚ σ ; x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ₁✝ }>⊢ <{ Γ ⊢ λ ~x : σ . t₁ ⦂ σ → τ₁✝ }>]posx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>σ:Tyt₁:Tmih:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>Γ:Contextτ₁✝:Tyh:<{ ~(x →ₚ σ ; x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ₁✝ }>⊢ <{ Γ ⊢ λ ~x : σ . t₁ ⦂ σ → τ₁✝ }>
        rw [PartialMap.update_shadowposx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>σ:Tyt₁:Tmih:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>Γ:Contextτ₁✝:Tyh:<{ ~(x →ₚ σ ; Γ) ⊢ t₁ ⦂ τ₁✝ }>⊢ <{ Γ ⊢ λ ~x : σ . t₁ ⦂ σ → τ₁✝ }>] at hposx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>σ:Tyt₁:Tmih:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>Γ:Contextτ₁✝:Tyh:<{ ~(x →ₚ σ ; Γ) ⊢ t₁ ⦂ τ₁✝ }>⊢ <{ Γ ⊢ λ ~x : σ . t₁ ⦂ σ → τ₁✝ }>
        constructorposx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>σ:Tyt₁:Tmih:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>Γ:Contextτ₁✝:Tyh:<{ ~(x →ₚ σ ; Γ) ⊢ t₁ ⦂ τ₁✝ }>⊢ <{ ~(x →ₚ σ ; Γ) ⊢ t₁ ⦂ τ₁✝ }>
        exact hAll goals completed! 🐙
      ·negx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:Stringσ:Tyt₁:Tmih:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>Γ:Contextτ₁✝:Tyh:<{ ~(y →ₚ σ ; x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ₁✝ }>hxy:¬x = y⊢ <{ Γ ⊢ [~x := v] (λ ~y : σ . t₁) ⦂ σ → τ₁✝ }> rw [subst_abs_ne _ _ _ _ _ hxynegx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:Stringσ:Tyt₁:Tmih:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>Γ:Contextτ₁✝:Tyh:<{ ~(y →ₚ σ ; x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ₁✝ }>hxy:¬x = y⊢ <{ Γ ⊢ λ ~y : σ . [~x := v] t₁ ⦂ σ → τ₁✝ }>]negx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:Stringσ:Tyt₁:Tmih:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>Γ:Contextτ₁✝:Tyh:<{ ~(y →ₚ σ ; x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ₁✝ }>hxy:¬x = y⊢ <{ Γ ⊢ λ ~y : σ . [~x := v] t₁ ⦂ σ → τ₁✝ }>
        rw [PartialMap.update_permute (Ne.symm hxy)negx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:Stringσ:Tyt₁:Tmih:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>Γ:Contextτ₁✝:Tyh:<{ ~(x →ₚ τ' ; y →ₚ σ ; Γ) ⊢ t₁ ⦂ τ₁✝ }>hxy:¬x = y⊢ <{ Γ ⊢ λ ~y : σ . [~x := v] t₁ ⦂ σ → τ₁✝ }>] at hnegx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:Stringσ:Tyt₁:Tmih:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>Γ:Contextτ₁✝:Tyh:<{ ~(x →ₚ τ' ; y →ₚ σ ; Γ) ⊢ t₁ ⦂ τ₁✝ }>hxy:¬x = y⊢ <{ Γ ⊢ λ ~y : σ . [~x := v] t₁ ⦂ σ → τ₁✝ }>
        constructornegx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:Stringσ:Tyt₁:Tmih:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>Γ:Contextτ₁✝:Tyh:<{ ~(x →ₚ τ' ; y →ₚ σ ; Γ) ⊢ t₁ ⦂ τ₁✝ }>hxy:¬x = y⊢ <{ ~(y →ₚ σ ; Γ) ⊢ [~x := v] t₁ ⦂ τ₁✝ }>
        apply ihnegx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>y:Stringσ:Tyt₁:Tmih:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t₁ ⦂ τ }> → <{ Γ ⊢ [~x := v] t₁ ⦂ τ }>Γ:Contextτ₁✝:Tyh:<{ ~(x →ₚ τ' ; y →ₚ σ ; Γ) ⊢ t₁ ⦂ τ₁✝ }>hxy:¬x = y⊢ <{ ~(x →ₚ τ' ; y →ₚ σ ; Γ) ⊢ t₁ ⦂ τ₁✝ }>
        exact hAll goals completed! 🐙
  | tru =>trux:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>Γ:Contextτ:Tyhτ:<{ ~(x →ₚ τ' ; Γ) ⊢ true ⦂ τ }>⊢ <{ Γ ⊢ [~x := v] true ⦂ τ }>
    cases hτ with
    | tru =>tru.trux:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>Γ:Context⊢ <{ Γ ⊢ [~x := v] true ⦂ Bool }>
      rw [subst_trutru.trux:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>Γ:Context⊢ <{ Γ ⊢ true ⦂ Bool }>]tru.trux:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>Γ:Context⊢ <{ Γ ⊢ true ⦂ Bool }>
      constructorAll goals completed! 🐙
  | fls =>flsx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>Γ:Contextτ:Tyhτ:<{ ~(x →ₚ τ' ; Γ) ⊢ false ⦂ τ }>⊢ <{ Γ ⊢ [~x := v] false ⦂ τ }>
    cases hτ with
    | fls =>fls.flsx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>Γ:Context⊢ <{ Γ ⊢ [~x := v] false ⦂ Bool }>
      rw [subst_flsfls.flsx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>Γ:Context⊢ <{ Γ ⊢ false ⦂ Bool }>]fls.flsx:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>Γ:Context⊢ <{ Γ ⊢ false ⦂ Bool }>
      constructorAll goals completed! 🐙
  | ite c t e ihc iht ihe =>itex:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>c:Tmt:Tme:Tmihc:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ τ }> → <{ Γ ⊢ [~x := v] c ⦂ τ }>iht:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }> → <{ Γ ⊢ [~x := v] t ⦂ τ }>ihe:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }> → <{ Γ ⊢ [~x := v] e ⦂ τ }>Γ:Contextτ:Tyhτ:<{ ~(x →ₚ τ' ; Γ) ⊢ if c then t else e ⦂ τ }>⊢ <{ Γ ⊢ [~x := v] (if c then t else e) ⦂ τ }>
    cases hτ with
    | ite _ _ _ _ _ h₁ h₂ h₃ =>ite.itex:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>c:Tmt:Tme:Tmihc:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ τ }> → <{ Γ ⊢ [~x := v] c ⦂ τ }>iht:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }> → <{ Γ ⊢ [~x := v] t ⦂ τ }>ihe:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }> → <{ Γ ⊢ [~x := v] e ⦂ τ }>Γ:Contextτ:Tyh₁:<{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ Bool }>h₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }>h₃:<{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }>⊢ <{ Γ ⊢ [~x := v] (if c then t else e) ⦂ τ }>
      rw [subst_iteite.itex:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>c:Tmt:Tme:Tmihc:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ τ }> → <{ Γ ⊢ [~x := v] c ⦂ τ }>iht:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }> → <{ Γ ⊢ [~x := v] t ⦂ τ }>ihe:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }> → <{ Γ ⊢ [~x := v] e ⦂ τ }>Γ:Contextτ:Tyh₁:<{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ Bool }>h₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }>h₃:<{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }>⊢ <{ Γ ⊢ if [~x := v] c then [~x := v] t else [~x := v] e ⦂ τ }>]ite.itex:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>c:Tmt:Tme:Tmihc:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ τ }> → <{ Γ ⊢ [~x := v] c ⦂ τ }>iht:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }> → <{ Γ ⊢ [~x := v] t ⦂ τ }>ihe:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }> → <{ Γ ⊢ [~x := v] e ⦂ τ }>Γ:Contextτ:Tyh₁:<{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ Bool }>h₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }>h₃:<{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }>⊢ <{ Γ ⊢ if [~x := v] c then [~x := v] t else [~x := v] e ⦂ τ }>
      constructorite.ite.h₁x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>c:Tmt:Tme:Tmihc:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ τ }> → <{ Γ ⊢ [~x := v] c ⦂ τ }>iht:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }> → <{ Γ ⊢ [~x := v] t ⦂ τ }>ihe:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }> → <{ Γ ⊢ [~x := v] e ⦂ τ }>Γ:Contextτ:Tyh₁:<{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ Bool }>h₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }>h₃:<{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }>⊢ <{ Γ ⊢ [~x := v] c ⦂ Bool }>ite.ite.h₂x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>c:Tmt:Tme:Tmihc:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ τ }> → <{ Γ ⊢ [~x := v] c ⦂ τ }>iht:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }> → <{ Γ ⊢ [~x := v] t ⦂ τ }>ihe:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }> → <{ Γ ⊢ [~x := v] e ⦂ τ }>Γ:Contextτ:Tyh₁:<{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ Bool }>h₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }>h₃:<{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }>⊢ <{ Γ ⊢ [~x := v] t ⦂ τ }>ite.ite.h₃x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>c:Tmt:Tme:Tmihc:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ τ }> → <{ Γ ⊢ [~x := v] c ⦂ τ }>iht:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }> → <{ Γ ⊢ [~x := v] t ⦂ τ }>ihe:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }> → <{ Γ ⊢ [~x := v] e ⦂ τ }>Γ:Contextτ:Tyh₁:<{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ Bool }>h₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }>h₃:<{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }>⊢ <{ Γ ⊢ [~x := v] e ⦂ τ }>
      ·ite.ite.h₁x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>c:Tmt:Tme:Tmihc:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ τ }> → <{ Γ ⊢ [~x := v] c ⦂ τ }>iht:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }> → <{ Γ ⊢ [~x := v] t ⦂ τ }>ihe:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }> → <{ Γ ⊢ [~x := v] e ⦂ τ }>Γ:Contextτ:Tyh₁:<{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ Bool }>h₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }>h₃:<{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }>⊢ <{ Γ ⊢ [~x := v] c ⦂ Bool }> apply ihcite.ite.h₁x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>c:Tmt:Tme:Tmihc:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ τ }> → <{ Γ ⊢ [~x := v] c ⦂ τ }>iht:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }> → <{ Γ ⊢ [~x := v] t ⦂ τ }>ihe:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }> → <{ Γ ⊢ [~x := v] e ⦂ τ }>Γ:Contextτ:Tyh₁:<{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ Bool }>h₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }>h₃:<{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }>⊢ <{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ Bool }>
        exact h₁All goals completed! 🐙
      ·ite.ite.h₂x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>c:Tmt:Tme:Tmihc:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ τ }> → <{ Γ ⊢ [~x := v] c ⦂ τ }>iht:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }> → <{ Γ ⊢ [~x := v] t ⦂ τ }>ihe:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }> → <{ Γ ⊢ [~x := v] e ⦂ τ }>Γ:Contextτ:Tyh₁:<{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ Bool }>h₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }>h₃:<{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }>⊢ <{ Γ ⊢ [~x := v] t ⦂ τ }> apply ihtite.ite.h₂x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>c:Tmt:Tme:Tmihc:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ τ }> → <{ Γ ⊢ [~x := v] c ⦂ τ }>iht:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }> → <{ Γ ⊢ [~x := v] t ⦂ τ }>ihe:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }> → <{ Γ ⊢ [~x := v] e ⦂ τ }>Γ:Contextτ:Tyh₁:<{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ Bool }>h₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }>h₃:<{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }>⊢ <{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }>
        exact h₂All goals completed! 🐙
      ·ite.ite.h₃x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>c:Tmt:Tme:Tmihc:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ τ }> → <{ Γ ⊢ [~x := v] c ⦂ τ }>iht:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }> → <{ Γ ⊢ [~x := v] t ⦂ τ }>ihe:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }> → <{ Γ ⊢ [~x := v] e ⦂ τ }>Γ:Contextτ:Tyh₁:<{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ Bool }>h₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }>h₃:<{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }>⊢ <{ Γ ⊢ [~x := v] e ⦂ τ }> apply iheite.ite.h₃x:Stringτ':Tyv:Tmhv:<{ ∅ ⊢ v ⦂ τ' }>c:Tmt:Tme:Tmihc:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ τ }> → <{ Γ ⊢ [~x := v] c ⦂ τ }>iht:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }> → <{ Γ ⊢ [~x := v] t ⦂ τ }>ihe:∀ (Γ : Context) (τ : Ty), <{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }> → <{ Γ ⊢ [~x := v] e ⦂ τ }>Γ:Contextτ:Tyh₁:<{ ~(x →ₚ τ' ; Γ) ⊢ c ⦂ Bool }>h₂:<{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }>h₃:<{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }>⊢ <{ ~(x →ₚ τ' ; Γ) ⊢ e ⦂ τ }>
        exact h₃All goals completed! 🐙

The substitution lemma can be viewed as a kind of "commutation property." Intuitively, it says that substitution and typing can be done in either order: we can either assign types to the terms t and v separately (under suitable contexts) and then combine them using substitution, or we can substitute first and then assign a type to [x:=v] t; the result is the same either way.

Proof: We show, by induction on t, that for all τ and Γ, if x ↦ τ' ; Γ ⊢ t ⦂ τ and ∅ ⊢ v ⦂ τ', then Γ ⊢ [x:=v]t ⦂ τ.

If t is a variable there are two cases to consider, depending on whether t is x or some other variable.
- If t = x, then from the fact that x ↦ τ' ; Γ ⊢ x ⦂ τ we conclude that τ' = τ. We must show that [x:=v]x = v has type τ under Γ, given the assumption that v has type τ' = τ under the empty context. This follows from the weakening lemma.
- If t is some variable y that is not equal to x, then we need only note that y has the same type under x ↦ τ' ; Γ as under Γ.
If t is an abstraction λy:σ. t₀, then τ = σ → τ₁ and the IH tells us, for all Γ' and τ₀, that if x ↦ τ' ; Γ' ⊢ t₀ ⦂ τ₀, then Γ' ⊢ [x:=v]t₀ ⦂ τ₀. Moreover, by inspecting the typing rules we see it must be the case that y ↦ σ ; x ↦ τ' ; Γ ⊢ t₀ ⦂ τ₁.

The substitution in the conclusion behaves differently depending on whether x and y are the same variable.

First, suppose x = y. Then, by the definition of substitution, [x:=v]t = t, so we just need to show Γ ⊢ t ⦂ τ. Using HasType.abs, we need to show that y ↦ σ ; Γ ⊢ t₀ ⦂ τ₁. But we know y ↦ σ ; x ↦ τ' ; Γ ⊢ t₀ ⦂ τ₁, and the claim follows since x = y.

Second, suppose x ≠ y. Again, using HasType.abs, we need to show that y ↦ σ ; Γ ⊢ [x:=v]t₀ ⦂ τ₁. Since x ≠ y, we have y ↦ σ ; x ↦ τ' ; Γ = x ↦ τ' ; y ↦ σ ; Γ. So we have x ↦ τ' ; y ↦ σ ; Γ ⊢ t₀ ⦂ τ₁. Then, the IH applies (taking Γ' = y ↦ σ ; Γ), giving us y ↦ σ ; Γ ⊢ [x:=v]t₀ ⦂ τ₁, as required.
If t is an application t₁ t₂, the result follows straightforwardly from the definition of substitution and the induction hypotheses.
The remaining cases are similar to the application case.

One technical subtlety in the statement of the above lemma is that we assume v has type τ' in the empty context — in other words, we assume v is closed. (Since we are using a simple definition of substitution that is not capture-avoiding, it doesn't make sense to substitute non-closed terms into other terms. Fortunately, closed terms are all we need!)

Exercise★★★(substitution_preserves_typing_from_typing_ind) (Advanced)

Show that substitutionpreservestyping can also be proved by induction on typing derivations instead of induction on terms.

theorem declaration uses `sorry`substitution_preserves_typing_from_typing_ind (Γ : Context) (x : String) (τ' : Ty)
    (t v : Tm) (τ : Ty)
    (hτ : <{ x ↦ τ' ; Γ ⊢ t ⦂ τ }>) (hv : <{ ∅ ⊢ v ⦂ τ' }>) :
    <{ Γ ⊢ [x := v] t ⦂ τ }> := byΓ:Contextx:Stringτ':Tyt:Tmv:Tmτ:Tyhτ:<{ ~(x →ₚ τ' ; Γ) ⊢ t ⦂ τ }>hv:<{ ∅ ⊢ v ⦂ τ' }>⊢ <{ Γ ⊢ [~x := v] t ⦂ τ }>
  sorryAll goals completed! 🐙

6.3.3. Main Theorem🔗

We now have the ingredients we need to prove preservation: if a closed, well-typed term t has type τ and takes a step to t', then t' is also a closed term with type τ. In other words, the small-step reduction relation preserves types.

theorem preservation (t t' : Tm) (τ : Ty)
    (hτ : <{ ∅ ⊢ t ⦂ τ }>) (hs : t ⟶ t') : <{ ∅ ⊢ t' ⦂ τ }> := byt:Tmt':Tmτ:Tyhτ:<{ ∅ ⊢ t ⦂ τ }>hs:t ⟶ t'⊢ <{ ∅ ⊢ t' ⦂ τ }>
  generalize hΓ : (∅ : Context) = Γ at hτt:Tmt':Tmτ:Tyhs:t ⟶ t'Γ:ContexthΓ:∅ = Γhτ:<{ Γ ⊢ t ⦂ τ }>⊢ <{ Γ ⊢ t' ⦂ τ }>
  induction hτ generalizing t' with
  | var =>vart:Tmτ:TyΓ:ContextΓ✝:Contextx✝:Stringτ₁✝:Tyh✝:Γ✝[x✝] = some τ₁✝t':Tmhs:Stlc.Tm.var x✝ ⟶ t'hΓ:∅ = Γ✝⊢ <{ Γ✝ ⊢ t' ⦂ τ₁✝ }> cases hsAll goals completed! 🐙
  | abs =>abst:Tmτ:TyΓ:ContextΓ✝:Contextx✝:Stringτ₁✝:Tyτ₂✝:Tyt₁✝:Tmh✝:<{ ~(x✝ →ₚ τ₂✝ ; Γ✝) ⊢ t₁✝ ⦂ τ₁✝ }>h_ih✝:∀ (t' : Tm), t₁✝ ⟶ t' → ∅ = x✝ →ₚ τ₂✝ ; Γ✝ → <{ ~(x✝ →ₚ τ₂✝ ; Γ✝) ⊢ t' ⦂ τ₁✝ }>t':Tmhs:<{ λ ~x✝ : τ₂✝ . t₁✝ }> ⟶ t'hΓ:∅ = Γ✝⊢ <{ Γ✝ ⊢ t' ⦂ τ₂✝ → τ₁✝ }> cases hsAll goals completed! 🐙
  | tru =>trut:Tmτ:TyΓ:ContextΓ✝:Contextt':Tmhs:<{ true }> ⟶ t'hΓ:∅ = Γ✝⊢ <{ Γ✝ ⊢ t' ⦂ Bool }> cases hsAll goals completed! 🐙
  | fls =>flst:Tmτ:TyΓ:ContextΓ✝:Contextt':Tmhs:<{ false }> ⟶ t'hΓ:∅ = Γ✝⊢ <{ Γ✝ ⊢ t' ⦂ Bool }> cases hsAll goals completed! 🐙
  | app Γ τ₁ τ₂ t₁ t₂ h₁ h₂ ih₁ ih₂ =>appt:Tmτ:TyΓ✝:ContextΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ Γ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ Γ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = Γ → <{ Γ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = Γ → <{ Γ ⊢ t' ⦂ τ₂ }>t':Tmhs:<{ t₁ t₂ }> ⟶ t'hΓ:∅ = Γ⊢ <{ Γ ⊢ t' ⦂ τ₁ }>
    subst hΓappt:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmt':Tmhs:<{ t₁ t₂ }> ⟶ t'h₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>⊢ <{ ∅ ⊢ t' ⦂ τ₁ }>
    cases hs with
    | appAbs _ _ _ _ _ =>app.appAbst:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₂:Tmh₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>x✝:Stringτ✝:Tyt✝:Tmh₁:<{ ∅ ⊢ λ ~x✝ : τ✝ . t✝ ⦂ τ₂ → τ₁ }>ih₁:∀ (t' : Tm), <{ λ ~x✝ : τ✝ . t✝ }> ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>hv✝:t₂.IsValue⊢ <{ ∅ ⊢ [~x✝ := t₂] t✝ ⦂ τ₁ }>
      -- The one interesting case: the desired result is the substitution lemma.
      cases h₁ with
      | abs _ _ _ _ _ hb =>app.appAbs.abst:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₂:Tmh₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>x✝:Stringt✝:Tmhv✝:t₂.IsValueih₁:∀ (t' : Tm), <{ λ ~x✝ : τ₂ . t✝ }> ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>hb:<{ ~(x✝ →ₚ τ₂) ⊢ t✝ ⦂ τ₁ }>⊢ <{ ∅ ⊢ [~x✝ := t₂] t✝ ⦂ τ₁ }>
        apply substitution_preserves_typingapp.appAbs.abs.hτt:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₂:Tmh₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>x✝:Stringt✝:Tmhv✝:t₂.IsValueih₁:∀ (t' : Tm), <{ λ ~x✝ : τ₂ . t✝ }> ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>hb:<{ ~(x✝ →ₚ τ₂) ⊢ t✝ ⦂ τ₁ }>⊢ <{ ~(x✝ →ₚ ?app.appAbs.abs.τ') ⊢ t✝ ⦂ τ₁ }>app.appAbs.abs.hvt:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₂:Tmh₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>x✝:Stringt✝:Tmhv✝:t₂.IsValueih₁:∀ (t' : Tm), <{ λ ~x✝ : τ₂ . t✝ }> ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>hb:<{ ~(x✝ →ₚ τ₂) ⊢ t✝ ⦂ τ₁ }>⊢ <{ ∅ ⊢ t₂ ⦂ ~?app.appAbs.abs.τ' }>app.appAbs.abs.τ't:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₂:Tmh₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>x✝:Stringt✝:Tmhv✝:t₂.IsValueih₁:∀ (t' : Tm), <{ λ ~x✝ : τ₂ . t✝ }> ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>hb:<{ ~(x✝ →ₚ τ₂) ⊢ t✝ ⦂ τ₁ }>⊢ Ty
        ·app.appAbs.abs.hτt:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₂:Tmh₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>x✝:Stringt✝:Tmhv✝:t₂.IsValueih₁:∀ (t' : Tm), <{ λ ~x✝ : τ₂ . t✝ }> ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>hb:<{ ~(x✝ →ₚ τ₂) ⊢ t✝ ⦂ τ₁ }>⊢ <{ ~(x✝ →ₚ ?app.appAbs.abs.τ') ⊢ t✝ ⦂ τ₁ }> exact hbAll goals completed! 🐙
        ·app.appAbs.abs.hvt:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₂:Tmh₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>x✝:Stringt✝:Tmhv✝:t₂.IsValueih₁:∀ (t' : Tm), <{ λ ~x✝ : τ₂ . t✝ }> ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>hb:<{ ~(x✝ →ₚ τ₂) ⊢ t✝ ⦂ τ₁ }>⊢ <{ ∅ ⊢ t₂ ⦂ τ₂ }> exact h₂All goals completed! 🐙
    | app1 _ t₁' _ h =>app.app1t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>t₁':Tmh:t₁ ⟶ t₁'⊢ <{ ∅ ⊢ t₁' t₂ ⦂ τ₁ }>
      constructorapp.app1.h₁t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>t₁':Tmh:t₁ ⟶ t₁'⊢ <{ ∅ ⊢ t₁' ⦂ ~?app.app1.τ₂ → τ₁ }>app.app1.h₂t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>t₁':Tmh:t₁ ⟶ t₁'⊢ <{ ∅ ⊢ t₂ ⦂ ~?app.app1.τ₂ }>app.app1.τ₂t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>t₁':Tmh:t₁ ⟶ t₁'⊢ Ty
      ·app.app1.h₁t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>t₁':Tmh:t₁ ⟶ t₁'⊢ <{ ∅ ⊢ t₁' ⦂ ~?app.app1.τ₂ → τ₁ }> apply ih₁app.app1.h₁.hst:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>t₁':Tmh:t₁ ⟶ t₁'⊢ t₁ ⟶ t₁'app.app1.h₁.hΓt:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>t₁':Tmh:t₁ ⟶ t₁'⊢ ∅ = ∅
        ·app.app1.h₁.hst:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>t₁':Tmh:t₁ ⟶ t₁'⊢ t₁ ⟶ t₁' exact hAll goals completed! 🐙
        ·app.app1.h₁.hΓt:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>t₁':Tmh:t₁ ⟶ t₁'⊢ ∅ = ∅ rflAll goals completed! 🐙
      ·app.app1.h₂t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>t₁':Tmh:t₁ ⟶ t₁'⊢ <{ ∅ ⊢ t₂ ⦂ τ₂ }> exact h₂All goals completed! 🐙
    | app2 _ _ t₂' _ h =>app.app2t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>t₂':Tmhv✝:t₁.IsValueh:t₂ ⟶ t₂'⊢ <{ ∅ ⊢ t₁ t₂' ⦂ τ₁ }>
      constructorapp.app2.h₁t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>t₂':Tmhv✝:t₁.IsValueh:t₂ ⟶ t₂'⊢ <{ ∅ ⊢ t₁ ⦂ ~?app.app2.τ₂ → τ₁ }>app.app2.h₂t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>t₂':Tmhv✝:t₁.IsValueh:t₂ ⟶ t₂'⊢ <{ ∅ ⊢ t₂' ⦂ ~?app.app2.τ₂ }>app.app2.τ₂t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>t₂':Tmhv✝:t₁.IsValueh:t₂ ⟶ t₂'⊢ Ty
      ·app.app2.h₁t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>t₂':Tmhv✝:t₁.IsValueh:t₂ ⟶ t₂'⊢ <{ ∅ ⊢ t₁ ⦂ ~?app.app2.τ₂ → τ₁ }> exact h₁All goals completed! 🐙
      ·app.app2.h₂t:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>t₂':Tmhv✝:t₁.IsValueh:t₂ ⟶ t₂'⊢ <{ ∅ ⊢ t₂' ⦂ τ₂ }> apply ih₂app.app2.h₂.hst:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>t₂':Tmhv✝:t₁.IsValueh:t₂ ⟶ t₂'⊢ t₂ ⟶ t₂'app.app2.h₂.hΓt:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>t₂':Tmhv✝:t₁.IsValueh:t₂ ⟶ t₂'⊢ ∅ = ∅
        ·app.app2.h₂.hst:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>t₂':Tmhv✝:t₁.IsValueh:t₂ ⟶ t₂'⊢ t₂ ⟶ t₂' exact hAll goals completed! 🐙
        ·app.app2.h₂.hΓt:Tmτ:TyΓ:Contextτ₁:Tyτ₂:Tyt₁:Tmt₂:Tmh₁:<{ ∅ ⊢ t₁ ⦂ τ₂ → τ₁ }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₂ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ → τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₂ }>t₂':Tmhv✝:t₁.IsValueh:t₂ ⟶ t₂'⊢ ∅ = ∅ rflAll goals completed! 🐙
  | ite Γ t₁ t₂ t₃ τ₁ h₁ h₂ h₃ ih₁ ih₂ ih₃ =>itet:Tmτ:TyΓ✝:ContextΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ Γ ⊢ t₁ ⦂ Bool }>h₂:<{ Γ ⊢ t₂ ⦂ τ₁ }>h₃:<{ Γ ⊢ t₃ ⦂ τ₁ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = Γ → <{ Γ ⊢ t' ⦂ Bool }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = Γ → <{ Γ ⊢ t' ⦂ τ₁ }>ih₃:∀ (t' : Tm), t₃ ⟶ t' → ∅ = Γ → <{ Γ ⊢ t' ⦂ τ₁ }>t':Tmhs:<{ if t₁ then t₂ else t₃ }> ⟶ t'hΓ:∅ = Γ⊢ <{ Γ ⊢ t' ⦂ τ₁ }>
    subst hΓitet:Tmτ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyt':Tmhs:<{ if t₁ then t₂ else t₃ }> ⟶ t'h₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ Bool }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>ih₃:∀ (t' : Tm), t₃ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>⊢ <{ ∅ ⊢ t' ⦂ τ₁ }>
    cases hs with
    | ifTrue =>ite.ifTruet:Tmτ:TyΓ:Contextt₂:Tmt₃:Tmτ₁:Tyh₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>ih₃:∀ (t' : Tm), t₃ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>h₁:<{ ∅ ⊢ true ⦂ Bool }>ih₁:∀ (t' : Tm), <{ true }> ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ Bool }>⊢ <{ ∅ ⊢ t₂ ⦂ τ₁ }> exact h₂All goals completed! 🐙
    | ifFalse =>ite.ifFalset:Tmτ:TyΓ:Contextt₂:Tmt₃:Tmτ₁:Tyh₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>ih₃:∀ (t' : Tm), t₃ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>h₁:<{ ∅ ⊢ false ⦂ Bool }>ih₁:∀ (t' : Tm), <{ false }> ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ Bool }>⊢ <{ ∅ ⊢ t₃ ⦂ τ₁ }> exact h₃All goals completed! 🐙
    | ifStep _ t₁' _ _ h =>ite.ifStept:Tmτ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ Bool }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>ih₃:∀ (t' : Tm), t₃ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>t₁':Tmh:t₁ ⟶ t₁'⊢ <{ ∅ ⊢ if t₁' then t₂ else t₃ ⦂ τ₁ }>
      constructorite.ifStep.h₁t:Tmτ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ Bool }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>ih₃:∀ (t' : Tm), t₃ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>t₁':Tmh:t₁ ⟶ t₁'⊢ <{ ∅ ⊢ t₁' ⦂ Bool }>ite.ifStep.h₂t:Tmτ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ Bool }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>ih₃:∀ (t' : Tm), t₃ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>t₁':Tmh:t₁ ⟶ t₁'⊢ <{ ∅ ⊢ t₂ ⦂ τ₁ }>ite.ifStep.h₃t:Tmτ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ Bool }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>ih₃:∀ (t' : Tm), t₃ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>t₁':Tmh:t₁ ⟶ t₁'⊢ <{ ∅ ⊢ t₃ ⦂ τ₁ }>
      ·ite.ifStep.h₁t:Tmτ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ Bool }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>ih₃:∀ (t' : Tm), t₃ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>t₁':Tmh:t₁ ⟶ t₁'⊢ <{ ∅ ⊢ t₁' ⦂ Bool }> apply ih₁ite.ifStep.h₁.hst:Tmτ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ Bool }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>ih₃:∀ (t' : Tm), t₃ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>t₁':Tmh:t₁ ⟶ t₁'⊢ t₁ ⟶ t₁'ite.ifStep.h₁.hΓt:Tmτ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ Bool }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>ih₃:∀ (t' : Tm), t₃ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>t₁':Tmh:t₁ ⟶ t₁'⊢ ∅ = ∅
        ·ite.ifStep.h₁.hst:Tmτ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ Bool }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>ih₃:∀ (t' : Tm), t₃ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>t₁':Tmh:t₁ ⟶ t₁'⊢ t₁ ⟶ t₁' exact hAll goals completed! 🐙
        ·ite.ifStep.h₁.hΓt:Tmτ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ Bool }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>ih₃:∀ (t' : Tm), t₃ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>t₁':Tmh:t₁ ⟶ t₁'⊢ ∅ = ∅ rflAll goals completed! 🐙
      ·ite.ifStep.h₂t:Tmτ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ Bool }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>ih₃:∀ (t' : Tm), t₃ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>t₁':Tmh:t₁ ⟶ t₁'⊢ <{ ∅ ⊢ t₂ ⦂ τ₁ }> exact h₂All goals completed! 🐙
      ·ite.ifStep.h₃t:Tmτ:TyΓ:Contextt₁:Tmt₂:Tmt₃:Tmτ₁:Tyh₁:<{ ∅ ⊢ t₁ ⦂ Bool }>h₂:<{ ∅ ⊢ t₂ ⦂ τ₁ }>h₃:<{ ∅ ⊢ t₃ ⦂ τ₁ }>ih₁:∀ (t' : Tm), t₁ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ Bool }>ih₂:∀ (t' : Tm), t₂ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>ih₃:∀ (t' : Tm), t₃ ⟶ t' → ∅ = ∅ → <{ ∅ ⊢ t' ⦂ τ₁ }>t₁':Tmh:t₁ ⟶ t₁'⊢ <{ ∅ ⊢ t₃ ⦂ τ₁ }> exact h₃All goals completed! 🐙

Proof: By induction on the derivation of ∅ ⊢ t ⦂ τ.

We can immediately rule out HasType.var, HasType.abs, HasType.tru, and HasType.fls as final rules in the derivation, since in each of these cases t cannot take a step.
If the last rule in the derivation is HasType.app, then t = t₁ t₂, and there are subderivations showing that ∅ ⊢ t₁ ⦂ τ₂ → τ and ∅ ⊢ t₂ ⦂ τ₂ plus two induction hypotheses: (1) t₁ ⟶ t₁' implies ∅ ⊢ t₁' ⦂ τ₂ → τ and (2) t₂ ⟶ t₂' implies ∅ ⊢ t₂' ⦂ τ₂. There are now three subcases to consider, one for each rule that could be used to show that t₁ t₂ takes a step to t'.
- If t₁ t₂ takes a step by Step.app1, with t₁ stepping to t₁', then, by the first IH, t₁' has the same type as t₁ (∅ ⊢ t₁' ⦂ τ₂ → τ), and hence by HasType.app t₁' t₂ has type τ.
- The Step.app2 case is similar, using the second IH.
- If t₁ t₂ takes a step by Step.appAbs, then t₁ = λx:τ₀. t₀ and t₁ t₂ steps to [x:=t₂]t₀; the desired result now follows from the substitution lemma.
If the last rule in the derivation is HasType.ite, then t = if t₁ then t₂ else t₃, with ∅ ⊢ t₁ ⦂ Bool, ∅ ⊢ t₂ ⦂ τ₁, and ∅ ⊢ t₃ ⦂ τ₁, and with three induction hypotheses: (1) t₁ ⟶ t₁' implies ∅ ⊢ t₁' ⦂ Bool, (2) t₂ ⟶ t₂' implies ∅ ⊢ t₂' ⦂ τ₁, and (3) t₃ ⟶ t₃' implies ∅ ⊢ t₃' ⦂ τ₁.

There are again three subcases to consider, depending on how t steps.
- If t steps to t₂ or t₃ by Step.ifTrue or Step.ifFalse, the result is immediate, since t₂ and t₃ have the same type as t.
- Otherwise, t steps by Step.ifStep, and the desired conclusion follows directly from the first induction hypothesis.

Exercise★★(subject_expansion_stlc) (Manually graded)

An exercise in the Types chapter asked about the subject expansion property for the simple language of arithmetic and boolean expressions. This property did not hold for that language, and it also fails for STLC. That is, it is not always the case that, if t ⟶ t' and ∅ ⊢ t' ⦂ τ, then ∅ ⊢ t ⦂ τ. Show this by giving a counter-example that does not involve conditionals.

theorem declaration uses `sorry`not_subject_expansion :
    ∃ (t t' : Tm) (τ : Ty), t ⟶ t' ∧ <{ ∅ ⊢ t' ⦂ τ }> ∧ ¬ <{ ∅ ⊢ t ⦂ τ }> := by⊢ ∃ t t' τ, t ⟶ t' ∧ <{ ∅ ⊢ t' ⦂ τ }> ∧ ¬<{ ∅ ⊢ t ⦂ τ }>
    -- Hint: for giving counterexamples in STLC, give each witness
    -- with `exists <{ … }>`.  This works for both terms and types, as
    -- in `<{true}>` and `<{ Bool }>`.
    sorryAll goals completed! 🐙

Alternative formulation.

6.4. Type Soundness🔗

Exercise★★(type_soundness) (Optional)

Put progress and preservation together and show that a well-typed term can never reach a stuck state.

def Tm.IsStuck (t : Tm) : Prop := IsNormalForm Step t ∧ ¬ t.IsValue

theorem declaration uses `sorry`type_soundness (t t' : Tm) (τ : Ty)
    (hτ : <{ ∅ ⊢ t ⦂ τ }>) (hm : t ⟶* t') : ¬ t'.IsStuck := byt:Tmt':Tmτ:Tyhτ:<{ ∅ ⊢ t ⦂ τ }>hm:t ⟶* t'⊢ ¬t'.IsStuck
  intro hstt:Tmt':Tmτ:Tyhτ:<{ ∅ ⊢ t ⦂ τ }>hm:t ⟶* t'hst:t'.IsStuck⊢ False
  obtain ⟨hnf, hnv⟩ := hstt:Tmt':Tmτ:Tyhτ:<{ ∅ ⊢ t ⦂ τ }>hm:t ⟶* t'hnf:IsNormalForm Step t'hnv:¬t'.IsValue⊢ False
  induction hm with
  | refl u =>reflt:Tmt':Tmτ:Tyu:Tmhτ:<{ ∅ ⊢ u ⦂ τ }>hnf:IsNormalForm Step uhnv:¬u.IsValue⊢ False
    sorryAll goals completed! 🐙
  | step u w z h₁ _ ih =>stept:Tmt':Tmτ:Tyu:Tmw:Tmz:Tmh₁:u ⟶ wh₂✝:w ⟶* zih:<{ ∅ ⊢ w ⦂ τ }> → IsNormalForm Step z → ¬z.IsValue → Falsehτ:<{ ∅ ⊢ u ⦂ τ }>hnf:IsNormalForm Step zhnv:¬z.IsValue⊢ False
    sorryAll goals completed! 🐙

6.5. Uniqueness of Types🔗

Exercise★★★(unique_types)

Another nice property of the STLC is that types are unique: a given term (in a given context) has at most one type.

theorem declaration uses `sorry`unique_types (Γ : Context) (e : Tm) (τ τ' : Ty)
    (h : <{ Γ ⊢ e ⦂ τ }>) (h' : <{ Γ ⊢ e ⦂ τ' }>) : τ = τ' := byΓ:Contexte:Tmτ:Tyτ':Tyh:<{ Γ ⊢ e ⦂ τ }>h':<{ Γ ⊢ e ⦂ τ' }>⊢ τ = τ'
  sorryAll goals completed! 🐙

6.6. Context Invariance (Optional)🔗

Another standard technical lemma associated with typed languages is context invariance. It states that typing is preserved under "inessential changes" to the context Γ — in particular, changes that do not affect any of the free variables of the term. In this section, we establish this property for our system, introducing some other standard terminology on the way.

First, we need to define the free variables in a term — i.e., variables that are used in the term in positions that are not in the scope of an enclosing function abstraction binding a variable of the same name.

More technically, a variable X appears free in a term t if t contains some occurrence of X that is not under an abstraction labeled X. For example:

Y appears free, but X does not, in λX:τ → τ'. X Y
both X and Y appear free in (λX:τ → τ'. X Y) X
no variables appear free in λX:τ → τ'. λY:τ. X Y

We write this schematically as x ∈ᶠ t, reading the relation as "x is one of the free variables of t". Formally:

section
set_option hygiene false in
local infix:50 " ∈ᶠ " => AppearsFreeIn

inductive AppearsFreeIn (x : String) : Tm → Prop where
  | var : x ∈ᶠ (Tm.var x)
  | app1 (t₁ t₂ : Tm) (h : x ∈ᶠ t₁) : x ∈ᶠ <{ t₁ t₂ }>
  | app2 (t₁ t₂ : Tm) (h : x ∈ᶠ t₂) : x ∈ᶠ <{ t₁ t₂ }>
  | abs (y : String) (τ₁ : Ty) (t₁ : Tm) (hne : y ≠ x) (h : x ∈ᶠ t₁) :
      x ∈ᶠ <{ λ y : τ₁ . t₁ }>
  | ite1 (t₁ t₂ t₃ : Tm) (h : x ∈ᶠ t₁) : x ∈ᶠ <{ if t₁ then t₂ else t₃ }>
  | ite2 (t₁ t₂ t₃ : Tm) (h : x ∈ᶠ t₂) : x ∈ᶠ <{ if t₁ then t₂ else t₃ }>
  | ite3 (t₁ t₂ t₃ : Tm) (h : x ∈ᶠ t₃) : x ∈ᶠ <{ if t₁ then t₂ else t₃ }>
end

scoped infix:50 " ∈ᶠ " => AppearsFreeIn

The free variables of a term are just the variables that appear free in it. This gives us another way to define closed terms — arguably a better one, since it applies even to ill-typed terms. Indeed, this is the standard definition of the term "closed."

def Tm.Closed (t : Tm) : Prop := ∀ x, ¬ x ∈ᶠ t

Conversely, an open term is one that may contain free variables. (I.e., every term is an open term; the closed terms are a subset of the open ones. "Open" precisely means "possibly containing free variables.")

Exercise★(afi) (Optional, Manually graded)

(Officially optional, but strongly recommended!) In the space below, write out the rules of the ∈ᶠ relation in informal inference-rule notation. (Use whatever notational conventions you like — the point of the exercise is just for you to think a bit about the meaning of each rule.) Although this is a rather low-level, technical definition, understanding it is crucial to understanding substitution and its properties, which are really the crux of the lambda-calculus.

Next, we show that if a variable x appears free in a term t, and if we know t is well typed in context Γ, then it must be the case that Γ assigns a type to x.

Proof: We show, by induction on the proof that x appears free in t, that, for all contexts Γ, if t is well typed under Γ, then Γ assigns some type to x.

If the last rule used is AppearsFreeIn.var, then t = x, and from the assumption that t is well typed under Γ we have immediately that Γ assigns a type to x.
If the last rule used is AppearsFreeIn.app1, then t = t₁ t₂ and x appears free in t₁. Since t is well typed under Γ, we can see from the typing rules that t₁ must also be, and the IH then tells us that Γ assigns x a type.
Almost all the other cases are similar: x appears free in a subterm of t, and since t is well typed under Γ, we know the subterm of t in which x appears is well typed under Γ as well, and the IH gives us exactly the conclusion we want.
The only remaining case is AppearsFreeIn.abs. In this case t = λy:τ₁. t₁ and x appears free in t₁, and we also know that x is different from y. The difference from the previous cases is that, whereas t is well typed under Γ, its body t₁ is well typed under y ↦ τ₁ ; Γ, so the IH allows us to conclude that x is assigned some type by the extended context y ↦ τ₁ ; Γ. To conclude that Γ assigns a type to x, we appeal to lemma PartialMap.update_neq, noting that x and y are different variables.

Exercise★★(free_in_context)

Complete the following proof.

theorem declaration uses `sorry`free_in_context (x : String) (t : Tm) (τ : Ty) (Γ : Context)
    (ha : x ∈ᶠ t) (hτ : <{ Γ ⊢ t ⦂ τ }>) : ∃ τ', Γ[x] = some τ' := byx:Stringt:Tmτ:TyΓ:Contextha:x ∈ᶠ thτ:<{ Γ ⊢ t ⦂ τ }>⊢ ∃ τ', Γ[x] = some τ'
  induction ha generalizing Γ τ with
  | var =>varx:Stringt:Tmτ:TyΓ:Contexthτ:<{ Γ ⊢ ~(Stlc.Tm.var x) ⦂ τ }>⊢ ∃ τ', Γ[x] = some τ'
    cases hτ with
    | var _ _ _ h =>var.varx:Stringt:Tmτ:TyΓ:Contexth:Γ[x] = some τ⊢ ∃ τ', Γ[x] = some τ'
      constructorvar.var.hx:Stringt:Tmτ:TyΓ:Contexth:Γ[x] = some τ⊢ Γ[x] = some ?var.var.wvar.var.wx:Stringt:Tmτ:TyΓ:Contexth:Γ[x] = some τ⊢ Ty
      exact hAll goals completed! 🐙
  | app1 _ _ _ ih =>app1x:Stringt:Tmt₁✝:Tmt₂✝:Tmh✝:x ∈ᶠ t₁✝ih:∀ (τ : Ty) (Γ : Context), <{ Γ ⊢ t₁✝ ⦂ τ }> → ∃ τ', Γ[x] = some τ'τ:TyΓ:Contexthτ:<{ Γ ⊢ t₁✝ t₂✝ ⦂ τ }>⊢ ∃ τ', Γ[x] = some τ'
    cases hτ with
    | app _ _ _ _ _ h₁ _ =>app1.appx:Stringt:Tmt₁✝:Tmt₂✝:Tmh✝:x ∈ᶠ t₁✝ih:∀ (τ : Ty) (Γ : Context), <{ Γ ⊢ t₁✝ ⦂ τ }> → ∃ τ', Γ[x] = some τ'τ:TyΓ:Contextτ₂✝:Tyh₂✝:<{ Γ ⊢ t₂✝ ⦂ τ₂✝ }>h₁:<{ Γ ⊢ t₁✝ ⦂ τ₂✝ → τ }>⊢ ∃ τ', Γ[x] = some τ'
      apply ihapp1.app.hτx:Stringt:Tmt₁✝:Tmt₂✝:Tmh✝:x ∈ᶠ t₁✝ih:∀ (τ : Ty) (Γ : Context), <{ Γ ⊢ t₁✝ ⦂ τ }> → ∃ τ', Γ[x] = some τ'τ:TyΓ:Contextτ₂✝:Tyh₂✝:<{ Γ ⊢ t₂✝ ⦂ τ₂✝ }>h₁:<{ Γ ⊢ t₁✝ ⦂ τ₂✝ → τ }>⊢ <{ Γ ⊢ t₁✝ ⦂ ~?app1.app.τ }>app1.app.τx:Stringt:Tmt₁✝:Tmt₂✝:Tmh✝:x ∈ᶠ t₁✝ih:∀ (τ : Ty) (Γ : Context), <{ Γ ⊢ t₁✝ ⦂ τ }> → ∃ τ', Γ[x] = some τ'τ:TyΓ:Contextτ₂✝:Tyh₂✝:<{ Γ ⊢ t₂✝ ⦂ τ₂✝ }>h₁:<{ Γ ⊢ t₁✝ ⦂ τ₂✝ → τ }>⊢ Ty
      exact h₁All goals completed! 🐙
  | app2 _ _ _ ih =>app2x:Stringt:Tmt₁✝:Tmt₂✝:Tmh✝:x ∈ᶠ t₂✝ih:∀ (τ : Ty) (Γ : Context), <{ Γ ⊢ t₂✝ ⦂ τ }> → ∃ τ', Γ[x] = some τ'τ:TyΓ:Contexthτ:<{ Γ ⊢ t₁✝ t₂✝ ⦂ τ }>⊢ ∃ τ', Γ[x] = some τ'
    cases hτ with
    | app _ _ _ _ _ _ h₂ =>app2.appx:Stringt:Tmt₁✝:Tmt₂✝:Tmh✝:x ∈ᶠ t₂✝ih:∀ (τ : Ty) (Γ : Context), <{ Γ ⊢ t₂✝ ⦂ τ }> → ∃ τ', Γ[x] = some τ'τ:TyΓ:Contextτ₂✝:Tyh₂:<{ Γ ⊢ t₂✝ ⦂ τ₂✝ }>h₁✝:<{ Γ ⊢ t₁✝ ⦂ τ₂✝ → τ }>⊢ ∃ τ', Γ[x] = some τ'
      apply ihapp2.app.hτx:Stringt:Tmt₁✝:Tmt₂✝:Tmh✝:x ∈ᶠ t₂✝ih:∀ (τ : Ty) (Γ : Context), <{ Γ ⊢ t₂✝ ⦂ τ }> → ∃ τ', Γ[x] = some τ'τ:TyΓ:Contextτ₂✝:Tyh₂:<{ Γ ⊢ t₂✝ ⦂ τ₂✝ }>h₁✝:<{ Γ ⊢ t₁✝ ⦂ τ₂✝ → τ }>⊢ <{ Γ ⊢ t₂✝ ⦂ ~?app2.app.τ }>app2.app.τx:Stringt:Tmt₁✝:Tmt₂✝:Tmh✝:x ∈ᶠ t₂✝ih:∀ (τ : Ty) (Γ : Context), <{ Γ ⊢ t₂✝ ⦂ τ }> → ∃ τ', Γ[x] = some τ'τ:TyΓ:Contextτ₂✝:Tyh₂:<{ Γ ⊢ t₂✝ ⦂ τ₂✝ }>h₁✝:<{ Γ ⊢ t₁✝ ⦂ τ₂✝ → τ }>⊢ Ty
      exact h₂All goals completed! 🐙
  | abs y _ _ hne _ ih =>absx:Stringt:Tmy:Stringτ₁✝:Tyt₁✝:Tmhne:y ≠ xh✝:x ∈ᶠ t₁✝ih:∀ (τ : Ty) (Γ : Context), <{ Γ ⊢ t₁✝ ⦂ τ }> → ∃ τ', Γ[x] = some τ'τ:TyΓ:Contexthτ:<{ Γ ⊢ λ ~y : τ₁✝ . t₁✝ ⦂ τ }>⊢ ∃ τ', Γ[x] = some τ'
    sorryAll goals completed! 🐙
  | ite1 _ _ _ _ ih =>ite1x:Stringt:Tmt₁✝:Tmt₂✝:Tmt₃✝:Tmh✝:x ∈ᶠ t₁✝ih:∀ (τ : Ty) (Γ : Context), <{ Γ ⊢ t₁✝ ⦂ τ }> → ∃ τ', Γ[x] = some τ'τ:TyΓ:Contexthτ:<{ Γ ⊢ if t₁✝ then t₂✝ else t₃✝ ⦂ τ }>⊢ ∃ τ', Γ[x] = some τ'
    cases hτ with
    | ite _ _ _ _ _ h₁ _ _ =>ite1.itex:Stringt:Tmt₁✝:Tmt₂✝:Tmt₃✝:Tmh✝:x ∈ᶠ t₁✝ih:∀ (τ : Ty) (Γ : Context), <{ Γ ⊢ t₁✝ ⦂ τ }> → ∃ τ', Γ[x] = some τ'τ:TyΓ:Contexth₁:<{ Γ ⊢ t₁✝ ⦂ Bool }>h₂✝:<{ Γ ⊢ t₂✝ ⦂ τ }>h₃✝:<{ Γ ⊢ t₃✝ ⦂ τ }>⊢ ∃ τ', Γ[x] = some τ'
      apply ihite1.ite.hτx:Stringt:Tmt₁✝:Tmt₂✝:Tmt₃✝:Tmh✝:x ∈ᶠ t₁✝ih:∀ (τ : Ty) (Γ : Context), <{ Γ ⊢ t₁✝ ⦂ τ }> → ∃ τ', Γ[x] = some τ'τ:TyΓ:Contexth₁:<{ Γ ⊢ t₁✝ ⦂ Bool }>h₂✝:<{ Γ ⊢ t₂✝ ⦂ τ }>h₃✝:<{ Γ ⊢ t₃✝ ⦂ τ }>⊢ <{ Γ ⊢ t₁✝ ⦂ ~?ite1.ite.τ }>ite1.ite.τx:Stringt:Tmt₁✝:Tmt₂✝:Tmt₃✝:Tmh✝:x ∈ᶠ t₁✝ih:∀ (τ : Ty) (Γ : Context), <{ Γ ⊢ t₁✝ ⦂ τ }> → ∃ τ', Γ[x] = some τ'τ:TyΓ:Contexth₁:<{ Γ ⊢ t₁✝ ⦂ Bool }>h₂✝:<{ Γ ⊢ t₂✝ ⦂ τ }>h₃✝:<{ Γ ⊢ t₃✝ ⦂ τ }>⊢ Ty
      exact h₁All goals completed! 🐙
  | ite2 _ _ _ _ ih =>ite2x:Stringt:Tmt₁✝:Tmt₂✝:Tmt₃✝:Tmh✝:x ∈ᶠ t₂✝ih:∀ (τ : Ty) (Γ : Context), <{ Γ ⊢ t₂✝ ⦂ τ }> → ∃ τ', Γ[x] = some τ'τ:TyΓ:Contexthτ:<{ Γ ⊢ if t₁✝ then t₂✝ else t₃✝ ⦂ τ }>⊢ ∃ τ', Γ[x] = some τ'
    cases hτ with
    | ite _ _ _ _ _ _ h₂ _ =>ite2.itex:Stringt:Tmt₁✝:Tmt₂✝:Tmt₃✝:Tmh✝:x ∈ᶠ t₂✝ih:∀ (τ : Ty) (Γ : Context), <{ Γ ⊢ t₂✝ ⦂ τ }> → ∃ τ', Γ[x] = some τ'τ:TyΓ:Contexth₁✝:<{ Γ ⊢ t₁✝ ⦂ Bool }>h₂:<{ Γ ⊢ t₂✝ ⦂ τ }>h₃✝:<{ Γ ⊢ t₃✝ ⦂ τ }>⊢ ∃ τ', Γ[x] = some τ'
      apply ihite2.ite.hτx:Stringt:Tmt₁✝:Tmt₂✝:Tmt₃✝:Tmh✝:x ∈ᶠ t₂✝ih:∀ (τ : Ty) (Γ : Context), <{ Γ ⊢ t₂✝ ⦂ τ }> → ∃ τ', Γ[x] = some τ'τ:TyΓ:Contexth₁✝:<{ Γ ⊢ t₁✝ ⦂ Bool }>h₂:<{ Γ ⊢ t₂✝ ⦂ τ }>h₃✝:<{ Γ ⊢ t₃✝ ⦂ τ }>⊢ <{ Γ ⊢ t₂✝ ⦂ ~?ite2.ite.τ }>ite2.ite.τx:Stringt:Tmt₁✝:Tmt₂✝:Tmt₃✝:Tmh✝:x ∈ᶠ t₂✝ih:∀ (τ : Ty) (Γ : Context), <{ Γ ⊢ t₂✝ ⦂ τ }> → ∃ τ', Γ[x] = some τ'τ:TyΓ:Contexth₁✝:<{ Γ ⊢ t₁✝ ⦂ Bool }>h₂:<{ Γ ⊢ t₂✝ ⦂ τ }>h₃✝:<{ Γ ⊢ t₃✝ ⦂ τ }>⊢ Ty
      exact h₂All goals completed! 🐙
  | ite3 _ _ _ _ ih =>ite3x:Stringt:Tmt₁✝:Tmt₂✝:Tmt₃✝:Tmh✝:x ∈ᶠ t₃✝ih:∀ (τ : Ty) (Γ : Context), <{ Γ ⊢ t₃✝ ⦂ τ }> → ∃ τ', Γ[x] = some τ'τ:TyΓ:Contexthτ:<{ Γ ⊢ if t₁✝ then t₂✝ else t₃✝ ⦂ τ }>⊢ ∃ τ', Γ[x] = some τ'
    cases hτ with
    | ite _ _ _ _ _ _ _ h₃ =>ite3.itex:Stringt:Tmt₁✝:Tmt₂✝:Tmt₃✝:Tmh✝:x ∈ᶠ t₃✝ih:∀ (τ : Ty) (Γ : Context), <{ Γ ⊢ t₃✝ ⦂ τ }> → ∃ τ', Γ[x] = some τ'τ:TyΓ:Contexth₁✝:<{ Γ ⊢ t₁✝ ⦂ Bool }>h₂✝:<{ Γ ⊢ t₂✝ ⦂ τ }>h₃:<{ Γ ⊢ t₃✝ ⦂ τ }>⊢ ∃ τ', Γ[x] = some τ'
      apply ihite3.ite.hτx:Stringt:Tmt₁✝:Tmt₂✝:Tmt₃✝:Tmh✝:x ∈ᶠ t₃✝ih:∀ (τ : Ty) (Γ : Context), <{ Γ ⊢ t₃✝ ⦂ τ }> → ∃ τ', Γ[x] = some τ'τ:TyΓ:Contexth₁✝:<{ Γ ⊢ t₁✝ ⦂ Bool }>h₂✝:<{ Γ ⊢ t₂✝ ⦂ τ }>h₃:<{ Γ ⊢ t₃✝ ⦂ τ }>⊢ <{ Γ ⊢ t₃✝ ⦂ ~?ite3.ite.τ }>ite3.ite.τx:Stringt:Tmt₁✝:Tmt₂✝:Tmt₃✝:Tmh✝:x ∈ᶠ t₃✝ih:∀ (τ : Ty) (Γ : Context), <{ Γ ⊢ t₃✝ ⦂ τ }> → ∃ τ', Γ[x] = some τ'τ:TyΓ:Contexth₁✝:<{ Γ ⊢ t₁✝ ⦂ Bool }>h₂✝:<{ Γ ⊢ t₂✝ ⦂ τ }>h₃:<{ Γ ⊢ t₃✝ ⦂ τ }>⊢ Ty
      exact h₃All goals completed! 🐙

From the free_in_context lemma, it immediately follows that any term t that is well typed in the empty context is closed (it has no free variables).

Exercise★★(typable_empty_closed) (Optional)

theorem declaration uses `sorry`typable_empty_closed (t : Tm) (τ : Ty) (hτ : <{ ∅ ⊢ t ⦂ τ }>) : t.Closed := byt:Tmτ:Tyhτ:<{ ∅ ⊢ t ⦂ τ }>⊢ t.Closed
  sorryAll goals completed! 🐙

Finally, we establish context invariance. It is useful in cases when we have a proof of some typing relation Γ ⊢ t ⦂ τ, and we need to replace Γ by a different context Γ'. When is it safe to do this? Intuitively, it must at least be the case that Γ' assigns the same types as Γ to all the variables that appear free in t. In fact, this is the only condition that is needed.

Proof: By induction on the derivation of Γ ⊢ t ⦂ τ.

If the last rule in the derivation was HasType.var, then t = x and Γ x = τ. By assumption, Γ' x = τ as well, and hence Γ' ⊢ t ⦂ τ by HasType.var.
If the last rule was HasType.abs, then t = λy:τ₂. t₁, with τ = τ₂ → τ₁ and y ↦ τ₂ ; Γ ⊢ t₁ ⦂ τ₁. The induction hypothesis states that for any context Γ'', if y ↦ τ₂ ; Γ and Γ'' assign the same types to all the free variables in t₁, then t₁ has type τ₁ under Γ''. Let Γ' be a context which agrees with Γ on the free variables in t; we must show Γ' ⊢ λy:τ₂. t₁ ⦂ τ₂ → τ₁.

By HasType.abs, it suffices to show that y ↦ τ₂ ; Γ' ⊢ t₁ ⦂ τ₁. By the IH (setting Γ'' = y ↦ τ₂ ; Γ'), it suffices to show that y ↦ τ₂ ; Γ and y ↦ τ₂ ; Γ' agree on all the variables that appear free in t₁.

Any variable occurring free in t₁ must be either y or some other variable. y ↦ τ₂ ; Γ and y ↦ τ₂ ; Γ' clearly agree on y. Otherwise, note that any variable other than y that occurs free in t₁ also occurs free in t = λy:τ₂. t₁, and by assumption Γ and Γ' agree on all such variables; hence so do y ↦ τ₂ ; Γ and y ↦ τ₂ ; Γ'.
If the last rule was HasType.app, then t = t₁ t₂, with Γ ⊢ t₁ ⦂ τ₂ → τ and Γ ⊢ t₂ ⦂ τ₂. One induction hypothesis states that for all contexts Γ', if Γ' agrees with Γ on the free variables in t₁, then t₁ has type τ₂ → τ under Γ'; there is a similar IH for t₂. We must show that t₁ t₂ also has type τ under Γ', given the assumption that Γ' agrees with Γ on all the free variables in t₁ t₂. By HasType.app, it suffices to show that t₁ and t₂ each have the same type under Γ' as under Γ. But all free variables in t₁ are also free in t₁ t₂, and similarly for t₂; hence the desired result follows from the induction hypotheses.

Exercise★★★(context_invariance) (Optional)

Complete the following proof.

theorem declaration uses `sorry`context_invariance (Γ Γ' : Context) (t : Tm) (τ : Ty)
    (hτ : <{ Γ ⊢ t ⦂ τ }>) (hf : ∀ x, x ∈ᶠ t → Γ[x] = Γ'[x]) :
    <{ Γ' ⊢ t ⦂ τ }> := byΓ:ContextΓ':Contextt:Tmτ:Tyhτ:<{ Γ ⊢ t ⦂ τ }>hf:∀ (x : String), x ∈ᶠ t → Γ[x] = Γ'[x]⊢ <{ Γ' ⊢ t ⦂ τ }>
  induction hτ generalizing Γ' with
  | var _ x _ h =>varΓ:Contextt:Tmτ:TyΓ✝:Contextx:Stringτ₁✝:Tyh:Γ✝[x] = some τ₁✝Γ':Contexthf:∀ (x_1 : String), x_1 ∈ᶠ Stlc.Tm.var x → Γ✝[x_1] = Γ'[x_1]⊢ <{ Γ' ⊢ ~(Stlc.Tm.var x) ⦂ τ₁✝ }>
    sorryAll goals completed! 🐙
  | abs _ y _ _ _ _ ih =>absΓ:Contextt:Tmτ:TyΓ✝:Contexty:Stringτ₁✝:Tyτ₂✝:Tyt₁✝:Tmh✝:<{ ~(y →ₚ τ₂✝ ; Γ✝) ⊢ t₁✝ ⦂ τ₁✝ }>ih:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₁✝ → (y →ₚ τ₂✝ ; Γ✝)[x] = Γ'[x]) → <{ Γ' ⊢ t₁✝ ⦂ τ₁✝ }>Γ':Contexthf:∀ (x : String), x ∈ᶠ <{ λ ~y : τ₂✝ . t₁✝ }> → Γ✝[x] = Γ'[x]⊢ <{ Γ' ⊢ λ ~y : τ₂✝ . t₁✝ ⦂ τ₂✝ → τ₁✝ }>
    sorryAll goals completed! 🐙
  | app _ _ _ t₁ t₂ _ _ ih₁ ih₂ =>appΓ:Contextt:Tmτ:TyΓ✝:Contextτ₁✝:Tyτ₂✝:Tyt₁:Tmt₂:Tmh₁✝:<{ Γ✝ ⊢ t₁ ⦂ τ₂✝ → τ₁✝ }>h₂✝:<{ Γ✝ ⊢ t₂ ⦂ τ₂✝ }>ih₁:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₁ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₁ ⦂ τ₂✝ → τ₁✝ }>ih₂:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₂ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₂ ⦂ τ₂✝ }>Γ':Contexthf:∀ (x : String), x ∈ᶠ <{ t₁ t₂ }> → Γ✝[x] = Γ'[x]⊢ <{ Γ' ⊢ t₁ t₂ ⦂ τ₁✝ }>
    sorryAll goals completed! 🐙
  | tru =>truΓ:Contextt:Tmτ:TyΓ✝:ContextΓ':Contexthf:∀ (x : String), x ∈ᶠ <{ true }> → Γ✝[x] = Γ'[x]⊢ <{ Γ' ⊢ true ⦂ Bool }> constructorAll goals completed! 🐙
  | fls =>flsΓ:Contextt:Tmτ:TyΓ✝:ContextΓ':Contexthf:∀ (x : String), x ∈ᶠ <{ false }> → Γ✝[x] = Γ'[x]⊢ <{ Γ' ⊢ false ⦂ Bool }> constructorAll goals completed! 🐙
  | ite _ t₁ t₂ t₃ _ _ _ _ ih₁ ih₂ ih₃ =>iteΓ:Contextt:Tmτ:TyΓ✝:Contextt₁:Tmt₂:Tmt₃:Tmτ₁✝:Tyh₁✝:<{ Γ✝ ⊢ t₁ ⦂ Bool }>h₂✝:<{ Γ✝ ⊢ t₂ ⦂ τ₁✝ }>h₃✝:<{ Γ✝ ⊢ t₃ ⦂ τ₁✝ }>ih₁:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₁ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₁ ⦂ Bool }>ih₂:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₂ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₂ ⦂ τ₁✝ }>ih₃:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₃ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₃ ⦂ τ₁✝ }>Γ':Contexthf:∀ (x : String), x ∈ᶠ <{ if t₁ then t₂ else t₃ }> → Γ✝[x] = Γ'[x]⊢ <{ Γ' ⊢ if t₁ then t₂ else t₃ ⦂ τ₁✝ }>
    constructorite.h₁Γ:Contextt:Tmτ:TyΓ✝:Contextt₁:Tmt₂:Tmt₃:Tmτ₁✝:Tyh₁✝:<{ Γ✝ ⊢ t₁ ⦂ Bool }>h₂✝:<{ Γ✝ ⊢ t₂ ⦂ τ₁✝ }>h₃✝:<{ Γ✝ ⊢ t₃ ⦂ τ₁✝ }>ih₁:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₁ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₁ ⦂ Bool }>ih₂:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₂ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₂ ⦂ τ₁✝ }>ih₃:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₃ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₃ ⦂ τ₁✝ }>Γ':Contexthf:∀ (x : String), x ∈ᶠ <{ if t₁ then t₂ else t₃ }> → Γ✝[x] = Γ'[x]⊢ <{ Γ' ⊢ t₁ ⦂ Bool }>ite.h₂Γ:Contextt:Tmτ:TyΓ✝:Contextt₁:Tmt₂:Tmt₃:Tmτ₁✝:Tyh₁✝:<{ Γ✝ ⊢ t₁ ⦂ Bool }>h₂✝:<{ Γ✝ ⊢ t₂ ⦂ τ₁✝ }>h₃✝:<{ Γ✝ ⊢ t₃ ⦂ τ₁✝ }>ih₁:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₁ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₁ ⦂ Bool }>ih₂:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₂ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₂ ⦂ τ₁✝ }>ih₃:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₃ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₃ ⦂ τ₁✝ }>Γ':Contexthf:∀ (x : String), x ∈ᶠ <{ if t₁ then t₂ else t₃ }> → Γ✝[x] = Γ'[x]⊢ <{ Γ' ⊢ t₂ ⦂ τ₁✝ }>ite.h₃Γ:Contextt:Tmτ:TyΓ✝:Contextt₁:Tmt₂:Tmt₃:Tmτ₁✝:Tyh₁✝:<{ Γ✝ ⊢ t₁ ⦂ Bool }>h₂✝:<{ Γ✝ ⊢ t₂ ⦂ τ₁✝ }>h₃✝:<{ Γ✝ ⊢ t₃ ⦂ τ₁✝ }>ih₁:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₁ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₁ ⦂ Bool }>ih₂:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₂ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₂ ⦂ τ₁✝ }>ih₃:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₃ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₃ ⦂ τ₁✝ }>Γ':Contexthf:∀ (x : String), x ∈ᶠ <{ if t₁ then t₂ else t₃ }> → Γ✝[x] = Γ'[x]⊢ <{ Γ' ⊢ t₃ ⦂ τ₁✝ }>
    ·ite.h₁Γ:Contextt:Tmτ:TyΓ✝:Contextt₁:Tmt₂:Tmt₃:Tmτ₁✝:Tyh₁✝:<{ Γ✝ ⊢ t₁ ⦂ Bool }>h₂✝:<{ Γ✝ ⊢ t₂ ⦂ τ₁✝ }>h₃✝:<{ Γ✝ ⊢ t₃ ⦂ τ₁✝ }>ih₁:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₁ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₁ ⦂ Bool }>ih₂:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₂ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₂ ⦂ τ₁✝ }>ih₃:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₃ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₃ ⦂ τ₁✝ }>Γ':Contexthf:∀ (x : String), x ∈ᶠ <{ if t₁ then t₂ else t₃ }> → Γ✝[x] = Γ'[x]⊢ <{ Γ' ⊢ t₁ ⦂ Bool }> apply ih₁ite.h₁Γ:Contextt:Tmτ:TyΓ✝:Contextt₁:Tmt₂:Tmt₃:Tmτ₁✝:Tyh₁✝:<{ Γ✝ ⊢ t₁ ⦂ Bool }>h₂✝:<{ Γ✝ ⊢ t₂ ⦂ τ₁✝ }>h₃✝:<{ Γ✝ ⊢ t₃ ⦂ τ₁✝ }>ih₁:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₁ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₁ ⦂ Bool }>ih₂:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₂ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₂ ⦂ τ₁✝ }>ih₃:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₃ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₃ ⦂ τ₁✝ }>Γ':Contexthf:∀ (x : String), x ∈ᶠ <{ if t₁ then t₂ else t₃ }> → Γ✝[x] = Γ'[x]⊢ ∀ (x : String), x ∈ᶠ t₁ → Γ✝[x] = Γ'[x]
      intro z hzite.h₁Γ:Contextt:Tmτ:TyΓ✝:Contextt₁:Tmt₂:Tmt₃:Tmτ₁✝:Tyh₁✝:<{ Γ✝ ⊢ t₁ ⦂ Bool }>h₂✝:<{ Γ✝ ⊢ t₂ ⦂ τ₁✝ }>h₃✝:<{ Γ✝ ⊢ t₃ ⦂ τ₁✝ }>ih₁:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₁ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₁ ⦂ Bool }>ih₂:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₂ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₂ ⦂ τ₁✝ }>ih₃:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₃ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₃ ⦂ τ₁✝ }>Γ':Contexthf:∀ (x : String), x ∈ᶠ <{ if t₁ then t₂ else t₃ }> → Γ✝[x] = Γ'[x]z:Stringhz:z ∈ᶠ t₁⊢ Γ✝[z] = Γ'[z]
      apply hfite.h₁Γ:Contextt:Tmτ:TyΓ✝:Contextt₁:Tmt₂:Tmt₃:Tmτ₁✝:Tyh₁✝:<{ Γ✝ ⊢ t₁ ⦂ Bool }>h₂✝:<{ Γ✝ ⊢ t₂ ⦂ τ₁✝ }>h₃✝:<{ Γ✝ ⊢ t₃ ⦂ τ₁✝ }>ih₁:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₁ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₁ ⦂ Bool }>ih₂:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₂ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₂ ⦂ τ₁✝ }>ih₃:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₃ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₃ ⦂ τ₁✝ }>Γ':Contexthf:∀ (x : String), x ∈ᶠ <{ if t₁ then t₂ else t₃ }> → Γ✝[x] = Γ'[x]z:Stringhz:z ∈ᶠ t₁⊢ z ∈ᶠ <{ if t₁ then t₂ else t₃ }>
      apply AppearsFreeIn.ite1ite.h₁Γ:Contextt:Tmτ:TyΓ✝:Contextt₁:Tmt₂:Tmt₃:Tmτ₁✝:Tyh₁✝:<{ Γ✝ ⊢ t₁ ⦂ Bool }>h₂✝:<{ Γ✝ ⊢ t₂ ⦂ τ₁✝ }>h₃✝:<{ Γ✝ ⊢ t₃ ⦂ τ₁✝ }>ih₁:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₁ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₁ ⦂ Bool }>ih₂:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₂ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₂ ⦂ τ₁✝ }>ih₃:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₃ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₃ ⦂ τ₁✝ }>Γ':Contexthf:∀ (x : String), x ∈ᶠ <{ if t₁ then t₂ else t₃ }> → Γ✝[x] = Γ'[x]z:Stringhz:z ∈ᶠ t₁⊢ z ∈ᶠ t₁
      exact hzAll goals completed! 🐙
    ·ite.h₂Γ:Contextt:Tmτ:TyΓ✝:Contextt₁:Tmt₂:Tmt₃:Tmτ₁✝:Tyh₁✝:<{ Γ✝ ⊢ t₁ ⦂ Bool }>h₂✝:<{ Γ✝ ⊢ t₂ ⦂ τ₁✝ }>h₃✝:<{ Γ✝ ⊢ t₃ ⦂ τ₁✝ }>ih₁:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₁ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₁ ⦂ Bool }>ih₂:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₂ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₂ ⦂ τ₁✝ }>ih₃:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₃ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₃ ⦂ τ₁✝ }>Γ':Contexthf:∀ (x : String), x ∈ᶠ <{ if t₁ then t₂ else t₃ }> → Γ✝[x] = Γ'[x]⊢ <{ Γ' ⊢ t₂ ⦂ τ₁✝ }> apply ih₂ite.h₂Γ:Contextt:Tmτ:TyΓ✝:Contextt₁:Tmt₂:Tmt₃:Tmτ₁✝:Tyh₁✝:<{ Γ✝ ⊢ t₁ ⦂ Bool }>h₂✝:<{ Γ✝ ⊢ t₂ ⦂ τ₁✝ }>h₃✝:<{ Γ✝ ⊢ t₃ ⦂ τ₁✝ }>ih₁:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₁ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₁ ⦂ Bool }>ih₂:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₂ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₂ ⦂ τ₁✝ }>ih₃:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₃ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₃ ⦂ τ₁✝ }>Γ':Contexthf:∀ (x : String), x ∈ᶠ <{ if t₁ then t₂ else t₃ }> → Γ✝[x] = Γ'[x]⊢ ∀ (x : String), x ∈ᶠ t₂ → Γ✝[x] = Γ'[x]
      intro z hzite.h₂Γ:Contextt:Tmτ:TyΓ✝:Contextt₁:Tmt₂:Tmt₃:Tmτ₁✝:Tyh₁✝:<{ Γ✝ ⊢ t₁ ⦂ Bool }>h₂✝:<{ Γ✝ ⊢ t₂ ⦂ τ₁✝ }>h₃✝:<{ Γ✝ ⊢ t₃ ⦂ τ₁✝ }>ih₁:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₁ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₁ ⦂ Bool }>ih₂:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₂ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₂ ⦂ τ₁✝ }>ih₃:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₃ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₃ ⦂ τ₁✝ }>Γ':Contexthf:∀ (x : String), x ∈ᶠ <{ if t₁ then t₂ else t₃ }> → Γ✝[x] = Γ'[x]z:Stringhz:z ∈ᶠ t₂⊢ Γ✝[z] = Γ'[z]
      apply hfite.h₂Γ:Contextt:Tmτ:TyΓ✝:Contextt₁:Tmt₂:Tmt₃:Tmτ₁✝:Tyh₁✝:<{ Γ✝ ⊢ t₁ ⦂ Bool }>h₂✝:<{ Γ✝ ⊢ t₂ ⦂ τ₁✝ }>h₃✝:<{ Γ✝ ⊢ t₃ ⦂ τ₁✝ }>ih₁:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₁ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₁ ⦂ Bool }>ih₂:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₂ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₂ ⦂ τ₁✝ }>ih₃:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₃ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₃ ⦂ τ₁✝ }>Γ':Contexthf:∀ (x : String), x ∈ᶠ <{ if t₁ then t₂ else t₃ }> → Γ✝[x] = Γ'[x]z:Stringhz:z ∈ᶠ t₂⊢ z ∈ᶠ <{ if t₁ then t₂ else t₃ }>
      apply AppearsFreeIn.ite2ite.h₂Γ:Contextt:Tmτ:TyΓ✝:Contextt₁:Tmt₂:Tmt₃:Tmτ₁✝:Tyh₁✝:<{ Γ✝ ⊢ t₁ ⦂ Bool }>h₂✝:<{ Γ✝ ⊢ t₂ ⦂ τ₁✝ }>h₃✝:<{ Γ✝ ⊢ t₃ ⦂ τ₁✝ }>ih₁:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₁ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₁ ⦂ Bool }>ih₂:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₂ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₂ ⦂ τ₁✝ }>ih₃:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₃ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₃ ⦂ τ₁✝ }>Γ':Contexthf:∀ (x : String), x ∈ᶠ <{ if t₁ then t₂ else t₃ }> → Γ✝[x] = Γ'[x]z:Stringhz:z ∈ᶠ t₂⊢ z ∈ᶠ t₂
      exact hzAll goals completed! 🐙
    ·ite.h₃Γ:Contextt:Tmτ:TyΓ✝:Contextt₁:Tmt₂:Tmt₃:Tmτ₁✝:Tyh₁✝:<{ Γ✝ ⊢ t₁ ⦂ Bool }>h₂✝:<{ Γ✝ ⊢ t₂ ⦂ τ₁✝ }>h₃✝:<{ Γ✝ ⊢ t₃ ⦂ τ₁✝ }>ih₁:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₁ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₁ ⦂ Bool }>ih₂:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₂ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₂ ⦂ τ₁✝ }>ih₃:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₃ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₃ ⦂ τ₁✝ }>Γ':Contexthf:∀ (x : String), x ∈ᶠ <{ if t₁ then t₂ else t₃ }> → Γ✝[x] = Γ'[x]⊢ <{ Γ' ⊢ t₃ ⦂ τ₁✝ }> apply ih₃ite.h₃Γ:Contextt:Tmτ:TyΓ✝:Contextt₁:Tmt₂:Tmt₃:Tmτ₁✝:Tyh₁✝:<{ Γ✝ ⊢ t₁ ⦂ Bool }>h₂✝:<{ Γ✝ ⊢ t₂ ⦂ τ₁✝ }>h₃✝:<{ Γ✝ ⊢ t₃ ⦂ τ₁✝ }>ih₁:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₁ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₁ ⦂ Bool }>ih₂:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₂ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₂ ⦂ τ₁✝ }>ih₃:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₃ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₃ ⦂ τ₁✝ }>Γ':Contexthf:∀ (x : String), x ∈ᶠ <{ if t₁ then t₂ else t₃ }> → Γ✝[x] = Γ'[x]⊢ ∀ (x : String), x ∈ᶠ t₃ → Γ✝[x] = Γ'[x]
      intro z hzite.h₃Γ:Contextt:Tmτ:TyΓ✝:Contextt₁:Tmt₂:Tmt₃:Tmτ₁✝:Tyh₁✝:<{ Γ✝ ⊢ t₁ ⦂ Bool }>h₂✝:<{ Γ✝ ⊢ t₂ ⦂ τ₁✝ }>h₃✝:<{ Γ✝ ⊢ t₃ ⦂ τ₁✝ }>ih₁:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₁ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₁ ⦂ Bool }>ih₂:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₂ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₂ ⦂ τ₁✝ }>ih₃:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₃ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₃ ⦂ τ₁✝ }>Γ':Contexthf:∀ (x : String), x ∈ᶠ <{ if t₁ then t₂ else t₃ }> → Γ✝[x] = Γ'[x]z:Stringhz:z ∈ᶠ t₃⊢ Γ✝[z] = Γ'[z]
      apply hfite.h₃Γ:Contextt:Tmτ:TyΓ✝:Contextt₁:Tmt₂:Tmt₃:Tmτ₁✝:Tyh₁✝:<{ Γ✝ ⊢ t₁ ⦂ Bool }>h₂✝:<{ Γ✝ ⊢ t₂ ⦂ τ₁✝ }>h₃✝:<{ Γ✝ ⊢ t₃ ⦂ τ₁✝ }>ih₁:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₁ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₁ ⦂ Bool }>ih₂:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₂ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₂ ⦂ τ₁✝ }>ih₃:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₃ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₃ ⦂ τ₁✝ }>Γ':Contexthf:∀ (x : String), x ∈ᶠ <{ if t₁ then t₂ else t₃ }> → Γ✝[x] = Γ'[x]z:Stringhz:z ∈ᶠ t₃⊢ z ∈ᶠ <{ if t₁ then t₂ else t₃ }>
      apply AppearsFreeIn.ite3ite.h₃Γ:Contextt:Tmτ:TyΓ✝:Contextt₁:Tmt₂:Tmt₃:Tmτ₁✝:Tyh₁✝:<{ Γ✝ ⊢ t₁ ⦂ Bool }>h₂✝:<{ Γ✝ ⊢ t₂ ⦂ τ₁✝ }>h₃✝:<{ Γ✝ ⊢ t₃ ⦂ τ₁✝ }>ih₁:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₁ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₁ ⦂ Bool }>ih₂:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₂ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₂ ⦂ τ₁✝ }>ih₃:∀ (Γ' : Context), (∀ (x : String), x ∈ᶠ t₃ → Γ✝[x] = Γ'[x]) → <{ Γ' ⊢ t₃ ⦂ τ₁✝ }>Γ':Contexthf:∀ (x : String), x ∈ᶠ <{ if t₁ then t₂ else t₃ }> → Γ✝[x] = Γ'[x]z:Stringhz:z ∈ᶠ t₃⊢ z ∈ᶠ t₃
      exact hzAll goals completed! 🐙

The context invariance lemma can actually be used in place of the weakening lemma to prove the crucial substitution lemma stated earlier.

6.7. Additional Exercises🔗

Exercise★(progress_preservation_statement) (Optional, Manually graded)

(Officially optional, but strongly recommended!) Without peeking at their statements above, write down the progress and preservation theorems for the simply typed lambda-calculus (as Lean theorems). You can write sorry for the proofs.

theorem progress_statement :
    FILL IN HERE := by
  apply progress

theorem preservation_statement :
    FILL IN HERE := by
  apply preservation

Exercise★★(stlc_variation1) (Manually graded)

Suppose we add a new term zap with the following reduction rule

                         ---------                  (zap)
                         t ⟶ zap

and the following typing rule:

                        -----------                 (zap)
                        Γ ⊢ zap ⦂ τ

Which of the following properties of the STLC remain true in the presence of these rules? For each property, write either "remains true" or "becomes false." If a property becomes false, give a counterexample.

Determinism of Step

Progress

Preservation

Exercise★★(stlc_variation2) (Manually graded)

Suppose instead that we add a new term foo with the following reduction rules:

                       -----------------                (foo1)
                        (λx:τ. x) ⟶ foo

                         ------------                   (foo2)
                          foo ⟶ true

Which of the following properties of the STLC remain true in the presence of this rule? For each one, write either "remains true" or else "becomes false." If a property becomes false, give a counterexample.

Determinism of Step

Progress

Preservation

Exercise★★(stlc_variation3) (Manually graded)

Suppose instead that we remove the rule Step.app1 from the Step relation. Which of the following properties of the STLC remain true in the presence of this rule? For each one, write either "remains true" or else "becomes false." If a property becomes false, give a counterexample.

Determinism of Step

Progress

Preservation

Exercise★★(stlc_variation4) (Optional)

Suppose instead that we add the following new rule to the reduction relation:

            ----------------------------------        (funnyIfTrue)
             (if true then t₁ else t₂) ⟶ true

Determinism of Step

Progress

Preservation

Exercise★★(stlc_variation5) (Optional)

Suppose instead that we add the following new rule to the typing relation:

                 Γ ⊢ t₁ ⦂ Bool → Bool → Bool
                        Γ ⊢ t₂ ⦂ Bool
                ------------------------------       (funnyApp)
                       Γ ⊢ t₁ t₂ ⦂ Bool

Determinism of Step

Progress

Preservation

Exercise★★(stlc_variation6) (Optional)

Suppose instead that we add the following new rule to the typing relation:

                        Γ ⊢ t₁ ⦂ Bool
                        Γ ⊢ t₂ ⦂ Bool
                      ------------------            (funnyApp')
                      Γ ⊢ t₁ t₂ ⦂ Bool

Determinism of Step

Progress

Preservation

Exercise★★(stlc_variation7) (Optional)

Suppose we add the following new rule to the typing relation of the STLC:

                       ------------------------     (funnyAbs)
                        ∅ ⊢ λx:Bool. t ⦂ Bool

Determinism of Step

Progress

Preservation

The STLC typing relation with the funnyAbs rule of stlc_variation7 added, and a proof that progress then fails.

end Stlc

6.7.1. Exercise: STLC with Arithmetic🔗

To see how the STLC might function as the core of a real programming language, let's extend it with a concrete base type of numbers and some constants and primitive operators.

The arithmetic we are adding is the arithmetic of the Slang chapter — numeric constants and multiplication — together with the successor, predecessor, and zero-test operations of the Types chapter. What is new is the setting: those operations now live in a language that also has variables, abstraction, and application, so an arithmetic computation can be packaged up as a function and passed around as a value.

namespace StlcArith

open scoped MyGetElem

To types, we add a base type of natural numbers (and remove booleans, for brevity).

inductive Ty where
  | arrow (τ₁ τ₂ : Ty)
  | nat

To terms, we add natural number constants, along with successor, predecessor, multiplication, and zero-testing.

inductive Tm where
  | var (x : String)
  | app (t₁ t₂ : Tm)
  | abs (x : String) (τ : Ty) (t : Tm)
  | const (n : Nat)
  | succ (t : Tm)
  | pred (t : Tm)
  | mult (t₁ t₂ : Tm)
  | ite0 (c t e : Tm)

StlcArith is a different language from the STLC of this chapter, not an extension of it, so it needs its own interpretation of the shared concrete syntax. Terms and types still use <{ ... }> and the same identifier convention as Stlc: capital Latin identifiers are object-language (StlcArith) names; lowercase and Greek identifiers refer directly to in-scope Lean variables; arbitrary Lean expressions require ~ antiquotation; and object-language identifiers cannot contain dots.

Notation encoding

scoped syntax:max num : stlcTm
scoped syntax:60 stlcTm:60 " * " stlcTm:61 : stlcTm
scoped syntax:50 "if0 " stlcTm:51 " then " stlcTm:50 " else " stlcTm:50 : stlcTm

namespace Elab

open StlcCommon
open Lean Meta Elab Term

def language : Language where
  tyType := ``Ty
  tmType := ``Tm
  arrowCtor := ``Ty.arrow
  varCtor := ``Tm.var
  appCtor := ``Tm.app
  absCtor := ``Tm.abs

  -- defined later
  subst := `StlcArith.subst
  hasType := `StlcArith.HasType

def natTyHandler : TyElabHandler :=
  fun _recur k T => do
    match T with
    | `(stlcTy| Nat) =>
        return mkConst ``Ty.nat
    | _ => k T

def tyHandlers : TyElabHandler :=
  natTyHandler.orElse (commonTyHandler language)

partial def elabTy : TyElab :=
  tyHandlers elabTy <| unsupportedTy language

def arithTmHandler : TmElabHandler :=
  fun recur k Γ free t => do
    match t with
    | `(stlcTm| $n:num) => do
        return (mkApp (mkConst ``Tm.const) (mkNatLit n.getNat), free)
    | `(stlcTm| Nat) => do
        throwError "`Nat` is not a valid term."
    | `(stlcTm| succ $e:stlcTm) => do
        let (e, free) ←  recur Γ free e
        return (mkApp (mkConst ``Tm.succ) e, free)
    | `(stlcTm| pred $e:stlcTm) => do
        let (e, free) ←  recur Γ free e
        return (mkApp (mkConst ``Tm.pred) e, free)
    | `(stlcTm| $t₁:stlcTm * $t₂:stlcTm) => do
        let (e₁, free) ←  recur Γ free t₁
        let (e₂, free) ←  recur Γ free t₂
        return (mkApp2 (mkConst ``Tm.mult) e₁ e₂, free)
    | `(stlcTm| if0 $c:stlcTm then $t:stlcTm else $e:stlcTm) => do
        let (c, free) ← recur Γ free c
        let (t, free) ← recur Γ free t
        let (e, free) ← recur Γ free e
        return (mkApp3 (mkConst ``Tm.ite0) c t e, free)
    | _ => k Γ free t

def tmHandlers : TmElabHandler :=
  arithTmHandler.orElse (commonTmHandler language elabTy)

partial def elabTm : TmElab :=
  tmHandlers elabTm unsupportedTm

def elabCtx : CtxElab := elabCtxCommon language elabTy

@[scoped term_elab StlcCommon.bracket]
def elabBracket : TermElab :=
  fun stx expectedType? => do
    let `(<{ $q:stlcQuoted }>) := stx
      | throwUnsupportedSyntax
    elabQuoted language elabTy elabTm elabCtx q expectedType?

end Elab

open scoped Elab


namespace Delab

open StlcCommon Elab Delab
open Lean PrettyPrinter Delaborator

@[app_unexpander Ty.nat]
private def Ty.unexpandNat : Unexpander
  | stx => do
    let T ← `(stlcTy| $(mkIdentFrom stx `Nat):ident)
    `(<{ $T:stlcTy }>)

@[app_unexpander Ty.arrow]
private def Ty.unexpandArrow : Unexpander := Delab.unexpandArrow

private def reservedNames : String → Bool
  | "Nat" | "succ" | "pred" | "if0" => true
  | _ => false

@[app_unexpander Tm.var]
private def Tm.unexpandVar : Unexpander := Delab.unexpandVar reservedNames ``Tm.var

@[app_delab Tm.var]
private def Tm.delabVar : Delab := Delab.delabVar ``Tm.var

@[app_unexpander Tm.app]
private def Tm.unexpandApp : Unexpander := Delab.unexpandApp

@[app_unexpander Tm.abs]
private def Tm.unexpandAbs : Unexpander := Delab.unexpandAbs

@[app_unexpander Tm.ite0]
private def Tm.unexpandIte : Unexpander
  | `($_ $c $t $e) =>
      `(<{ if0 $(getTm c) then $(getTm t) else $(getTm e) }>)
  | _ => throw ()

@[app_unexpander Tm.const]
def Tm.unexpandConst : Unexpander
  | `($_ $n:num) => `(<{ $n:num }>)
  | _ => throw ()

@[app_unexpander Tm.succ]
def Tm.unexpandSucc : Unexpander
  | stx@`($_ $t) => do
    let succ := mkObjectIdentFrom stx "succ"
    `(<{ $succ:ident $(getTm t) }>)
  | _ => throw ()

@[app_unexpander Tm.pred]
def Tm.unexpandPred : Unexpander
  | stx@`($_ $t) => do
    let pred := mkObjectIdentFrom stx "pred"
    `(<{ $pred:ident $(getTm t) }>)
  | _ => throw ()

@[app_unexpander Tm.mult]
def Tm.unexpandMult : Unexpander
  | `($_ $t₁ $t₂) => do
    let t ← `(stlcTm| $(getTm t₁) * $(getTm t₂))
    let q ← `(stlcQuoted| $t:stlcTm)
    `(<{ $q:stlcQuoted }>)
  | _ => throw ()

end Delab

In this extended exercise, your job is to finish formalizing the definition and properties of the STLC extended with arithmetic. Specifically:

Fill in the core definitions for StlcArith, by starting with the rules and terms which are the same as the STLC. Then prove the key lemmas and theorems we provide. You will need to define and prove helper lemmas, as before.

Make sure Lean accepts the whole file before submitting.

Exercise★★★★★(StlcArith.subst)

Substitution is defined exactly as it was for the STLC, with one clause per new constructor.

def declaration uses `sorry`subst (x : String) (s : Tm) (t : Tm) : Tm := sorry

Notation encoding

open Lean PrettyPrinter in
@[app_unexpander subst]
def unexpandSubst : Unexpander := StlcCommon.Delab.unexpandSubst

You will also want one @[simp] simplification lemma per constructor, saying how your subst behaves on that constructor, in the style of the Stlc chapter — the substitution lemma below is proved by rewriting with them rather than by unfolding the definition. Two of the constructors need two lemmas apiece, since substitution treats a bound name differently depending on whether it is the name being substituted for.

section
variable (x y : String) (s t t₁ t₂ t₃ : Tm) (τ : Ty) (n : Nat)
--  FILL IN HERE
end

Next, the values.

inductive Tm.IsValue : Tm → Prop where
--  FILL IN HERE

Now the reduction relation.

section
set_option hygiene false in
local notation:40 t:41 " ⟶ " t':41 => Step t t'

inductive Step : Tm → Tm → Prop where
--  FILL IN HERE
end

scoped notation:40 t:41 " ⟶ " t':41 => Step t t'
scoped notation:40 t:41 " ⟶* " t':41 => Multi Step t t'

An example:

--  FILL IN HERE

--  FILL IN HERE

theorem declaration uses `sorry`Nat_step_example : ∃ t, <{ (λ X : Nat . λ Y : Nat . X * Y) 3 2 }> ⟶* t := by⊢ ∃ t, <{ (λ X : Nat . λ Y : Nat . X * Y) 3 2 }> ⟶* t
  sorryAll goals completed! 🐙

A typing context is a partial map from variables to types, exactly as before.

abbrev Context := PartialMap String Ty

Now the typing relation.

inductive HasType : Context → Tm → Ty → Prop where
--  FILL IN HERE

Notation encoding

open Lean PrettyPrinter in
@[app_unexpander HasType]
def HasType.unexpand : Unexpander := StlcCommon.Delab.unexpandHasType

An example:

theorem declaration uses `sorry`Nat_typing_example : <{ ∅ ⊢ (λ X : Nat . λ Y : Nat . X * Y) 3 2 ⦂ Nat }> := by⊢ <{ ∅ ⊢ (λ X : Nat . λ Y : Nat . X * Y) 3 2 ⦂ Nat }>
  sorryAll goals completed! 🐙

6.7.1.1. The Technical Theorems🔗

The next lemmas are proved exactly as before.

Exercise★★★★(StlcArith.weakening)

theorem declaration uses `sorry`weakening (Γ Γ' : Context) (t : Tm) (τ : Ty)
    (hi : Γ ⊆ Γ') (hτ : <{ Γ ⊢ t ⦂ τ }>) : <{ Γ' ⊢ t ⦂ τ }> := byΓ:ContextΓ':Contextt:Tmτ:Tyhi:Γ ⊆ Γ'hτ:<{ Γ ⊢ t ⦂ τ }>⊢ <{ Γ' ⊢ t ⦂ τ }>
  sorryAll goals completed! 🐙

The two helper lemmas that weakening is for are also proved just as they were for the STLC.

--  FILL IN HERE
--  FILL IN HERE
unexpected end of input

6.7.1.2. Preservation🔗

Exercise★★★★(StlcArith.preservation)

Hint: you will need to define and prove the same helper lemmas we used before.

theorem declaration uses `sorry`preservation (t t' : Tm) (τ : Ty)
    (hτ : <{ ∅ ⊢ t ⦂ τ }>) (hs : t ⟶ t') : <{ ∅ ⊢ t' ⦂ τ }> := byt:Tmt':Tmτ:Tyhτ:<{ ∅ ⊢ t ⦂ τ }>hs:t ⟶ t'⊢ <{ ∅ ⊢ t' ⦂ τ }>
  sorryAll goals completed! 🐙

6.7.1.3. Progress🔗

Exercise★★★★(StlcArith.progress)

theorem declaration uses `sorry`progress (t : Tm) (τ : Ty) (hτ : <{ ∅ ⊢ t ⦂ τ }>) :
    t.IsValue ∨ ∃ t', t ⟶ t' := byt:Tmτ:Tyhτ:<{ ∅ ⊢ t ⦂ τ }>⊢ t.IsValue ∨ ∃ t', t ⟶ t'
  sorryAll goals completed! 🐙

end StlcArith

Source revision: e85fe77, committed 2026-10-06 21:16 UTC