Inductive keyAssignmentListIsSorted : list keyAssignment -> Prop :=
  | kaListNone : keyAssignmentListIsSorted []
  | kaListOne : forall s, keyAssignmentListIsSorted [s]
  | kaListCons : forall s0 s1 s,
    lt (kaId s0) (kaId s1) ->
      keyAssignmentListIsSorted (s0 :: s) ->
        keyAssignmentListIsSorted (s1 :: s0 :: s).
