Definition keyAssignmentsOverlapping
  (k  : keyAssignment)
  (ka : list keyAssignment)
: list keyAssignment :=
  filter (fun j =>
    match keyAssignmentsOverlapDecidable k j with
    | left _ =>
      match Nat.eq_dec (kaId k) (kaId j) with
      | left _  => false
      | right _ => true
      end
    | right _ => false
    end) ka.
