I am new to lambda calculus and I am trying to proof that the successor function $suc := \lambda nfx.f (n f x)$ is injective, i.e. that $suc \, a = suc \, b \to a = b$ for all $a$ and $b$.
My argument goes as follows:
$suc \, a = suc \, b$
$\lambda fx.f (a f x) = \lambda fx.f (b f x)$
As both sides are equivalent, they have to yield the same result when applied to all $g$ and $y$.
$(\lambda fx.f (a f x) ) g y = (\lambda fx.f (b f x) ) g y$
$g (a g y) = g (b g y)$
As this holds for all $g$, it also holds when $g$ is injective. Therefore the arguments of $g$ must be equivalent.
$a g y = b g y$
This states that $a$ and $b$ yield the same result for all $g$ and all $y$. Therefore $a$ and $b$ must be equivalent.
Does this argumentation make any sense? Or how does one go about proofing equivalences in lambda calculus?