{P : Sort u} →
  {mainEnv asyncEnv : Lean.Environment} →
    {constName : Lean.Name} →
      {kind : Lean.ConstantKind} →
        {exportedKind? : Option Lean.ConstantKind} →
          {sigPromise : IO.Promise Lean.ConstantVal} →
            {constPromise : IO.Promise Lean.Environment.ConstPromiseVal✝} →
              {checkedEnvPromise : IO.Promise Lean.Kernel.Environment} →
                {allRealizationsPromise : IO.Promise (Lean.NameMap Lean.AsyncConst✝)} →
                  {mainEnv' asyncEnv' : Lean.Environment} →
                    {constName' : Lean.Name} →
                      {kind' : Lean.ConstantKind} →
                        {exportedKind?' : Option Lean.ConstantKind} →
                          {sigPromise' : IO.Promise Lean.ConstantVal} →
                            {constPromise' : IO.Promise Lean.Environment.ConstPromiseVal✝¹} →
                              {checkedEnvPromise' : IO.Promise Lean.Kernel.Environment} →
                                {allRealizationsPromise' : IO.Promise (Lean.NameMap Lean.AsyncConst✝¹)} →
                                  { mainEnv := mainEnv, asyncEnv := asyncEnv, constName := constName, kind := kind,
                                        exportedKind? := exportedKind?, sigPromise := sigPromise,
                                        constPromise := constPromise, checkedEnvPromise := checkedEnvPromise,
                                        allRealizationsPromise := allRealizationsPromise } =
                                      { mainEnv := mainEnv', asyncEnv := asyncEnv', constName := constName',
                                        kind := kind', exportedKind? := exportedKind?', sigPromise := sigPromise',
                                        constPromise := constPromise', checkedEnvPromise := checkedEnvPromise',
                                        allRealizationsPromise := allRealizationsPromise' } →
                                    (mainEnv = mainEnv' →
                                        asyncEnv = asyncEnv' →
                                          constName = constName' →
                                            kind = kind' →
                                              exportedKind? = exportedKind?' →
                                                sigPromise = sigPromise' →
                                                  constPromise = constPromise' →
                                                    checkedEnvPromise = checkedEnvPromise' →
                                                      allRealizationsPromise = allRealizationsPromise' → P) →
                                      P