case abs body =>
  simp at h
  exists body
  have ⟨_, h, _⟩ := inversion_abs h
  injection h with h
  rw [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
no goals