Theorem keyAssignmentsOverlappingFind0 : 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.
