HB command for aliases

[CohenCyril]

Currently we have to do e.g.

Definition foo (T : Type) : Type := T

or even

Definition foo (T : A.type) : Type := T

forgetting the Type ascription in the second case results in a series of non-forgetful-inheritance warnings/errors which are hard to debug.
Additionally, people usually start with re-equipping foo with some structure already available on T before parting from it.

We should provide a new command: #[ensures(A)] HB.alias Definition foo := T to do that and make sure it is amenable to HB.