case app hi₁ hi₂ => exact .app (hi₁ hs rfl) (hi₂ hs rfl)
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₁✝
hi₁ :
  ∀ {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₂✝
hi₂ :
  ∀ {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₂✝
no goals