{motive : Std.Time.TimeZone.ZoneRules → Sort u} →
  (t : Std.Time.TimeZone.ZoneRules) →
    ((initialLocalTimeType : Std.Time.TimeZone.LocalTimeType) →
        (transitions : Array Std.Time.TimeZone.Transition) →
          motive { initialLocalTimeType := initialLocalTimeType, transitions := transitions }) →
      motive t