Theorem keyAssignmentsOverlappingNotSelf : forall k ka,
  ~In k (keyAssignmentsOverlapping k ka).
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.
