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.

added Kernel Optimisation feature labels

created branch 95-replace-succ-with-an-add-constructor-on-level to address this issue

mentioned in merge request !84 (merged)

added To review label

assigned to @belazy

closed with merge request !84 (merged)

closed with commit 4049f3ef

mentioned in commit 4049f3ef