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
ht₁ : ∅ ⊢ 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'
no goals