redesign factory-alias + builders

[gares]

Avoid (where R1 is richer than R)

HB.factory Definition alias R1 := real (proj R1).
HB.builders R1 of alias R1.
  HB.instance Definition : more := more.Build.
..
HB.instance Definition _ R := real.Build ...
HB.instance Definition _ R1 := alias.Build ...

and rather have

HB.builders R1 of real (proj R1).
...
HB.instance Definition _ R1 : real (proj R1) * more R1 := real.Build ...