[
  "\u001fp;�`E�v\"�4\u0011�\u000b;\b",
  [
    [
      "Math.Poly2.Lemmas.lemma_shift_define_forward",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "int_inversion", "int_typing",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "477b5c1b9802bf46ee2a7bf60ca605d2"
    ],
    [
      "Math.Poly2.Lemmas.lemma_degree_is",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "int_inversion", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Math.Poly2_s.degree"
      ],
      0,
      "e700cd44b6a7ebe9274fd6e795bb761f"
    ],
    [
      "Math.Poly2.Lemmas.lemma_degree_negative",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "typing_Math.Poly2_s.poly_index", "typing_Math.Poly2_s.zero"
      ],
      0,
      "77ba342cfb9733eb1991ccb0ba58bf81"
    ],
    [
      "Math.Poly2.Lemmas.lemma_zero_degree",
      1,
      1,
      0,
      [ "@query", "typing_Math.Poly2_s.degree", "typing_Math.Poly2_s.zero" ],
      0,
      "39e699e3dccfabb340492dc8c18b36ee"
    ],
    [
      "Math.Poly2.Lemmas.lemma_monomial_degree",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "primitive_Prims.op_Equality",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "339ff7e0ce4851534f2020823bc7a10b"
    ],
    [
      "Math.Poly2.Lemmas.lemma_shift_degree",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Math.Poly2_s.degree", "typing_Math.Poly2_s.poly_index",
        "typing_Math.Poly2_s.zero"
      ],
      0,
      "c17f9cf1055d9e1b42728ad0301e48d1"
    ],
    [
      "Math.Poly2.Lemmas.lemma_reverse_degree",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "int_inversion", "int_typing", "primitive_Prims.op_AmpAmp",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Math.Poly2_s.degree", "typing_Math.Poly2_s.reverse"
      ],
      0,
      "9a747f6f147fdbe85b559d254250964e"
    ],
    [
      "Math.Poly2.Lemmas.lemma_of_list_degree",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.bool", "int_inversion",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.List.Tot.Base.length"
      ],
      0,
      "51c805211f1ffa0311ab97ab97ea6db4"
    ],
    [
      "Math.Poly2.Lemmas.lemma_of_list_degree",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.index.fuel_instrumented",
        "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "@fuel_irrelevance_FStar.List.Tot.Base.index.fuel_instrumented",
        "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
        "bool_typing", "constructor_distinct_Tm_unit",
        "disc_equation_Prims.Cons", "equation_FStar.List.Tot.Base.tail",
        "equation_FStar.List.Tot.Base.tl", "equation_Prims.eqtype",
        "equation_Prims.nat",
        "equation_with_fuel_FStar.List.Tot.Base.index.fuel_instrumented",
        "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.bool",
        "function_token_typing_Prims.int",
        "haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d", "int_inversion",
        "int_typing", "lemma_FStar.Seq.Properties.lemma_seq_of_list_index",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_3d7b649663b4fab04cceb6e2c2c28fc1",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_5b76b1c4682092d8298d5677347b4a58",
        "refinement_interpretation_Tm_refine_7aac12c24449a22c34d98a0ea8ed4a32",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d2d1ea66f2b3a92c2deb42edcbb784ce",
        "typing_FStar.List.Tot.Base.length", "typing_FStar.List.Tot.Base.tl",
        "typing_FStar.Seq.Base.length", "typing_Math.Poly2_s.degree",
        "typing_Math.Poly2_s.poly_index"
      ],
      0,
      "6c73a3c4921d5bc30e8c9858b86c17ce"
    ],
    [
      "Math.Poly2.Lemmas.lemma_mul_distribute_left",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "5dc755f970ebab63dbe13c3c18786fe6"
    ],
    [
      "Math.Poly2.Lemmas.lemma_mul_smaller_is_zero",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Math.Poly2.Lemmas.lemma_zero_degree",
        "function_token_typing_Math.Poly2.Lemmas.lemma_zero_degree",
        "int_inversion", "lemma_Math.Poly2.lemma_mul_degree",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Math.Poly2.Lemmas_Tm_refine_5468a4a33c97ff1e544f3d9c480e68d2",
        "typing_Math.Poly2_s.degree"
      ],
      0,
      "8c12b3eddc002c4c533d074cb4e324eb"
    ],
    [
      "Math.Poly2.Lemmas.lemma_mul_monomials",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "826be38cc314a88a89c06d12ba0190c9"
    ],
    [
      "Math.Poly2.Lemmas.lemma_mul_monomials",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Equality",
        "primitive_Prims.op_GreaterThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "299cb4f19b70205cbeb6884c08ade134"
    ],
    [
      "Math.Poly2.Lemmas.lemma_mul_reverse_shift_1",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "189362c85aa2e7f5692a12cad2d06e5d"
    ],
    [
      "Math.Poly2.Lemmas.lemma_mul_reverse_shift_1",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "equation_Prims.nat", "int_typing",
        "lemma_Math.Poly2.lemma_mul_degree", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_GreaterThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Math.Poly2_s.mul", "typing_Math.Poly2_s.poly_index"
      ],
      0,
      "8ab018ea75274e1f90593cfafe675dad"
    ],
    [
      "Math.Poly2.Lemmas.lemma_mod_distribute",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
        "bool_typing", "int_inversion", "lemma_Math.Poly2.lemma_add_degree",
        "lemma_Math.Poly2.lemma_mod_degree",
        "primitive_Prims.op_disEquality",
        "projection_inverse_BoxBool_proj_0", "typing_Math.Poly2_s.add",
        "typing_Math.Poly2_s.div", "typing_Math.Poly2_s.mod",
        "typing_Math.Poly2_s.mul", "typing_Math.Poly2_s.poly_index"
      ],
      0,
      "f9ea50c982c80fea342ce72c014c1164"
    ],
    [
      "Math.Poly2.Lemmas.lemma_div_mod_unique",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
        "bool_typing", "int_inversion", "lemma_Math.Poly2.lemma_add_degree",
        "lemma_Math.Poly2.lemma_mod_degree",
        "primitive_Prims.op_disEquality",
        "projection_inverse_BoxBool_proj_0", "typing_Math.Poly2_s.div",
        "typing_Math.Poly2_s.mod", "typing_Math.Poly2_s.mul",
        "typing_Math.Poly2_s.poly_index"
      ],
      0,
      "96557ebf8d0741d23ecc8ed225e14da6"
    ],
    [
      "Math.Poly2.Lemmas.lemma_div_mod_exact",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Math.Poly2.Lemmas.lemma_zero_degree",
        "function_token_typing_Math.Poly2.Lemmas.lemma_zero_degree",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_5468a4a33c97ff1e544f3d9c480e68d2"
      ],
      0,
      "42e36cd41fe1a96791f66ae390726acb"
    ],
    [
      "Math.Poly2.Lemmas.lemma_mod_small",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "6133622d5b2a53ca28faef55be77b951"
    ],
    [
      "Math.Poly2.Lemmas.lemma_mod_mod",
      1,
      1,
      0,
      [ "@query", "lemma_Math.Poly2.lemma_mod_degree" ],
      0,
      "263e97708c6912638f3fe5824d98750a"
    ],
    [
      "Math.Poly2.Lemmas.lemma_mod_cancel",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "bfc7f485e34c1e6428b9cb8445d57d26"
    ],
    [
      "Math.Poly2.Lemmas.lemma_mod_mul_mod",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
        "bool_typing", "int_inversion", "lemma_Math.Poly2.lemma_add_degree",
        "lemma_Math.Poly2.lemma_mod_degree",
        "primitive_Prims.op_disEquality",
        "projection_inverse_BoxBool_proj_0", "typing_Math.Poly2_s.add",
        "typing_Math.Poly2_s.div", "typing_Math.Poly2_s.mod",
        "typing_Math.Poly2_s.mul", "typing_Math.Poly2_s.poly_index"
      ],
      0,
      "954e6de838bc2c33cc8e6e7de8043a6e"
    ],
    [
      "Math.Poly2.Lemmas.lemma_split_define",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
        "equation_Prims.nat", "int_inversion", "int_typing",
        "lemma_Math.Poly2.Lemmas.lemma_monomial_degree",
        "lemma_Math.Poly2.lemma_mod_degree", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_disEquality",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Math.Poly2_s.div", "typing_Math.Poly2_s.mod",
        "typing_Math.Poly2_s.monomial", "typing_Math.Poly2_s.mul",
        "typing_Math.Poly2_s.poly_index"
      ],
      0,
      "40a18978864d24bb7ca314e410514cf2"
    ],
    [
      "Math.Poly2.Lemmas.lemma_split_define_forward",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_LessThan",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Math.Poly2_s.div", "typing_Math.Poly2_s.monomial",
        "typing_Math.Poly2_s.poly_index"
      ],
      0,
      "1d15e356d0389977032d5a9a32743cd2"
    ],
    [
      "Math.Poly2.Lemmas.lemma_combine_define",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "equation_Prims.nat", "int_inversion", "int_typing",
        "lemma_Math.Poly2.Lemmas.lemma_monomial_degree",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_disEquality",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Math.Poly2_s.add", "typing_Math.Poly2_s.div",
        "typing_Math.Poly2_s.mod", "typing_Math.Poly2_s.monomial",
        "typing_Math.Poly2_s.mul", "typing_Math.Poly2_s.poly_index"
      ],
      0,
      "872ae05c679f3f9c2f40b85a4c1bc7f9"
    ]
  ]
]