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 : (if x✝ = x then some ty' else ctx x✝) = some ty✝
h : ¬x✝ = x
⊢ ctx ⊢ Term.var x✝ ⋮ ty✝
no goals