induction h <;> simp [type]
ctx : Ctx
t : Term
ty : Ty
h : ctx ⊢ t ⋮ ty
⊢ type ctx t = some ty
case var
ctx : Ctx
t : Term
ty : Ty
ctx✝ : Ctx
ty✝ : Ty
x✝ : Nat
a✝ : ctx✝ x✝ = some ty✝
⊢ ctx✝ x✝ = some ty✝

case abs
ctx : Ctx
t : Term
ty ty₁✝ : Ty
ctx✝ : Ctx
t✝ : Term
ty₂✝ : Ty
a✝ : (↥ctx✝)[0 ↦ ty₁✝] ⊢ t✝ ⋮ ty₂✝
a_ih✝ : type (↥ctx✝)[0 ↦ ty₁✝] t✝ = some ty₂✝
⊢ (do
      let __do_lift ← type (↥ctx✝)[0 ↦ ty₁✝] t✝
      pure (Ty.arrow ty₁✝ __do_lift)) =
    some (Ty.arrow ty₁✝ ty₂✝)

case app
ctx : Ctx
t : Term
ty : Ty
ctx✝ : Ctx
t₁✝ : Term
ty₁✝ ty₂✝ : Ty
t₂✝ : Term
a✝¹ : ctx✝ ⊢ t₁✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a✝ : ctx✝ ⊢ t₂✝ ⋮ ty₁✝
a_ih✝¹ : type ctx✝ t₁✝ = some (Ty.arrow ty₁✝ ty₂✝)
a_ih✝ : type ctx✝ t₂✝ = some ty₁✝
⊢ (match type ctx✝ t₁✝ with
    | some (Ty.arrow ty₁ ty₂) => do
      let __do_lift ← type ctx✝ t₂✝
      if ty₁ = __do_lift then some ty₂ else none
    | x => none) =
    some ty₂✝