case app t₁ t₂ hi₁ hi₂ =>
  cases h₁ : type ctx t₁ <;> cases h₂ : type ctx t₂ <;> simp_all [h₁, h₂]
  all_goals split at h <;> try contradiction
  case _ ty₁ ty₂ _ ty₁₁ _ ha =>
    specialize hi₁ h₁
    split at h <;> simp_all
    exact .app hi₁ (hi₂ 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
no goals