{motive : Lean.ImportedModule✝ → Sort u} →
  (t : Lean.ImportedModule✝¹) →
    ((toEffectiveImport : Lean.EffectiveImport) →
        (parts : Array (Lean.ModuleData × Lean.CompactedRegion)) →
          (irData? : Option (Lean.ModuleData × Lean.CompactedRegion)) →
            (needsData needsIRTrans : Bool) →
              motive
                { toEffectiveImport := toEffectiveImport, parts := parts, irData? := irData?, needsData := needsData,
                  needsIRTrans := needsIRTrans }) →
      motive t