induction h <;> (subst hc; simp at *)
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'
case var
t : Term
ty : Ty
ctx : Ctx
ty✝ : Ty
x✝ : Nat
a✝ : ∅ x✝ = some ty✝
⊢ (∃ v, False) ∨ ∃ t', Term.var x✝ ⇒ t'

case abs
t : Term
ty : Ty
ctx : Ctx
ty₁✝ : Ty
t✝ : Term
ty₂✝ : Ty
a✝ : (↥∅)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
a_ih✝ : ∅ = (↥∅)[0 ↦ ty₁✝] → (∃ v, t✝ = Term.abs v.1 v.2) ∨ ∃ t', t✝ ⇒ t'
⊢ (∃ v, ty₁✝ = v.1 ∧ t✝ = v.2) ∨ ∃ t', Term.abs ty₁✝ t✝ ⇒ t'

case app
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁✝
a_ih✝¹ : (∃ v, t₁✝ = Term.abs v.1 v.2) ∨ ∃ t', t₁✝ ⇒ t'
a_ih✝ : (∃ v, t₂✝ = Term.abs v.1 v.2) ∨ ∃ t', t₂✝ ⇒ t'
⊢ (∃ v, False) ∨ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'