In the article "Extensional models of polymorphism" by Breazu-Tannen and Coquand, natural numbers are presented using a Church-like encoding:
$polyint = \forall t . (t \to t) \to t \to t$
Addition for this encoding is introduced as:
$\mathsf{Add} = \lambda u,v : polyint . \Lambda t . \lambda f : t \to t . \lambda x : t . u t f (v t f x)$
Then they say that commutativity of addition cannot be proved, and they say that $\mathsf{Add} u v = \mathsf{Add} v u$ does not follow from polymorphic lambda calculus theory by a simple Church-Rosser argument. What's this Church-Rosser argument? Is it related to the Church-rosser property? How can I prove it?
EDIT: the exact statement is:
"However, the pure $\lambda^{\forall}$ is not sufficient for that, as it cannot even prove, for example, that the operation of addition is commutative:
$\mathsf{Add}\ u\ v = \mathsf{Add}\ v\ u$
with arbitrary $u, v : polyint$ is not provable in $\lambda^{\forall}$ (by a simple Church-Rosser argument)".