[
  "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,
      "5dcefb556eb38116a6895886e9a5988c"
    ],
    [
      "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,
      "35fbc7d04f108b4b7c85f0aa3ed1d8c4"
    ],
    [
      "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,
      "c7b7b0db527f56ddb4ec5c04cdd68ef5"
    ],
    [
      "Vale.Def.Words.Two.two_to_nat_to_two",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "eebd44f30f377ab566fbfa51f92e61f3"
    ],
    [
      "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,
      "4610f46669fbce8b08c0aab5d35f0a59"
    ],
    [
      "Vale.Def.Words.Two.two_to_nat_32_injective",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "a423ed960e3a6ef94b78f33b37483236"
    ],
    [
      "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,
      "48800015e8cf1cd0e2f9cfb18e81c2e4"
    ]
  ]
]