[
  "†#E³\u001e(§$Ÿœ'©žñe1",
  [
    [
      "Vale.Def.Words.Four_s.nat_to_four_unfold",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "75a9585d10edd352cc6e0747ac8620d2"
    ],
    [
      "Vale.Def.Words.Four_s.nat_to_four_unfold",
      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_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_Prims.pow2"
      ],
      0,
      "5d3ef209690ab9f42bf0cfa564942060"
    ],
    [
      "Vale.Def.Words.Four_s.nat_to_four",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "64ae086a9f6c1c68cf61be5b8eb10ef1"
    ],
    [
      "Vale.Def.Words.Four_s.nat_to_four",
      2,
      1,
      0,
      [ "@query" ],
      0,
      "484e6b7cf2f245d8652f55e9706a5efd"
    ],
    [
      "Vale.Def.Words.Four_s.four_to_nat_unfold",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "0f81d20e1b1d53d255ff23eaae81b954"
    ],
    [
      "Vale.Def.Words.Four_s.four_to_nat_unfold",
      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_with_fuel_Prims.pow2.fuel_instrumented",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_Prims.pow2"
      ],
      0,
      "dc6ca1fcfada7a75b83377ca5b1491de"
    ],
    [
      "Vale.Def.Words.Four_s.four_to_nat",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "659145ec6534585ad7d7bc48a60e65f0"
    ],
    [
      "Vale.Def.Words.Four_s.four_to_nat",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "84aeb8f675600549d4e8054620c17a3b"
    ],
    [
      "Vale.Def.Words.Four_s.four_select",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.Def.Words_s.nat2", "equation_Vale.Def.Words_s.natN",
        "int_inversion", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "fb80a6eab84e9950354f1d6fca78048b"
    ],
    [
      "Vale.Def.Words.Four_s.four_insert",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.Def.Words_s.nat2", "equation_Vale.Def.Words_s.natN",
        "int_inversion", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "13fee429798c1fd750a5c45b46e4b4de"
    ]
  ]
]