cases v
ty₁ ty₂ : Ty
v : Value
h :
  ∅ ⊢
    match v with
    | Value.abs ty body => Term.abs ty body ⋮
    Ty.arrow ty₁ ty₂
⊢ ∃ t, v = Value.abs ty₁ t
case abs
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