{motive : Std.Time.OffsetZ → Sort u} →
  (t : Std.Time.OffsetZ) →
    motive Std.Time.OffsetZ.hourMinute →
      motive Std.Time.OffsetZ.full → motive Std.Time.OffsetZ.hourMinuteSecondColon → motive t