Commutativity of addition in polymorphic lambda calculus
The fact that $\mathsf{Add}\ u\ v = \mathsf{Add}\ v\ u$ is not provable for arbitrary $u$ and $v$ does indeed follow from the Church-Rosser property.

Write $u =_\beta v$ if $u \mathrel{({}_\beta\!\!\leftarrow\cup\rightarrow_\beta)^\ast} v$, where $\rightarrow_\beta$ is $\beta$-reduction in System F and $(\cdot)^\ast$ is the reflexive-transitive closure operator (this is a possible definition of $\beta$-equality, which Breazu-Tannen and Coquand denote simply by $=$. Here I will use the $\beta$ subscript and keep the $=$ symbol for strict equality, i.e., $\alpha$-equivalence if you like).  It follows immediately from the definition that if two terms have a common reduct, i.e., $u\rightarrow_\beta^\ast w$ and $v\rightarrow_\beta^\ast w$, then $u=_\beta v$. The Church-Rosser theorem states that the converse also holds:
$$u=_\beta v \quad \textrm{implies}\quad \exists w.\ u\rightarrow^\ast w\textrm{ and }v\rightarrow^\ast w.$$
It follows that $\beta$-equivalent normal forms are necessarily identical:
$$u,v\textrm{ normal and }u=_\beta v\textrm{ implies }u=v.$$

Read contrapositively, the above says that different normal forms can never be $\beta$-equivalent. Now, suppose $\mathsf{Add}\ u\ v=_\beta\mathsf{Add}\ v\ u$ for arbitrary $u$, $v$. In particular, this holds when $u=x$ and $v=y$ are distinct variables of type $polyint$. But it is easy to show (just apply a couple of steps of $\rightarrow_\beta$) that $\mathsf{Add}\ x\ y=_\beta u'$ and $\mathsf{Add}\ y\ x=_\beta v'$ with $u'$ and $v'$ distinct normal forms. Contradiction.