all_goals split at h <;> try contradiction
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
case some.some.h_1
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₁ : type ctx t₁ = some val✝¹
h₂ : type ctx t₂ = some val✝
x✝ : Option Ty
ty₁✝ ty₂✝ : Ty
heq✝ : some val✝¹ = some (Ty.arrow ty₁✝ ty₂✝)
h : (if ty₁✝ = val✝ then some ty₂✝ else none) = some ty
⊢ ctx ⊢ Term.app t₁ t₂ ⋮ ty