Fixpoint keyAssignmentForId
  (i  : nat)
  (ka : list keyAssignment)
: option keyAssignment :=
  match ka with
  | nil         => None
  | cons a rest =>
    match Nat.eq_dec (kaId a) i with
    | left _  => Some a
    | right _ => keyAssignmentForId i rest
    end
  end.
