rw [hi]
ctx : Ctx
t : Term
ty ty₁✝ : Ty
ctx✝ : Ctx
t✝ : Term
ty₂✝ : Ty
a✝ : (↥ctx✝)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
hi : type (↥ctx✝)[0 ↦ ty₁✝] t✝ = some ty₂✝
⊢ (do
      let __do_lift ← type (↥ctx✝)[0 ↦ ty₁✝] t✝
      pure (Ty.arrow ty₁✝ __do_lift)) =
    some (Ty.arrow ty₁✝ ty₂✝)
ctx : Ctx
t : Term
ty ty₁✝ : Ty
ctx✝ : Ctx
t✝ : Term
ty₂✝ : Ty
a✝ : (↥ctx✝)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
hi : type (↥ctx✝)[0 ↦ ty₁✝] t✝ = some ty₂✝
⊢ (do
      let __do_lift ← some ty₂✝
      pure (Ty.arrow ty₁✝ __do_lift)) =
    some (Ty.arrow ty₁✝ ty₂✝)