Copy of instances over convertible types

We have R and R^o which are convertible and we want to copy instances from one to the other. This is the simplest form.

HB.instance Definition _ := Foo.on R^o.

Which is equivalent to:

HB.instance Definition _ := Foo.copy R^o R.

Since R^o reduces to R, Foo.on is able to find it.

Note that the following code is not only more verbose

HB.instance Definition _ : IsFoo R^o := IsFoo.Build R^o bli bla' blu.

but also risky, since if one gets a piece wrong (here bla' is a non convertible term with the same type of bla, which is used in IsFoo.Build for R) then inference problems will arise later.