How strong is equivalence of lambda expressions?
In general, there is always an infinite number of "computationally different" functions that are extensionally equal: take for instance the "$3n+1$-function" $g$, and for any function $f$ define $G_f$ to be:

$$ G_f(n)=\begin{cases} f(n) &amp; \mbox{if }g(n)\mbox{ cycles at }1 \\ 0 &amp; \mbox{otherwise}\end{cases}$$

This function is (probably) extensionally equal to $f$ for every $f$, but this is (possibly) not provable in $\mathrm{PA}$, or indeed in the weak framework of $\beta\eta\alpha$-conversion.

More pragmatically, the identity function $\lambda x.x$ and the "stupid identity"
$$ \lambda n.n\ (\lambda x\ f.x)\ (\lambda m\ x\ f.f(m\ x \ f))$$

Denote the same function $\mathrm{id}:\mathbb{N}\rightarrow \mathbb{N}$, under the usual church encoding, but are not $\beta\eta$-equal, as can easily be seen (they are both in normal form).