induction ht generalizing ctx x s <;> (subst hc; try simp at *)
x : Nat
ty' : Ty
ctx : Ctx
t : Term
ty : Ty
s : Term
hs : ctx ⊢ s ⋮ ty'
ctx' : Ctx
ht : ctx' ⊢ t ⋮ ty
hc : ctx[x ↦ ty'] = ctx'
⊢ ctx ⊢ t[x ↦ s] ⋮ ty
case var
ty' : Ty
t : Term
ty : Ty
ctx' : Ctx
ty✝ : Ty
x✝ x : Nat
ctx : Ctx
s : Term
hs : ctx ⊢ s ⋮ ty'
a✝ : ctx[x ↦ ty'] x✝ = some ty✝
⊢ ctx ⊢ (Term.var x✝)[x ↦ s] ⋮ ty✝

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

case app
ty' : Ty
t : Term
ty : Ty
ctx' : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
x : Nat
ctx : Ctx
s : Term
hs : ctx ⊢ s ⋮ ty'
a✝¹ : ctx[x ↦ ty'] ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ctx[x ↦ ty'] ⊢ t₂✝ ⋮ ty₁✝
a_ih✝¹ :
  ∀ {x_1 : Nat} {ctx_1 : Ctx} {s : Term},
    (ctx_1 ⊢ s ⋮ ty') → ctx_1[x_1 ↦ ty'] = ctx[x ↦ ty'] → ctx_1 ⊢ t₁✝[x_1 ↦ s] ⋮ Ty.arrow ty₁✝ ty₂✝
a_ih✝ :
  ∀ {x_1 : Nat} {ctx_1 : Ctx} {s : Term},
    (ctx_1 ⊢ s ⋮ ty') → ctx_1[x_1 ↦ ty'] = ctx[x ↦ ty'] → ctx_1 ⊢ t₂✝[x_1 ↦ s] ⋮ ty₁✝
⊢ ctx ⊢ (Term.app t₁✝ t₂✝)[x ↦ s] ⋮ ty₂✝