Combinator creating full parametricity witnesses from individual record fields

[ecranceMERCE]

This repository contains a few files giving parametricity proofs for inductive types like nat, bool, option, but also equality and vectors for example. It looks like we first define the individual fields (i.e., map from nat to nat, then map_in_R, etc.), then a proof of equivalence between the relation and its symmetrisation:

R_sym : forall x x', sym_rel R x' x <~> R x x'

before actually building the full record at level $(m, n)$ by taking $m$ fields for R and $n$ fields for sym_rel R, then glueing both subrecords using R_sym so that the second one typechecks as the contravariant field of the Param record.

Can this symmetry proof be made automatically just from the definition of R, even when R is non-trivial and provided by the user?
Can the whole process be automated so that the user just has to input the individual fields and Trocq generates all the possible records (possibly on the fly during the translation)?

[CohenCyril]

There are two ways to go about that:

1. Modify and use HB (cf Adapt and use HB to generate Trocq relational structures #28)
2. Implement some of the features of HB in Trocq