replace `Succ` with an `Add` constructor on `Level`

This should help avoid some cases of overflow, though what optimisations could be brought during checking is not yet clear to me.