Inductive clipsListIdIsSorted : list clip -> Prop :=
  | ClipIdOne  : forall s,
      clipsListIdIsSorted [s]
  | ClipIdCons : forall s0 s1 ss,
    (clipId s0) < (clipId s1) ->
      clipsListIdIsSorted (s0 :: ss) ->
        clipsListIdIsSorted (s1 :: s0 :: ss).
