case app hi₁ hi₂ => exact .app hi₁ hi₂
ctx : Ctx
t : Term
ty : Ty
ctx✝ : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ctx✝ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ctx✝ ⊢ t₂✝ ⋮ ty₁✝
hi₁ : ↥ctx✝ ⊢ Term.shift Dir.up 0 t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
hi₂ : ↥ctx✝ ⊢ Term.shift Dir.up 0 t₂✝ ⋮ ty₁✝
⊢ ↥ctx✝ ⊢ Term.shift Dir.up 0 (Term.app t₁✝ t₂✝) ⋮ ty₂✝
no goals