contradiction
case some.some.h_2
t₁ t₂ : Term
hi₁ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₁ = some ty → ctx ⊢ t₁ ⋮ ty
hi₂ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₂ = some ty → ctx ⊢ t₂ ⋮ ty
ctx : Ctx
ty val✝¹ val✝ : Ty
h₁ : type ctx t₁ = some val✝¹
h₂ : type ctx t₂ = some val✝
x✝¹ : Option Ty
x✝ : ∀ (ty₁ ty₂ : Ty), some val✝¹ = some (Ty.arrow ty₁ ty₂) → False
h : none = some ty
⊢ ctx ⊢ Term.app t₁ t₂ ⋮ ty
no goals