induction h <;> (subst hc; try simp at *)
ctx : Ctx
t : Term
ty : Ty
ctx' : Ctx
h : ctx' ⊢ t ⋮ ty
hc : ↥ctx = ctx'
⊢ ctx ⊢ Term.shift Dir.down 0 t ⋮ ty
case var
ctx : Ctx
t : Term
ty : Ty
ctx' : Ctx
ty✝ : Ty
x✝ : Nat
a✝ : ↥ctx x✝ = some ty✝
⊢ ctx ⊢ Term.shift Dir.down 0 (Term.var x✝) ⋮ ty✝

case abs
ctx : Ctx
t : Term
ty : Ty
ctx' : Ctx
ty₁✝ : Ty
t✝ : Term
ty₂✝ : Ty
a✝ : (↥↥ctx)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
a_ih✝ : ↥ctx = (↥↥ctx)[0 ↦ ty₁✝] → ctx ⊢ Term.shift Dir.down 0 t✝ ⋮ ty₂✝
⊢ ctx ⊢ Term.shift Dir.down 0 (Term.abs ty₁✝ t✝) ⋮ Ty.arrow ty₁✝ ty₂✝

case app
ctx : Ctx
t : Term
ty : Ty
ctx' : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ↥ctx ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ↥ctx ⊢ t₂✝ ⋮ ty₁✝
a_ih✝¹ : ctx ⊢ Term.shift Dir.down 0 t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a_ih✝ : ctx ⊢ Term.shift Dir.down 0 t₂✝ ⋮ ty₁✝
⊢ ctx ⊢ Term.shift Dir.down 0 (Term.app t₁✝ t₂✝) ⋮ ty₂✝