rw [←ctx.shift_set_comm, (↥ctx).set_ne_comm 0 (x + 1)]
case refine_2
ty' : Ty
t : Term
ty : Ty
ctx' : Ctx
ty₁ : Ty
t✝ : Term
ty₂✝ : Ty
x : Nat
ctx : Ctx
s : Term
hs : ctx ⊢ s ⋮ ty'
a✝ : (↥ctx[x ↦ ty'])[0 ↦ ty₁] ⊢ t✝ ⋮ ty₂✝
hi :
  ∀ {x_1 : Nat} {ctx_1 : Ctx} {s : Term},
    (ctx_1 ⊢ s ⋮ ty') → ctx_1[x_1 ↦ ty'] = (↥ctx[x ↦ ty'])[0 ↦ ty₁] → ctx_1 ⊢ t✝[x_1 ↦ s] ⋮ ty₂✝
⊢ (↥ctx)[0 ↦ ty₁][x + 1 ↦ ty'] = (↥ctx[x ↦ ty'])[0 ↦ ty₁]
no goals