[
  "¢\u000bO‹¢¸'‚+Ü÷jà~‹",
  [
    [
      "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,
      "0a86738798328f850130cd5b60b565cf"
    ],
    [
      "Vale.Def.Words.Two.two_to_nat_to_two",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "0fe32356506748fdd1b2c7783af20564"
    ],
    [
      "Vale.Def.Words.Two.two_to_nat_32_injective",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "a509a19770f5dbf4bb5244b5d2b32620"
    ]
  ]
]