∀ {tz : Std.Time.TimeZone} (timestamp : Std.Time.Timestamp) (date : Thunk Std.Time.PlainDateTime)
  (timestamp_1 : Std.Time.Timestamp) (date_1 : Thunk Std.Time.PlainDateTime),
  ({ timestamp := timestamp, date := date } = { timestamp := timestamp_1, date := date_1 }) =
    (timestamp = timestamp_1 ∧ date = date_1)