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