Proving that different definitions for the successor function are not $\beta$-equal in the $\lambda$-calculus

In Lectures on the Curry-Howard Isomorphism, by Sørensen and Urzyczin, it is informed that these two definitions of the successor function over the Church numerals aren't $$\beta$$-equal: $$A_s = \lambda x. \lambda s. \lambda z. s\ (x\ s\ z) \\ A_s^{'} = \lambda x. \lambda s. \lambda z. x\ s\ (s\ z)$$

One can easily calculate that $$A_s c_n =_\beta c_{n+1} \\ A_s^{'} c_n =_\beta c_{n+1}$$

And, from the definition of the $$=_\beta$$ relation, we have that it's symmetric and also transitive. So, one could argue $$A_s c_n =_\beta c_{n+1}\ \land\ c_{n+1}=_{\beta} A_s^{'} c_n \implies A_s c_n =_\beta A_s^{'} c_n$$

But since the authors said this isn't the case, I don't see where I made the mistake.

The fact that $$A_s$$ and $$A_s’$$ give equal results when applied to Church numerals does not mean they are equal. It is true that for all $$n \in \mathbb{N}$$, $$A_s c_n =_\beta A_s’ c_n =_\beta c_{n + 1}$$. However, there is no rule of the lambda calculus saying this means $$A_s =_\beta A_s’$$; in fact, they are not $$\beta$$-equivalent, since they are both in normal form and are not $$\alpha$$ equivalent.
• Hmm, I think was a misinterpretation of my part. I thought the authors were saying that both terms, when applied to the Church numeral $c_n$, were not $\beta$-equal. Apparently, they were saying that the terms by themselves (not applied to anyone, therefore not computing anything), are not $\beta$-equal which does indeed make sense.