[
  "L@ÂŒ¡+²‰QÕ´‰v\u0006VÃ",
  [
    [
      "Vale.Def.Words.Two.lemma_fundamental_div_mod",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "int_inversion", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "6e854be9751a1e3a5f57e2594a450a70"
    ],
    [
      "Vale.Def.Words.Two.nat_to_two_to_nat",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "b47b922cbd9249a68b36ea2816b41a10"
    ],
    [
      "Vale.Def.Words.Two.nat_to_two_to_nat",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Vale.Def.Words.Two_s.nat_to_two",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
        "int_typing", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_30c926ebf383bedbae82319bb48dcf51",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_Vale.Def.Words_s.int_to_natN"
      ],
      0,
      "058f2116b0967924b17be747613fd32a"
    ],
    [
      "Vale.Def.Words.Two.two_to_nat_to_two",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "5aab891865694c02d9bf92e300f8488e"
    ],
    [
      "Vale.Def.Words.Two.two_to_nat_to_two",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Vale.Def.Words.Two_s.nat_to_two",
        "equation_Vale.Def.Words.Two_s.two_to_nat",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
        "int_typing", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Vale.Def.Words_s.Mktwo_hi",
        "projection_inverse_Vale.Def.Words_s.Mktwo_lo",
        "refinement_interpretation_Tm_refine_30c926ebf383bedbae82319bb48dcf51",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_Vale.Def.Words_s.int_to_natN"
      ],
      0,
      "382669fd72381b67fe309d90c9d8fcef"
    ],
    [
      "Vale.Def.Words.Two.two_to_nat_32_injective",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "ac164e32e5c0f59a7de8a85afae0f73e"
    ],
    [
      "Vale.Def.Words.Two.two_to_nat_32_injective",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "assumption_Vale.Def.Words_s.two__uu___haseq",
        "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "fuel_guarded_inversion_Vale.Def.Words_s.two",
        "function_token_typing_Prims.int",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "int_inversion",
        "int_typing", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_Vale.Def.Words_s.Mktwo_hi",
        "proj_equation_Vale.Def.Words_s.Mktwo_lo",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "token_correspondence_Prims.pow2.fuel_instrumented"
      ],
      0,
      "d6d9d2850f5ffb6bca2557ce14012225"
    ]
  ]
]