{P : Sort u} →
  {privateConstInfo exportedConstInfo : Lean.ConstantInfo} →
    {exts : Array Lean.EnvExtensionState} →
      {nestedConsts : Lean.VisibilityMap✝ Lean.AsyncConsts✝} →
        {privateConstInfo' exportedConstInfo' : Lean.ConstantInfo} →
          {exts' : Array Lean.EnvExtensionState} →
            {nestedConsts' : Lean.VisibilityMap✝¹ Lean.AsyncConsts✝¹} →
              { privateConstInfo := privateConstInfo, exportedConstInfo := exportedConstInfo, exts := exts,
                    nestedConsts := nestedConsts } =
                  { privateConstInfo := privateConstInfo', exportedConstInfo := exportedConstInfo', exts := exts',
                    nestedConsts := nestedConsts' } →
                (privateConstInfo = privateConstInfo' →
                    exportedConstInfo = exportedConstInfo' → exts = exts' → nestedConsts = nestedConsts' → P) →
                  P