induction ht generalizing x
ctx : Ctx
t : Term
ty : Ty
x : Nat
ty' : Ty
ht : ctx ⊢ t ⋮ ty
hx : ctx x = none
⊢ ctx[x ↦ ty'] ⊢ t ⋮ ty
case var
ctx : Ctx
t : Term
ty ty' : Ty
ctx✝ : Ctx
ty✝ : Ty
x✝ : Nat
a✝ : ctx✝ x✝ = some ty✝
x : Nat
hx : ctx✝ x = none
⊢ ctx✝[x ↦ ty'] ⊢ Term.var x✝ ⋮ ty✝

case abs
ctx : Ctx
t : Term
ty ty' ty₁✝ : Ty
ctx✝ : Ctx
t✝ : Term
ty₂✝ : Ty
a✝ : (↥ctx✝)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
a_ih✝ : ∀ {x : Nat}, (↥ctx✝)[0 ↦ ty₁✝] x = none → (↥ctx✝)[0 ↦ ty₁✝][x ↦ ty'] ⊢ t✝ ⋮ ty₂✝
x : Nat
hx : ctx✝ x = none
⊢ ctx✝[x ↦ ty'] ⊢ Term.abs ty₁✝ t✝ ⋮ Ty.arrow ty₁✝ ty₂✝

case app
ctx : Ctx
t : Term
ty ty' : Ty
ctx✝ : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ctx✝ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ctx✝ ⊢ t₂✝ ⋮ ty₁✝
a_ih✝¹ : ∀ {x : Nat}, ctx✝ x = none → ctx✝[x ↦ ty'] ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a_ih✝ : ∀ {x : Nat}, ctx✝ x = none → ctx✝[x ↦ ty'] ⊢ t₂✝ ⋮ ty₁✝
x : Nat
hx : ctx✝ x = none
⊢ ctx✝[x ↦ ty'] ⊢ Term.app t₁✝ t₂✝ ⋮ ty₂✝