Facility for single proposition mixins

[CohenCyril]

Sometimes mixins are constituted of a single field, in which case it is extremely verbose to declare it. We should be able to promote definitions to mixins. (or automatically wrap 🤷)

e.g. for now

Definition commutative {T} (op : T -> T -> T) := forall x y,  op x y = op y x.

HB.mixin Record isCommutative T op := { opC : commutative T op }.
HB.structure Definition Commutative T := { op of isCommutative T op }

now we want (tentative)

Definition commutative {T} (op : T -> T -> T) := forall x y,  op x y = op y x.
HB.structure Definition Commutative T := { op; opC : commutative op}.