split <;> simp [Ctx.set] at hc
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 ⊢ if x✝ = x then s else Term.var x✝ ⋮ ty✝
case inl
ty' : Ty
t : Term
ty : Ty
ctx' : Ctx
ty✝ : Ty
x✝ x : Nat
ctx : Ctx
s : Term
hs : ctx ⊢ s ⋮ ty'
hc : (if x✝ = x then some ty' else ctx x✝) = some ty✝
h✝ : x✝ = x
⊢ ctx ⊢ s ⋮ ty✝

case inr
ty' : Ty
t : Term
ty : Ty
ctx' : Ctx
ty✝ : Ty
x✝ x : Nat
ctx : Ctx
s : Term
hs : ctx ⊢ s ⋮ ty'
hc : (if x✝ = x then some ty' else ctx x✝) = some ty✝
h✝ : ¬x✝ = x
⊢ ctx ⊢ Term.var x✝ ⋮ ty✝