rw [hc] at ht
x : Nat
ty' : Ty
ctx : Ctx
t : Term
ty : Ty
s : Term
ht : ctx[x ↦ ty'] ⊢ t ⋮ ty
hs : ctx ⊢ s ⋮ ty'
ctx' : Ctx
hc : ctx[x ↦ ty'] = ctx'
⊢ ctx ⊢ t[x ↦ s] ⋮ ty
x : Nat
ty' : Ty
ctx : Ctx
t : Term
ty : Ty
s : Term
hs : ctx ⊢ s ⋮ ty'
ctx' : Ctx
ht : ctx' ⊢ t ⋮ ty
hc : ctx[x ↦ ty'] = ctx'
⊢ ctx ⊢ t[x ↦ s] ⋮ ty