rw [hc] at h
t : Term
ty : Ty
h : ∅ ⊢ t ⋮ ty
ctx : Ctx
hc : ∅ = ctx
⊢ (∃ v,
      t =
        match v with
        | Value.abs ty body => Term.abs ty body) ∨
    ∃ t', t ⇒ t'
t : Term
ty : Ty
ctx : Ctx
h : ctx ⊢ t ⋮ ty
hc : ∅ = ctx
⊢ (∃ v,
      t =
        match v with
        | Value.abs ty body => Term.abs ty body) ∨
    ∃ t', t ⇒ t'