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