case app hi₁ hi₂ =>
  cases hi₁ <;> apply Or.inr
  case inr h =>
    have ⟨_, h⟩ := h
    exact ⟨_, .app₁ _ h⟩
  case inl ty₁ _ _ ht₁ _ h₁ =>
    cases hi₂ 
    case inl h₂ =>
      have ⟨v₁, hv₁⟩ := h₁ 
      have ⟨v₂, hv₂⟩ := h₂
      subst hv₁ hv₂
      have ⟨body₁, hv₁⟩ := canonical_forms ht₁
      subst hv₁
      exact ⟨_, .beta ..⟩ 
    case inr h₂ =>
      have ⟨_, h₁⟩ := h₁
      have ⟨_, h₂⟩ := h₂
      subst h₁
      exact ⟨_, .app₂ _ 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'
hi₂ : (∃ v, t₂✝ = Term.abs v.1 v.2) ∨ ∃ t', t₂✝ ⇒ t'
⊢ (∃ v, False) ∨ ∃ t', Term.app t₁✝ t₂✝ ⇒ t'
no goals