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