case abs => 
  sorry
ctx : Ctx
t : Term
ty : Ty
ctx' : Ctx
ty₁✝ : Ty
t✝ : Term
ty₂✝ : Ty
a✝ : (↥↥ctx)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
a_ih✝ : ↥ctx = (↥↥ctx)[0 ↦ ty₁✝] → ctx ⊢ Term.shift Dir.down 0 t✝ ⋮ ty₂✝
⊢ ctx ⊢ Term.shift Dir.down 0 (Term.abs ty₁✝ t✝) ⋮ Ty.arrow ty₁✝ ty₂✝
no goals