A list-oriented extension of the lambda-calculus satisfying the Church-Rosser theorem (Q1185009)

It is shown that the Church-Rosser property holds for an extension of the (type-free) \(\lambda\)-calculus with lists. This extension is such that \((\lambda \kappa \cdot[e_1,\dots,e_ n])u\) reduces to \([e_1[\kappa:=u],\ldots,e_n[\kappa:=u]]\) if \([e_1,\ldots,e_n]\) is the notation for the list \(e_1,\ldots,e_n\).