I think the following encoding also works.

```
ZERO := λf. λx. x
ONE  := λf. f
TWO  := λf. f f
THREE:= λf. f (f f)

```

Note: the original encoding is

```
ZERO := λf. λx. x
ONE  := λf. λx. f x
TWO  := λf. λx. f (f x)
THREE:= λf. λx. f (f (f x))

```

Why is the original one better?