case var hc =>
  simp [Term.subst]
  split <;> simp [Ctx.set] at hc
  case inl h => simp_all
  case inr h => exact .var <| by simp_all
ty' : Ty
t : Term
ty : Ty
ctx' : Ctx
ty✝ : Ty
x✝ x : Nat
ctx : Ctx
s : Term
hs : ctx ⊢ s ⋮ ty'
hc : ctx[x ↦ ty'] x✝ = some ty✝
⊢ ctx ⊢ (Term.var x✝)[x ↦ s] ⋮ ty✝
no goals