∀ {trustLevel : UInt32} {mainModule : Lean.Name} {isModule : Bool} {imports : Array Lean.Import}
  {regions : Array Lean.CompactedRegion} {modules : Array Lean.EffectiveImport}
  {moduleName2Idx : Std.HashMap Lean.Name Lean.ModuleIdx} {importAllModules : Array Lean.EffectiveImport}
  {moduleData : Array Lean.ModuleData} {trustLevel_1 : UInt32} {mainModule_1 : Lean.Name} {isModule_1 : Bool}
  {imports_1 : Array Lean.Import} {regions_1 : Array Lean.CompactedRegion} {modules_1 : Array Lean.EffectiveImport}
  {moduleName2Idx_1 : Std.HashMap Lean.Name Lean.ModuleIdx} {importAllModules_1 : Array Lean.EffectiveImport}
  {moduleData_1 : Array Lean.ModuleData},
  { trustLevel := trustLevel, mainModule := mainModule, isModule := isModule, imports := imports, regions := regions,
        modules := modules, moduleName2Idx := moduleName2Idx, importAllModules := importAllModules,
        moduleData := moduleData } =
      { trustLevel := trustLevel_1, mainModule := mainModule_1, isModule := isModule_1, imports := imports_1,
        regions := regions_1, modules := modules_1, moduleName2Idx := moduleName2Idx_1,
        importAllModules := importAllModules_1, moduleData := moduleData_1 } →
    trustLevel = trustLevel_1 ∧
      mainModule = mainModule_1 ∧
        isModule = isModule_1 ∧
          imports = imports_1 ∧
            regions = regions_1 ∧
              modules = modules_1 ∧
                moduleName2Idx = moduleName2Idx_1 ∧ importAllModules = importAllModules_1 ∧ moduleData = moduleData_1