rw [(↥ctx).set_ne_comm 0 (x + 1), ctx.shift_set_comm x] at hi
ctx✝ : Ctx
t : Term
ty ty' ty₁✝ : Ty
ctx : Ctx
t✝ : Term
ty₂✝ : Ty
a✝ : (↥ctx)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
x : Nat
hx : ctx x = none
hi : (↥ctx)[0 ↦ ty₁✝][x + 1 ↦ ty'] ⊢ t✝ ⋮ ty₂✝
⊢ ctx[x ↦ ty'] ⊢ Term.abs ty₁✝ t✝ ⋮ Ty.arrow ty₁✝ ty₂✝
ctx✝ : Ctx
t : Term
ty ty' ty₁✝ : Ty
ctx : Ctx
t✝ : Term
ty₂✝ : Ty
a✝ : (↥ctx)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
x : Nat
hx : ctx x = none
hi : (↥ctx[x ↦ ty'])[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
⊢ ctx[x ↦ ty'] ⊢ Term.abs ty₁✝ t✝ ⋮ Ty.arrow ty₁✝ ty₂✝