{tz : Std.Time.TimeZone} →
  {motive : Std.Time.DateTime tz → Sort u} →
    (t : Std.Time.DateTime tz) →
      ((timestamp : Std.Time.Timestamp) →
          (date : Thunk Std.Time.PlainDateTime) → motive { timestamp := timestamp, date := date }) →
        motive t