∀ (env : Lean.Environment) (messages : Lean.MessageLog) (scopes : List Lean.Elab.Command.Scope)
  (usedQuotCtxts : Lean.NameSet) (nextMacroScope maxRecDepth : ℕ) (ngen : Lean.NameGenerator)
  (auxDeclNGen : Lean.DeclNameGenerator) (infoState : Lean.Elab.InfoState) (traceState : Lean.TraceState)
  (snapshotTasks : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)) (env_1 : Lean.Environment)
  (messages_1 : Lean.MessageLog) (scopes_1 : List Lean.Elab.Command.Scope) (usedQuotCtxts_1 : Lean.NameSet)
  (nextMacroScope_1 maxRecDepth_1 : ℕ) (ngen_1 : Lean.NameGenerator) (auxDeclNGen_1 : Lean.DeclNameGenerator)
  (infoState_1 : Lean.Elab.InfoState) (traceState_1 : Lean.TraceState)
  (snapshotTasks_1 : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)),
  ({ env := env, messages := messages, scopes := scopes, usedQuotCtxts := usedQuotCtxts,
        nextMacroScope := nextMacroScope, maxRecDepth := maxRecDepth, ngen := ngen, auxDeclNGen := auxDeclNGen,
        infoState := infoState, traceState := traceState, snapshotTasks := snapshotTasks } =
      { env := env_1, messages := messages_1, scopes := scopes_1, usedQuotCtxts := usedQuotCtxts_1,
        nextMacroScope := nextMacroScope_1, maxRecDepth := maxRecDepth_1, ngen := ngen_1, auxDeclNGen := auxDeclNGen_1,
        infoState := infoState_1, traceState := traceState_1, snapshotTasks := snapshotTasks_1 }) =
    (env = env_1 ∧
      messages = messages_1 ∧
        scopes = scopes_1 ∧
          usedQuotCtxts = usedQuotCtxts_1 ∧
            nextMacroScope = nextMacroScope_1 ∧
              maxRecDepth = maxRecDepth_1 ∧
                ngen = ngen_1 ∧
                  auxDeclNGen = auxDeclNGen_1 ∧
                    infoState = infoState_1 ∧ traceState = traceState_1 ∧ snapshotTasks = snapshotTasks_1)