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

State before:
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
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 ∶ τ
⊢ LambdaTerm.freeVarRange t ≤ List.length Γ
Tactic:
induction t generalizing Γ τ
State after:
case const
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
a✝ : C✝
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.const a✝ ∶ τ
⊢ LambdaTerm.freeVarRange (LambdaTerm.const a✝) ≤ List.length Γ

case var
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
a✝ : ℕ
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.var a✝ ∶ τ
⊢ LambdaTerm.freeVarRange (LambdaTerm.var a✝) ≤ List.length Γ

case lambda
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType 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 Γ
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.lambda a✝² a✝¹ a✝ ∶ τ
⊢ LambdaTerm.freeVarRange (LambdaTerm.lambda a✝² a✝¹ a✝) ≤ List.length Γ

case app
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType 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 Γ
a_ih✝ : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝ ∶ τ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.app a✝² a✝¹ a✝ ∶ τ
⊢ LambdaTerm.freeVarRange (LambdaTerm.app a✝² a✝¹ a✝) ≤ List.length Γ

case pair
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType 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 Γ
a_ih✝ : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝ ∶ τ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.pair a✝² a✝¹ a✝ ∶ τ
⊢ LambdaTerm.freeVarRange (LambdaTerm.pair a✝² a✝¹ a✝) ≤ List.length Γ

case fst
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType 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 Γ
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.fst a✝¹ a✝ ∶ τ
⊢ LambdaTerm.freeVarRange (LambdaTerm.fst a✝¹ a✝) ≤ List.length Γ

case snd
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType 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 Γ
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.snd a✝¹ a✝ ∶ τ
⊢ LambdaTerm.freeVarRange (LambdaTerm.snd a✝¹ a✝) ≤ List.length Γ

case inl
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType 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 Γ
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.inl a✝² a✝¹ a✝ ∶ τ
⊢ LambdaTerm.freeVarRange (LambdaTerm.inl a✝² a✝¹ a✝) ≤ List.length Γ

case inr
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType 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 Γ
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.inr a✝² a✝¹ a✝ ∶ τ
⊢ LambdaTerm.freeVarRange (LambdaTerm.inr a✝² a✝¹ a✝) ≤ List.length Γ

case case
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType 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 Γ
a_ih✝¹ : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝¹ ∶ τ) → LambdaTerm.freeVarRange a✝¹ ≤ List.length Γ
a_ih✝ : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝ ∶ τ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.case a✝³ a✝² a✝¹ a✝ ∶ τ
⊢ LambdaTerm.freeVarRange (LambdaTerm.case a✝³ a✝² a✝¹ a✝) ≤ List.length Γ

case star
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
a✝ : p✝.unit = true
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.star a✝ ∶ τ
⊢ LambdaTerm.freeVarRange (LambdaTerm.star a✝) ≤ List.length Γ

case elim
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType 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 Γ
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.elim a✝² a✝¹ a✝ ∶ τ
⊢ LambdaTerm.freeVarRange (LambdaTerm.elim a✝² a✝¹ a✝) ≤ List.length Γ

State before:
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
a✝² : p✝.lambda = true
a✝¹ : LambdaType p✝ U✝
a✝ : LambdaTerm p✝ U✝ C✝
ih : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝ ∶ τ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.lambda a✝² a✝¹ a✝ ∶ τ
⊢ LambdaTerm.freeVarRange (LambdaTerm.lambda a✝² a✝¹ a✝) ≤ List.length Γ
Tactic:
case lambda ih =>
  simp at h ⊢
  obtain ⟨σ, rfl, h⟩ := h
  exact ih h
State after:
no goals

State before:
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
a✝³ : p✝.coprod = true
a✝² a✝¹ a✝ : LambdaTerm p✝ U✝ C✝
ih₁ : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝² ∶ τ) → LambdaTerm.freeVarRange a✝² ≤ List.length Γ
ih₂ : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝¹ ∶ τ) → LambdaTerm.freeVarRange a✝¹ ≤ List.length Γ
ih : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝ ∶ τ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.case a✝³ a✝² a✝¹ a✝ ∶ τ
⊢ LambdaTerm.freeVarRange (LambdaTerm.case a✝³ a✝² a✝¹ a✝) ≤ List.length Γ
Tactic:
case case ih₁ ih₂ ih =>
  simp at h ⊢
  obtain ⟨τ₁, τ₂, h, h₁, h₂⟩ := h
  exact ⟨⟨ih₁ h₁, ih₂ h₂⟩, ih h⟩
State after:
no goals

State before:
case const
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
a✝ : C✝
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.const a✝ ∶ τ
⊢ LambdaTerm.freeVarRange (LambdaTerm.const a✝) ≤ List.length Γ

case var
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
a✝ : ℕ
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.var a✝ ∶ τ
⊢ LambdaTerm.freeVarRange (LambdaTerm.var a✝) ≤ List.length Γ

case app
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType 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 Γ
a_ih✝ : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝ ∶ τ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.app a✝² a✝¹ a✝ ∶ τ
⊢ LambdaTerm.freeVarRange (LambdaTerm.app a✝² a✝¹ a✝) ≤ List.length Γ

case pair
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType 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 Γ
a_ih✝ : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝ ∶ τ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.pair a✝² a✝¹ a✝ ∶ τ
⊢ LambdaTerm.freeVarRange (LambdaTerm.pair a✝² a✝¹ a✝) ≤ List.length Γ

case fst
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType 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 Γ
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.fst a✝¹ a✝ ∶ τ
⊢ LambdaTerm.freeVarRange (LambdaTerm.fst a✝¹ a✝) ≤ List.length Γ

case snd
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType 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 Γ
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.snd a✝¹ a✝ ∶ τ
⊢ LambdaTerm.freeVarRange (LambdaTerm.snd a✝¹ a✝) ≤ List.length Γ

case inl
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType 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 Γ
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.inl a✝² a✝¹ a✝ ∶ τ
⊢ LambdaTerm.freeVarRange (LambdaTerm.inl a✝² a✝¹ a✝) ≤ List.length Γ

case inr
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType 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 Γ
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.inr a✝² a✝¹ a✝ ∶ τ
⊢ LambdaTerm.freeVarRange (LambdaTerm.inr a✝² a✝¹ a✝) ≤ List.length Γ

case star
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
a✝ : p✝.unit = true
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.star a✝ ∶ τ
⊢ LambdaTerm.freeVarRange (LambdaTerm.star a✝) ≤ List.length Γ

case elim
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType 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 Γ
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.elim a✝² a✝¹ a✝ ∶ τ
⊢ LambdaTerm.freeVarRange (LambdaTerm.elim a✝² a✝¹ a✝) ≤ List.length Γ
Tactic:
all_goals aesop
State after:
no goals

State before:
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
a✝² : p✝.lambda = true
a✝¹ : LambdaType p✝ U✝
a✝ : LambdaTerm p✝ U✝ C✝
ih : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝ ∶ τ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.lambda a✝² a✝¹ a✝ ∶ τ
⊢ LambdaTerm.freeVarRange (LambdaTerm.lambda a✝² a✝¹ a✝) ≤ List.length Γ
Tactic:
simp at h ⊢
State after:
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
a✝² : p✝.lambda = true
a✝¹ : LambdaType p✝ U✝
a✝ : LambdaTerm p✝ U✝ C✝
ih : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝ ∶ τ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : ∃ σ, τ = LambdaType.lambda a✝² a✝¹ σ ∧ (a✝¹ :: Γ ⊢[T] a✝ ∶ σ)
⊢ LambdaTerm.freeVarRange a✝ ≤ List.length Γ + 1

State before:
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
a✝² : p✝.lambda = true
a✝¹ : LambdaType p✝ U✝
a✝ : LambdaTerm p✝ U✝ C✝
ih : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝ ∶ τ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : ∃ σ, τ = LambdaType.lambda a✝² a✝¹ σ ∧ (a✝¹ :: Γ ⊢[T] a✝ ∶ σ)
⊢ LambdaTerm.freeVarRange a✝ ≤ List.length Γ + 1
Tactic:
obtain ⟨σ, rfl, h⟩ := h
State after:
case intro.intro
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
a✝² : p✝.lambda = true
a✝¹ : LambdaType p✝ U✝
a✝ : LambdaTerm p✝ U✝ C✝
ih : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝ ∶ τ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ
Γ : Context p✝ U✝
σ : LambdaType p✝ U✝
h : a✝¹ :: Γ ⊢[T] a✝ ∶ σ
⊢ LambdaTerm.freeVarRange a✝ ≤ List.length Γ + 1

State before:
case intro.intro
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
a✝² : p✝.lambda = true
a✝¹ : LambdaType p✝ U✝
a✝ : LambdaTerm p✝ U✝ C✝
ih : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝ ∶ τ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ
Γ : Context p✝ U✝
σ : LambdaType p✝ U✝
h : a✝¹ :: Γ ⊢[T] a✝ ∶ σ
⊢ LambdaTerm.freeVarRange a✝ ≤ List.length Γ + 1
Tactic:
exact ih h
State after:
no goals

State before:
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
a✝³ : p✝.coprod = true
a✝² a✝¹ a✝ : LambdaTerm p✝ U✝ C✝
ih₁ : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝² ∶ τ) → LambdaTerm.freeVarRange a✝² ≤ List.length Γ
ih₂ : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝¹ ∶ τ) → LambdaTerm.freeVarRange a✝¹ ≤ List.length Γ
ih : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝ ∶ τ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.case a✝³ a✝² a✝¹ a✝ ∶ τ
⊢ LambdaTerm.freeVarRange (LambdaTerm.case a✝³ a✝² a✝¹ a✝) ≤ List.length Γ
Tactic:
simp at h ⊢
State after:
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
a✝³ : p✝.coprod = true
a✝² a✝¹ a✝ : LambdaTerm p✝ U✝ C✝
ih₁ : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝² ∶ τ) → LambdaTerm.freeVarRange a✝² ≤ List.length Γ
ih₂ : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝¹ ∶ τ) → LambdaTerm.freeVarRange a✝¹ ≤ List.length Γ
ih : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝ ∶ τ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : ∃ τ₁ τ₂, (Γ ⊢[T] a✝ ∶ LambdaType.coprod a✝³ τ₁ τ₂) ∧ (τ₁ :: Γ ⊢[T] a✝² ∶ τ) ∧ (τ₂ :: Γ ⊢[T] a✝¹ ∶ τ)
⊢ (LambdaTerm.freeVarRange a✝² ≤ List.length Γ + 1 ∧ LambdaTerm.freeVarRange a✝¹ ≤ List.length Γ + 1) ∧
    LambdaTerm.freeVarRange a✝ ≤ List.length Γ

State before:
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
a✝³ : p✝.coprod = true
a✝² a✝¹ a✝ : LambdaTerm p✝ U✝ C✝
ih₁ : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝² ∶ τ) → LambdaTerm.freeVarRange a✝² ≤ List.length Γ
ih₂ : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝¹ ∶ τ) → LambdaTerm.freeVarRange a✝¹ ≤ List.length Γ
ih : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝ ∶ τ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : ∃ τ₁ τ₂, (Γ ⊢[T] a✝ ∶ LambdaType.coprod a✝³ τ₁ τ₂) ∧ (τ₁ :: Γ ⊢[T] a✝² ∶ τ) ∧ (τ₂ :: Γ ⊢[T] a✝¹ ∶ τ)
⊢ (LambdaTerm.freeVarRange a✝² ≤ List.length Γ + 1 ∧ LambdaTerm.freeVarRange a✝¹ ≤ List.length Γ + 1) ∧
    LambdaTerm.freeVarRange a✝ ≤ List.length Γ
Tactic:
obtain ⟨τ₁, τ₂, h, h₁, h₂⟩ := h
State after:
case intro.intro.intro.intro
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
a✝³ : p✝.coprod = true
a✝² a✝¹ a✝ : LambdaTerm p✝ U✝ C✝
ih₁ : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝² ∶ τ) → LambdaTerm.freeVarRange a✝² ≤ List.length Γ
ih₂ : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝¹ ∶ τ) → LambdaTerm.freeVarRange a✝¹ ≤ List.length Γ
ih : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝ ∶ τ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ
Γ : Context p✝ U✝
τ τ₁ τ₂ : LambdaType p✝ U✝
h : Γ ⊢[T] a✝ ∶ LambdaType.coprod a✝³ τ₁ τ₂
h₁ : τ₁ :: Γ ⊢[T] a✝² ∶ τ
h₂ : τ₂ :: Γ ⊢[T] a✝¹ ∶ τ
⊢ (LambdaTerm.freeVarRange a✝² ≤ List.length Γ + 1 ∧ LambdaTerm.freeVarRange a✝¹ ≤ List.length Γ + 1) ∧
    LambdaTerm.freeVarRange a✝ ≤ List.length Γ

State before:
case intro.intro.intro.intro
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
a✝³ : p✝.coprod = true
a✝² a✝¹ a✝ : LambdaTerm p✝ U✝ C✝
ih₁ : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝² ∶ τ) → LambdaTerm.freeVarRange a✝² ≤ List.length Γ
ih₂ : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝¹ ∶ τ) → LambdaTerm.freeVarRange a✝¹ ≤ List.length Γ
ih : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝ ∶ τ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ
Γ : Context p✝ U✝
τ τ₁ τ₂ : LambdaType p✝ U✝
h : Γ ⊢[T] a✝ ∶ LambdaType.coprod a✝³ τ₁ τ₂
h₁ : τ₁ :: Γ ⊢[T] a✝² ∶ τ
h₂ : τ₂ :: Γ ⊢[T] a✝¹ ∶ τ
⊢ (LambdaTerm.freeVarRange a✝² ≤ List.length Γ + 1 ∧ LambdaTerm.freeVarRange a✝¹ ≤ List.length Γ + 1) ∧
    LambdaTerm.freeVarRange a✝ ≤ List.length Γ
Tactic:
exact ⟨⟨ih₁ h₁, ih₂ h₂⟩, ih h⟩
State after:
no goals

State before:
case elim
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType 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 Γ
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.elim a✝² a✝¹ a✝ ∶ τ
⊢ LambdaTerm.freeVarRange (LambdaTerm.elim a✝² a✝¹ a✝) ≤ List.length Γ
Tactic:
aesop
State after:
no goals