case abs ty₁ t₁ _ _ _ => exact .inl ⟨⟨_, _⟩, rfl, rfl⟩
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'
no goals