Theorem: LambdaCalculi.append_hasType
Proof 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
Proof state after:
no goals