simp at *
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₁✝ =
          match v with
          | Value.abs ty body => Term.abs ty body) ∨
      ∃ t', t₁✝ ⇒ t'
a_ih✝ :
  ∅ = ∅ →
    (∃ v,
        t₂✝ =
          match v with
          | Value.abs ty body => Term.abs ty body) ∨
      ∃ t', t₂✝ ⇒ t'
⊢ (∃ v,
      Term.app t₁✝ t₂✝ =
        match v with
        | Value.abs ty body => Term.abs ty body) ∨
    ∃ t', Term.app t₁✝ 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'