-- Std.Time.Format.DateFormat
Std.Time.DateFormatSymbols.mk.inj : ∀ {monthLong monthShort monthNarrow : Vector String 12}
  {weekdayLong weekdayShort weekdayNarrow weekdayTwoLetter : Vector String 7}
  {eraShort eraLong eraNarrow : Vector String 2} {quarterShort quarterLong quarterNarrow : Vector String 4}
  {amShort pmShort amLong pmLong amNarrow pmNarrow : String}
  {dayPeriodShort dayPeriodLong dayPeriodNarrow : Std.Time.DayPeriodSymbols}
  {extendedDayPeriodShort extendedDayPeriodLong extendedDayPeriodNarrow : Vector String 6}
  {monthLong_1 monthShort_1 monthNarrow_1 : Vector String 12}
  {weekdayLong_1 weekdayShort_1 weekdayNarrow_1 weekdayTwoLetter_1 : Vector String 7}
  {eraShort_1 eraLong_1 eraNarrow_1 : Vector String 2} {quarterShort_1 quarterLong_1 quarterNarrow_1 : Vector String 4}
  {amShort_1 pmShort_1 amLong_1 pmLong_1 amNarrow_1 pmNarrow_1 : String}
  {dayPeriodShort_1 dayPeriodLong_1 dayPeriodNarrow_1 : Std.Time.DayPeriodSymbols}
  {extendedDayPeriodShort_1 extendedDayPeriodLong_1 extendedDayPeriodNarrow_1 : Vector String 6},
  { monthLong := monthLong, monthShort := monthShort, monthNarrow := monthNarrow, weekdayLong := weekdayLong,
        weekdayShort := weekdayShort, weekdayNarrow := weekdayNarrow, weekdayTwoLetter := weekdayTwoLetter,
        eraShort := eraShort, eraLong := eraLong, eraNarrow := eraNarrow, quarterShort := quarterShort,
        quarterLong := quarterLong, quarterNarrow := quarterNarrow, amShort := amShort, pmShort := pmShort,
        amLong := amLong, pmLong := pmLong, amNarrow := amNarrow, pmNarrow := pmNarrow,
        dayPeriodShort := dayPeriodShort, dayPeriodLong := dayPeriodLong, dayPeriodNarrow := dayPeriodNarrow,
        extendedDayPeriodShort := extendedDayPeriodShort, extendedDayPeriodLong := extendedDayPeriodLong,
        extendedDayPeriodNarrow := extendedDayPeriodNarrow } =
      { monthLong := monthLong_1, monthShort := monthShort_1, monthNarrow := monthNarrow_1,
        weekdayLong := weekdayLong_1, weekdayShort := weekdayShort_1, weekdayNarrow := weekdayNarrow_1,
        weekdayTwoLetter := weekdayTwoLetter_1, eraShort := eraShort_1, eraLong := eraLong_1, eraNarrow := eraNarrow_1,
        quarterShort := quarterShort_1, quarterLong := quarterLong_1, quarterNarrow := quarterNarrow_1,
        amShort := amShort_1, pmShort := pmShort_1, amLong := amLong_1, pmLong := pmLong_1, amNarrow := amNarrow_1,
        pmNarrow := pmNarrow_1, dayPeriodShort := dayPeriodShort_1, dayPeriodLong := dayPeriodLong_1,
        dayPeriodNarrow := dayPeriodNarrow_1, extendedDayPeriodShort := extendedDayPeriodShort_1,
        extendedDayPeriodLong := extendedDayPeriodLong_1, extendedDayPeriodNarrow := extendedDayPeriodNarrow_1 } →
    monthLong = monthLong_1 ∧
      monthShort = monthShort_1 ∧
        monthNarrow = monthNarrow_1 ∧
          weekdayLong = weekdayLong_1 ∧
            weekdayShort = weekdayShort_1 ∧
              weekdayNarrow = weekdayNarrow_1 ∧
                weekdayTwoLetter = weekdayTwoLetter_1 ∧
                  eraShort = eraShort_1 ∧
                    eraLong = eraLong_1 ∧
                      eraNarrow = eraNarrow_1 ∧
                        quarterShort = quarterShort_1 ∧
                          quarterLong = quarterLong_1 ∧
                            quarterNarrow = quarterNarrow_1 ∧
                              amShort = amShort_1 ∧
                                pmShort = pmShort_1 ∧
                                  amLong = amLong_1 ∧
                                    pmLong = pmLong_1 ∧
                                      amNarrow = amNarrow_1 ∧
                                        pmNarrow = pmNarrow_1 ∧
                                          dayPeriodShort = dayPeriodShort_1 ∧
                                            dayPeriodLong = dayPeriodLong_1 ∧
                                              dayPeriodNarrow = dayPeriodNarrow_1 ∧
                                                extendedDayPeriodShort = extendedDayPeriodShort_1 ∧
                                                  extendedDayPeriodLong = extendedDayPeriodLong_1 ∧
                                                    extendedDayPeriodNarrow = extendedDayPeriodNarrow_1