{ {
    children = { {
        children = {},
        deprecated = false,
        kind = 13,
        name = "Definition",
        range = {
          ["end"] = {
            character = 16,
            line = 18
          },
          start = {
            character = 0,
            line = 15
          }
        },
        selectionRange = {
          ["end"] = {
            character = 16,
            line = 18
          },
          start = {
            character = 0,
            line = 15
          }
        }
      }, {
        children = { {
            children = { {
                children = {},
                deprecated = false,
                kind = 22,
                name = "Item",
                range = {
                  ["end"] = {
                    character = 176,
                    line = 23
                  },
                  start = {
                    character = 2,
                    line = 23
                  }
                },
                selectionRange = {
                  ["end"] = {
                    character = 176,
                    line = 23
                  },
                  start = {
                    character = 2,
                    line = 23
                  }
                }
              }, {
                children = {},
                deprecated = false,
                kind = 22,
                name = "Item",
                range = {
                  ["end"] = {
                    character = 107,
                    line = 24
                  },
                  start = {
                    character = 2,
                    line = 24
                  }
                },
                selectionRange = {
                  ["end"] = {
                    character = 107,
                    line = 24
                  },
                  start = {
                    character = 2,
                    line = 24
                  }
                }
              }, {
                children = { {
                    children = { {
                        children = {},
                        deprecated = false,
                        kind = 22,
                        name = "Item",
                        range = {
                          ["end"] = {
                            character = 40,
                            line = 28
                          },
                          start = {
                            character = 9,
                            line = 28
                          }
                        },
                        selectionRange = {
                          ["end"] = {
                            character = 40,
                            line = 28
                          },
                          start = {
                            character = 9,
                            line = 28
                          }
                        }
                      }, {
                        children = {},
                        deprecated = false,
                        kind = 22,
                        name = "Item",
                        range = {
                          ["end"] = {
                            character = 53,
                            line = 29
                          },
                          start = {
                            character = 9,
                            line = 29
                          }
                        },
                        selectionRange = {
                          ["end"] = {
                            character = 53,
                            line = 29
                          },
                          start = {
                            character = 9,
                            line = 29
                          }
                        }
                      }, {
                        children = {},
                        deprecated = false,
                        kind = 22,
                        name = "Item",
                        range = {
                          ["end"] = {
                            character = 45,
                            line = 30
                          },
                          start = {
                            character = 9,
                            line = 30
                          }
                        },
                        selectionRange = {
                          ["end"] = {
                            character = 45,
                            line = 30
                          },
                          start = {
                            character = 9,
                            line = 30
                          }
                        }
                      } },
                    deprecated = false,
                    kind = 10,
                    name = "Enumerate",
                    range = {
                      ["end"] = {
                        character = 23,
                        line = 31
                      },
                      start = {
                        character = 8,
                        line = 27
                      }
                    },
                    selectionRange = {
                      ["end"] = {
                        character = 23,
                        line = 31
                      },
                      start = {
                        character = 8,
                        line = 27
                      }
                    }
                  } },
                deprecated = false,
                kind = 22,
                name = "Item",
                range = {
                  ["end"] = {
                    character = 23,
                    line = 31
                  },
                  start = {
                    character = 2,
                    line = 25
                  }
                },
                selectionRange = {
                  ["end"] = {
                    character = 23,
                    line = 31
                  },
                  start = {
                    character = 2,
                    line = 25
                  }
                }
              }, {
                children = {},
                deprecated = false,
                kind = 22,
                name = "Item",
                range = {
                  ["end"] = {
                    character = 45,
                    line = 32
                  },
                  start = {
                    character = 2,
                    line = 32
                  }
                },
                selectionRange = {
                  ["end"] = {
                    character = 45,
                    line = 32
                  },
                  start = {
                    character = 2,
                    line = 32
                  }
                }
              }, {
                children = {},
                deprecated = false,
                kind = 22,
                name = "Item",
                range = {
                  ["end"] = {
                    character = 42,
                    line = 33
                  },
                  start = {
                    character = 2,
                    line = 33
                  }
                },
                selectionRange = {
                  ["end"] = {
                    character = 42,
                    line = 33
                  },
                  start = {
                    character = 2,
                    line = 33
                  }
                }
              }, {
                children = {},
                deprecated = false,
                kind = 22,
                name = "Item",
                range = {
                  ["end"] = {
                    character = 75,
                    line = 34
                  },
                  start = {
                    character = 2,
                    line = 34
                  }
                },
                selectionRange = {
                  ["end"] = {
                    character = 75,
                    line = 34
                  },
                  start = {
                    character = 2,
                    line = 34
                  }
                }
              } },
            deprecated = false,
            kind = 10,
            name = "Enumerate",
            range = {
              ["end"] = {
                character = 16,
                line = 35
              },
              start = {
                character = 1,
                line = 22
              }
            },
            selectionRange = {
              ["end"] = {
                character = 16,
                line = 35
              },
              start = {
                character = 1,
                line = 22
              }
            }
          } },
        deprecated = false,
        kind = 13,
        name = "Theorem",
        range = {
          ["end"] = {
            character = 13,
            line = 36
          },
          start = {
            character = 0,
            line = 20
          }
        },
        selectionRange = {
          ["end"] = {
            character = 13,
            line = 36
          },
          start = {
            character = 0,
            line = 20
          }
        }
      }, {
        children = {},
        deprecated = false,
        kind = 10,
        name = "Enumerate",
        range = {
          ["end"] = {
            character = 15,
            line = 39
          },
          start = {
            character = 0,
            line = 37
          }
        },
        selectionRange = {
          ["end"] = {
            character = 15,
            line = 39
          },
          start = {
            character = 0,
            line = 37
          }
        }
      } },
    deprecated = false,
    kind = 2,
    name = "1 Main result",
    range = {
      ["end"] = {
        character = 15,
        line = 39
      },
      start = {
        character = 0,
        line = 13
      }
    },
    selectionRange = {
      ["end"] = {
        character = 15,
        line = 39
      },
      start = {
        character = 0,
        line = 13
      }
    }
  } }