for N being with_zero set
for l being Nat holds SUCC (l,(STC N)) = {l,(l + 1)} by Th8;