{motive : Std.Time.OffsetX → Sort u} →
  (t : Std.Time.OffsetX) →
    motive Std.Time.OffsetX.hour →
      motive Std.Time.OffsetX.hourMinute →
        motive Std.Time.OffsetX.hourMinuteColon →
          motive Std.Time.OffsetX.hourMinuteSecond → motive Std.Time.OffsetX.hourMinuteSecondColon → motive t