3.4. Metatheory🔗

The rest of the file records the first general facts about typing. The visible proof steps are intended to be mathematical statements; automation is used to discharge the routine bookkeeping inside those steps.

theorem typing_independent_of_context
  (hlookup : ∀x ∈ L1.FV e, lookup x Γ = lookup x Δ)
  (ht : Γ ⊢ e : A)
  : Δ ⊢ e : A :=
bye:L1Γ:ContextΔ:ContextA:Tyhlookup:∀ (x : String), x ∈ e.FV → lookup x Γ = lookup x Δht:Γ ⊢ e : A⊢ Δ ⊢ e : A
  induction ht generalizing Δvare:L1Γ:ContextA:Tyx✝:StringΓ✝:ContextA✝:Tya✝:lookup x✝ Γ✝ = some A✝Δ:Contexthlookup:∀ (x : String), x ∈ (L1.var x✝).FV → lookup x Γ✝ = lookup x Δ⊢ Δ ⊢ L1.var x✝ : A✝lame:L1Γ:ContextA:Tyx✝:StringA✝:TyΓ✝:List (String × Ty)body✝:L1B✝:Tya✝:(x✝, A✝) :: Γ✝ ⊢ body✝ : B✝a_ih✝:∀ {Δ : Context}, (∀ (x : String), x ∈ body✝.FV → lookup x ((x✝, A✝) :: Γ✝) = lookup x Δ) → Δ ⊢ body✝ : B✝Δ:Contexthlookup:∀ (x : String), x ∈ (L1.lam x✝ body✝).FV → lookup x Γ✝ = lookup x Δ⊢ Δ ⊢ L1.lam x✝ body✝ : A✝ ⇒ B✝appe:L1Γ:ContextA:TyΓ✝:Contextfn✝:L1A✝:TyB✝:Tyarg✝:L1a✝¹:Γ✝ ⊢ fn✝ : A✝ ⇒ B✝a✝:Γ✝ ⊢ arg✝ : A✝a_ih✝¹:∀ {Δ : Context}, (∀ (x : String), x ∈ fn✝.FV → lookup x Γ✝ = lookup x Δ) → Δ ⊢ fn✝ : A✝ ⇒ B✝a_ih✝:∀ {Δ : Context}, (∀ (x : String), x ∈ arg✝.FV → lookup x Γ✝ = lookup x Δ) → Δ ⊢ arg✝ : A✝Δ:Contexthlookup:∀ (x : String), x ∈ (fn✝.app arg✝).FV → lookup x Γ✝ = lookup x Δ⊢ Δ ⊢ fn✝.app arg✝ : B✝
  case var x Γ A h =>e:L1Γ✝:ContextA✝:Tyx:StringΓ:ContextA:Tyh:lookup x✝ Γ✝ = some A✝Δ:Contexthlookup:∀ (x : String), x ∈ (L1.var x✝).FV → lookup x Γ✝ = lookup x Δ⊢ Δ ⊢ L1.var x✝ : A✝
      have : x ∈ L1.FV (L1.var x) := bye:L1Γ:ContextΔ:ContextA:Tyhlookup:∀ (x : String), x ∈ e.FV → lookup x Γ = lookup x Δht:Γ ⊢ e : A⊢ Δ ⊢ e : A
        rflAll goals completed! 🐙
      have : lookup x Δ = some A := bye:L1Γ:ContextΔ:ContextA:Tyhlookup:∀ (x : String), x ∈ e.FV → lookup x Γ = lookup x Δht:Γ ⊢ e : A⊢ Δ ⊢ e : A
        grindAll goals completed! 🐙
      exact HasType.var thisAll goals completed! 🐙
  case lam x A Γ body B hbody ih =>e:L1Γ✝:ContextA✝:Tyx:StringA:TyΓ:List (String × Ty)body:L1B:Tyhbody:(x✝, A✝) :: Γ✝ ⊢ body✝ : B✝ih:∀ {Δ : Context}, (∀ (x : String), x ∈ body✝.FV → lookup x ((x✝, A✝) :: Γ✝) = lookup x Δ) → Δ ⊢ body✝ : B✝Δ:Contexthlookup:∀ (x : String), x ∈ (L1.lam x✝ body✝).FV → lookup x Γ✝ = lookup x Δ⊢ Δ ⊢ L1.lam x✝ body✝ : A✝ ⇒ B✝
      have : ∀z ∈ L1.FV body,
          lookup z ((x, A) :: Γ) = lookup z ((x, A) :: Δ) := bye:L1Γ:ContextΔ:ContextA:Tyhlookup:∀ (x : String), x ∈ e.FV → lookup x Γ = lookup x Δht:Γ ⊢ e : A⊢ Δ ⊢ e : A
        intro z hze:L1Γ✝:ContextA✝:Tyx:StringA:TyΓ:List (String × Ty)body:L1B:Tyhbody:(x✝, A✝) :: Γ✝ ⊢ body✝ : B✝ih:∀ {Δ : Context}, (∀ (x : String), x ∈ body✝.FV → lookup x ((x✝, A✝) :: Γ✝) = lookup x Δ) → Δ ⊢ body✝ : B✝Δ:Contexthlookup:∀ (x : String), x ∈ (L1.lam x✝ body✝).FV → lookup x Γ✝ = lookup x Δz:Stringhz:z ∈ body.FV⊢ lookup z ((x, A) :: Γ) = lookup z ((x, A) :: Δ)
        by_cases z = xpose:L1Γ✝:ContextA✝:Tyx:StringA:TyΓ:List (String × Ty)body:L1B:Tyhbody:(x✝, A✝) :: Γ✝ ⊢ body✝ : B✝ih:∀ {Δ : Context}, (∀ (x : String), x ∈ body✝.FV → lookup x ((x✝, A✝) :: Γ✝) = lookup x Δ) → Δ ⊢ body✝ : B✝Δ:Contexthlookup:∀ (x : String), x ∈ (L1.lam x✝ body✝).FV → lookup x Γ✝ = lookup x Δz:Stringhz:z ∈ body.FVh✝:z = x⊢ lookup z ((x, A) :: Γ) = lookup z ((x, A) :: Δ)nege:L1Γ✝:ContextA✝:Tyx:StringA:TyΓ:List (String × Ty)body:L1B:Tyhbody:(x✝, A✝) :: Γ✝ ⊢ body✝ : B✝ih:∀ {Δ : Context}, (∀ (x : String), x ∈ body✝.FV → lookup x ((x✝, A✝) :: Γ✝) = lookup x Δ) → Δ ⊢ body✝ : B✝Δ:Contexthlookup:∀ (x : String), x ∈ (L1.lam x✝ body✝).FV → lookup x Γ✝ = lookup x Δz:Stringhz:z ∈ body.FVh✝:¬z = x⊢ lookup z ((x, A) :: Γ) = lookup z ((x, A) :: Δ)
        ·pose:L1Γ✝:ContextA✝:Tyx:StringA:TyΓ:List (String × Ty)body:L1B:Tyhbody:(x✝, A✝) :: Γ✝ ⊢ body✝ : B✝ih:∀ {Δ : Context}, (∀ (x : String), x ∈ body✝.FV → lookup x ((x✝, A✝) :: Γ✝) = lookup x Δ) → Δ ⊢ body✝ : B✝Δ:Contexthlookup:∀ (x : String), x ∈ (L1.lam x✝ body✝).FV → lookup x Γ✝ = lookup x Δz:Stringhz:z ∈ body.FVh✝:z = x⊢ lookup z ((x, A) :: Γ) = lookup z ((x, A) :: Δ) grind [lookup]All goals completed! 🐙
        ·nege:L1Γ✝:ContextA✝:Tyx:StringA:TyΓ:List (String × Ty)body:L1B:Tyhbody:(x✝, A✝) :: Γ✝ ⊢ body✝ : B✝ih:∀ {Δ : Context}, (∀ (x : String), x ∈ body✝.FV → lookup x ((x✝, A✝) :: Γ✝) = lookup x Δ) → Δ ⊢ body✝ : B✝Δ:Contexthlookup:∀ (x : String), x ∈ (L1.lam x✝ body✝).FV → lookup x Γ✝ = lookup x Δz:Stringhz:z ∈ body.FVh✝:¬z = x⊢ lookup z ((x, A) :: Γ) = lookup z ((x, A) :: Δ) have : z ∈ L1.FV (L1.lam x body) := bye:L1Γ:ContextΔ:ContextA:Tyhlookup:∀ (x : String), x ∈ e.FV → lookup x Γ = lookup x Δht:Γ ⊢ e : A⊢ Δ ⊢ e : A
            exact ⟨hz, ‹z ≠ x›⟩All goals completed! 🐙
          grind [lookup]All goals completed! 🐙
      have : (x, A) :: Δ ⊢ body : B := bye:L1Γ:ContextΔ:ContextA:Tyhlookup:∀ (x : String), x ∈ e.FV → lookup x Γ = lookup x Δht:Γ ⊢ e : A⊢ Δ ⊢ e : A
        exact ih thisAll goals completed! 🐙
      exact HasType.lam thisAll goals completed! 🐙
  case app Γ fn A B arg htfn htarg ihfn iharg =>e:L1Γ✝:ContextA✝:TyΓ:Contextfn:L1A:TyB:Tyarg:L1htfn:Γ✝ ⊢ fn✝ : A✝ ⇒ B✝htarg:Γ✝ ⊢ arg✝ : A✝ihfn:∀ {Δ : Context}, (∀ (x : String), x ∈ fn✝.FV → lookup x Γ✝ = lookup x Δ) → Δ ⊢ fn✝ : A✝ ⇒ B✝iharg:∀ {Δ : Context}, (∀ (x : String), x ∈ arg✝.FV → lookup x Γ✝ = lookup x Δ) → Δ ⊢ arg✝ : A✝Δ:Contexthlookup:∀ (x : String), x ∈ (fn✝.app arg✝).FV → lookup x Γ✝ = lookup x Δ⊢ Δ ⊢ fn✝.app arg✝ : B✝
      have : ∀z ∈ L1.FV fn, lookup z Γ = lookup z Δ := bye:L1Γ:ContextΔ:ContextA:Tyhlookup:∀ (x : String), x ∈ e.FV → lookup x Γ = lookup x Δht:Γ ⊢ e : A⊢ Δ ⊢ e : A
        intro z hze:L1Γ✝:ContextA✝:TyΓ:Contextfn:L1A:TyB:Tyarg:L1htfn:Γ✝ ⊢ fn✝ : A✝ ⇒ B✝htarg:Γ✝ ⊢ arg✝ : A✝ihfn:∀ {Δ : Context}, (∀ (x : String), x ∈ fn✝.FV → lookup x Γ✝ = lookup x Δ) → Δ ⊢ fn✝ : A✝ ⇒ B✝iharg:∀ {Δ : Context}, (∀ (x : String), x ∈ arg✝.FV → lookup x Γ✝ = lookup x Δ) → Δ ⊢ arg✝ : A✝Δ:Contexthlookup:∀ (x : String), x ∈ (fn✝.app arg✝).FV → lookup x Γ✝ = lookup x Δz:Stringhz:z ∈ fn.FV⊢ lookup z Γ = lookup z Δ
        exact hlookup z (Or.inl hz)All goals completed! 🐙
      have : Δ ⊢ fn : A ⇒ B := bye:L1Γ:ContextΔ:ContextA:Tyhlookup:∀ (x : String), x ∈ e.FV → lookup x Γ = lookup x Δht:Γ ⊢ e : A⊢ Δ ⊢ e : A
        exact ihfn thisAll goals completed! 🐙
      have : ∀z ∈ L1.FV arg, lookup z Γ = lookup z Δ := bye:L1Γ:ContextΔ:ContextA:Tyhlookup:∀ (x : String), x ∈ e.FV → lookup x Γ = lookup x Δht:Γ ⊢ e : A⊢ Δ ⊢ e : A
        intro z hze:L1Γ✝:ContextA✝:TyΓ:Contextfn:L1A:TyB:Tyarg:L1htfn:Γ✝ ⊢ fn✝ : A✝ ⇒ B✝htarg:Γ✝ ⊢ arg✝ : A✝ihfn:∀ {Δ : Context}, (∀ (x : String), x ∈ fn✝.FV → lookup x Γ✝ = lookup x Δ) → Δ ⊢ fn✝ : A✝ ⇒ B✝iharg:∀ {Δ : Context}, (∀ (x : String), x ∈ arg✝.FV → lookup x Γ✝ = lookup x Δ) → Δ ⊢ arg✝ : A✝Δ:Contexthlookup:∀ (x : String), x ∈ (fn✝.app arg✝).FV → lookup x Γ✝ = lookup x Δthis✝:∀ (z : String), z ∈ fn.FV → lookup z Γ = lookup z Δthis:Δ ⊢ fn : A ⇒ Bz:Stringhz:z ∈ arg.FV⊢ lookup z Γ = lookup z Δ
        exact hlookup z (Or.inr hz)All goals completed! 🐙
      have : Δ ⊢ arg : A := bye:L1Γ:ContextΔ:ContextA:Tyhlookup:∀ (x : String), x ∈ e.FV → lookup x Γ = lookup x Δht:Γ ⊢ e : A⊢ Δ ⊢ e : A
        exact iharg thisAll goals completed! 🐙
      exact HasType.app ‹Δ ⊢ fn : A ⇒ B› ‹Δ ⊢ arg : A›All goals completed! 🐙

theorem neutrality
  (hΓ : ∀x A B, lookup x Γ ≠ some (A ⇒ B))
  (hn : L1.Neutral e)
  (ht : Γ ⊢ e : A)
  : ∃x, e = L1.var x ∧ lookup x Γ = some A :=
byΓ:Contexte:L1A:TyhΓ:∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)hn:e.Neutralht:Γ ⊢ e : A⊢ ∃ x, e = L1.var x ∧ lookup x Γ = some A induction e generalizing Γ Avarx✝:StringΓ:ContextA:TyhΓ:∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)hn:(L1.var x✝).Neutralht:Γ ⊢ L1.var x✝ : A⊢ ∃ x, L1.var x✝ = L1.var x ∧ lookup x Γ = some Alamx✝:Stringbody✝:L1body_ih✝:∀ {Γ : Context} {A : Ty},
  (∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)) →
    body✝.Neutral → (Γ ⊢ body✝ : A) → ∃ x, body✝ = L1.var x ∧ lookup x Γ = some AΓ:ContextA:TyhΓ:∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)hn:(L1.lam x✝ body✝).Neutralht:Γ ⊢ L1.lam x✝ body✝ : A⊢ ∃ x, L1.lam x✝ body✝ = L1.var x ∧ lookup x Γ = some Aappfn✝:L1arg✝:L1fn_ih✝:∀ {Γ : Context} {A : Ty},
  (∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)) →
    fn✝.Neutral → (Γ ⊢ fn✝ : A) → ∃ x, fn✝ = L1.var x ∧ lookup x Γ = some Aarg_ih✝:∀ {Γ : Context} {A : Ty},
  (∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)) →
    arg✝.Neutral → (Γ ⊢ arg✝ : A) → ∃ x, arg✝ = L1.var x ∧ lookup x Γ = some AΓ:ContextA:TyhΓ:∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)hn:(fn✝.app arg✝).Neutralht:Γ ⊢ fn✝.app arg✝ : A⊢ ∃ x, fn✝.app arg✝ = L1.var x ∧ lookup x Γ = some A <;>varx✝:StringΓ:ContextA:TyhΓ:∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)hn:(L1.var x✝).Neutralht:Γ ⊢ L1.var x✝ : A⊢ ∃ x, L1.var x✝ = L1.var x ∧ lookup x Γ = some Alamx✝:Stringbody✝:L1body_ih✝:∀ {Γ : Context} {A : Ty},
  (∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)) →
    body✝.Neutral → (Γ ⊢ body✝ : A) → ∃ x, body✝ = L1.var x ∧ lookup x Γ = some AΓ:ContextA:TyhΓ:∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)hn:(L1.lam x✝ body✝).Neutralht:Γ ⊢ L1.lam x✝ body✝ : A⊢ ∃ x, L1.lam x✝ body✝ = L1.var x ∧ lookup x Γ = some Aappfn✝:L1arg✝:L1fn_ih✝:∀ {Γ : Context} {A : Ty},
  (∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)) →
    fn✝.Neutral → (Γ ⊢ fn✝ : A) → ∃ x, fn✝ = L1.var x ∧ lookup x Γ = some Aarg_ih✝:∀ {Γ : Context} {A : Ty},
  (∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)) →
    arg✝.Neutral → (Γ ⊢ arg✝ : A) → ∃ x, arg✝ = L1.var x ∧ lookup x Γ = some AΓ:ContextA:TyhΓ:∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)hn:(fn✝.app arg✝).Neutralht:Γ ⊢ fn✝.app arg✝ : A⊢ ∃ x, fn✝.app arg✝ = L1.var x ∧ lookup x Γ = some A cases hnapp.appfn✝:L1arg✝:L1fn_ih✝:∀ {Γ : Context} {A : Ty},
  (∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)) →
    fn✝.Neutral → (Γ ⊢ fn✝ : A) → ∃ x, fn✝ = L1.var x ∧ lookup x Γ = some Aarg_ih✝:∀ {Γ : Context} {A : Ty},
  (∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)) →
    arg✝.Neutral → (Γ ⊢ arg✝ : A) → ∃ x, arg✝ = L1.var x ∧ lookup x Γ = some AΓ:ContextA:TyhΓ:∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)ht:Γ ⊢ fn✝.app arg✝ : Aa✝¹:fn✝.Neutrala✝:arg✝.Normal⊢ ∃ x, fn✝.app arg✝ = L1.var x ∧ lookup x Γ = some A <;>var.varx✝:StringΓ:ContextA:TyhΓ:∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)ht:Γ ⊢ L1.var x✝ : A⊢ ∃ x, L1.var x✝ = L1.var x ∧ lookup x Γ = some Aapp.appfn✝:L1arg✝:L1fn_ih✝:∀ {Γ : Context} {A : Ty},
  (∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)) →
    fn✝.Neutral → (Γ ⊢ fn✝ : A) → ∃ x, fn✝ = L1.var x ∧ lookup x Γ = some Aarg_ih✝:∀ {Γ : Context} {A : Ty},
  (∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)) →
    arg✝.Neutral → (Γ ⊢ arg✝ : A) → ∃ x, arg✝ = L1.var x ∧ lookup x Γ = some AΓ:ContextA:TyhΓ:∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)ht:Γ ⊢ fn✝.app arg✝ : Aa✝¹:fn✝.Neutrala✝:arg✝.Normal⊢ ∃ x, fn✝.app arg✝ = L1.var x ∧ lookup x Γ = some A cases htapp.app.appfn✝:L1arg✝:L1fn_ih✝:∀ {Γ : Context} {A : Ty},
  (∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)) →
    fn✝.Neutral → (Γ ⊢ fn✝ : A) → ∃ x, fn✝ = L1.var x ∧ lookup x Γ = some Aarg_ih✝:∀ {Γ : Context} {A : Ty},
  (∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)) →
    arg✝.Neutral → (Γ ⊢ arg✝ : A) → ∃ x, arg✝ = L1.var x ∧ lookup x Γ = some AΓ:ContextA:TyhΓ:∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)a✝³:fn✝.Neutrala✝²:arg✝.NormalA✝:Tya✝¹:Γ ⊢ arg✝ : A✝a✝:Γ ⊢ fn✝ : A✝ ⇒ A⊢ ∃ x, fn✝.app arg✝ = L1.var x ∧ lookup x Γ = some A <;>var.var.varx✝:StringΓ:ContextA:TyhΓ:∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)a✝:lookup x✝ Γ = some A⊢ ∃ x, L1.var x✝ = L1.var x ∧ lookup x Γ = some Aapp.app.appfn✝:L1arg✝:L1fn_ih✝:∀ {Γ : Context} {A : Ty},
  (∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)) →
    fn✝.Neutral → (Γ ⊢ fn✝ : A) → ∃ x, fn✝ = L1.var x ∧ lookup x Γ = some Aarg_ih✝:∀ {Γ : Context} {A : Ty},
  (∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)) →
    arg✝.Neutral → (Γ ⊢ arg✝ : A) → ∃ x, arg✝ = L1.var x ∧ lookup x Γ = some AΓ:ContextA:TyhΓ:∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)a✝³:fn✝.Neutrala✝²:arg✝.NormalA✝:Tya✝¹:Γ ⊢ arg✝ : A✝a✝:Γ ⊢ fn✝ : A✝ ⇒ A⊢ ∃ x, fn✝.app arg✝ = L1.var x ∧ lookup x Γ = some A grindAll goals completed! 🐙

theorem normal_arrow_is_lam
  (hΓ : ∀x A B, lookup x Γ ≠ some (A ⇒ B))
  (hn : L1.Normal e)
  (ht : Γ ⊢ e : A ⇒ B)
  : ∃x body, e = L1.lam x body ∧ L1.Normal body ∧ ((x, A) :: Γ) ⊢ body : B :=
byΓ:Contexte:L1A:TyB:TyhΓ:∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)hn:e.Normalht:Γ ⊢ e : A ⇒ B⊢ ∃ x body, e = L1.lam x body ∧ body.Normal ∧ (x, A) :: Γ ⊢ body : B
  have            : ¬ L1.Neutral e                := byΓ:Contexte:L1A:TyB:TyhΓ:∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)hn:e.Normalht:Γ ⊢ e : A ⇒ B⊢ ∃ x body, e = L1.lam x body ∧ body.Normal ∧ (x, A) :: Γ ⊢ body : B grind [neutrality]All goals completed! 🐙
  obtain_by x b   : e = L1.lam x b ∧ L1.Normal b  := byΓ:Contexte:L1A:TyB:TyhΓ:∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)hn:e.Normalht:Γ ⊢ e : A ⇒ Bthis:¬e.Neutral⊢ ∃ x b, e = L1.lam x b ∧ b.Normal cases hnlamΓ:ContextA:TyB:TyhΓ:∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)body:L1x:Stringa:body.Normalht:Γ ⊢ L1.lam x body : A ⇒ Bthis:¬(L1.lam x body).Neutral⊢ ∃ x_1 b, L1.lam x body = L1.lam x_1 b ∧ b.NormalneutralΓ:Contexte:L1A:TyB:TyhΓ:∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)ht:Γ ⊢ e : A ⇒ Bthis:¬e.Neutrala:e.Neutral⊢ ∃ x b, e = L1.lam x b ∧ b.Normal <;>lamΓ:ContextA:TyB:TyhΓ:∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)body:L1x:Stringa:body.Normalht:Γ ⊢ L1.lam x body : A ⇒ Bthis:¬(L1.lam x body).Neutral⊢ ∃ x_1 b, L1.lam x body = L1.lam x_1 b ∧ b.NormalneutralΓ:Contexte:L1A:TyB:TyhΓ:∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)ht:Γ ⊢ e : A ⇒ Bthis:¬e.Neutrala:e.Neutral⊢ ∃ x b, e = L1.lam x b ∧ b.Normal grindAll goals completed! 🐙
  have            : ((x, A) :: Γ) ⊢ b : B         := byΓ:Contexte:L1A:TyB:TyhΓ:∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)hn:e.Normalht:Γ ⊢ e : A ⇒ B⊢ ∃ x body, e = L1.lam x body ∧ body.Normal ∧ (x, A) :: Γ ⊢ body : B cases htvarΓ:ContextA:TyB:TyhΓ:∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)x:Stringb:L1h1:b.Normalx✝:Stringhn:(L1.var x✝).Normalthis:¬(L1.var x✝).Neutralh0:L1.var x✝ = L1.lam x ba✝:lookup x✝ Γ = some (A ⇒ B)⊢ (x, A) :: Γ ⊢ b : BlamΓ:ContextA:TyB:TyhΓ:∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)x:Stringb:L1h1:b.Normalx✝:Stringbody✝:L1hn:(L1.lam x✝ body✝).Normalthis:¬(L1.lam x✝ body✝).Neutralh0:L1.lam x✝ body✝ = L1.lam x ba✝:(x✝, A) :: Γ ⊢ body✝ : B⊢ (x, A) :: Γ ⊢ b : BappΓ:ContextA:TyB:TyhΓ:∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)x:Stringb:L1h1:b.Normalfn✝:L1A✝:Tyarg✝:L1a✝¹:Γ ⊢ arg✝ : A✝hn:(fn✝.app arg✝).Normalthis:¬(fn✝.app arg✝).Neutralh0:fn✝.app arg✝ = L1.lam x ba✝:Γ ⊢ fn✝ : A✝ ⇒ A ⇒ B⊢ (x, A) :: Γ ⊢ b : B <;>varΓ:ContextA:TyB:TyhΓ:∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)x:Stringb:L1h1:b.Normalx✝:Stringhn:(L1.var x✝).Normalthis:¬(L1.var x✝).Neutralh0:L1.var x✝ = L1.lam x ba✝:lookup x✝ Γ = some (A ⇒ B)⊢ (x, A) :: Γ ⊢ b : BlamΓ:ContextA:TyB:TyhΓ:∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)x:Stringb:L1h1:b.Normalx✝:Stringbody✝:L1hn:(L1.lam x✝ body✝).Normalthis:¬(L1.lam x✝ body✝).Neutralh0:L1.lam x✝ body✝ = L1.lam x ba✝:(x✝, A) :: Γ ⊢ body✝ : B⊢ (x, A) :: Γ ⊢ b : BappΓ:ContextA:TyB:TyhΓ:∀ (x : String) (A B : Ty), lookup x Γ ≠ some (A ⇒ B)x:Stringb:L1h1:b.Normalfn✝:L1A✝:Tyarg✝:L1a✝¹:Γ ⊢ arg✝ : A✝hn:(fn✝.app arg✝).Normalthis:¬(fn✝.app arg✝).Neutralh0:fn✝.app arg✝ = L1.lam x ba✝:Γ ⊢ fn✝ : A✝ ⇒ A ⇒ B⊢ (x, A) :: Γ ⊢ b : B grindAll goals completed! 🐙
  exists x, bAll goals completed! 🐙

theorem boolean_normal_forms
  (hc : L1.Closed e)
  (hn : L1.Normal e)
  (ht : Γ ⊢ e : #α ⇒ #α ⇒ #α)
  : (e =α₁ L1.T) ∨ (e =α₁ L1.F)
:= bye:L1Γ:Contexthc:e.Closedhn:e.Normalht:Γ ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"⊢ e =α₁ L1.T ∨ e =α₁ L1.F
  have : [] ⊢ e : #α ⇒ #α ⇒ #α
  := bye:L1Γ:Contexthc:e.Closedhn:e.Normalht:Γ ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"⊢ e =α₁ L1.T ∨ e =α₁ L1.F grind [typing_independent_of_context, L1.Closed, L1.FV, L0.Closed]All goals completed! 🐙

  obtain_by x y e₂ : e = L1[λ{x}. λ{y}. {e₂}] ∧ L1.Normal e₂ ∧ [(y, #α), (x, #α)] ⊢ e₂ : #α
  := bye:L1Γ:Contexthc:e.Closedhn:e.Normalht:Γ ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"this:[] ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"⊢ ∃ x y e₂, e = L1.lam x (L1.lam y e₂) ∧ e₂.Normal ∧ [(y, Ty.base "α"), (x, Ty.base "α")] ⊢ e₂ : Ty.base "α" grind [normal_arrow_is_lam, lookup]All goals completed! 🐙

  have : L1.Neutral e₂
  := bye:L1Γ:Contexthc:e.Closedhn:e.Normalht:Γ ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"⊢ e =α₁ L1.T ∨ e =α₁ L1.F cases ‹[(y, #α), (x, #α)] ⊢ e₂ : #α›vare:L1Γ:Contexthc:e.Closedhn:e.Normalht:Γ ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"this:[] ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"x:Stringy:Stringx✝:Stringh0:e = L1.lam x (L1.lam y (L1.var x✝))h1:(L1.var x✝).Normala✝:lookup x✝ [(y, Ty.base "α"), (x, Ty.base "α")] = some (Ty.base "α")⊢ (L1.var x✝).Neutralappe:L1Γ:Contexthc:e.Closedhn:e.Normalht:Γ ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"this:[] ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"x:Stringy:Stringfn✝:L1A✝:Tyarg✝:L1a✝¹:[(y, Ty.base "α"), (x, Ty.base "α")] ⊢ arg✝ : A✝h0:e = L1.lam x (L1.lam y (fn✝.app arg✝))h1:(fn✝.app arg✝).Normala✝:[(y, Ty.base "α"), (x, Ty.base "α")] ⊢ fn✝ : A✝ ⇒ Ty.base "α"⊢ (fn✝.app arg✝).Neutral <;>vare:L1Γ:Contexthc:e.Closedhn:e.Normalht:Γ ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"this:[] ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"x:Stringy:Stringx✝:Stringh0:e = L1.lam x (L1.lam y (L1.var x✝))h1:(L1.var x✝).Normala✝:lookup x✝ [(y, Ty.base "α"), (x, Ty.base "α")] = some (Ty.base "α")⊢ (L1.var x✝).Neutralappe:L1Γ:Contexthc:e.Closedhn:e.Normalht:Γ ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"this:[] ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"x:Stringy:Stringfn✝:L1A✝:Tyarg✝:L1a✝¹:[(y, Ty.base "α"), (x, Ty.base "α")] ⊢ arg✝ : A✝h0:e = L1.lam x (L1.lam y (fn✝.app arg✝))h1:(fn✝.app arg✝).Normala✝:[(y, Ty.base "α"), (x, Ty.base "α")] ⊢ fn✝ : A✝ ⇒ Ty.base "α"⊢ (fn✝.app arg✝).Neutral cases ‹L1.Normal _›app.neutrale:L1Γ:Contexthc:e.Closedhn:e.Normalht:Γ ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"this:[] ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"x:Stringy:Stringfn✝:L1A✝:Tyarg✝:L1a✝²:[(y, Ty.base "α"), (x, Ty.base "α")] ⊢ arg✝ : A✝h0:e = L1.lam x (L1.lam y (fn✝.app arg✝))a✝¹:[(y, Ty.base "α"), (x, Ty.base "α")] ⊢ fn✝ : A✝ ⇒ Ty.base "α"a✝:(fn✝.app arg✝).Neutral⊢ (fn✝.app arg✝).Neutral <;>var.neutrale:L1Γ:Contexthc:e.Closedhn:e.Normalht:Γ ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"this:[] ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"x:Stringy:Stringx✝:Stringh0:e = L1.lam x (L1.lam y (L1.var x✝))a✝¹:lookup x✝ [(y, Ty.base "α"), (x, Ty.base "α")] = some (Ty.base "α")a✝:(L1.var x✝).Neutral⊢ (L1.var x✝).Neutralapp.neutrale:L1Γ:Contexthc:e.Closedhn:e.Normalht:Γ ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"this:[] ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"x:Stringy:Stringfn✝:L1A✝:Tyarg✝:L1a✝²:[(y, Ty.base "α"), (x, Ty.base "α")] ⊢ arg✝ : A✝h0:e = L1.lam x (L1.lam y (fn✝.app arg✝))a✝¹:[(y, Ty.base "α"), (x, Ty.base "α")] ⊢ fn✝ : A✝ ⇒ Ty.base "α"a✝:(fn✝.app arg✝).Neutral⊢ (fn✝.app arg✝).Neutral assumptionAll goals completed! 🐙

  obtain_by z : e₂ = L1.var z ∧ lookup z [(y, #α), (x, #α)] = some #α
  := bye:L1Γ:Contexthc:e.Closedhn:e.Normalht:Γ ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"this✝:[] ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"x:Stringy:Stringe₂:L1h0:e = L1.lam x (L1.lam y e₂)h1:e₂.Normalh2:[(y, Ty.base "α"), (x, Ty.base "α")] ⊢ e₂ : Ty.base "α"this:e₂.Neutral⊢ ∃ z, e₂ = L1.var z ∧ lookup z [(y, Ty.base "α"), (x, Ty.base "α")] = some (Ty.base "α") grind [neutrality, lookup]All goals completed! 🐙

  cases_or : (z = x) ∨ (z = y) := bye:L1Γ:Contexthc:e.Closedhn:e.Normalht:Γ ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"⊢ e =α₁ L1.T ∨ e =α₁ L1.F grind [lookup]All goals completed! 🐙
  | inl =>
      by_cases x = ypose:L1Γ:Contexthc:e.Closedhn:e.Normalht:Γ ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"this✝:[] ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"x:Stringy:Stringe₂:L1h0✝:e = L1.lam x (L1.lam y e₂)h1✝:e₂.Normalh2:[(y, Ty.base "α"), (x, Ty.base "α")] ⊢ e₂ : Ty.base "α"this:e₂.Neutralz:Stringh0:e₂ = L1.var zh1:lookup z [(y, Ty.base "α"), (x, Ty.base "α")] = some (Ty.base "α")h✝¹:z = xh✝:x = y⊢ e =α₁ L1.T ∨ e =α₁ L1.Fnege:L1Γ:Contexthc:e.Closedhn:e.Normalht:Γ ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"this✝:[] ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"x:Stringy:Stringe₂:L1h0✝:e = L1.lam x (L1.lam y e₂)h1✝:e₂.Normalh2:[(y, Ty.base "α"), (x, Ty.base "α")] ⊢ e₂ : Ty.base "α"this:e₂.Neutralz:Stringh0:e₂ = L1.var zh1:lookup z [(y, Ty.base "α"), (x, Ty.base "α")] = some (Ty.base "α")h✝¹:z = xh✝:¬x = y⊢ e =α₁ L1.T ∨ e =α₁ L1.F
      ·pose:L1Γ:Contexthc:e.Closedhn:e.Normalht:Γ ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"this✝:[] ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"x:Stringy:Stringe₂:L1h0✝:e = L1.lam x (L1.lam y e₂)h1✝:e₂.Normalh2:[(y, Ty.base "α"), (x, Ty.base "α")] ⊢ e₂ : Ty.base "α"this:e₂.Neutralz:Stringh0:e₂ = L1.var zh1:lookup z [(y, Ty.base "α"), (x, Ty.base "α")] = some (Ty.base "α")h✝¹:z = xh✝:x = y⊢ e =α₁ L1.T ∨ e =α₁ L1.F rightpose:L1Γ:Contexthc:e.Closedhn:e.Normalht:Γ ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"this✝:[] ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"x:Stringy:Stringe₂:L1h0✝:e = L1.lam x (L1.lam y e₂)h1✝:e₂.Normalh2:[(y, Ty.base "α"), (x, Ty.base "α")] ⊢ e₂ : Ty.base "α"this:e₂.Neutralz:Stringh0:e₂ = L1.var zh1:lookup z [(y, Ty.base "α"), (x, Ty.base "α")] = some (Ty.base "α")h✝¹:z = xh✝:x = y⊢ e =α₁ L1.F; unfold L1.Fpose:L1Γ:Contexthc:e.Closedhn:e.Normalht:Γ ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"this✝:[] ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"x:Stringy:Stringe₂:L1h0✝:e = L1.lam x (L1.lam y e₂)h1✝:e₂.Normalh2:[(y, Ty.base "α"), (x, Ty.base "α")] ⊢ e₂ : Ty.base "α"this:e₂.Neutralz:Stringh0:e₂ = L1.var zh1:lookup z [(y, Ty.base "α"), (x, Ty.base "α")] = some (Ty.base "α")h✝¹:z = xh✝:x = y⊢ e =α₁ L1.lam "x" (L1.lam "y" (L1.var "y")); alpha_eqAll goals completed! 🐙
      ·nege:L1Γ:Contexthc:e.Closedhn:e.Normalht:Γ ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"this✝:[] ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"x:Stringy:Stringe₂:L1h0✝:e = L1.lam x (L1.lam y e₂)h1✝:e₂.Normalh2:[(y, Ty.base "α"), (x, Ty.base "α")] ⊢ e₂ : Ty.base "α"this:e₂.Neutralz:Stringh0:e₂ = L1.var zh1:lookup z [(y, Ty.base "α"), (x, Ty.base "α")] = some (Ty.base "α")h✝¹:z = xh✝:¬x = y⊢ e =α₁ L1.T ∨ e =α₁ L1.F leftnege:L1Γ:Contexthc:e.Closedhn:e.Normalht:Γ ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"this✝:[] ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"x:Stringy:Stringe₂:L1h0✝:e = L1.lam x (L1.lam y e₂)h1✝:e₂.Normalh2:[(y, Ty.base "α"), (x, Ty.base "α")] ⊢ e₂ : Ty.base "α"this:e₂.Neutralz:Stringh0:e₂ = L1.var zh1:lookup z [(y, Ty.base "α"), (x, Ty.base "α")] = some (Ty.base "α")h✝¹:z = xh✝:¬x = y⊢ e =α₁ L1.T; unfold L1.Tnege:L1Γ:Contexthc:e.Closedhn:e.Normalht:Γ ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"this✝:[] ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"x:Stringy:Stringe₂:L1h0✝:e = L1.lam x (L1.lam y e₂)h1✝:e₂.Normalh2:[(y, Ty.base "α"), (x, Ty.base "α")] ⊢ e₂ : Ty.base "α"this:e₂.Neutralz:Stringh0:e₂ = L1.var zh1:lookup z [(y, Ty.base "α"), (x, Ty.base "α")] = some (Ty.base "α")h✝¹:z = xh✝:¬x = y⊢ e =α₁ L1.lam "x" (L1.lam "y" (L1.var "x")); alpha_eqAll goals completed! 🐙
  | inr =>
      rightinre:L1Γ:Contexthc:e.Closedhn:e.Normalht:Γ ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"this✝:[] ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"x:Stringy:Stringe₂:L1h0✝:e = L1.lam x (L1.lam y e₂)h1✝:e₂.Normalh2:[(y, Ty.base "α"), (x, Ty.base "α")] ⊢ e₂ : Ty.base "α"this:e₂.Neutralz:Stringh0:e₂ = L1.var zh1:lookup z [(y, Ty.base "α"), (x, Ty.base "α")] = some (Ty.base "α")h✝:z = y⊢ e =α₁ L1.F; unfold L1.Finre:L1Γ:Contexthc:e.Closedhn:e.Normalht:Γ ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"this✝:[] ⊢ e : Ty.base "α" ⇒ Ty.base "α" ⇒ Ty.base "α"x:Stringy:Stringe₂:L1h0✝:e = L1.lam x (L1.lam y e₂)h1✝:e₂.Normalh2:[(y, Ty.base "α"), (x, Ty.base "α")] ⊢ e₂ : Ty.base "α"this:e₂.Neutralz:Stringh0:e₂ = L1.var zh1:lookup z [(y, Ty.base "α"), (x, Ty.base "α")] = some (Ty.base "α")h✝:z = y⊢ e =α₁ L1.lam "x" (L1.lam "y" (L1.var "y")); alpha_eqAll goals completed! 🐙

theorem progress_in
  (ht : Γ ⊢ e : A)
  : L1.Normal e ∨ L1.ReducibleIn ρ e :=
byΓ:Contexte:L1A:Tyρ:List Stringht:Γ ⊢ e : A⊢ e.Normal ∨ L1.ReducibleIn ρ e
  induction ht generalizing ρvarΓ:Contexte:L1A:Tyx✝:StringΓ✝:ContextA✝:Tya✝:lookup x✝ Γ✝ = some A✝ρ:List String⊢ (L1.var x✝).Normal ∨ L1.ReducibleIn ρ (L1.var x✝)lamΓ:Contexte:L1A:Tyx✝:StringA✝:TyΓ✝:List (String × Ty)body✝:L1B✝:Tya✝:(x✝, A✝) :: Γ✝ ⊢ body✝ : B✝a_ih✝:∀ {ρ : List String}, body✝.Normal ∨ L1.ReducibleIn ρ body✝ρ:List String⊢ (L1.lam x✝ body✝).Normal ∨ L1.ReducibleIn ρ (L1.lam x✝ body✝)appΓ:Contexte:L1A:TyΓ✝:Contextfn✝:L1A✝:TyB✝:Tyarg✝:L1a✝¹:Γ✝ ⊢ fn✝ : A✝ ⇒ B✝a✝:Γ✝ ⊢ arg✝ : A✝a_ih✝¹:∀ {ρ : List String}, fn✝.Normal ∨ L1.ReducibleIn ρ fn✝a_ih✝:∀ {ρ : List String}, arg✝.Normal ∨ L1.ReducibleIn ρ arg✝ρ:List String⊢ (fn✝.app arg✝).Normal ∨ L1.ReducibleIn ρ (fn✝.app arg✝)
  case var x _ _ _ =>Γ:Contexte:L1A:Tyx:StringΓ✝:ContextA✝:Tya✝:lookup x✝ Γ✝ = some A✝ρ:List String⊢ (L1.var x✝).Normal ∨ L1.ReducibleIn ρ (L1.var x✝)
      have : L1.Normal (L1.var x) := byΓ:Contexte:L1A:Tyρ:List Stringht:Γ ⊢ e : A⊢ e.Normal ∨ L1.ReducibleIn ρ e solve_by_elim [L1.Normal.neutral, L1.Neutral.var]All goals completed! 🐙
      grindAll goals completed! 🐙
  case lam x _ _ body _ _ ih =>Γ:Contexte:L1A:Tyx:StringA✝:TyΓ✝:List (String × Ty)body:L1B✝:Tya✝:(x✝, A✝) :: Γ✝ ⊢ body✝ : B✝ih:∀ {ρ : List String}, body✝.Normal ∨ L1.ReducibleIn ρ body✝ρ:List String⊢ (L1.lam x✝ body✝).Normal ∨ L1.ReducibleIn ρ (L1.lam x✝ body✝)
      cases_or : (L1.Normal body) ∨ (L1.ReducibleIn (x :: ρ) body) := byΓ:Contexte:L1A:Tyρ:List Stringht:Γ ⊢ e : A⊢ e.Normal ∨ L1.ReducibleIn ρ e grindAll goals completed! 🐙
      | inl =>Γ:Contexte:L1A:Tyx:StringA✝:TyΓ✝:List (String × Ty)body:L1B✝:Tya✝:(x✝, A✝) :: Γ✝ ⊢ body✝ : B✝ih:∀ {ρ : List String}, body✝.Normal ∨ L1.ReducibleIn ρ body✝ρ:List String⊢ (L1.lam x✝ body✝).Normal ∨ L1.ReducibleIn ρ (L1.lam x✝ body✝)
        have : L1.Normal (L1.lam x body) := byΓ:Contexte:L1A:Tyρ:List Stringht:Γ ⊢ e : A⊢ e.Normal ∨ L1.ReducibleIn ρ e solve_by_elim [L1.Normal.lam]All goals completed! 🐙
        grindAll goals completed! 🐙
      | inr =>Γ:Contexte:L1A:Tyx:StringA✝:TyΓ✝:List (String × Ty)body:L1B✝:Tya✝:(x✝, A✝) :: Γ✝ ⊢ body✝ : B✝ih:∀ {ρ : List String}, body✝.Normal ∨ L1.ReducibleIn ρ body✝ρ:List String⊢ (L1.lam x✝ body✝).Normal ∨ L1.ReducibleIn ρ (L1.lam x✝ body✝)
        have : L1.ReducibleIn ρ (L1.lam x body) := byΓ:Contexte:L1A:Tyρ:List Stringht:Γ ⊢ e : A⊢ e.Normal ∨ L1.ReducibleIn ρ e
          simp_all [L1.ReducibleIn, L1.toL0With]Γ:Contexte:L1A:Tyx:StringA✝:TyΓ✝:List (String × Ty)body:L1B✝:Tya✝:(x✝, A✝) :: Γ✝ ⊢ body✝ : B✝ρ:List Stringih:∀ {ρ : List String}, body.Normal ∨ ∃ e', L1.toL0With ρ body →β₀ e'h✝:∃ e', L1.toL0With (x :: ρ) body →β₀ e'⊢ ∃ e', (L1.toL0With (x :: ρ) body).lam →β₀ e'
          aesop (add safe constructors Exists, safe constructors L0.BetaStep)All goals completed! 🐙
        grindAll goals completed! 🐙
  case app _ fn _ _ arg _ _ ihfn iharg =>Γ:Contexte:L1A:TyΓ✝:Contextfn:L1A✝:TyB✝:Tyarg:L1a✝¹:Γ✝ ⊢ fn✝ : A✝ ⇒ B✝a✝:Γ✝ ⊢ arg✝ : A✝ihfn:∀ {ρ : List String}, fn✝.Normal ∨ L1.ReducibleIn ρ fn✝iharg:∀ {ρ : List String}, arg✝.Normal ∨ L1.ReducibleIn ρ arg✝ρ:List String⊢ (fn✝.app arg✝).Normal ∨ L1.ReducibleIn ρ (fn✝.app arg✝)
      cases_or : (L1.Normal fn) ∨ (L1.ReducibleIn ρ fn) := byΓ:Contexte:L1A:Tyρ:List Stringht:Γ ⊢ e : A⊢ e.Normal ∨ L1.ReducibleIn ρ e grindAll goals completed! 🐙
      | inl =>Γ:Contexte:L1A:TyΓ✝:Contextfn:L1A✝:TyB✝:Tyarg:L1a✝¹:Γ✝ ⊢ fn✝ : A✝ ⇒ B✝a✝:Γ✝ ⊢ arg✝ : A✝ihfn:∀ {ρ : List String}, fn✝.Normal ∨ L1.ReducibleIn ρ fn✝iharg:∀ {ρ : List String}, arg✝.Normal ∨ L1.ReducibleIn ρ arg✝ρ:List String⊢ (fn✝.app arg✝).Normal ∨ L1.ReducibleIn ρ (fn✝.app arg✝)
        cases_or : (L1.Normal arg) ∨ (L1.ReducibleIn ρ arg) := byΓ:Contexte:L1A:Tyρ:List Stringht:Γ ⊢ e : A⊢ e.Normal ∨ L1.ReducibleIn ρ e grindAll goals completed! 🐙
        | inl =>Γ:Contexte:L1A:TyΓ✝:Contextfn:L1A✝:TyB✝:Tyarg:L1a✝¹:Γ✝ ⊢ fn✝ : A✝ ⇒ B✝a✝:Γ✝ ⊢ arg✝ : A✝ihfn:∀ {ρ : List String}, fn✝.Normal ∨ L1.ReducibleIn ρ fn✝iharg:∀ {ρ : List String}, arg✝.Normal ∨ L1.ReducibleIn ρ arg✝ρ:List String⊢ (fn✝.app arg✝).Normal ∨ L1.ReducibleIn ρ (fn✝.app arg✝)
          cases ‹L1.Normal fn› with
          | neutral =>inl.inl.neutralΓ:Contexte:L1A:TyΓ✝:Contextfn:L1A✝:TyB✝:Tyarg:L1a✝²:Γ✝ ⊢ fn✝ : A✝ ⇒ B✝a✝¹:Γ✝ ⊢ arg✝ : A✝ihfn:∀ {ρ : List String}, fn✝.Normal ∨ L1.ReducibleIn ρ fn✝iharg:∀ {ρ : List String}, arg✝.Normal ∨ L1.ReducibleIn ρ arg✝ρ:List Stringh✝:arg.Normala✝:fn.Neutral⊢ (fn.app arg).Normal ∨ L1.ReducibleIn ρ (fn.app arg)
              have : L1.Normal (L1.app fn arg) := byΓ:Contexte:L1A:Tyρ:List Stringht:Γ ⊢ e : A⊢ e.Normal ∨ L1.ReducibleIn ρ e
                solve_by_elim [L1.Normal.neutral, L1.Neutral.app]All goals completed! 🐙
              grindAll goals completed! 🐙
          | @lam b x nb =>inl.inl.lamΓ:Contexte:L1A:TyΓ✝:ContextA✝:TyB✝:Tyarg:L1a✝¹:Γ✝ ⊢ arg✝ : A✝iharg:∀ {ρ : List String}, arg✝.Normal ∨ L1.ReducibleIn ρ arg✝ρ:List Stringh✝:arg.Normalb:L1x:Stringnb:b.Normala✝:Γ✝ ⊢ L1.lam x b : A✝ ⇒ B✝ihfn:∀ {ρ : List String}, (L1.lam x b).Normal ∨ L1.ReducibleIn ρ (L1.lam x b)⊢ ((L1.lam x b).app arg).Normal ∨ L1.ReducibleIn ρ ((L1.lam x b).app arg)
              have : L1.ReducibleIn ρ ((L1.lam x b).app arg) := byΓ:Contexte:L1A:Tyρ:List Stringht:Γ ⊢ e : A⊢ e.Normal ∨ L1.ReducibleIn ρ e
                simp_all [L1.ReducibleIn, L1.toL0With]Γ:Contexte:L1A:TyΓ✝:ContextA✝:TyB✝:Tyarg:L1a✝¹:Γ✝ ⊢ arg✝ : A✝ρ:List Stringh✝:arg.Normalb:L1x:Stringnb:b.Normala✝:Γ✝ ⊢ L1.lam x b : A✝ ⇒ B✝ihfn:∀ {ρ : List String}, (L1.lam x b).Normal ∨ ∃ e', (L1.toL0With (x :: ρ) b).lam →β₀ e'⊢ ∃ e', (L1.toL0With (x :: ρ) b).lam.app (L1.toL0With ρ arg) →β₀ e'
                aesop (add safe constructors Exists, safe apply L0.BetaStep.beta)All goals completed! 🐙
              grindAll goals completed! 🐙
        | inr =>Γ:Contexte:L1A:TyΓ✝:Contextfn:L1A✝:TyB✝:Tyarg:L1a✝¹:Γ✝ ⊢ fn✝ : A✝ ⇒ B✝a✝:Γ✝ ⊢ arg✝ : A✝ihfn:∀ {ρ : List String}, fn✝.Normal ∨ L1.ReducibleIn ρ fn✝iharg:∀ {ρ : List String}, arg✝.Normal ∨ L1.ReducibleIn ρ arg✝ρ:List String⊢ (fn✝.app arg✝).Normal ∨ L1.ReducibleIn ρ (fn✝.app arg✝)
          have : L1.ReducibleIn ρ (L1.app fn arg) := byΓ:Contexte:L1A:Tyρ:List Stringht:Γ ⊢ e : A⊢ e.Normal ∨ L1.ReducibleIn ρ e
            simp_all [L1.ReducibleIn, L1.toL0With]Γ:Contexte:L1A:TyΓ✝:Contextfn:L1A✝:TyB✝:Tyarg:L1a✝¹:Γ✝ ⊢ fn✝ : A✝ ⇒ B✝a✝:Γ✝ ⊢ arg✝ : A✝ρ:List Stringiharg:∀ {ρ : List String}, arg.Normal ∨ ∃ e', L1.toL0With ρ arg →β₀ e'h✝¹:fn.Normalh✝:∃ e', L1.toL0With ρ arg →β₀ e'⊢ ∃ e', (L1.toL0With ρ fn).app (L1.toL0With ρ arg) →β₀ e'
            aesop (add safe constructors Exists, safe apply L0.BetaStep.app_right)All goals completed! 🐙
          grindAll goals completed! 🐙
      | inr =>Γ:Contexte:L1A:TyΓ✝:Contextfn:L1A✝:TyB✝:Tyarg:L1a✝¹:Γ✝ ⊢ fn✝ : A✝ ⇒ B✝a✝:Γ✝ ⊢ arg✝ : A✝ihfn:∀ {ρ : List String}, fn✝.Normal ∨ L1.ReducibleIn ρ fn✝iharg:∀ {ρ : List String}, arg✝.Normal ∨ L1.ReducibleIn ρ arg✝ρ:List String⊢ (fn✝.app arg✝).Normal ∨ L1.ReducibleIn ρ (fn✝.app arg✝)
        have : L1.ReducibleIn ρ (L1.app fn arg) := byΓ:Contexte:L1A:Tyρ:List Stringht:Γ ⊢ e : A⊢ e.Normal ∨ L1.ReducibleIn ρ e
          simp_all [L1.ReducibleIn, L1.toL0With]Γ:Contexte:L1A:TyΓ✝:Contextfn:L1A✝:TyB✝:Tyarg:L1a✝¹:Γ✝ ⊢ fn✝ : A✝ ⇒ B✝a✝:Γ✝ ⊢ arg✝ : A✝ρ:List Stringihfn:∀ {ρ : List String}, fn.Normal ∨ ∃ e', L1.toL0With ρ fn →β₀ e'iharg:∀ {ρ : List String}, arg.Normal ∨ ∃ e', L1.toL0With ρ arg →β₀ e'h✝:∃ e', L1.toL0With ρ fn →β₀ e'⊢ ∃ e', (L1.toL0With ρ fn).app (L1.toL0With ρ arg) →β₀ e'
          aesop (add safe constructors Exists, safe apply L0.BetaStep.app_left)All goals completed! 🐙
        grindAll goals completed! 🐙

end L2