Generic coercion code

[CohenCyril]

This code replaces the specific code to generate coercions with a named based version.
The cons: it is specialized to one universe 😬
The pros: it is very generic (it supports arbitrary nesting), generates/relies on coercions and will support extensions of the hierarchy out of the box: it might also be used in future versions of HB if it does the job.

CC @ecranceMERCE @amahboubi

[amahboubi]

@CohenCyril what do you mean by "it is specialized to one universe"
?

[CohenCyril]

The code automatically generates coercions from a record $R_1$ to a record $R_2$ whenever the names of the fields of $R_2$ is a subset of the names of $R_1$ (e.g. given Record R1 := {a : X, b : Y}. Record R2 := {a : X}, we generate automatically a function of type R1 -> R2 solely based on the naming).
However this code works if and only if the designated records depend exactly on one universe variable.

[CohenCyril]

PS: This is not a problem for the current use cases because we indeed have exactly one universe variable in our hierarchy.

[CohenCyril]

I documented here the limitation