Parametricity and projective eliminations for dependent records
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."