Trocq records for inductive types

[ecranceMERCE]

Several files of the repository relate inductive types to themselves. The proofs do not look very interesting, and they are mainly used for Trocq not to fail when translating a goal containing a type that the user does not focus on (i.e., they want it to be left untouched in the process). Therefore, it would be interesting to have a generator of reflexive proofs for any inductive type:

(* α is a vector of parameters/indices *)
Inductive T α := (* ... *)

Trocq Generate T. (* generates TR : forall α α' αR, ParamMN.Rel (T α) (T α') *)