Theorem keyAssignmentEvaluateRateNonNegative : forall k v a,
  keyAssignmentMatches k v a
    -> Rle 0 (keyAssignmentEvaluateRate k a).
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.
