{P : Sort u} →
  {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' : 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 := env, messages := messages, scopes := scopes,
                                                usedQuotCtxts := usedQuotCtxts, nextMacroScope := nextMacroScope,
                                                maxRecDepth := maxRecDepth, ngen := ngen, auxDeclNGen := auxDeclNGen,
                                                infoState := infoState, traceState := traceState,
                                                snapshotTasks := snapshotTasks } =
                                              { env := env', messages := messages', scopes := scopes',
                                                usedQuotCtxts := usedQuotCtxts', nextMacroScope := nextMacroScope',
                                                maxRecDepth := maxRecDepth', ngen := ngen', auxDeclNGen := auxDeclNGen',
                                                infoState := infoState', traceState := traceState',
                                                snapshotTasks := snapshotTasks' } →
                                            (env = env' →
                                                messages = messages' →
                                                  scopes = scopes' →
                                                    usedQuotCtxts = usedQuotCtxts' →
                                                      nextMacroScope = nextMacroScope' →
                                                        maxRecDepth = maxRecDepth' →
                                                          ngen = ngen' →
                                                            auxDeclNGen = auxDeclNGen' →
                                                              infoState = infoState' →
                                                                traceState = traceState' →
                                                                  snapshotTasks = snapshotTasks' → P) →
                                              P