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