Theorem: LambdaCalculi.hasType_of_append_hasType (LambdaCalculi/HasType.lean)

State before:
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ Δ : Context p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
h : Γ ++ Δ ⊢[T] t ∶ σ
ht : LambdaTerm.freeVarRange t ≤ List.length Γ
⊢ Γ ⊢[T] t ∶ σ
Tactic:
induction t generalizing Γ σ
State after:
case const
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝ : C✝
Γ : Context p✝ U✝
σ : LambdaType p✝ U✝
h : Γ ++ Δ ⊢[T] LambdaTerm.const a✝ ∶ σ
ht : LambdaTerm.freeVarRange (LambdaTerm.const a✝) ≤ List.length Γ
⊢ Γ ⊢[T] LambdaTerm.const a✝ ∶ σ

case var
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝ : ℕ
Γ : Context p✝ U✝
σ : LambdaType p✝ U✝
h : Γ ++ Δ ⊢[T] LambdaTerm.var a✝ ∶ σ
ht : LambdaTerm.freeVarRange (LambdaTerm.var a✝) ≤ List.length Γ
⊢ Γ ⊢[T] LambdaTerm.var a✝ ∶ σ

case lambda
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝² : p✝.lambda = true
a✝¹ : LambdaType p✝ U✝
a✝ : LambdaTerm p✝ U✝ C✝
a_ih✝ :
  ∀ {Γ : Context p✝ U✝} {σ : LambdaType p✝ U✝},
    (Γ ++ Δ ⊢[T] a✝ ∶ σ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ → (Γ ⊢[T] a✝ ∶ σ)
Γ : Context p✝ U✝
σ : LambdaType p✝ U✝
h : Γ ++ Δ ⊢[T] LambdaTerm.lambda a✝² a✝¹ a✝ ∶ σ
ht : LambdaTerm.freeVarRange (LambdaTerm.lambda a✝² a✝¹ a✝) ≤ List.length Γ
⊢ Γ ⊢[T] LambdaTerm.lambda a✝² a✝¹ a✝ ∶ σ

case app
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝² : p✝.lambda = true
a✝¹ a✝ : LambdaTerm p✝ U✝ C✝
a_ih✝¹ :
  ∀ {Γ : Context p✝ U✝} {σ : LambdaType p✝ U✝},
    (Γ ++ Δ ⊢[T] a✝¹ ∶ σ) → LambdaTerm.freeVarRange a✝¹ ≤ List.length Γ → (Γ ⊢[T] a✝¹ ∶ σ)
a_ih✝ :
  ∀ {Γ : Context p✝ U✝} {σ : LambdaType p✝ U✝},
    (Γ ++ Δ ⊢[T] a✝ ∶ σ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ → (Γ ⊢[T] a✝ ∶ σ)
Γ : Context p✝ U✝
σ : LambdaType p✝ U✝
h : Γ ++ Δ ⊢[T] LambdaTerm.app a✝² a✝¹ a✝ ∶ σ
ht : LambdaTerm.freeVarRange (LambdaTerm.app a✝² a✝¹ a✝) ≤ List.length Γ
⊢ Γ ⊢[T] LambdaTerm.app a✝² a✝¹ a✝ ∶ σ

case pair
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝² : p✝.prod = true
a✝¹ a✝ : LambdaTerm p✝ U✝ C✝
a_ih✝¹ :
  ∀ {Γ : Context p✝ U✝} {σ : LambdaType p✝ U✝},
    (Γ ++ Δ ⊢[T] a✝¹ ∶ σ) → LambdaTerm.freeVarRange a✝¹ ≤ List.length Γ → (Γ ⊢[T] a✝¹ ∶ σ)
a_ih✝ :
  ∀ {Γ : Context p✝ U✝} {σ : LambdaType p✝ U✝},
    (Γ ++ Δ ⊢[T] a✝ ∶ σ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ → (Γ ⊢[T] a✝ ∶ σ)
Γ : Context p✝ U✝
σ : LambdaType p✝ U✝
h : Γ ++ Δ ⊢[T] LambdaTerm.pair a✝² a✝¹ a✝ ∶ σ
ht : LambdaTerm.freeVarRange (LambdaTerm.pair a✝² a✝¹ a✝) ≤ List.length Γ
⊢ Γ ⊢[T] LambdaTerm.pair a✝² a✝¹ a✝ ∶ σ

case fst
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝¹ : p✝.prod = true
a✝ : LambdaTerm p✝ U✝ C✝
a_ih✝ :
  ∀ {Γ : Context p✝ U✝} {σ : LambdaType p✝ U✝},
    (Γ ++ Δ ⊢[T] a✝ ∶ σ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ → (Γ ⊢[T] a✝ ∶ σ)
Γ : Context p✝ U✝
σ : LambdaType p✝ U✝
h : Γ ++ Δ ⊢[T] LambdaTerm.fst a✝¹ a✝ ∶ σ
ht : LambdaTerm.freeVarRange (LambdaTerm.fst a✝¹ a✝) ≤ List.length Γ
⊢ Γ ⊢[T] LambdaTerm.fst a✝¹ a✝ ∶ σ

case snd
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝¹ : p✝.prod = true
a✝ : LambdaTerm p✝ U✝ C✝
a_ih✝ :
  ∀ {Γ : Context p✝ U✝} {σ : LambdaType p✝ U✝},
    (Γ ++ Δ ⊢[T] a✝ ∶ σ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ → (Γ ⊢[T] a✝ ∶ σ)
Γ : Context p✝ U✝
σ : LambdaType p✝ U✝
h : Γ ++ Δ ⊢[T] LambdaTerm.snd a✝¹ a✝ ∶ σ
ht : LambdaTerm.freeVarRange (LambdaTerm.snd a✝¹ a✝) ≤ List.length Γ
⊢ Γ ⊢[T] LambdaTerm.snd a✝¹ a✝ ∶ σ

case inl
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝² : p✝.coprod = true
a✝¹ : LambdaType p✝ U✝
a✝ : LambdaTerm p✝ U✝ C✝
a_ih✝ :
  ∀ {Γ : Context p✝ U✝} {σ : LambdaType p✝ U✝},
    (Γ ++ Δ ⊢[T] a✝ ∶ σ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ → (Γ ⊢[T] a✝ ∶ σ)
Γ : Context p✝ U✝
σ : LambdaType p✝ U✝
h : Γ ++ Δ ⊢[T] LambdaTerm.inl a✝² a✝¹ a✝ ∶ σ
ht : LambdaTerm.freeVarRange (LambdaTerm.inl a✝² a✝¹ a✝) ≤ List.length Γ
⊢ Γ ⊢[T] LambdaTerm.inl a✝² a✝¹ a✝ ∶ σ

case inr
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝² : p✝.coprod = true
a✝¹ : LambdaType p✝ U✝
a✝ : LambdaTerm p✝ U✝ C✝
a_ih✝ :
  ∀ {Γ : Context p✝ U✝} {σ : LambdaType p✝ U✝},
    (Γ ++ Δ ⊢[T] a✝ ∶ σ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ → (Γ ⊢[T] a✝ ∶ σ)
Γ : Context p✝ U✝
σ : LambdaType p✝ U✝
h : Γ ++ Δ ⊢[T] LambdaTerm.inr a✝² a✝¹ a✝ ∶ σ
ht : LambdaTerm.freeVarRange (LambdaTerm.inr a✝² a✝¹ a✝) ≤ List.length Γ
⊢ Γ ⊢[T] LambdaTerm.inr a✝² a✝¹ a✝ ∶ σ

case case
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝³ : p✝.coprod = true
a✝² a✝¹ a✝ : LambdaTerm p✝ U✝ C✝
a_ih✝² :
  ∀ {Γ : Context p✝ U✝} {σ : LambdaType p✝ U✝},
    (Γ ++ Δ ⊢[T] a✝² ∶ σ) → LambdaTerm.freeVarRange a✝² ≤ List.length Γ → (Γ ⊢[T] a✝² ∶ σ)
a_ih✝¹ :
  ∀ {Γ : Context p✝ U✝} {σ : LambdaType p✝ U✝},
    (Γ ++ Δ ⊢[T] a✝¹ ∶ σ) → LambdaTerm.freeVarRange a✝¹ ≤ List.length Γ → (Γ ⊢[T] a✝¹ ∶ σ)
a_ih✝ :
  ∀ {Γ : Context p✝ U✝} {σ : LambdaType p✝ U✝},
    (Γ ++ Δ ⊢[T] a✝ ∶ σ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ → (Γ ⊢[T] a✝ ∶ σ)
Γ : Context p✝ U✝
σ : LambdaType p✝ U✝
h : Γ ++ Δ ⊢[T] LambdaTerm.case a✝³ a✝² a✝¹ a✝ ∶ σ
ht : LambdaTerm.freeVarRange (LambdaTerm.case a✝³ a✝² a✝¹ a✝) ≤ List.length Γ
⊢ Γ ⊢[T] LambdaTerm.case a✝³ a✝² a✝¹ a✝ ∶ σ

case star
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝ : p✝.unit = true
Γ : Context p✝ U✝
σ : LambdaType p✝ U✝
h : Γ ++ Δ ⊢[T] LambdaTerm.star a✝ ∶ σ
ht : LambdaTerm.freeVarRange (LambdaTerm.star a✝) ≤ List.length Γ
⊢ Γ ⊢[T] LambdaTerm.star a✝ ∶ σ

case elim
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝² : p✝.empty = true
a✝¹ : LambdaType p✝ U✝
a✝ : LambdaTerm p✝ U✝ C✝
a_ih✝ :
  ∀ {Γ : Context p✝ U✝} {σ : LambdaType p✝ U✝},
    (Γ ++ Δ ⊢[T] a✝ ∶ σ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ → (Γ ⊢[T] a✝ ∶ σ)
Γ : Context p✝ U✝
σ : LambdaType p✝ U✝
h : Γ ++ Δ ⊢[T] LambdaTerm.elim a✝² a✝¹ a✝ ∶ σ
ht : LambdaTerm.freeVarRange (LambdaTerm.elim a✝² a✝¹ a✝) ≤ List.length Γ
⊢ Γ ⊢[T] LambdaTerm.elim a✝² a✝¹ a✝ ∶ σ

State before:
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝ : ℕ
Γ : Context p✝ U✝
σ : LambdaType p✝ U✝
h : Γ ++ Δ ⊢[T] LambdaTerm.var a✝ ∶ σ
ht : LambdaTerm.freeVarRange (LambdaTerm.var a✝) ≤ List.length Γ
⊢ Γ ⊢[T] LambdaTerm.var a✝ ∶ σ
Tactic:
case var =>
  simp only [hasType_var, List.length_append] at h ⊢
  obtain ⟨_, rfl⟩ := h
  rw [LambdaTerm.freeVarRange_var, Nat.add_one_le_iff] at ht
  refine ⟨ht, ?_⟩
  rw [List.get_append]
State after:
no goals

State before:
case const
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝ : C✝
Γ : Context p✝ U✝
σ : LambdaType p✝ U✝
h : Γ ++ Δ ⊢[T] LambdaTerm.const a✝ ∶ σ
ht : LambdaTerm.freeVarRange (LambdaTerm.const a✝) ≤ List.length Γ
⊢ Γ ⊢[T] LambdaTerm.const a✝ ∶ σ

case lambda
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝² : p✝.lambda = true
a✝¹ : LambdaType p✝ U✝
a✝ : LambdaTerm p✝ U✝ C✝
a_ih✝ :
  ∀ {Γ : Context p✝ U✝} {σ : LambdaType p✝ U✝},
    (Γ ++ Δ ⊢[T] a✝ ∶ σ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ → (Γ ⊢[T] a✝ ∶ σ)
Γ : Context p✝ U✝
σ : LambdaType p✝ U✝
h : Γ ++ Δ ⊢[T] LambdaTerm.lambda a✝² a✝¹ a✝ ∶ σ
ht : LambdaTerm.freeVarRange (LambdaTerm.lambda a✝² a✝¹ a✝) ≤ List.length Γ
⊢ Γ ⊢[T] LambdaTerm.lambda a✝² a✝¹ a✝ ∶ σ

case app
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝² : p✝.lambda = true
a✝¹ a✝ : LambdaTerm p✝ U✝ C✝
a_ih✝¹ :
  ∀ {Γ : Context p✝ U✝} {σ : LambdaType p✝ U✝},
    (Γ ++ Δ ⊢[T] a✝¹ ∶ σ) → LambdaTerm.freeVarRange a✝¹ ≤ List.length Γ → (Γ ⊢[T] a✝¹ ∶ σ)
a_ih✝ :
  ∀ {Γ : Context p✝ U✝} {σ : LambdaType p✝ U✝},
    (Γ ++ Δ ⊢[T] a✝ ∶ σ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ → (Γ ⊢[T] a✝ ∶ σ)
Γ : Context p✝ U✝
σ : LambdaType p✝ U✝
h : Γ ++ Δ ⊢[T] LambdaTerm.app a✝² a✝¹ a✝ ∶ σ
ht : LambdaTerm.freeVarRange (LambdaTerm.app a✝² a✝¹ a✝) ≤ List.length Γ
⊢ Γ ⊢[T] LambdaTerm.app a✝² a✝¹ a✝ ∶ σ

case pair
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝² : p✝.prod = true
a✝¹ a✝ : LambdaTerm p✝ U✝ C✝
a_ih✝¹ :
  ∀ {Γ : Context p✝ U✝} {σ : LambdaType p✝ U✝},
    (Γ ++ Δ ⊢[T] a✝¹ ∶ σ) → LambdaTerm.freeVarRange a✝¹ ≤ List.length Γ → (Γ ⊢[T] a✝¹ ∶ σ)
a_ih✝ :
  ∀ {Γ : Context p✝ U✝} {σ : LambdaType p✝ U✝},
    (Γ ++ Δ ⊢[T] a✝ ∶ σ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ → (Γ ⊢[T] a✝ ∶ σ)
Γ : Context p✝ U✝
σ : LambdaType p✝ U✝
h : Γ ++ Δ ⊢[T] LambdaTerm.pair a✝² a✝¹ a✝ ∶ σ
ht : LambdaTerm.freeVarRange (LambdaTerm.pair a✝² a✝¹ a✝) ≤ List.length Γ
⊢ Γ ⊢[T] LambdaTerm.pair a✝² a✝¹ a✝ ∶ σ

case fst
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝¹ : p✝.prod = true
a✝ : LambdaTerm p✝ U✝ C✝
a_ih✝ :
  ∀ {Γ : Context p✝ U✝} {σ : LambdaType p✝ U✝},
    (Γ ++ Δ ⊢[T] a✝ ∶ σ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ → (Γ ⊢[T] a✝ ∶ σ)
Γ : Context p✝ U✝
σ : LambdaType p✝ U✝
h : Γ ++ Δ ⊢[T] LambdaTerm.fst a✝¹ a✝ ∶ σ
ht : LambdaTerm.freeVarRange (LambdaTerm.fst a✝¹ a✝) ≤ List.length Γ
⊢ Γ ⊢[T] LambdaTerm.fst a✝¹ a✝ ∶ σ

case snd
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝¹ : p✝.prod = true
a✝ : LambdaTerm p✝ U✝ C✝
a_ih✝ :
  ∀ {Γ : Context p✝ U✝} {σ : LambdaType p✝ U✝},
    (Γ ++ Δ ⊢[T] a✝ ∶ σ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ → (Γ ⊢[T] a✝ ∶ σ)
Γ : Context p✝ U✝
σ : LambdaType p✝ U✝
h : Γ ++ Δ ⊢[T] LambdaTerm.snd a✝¹ a✝ ∶ σ
ht : LambdaTerm.freeVarRange (LambdaTerm.snd a✝¹ a✝) ≤ List.length Γ
⊢ Γ ⊢[T] LambdaTerm.snd a✝¹ a✝ ∶ σ

case inl
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝² : p✝.coprod = true
a✝¹ : LambdaType p✝ U✝
a✝ : LambdaTerm p✝ U✝ C✝
a_ih✝ :
  ∀ {Γ : Context p✝ U✝} {σ : LambdaType p✝ U✝},
    (Γ ++ Δ ⊢[T] a✝ ∶ σ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ → (Γ ⊢[T] a✝ ∶ σ)
Γ : Context p✝ U✝
σ : LambdaType p✝ U✝
h : Γ ++ Δ ⊢[T] LambdaTerm.inl a✝² a✝¹ a✝ ∶ σ
ht : LambdaTerm.freeVarRange (LambdaTerm.inl a✝² a✝¹ a✝) ≤ List.length Γ
⊢ Γ ⊢[T] LambdaTerm.inl a✝² a✝¹ a✝ ∶ σ

case inr
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝² : p✝.coprod = true
a✝¹ : LambdaType p✝ U✝
a✝ : LambdaTerm p✝ U✝ C✝
a_ih✝ :
  ∀ {Γ : Context p✝ U✝} {σ : LambdaType p✝ U✝},
    (Γ ++ Δ ⊢[T] a✝ ∶ σ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ → (Γ ⊢[T] a✝ ∶ σ)
Γ : Context p✝ U✝
σ : LambdaType p✝ U✝
h : Γ ++ Δ ⊢[T] LambdaTerm.inr a✝² a✝¹ a✝ ∶ σ
ht : LambdaTerm.freeVarRange (LambdaTerm.inr a✝² a✝¹ a✝) ≤ List.length Γ
⊢ Γ ⊢[T] LambdaTerm.inr a✝² a✝¹ a✝ ∶ σ

case case
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝³ : p✝.coprod = true
a✝² a✝¹ a✝ : LambdaTerm p✝ U✝ C✝
a_ih✝² :
  ∀ {Γ : Context p✝ U✝} {σ : LambdaType p✝ U✝},
    (Γ ++ Δ ⊢[T] a✝² ∶ σ) → LambdaTerm.freeVarRange a✝² ≤ List.length Γ → (Γ ⊢[T] a✝² ∶ σ)
a_ih✝¹ :
  ∀ {Γ : Context p✝ U✝} {σ : LambdaType p✝ U✝},
    (Γ ++ Δ ⊢[T] a✝¹ ∶ σ) → LambdaTerm.freeVarRange a✝¹ ≤ List.length Γ → (Γ ⊢[T] a✝¹ ∶ σ)
a_ih✝ :
  ∀ {Γ : Context p✝ U✝} {σ : LambdaType p✝ U✝},
    (Γ ++ Δ ⊢[T] a✝ ∶ σ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ → (Γ ⊢[T] a✝ ∶ σ)
Γ : Context p✝ U✝
σ : LambdaType p✝ U✝
h : Γ ++ Δ ⊢[T] LambdaTerm.case a✝³ a✝² a✝¹ a✝ ∶ σ
ht : LambdaTerm.freeVarRange (LambdaTerm.case a✝³ a✝² a✝¹ a✝) ≤ List.length Γ
⊢ Γ ⊢[T] LambdaTerm.case a✝³ a✝² a✝¹ a✝ ∶ σ

case star
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝ : p✝.unit = true
Γ : Context p✝ U✝
σ : LambdaType p✝ U✝
h : Γ ++ Δ ⊢[T] LambdaTerm.star a✝ ∶ σ
ht : LambdaTerm.freeVarRange (LambdaTerm.star a✝) ≤ List.length Γ
⊢ Γ ⊢[T] LambdaTerm.star a✝ ∶ σ

case elim
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝² : p✝.empty = true
a✝¹ : LambdaType p✝ U✝
a✝ : LambdaTerm p✝ U✝ C✝
a_ih✝ :
  ∀ {Γ : Context p✝ U✝} {σ : LambdaType p✝ U✝},
    (Γ ++ Δ ⊢[T] a✝ ∶ σ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ → (Γ ⊢[T] a✝ ∶ σ)
Γ : Context p✝ U✝
σ : LambdaType p✝ U✝
h : Γ ++ Δ ⊢[T] LambdaTerm.elim a✝² a✝¹ a✝ ∶ σ
ht : LambdaTerm.freeVarRange (LambdaTerm.elim a✝² a✝¹ a✝) ≤ List.length Γ
⊢ Γ ⊢[T] LambdaTerm.elim a✝² a✝¹ a✝ ∶ σ
Tactic:
all_goals aesop
State after:
no goals

State before:
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝ : ℕ
Γ : Context p✝ U✝
σ : LambdaType p✝ U✝
h : Γ ++ Δ ⊢[T] LambdaTerm.var a✝ ∶ σ
ht : LambdaTerm.freeVarRange (LambdaTerm.var a✝) ≤ List.length Γ
⊢ Γ ⊢[T] LambdaTerm.var a✝ ∶ σ
Tactic:
simp only [hasType_var, List.length_append] at h ⊢
State after:
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝ : ℕ
Γ : Context p✝ U✝
σ : LambdaType p✝ U✝
ht : LambdaTerm.freeVarRange (LambdaTerm.var a✝) ≤ List.length Γ
h :
  ∃ (h : a✝ < List.length Γ + List.length Δ),
    σ = List.get (Γ ++ Δ) { val := a✝, isLt := (_ : a✝ < List.length (Γ ++ Δ)) }
⊢ ∃ (h : a✝ < List.length Γ), σ = List.get Γ { val := a✝, isLt := h }

State before:
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝ : ℕ
Γ : Context p✝ U✝
σ : LambdaType p✝ U✝
ht : LambdaTerm.freeVarRange (LambdaTerm.var a✝) ≤ List.length Γ
h :
  ∃ (h : a✝ < List.length Γ + List.length Δ),
    σ = List.get (Γ ++ Δ) { val := a✝, isLt := (_ : a✝ < List.length (Γ ++ Δ)) }
⊢ ∃ (h : a✝ < List.length Γ), σ = List.get Γ { val := a✝, isLt := h }
Tactic:
obtain ⟨_, rfl⟩ := h
State after:
case intro
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝ : ℕ
Γ : Context p✝ U✝
ht : LambdaTerm.freeVarRange (LambdaTerm.var a✝) ≤ List.length Γ
w✝ : a✝ < List.length Γ + List.length Δ
⊢ ∃ (h : a✝ < List.length Γ),
    List.get (Γ ++ Δ) { val := a✝, isLt := (_ : a✝ < List.length (Γ ++ Δ)) } = List.get Γ { val := a✝, isLt := h }

State before:
case intro
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝ : ℕ
Γ : Context p✝ U✝
ht : LambdaTerm.freeVarRange (LambdaTerm.var a✝) ≤ List.length Γ
w✝ : a✝ < List.length Γ + List.length Δ
⊢ ∃ (h : a✝ < List.length Γ),
    List.get (Γ ++ Δ) { val := a✝, isLt := (_ : a✝ < List.length (Γ ++ Δ)) } = List.get Γ { val := a✝, isLt := h }
Tactic:
rw [LambdaTerm.freeVarRange_var, Nat.add_one_le_iff] at ht
State after:
case intro
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝ : ℕ
Γ : Context p✝ U✝
ht : a✝ < List.length Γ
w✝ : a✝ < List.length Γ + List.length Δ
⊢ ∃ (h : a✝ < List.length Γ),
    List.get (Γ ++ Δ) { val := a✝, isLt := (_ : a✝ < List.length (Γ ++ Δ)) } = List.get Γ { val := a✝, isLt := h }

State before:
case intro
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝ : ℕ
Γ : Context p✝ U✝
ht : a✝ < List.length Γ
w✝ : a✝ < List.length Γ + List.length Δ
⊢ ∃ (h : a✝ < List.length Γ),
    List.get (Γ ++ Δ) { val := a✝, isLt := (_ : a✝ < List.length (Γ ++ Δ)) } = List.get Γ { val := a✝, isLt := h }
Tactic:
refine ⟨ht, ?_⟩
State after:
case intro
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝ : ℕ
Γ : Context p✝ U✝
ht : a✝ < List.length Γ
w✝ : a✝ < List.length Γ + List.length Δ
⊢ List.get (Γ ++ Δ) { val := a✝, isLt := (_ : a✝ < List.length (Γ ++ Δ)) } = List.get Γ { val := a✝, isLt := ht }

State before:
case intro
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝ : ℕ
Γ : Context p✝ U✝
ht : a✝ < List.length Γ
w✝ : a✝ < List.length Γ + List.length Δ
⊢ List.get (Γ ++ Δ) { val := a✝, isLt := (_ : a✝ < List.length (Γ ++ Δ)) } = List.get Γ { val := a✝, isLt := ht }
Tactic:
rw [List.get_append]
State after:
no goals

State before:
case elim
p : LambdaParams
U : Type ?u.469890
C : Type ?u.469893
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Δ : Context p✝ U✝
a✝² : p✝.empty = true
a✝¹ : LambdaType p✝ U✝
a✝ : LambdaTerm p✝ U✝ C✝
a_ih✝ :
  ∀ {Γ : Context p✝ U✝} {σ : LambdaType p✝ U✝},
    (Γ ++ Δ ⊢[T] a✝ ∶ σ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ → (Γ ⊢[T] a✝ ∶ σ)
Γ : Context p✝ U✝
σ : LambdaType p✝ U✝
h : Γ ++ Δ ⊢[T] LambdaTerm.elim a✝² a✝¹ a✝ ∶ σ
ht : LambdaTerm.freeVarRange (LambdaTerm.elim a✝² a✝¹ a✝) ≤ List.length Γ
⊢ Γ ⊢[T] LambdaTerm.elim a✝² a✝¹ a✝ ∶ σ
Tactic:
aesop
State after:
no goals