simp at *
ctx✝ : Ctx
t✝ : Term
ty ty₁ : Ty
ctx : Ctx
t : Term
ty₂ : Ty
ht : (↥ctx)[0 ↦ ty₁] ⊢ t ⋮ ty₂
hi : (↥↥ctx)[0 + 1 ↦ ty₁] ⊢ Term.shift Dir.up 0 t ⋮ ty₂
⊢ (↥↥ctx)[0 ↦ ty₁] ⊢ Term.shift Dir.up (0 + 1) t ⋮ ty₂
ctx✝ : Ctx
t✝ : Term
ty ty₁ : Ty
ctx : Ctx
t : Term
ty₂ : Ty
ht : (↥ctx)[0 ↦ ty₁] ⊢ t ⋮ ty₂
hi : (↥↥ctx)[1 ↦ ty₁] ⊢ Term.shift Dir.up 0 t ⋮ ty₂
⊢ (↥↥ctx)[0 ↦ ty₁] ⊢ Term.shift Dir.up 1 t ⋮ ty₂