Theorem keyAssignmentsOverlapDecidable : forall x y,
  {keyAssignmentsOverlap x y}+{~keyAssignmentsOverlap x y}.
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.
