funsplit and polarity of Pi-types
Here's a slightly different perspective on Fredrik's answer. It's generally the case that impredicative Church encodings of types will satisfy the relevant $\beta$ laws, but will not satisfy the $\eta$ laws. 

So this means we can define a dependent pair as follows:

$$
\exists x:X.\;Y[x] \triangleq \forall \alpha:\ast.\; (\Pi x:X.\;Y[x] \to \alpha) \to \alpha
$$
Now, note that $\pi_1$ is easily definable:
$$
\pi_1 : \exists x:X.\;Y[x] \to X \triangleq \lambda p:(\exists x:X.\;Y[x]).\;p\;X\;(\lambda x\;y.x)
$$
However, you cannot define the second projection $\pi_2 : \Pi p:(\exists x:X.\;Y[x]).\; Y[\pi_1\;p]$ -- try it! You can only define a weak eliminator for it, which is why I wrote it with an existential. 

However, the second projection is realizable, and in a parametric model you can show that it has the right behavior, too. (See my recent draft with Derek Dreyer on parametricity in the Calculus of Constructions for more on this.) So I think that the $\pi_2$ projection fundamentally demands some strong extensionality properties for it to make sense. 

In terms of the sequent calculus, the weak eliminator has a rule that looks a bit like:

$$
\frac{\Gamma, x:X, y:Y[x],\; \Gamma' \vdash e' : C}
     {\Gamma, p:\exists x:X.\,Y[x],\; \Gamma' \vdash \mathsf{let}(x,y)=p\;\mathsf{in}\;e' : C}
$$
Here, the implicit well-formedness conditions imply that $p$ cannot occur free in $\Gamma'$ or $C$. If we relax that condition, we get the split rule, which has a left-rule that looks like
$$
\frac{\Gamma, x:X, y:Y[x],\; [(x,y)/p]\Gamma' \vdash e' : [(x,y)/p]C}
     {\Gamma, p:\exists x:X.\,Y[x],\; \Gamma' \vdash \mathsf{let}(x,y)=p\;\mathsf{in}\;e' : C}
$$
That substitution reminds me an awful lot of the Girard/Schroeder-Heister elimination rule for equality. I asked a question about this rule a while back, and David Baelde and Gopalan Nadathur give the state-of-the-art version in their LICS 2012 paper, Combining Deduction Modulo and Logics of Fixed-Point Definitions. I think Conor McBride has spent some time thinking about the relationship between the identity type and the Schroeder-Heister equality, so you might want to see what he thinks.