case abs hi => 
  split at h <;> try contradiction
  case _ ht =>
    simp [pure] at h
    subst h
    exact .abs (hi ht)
ty✝ : Ty
body✝ : Term
hi : ∀ {ctx : Ctx} {ty : Ty}, type ctx body✝ = some ty → ctx ⊢ body✝ ⋮ ty
ctx : Ctx
ty : Ty
h :
  (match type (↥ctx)[0 ↦ ty✝] body✝, fun __do_lift => pure (Ty.arrow ty✝ __do_lift) with
    | none, x => none
    | some a, b => b a) =
    some ty
⊢ ctx ⊢ Term.abs ty✝ body✝ ⋮ ty
no goals