[
  "��\u0004�\u001cĂ\u0001V\u00177z1h��",
  [
    [
      "Math.Lemmas.Int.multiply_fractions",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Prims_Tm_refine_c42d7927e44e0f393ec040dac09bfa8d"
      ],
      0,
      "c94c8cd46fd0a5b71d496411b413b65e"
    ],
    [
      "Math.Lemmas.Int.lemma_div_mod",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Prims_Tm_refine_c42d7927e44e0f393ec040dac09bfa8d"
      ],
      0,
      "e77e7a046de926fc1b12ef62622b7b86"
    ],
    [
      "Math.Lemmas.Int.lemma_div_lt",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.l_and",
        "equation_Prims.squash", "l_and-interp",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "720afd70eaf35ea92610a0257e70daba"
    ],
    [
      "Math.Lemmas.Int.small_div",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Prims_Tm_refine_c42d7927e44e0f393ec040dac09bfa8d"
      ],
      0,
      "ca3265f266b4700c05a6c8841b0bc27a"
    ],
    [
      "Math.Lemmas.Int.small_mod",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Prims_Tm_refine_c42d7927e44e0f393ec040dac09bfa8d"
      ],
      0,
      "5dbdc44e233f459501b270fd5b4d4e74"
    ],
    [
      "Math.Lemmas.Int.lemma_div_plus",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Prims_Tm_refine_c42d7927e44e0f393ec040dac09bfa8d"
      ],
      0,
      "f9e1bc03356a079a7cd17875698de910"
    ],
    [
      "Math.Lemmas.Int.lemma_mod_plus",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Prims_Tm_refine_c42d7927e44e0f393ec040dac09bfa8d"
      ],
      0,
      "cd88c41b0ccda205813bda348e4e0d27"
    ],
    [
      "Math.Lemmas.Int.cancel_mul_div",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Prims_Tm_refine_c42d7927e44e0f393ec040dac09bfa8d"
      ],
      0,
      "699e35ea167cefa6f2bde54ee8aee817"
    ],
    [
      "Math.Lemmas.Int.cancel_mul_mod",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Prims_Tm_refine_c42d7927e44e0f393ec040dac09bfa8d"
      ],
      0,
      "f42f37dc73dee0946de2259b0d1e04c4"
    ],
    [
      "Math.Lemmas.Int.mod_add_both",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Prims_Tm_refine_c42d7927e44e0f393ec040dac09bfa8d"
      ],
      0,
      "ee2ea10ef74ba2f41544973ad481d432"
    ],
    [
      "Math.Lemmas.Int.lemma_mod_add_distr",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Prims_Tm_refine_c42d7927e44e0f393ec040dac09bfa8d"
      ],
      0,
      "d5dbc4b3b6dfea242d8a59ee81813616"
    ],
    [
      "Math.Lemmas.Int.lemma_mod_sub_distr",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Prims_Tm_refine_c42d7927e44e0f393ec040dac09bfa8d"
      ],
      0,
      "eab416137383ddfb085f243f03f32b57"
    ],
    [
      "Math.Lemmas.Int.lemma_mod_mul_distr_l",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Prims_Tm_refine_c42d7927e44e0f393ec040dac09bfa8d"
      ],
      0,
      "f3db9cc9ab3b458ec3bafc209ec71e6e"
    ],
    [
      "Math.Lemmas.Int.lemma_mod_mul_distr_r",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Prims_Tm_refine_c42d7927e44e0f393ec040dac09bfa8d"
      ],
      0,
      "89df4f4187f7e0880ce46bec7033a507"
    ],
    [
      "Math.Lemmas.Int.lemma_div_exact",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Prims_Tm_refine_c42d7927e44e0f393ec040dac09bfa8d"
      ],
      0,
      "105600ebdfc9dc84712308a65ad37bd7"
    ],
    [
      "Math.Lemmas.Int.div_exact_r",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Prims_Tm_refine_c42d7927e44e0f393ec040dac09bfa8d"
      ],
      0,
      "1da3703cd0c35524be59366f99f53ba9"
    ],
    [
      "Math.Lemmas.Int.lemma_mod_spec",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Prims_Tm_refine_c42d7927e44e0f393ec040dac09bfa8d"
      ],
      0,
      "9cb1896aded8f39d01b51e31a124c024"
    ],
    [
      "Math.Lemmas.Int.lemma_mod_spec2",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Prims_Tm_refine_c42d7927e44e0f393ec040dac09bfa8d"
      ],
      0,
      "fba76a7b6fdcc90e4053689accefeca3"
    ],
    [
      "Math.Lemmas.Int.lemma_mod_plus_distr_l",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Prims_Tm_refine_c42d7927e44e0f393ec040dac09bfa8d"
      ],
      0,
      "9b50ccb23efb6bd4b667c9941cac7690"
    ],
    [
      "Math.Lemmas.Int.lemma_mod_plus_distr_r",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Prims_Tm_refine_c42d7927e44e0f393ec040dac09bfa8d"
      ],
      0,
      "e779ae0828f0b9446f5a0e59f39d7fb9"
    ],
    [
      "Math.Lemmas.Int.small_division_lemma_2",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Prims_Tm_refine_c42d7927e44e0f393ec040dac09bfa8d"
      ],
      0,
      "48c5b6ddfe976b13c3ede698cfef354b"
    ],
    [
      "Math.Lemmas.Int.division_propriety",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Prims_Tm_refine_c42d7927e44e0f393ec040dac09bfa8d"
      ],
      0,
      "7987e77963207dd9c4aff0e51ca84d39"
    ],
    [
      "Math.Lemmas.Int.division_definition",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Prims_Tm_refine_c42d7927e44e0f393ec040dac09bfa8d"
      ],
      0,
      "aca01f9b1b55b079f8fced3ad2be4275"
    ],
    [
      "Math.Lemmas.Int.multiple_division_lemma",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Prims_Tm_refine_c42d7927e44e0f393ec040dac09bfa8d"
      ],
      0,
      "f471297120d15be4ee1723ac0923e337"
    ],
    [
      "Math.Lemmas.Int.multiple_modulo_lemma",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Prims_Tm_refine_c42d7927e44e0f393ec040dac09bfa8d"
      ],
      0,
      "8871d9279166c47dc130bc3154a71c19"
    ],
    [
      "Math.Lemmas.Int.division_addition_lemma",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Prims_Tm_refine_c42d7927e44e0f393ec040dac09bfa8d"
      ],
      0,
      "9f11710ae9505018a0dd0055d0c817ac"
    ],
    [
      "Math.Lemmas.Int.division_sub_lemma",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Prims_Tm_refine_c42d7927e44e0f393ec040dac09bfa8d"
      ],
      0,
      "bb91d59417f9d8cb8bcd21cbcd063ba4"
    ],
    [
      "Math.Lemmas.Int.modulo_distributivity",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Prims_Tm_refine_c42d7927e44e0f393ec040dac09bfa8d"
      ],
      0,
      "0a3a28fc2b0efa8223202064c36060d2"
    ],
    [
      "Math.Lemmas.Int.modulo_addition_lemma",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Prims_Tm_refine_c42d7927e44e0f393ec040dac09bfa8d"
      ],
      0,
      "a6b71a54471ad4f8aee0bb7d7447ebb6"
    ],
    [
      "Math.Lemmas.Int.lemma_mod_sub",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Prims_Tm_refine_c42d7927e44e0f393ec040dac09bfa8d"
      ],
      0,
      "37c72787d87bbf59ea0ddd1306408805"
    ],
    [
      "Math.Lemmas.Int.mod_mult_exact",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Prims_Tm_refine_c42d7927e44e0f393ec040dac09bfa8d"
      ],
      0,
      "15b8cbaa88b57cca6c8a4d7d4ffc8ac2"
    ],
    [
      "Math.Lemmas.Int.mod_mul_div_exact",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp", "equation_Prims.pos",
        "equation_Prims.squash", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Prims_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "refinement_interpretation_Prims_Tm_refine_c42d7927e44e0f393ec040dac09bfa8d"
      ],
      0,
      "ec1e65ee59d5e3c5c404d4397afbf012"
    ],
    [
      "Math.Lemmas.Int.mod_pow2_div2",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.pos",
        "function_token_typing_Prims.__cache_version_number__",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b"
      ],
      0,
      "73f2e0e95381114177f12f490aa622ca"
    ],
    [
      "Math.Lemmas.Int.division_multiplication_lemma",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Prims_Tm_refine_c42d7927e44e0f393ec040dac09bfa8d"
      ],
      0,
      "0fc7901b29b774f7b56c382647c21d38"
    ],
    [
      "Math.Lemmas.Int.modulo_modulo_lemma",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Prims_Tm_refine_c42d7927e44e0f393ec040dac09bfa8d"
      ],
      0,
      "d1b747c8035fd1693e01df9472a716ce"
    ],
    [
      "Math.Lemmas.Int.lemma_mod_plus_injective",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b"
      ],
      0,
      "a580f609b7fa4aa7df8d245549fbe19a"
    ]
  ]
]