{α : Type} →
  {motive : Std.Time.Database α → Sort u} →
    (t : Std.Time.Database α) →
      ((getZoneRules : α → String → IO Std.Time.TimeZone.ZoneRules) →
          (getLocalZoneRules : α → IO Std.Time.TimeZone.ZoneRules) →
            motive { getZoneRules := getZoneRules, getLocalZoneRules := getLocalZoneRules }) →
        motive t