Inductive keyEvaluation : Set := keyEvaluationMake {
  keyEvaluationClipId                  : nat;
  keyEvaluationVelocityAmplitude       : R;
  keyEvaluationVelocityAmplitudeNormal : isNormalized keyEvaluationVelocityAmplitude;
  keyEvaluationKeyAmplitude            : R;
  keyEvaluationKeyAmplitudeNormal      : isNormalized keyEvaluationKeyAmplitude;
  keyEvaluationRate                    : R;
  keyEvaluationRateNonNegative         : 0 <= keyEvaluationRate
}.
