try simp at *
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 = ↥ctx → ctx ⊢ Term.shift Dir.down 0 t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a_ih✝ : ↥ctx = ↥ctx → ctx ⊢ Term.shift Dir.down 0 t₂✝ ⋮ ty₁✝
⊢ ctx ⊢ Term.shift Dir.down 0 (Term.app t₁✝ t₂✝) ⋮ 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₂✝