[
  "üÚ\u0011W&\u0001-dëq¢Þ\ty+•",
  [
    [
      "Lib.NatMod.mk_nat_comm_monoid",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "37275c3c927a0dd62fe150c4d91a62b5"
    ],
    [
      "Lib.NatMod.pow",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_ae567c2fb75be05905677af440075565_0",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1", "equation_Prims.nat",
        "equation_Prims.op_Equals_Equals_Equals",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_Equality",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "well-founded-ordering-on-nat"
      ],
      0,
      "39acb71f29ae69090d991cbea2bc2c9e"
    ],
    [
      "Lib.NatMod.lemma_pow_unfold",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "b4e321043cef9ee54b5205513f54d313"
    ],
    [
      "Lib.NatMod.lemma_pow_add",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "d5afa31268419bb79ff3849fca8f3544"
    ],
    [
      "Lib.NatMod.lemma_pow_mul",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "37c0ade088bf129fea15112674fbbcb3"
    ],
    [
      "Lib.NatMod.lemma_pow_double",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "1bbfce1ebe5293777473fc0c824b40ef"
    ],
    [
      "Lib.NatMod.lemma_pow_mod_base",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "14c3f6a2071c801fe49371152be27ce7"
    ],
    [
      "Lib.NatMod.one_mod",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "int_inversion", "primitive_Prims.op_Modulus",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "97c9cbb47f08ee69ac7daa2a59a52a0c"
    ],
    [
      "Lib.NatMod.mul_mod",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "int_inversion", "primitive_Prims.op_Modulus",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "47cc071ebab62fc9e027fd77565214f3"
    ],
    [
      "Lib.NatMod.add_mod",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "int_inversion", "primitive_Prims.op_Modulus",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "ae9183a870f6e9506d37d913582f05fc"
    ],
    [
      "Lib.NatMod.sub_mod",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "int_inversion", "primitive_Prims.op_Modulus",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "0f302142b51e57a99554086ef67c509c"
    ],
    [
      "Lib.NatMod.lemma_pow_mod",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "cc9886da46a779fb060466a77f464cd1"
    ],
    [
      "Lib.NatMod.lemma_pow_nat_mod_is_pow",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "c982668ac395862f1c810c6f42f10f73"
    ],
    [
      "Lib.NatMod.lemma_add_mod_one",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "3a022129576ac4ee324e18774971ee9c"
    ],
    [
      "Lib.NatMod.inv_mod",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Lib.NatMod.prime",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_c94e6d54c545297365221a2bcc484b9a"
      ],
      0,
      "a493bd662f6dd19dd26c49acd99b1a10"
    ],
    [
      "Lib.NatMod.lemma_div_mod_prime_one",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Lib.NatMod.prime",
        "refinement_interpretation_Tm_refine_c94e6d54c545297365221a2bcc484b9a"
      ],
      0,
      "b45ca0d2ab160c36727ca87704df8349"
    ]
  ]
]