let rec split_clock_type ct =
  match ct with
  | CT_var alpha -> alpha, Pbw one
  | CT_on (CT_var alpha, p) -> alpha, Pbw p
  | CT_on (ct', p) ->
      let alpha, w = split_clock_type ct' in
      alpha, On (w, Pbw p)