[
  "g™~óÙ¨¨Êk缪\u001f߆Š",
  [
    [
      "Vale.Math.Poly2.Words.lemma_quad32_zero",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
        "equation_Vale.Math.Poly2.Bits.poly128_of_nat32s",
        "equation_Vale.Math.Poly2.Bits.poly128_of_poly32s",
        "function_token_typing_Vale.Math.Poly2.Bits.of_nat32_zero",
        "function_token_typing_Vale.Math.Poly2.Lemmas.lemma_zero_degree",
        "int_inversion", "int_typing", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_disEquality", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_4337ec945cb4c294d0e8ff2d420e64d7",
        "refinement_interpretation_Tm_refine_6c3579831eb81025494abc2bedea1303",
        "typing_Vale.Math.Poly2_s.add",
        "typing_Vale.Math.Poly2_s.poly_index",
        "typing_Vale.Math.Poly2_s.shift", "typing_Vale.Math.Poly2_s.zero"
      ],
      0,
      "744f77daf7f8e8fc65ab58fcd4e26b7e"
    ],
    [
      "Vale.Math.Poly2.Words.lemma_quad32_ones",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.Math.Poly2.Bits.poly128_of_nat32s",
        "equation_Vale.Math.Poly2.Bits.poly128_of_poly32s",
        "function_token_typing_Vale.Math.Poly2.Bits.of_nat32_ones",
        "int_inversion", "int_typing",
        "lemma_Vale.Math.Poly2.Lemmas.lemma_ones_degree",
        "primitive_Prims.op_AmpAmp", "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_10fce5557d0593095ff373cff619471e",
        "refinement_interpretation_Tm_refine_37b3edec16faddba730e4e710f565937",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "typing_Vale.Math.Poly2.Bits.of_nat32",
        "typing_Vale.Math.Poly2.ones", "typing_Vale.Math.Poly2_s.add",
        "typing_Vale.Math.Poly2_s.poly_index",
        "typing_Vale.Math.Poly2_s.shift"
      ],
      0,
      "32b78e60caae435db38287b542d8c2f0"
    ],
    [
      "Vale.Math.Poly2.Words.lemma_add128",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
        "equation_Vale.Def.Types_s.quad32_xor_def",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.Math.Poly2.Bits.poly128_of_nat32s",
        "equation_Vale.Math.Poly2.Bits.poly128_of_poly32s",
        "function_token_typing_Vale.Def.Types_s.quad32_xor", "int_inversion",
        "int_typing", "lemma_Vale.Math.Poly2.lemma_add_degree",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_disEquality",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
        "refinement_interpretation_Tm_refine_37b3edec16faddba730e4e710f565937",
        "token_correspondence_Vale.Def.Types_s.quad32_xor_def",
        "typing_Vale.Math.Poly2.Bits.of_nat32",
        "typing_Vale.Math.Poly2.Bits.poly128_of_poly32s",
        "typing_Vale.Math.Poly2_s.add",
        "typing_Vale.Math.Poly2_s.poly_index",
        "typing_Vale.Math.Poly2_s.shift"
      ],
      0,
      "bb1e4531a7b7539aa4c69c4f45687482"
    ],
    [
      "Vale.Math.Poly2.Words.lemma_add_quad32",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "lemma_Vale.Math.Poly2.Bits.lemma_of_quad32_degree",
        "lemma_Vale.Math.Poly2.Bits.lemma_to_of_quad32",
        "lemma_Vale.Math.Poly2.lemma_add_degree",
        "typing_Vale.Math.Poly2.Bits_s.of_quad32"
      ],
      0,
      "a35d5ff8787ea409d441fd97255a8661"
    ],
    [
      "Vale.Math.Poly2.Words.lemma_and128",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.Math.Poly2.Bits.poly128_of_nat32s",
        "equation_Vale.Math.Poly2.Bits.poly128_of_poly32s", "int_inversion",
        "int_typing", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_disEquality",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
        "refinement_interpretation_Tm_refine_37b3edec16faddba730e4e710f565937",
        "typing_Vale.Math.Poly2.Bits.of_nat32",
        "typing_Vale.Math.Poly2.Bits.poly128_of_poly32s",
        "typing_Vale.Math.Poly2.poly_and", "typing_Vale.Math.Poly2_s.add",
        "typing_Vale.Math.Poly2_s.poly_index",
        "typing_Vale.Math.Poly2_s.shift"
      ],
      0,
      "6a7328e8a472257d2442f28ad483bdb1"
    ],
    [
      "Vale.Math.Poly2.Words.lemma_and_quad32",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "lemma_Vale.Math.Poly2.Bits.lemma_of_quad32_degree",
        "lemma_Vale.Math.Poly2.Bits.lemma_to_of_quad32",
        "lemma_Vale.Math.Poly2.Lemmas.lemma_and_degree",
        "typing_Vale.Math.Poly2.Bits_s.of_quad32"
      ],
      0,
      "06272af92bd6086de9900e3bbb61c591"
    ],
    [
      "Vale.Math.Poly2.Words.lemma_quad32_double_shift",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
        "bool_typing", "equation_Prims.nat",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.Math.Poly2.Bits.poly128_of_nat32s",
        "equation_Vale.Math.Poly2.Bits.poly128_of_poly32s",
        "function_token_typing_Vale.Math.Poly2.Bits.of_nat32_zero",
        "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",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
        "refinement_interpretation_Tm_refine_37b3edec16faddba730e4e710f565937",
        "refinement_interpretation_Tm_refine_4337ec945cb4c294d0e8ff2d420e64d7",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "typing_Vale.Math.Poly2.Bits.of_nat32",
        "typing_Vale.Math.Poly2.Bits.poly128_of_nat32s",
        "typing_Vale.Math.Poly2.mask", "typing_Vale.Math.Poly2_s.add",
        "typing_Vale.Math.Poly2_s.poly_index",
        "typing_Vale.Math.Poly2_s.shift", "typing_Vale.Math.Poly2_s.zero"
      ],
      0,
      "56a6273ee60d0fa1726347f0848790cd"
    ],
    [
      "Vale.Math.Poly2.Words.lemma_quad32_double_swap",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion",
        "bool_typing", "equation_Prims.nat",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.Math.Poly2.Bits.poly128_of_nat32s",
        "equation_Vale.Math.Poly2.Bits.poly128_of_poly32s",
        "equation_Vale.Math.Poly2.swap", "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",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
        "refinement_interpretation_Tm_refine_37b3edec16faddba730e4e710f565937",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Vale.Math.Poly2.Bits.of_nat32",
        "typing_Vale.Math.Poly2.Bits.poly128_of_nat32s",
        "typing_Vale.Math.Poly2.mask", "typing_Vale.Math.Poly2.swap",
        "typing_Vale.Math.Poly2_s.add",
        "typing_Vale.Math.Poly2_s.poly_index",
        "typing_Vale.Math.Poly2_s.shift"
      ],
      0,
      "73b3bb416b25c4aac513487710145a74"
    ]
  ]
]