contradiction
case h_1
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
heq✝ : type (↥ctx)[0 ↦ ty✝] body✝ = none
h : none = some ty
⊢ ctx ⊢ Term.abs ty✝ body✝ ⋮ ty
no goals