induction h₁ generalizing ty₂ <;> cases h₂
ctx : Ctx
t : Term
ty₁ ty₂ : Ty
h₁ : ctx ⊢ t ⋮ ty₁
h₂ : ctx ⊢ t ⋮ ty₂
⊢ ty₁ = ty₂
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₂