split
n : Nat
h : n ≠ zero
⊢ succ
      (match n with
      | zero => zero
      | succ k => k) =
    n
case h_1
x✝ : Nat
h : zero ≠ zero
⊢ succ zero = zero

case h_2
x✝ a✝ : Nat
h : succ a✝ ≠ zero
⊢ succ a✝ = succ a✝