generalize hc : ↥ctx = ctx'
ctx : Ctx
t : Term
ty : Ty
h : ↥ctx ⊢ t ⋮ ty
⊢ ctx ⊢ Term.shift Dir.down 0 t ⋮ ty
ctx : Ctx
t : Term
ty : Ty
h : ↥ctx ⊢ t ⋮ ty
ctx' : Ctx
hc : ↥ctx = ctx'
⊢ ctx ⊢ Term.shift Dir.down 0 t ⋮ ty