HB.factory must not alter relevant data

[CohenCyril]

When writing down builders of a factory, the input fields that are not in Prop must not be changed by the builders.
E.g.

HB.mixin Record Two T := { a : T; b : T }.
HB.factor Record TwoF T := {a : T; b : T}.
HB.builders Context T of TwoF T.
HB.instance Definition _ := Two.Build T b a.
HB.end (* We must fail here! *)

Should be forbidden as when doing HB.instance Definition _ := TwoF.Build nat 0 1, the constants will be swapped, i.e. a := 1 and b := 1 which is not what the user expects.