∀ (env : Lean.Environment) (cmdEnv? : Option Lean.Environment) (fileMap : Lean.FileMap) (mctx : Lean.MetavarContext)
  (options : Lean.Options) (currNamespace : Lean.Name) (openDecls : List Lean.OpenDecl) (ngen : Lean.NameGenerator)
  (env_1 : Lean.Environment) (cmdEnv?_1 : Option Lean.Environment) (fileMap_1 : Lean.FileMap)
  (mctx_1 : Lean.MetavarContext) (options_1 : Lean.Options) (currNamespace_1 : Lean.Name)
  (openDecls_1 : List Lean.OpenDecl) (ngen_1 : Lean.NameGenerator),
  ({ env := env, cmdEnv? := cmdEnv?, fileMap := fileMap, mctx := mctx, options := options,
        currNamespace := currNamespace, openDecls := openDecls, ngen := ngen } =
      { env := env_1, cmdEnv? := cmdEnv?_1, fileMap := fileMap_1, mctx := mctx_1, options := options_1,
        currNamespace := currNamespace_1, openDecls := openDecls_1, ngen := ngen_1 }) =
    (env = env_1 ∧
      cmdEnv? = cmdEnv?_1 ∧
        fileMap = fileMap_1 ∧
          mctx = mctx_1 ∧
            options = options_1 ∧ currNamespace = currNamespace_1 ∧ openDecls = openDecls_1 ∧ ngen = ngen_1)