∀ (year : Std.Time.Year.Offset) (month : Std.Time.Month.Ordinal) (day : Std.Time.Day.Ordinal)
  (valid : year.Valid month day),
  sizeOf { year := year, month := month, day := day, valid := valid } =
    1 + sizeOf year + sizeOf month + sizeOf day + sizeOf valid