case inl h => simp_all
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✝
no goals