{motive : Lean.Environment → Sort u} →
  (t : Lean.Environment) →
    ((base : Lean.VisibilityMap✝ Lean.Kernel.Environment) →
        (serverBaseExts : Array Lean.EnvExtensionState) →
          (checked : Task Lean.Kernel.Environment) →
            (asyncConstsMap : Lean.VisibilityMap✝¹ Lean.AsyncConsts✝) →
              (asyncCtx? : Option Lean.AsyncContext✝) →
                (importRealizationCtx? : Option Lean.RealizationContext✝) →
                  (localRealizationCtxMap : Lean.NameMap Lean.RealizationContext✝¹) →
                    (allRealizations : Task (Lean.NameMap Lean.AsyncConst✝)) →
                      (isExporting : Bool) →
                        motive
                          { base := base, serverBaseExts := serverBaseExts, checked := checked,
                            asyncConstsMap := asyncConstsMap, asyncCtx? := asyncCtx?,
                            importRealizationCtx? := importRealizationCtx?,
                            localRealizationCtxMap := localRealizationCtxMap, allRealizations := allRealizations,
                            isExporting := isExporting }) →
      motive t