split <;> try split at h <;> try contradiction
ctx : Ctx
t : Term
ty : Ty
ctx' : Ctx
ty✝ : Ty
x✝ : Nat
h :
  (match x✝ with
    | 0 => none
    | Nat.succ x => ctx x) =
    some ty✝
⊢ ctx ⊢ if x✝ < 0 then Term.var x✝ else Term.var (x✝ - 1) ⋮ ty✝
case inr.h_2
ctx : Ctx
t : Term
ty : Ty
ctx' : Ctx
ty✝ : Ty
x✝¹ x✝ : Nat
h✝ : ¬Nat.succ x✝ < 0
h : ctx x✝ = some ty✝
⊢ ctx ⊢ Term.var (Nat.succ x✝ - 1) ⋮ ty✝