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