exists body
ty₁ ty₂ ty✝ : Ty
body : Term
h : ∅ ⊢ Term.abs ty✝ body ⋮ Ty.arrow ty₁ ty₂
⊢ ∃ t, Value.abs ty✝ body = Value.abs ty₁ t
ty₁ ty₂ ty✝ : Ty
body : Term
h : ∅ ⊢ Term.abs ty✝ body ⋮ Ty.arrow ty₁ ty₂
⊢ Value.abs ty✝ body = Value.abs ty₁ body