simp at h
ty₁ ty₂ ty✝ : Ty
body : Term
h :
  ∅ ⊢
    match Value.abs ty✝ body with
    | Value.abs ty body => 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₂
⊢ ∃ t, Value.abs ty✝ body = Value.abs ty₁ t