cases h₁ : type ctx t₁ <;> cases h₂ : type ctx t₂ <;> simp_all [h₁, h₂]
t₁ t₂ : Term
hi₁ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₁ = some ty → ctx ⊢ t₁ ⋮ ty
hi₂ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₂ = some ty → ctx ⊢ t₂ ⋮ ty
ctx : Ctx
ty : Ty
h :
  (match type ctx t₁ with
    | some (Ty.arrow ty₁ ty₂) =>
      match type ctx t₂, fun __do_lift => if ty₁ = __do_lift then some ty₂ else none with
      | none, x => none
      | some a, b => b a
    | x => none) =
    some ty
⊢ ctx ⊢ Term.app t₁ t₂ ⋮ ty
case some.none
t₁ t₂ : Term
hi₁ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₁ = some ty → ctx ⊢ t₁ ⋮ ty
hi₂ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₂ = some ty → ctx ⊢ t₂ ⋮ ty
ctx : Ctx
ty val✝ : Ty
h :
  (match some val✝ with
    | some (Ty.arrow ty₁ ty₂) => none
    | x => none) =
    some ty
h₁ : type ctx t₁ = some val✝
h₂ : type ctx t₂ = none
⊢ ctx ⊢ Term.app t₁ t₂ ⋮ ty

case some.some
t₁ t₂ : Term
hi₁ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₁ = some ty → ctx ⊢ t₁ ⋮ ty
hi₂ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₂ = some ty → ctx ⊢ t₂ ⋮ ty
ctx : Ctx
ty val✝¹ val✝ : Ty
h :
  (match some val✝¹ with
    | some (Ty.arrow ty₁ ty₂) => if ty₁ = val✝ then some ty₂ else none
    | x => none) =
    some ty
h₁ : type ctx t₁ = some val✝¹
h₂ : type ctx t₂ = some val✝
⊢ ctx ⊢ Term.app t₁ t₂ ⋮ ty