[
  "y\tÐãÜ”åW«ë’´È×Uù",
  [
    [
      "Vale.Math.Poly2.Defs.lemma_poly_equal_elim",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
        "equation_FStar.Math.Lib.max", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Math.Poly2.Defs.poly_equal",
        "equation_Vale.Math.Poly2.Defs_s.poly",
        "equation_Vale.Math.Poly2.Defs_s.poly_index",
        "equation_Vale.Math.Poly2.Defs_s.valid",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.bool", "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_3b1de445e68d5a7cbfc9e637b6d5fe5c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f",
        "typing_FStar.Math.Lib.max", "typing_FStar.Seq.Base.index",
        "typing_FStar.Seq.Base.length", "typing_Vale.Math.Poly2.Defs_s.valid"
      ],
      0,
      "a798b2bef127a4953368a1d4f56ec984"
    ],
    [
      "Vale.Math.Poly2.Defs.lemma_pointwise_equal",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.Math.Poly2.Defs.poly_equal",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "d109c6db51092dc1bc21209599061e26"
    ],
    [
      "Vale.Math.Poly2.Defs.lemma_add_zero",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
        "bool_typing", "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Vale.Math.Poly2.Defs.poly_equal",
        "equation_Vale.Math.Poly2.Defs_s.poly",
        "equation_Vale.Math.Poly2.Defs_s.poly_index",
        "equation_Vale.Math.Poly2.Defs_s.valid",
        "equation_Vale.Math.Poly2.Defs_s.zero",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.bool", "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_create_len", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_disEquality",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_06d278fd5617c2fb19b59f968ef9f2ee",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f",
        "typing_Vale.Math.Poly2.Defs_s.add",
        "typing_Vale.Math.Poly2.Defs_s.poly_index",
        "typing_Vale.Math.Poly2.Defs_s.valid",
        "typing_Vale.Math.Poly2.Defs_s.zero"
      ],
      0,
      "397d24fa1140f66b439edb2b2509f596"
    ],
    [
      "Vale.Math.Poly2.Defs.lemma_add_cancel",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
        "bool_typing", "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Vale.Math.Poly2.Defs.poly_equal",
        "equation_Vale.Math.Poly2.Defs_s.poly",
        "equation_Vale.Math.Poly2.Defs_s.poly_index",
        "equation_Vale.Math.Poly2.Defs_s.valid",
        "equation_Vale.Math.Poly2.Defs_s.zero",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.bool", "int_typing",
        "lemma_FStar.Seq.Base.lemma_create_len", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_disEquality",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_06d278fd5617c2fb19b59f968ef9f2ee",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f",
        "typing_Vale.Math.Poly2.Defs_s.add",
        "typing_Vale.Math.Poly2.Defs_s.valid"
      ],
      0,
      "7c292946f0c54bf7005844e1f839ca30"
    ],
    [
      "Vale.Math.Poly2.Defs.lemma_add_cancel_eq",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_typing",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Vale.Math.Poly2.Defs.poly_equal",
        "equation_Vale.Math.Poly2.Defs_s.poly_index",
        "equation_Vale.Math.Poly2.Defs_s.zero",
        "function_token_typing_Prims.bool", "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_create_len", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_disEquality",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_06d278fd5617c2fb19b59f968ef9f2ee",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Vale.Math.Poly2.Defs_s.add"
      ],
      0,
      "6c7a7f1ecb8105865cace2cad45fdab9"
    ],
    [
      "Vale.Math.Poly2.Defs.lemma_add_commute",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.Math.Poly2.Defs.poly_equal",
        "primitive_Prims.op_disEquality",
        "refinement_interpretation_Tm_refine_06d278fd5617c2fb19b59f968ef9f2ee",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Vale.Math.Poly2.Defs_s.add"
      ],
      0,
      "6936a15704c75af6e14da8a7bc4f8961"
    ],
    [
      "Vale.Math.Poly2.Defs.lemma_add_associate",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
        "bool_typing", "equation_Prims.nat",
        "equation_Vale.Math.Poly2.Defs.poly_equal",
        "equation_Vale.Math.Poly2.Defs_s.poly_index", "int_inversion",
        "primitive_Prims.op_disEquality",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_06d278fd5617c2fb19b59f968ef9f2ee",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Vale.Math.Poly2.Defs_s.add",
        "typing_Vale.Math.Poly2.Defs_s.poly_index"
      ],
      0,
      "bafd43fcfdfd7d18cda9374e136febc8"
    ],
    [
      "Vale.Math.Poly2.Defs.lemma_add_move",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
        "bool_typing", "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Vale.Math.Poly2.Defs_s.poly",
        "equation_Vale.Math.Poly2.Defs_s.valid",
        "equation_Vale.Math.Poly2.Defs_s.zero",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.bool", "int_typing",
        "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_Vale.Math.Poly2.Defs.lemma_poly_equal_elim",
        "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_06d278fd5617c2fb19b59f968ef9f2ee",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f",
        "typing_Vale.Math.Poly2.Defs_s.add",
        "typing_Vale.Math.Poly2.Defs_s.valid",
        "typing_Vale.Math.Poly2.Defs_s.zero"
      ],
      0,
      "c5a9d185f8f8ccef407ceadf5aeb4ce0"
    ],
    [
      "Vale.Math.Poly2.Defs.lemma_sum_empty",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "@query",
        "equation_with_fuel_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "int_inversion", "primitive_Prims.op_GreaterThanOrEqual",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "29959fc83ca2c1e7ffb7772281fb3b8b"
    ],
    [
      "Vale.Math.Poly2.Defs.lemma_sum_of_zero",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "@fuel_irrelevance_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "Vale.Math.Poly2.Defs_s_interpretation_Tm_arrow_2b00b574e3c859da902fc1b8ce85c0f1",
        "binder_x_ae567c2fb75be05905677af440075565_0",
        "binder_x_ae567c2fb75be05905677af440075565_1",
        "binder_x_d572127907d518d641a8068497b9d6e8_2", "bool_inversion",
        "bool_typing", "equality_tok_Prims.LexTop@tok",
        "equation_with_fuel_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_disEquality",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "typing_Vale.Math.Poly2.Defs_s.sum_of_bools",
        "well-founded-ordering-on-nat"
      ],
      0,
      "4786c50f9eab3c83b36da14867e804b9"
    ],
    [
      "Vale.Math.Poly2.Defs.lemma_sum_join",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "@fuel_irrelevance_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "Vale.Math.Poly2.Defs_s_interpretation_Tm_arrow_2b00b574e3c859da902fc1b8ce85c0f1",
        "binder_x_ae567c2fb75be05905677af440075565_0",
        "binder_x_ae567c2fb75be05905677af440075565_1",
        "binder_x_ae567c2fb75be05905677af440075565_2",
        "binder_x_d572127907d518d641a8068497b9d6e8_3", "bool_inversion",
        "bool_typing", "equality_tok_Prims.LexTop@tok",
        "equation_with_fuel_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_disEquality",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "token_correspondence_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "typing_Vale.Math.Poly2.Defs_s.sum_of_bools",
        "well-founded-ordering-on-nat"
      ],
      0,
      "8c3bec58eb9187df472506fa543acc3f"
    ],
    [
      "Vale.Math.Poly2.Defs.lemma_sum_extend",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "@query", "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "bool_inversion",
        "equation_with_fuel_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "int_inversion", "primitive_Prims.op_disEquality",
        "typing_Vale.Math.Poly2.Defs_s.sum_of_bools"
      ],
      0,
      "e164a09ba4a2f532b2d5791d1d7b1f4e"
    ],
    [
      "Vale.Math.Poly2.Defs.lemma_sum_of_pairs",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "@fuel_irrelevance_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "Vale.Math.Poly2.Defs_s_interpretation_Tm_arrow_2b00b574e3c859da902fc1b8ce85c0f1",
        "binder_x_ae567c2fb75be05905677af440075565_0",
        "binder_x_ae567c2fb75be05905677af440075565_1",
        "binder_x_d572127907d518d641a8068497b9d6e8_2",
        "binder_x_d572127907d518d641a8068497b9d6e8_3",
        "binder_x_d572127907d518d641a8068497b9d6e8_4", "bool_inversion",
        "bool_typing", "equality_tok_Prims.LexTop@tok",
        "equation_with_fuel_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_disEquality",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "token_correspondence_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "typing_Vale.Math.Poly2.Defs_s.sum_of_bools",
        "well-founded-ordering-on-nat"
      ],
      0,
      "e28fcba955d9bc5775ce3b8e31eb6297"
    ],
    [
      "Vale.Math.Poly2.Defs.lemma_sum_shift",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "@fuel_irrelevance_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_ae567c2fb75be05905677af440075565_0",
        "binder_x_ae567c2fb75be05905677af440075565_1",
        "binder_x_d572127907d518d641a8068497b9d6e8_3",
        "binder_x_d572127907d518d641a8068497b9d6e8_4",
        "equality_tok_Prims.LexTop@tok",
        "equation_with_fuel_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0", "well-founded-ordering-on-nat"
      ],
      0,
      "6da231e6074e3fac634c6cbff35d2c6e"
    ],
    [
      "Vale.Math.Poly2.Defs.lemma_sum_invert_rec",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "@fuel_irrelevance_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "Vale.Math.Poly2.Defs_s_interpretation_Tm_arrow_2b00b574e3c859da902fc1b8ce85c0f1",
        "binder_x_ae567c2fb75be05905677af440075565_0",
        "binder_x_ae567c2fb75be05905677af440075565_1",
        "binder_x_ae567c2fb75be05905677af440075565_2",
        "binder_x_d572127907d518d641a8068497b9d6e8_3",
        "binder_x_d572127907d518d641a8068497b9d6e8_4", "bool_inversion",
        "equality_tok_Prims.LexTop@tok",
        "equation_with_fuel_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_disEquality",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "typing_Vale.Math.Poly2.Defs_s.sum_of_bools",
        "well-founded-ordering-on-nat"
      ],
      0,
      "1f39f0397f26caeaafbbb3ad1fccd541"
    ],
    [
      "Vale.Math.Poly2.Defs.lemma_sum_invert",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "@query", "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "bool_inversion", "bool_typing",
        "equation_with_fuel_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "int_inversion", "int_typing",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_disEquality",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "typing_Vale.Math.Poly2.Defs_s.sum_of_bools"
      ],
      0,
      "36564712d99113ce668d3e5927de0a0e"
    ],
    [
      "Vale.Math.Poly2.Defs.lemma_sum_reverse",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "int_inversion", "int_typing",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "0d377e7750f7526525910acc8536c96a"
    ],
    [
      "Vale.Math.Poly2.Defs.lemma_sum_mul",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "@fuel_irrelevance_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "Vale.Math.Poly2.Defs_s_interpretation_Tm_arrow_2b00b574e3c859da902fc1b8ce85c0f1",
        "binder_x_ae567c2fb75be05905677af440075565_0",
        "binder_x_ae567c2fb75be05905677af440075565_1",
        "binder_x_d572127907d518d641a8068497b9d6e8_3",
        "binder_x_d572127907d518d641a8068497b9d6e8_4",
        "binder_x_f537159ed795b314b4e58c260361ae86_2", "bool_inversion",
        "equality_tok_Prims.LexTop@tok",
        "equation_with_fuel_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "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",
        "token_correspondence_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "typing_Vale.Math.Poly2.Defs_s.sum_of_bools",
        "well-founded-ordering-on-nat"
      ],
      0,
      "f25833503594ace3e108abfae31b4809"
    ],
    [
      "Vale.Math.Poly2.Defs.lemma_sum_swap",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "@fuel_irrelevance_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "Vale.Math.Poly2.Defs_interpretation_Tm_arrow_a3e60d2a4d3886e67c6e6d54fdc03056",
        "Vale.Math.Poly2.Defs_s_interpretation_Tm_arrow_2b00b574e3c859da902fc1b8ce85c0f1",
        "binder_x_1ede9435921966118aded11e9a38452e_2",
        "binder_x_1ede9435921966118aded11e9a38452e_3",
        "binder_x_ae567c2fb75be05905677af440075565_0",
        "binder_x_ae567c2fb75be05905677af440075565_1",
        "binder_x_d572127907d518d641a8068497b9d6e8_4",
        "binder_x_d572127907d518d641a8068497b9d6e8_5", "bool_inversion",
        "bool_typing", "equality_tok_Prims.LexTop@tok",
        "equation_with_fuel_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "interpretation_Tm_abs_38449486c044f5d5ec5d38d0307fdca3",
        "interpretation_Tm_abs_fa3a04a8e4ef10e4d16d146f67e25a39",
        "lemma_Vale.Math.Poly2.Defs.lemma_sum_empty",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_disEquality",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "token_correspondence_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "typing_Tm_abs_38449486c044f5d5ec5d38d0307fdca3",
        "typing_Tm_abs_b22ebf352860dc2cbad0f87bbe01ae00",
        "typing_Tm_abs_fa3a04a8e4ef10e4d16d146f67e25a39",
        "typing_Vale.Math.Poly2.Defs_s.sum_of_bools",
        "well-founded-ordering-on-nat"
      ],
      0,
      "0a24debcc6ea5a4cb30b7048fd3f5cb1"
    ],
    [
      "Vale.Math.Poly2.Defs.lemma_sum_swap_mul_associate",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "@query", "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "Vale.Math.Poly2.Defs_interpretation_Tm_arrow_a3e60d2a4d3886e67c6e6d54fdc03056",
        "Vale.Math.Poly2.Defs_s_interpretation_Tm_arrow_2b00b574e3c859da902fc1b8ce85c0f1",
        "binder_x_1ede9435921966118aded11e9a38452e_1",
        "binder_x_1ede9435921966118aded11e9a38452e_2",
        "binder_x_ae567c2fb75be05905677af440075565_0",
        "binder_x_d572127907d518d641a8068497b9d6e8_3",
        "binder_x_d572127907d518d641a8068497b9d6e8_4", "bool_inversion",
        "bool_typing", "equation_Prims.nat",
        "equation_with_fuel_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "int_inversion", "int_typing",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_disEquality",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Vale.Math.Poly2.Defs_s.sum_of_bools"
      ],
      0,
      "b762262a43b1baafb067d5a7ba6206c7"
    ],
    [
      "Vale.Math.Poly2.Defs.lemma_sum_pointwise_equal",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "@fuel_irrelevance_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_ae567c2fb75be05905677af440075565_0",
        "binder_x_ae567c2fb75be05905677af440075565_1",
        "binder_x_d572127907d518d641a8068497b9d6e8_2",
        "binder_x_d572127907d518d641a8068497b9d6e8_3",
        "equality_tok_Prims.LexTop@tok",
        "equation_with_fuel_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0", "well-founded-ordering-on-nat"
      ],
      0,
      "3355792cbb93d2cf7cf3084fbb3f9b6f"
    ],
    [
      "Vale.Math.Poly2.Defs.lemma_mul_element",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "@query",
        "Vale.Math.Poly2.Defs_s_interpretation_Tm_arrow_2b00b574e3c859da902fc1b8ce85c0f1",
        "Vale.Math.Poly2.Defs_s_interpretation_Tm_arrow_5368a5dcf3cc1245d9de2513f7e404d6",
        "bool_inversion", "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Vale.Math.Poly2.Defs_s.mul_element",
        "equation_Vale.Math.Poly2.Defs_s.mul_element_fun",
        "equation_Vale.Math.Poly2.Defs_s.poly",
        "equation_Vale.Math.Poly2.Defs_s.poly_index",
        "equation_Vale.Math.Poly2.Defs_s.valid",
        "equation_with_fuel_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "function_token_typing_Prims.bool",
        "function_token_typing_Vale.Math.Poly2.Defs_s.mul_element_fun",
        "int_inversion", "int_typing", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f",
        "refinement_interpretation_Tm_refine_fd244d6c9e4b35304d782c4ee6d82cfb",
        "typing_FStar.Seq.Base.length", "typing_Vale.Math.Poly2.Defs_s.mul",
        "typing_Vale.Math.Poly2.Defs_s.mul_element",
        "typing_Vale.Math.Poly2.Defs_s.poly_index",
        "typing_Vale.Math.Poly2.Defs_s.valid"
      ],
      0,
      "a034d0dc0e152629d8593826d4e6eb0e"
    ],
    [
      "Vale.Math.Poly2.Defs.lemma_mul_zero",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
        "bool_typing", "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Vale.Math.Poly2.Defs.poly_equal",
        "equation_Vale.Math.Poly2.Defs_s.mul_element",
        "equation_Vale.Math.Poly2.Defs_s.mul_element_fun",
        "equation_Vale.Math.Poly2.Defs_s.poly",
        "equation_Vale.Math.Poly2.Defs_s.poly_index",
        "equation_Vale.Math.Poly2.Defs_s.valid",
        "equation_Vale.Math.Poly2.Defs_s.zero",
        "equation_with_fuel_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.bool", "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_Vale.Math.Poly2.Defs.lemma_mul_element",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
        "primitive_Prims.op_Equality",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f",
        "refinement_interpretation_Tm_refine_fd244d6c9e4b35304d782c4ee6d82cfb",
        "typing_Vale.Math.Poly2.Defs_s.mul",
        "typing_Vale.Math.Poly2.Defs_s.mul_element",
        "typing_Vale.Math.Poly2.Defs_s.poly_index",
        "typing_Vale.Math.Poly2.Defs_s.sum_of_bools",
        "typing_Vale.Math.Poly2.Defs_s.valid",
        "typing_Vale.Math.Poly2.Defs_s.zero"
      ],
      0,
      "bd36a2c6f4802b7127d84c77db8900a2"
    ],
    [
      "Vale.Math.Poly2.Defs.lemma_mul_one",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "@fuel_irrelevance_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "@query", "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "bool_inversion", "bool_typing", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Math.Poly2.Defs.poly_equal",
        "equation_Vale.Math.Poly2.Defs_s.mul_element",
        "equation_Vale.Math.Poly2.Defs_s.mul_element_fun",
        "equation_Vale.Math.Poly2.Defs_s.one",
        "equation_Vale.Math.Poly2.Defs_s.poly",
        "equation_Vale.Math.Poly2.Defs_s.poly_index",
        "equation_Vale.Math.Poly2.Defs_s.valid",
        "equation_with_fuel_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "function_token_typing_Prims.bool", "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.Seq.Base.lemma_index_create",
        "lemma_Vale.Math.Poly2.Defs.lemma_mul_element",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_disEquality",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f",
        "token_correspondence_Vale.Math.Poly2.Defs_s.mul_element_fun",
        "token_correspondence_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "typing_FStar.Seq.Base.length",
        "typing_Vale.Math.Poly2.Defs_s.mul_element",
        "typing_Vale.Math.Poly2.Defs_s.one",
        "typing_Vale.Math.Poly2.Defs_s.poly_index",
        "typing_Vale.Math.Poly2.Defs_s.sum_of_bools",
        "typing_Vale.Math.Poly2.Defs_s.valid"
      ],
      0,
      "633468fa624045c8e2eba5acf716ba9e"
    ],
    [
      "Vale.Math.Poly2.Defs.lemma_mul_commute",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "equation_Prims.nat", "equation_Vale.Math.Poly2.Defs.poly_equal",
        "equation_Vale.Math.Poly2.Defs_s.mul_element",
        "equation_Vale.Math.Poly2.Defs_s.mul_element_fun",
        "equation_Vale.Math.Poly2.Defs_s.poly",
        "equation_Vale.Math.Poly2.Defs_s.poly_index",
        "equation_Vale.Math.Poly2.Defs_s.valid", "int_inversion",
        "int_typing", "lemma_Vale.Math.Poly2.Defs.lemma_mul_element",
        "primitive_Prims.op_AmpAmp", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f",
        "typing_Vale.Math.Poly2.Defs_s.poly_index"
      ],
      0,
      "4a569563bfad328f8cd425c37f4146c0"
    ],
    [
      "Vale.Math.Poly2.Defs.lemma_mul_associate",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "@fuel_irrelevance_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Vale.Math.Poly2.Defs_s_interpretation_Tm_arrow_2b00b574e3c859da902fc1b8ce85c0f1",
        "Vale.Math.Poly2.Defs_s_interpretation_Tm_arrow_5368a5dcf3cc1245d9de2513f7e404d6",
        "bool_inversion", "bool_typing", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Math.Poly2.Defs.poly_equal",
        "equation_Vale.Math.Poly2.Defs_s.mul_element",
        "equation_Vale.Math.Poly2.Defs_s.mul_element_fun",
        "equation_Vale.Math.Poly2.Defs_s.poly",
        "equation_Vale.Math.Poly2.Defs_s.poly_index",
        "equation_Vale.Math.Poly2.Defs_s.valid",
        "equation_with_fuel_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.bool",
        "function_token_typing_Vale.Math.Poly2.Defs_s.mul_element_fun",
        "int_inversion", "int_typing",
        "lemma_Vale.Math.Poly2.Defs.lemma_mul_element",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f",
        "refinement_interpretation_Tm_refine_fd244d6c9e4b35304d782c4ee6d82cfb",
        "token_correspondence_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_4784031f2a410f59f6c27f9858afd03e",
        "typing_Vale.Math.Poly2.Defs_s.mul",
        "typing_Vale.Math.Poly2.Defs_s.mul_element",
        "typing_Vale.Math.Poly2.Defs_s.poly_index",
        "typing_Vale.Math.Poly2.Defs_s.valid"
      ],
      0,
      "5de8acb7758c2487d731e66416b1d51a"
    ],
    [
      "Vale.Math.Poly2.Defs.lemma_mul_distribute",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "@query", "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "Vale.Math.Poly2.Defs_s_interpretation_Tm_arrow_2b00b574e3c859da902fc1b8ce85c0f1",
        "Vale.Math.Poly2.Defs_s_interpretation_Tm_arrow_5368a5dcf3cc1245d9de2513f7e404d6",
        "bool_inversion", "equation_Prims.nat",
        "equation_Vale.Math.Poly2.Defs.poly_equal",
        "equation_Vale.Math.Poly2.Defs_s.mul_element",
        "equation_Vale.Math.Poly2.Defs_s.mul_element_fun",
        "equation_Vale.Math.Poly2.Defs_s.poly",
        "equation_Vale.Math.Poly2.Defs_s.poly_index",
        "equation_Vale.Math.Poly2.Defs_s.valid",
        "equation_with_fuel_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "function_token_typing_Vale.Math.Poly2.Defs_s.mul_element_fun",
        "int_inversion", "int_typing",
        "lemma_Vale.Math.Poly2.Defs.lemma_mul_element",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_disEquality",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_06d278fd5617c2fb19b59f968ef9f2ee",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f",
        "refinement_interpretation_Tm_refine_fd244d6c9e4b35304d782c4ee6d82cfb",
        "typing_Vale.Math.Poly2.Defs_s.add",
        "typing_Vale.Math.Poly2.Defs_s.mul",
        "typing_Vale.Math.Poly2.Defs_s.mul_element",
        "typing_Vale.Math.Poly2.Defs_s.poly_index",
        "typing_Vale.Math.Poly2.Defs_s.valid"
      ],
      0,
      "c340a11d00f521ca7e928493128ed580"
    ],
    [
      "Vale.Math.Poly2.Defs.lemma_mul_distribute_left",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Vale.Math.Poly2.Defs.poly_equal",
        "lemma_Vale.Math.Poly2.Defs.lemma_poly_equal_elim",
        "refinement_interpretation_Tm_refine_fd244d6c9e4b35304d782c4ee6d82cfb",
        "typing_Vale.Math.Poly2.Defs_s.mul"
      ],
      0,
      "4dd5deb7117d80a65921c9659a19e2f7"
    ],
    [
      "Vale.Math.Poly2.Defs.lemma_shift_is_mul",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "@fuel_irrelevance_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "Vale.Math.Poly2.Defs_s_interpretation_Tm_arrow_2b00b574e3c859da902fc1b8ce85c0f1",
        "Vale.Math.Poly2.Defs_s_interpretation_Tm_arrow_5368a5dcf3cc1245d9de2513f7e404d6",
        "binder_x_3e94af60b2131294de5742284d9caf65_0",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1", "bool_inversion",
        "bool_typing", "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Vale.Math.Poly2.Defs.poly_equal",
        "equation_Vale.Math.Poly2.Defs_s.lshift",
        "equation_Vale.Math.Poly2.Defs_s.monomial",
        "equation_Vale.Math.Poly2.Defs_s.mul_element",
        "equation_Vale.Math.Poly2.Defs_s.mul_element_fun",
        "equation_Vale.Math.Poly2.Defs_s.one",
        "equation_Vale.Math.Poly2.Defs_s.poly",
        "equation_Vale.Math.Poly2.Defs_s.poly_index",
        "equation_Vale.Math.Poly2.Defs_s.shift",
        "equation_Vale.Math.Poly2.Defs_s.valid",
        "equation_with_fuel_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.bool",
        "function_token_typing_Vale.Math.Poly2.Defs_s.mul_element_fun",
        "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.Seq.Base.lemma_index_app1",
        "lemma_FStar.Seq.Base.lemma_index_app2",
        "lemma_FStar.Seq.Base.lemma_index_create",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_Vale.Math.Poly2.Defs.lemma_mul_element",
        "lemma_Vale.Math.Poly2.Defs.lemma_sum_empty",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction", "primitive_Prims.op_disEquality",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f",
        "token_correspondence_Vale.Math.Poly2.Defs_s.mul_element_fun",
        "token_correspondence_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.index",
        "typing_FStar.Seq.Base.length",
        "typing_Vale.Math.Poly2.Defs_s.monomial",
        "typing_Vale.Math.Poly2.Defs_s.mul_element",
        "typing_Vale.Math.Poly2.Defs_s.mul_element_fun",
        "typing_Vale.Math.Poly2.Defs_s.one",
        "typing_Vale.Math.Poly2.Defs_s.poly_index",
        "typing_Vale.Math.Poly2.Defs_s.shift",
        "typing_Vale.Math.Poly2.Defs_s.sum_of_bools",
        "typing_Vale.Math.Poly2.Defs_s.valid"
      ],
      0,
      "d75d6e4b718cb21c0ec94099ef274b75"
    ],
    [
      "Vale.Math.Poly2.Defs.lemma_mul_degree",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "Vale.Math.Poly2.Defs_s_interpretation_Tm_arrow_2b00b574e3c859da902fc1b8ce85c0f1",
        "Vale.Math.Poly2.Defs_s_interpretation_Tm_arrow_5368a5dcf3cc1245d9de2513f7e404d6",
        "bool_inversion", "bool_typing", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Math.Poly2.Defs.poly_equal",
        "equation_Vale.Math.Poly2.Defs_s.degree",
        "equation_Vale.Math.Poly2.Defs_s.mul_element",
        "equation_Vale.Math.Poly2.Defs_s.mul_element_fun",
        "equation_Vale.Math.Poly2.Defs_s.poly",
        "equation_Vale.Math.Poly2.Defs_s.poly_index",
        "equation_Vale.Math.Poly2.Defs_s.valid",
        "equation_Vale.Math.Poly2.Defs_s.zero",
        "equation_with_fuel_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.bool",
        "function_token_typing_Vale.Math.Poly2.Defs_s.mul_element_fun",
        "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_Vale.Math.Poly2.Defs.lemma_mul_element",
        "lemma_Vale.Math.Poly2.Defs.lemma_poly_equal_elim",
        "lemma_Vale.Math.Poly2.Defs.lemma_sum_empty",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
        "primitive_Prims.op_Equality",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_disEquality",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f",
        "refinement_interpretation_Tm_refine_fd244d6c9e4b35304d782c4ee6d82cfb",
        "token_correspondence_Vale.Math.Poly2.Defs_s.mul_element_fun",
        "token_correspondence_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
        "typing_Vale.Math.Poly2.Defs_s.mul",
        "typing_Vale.Math.Poly2.Defs_s.poly_index",
        "typing_Vale.Math.Poly2.Defs_s.sum_of_bools",
        "typing_Vale.Math.Poly2.Defs_s.valid", "unit_inversion",
        "unit_typing"
      ],
      0,
      "edb68fe471773b540f907a0d5d0b17f5"
    ],
    [
      "Vale.Math.Poly2.Defs.lemma_mul_reverse",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
        "bool_typing", "equation_FStar.Math.Lib.max",
        "equation_Prims.eqtype", "equation_Prims.min", "equation_Prims.nat",
        "equation_Vale.Math.Poly2.Defs.poly_equal",
        "equation_Vale.Math.Poly2.Defs_s.degree",
        "equation_Vale.Math.Poly2.Defs_s.mul_element",
        "equation_Vale.Math.Poly2.Defs_s.mul_element_fun",
        "equation_Vale.Math.Poly2.Defs_s.poly",
        "equation_Vale.Math.Poly2.Defs_s.poly_index",
        "equation_Vale.Math.Poly2.Defs_s.valid",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.bool", "int_inversion", "int_typing",
        "lemma_Vale.Math.Poly2.Defs.lemma_mul_element",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_3b1de445e68d5a7cbfc9e637b6d5fe5c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b1d28f840de949bc346d201a47c0cfe3",
        "refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f",
        "refinement_interpretation_Tm_refine_fd244d6c9e4b35304d782c4ee6d82cfb",
        "typing_FStar.Math.Lib.max", "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_9d5ec9113f4b570f18f3faa1801e323e",
        "typing_Vale.Math.Poly2.Defs_s.mul",
        "typing_Vale.Math.Poly2.Defs_s.poly_index",
        "typing_Vale.Math.Poly2.Defs_s.reverse",
        "typing_Vale.Math.Poly2.Defs_s.sum_of_bools",
        "typing_Vale.Math.Poly2.Defs_s.valid"
      ],
      0,
      "071200720947cb03742fdc4a3765c15a"
    ],
    [
      "Vale.Math.Poly2.Defs.lemma_div_mod",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.squash",
        "primitive_Prims.op_GreaterThan",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "7e2c39e040f1fefe4a3874a16ec4e0d7"
    ],
    [
      "Vale.Math.Poly2.Defs.lemma_div_mod",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.Math.Poly2.Defs_s.divmod.fuel_instrumented",
        "@fuel_correspondence_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "@fuel_irrelevance_Vale.Math.Poly2.Defs_s.divmod.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "Vale.Math.Poly2.Defs_s_interpretation_Tm_arrow_2b00b574e3c859da902fc1b8ce85c0f1",
        "Vale.Math.Poly2.Defs_s_interpretation_Tm_arrow_5368a5dcf3cc1245d9de2513f7e404d6",
        "b2t_def", "binder_x_3e94af60b2131294de5742284d9caf65_0",
        "binder_x_3e94af60b2131294de5742284d9caf65_1", "bool_inversion",
        "bool_typing", "equality_tok_Prims.LexTop@tok",
        "equation_FStar.Math.Lib.max",
        "equation_FStar.Pervasives.Native.fst",
        "equation_FStar.Pervasives.Native.snd", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Vale.Math.Poly2.Defs.poly_equal",
        "equation_Vale.Math.Poly2.Defs_s.div",
        "equation_Vale.Math.Poly2.Defs_s.lshift",
        "equation_Vale.Math.Poly2.Defs_s.mod",
        "equation_Vale.Math.Poly2.Defs_s.mul_element",
        "equation_Vale.Math.Poly2.Defs_s.mul_element_fun",
        "equation_Vale.Math.Poly2.Defs_s.poly",
        "equation_Vale.Math.Poly2.Defs_s.poly_index",
        "equation_Vale.Math.Poly2.Defs_s.shift",
        "equation_Vale.Math.Poly2.Defs_s.valid",
        "equation_Vale.Math.Poly2.Defs_s.zero",
        "equation_with_fuel_Vale.Math.Poly2.Defs_s.divmod.fuel_instrumented",
        "equation_with_fuel_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.bool",
        "function_token_typing_Vale.Math.Poly2.Defs_s.mul_element_fun",
        "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.Seq.Base.lemma_index_app2",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_Vale.Math.Poly2.Defs.lemma_mul_element",
        "lemma_Vale.Math.Poly2.Defs.lemma_poly_equal_elim",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
        "primitive_Prims.op_GreaterThan",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction", "primitive_Prims.op_disEquality",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__1",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_Tm_refine_06d278fd5617c2fb19b59f968ef9f2ee",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_3b1de445e68d5a7cbfc9e637b6d5fe5c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_919a8154a884fef643f87583005a7c0a",
        "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f",
        "refinement_interpretation_Tm_refine_fd244d6c9e4b35304d782c4ee6d82cfb",
        "token_correspondence_Vale.Math.Poly2.Defs_s.mul_element_fun",
        "token_correspondence_Vale.Math.Poly2.Defs_s.sum_of_bools.fuel_instrumented",
        "typing_FStar.Math.Lib.max", "typing_FStar.Seq.Base.create",
        "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
        "typing_Vale.Math.Poly2.Defs_s.add",
        "typing_Vale.Math.Poly2.Defs_s.div",
        "typing_Vale.Math.Poly2.Defs_s.mod",
        "typing_Vale.Math.Poly2.Defs_s.mul",
        "typing_Vale.Math.Poly2.Defs_s.poly_index",
        "typing_Vale.Math.Poly2.Defs_s.shift",
        "typing_Vale.Math.Poly2.Defs_s.valid",
        "typing_Vale.Math.Poly2.Defs_s.zero", "well-founded-ordering-on-nat"
      ],
      0,
      "5ac366b9dbdf7c687183ac2326ec1403"
    ],
    [
      "Vale.Math.Poly2.Defs.lemma_div_degree",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.squash",
        "primitive_Prims.op_GreaterThan",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "9a7c0dee34c70b4392982a8b8884a6b7"
    ],
    [
      "Vale.Math.Poly2.Defs.lemma_div_degree",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.Math.Poly2.Defs_s.divmod.fuel_instrumented",
        "@fuel_irrelevance_Vale.Math.Poly2.Defs_s.divmod.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
        "binder_x_3e94af60b2131294de5742284d9caf65_0",
        "binder_x_3e94af60b2131294de5742284d9caf65_1", "bool_inversion",
        "bool_typing", "equality_tok_Prims.LexTop@tok",
        "equation_FStar.Math.Lib.max",
        "equation_FStar.Pervasives.Native.fst", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Vale.Math.Poly2.Defs_s.degree",
        "equation_Vale.Math.Poly2.Defs_s.div",
        "equation_Vale.Math.Poly2.Defs_s.lshift",
        "equation_Vale.Math.Poly2.Defs_s.monomial",
        "equation_Vale.Math.Poly2.Defs_s.one",
        "equation_Vale.Math.Poly2.Defs_s.poly",
        "equation_Vale.Math.Poly2.Defs_s.poly_index",
        "equation_Vale.Math.Poly2.Defs_s.shift",
        "equation_Vale.Math.Poly2.Defs_s.valid",
        "equation_Vale.Math.Poly2.Defs_s.zero",
        "equation_with_fuel_Vale.Math.Poly2.Defs_s.divmod.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.bool", "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.Seq.Base.lemma_index_app2",
        "lemma_FStar.Seq.Base.lemma_index_create",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
        "primitive_Prims.op_GreaterThan",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction", "primitive_Prims.op_disEquality",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "refinement_interpretation_Tm_refine_06d278fd5617c2fb19b59f968ef9f2ee",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_3b1de445e68d5a7cbfc9e637b6d5fe5c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_919a8154a884fef643f87583005a7c0a",
        "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f",
        "typing_FStar.Math.Lib.max", "typing_FStar.Seq.Base.create",
        "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
        "typing_Vale.Math.Poly2.Defs_s.add",
        "typing_Vale.Math.Poly2.Defs_s.div",
        "typing_Vale.Math.Poly2.Defs_s.monomial",
        "typing_Vale.Math.Poly2.Defs_s.one",
        "typing_Vale.Math.Poly2.Defs_s.poly_index",
        "typing_Vale.Math.Poly2.Defs_s.shift",
        "typing_Vale.Math.Poly2.Defs_s.valid", "well-founded-ordering-on-nat"
      ],
      0,
      "db3107aa8a0df30bbb098f142c1f1159"
    ],
    [
      "Vale.Math.Poly2.Defs.lemma_mod_degree",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.squash",
        "primitive_Prims.op_GreaterThan",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "54274df4d8338b7af82f51f68d48cf6c"
    ],
    [
      "Vale.Math.Poly2.Defs.lemma_mod_degree",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.Math.Poly2.Defs_s.divmod.fuel_instrumented",
        "@fuel_irrelevance_Vale.Math.Poly2.Defs_s.divmod.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
        "binder_x_3e94af60b2131294de5742284d9caf65_0",
        "binder_x_3e94af60b2131294de5742284d9caf65_1", "bool_inversion",
        "bool_typing", "equality_tok_Prims.LexTop@tok",
        "equation_FStar.Math.Lib.max",
        "equation_FStar.Pervasives.Native.snd", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Vale.Math.Poly2.Defs_s.degree",
        "equation_Vale.Math.Poly2.Defs_s.lshift",
        "equation_Vale.Math.Poly2.Defs_s.mod",
        "equation_Vale.Math.Poly2.Defs_s.poly",
        "equation_Vale.Math.Poly2.Defs_s.poly_index",
        "equation_Vale.Math.Poly2.Defs_s.shift",
        "equation_Vale.Math.Poly2.Defs_s.valid",
        "equation_with_fuel_Vale.Math.Poly2.Defs_s.divmod.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.bool", "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.Seq.Base.lemma_index_app2",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
        "primitive_Prims.op_GreaterThan",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction", "primitive_Prims.op_disEquality",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_3b1de445e68d5a7cbfc9e637b6d5fe5c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_919a8154a884fef643f87583005a7c0a",
        "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_f57a9e437e59d89f626741292bcb316f",
        "typing_FStar.Math.Lib.max", "typing_FStar.Seq.Base.create",
        "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
        "typing_Vale.Math.Poly2.Defs_s.poly_index",
        "typing_Vale.Math.Poly2.Defs_s.shift",
        "typing_Vale.Math.Poly2.Defs_s.valid", "well-founded-ordering-on-nat"
      ],
      0,
      "871769198063958acc359f4d05f1ba0c"
    ]
  ]
]