induction t generalizing ty ctx <;> simp [type, bind, Option.bind] at h
ctx : Ctx
t : Term
ty : Ty
h : type ctx t = some ty
⊢ ctx ⊢ t ⋮ ty
case var
fvar✝ : Nat
ctx : Ctx
ty : Ty
h : ctx fvar✝ = some ty
⊢ ctx ⊢ Term.var fvar✝ ⋮ ty

case abs
ty✝ : Ty
body✝ : Term
body_ih✝ : ∀ {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

case app
t₁✝ t₂✝ : Term
t₁_ih✝ : ∀ {ctx : Ctx} {ty : Ty}, type ctx t₁✝ = some ty → ctx ⊢ t₁✝ ⋮ ty
t₂_ih✝ : ∀ {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