simp [hi₁, hi₂]
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₁✝
hi₁ : type ctx✝ t₁✝ = some (Ty.arrow ty₁✝ ty₂✝)
hi₂ : type ctx✝ t₂✝ = some ty₁✝
⊢ (match type ctx✝ t₁✝ with
    | some (Ty.arrow ty₁ ty₂) => do
      let __do_lift ← type ctx✝ t₂✝
      if ty₁ = __do_lift then some ty₂ else none
    | x => none) =
    some ty₂✝
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₁✝
hi₁ : type ctx✝ t₁✝ = some (Ty.arrow ty₁✝ ty₂✝)
hi₂ : type ctx✝ t₂✝ = some ty₁✝
⊢ (do
      let __do_lift ← some ty₁✝
      if ty₁✝ = __do_lift then some ty₂✝ else none) =
    some ty₂✝