refine .var (hy ▸ ctx.set_get_ne _ _ ?_)
ctx✝ : Ctx
t : Term
ty ty' : Ty
ctx : Ctx
ty✝ : Ty
y : Nat
hy : ctx y = some ty✝
x : Nat
hx : ctx x = none
⊢ ctx[x ↦ ty'] ⊢ Term.var y ⋮ ty✝
ctx✝ : Ctx
t : Term
ty ty' : Ty
ctx : Ctx
ty✝ : Ty
y : Nat
hy : ctx y = some ty✝
x : Nat
hx : ctx x = none
⊢ x ≠ y