Given a pair $[M_1,M_2]$ there is an easy encoding $\lambda x.x M_1 M_2$. For the n-tuple we have two options. First encoding: $$\lambda x.x M_1, M_2, \ldots , M_n$$ Second encoding: $$[M_0, [M_1 , [M_2, \ldots ]]] = \lambda x.xM_0 \lambda y.y M_1 \lambda z.z M_2 \ldots$$ For the first encoding it is easy to define projectors to extract the k-th value: $\lambda x_1 x_2 \ldots x_n . x_k$ What I can't understand is how is it possible to extract a value from an n-tuple encoded in the second way.
I am told that the following projector works: $$\pi^n_k = \lambda x.x F^k T$$ Where $T=\lambda xy.x$ and $F=\lambda xy.y$
But according to my calculations that does not work. Can you provide me with a working example?