I was reading about Church encoding, and couldn't figure out some of the grammar of function applications (in terms of church numerals). In particular, the examples I've seen thus far apply to unary functions $f$, i.e. something like $n \space f \space x \equiv f^n \space x$.
What does it mean for a binary function $f_2$ to have (can't figure out the arity etc.):
$ n \space f_2 \space x \space y $ ?
Here, it's not clear to me what a $f^n_2$ can mean.
The motivation of the question is to understand the body of the following
predecessor function from Wikipedia page linked earlier:
$ pred \equiv \lambda n.\lambda f. \lambda x. n \space (\lambda g. \lambda h. (g \space f)) \space (\lambda u.x) \space (\lambda u.u) $
(i.e. $ \space n \space (\lambda g. \lambda h. (g \space f)) \space (\lambda u.x) \space (\lambda u.u) $ )
Also, I tried to understand this using e.g.
$n \space (+) \space 1 \space 2$
, but couldn't figure out what's the correct meaning.