Using the following definitions
$0 := \lambda fx.x $
$suc := \lambda nfx.f \, (n \, f \, x)$
I am trying to proof that there exists no expression $a$, such that $suc \, a = 0$.
First try:
$suc \, a = (\lambda nfx.f \, (n \, f \, x)) \, a = \lambda fx.f \, (a \, f \, x) $
The expression $\lambda fx.f \, (a \, f \, x)$ is in $\beta$-normal form, as is $\lambda fx.x$ for $0$. Since both expressions are not identical (up to $\alpha$-equivalence), they are not equivalent. Therefore, no such $a$ exists. Is this sufficient to proof the statement?
Second try:
$suc \, a = 0$
$\lambda fx.f \, (a \, f \, x) = \lambda fx.x $
If they are equivalent, by extensionality, they should yield the same result when applied to the same parameters. Let's choose arbitrarily $g$ and $y$.
$(\lambda fx.f \, (a \, f \, x) ) \, g \, y = (\lambda fx.x) \, g \, y $
$g \, (a \, g \, y) = y $
As this must hold for all $g$ and $y$, let's choose an $z$ such that $z \neq y$ and pick $g=\lambda x.z$
$(\lambda x.z) \, (a \, (\lambda x.z) \, y) = y $
$z = y$
As we chose $z$ to be distinct from $y$, we found a contradiction, thus proofing that no such $a$ exists. Does this proof work?