{P : Sort u} →
  {module : Lean.Name} →
    {isExported isMeta : Bool} →
      {module' : Lean.Name} →
        {isExported' isMeta' : Bool} →
          { module := module, isExported := isExported, isMeta := isMeta } =
              { module := module', isExported := isExported', isMeta := isMeta' } →
            (module = module' → isExported = isExported' → isMeta = isMeta' → P) → P