In dependent type theory, parametricity is often written as a function structurally recursive on the abstract syntax tree of terms. We identify a shortcoming of the functional presentations and offer an alternative in the style of a sequent calculus, and further illustrate how it can be implemented as a logic program using the Rocq-ELPI metaprogramming framework. We also offer two extensions of binary parametricity to cover features of Rocq, namely translating fixpoint operators and record types.