Inductive keyAssignment : Set := {
  (** The unique identifier of the key assignment. *)
  kaId : nat;
  (** The lowest key value that will trigger this clip. *)
  kaValueStart : nat;
  (** The key value at which the clip plays at the normal playback rate. *)
  kaValueCenter: nat;
  (** The highest key value that will trigger this clip. *)
  kaValueEnd : nat;
  kaValueEndRange : le kaValueEnd 294967295;
  (** The key values must be ordered. *)
  kaValueStartOrder : le kaValueStart kaValueCenter;
  kaValueCenterOrder : le kaValueCenter kaValueEnd;
  (** The clip that will be triggered. *)
  kaClipId : nat;
  (** The amplitude at which this clip will be played when at the lowest key value. *)
  kaAmplitudeAtKeyStart : R;
  (** The amplitude at which this clip will be played when at the center key value. *)
  kaAmplitudeAtKeyCenter : R;
  (** The amplitude at which this clip will be played when at the highest key value. *)
  kaAmplitudeAtKeyEnd : R;
  (** The amplitude values are normalized values. *)
  kaAmplitudeAtKeyStartNormal : isNormalized kaAmplitudeAtKeyStart;
  kaAmplitudeAtKeyCenterNormal : isNormalized kaAmplitudeAtKeyCenter;
  kaAmplitudeAtKeyEndNormal : isNormalized kaAmplitudeAtKeyEnd;
  (** The velocity value at which this clip starts to be triggered. *)
  kaAtVelocityStart : R;
  (** The velocity value at which the amplitude of this clip is at maximum. *)
  kaAtVelocityCenter : R;
  (** The velocity value at which this clip stops being triggered. *)
  kaAtVelocityEnd : R;
  (** The velocity values are normalized values and are correctly ordered. *)
  kaAtVelocityStartNormal : isNormalized kaAtVelocityStart;
  kaAtVelocityCenterNormal : isNormalized kaAtVelocityCenter;
  kaAtVelocityEndNormal : isNormalized kaAtVelocityEnd;
  kaAtVelocityStartOrder : kaAtVelocityStart <= kaAtVelocityCenter;
  kaAtVelocityCenterOrder : kaAtVelocityCenter <= kaAtVelocityEnd;
  (** The amplitude at which this clip will be played when at the starting velocity value. *)
  kaAmplitudeAtVelocityStart : R;
  (** The amplitude at which this clip will be played when at the center velocity value. *)
  kaAmplitudeAtVelocityCenter : R;
  (** The amplitude at which this clip will be played when at the end velocity value. *)
  kaAmplitudeAtVelocityEnd : R;
  (** The amplitude values are normalized values. *)
  kaAmplitudeAtVelocityStartNormal : isNormalized kaAmplitudeAtVelocityStart;
  kaAmplitudeAtVelocityCenterNormal : isNormalized kaAmplitudeAtVelocityCenter;
  kaAmplitudeAtVelocityEndNormal : isNormalized kaAmplitudeAtVelocityEnd;
  (** The associated key assignment flags. *)
  kaFlags : list keyAssignmentFlag;
  kaFlagsUnique : NoDup kaFlags;
}.
