Theorem keyAssignmentsOverlapCommutative : forall x y,
  keyAssignmentsOverlap x y -> keyAssignmentsOverlap y x.
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.
