Theorem keyAssignmentsOverlappingFind : forall k ka p,
  (In p ka /\ keyAssignmentsOverlap k p /\ (kaId k) <> (kaId p))
    <-> In p (keyAssignmentsOverlapping k ka).
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.
