case abs ty₁ ctx t ty₂ ht hi =>
  refine .abs ?_
  rw [←Ctx.shift_set_comm] at hi
  simp at *
  sorry
ctx✝ : Ctx
t✝ : Term
ty ty₁ : Ty
ctx : Ctx
t : Term
ty₂ : Ty
ht : (↥ctx)[0 ↦ ty₁] ⊢ t ⋮ ty₂
hi : ↥(↥ctx)[0 ↦ ty₁] ⊢ Term.shift Dir.up 0 t ⋮ ty₂
⊢ ↥ctx ⊢ Term.shift Dir.up 0 (Term.abs ty₁ t) ⋮ Ty.arrow ty₁ ty₂
no goals