(year : Std.Time.Year.Offset) →
  (motive : Std.Time.ValidDate year.isLeap → Sort u_1) →
    (x : Std.Time.ValidDate year.isLeap) →
      ((month : Std.Time.Month.Ordinal) →
          (day : Std.Time.Day.Ordinal) →
            (proof : Std.Time.Month.Ordinal.Valid year.isLeap (month, day).1 (month, day).2) →
              motive ⟨(month, day), proof⟩) →
        motive x