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