∀ {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