{motive : Lean.Firefox.ProfileMeta → Sort u} →
  (t : Lean.Firefox.ProfileMeta) →
    ((interval startTime : Lean.Firefox.Milliseconds) →
        (categories : Array Lean.Firefox.Category) →
          (processType : ℕ) →
            (product : String) →
              (preprocessedProfileVersion : ℕ) →
                (markerSchema : Array Lean.Json) →
                  (sampleUnits : Lean.Firefox.SampleUnits) →
                    motive
                      { interval := interval, startTime := startTime, categories := categories,
                        processType := processType, product := product,
                        preprocessedProfileVersion := preprocessedProfileVersion, markerSchema := markerSchema,
                        sampleUnits := sampleUnits }) →
      motive t