- > * when `n == 0`, it reduces to `\s z. (\v. z) I`, or `\s z. z`
- > * when `n == 1`, it reduces to `\s z. (\v. v z) I`, or `\s z. z`
- > * when `n == 2`, it reduces to `\s z. (\v. v (s z)) I`, or `\s z. s z`
- > * when `n == 3`, it reduces to `\s z. (\v. v (s (s z))) I`, or `\s z. s (s z)`
+ > * when `n == 0`, it reduces to `\s z. (K z) I`, or `\s z. z`
+ > * when `n == 1`, it reduces to `\s z. (box z) I`, or `\s z. z`
+ > * when `n == 2`, it reduces to `\s z. (box (s z)) I`, or `\s z. s z`
+ > * when `n == 3`, it reduces to `\s z. (box (s (s z))) I`, or `\s z. s (s z)`