Check [n](S (S n)).
Check [n](S (plus n n)).