Theorem: uniqueness (STLC.lean)

State before:
ctx : Ctx
t : Term
ty₁ ty₂ : Ty
h₁ : ctx ⊢ t ⋮ ty₁
h₂ : ctx ⊢ t ⋮ ty₂
⊢ ty₁ = ty₂
Tactic:
induction h₁ generalizing ty₂ <;> cases h₂
State after:
case var.var
ctx : Ctx
t : Term
ty₁ : Ty
ctx✝ : Ctx
ty✝ : Ty
x✝ : Nat
a✝¹ : ctx✝ x✝ = some ty✝
ty₂ : Ty
a✝ : ctx✝ x✝ = some ty₂
⊢ ty✝ = ty₂

case abs.abs
ctx : Ctx
t : Term
ty₁ ty₁✝ : Ty
ctx✝ : Ctx
t✝ : Term
ty₂✝¹ : Ty
a✝¹ : (↥ctx✝)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝¹
a_ih✝ : ∀ {ty₂ : Ty}, ((↥ctx✝)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂) → ty₂✝¹ = ty₂
ty₂✝ : Ty
a✝ : (↥ctx✝)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
⊢ Ty.arrow ty₁✝ ty₂✝¹ = Ty.arrow ty₁✝ ty₂✝

case app.app
ctx : Ctx
t : Term
ty₁ : Ty
ctx✝ : Ctx
t₁✝ : Term
ty₁✝¹ ty₂✝ : Ty
t₂✝ : Term
a✝³ : ctx✝ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝¹ ty₂✝
a✝² : ctx✝ ⊢ t₂✝ ⋮ ty₁✝¹
a_ih✝¹ : ∀ {ty₂ : Ty}, (ctx✝ ⊢ t₁✝ ⋮ ty₂) → Ty.arrow ty₁✝¹ ty₂✝ = ty₂
a_ih✝ : ∀ {ty₂ : Ty}, (ctx✝ ⊢ t₂✝ ⋮ ty₂) → ty₁✝¹ = ty₂
ty₂ ty₁✝ : Ty
a✝¹ : ctx✝ ⊢ t₂✝ ⋮ ty₁✝
a✝ : ctx✝ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂
⊢ ty₂✝ = ty₂

State before:
ctx : Ctx
t : Term
ty₁ : Ty
ctx✝ : Ctx
ty✝ : Ty
x✝ : Nat
h₁ : ctx✝ x✝ = some ty✝
ty₂ : Ty
h₂ : ctx✝ x✝ = some ty₂
⊢ ty✝ = ty₂
Tactic:
case var.var h₁ h₂      => injection h₁ ▸ h₂
State after:
no goals

State before:
ctx : Ctx
t : Term
ty₁ ty₁✝ : Ty
ctx✝ : Ctx
t✝ : Term
ty₂✝¹ : Ty
a✝ : (↥ctx✝)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝¹
hi : ∀ {ty₂ : Ty}, ((↥ctx✝)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂) → ty₂✝¹ = ty₂
ty₂✝ : Ty
h : (↥ctx✝)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
⊢ Ty.arrow ty₁✝ ty₂✝¹ = Ty.arrow ty₁✝ ty₂✝
Tactic:
case abs.abs hi _ h     => rw [hi h]
State after:
no goals

State before:
ctx : Ctx
t : Term
ty₁ : Ty
ctx✝ : Ctx
t₁✝ : Term
ty₁✝¹ ty₂✝ : Ty
t₂✝ : Term
a✝² : ctx✝ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝¹ ty₂✝
a✝¹ : ctx✝ ⊢ t₂✝ ⋮ ty₁✝¹
hi : ∀ {ty₂ : Ty}, (ctx✝ ⊢ t₁✝ ⋮ ty₂) → Ty.arrow ty₁✝¹ ty₂✝ = ty₂
a_ih✝ : ∀ {ty₂ : Ty}, (ctx✝ ⊢ t₂✝ ⋮ ty₂) → ty₁✝¹ = ty₂
ty₂ ty₁✝ : Ty
a✝ : ctx✝ ⊢ t₂✝ ⋮ ty₁✝
h : ctx✝ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂
⊢ ty₂✝ = ty₂
Tactic:
case app.app hi _ _ _ h => injection hi h
State after:
no goals

State before:
ctx : Ctx
t : Term
ty₁ : Ty
ctx✝ : Ctx
ty✝ : Ty
x✝ : Nat
h₁ : ctx✝ x✝ = some ty✝
ty₂ : Ty
h₂ : ctx✝ x✝ = some ty₂
⊢ ty✝ = ty₂
Tactic:
injection h₁ ▸ h₂
State after:
no goals

State before:
ctx : Ctx
t : Term
ty₁ ty₁✝ : Ty
ctx✝ : Ctx
t✝ : Term
ty₂✝¹ : Ty
a✝ : (↥ctx✝)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝¹
hi : ∀ {ty₂ : Ty}, ((↥ctx✝)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂) → ty₂✝¹ = ty₂
ty₂✝ : Ty
h : (↥ctx✝)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
⊢ Ty.arrow ty₁✝ ty₂✝¹ = Ty.arrow ty₁✝ ty₂✝
Tactic:
rw [hi h]
State after:
no goals

State before:
ctx : Ctx
t : Term
ty₁ : Ty
ctx✝ : Ctx
t₁✝ : Term
ty₁✝¹ ty₂✝ : Ty
t₂✝ : Term
a✝² : ctx✝ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝¹ ty₂✝
a✝¹ : ctx✝ ⊢ t₂✝ ⋮ ty₁✝¹
hi : ∀ {ty₂ : Ty}, (ctx✝ ⊢ t₁✝ ⋮ ty₂) → Ty.arrow ty₁✝¹ ty₂✝ = ty₂
a_ih✝ : ∀ {ty₂ : Ty}, (ctx✝ ⊢ t₂✝ ⋮ ty₂) → ty₁✝¹ = ty₂
ty₂ ty₁✝ : Ty
a✝ : ctx✝ ⊢ t₂✝ ⋮ ty₁✝
h : ctx✝ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂
⊢ ty₂✝ = ty₂
Tactic:
injection hi h
State after:
no goals