{P : Sort u} →
  {leadingTable : Lean.Parser.TokenMap (Lean.Parser.Parser × ℕ)} →
    {leadingParsers : List (Lean.Parser.Parser × ℕ)} →
      {trailingTable : Lean.Parser.TokenMap (Lean.Parser.Parser × ℕ)} →
        {trailingParsers : List (Lean.Parser.Parser × ℕ)} →
          {leadingTable' : Lean.Parser.TokenMap (Lean.Parser.Parser × ℕ)} →
            {leadingParsers' : List (Lean.Parser.Parser × ℕ)} →
              {trailingTable' : Lean.Parser.TokenMap (Lean.Parser.Parser × ℕ)} →
                {trailingParsers' : List (Lean.Parser.Parser × ℕ)} →
                  { leadingTable := leadingTable, leadingParsers := leadingParsers, trailingTable := trailingTable,
                        trailingParsers := trailingParsers } =
                      { leadingTable := leadingTable', leadingParsers := leadingParsers',
                        trailingTable := trailingTable', trailingParsers := trailingParsers' } →
                    (leadingTable = leadingTable' →
                        leadingParsers = leadingParsers' →
                          trailingTable = trailingTable' → trailingParsers = trailingParsers' → P) →
                      P