case var h =>
  simp_all [Term.shift, Ctx.shift, Dir.move]
  split <;> try split at h <;> try contradiction
  exact .var h
ctx : Ctx
t : Term
ty : Ty
ctx' : Ctx
ty✝ : Ty
x✝ : Nat
h : ↥ctx x✝ = some ty✝
⊢ ctx ⊢ Term.shift Dir.down 0 (Term.var x✝) ⋮ ty✝
no goals