cases hi₁ <;> apply Or.inr
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁✝
hi₁ : (∃ v, t₁✝ = Term.abs v.1 v.2) ∨ ∃ t', t₁✝ ⇒ t'
hi₂ : (∃ v, t₂✝ = Term.abs v.1 v.2) ∨ ∃ t', t₂✝ ⇒ t'
⊢ (∃ v, False) ∨ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
case inl.h
t : Term
ty : Ty
ctx : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ∅ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ∅ ⊢ t₂✝ ⋮ ty₁✝
hi₂ : (∃ v, t₂✝ = Term.abs v.1 v.2) ∨ ∃ t', t₂✝ ⇒ t'
h✝ : ∃ v, t₁✝ = Term.abs v.1 v.2
⊢ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'

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