simp_all [Term.shift, Ctx.shift, Dir.move]
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✝
ctx : Ctx
t : Term
ty : Ty
ctx' : Ctx
ty✝ : Ty
x✝ : Nat
h :
  (match x✝ with
    | 0 => none
    | Nat.succ x => ctx x) =
    some ty✝
⊢ ctx ⊢ if x✝ < 0 then Term.var x✝ else Term.var (x✝ - 1) ⋮ ty✝