Theorem keyAssignmentValuesEqDec
  (x y : keyAssignment)
: {keyAssignmentValuesEq x y}+{~keyAssignmentValuesEq x y}.
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.
