Theorem: LambdaCalculi.eq_of_hasType
Proof state before:
p : LambdaParams
U : Type ?u.145218
C : Type ?u.145221
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 ∶ σ
hτ : Γ ⊢[T] t ∶ τ
⊢ σ = τ
Tactic:
induction t generalizing Γ σ τ
Proof state after:
case const
p : LambdaParams
U : Type ?u.145218
C : Type ?u.145221
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✝ ∶ σ
hτ : Γ ⊢[T] LambdaTerm.const a✝ ∶ τ
⊢ σ = τ

case var
p : LambdaParams
U : Type ?u.145218
C : Type ?u.145221
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✝ ∶ σ
hτ : Γ ⊢[T] LambdaTerm.var a✝ ∶ τ
⊢ σ = τ

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

case app
p : LambdaParams
U : Type ?u.145218
C : Type ?u.145221
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✝¹ ∶ σ) → (Γ ⊢[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✝ ∶ σ
hτ : Γ ⊢[T] LambdaTerm.app a✝² a✝¹ a✝ ∶ τ
⊢ σ = τ

case pair
p : LambdaParams
U : Type ?u.145218
C : Type ?u.145221
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✝¹ ∶ σ) → (Γ ⊢[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✝ ∶ σ
hτ : Γ ⊢[T] LambdaTerm.pair a✝² a✝¹ a✝ ∶ τ
⊢ σ = τ

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

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

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

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

case case
p : LambdaParams
U : Type ?u.145218
C : Type ?u.145221
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✝² ∶ σ) → (Γ ⊢[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✝ ∶ σ
hτ : Γ ⊢[T] LambdaTerm.case a✝³ a✝² a✝¹ a✝ ∶ τ
⊢ σ = τ

case star
p : LambdaParams
U : Type ?u.145218
C : Type ?u.145221
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✝ ∶ σ
hτ : Γ ⊢[T] LambdaTerm.star a✝ ∶ τ
⊢ σ = τ

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