rw [hc] at h
ctx : Ctx
t : Term
ty : Ty
h : ↥ctx ⊢ t ⋮ ty
ctx' : Ctx
hc : ↥ctx = ctx'
⊢ ctx ⊢ Term.shift Dir.down 0 t ⋮ ty
ctx : Ctx
t : Term
ty : Ty
ctx' : Ctx
h : ctx' ⊢ t ⋮ ty
hc : ↥ctx = ctx'
⊢ ctx ⊢ Term.shift Dir.down 0 t ⋮ ty