Parametricity and projective eliminations for dependent records It's well-known that in System F, you can encode binary products with the type
$$
A \times B \triangleq \forall\alpha.\; (A \to B \to \alpha) \to \alpha
$$
You can then define projection functions $\pi_1 : A \times B \to A$ and $\pi_2 : A \times B \to B$. 

This isn't so surprising, even though the natural reading of the F type is of a pair with a 
let-style elimination $\mathsf{let}\;(x,y) = p \;\mathsf{in}\; e$, because the two kinds of pair
are interderivable in intuitionistic logic. 

Now, in a dependent type theory with impredicative quantification, you
can follow the same pattern to encode a dependent record type $\Sigma x:A.\; B[x]$ as
$$
\Sigma x:A.\;B[x] \triangleq \forall\alpha.\; (\Pi x:A.\; B[x] \to \alpha) \to \alpha
$$
But in this case, there isn't a simple way of defining the projective eliminators
$\pi_1 : \Sigma x:A.\;B[x] \to A$ and $\pi_2 : \Pi p:(\Sigma x:A.\;B[x]).\; B[\pi_1\,p]$. 

However, if the type theory is parametric, you can use parametricity to show that $\pi_2$ is definable. This appears to be known --- see, for example, this Agda development by Dan Doel in which he derives it without comment --- but I can't seem to find a reference for this fact. 

Does anyone know a reference for the fact that parametricity allows defining projective eliminations for dependent types?

EDIT: The closest thing I've found so far is this 2001 paper by Herman Geuvers, Induction is not derivable in second order dependent type theory, in which he proves that you can't do it without parametricity.
I just talked to Dan Doel and he explained that his reference was in fact one Neel Krishnaswami. He saw a comment on n-cafe by you that one could do strong induction using parametricity, so he went ahead and did it as an exercise, not realizing that doing it for sigma was apparently a novel result.

The precise quote: "My reference was him. I thought he said it was possible, so I did it."