induction h
ctx : Ctx
t : Term
ty : Ty
h : ctx ⊢ t ⋮ ty
⊢ ↥ctx ⊢ Term.shift Dir.up 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.up 0 (Term.var x✝) ⋮ ty✝

case abs
ctx : Ctx
t : Term
ty ty₁✝ : Ty
ctx✝ : Ctx
t✝ : Term
ty₂✝ : Ty
a✝ : (↥ctx✝)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
a_ih✝ : ↥(↥ctx✝)[0 ↦ ty₁✝] ⊢ Term.shift Dir.up 0 t✝ ⋮ ty₂✝
⊢ ↥ctx✝ ⊢ Term.shift Dir.up 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.up 0 t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a_ih✝ : ↥ctx✝ ⊢ Term.shift Dir.up 0 t₂✝ ⋮ ty₁✝
⊢ ↥ctx✝ ⊢ Term.shift Dir.up 0 (Term.app t₁✝ t₂✝) ⋮ ty₂✝