exact .app (hi₁ hx) (hi₂ hx)
ctx : Ctx
t : Term
ty ty' : Ty
ctx✝ : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ctx✝ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ctx✝ ⊢ t₂✝ ⋮ ty₁✝
hi₁ : ∀ {x : Nat}, ctx✝ x = none → ctx✝[x ↦ ty'] ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
hi₂ : ∀ {x : Nat}, ctx✝ x = none → ctx✝[x ↦ ty'] ⊢ t₂✝ ⋮ ty₁✝
x : Nat
hx : ctx✝ x = none
⊢ ctx✝[x ↦ ty'] ⊢ Term.app t₁✝ t₂✝ ⋮ ty₂✝
no goals