split <;> simp_all
case h.inr
ty : Ty
ctx : Ctx
x x✝ : Nat
h✝ : ¬x✝ = x + 1
⊢ (match x✝ with
    | 0 => none
    | Nat.succ x => ctx x) =
    match x✝ with
    | 0 => none
    | Nat.succ x_1 => if x_1 = x then some ty else ctx x_1
no goals