This is easier to understand in constructive type theory. You can't pattern match on `k` to recur, but you can pattern match on `succ(k)` to recur on `k`.

Even when doing classic logic, I start with my constructive intuition and the sprinkle in the continuation-passing-style spooky magic when needed to get back the classical craziness.

Everyone should learn constructive first.