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

State before:
p : LambdaParams
U : Type ?u.25589
C : Type ?u.25592
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.unit = true
σ : LambdaType p✝ U✝
⊢ (Γ ⊢[T] LambdaTerm.star h ∶ σ) ↔ σ = LambdaType.unit h
Tactic:
constructor
State after:
case mp
p : LambdaParams
U : Type ?u.25589
C : Type ?u.25592
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.unit = true
σ : LambdaType p✝ U✝
⊢ (Γ ⊢[T] LambdaTerm.star h ∶ σ) → σ = LambdaType.unit h

case mpr
p : LambdaParams
U : Type ?u.25589
C : Type ?u.25592
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.unit = true
σ : LambdaType p✝ U✝
⊢ σ = LambdaType.unit h → (Γ ⊢[T] LambdaTerm.star h ∶ σ)

State before:
case mp
p : LambdaParams
U : Type ?u.25589
C : Type ?u.25592
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.unit = true
σ : LambdaType p✝ U✝
⊢ (Γ ⊢[T] LambdaTerm.star h ∶ σ) → σ = LambdaType.unit h
Tactic:
intro h
State after:
case mp
p : LambdaParams
U : Type ?u.25589
C : Type ?u.25592
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h✝ : p✝.unit = true
σ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.star h✝ ∶ σ
⊢ σ = LambdaType.unit h✝

State before:
case mp
p : LambdaParams
U : Type ?u.25589
C : Type ?u.25592
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h✝ : p✝.unit = true
σ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.star h✝ ∶ σ
⊢ σ = LambdaType.unit h✝
Tactic:
cases h
State after:
case mp.star
p : LambdaParams
U : Type ?u.25589
C : Type ?u.25592
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h h✝ : p✝.unit = true
⊢ LambdaType.unit h✝ = LambdaType.unit h

State before:
case mp.star
p : LambdaParams
U : Type ?u.25589
C : Type ?u.25592
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h h✝ : p✝.unit = true
⊢ LambdaType.unit h✝ = LambdaType.unit h
Tactic:
rfl
State after:
no goals

State before:
case mpr
p : LambdaParams
U : Type ?u.25589
C : Type ?u.25592
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.unit = true
σ : LambdaType p✝ U✝
⊢ σ = LambdaType.unit h → (Γ ⊢[T] LambdaTerm.star h ∶ σ)
Tactic:
rintro rfl
State after:
case mpr
p : LambdaParams
U : Type ?u.25589
C : Type ?u.25592
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.unit = true
⊢ Γ ⊢[T] LambdaTerm.star h ∶ LambdaType.unit h

State before:
case mpr
p : LambdaParams
U : Type ?u.25589
C : Type ?u.25592
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.unit = true
⊢ Γ ⊢[T] LambdaTerm.star h ∶ LambdaType.unit h
Tactic:
exact .star
State after:
no goals