[Agda] sharing a variable in a with clause and its result

[effectfully]

I would write

h : (m n : N) -> N
h zero n = n
h (suc m) n with suc n
... | n' with h m n'
... | x = x + n'