post-translation mappings

[agontard]

Some working but not cleaned up code translating hol-light developments to theorems in a context of a Rocq module type for mappings, but where proofs are translated in a context of a Rocq record, along with compatibility proofs to go from one representation to another.

The main command is hol2dk translate-with classes. It is not yet added in the main hol2dk documentation but some explanations are provided if it is run without arguments (this does not describe the conversion to module types yet).

[agontard]

commit history before 0a67ff5 is garbage

[agontard]

Note that transformations would be difficult with sed: there needs to be a distinction between defined object and local bound variables.
For example λ f, Π x y, eq (f x) (f x) needs to be translated to fun f => forall x y, eq Ctx (f x) (f y) instead of fun f => forall x y, eq Ctx (f Ctx (x Ctx)) (f Ctx (y Ctx)), where Ctx is an instance of the mappings record.