  where \(x_1,..., x_n\) are distinct variables, and \(M\) is a term having all free variables among \(x_1,..., x_n\). In order to be able to get Church’s system, one adds some constants in order to form propositions. Typically