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

State before:
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
T : C✝ → LambdaType p U
Γ : Context p U
t : LambdaTerm p U C✝
σ : LambdaType p U
h : Γ ⊢[T] t ∶ σ
Δ : Context p U
⊢ Γ ++ Δ ⊢[T] t ∶ σ
Tactic:
induction t generalizing Γ σ
State after:
case const
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
T : C✝ → LambdaType p U
Δ : Context p U
a✝ : C✝
Γ : Context p U
σ : LambdaType p U
h : Γ ⊢[T] LambdaTerm.const a✝ ∶ σ
⊢ Γ ++ Δ ⊢[T] LambdaTerm.const a✝ ∶ σ

case var
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
T : C✝ → LambdaType p U
Δ : Context p U
a✝ : ℕ
Γ : Context p U
σ : LambdaType p U
h : Γ ⊢[T] LambdaTerm.var a✝ ∶ σ
⊢ Γ ++ Δ ⊢[T] LambdaTerm.var a✝ ∶ σ

case lambda
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
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✝ ∶ σ) → (Γ ++ Δ ⊢[T] a✝ ∶ σ)
Γ : Context p U
σ : LambdaType p U
h : Γ ⊢[T] LambdaTerm.lambda a✝² a✝¹ a✝ ∶ σ
⊢ Γ ++ Δ ⊢[T] LambdaTerm.lambda a✝² a✝¹ a✝ ∶ σ

case app
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
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✝¹ ∶ σ) → (Γ ++ Δ ⊢[T] a✝¹ ∶ σ)
a_ih✝ : ∀ {Γ : Context p U} {σ : LambdaType p U}, (Γ ⊢[T] a✝ ∶ σ) → (Γ ++ Δ ⊢[T] a✝ ∶ σ)
Γ : Context p U
σ : LambdaType p U
h : Γ ⊢[T] LambdaTerm.app a✝² a✝¹ a✝ ∶ σ
⊢ Γ ++ Δ ⊢[T] LambdaTerm.app a✝² a✝¹ a✝ ∶ σ

case pair
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
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✝¹ ∶ σ) → (Γ ++ Δ ⊢[T] a✝¹ ∶ σ)
a_ih✝ : ∀ {Γ : Context p U} {σ : LambdaType p U}, (Γ ⊢[T] a✝ ∶ σ) → (Γ ++ Δ ⊢[T] a✝ ∶ σ)
Γ : Context p U
σ : LambdaType p U
h : Γ ⊢[T] LambdaTerm.pair a✝² a✝¹ a✝ ∶ σ
⊢ Γ ++ Δ ⊢[T] LambdaTerm.pair a✝² a✝¹ a✝ ∶ σ

case fst
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
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✝ ∶ σ) → (Γ ++ Δ ⊢[T] a✝ ∶ σ)
Γ : Context p U
σ : LambdaType p U
h : Γ ⊢[T] LambdaTerm.fst a✝¹ a✝ ∶ σ
⊢ Γ ++ Δ ⊢[T] LambdaTerm.fst a✝¹ a✝ ∶ σ

case snd
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
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✝ ∶ σ) → (Γ ++ Δ ⊢[T] a✝ ∶ σ)
Γ : Context p U
σ : LambdaType p U
h : Γ ⊢[T] LambdaTerm.snd a✝¹ a✝ ∶ σ
⊢ Γ ++ Δ ⊢[T] LambdaTerm.snd a✝¹ a✝ ∶ σ

case inl
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
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✝ ∶ σ) → (Γ ++ Δ ⊢[T] a✝ ∶ σ)
Γ : Context p U
σ : LambdaType p U
h : Γ ⊢[T] LambdaTerm.inl a✝² a✝¹ a✝ ∶ σ
⊢ Γ ++ Δ ⊢[T] LambdaTerm.inl a✝² a✝¹ a✝ ∶ σ

case inr
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
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✝ ∶ σ) → (Γ ++ Δ ⊢[T] a✝ ∶ σ)
Γ : Context p U
σ : LambdaType p U
h : Γ ⊢[T] LambdaTerm.inr a✝² a✝¹ a✝ ∶ σ
⊢ Γ ++ Δ ⊢[T] LambdaTerm.inr a✝² a✝¹ a✝ ∶ σ

case case
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
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✝² ∶ σ) → (Γ ++ Δ ⊢[T] a✝² ∶ σ)
a_ih✝¹ : ∀ {Γ : Context p U} {σ : LambdaType p U}, (Γ ⊢[T] a✝¹ ∶ σ) → (Γ ++ Δ ⊢[T] a✝¹ ∶ σ)
a_ih✝ : ∀ {Γ : Context p U} {σ : LambdaType p U}, (Γ ⊢[T] a✝ ∶ σ) → (Γ ++ Δ ⊢[T] a✝ ∶ σ)
Γ : Context p U
σ : LambdaType p U
h : Γ ⊢[T] LambdaTerm.case a✝³ a✝² a✝¹ a✝ ∶ σ
⊢ Γ ++ Δ ⊢[T] LambdaTerm.case a✝³ a✝² a✝¹ a✝ ∶ σ

case star
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
T : C✝ → LambdaType p U
Δ : Context p U
a✝ : p.unit = true
Γ : Context p U
σ : LambdaType p U
h : Γ ⊢[T] LambdaTerm.star a✝ ∶ σ
⊢ Γ ++ Δ ⊢[T] LambdaTerm.star a✝ ∶ σ

case elim
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
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✝ ∶ σ) → (Γ ++ Δ ⊢[T] a✝ ∶ σ)
Γ : Context p U
σ : LambdaType p U
h : Γ ⊢[T] LambdaTerm.elim a✝² a✝¹ a✝ ∶ σ
⊢ Γ ++ Δ ⊢[T] LambdaTerm.elim a✝² a✝¹ a✝ ∶ σ

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

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

State before:
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
T : C✝ → LambdaType p U
Δ : Context p U
a✝³ : p.coprod = true
a✝² a✝¹ a✝ : LambdaTerm p U C✝
ih₁ : ∀ {Γ : Context p U} {σ : LambdaType p U}, (Γ ⊢[T] a✝² ∶ σ) → (Γ ++ Δ ⊢[T] a✝² ∶ σ)
ih₂ : ∀ {Γ : Context p U} {σ : LambdaType p U}, (Γ ⊢[T] a✝¹ ∶ σ) → (Γ ++ Δ ⊢[T] a✝¹ ∶ σ)
ih : ∀ {Γ : Context p U} {σ : LambdaType p U}, (Γ ⊢[T] a✝ ∶ σ) → (Γ ++ Δ ⊢[T] a✝ ∶ σ)
Γ : Context p U
σ : LambdaType p U
h : Γ ⊢[T] LambdaTerm.case a✝³ a✝² a✝¹ a✝ ∶ σ
⊢ Γ ++ Δ ⊢[T] LambdaTerm.case a✝³ a✝² a✝¹ a✝ ∶ σ
Tactic:
case case ih₁ ih₂ ih =>
  simp only [hasType_case] 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_2
C : Type ?u.350830
C✝ : Type u_1
T : C✝ → LambdaType p U
Δ : Context p U
a✝ : C✝
Γ : Context p U
σ : LambdaType p U
h : Γ ⊢[T] LambdaTerm.const a✝ ∶ σ
⊢ Γ ++ Δ ⊢[T] LambdaTerm.const a✝ ∶ σ

case app
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
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✝¹ ∶ σ) → (Γ ++ Δ ⊢[T] a✝¹ ∶ σ)
a_ih✝ : ∀ {Γ : Context p U} {σ : LambdaType p U}, (Γ ⊢[T] a✝ ∶ σ) → (Γ ++ Δ ⊢[T] a✝ ∶ σ)
Γ : Context p U
σ : LambdaType p U
h : Γ ⊢[T] LambdaTerm.app a✝² a✝¹ a✝ ∶ σ
⊢ Γ ++ Δ ⊢[T] LambdaTerm.app a✝² a✝¹ a✝ ∶ σ

case pair
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
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✝¹ ∶ σ) → (Γ ++ Δ ⊢[T] a✝¹ ∶ σ)
a_ih✝ : ∀ {Γ : Context p U} {σ : LambdaType p U}, (Γ ⊢[T] a✝ ∶ σ) → (Γ ++ Δ ⊢[T] a✝ ∶ σ)
Γ : Context p U
σ : LambdaType p U
h : Γ ⊢[T] LambdaTerm.pair a✝² a✝¹ a✝ ∶ σ
⊢ Γ ++ Δ ⊢[T] LambdaTerm.pair a✝² a✝¹ a✝ ∶ σ

case fst
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
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✝ ∶ σ) → (Γ ++ Δ ⊢[T] a✝ ∶ σ)
Γ : Context p U
σ : LambdaType p U
h : Γ ⊢[T] LambdaTerm.fst a✝¹ a✝ ∶ σ
⊢ Γ ++ Δ ⊢[T] LambdaTerm.fst a✝¹ a✝ ∶ σ

case snd
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
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✝ ∶ σ) → (Γ ++ Δ ⊢[T] a✝ ∶ σ)
Γ : Context p U
σ : LambdaType p U
h : Γ ⊢[T] LambdaTerm.snd a✝¹ a✝ ∶ σ
⊢ Γ ++ Δ ⊢[T] LambdaTerm.snd a✝¹ a✝ ∶ σ

case inl
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
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✝ ∶ σ) → (Γ ++ Δ ⊢[T] a✝ ∶ σ)
Γ : Context p U
σ : LambdaType p U
h : Γ ⊢[T] LambdaTerm.inl a✝² a✝¹ a✝ ∶ σ
⊢ Γ ++ Δ ⊢[T] LambdaTerm.inl a✝² a✝¹ a✝ ∶ σ

case inr
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
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✝ ∶ σ) → (Γ ++ Δ ⊢[T] a✝ ∶ σ)
Γ : Context p U
σ : LambdaType p U
h : Γ ⊢[T] LambdaTerm.inr a✝² a✝¹ a✝ ∶ σ
⊢ Γ ++ Δ ⊢[T] LambdaTerm.inr a✝² a✝¹ a✝ ∶ σ

case star
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
T : C✝ → LambdaType p U
Δ : Context p U
a✝ : p.unit = true
Γ : Context p U
σ : LambdaType p U
h : Γ ⊢[T] LambdaTerm.star a✝ ∶ σ
⊢ Γ ++ Δ ⊢[T] LambdaTerm.star a✝ ∶ σ

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

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

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

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

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

State before:
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
T : C✝ → LambdaType p U
Δ : Context p U
a✝² : p.lambda = true
a✝¹ : LambdaType p U
a✝ : LambdaTerm p U C✝
ih : ∀ {Γ : Context p U} {σ : LambdaType p U}, (Γ ⊢[T] a✝ ∶ σ) → (Γ ++ Δ ⊢[T] a✝ ∶ σ)
Γ : Context p U
σ : LambdaType p U
h : Γ ⊢[T] LambdaTerm.lambda a✝² a✝¹ a✝ ∶ σ
⊢ Γ ++ Δ ⊢[T] LambdaTerm.lambda a✝² a✝¹ a✝ ∶ σ
Tactic:
simp only [hasType_lambda] at h ⊢
State after:
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
T : C✝ → LambdaType p U
Δ : Context p U
a✝² : p.lambda = true
a✝¹ : LambdaType p U
a✝ : LambdaTerm p U C✝
ih : ∀ {Γ : Context p U} {σ : LambdaType p U}, (Γ ⊢[T] a✝ ∶ σ) → (Γ ++ Δ ⊢[T] a✝ ∶ σ)
Γ : Context p U
σ : LambdaType p U
h : ∃ σ_1, σ = LambdaType.lambda a✝² a✝¹ σ_1 ∧ (a✝¹ :: Γ ⊢[T] a✝ ∶ σ_1)
⊢ ∃ σ_1, σ = LambdaType.lambda a✝² a✝¹ σ_1 ∧ (a✝¹ :: (Γ ++ Δ) ⊢[T] a✝ ∶ σ_1)

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

State before:
case intro.intro
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
T : C✝ → LambdaType p U
Δ : Context p U
a✝² : p.lambda = true
a✝¹ : LambdaType p U
a✝ : LambdaTerm p U C✝
ih : ∀ {Γ : Context p U} {σ : LambdaType p U}, (Γ ⊢[T] a✝ ∶ σ) → (Γ ++ Δ ⊢[T] a✝ ∶ σ)
Γ : Context p U
σ : LambdaType p U
h : a✝¹ :: Γ ⊢[T] a✝ ∶ σ
⊢ ∃ σ_1, LambdaType.lambda a✝² a✝¹ σ = LambdaType.lambda a✝² a✝¹ σ_1 ∧ (a✝¹ :: (Γ ++ Δ) ⊢[T] a✝ ∶ σ_1)
Tactic:
exact ⟨σ, rfl, ih h⟩
State after:
no goals

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

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

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

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