feat: better support for reducing `Nat.rec`

closes #3022

With this commit, given the declaration
```
def foo : Nat → Nat
  | 0 => 2
  | n + 1 => foo n
```
when we unfold `foo (n+1)`, we now obtain `foo n` instead of
`foo (Nat.add n 0)`.