{motive : Lean.Environment.ConstPromiseVal✝ → Sort u} →
  (t : Lean.Environment.ConstPromiseVal✝¹) →
    ((privateConstInfo exportedConstInfo : Lean.ConstantInfo) →
        (exts : Array Lean.EnvExtensionState) →
          (nestedConsts : Lean.VisibilityMap✝ Lean.AsyncConsts✝) →
            motive
              { privateConstInfo := privateConstInfo, exportedConstInfo := exportedConstInfo, exts := exts,
                nestedConsts := nestedConsts }) →
      motive t