∀ {interval startTime : Lean.Firefox.Milliseconds} {categories : Array Lean.Firefox.Category} {processType : ℕ}
  {product : String} {preprocessedProfileVersion : ℕ} {markerSchema : Array Lean.Json}
  {sampleUnits : Lean.Firefox.SampleUnits} {interval_1 startTime_1 : Lean.Firefox.Milliseconds}
  {categories_1 : Array Lean.Firefox.Category} {processType_1 : ℕ} {product_1 : String}
  {preprocessedProfileVersion_1 : ℕ} {markerSchema_1 : Array Lean.Json} {sampleUnits_1 : Lean.Firefox.SampleUnits},
  { interval := interval, startTime := startTime, categories := categories, processType := processType,
        product := product, preprocessedProfileVersion := preprocessedProfileVersion, markerSchema := markerSchema,
        sampleUnits := sampleUnits } =
      { interval := interval_1, startTime := startTime_1, categories := categories_1, processType := processType_1,
        product := product_1, preprocessedProfileVersion := preprocessedProfileVersion_1,
        markerSchema := markerSchema_1, sampleUnits := sampleUnits_1 } →
    interval = interval_1 ∧
      startTime = startTime_1 ∧
        categories = categories_1 ∧
          processType = processType_1 ∧
            product = product_1 ∧
              preprocessedProfileVersion = preprocessedProfileVersion_1 ∧
                markerSchema = markerSchema_1 ∧ sampleUnits = sampleUnits_1