关于由succ构造的Lambda calculus项是否均为Church numerals上多项式函数的求证问询

我最近在研究Church numerals里的$\mathsf{succ}$操作，它的定义是：

$$ \mathsf{succ} = \lambda n f x. f (n f x) $$

我发现把它多次迭代应用在自身上时，会呈现出很有意思的多项式性质——这里要说明一下，所有涉及$n$的表达式都指对应数值的Church numeral：

$$ \begin{align}

\mathsf{succ} ; \mathsf{succ} ; n f x &= (n^2+n) f x \

\mathsf{succ} ; \mathsf{succ} ; \mathsf{succ} ; n f x &= (n^2+n+1) f x \

\mathsf{succ} ; \mathsf{succ} ; \mathsf{succ} ; \mathsf{succ} ; n f x &= (n³⁺ⁿ2+n) f x \

\mathsf{succ} ; \mathsf{succ} ; \mathsf{succ} ; \mathsf{succ} ; \mathsf{succ} ; n f x &= (n³⁺ⁿ2+n+1) f x

\end{align} $$

更一般化的规律也成立：

$$ \begin{align}

\underbrace{\mathsf{succ} ; \cdots ; \mathsf{succ}}_{2k \text{ times}}

; n f x &= (\sum_{i=1}^{k+1}{ni}) f x \

\underbrace{\mathsf{succ} ; \cdots ; \mathsf{succ}}_{2k+1 \text{ times}}

; n f x &= (\sum_{i=0}^{k+1}{ni}) f x

\end{align} $$

我尝试过对这个规律做证明，不过现在更感兴趣的是一个更宽泛的问题：如果用$\mathsf{succ}$构造更复杂的Lambda项，比如$\mathsf{succ} (\mathsf{succ} ; \mathsf{succ})$、$\mathsf{succ} (\mathsf{succ} (\mathsf{succ} ; \mathsf{succ}) \mathsf{succ})$这类带嵌套的组合，这些项作用在Church numerals上时，是否也都对应多项式函数？

我自己做过一些手动实验，最近还写了个Mathematica程序通过项重写来模拟这些表达式的行为，但至今既找不到能证明所有这类项都满足多项式性质的严谨方法，也没找到反例。实在不知道该从哪里入手，想请教大家有没有思路或者相关的结论可以参考？

备注：内容来源于stack exchange，提问作者Bubbler