HB support for importing non-canonical instances

[CohenCyril]

There are very common design patterns to promote a non canonical choice as locally canonical.
Indeed aliases allow one to refer to a non canonical construction, but sometimes one wants to import instances in the current section/proof.
e.g.
https://github.com/math-comp/math-comp/blob/6c97ac8595c1a6ffb969c42a08cf8c68ef28671f/order/order.v#L6675-L6792

This design pattern should be supported by HB at the same time as aliases, maybe by providing a module name to import, or by creating a module with the same name as the alias?

(note that it is also common to require non forgetful inheritance locally)