have ⟨_, h₂⟩ := h₂
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁ ty₂✝ : Ty
t₂✝ : Term
ht₁ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁
h₁✝ : ∃ v, t₁✝ = Term.abs v.1 v.2
h₂ : ∃ t', t₂✝ ⇒ t'
w✝ : Value
h₁ : t₁✝ = Term.abs w✝.1 w✝.2
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁ ty₂✝ : Ty
t₂✝ : Term
ht₁ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁
h₁✝ : ∃ v, t₁✝ = Term.abs v.1 v.2
h₂✝ : ∃ t', t₂✝ ⇒ t'
w✝¹ : Value
h₁ : t₁✝ = Term.abs w✝¹.1 w✝¹.2
w✝ : Term
h₂ : t₂✝ ⇒ w✝
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'