{P : Sort u} →
  {expandMacro? : Lean.Syntax → Lean.MacroM (Option Lean.Syntax)} →
    {getCurrNamespace : Lean.MacroM Lean.Name} →
      {hasDecl : Lean.Name → Lean.MacroM Bool} →
        {resolveNamespace : Lean.Name → Lean.MacroM (List Lean.Name)} →
          {resolveGlobalName : Lean.Name → Lean.MacroM (List (Lean.Name × List String))} →
            {expandMacro?' : Lean.Syntax → Lean.MacroM (Option Lean.Syntax)} →
              {getCurrNamespace' : Lean.MacroM Lean.Name} →
                {hasDecl' : Lean.Name → Lean.MacroM Bool} →
                  {resolveNamespace' : Lean.Name → Lean.MacroM (List Lean.Name)} →
                    {resolveGlobalName' : Lean.Name → Lean.MacroM (List (Lean.Name × List String))} →
                      { expandMacro? := expandMacro?, getCurrNamespace := getCurrNamespace, hasDecl := hasDecl,
                            resolveNamespace := resolveNamespace, resolveGlobalName := resolveGlobalName } =
                          { expandMacro? := expandMacro?', getCurrNamespace := getCurrNamespace', hasDecl := hasDecl',
                            resolveNamespace := resolveNamespace', resolveGlobalName := resolveGlobalName' } →
                        (expandMacro? = expandMacro?' →
                            getCurrNamespace = getCurrNamespace' →
                              hasDecl = hasDecl' →
                                resolveNamespace = resolveNamespace' → resolveGlobalName = resolveGlobalName' → P) →
                          P