$\underline{iszero}$ function is defined as
$$ \underline{iszero} = \lambda n. n(\lambda x. \underline{false})\underline{true} $$
I want to show that $\underline{iszero} \ \underline{5} = \underline{false}$.
Here's my try:
$$ \underline{iszero} \ \underline{5} = (\lambda n. n(\lambda x. \underline{false})\underline{true})\underline{5} = \underline{5}(\lambda x. \underline{false})\underline{true} = (\lambda fx. f^5 x)(\lambda x. \underline{false})\underline{true} = (\lambda x. (\lambda x_0. \underline{false})^5 x)\underline{true} = (\lambda x_0. \underline{false})^5 \underline{true} $$
Use induction:
$$ (\lambda x_0. \underline{false})\underline{true} = \underline{false} $$
$$ (\lambda x_0. \underline{false})^2 \underline{true} = (\lambda x_0. \underline{false})((\lambda x_0. \underline{false})\underline{true}) = (\lambda x_0. \underline{false})\underline{false} = \underline{false} $$
$$ \vdots $$
$$ (\lambda x_0. \underline{false})^3 \underline{true} = \underline{false} \ and \ (\lambda x_0. \underline{false})^4 \underline{true} = \underline{false} $$
So $$ (\lambda x_0. \underline{false})^5 \underline{true} = (\lambda x_0. \underline{false})((\lambda x_0. \underline{false})^4 \underline{true}) = (\lambda x_0. \underline{false})\underline{false} = \underline{false} $$
$\square$
Are the steps correct and reasonable? Thanks a bunch!