Theorem keyAssignmentEvaluateAmplitudeForVelocityNormalized : forall k v a,
  keyAssignmentMatches k v a
    -> isNormalized (keyAssignmentEvaluateAmplitudeForVelocity v a).
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.
