subst h
ty✝ : Ty
body✝ : Term
hi : ∀ {ctx : Ctx} {ty : Ty}, type ctx body✝ = some ty → ctx ⊢ body✝ ⋮ ty
ctx : Ctx
ty : Ty
x✝¹ : Option Ty
x✝ : Ty → Option Ty
a✝ : Ty
ht : type (↥ctx)[0 ↦ ty✝] body✝ = some a✝
h : Ty.arrow ty✝ a✝ = ty
⊢ ctx ⊢ Term.abs ty✝ body✝ ⋮ ty
ty✝ : Ty
body✝ : Term
hi : ∀ {ctx : Ctx} {ty : Ty}, type ctx body✝ = some ty → ctx ⊢ body✝ ⋮ ty
ctx : Ctx
x✝¹ : Option Ty
x✝ : Ty → Option Ty
a✝ : Ty
ht : type (↥ctx)[0 ↦ ty✝] body✝ = some a✝
⊢ ctx ⊢ Term.abs ty✝ body✝ ⋮ Ty.arrow ty✝ a✝