 Formally, the predication operator p\(_k\) is a \((k+1)\)-ary predicate symbol. The first argument is intended to be a \(\lambda\)-term of \(k\) arguments, and the rest of the arguments are intended to be the arguments of the body of the \(\lambda\)-term. The \(\beta\)-principle above says that the predication of an \(n\)-ary \(\lambda\)-term \(L\) to \(n\) terms holds precisely when the body of \(L\) holds of those terms.