[
  "��/��ύB�;���^r�",
  [
    [
      "Lib.RawIntTypes.u8_from_UInt8",
      1,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "d01fa289a1a0ce2cb4302e44e759aac4"
    ],
    [
      "Lib.RawIntTypes.u16_from_UInt16",
      1,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U16",
        "equality_tok_Lib.IntTypes.U16@tok",
        "equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "81922efdacf49dbbf55235fe4ae84f3d"
    ],
    [
      "Lib.RawIntTypes.u32_from_UInt32",
      1,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "938f8f4a58727d976ca01209ed9c77d0"
    ],
    [
      "Lib.RawIntTypes.u64_from_UInt64",
      1,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "88fab032922cf7a908afab82dbe0ebfe"
    ],
    [
      "Lib.RawIntTypes.u128_from_UInt128",
      1,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U128",
        "equality_tok_Lib.IntTypes.U128@tok", "equation_FStar.UInt128.n",
        "equation_Lib.IntTypes.unsigned",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "3df6b1827f13f7b715c5c85f8817af72"
    ],
    [
      "Lib.RawIntTypes.size_from_UInt32",
      1,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "eeeeb9ba1b67e2fcf7be4d32dff9ee17"
    ],
    [
      "Lib.RawIntTypes.u8_to_UInt8",
      1,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "d25e4c07dee715fd71cb5a97947f96b5"
    ],
    [
      "Lib.RawIntTypes.u16_to_UInt16",
      1,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U16",
        "equality_tok_Lib.IntTypes.U16@tok",
        "equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "ad84bc8528551817f634e00844ee711f"
    ],
    [
      "Lib.RawIntTypes.u32_to_UInt32",
      1,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "b0db12f6282e62046de7622687dd3462"
    ],
    [
      "Lib.RawIntTypes.u64_to_UInt64",
      1,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "191643691ead607f2a968cac450f68b3"
    ],
    [
      "Lib.RawIntTypes.u128_to_UInt128",
      1,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U128",
        "equality_tok_Lib.IntTypes.U128@tok", "equation_FStar.UInt128.n",
        "equation_Lib.IntTypes.unsigned",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "d24d174b742d33953309a209c82f186c"
    ],
    [
      "Lib.RawIntTypes.size_to_UInt32",
      1,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "37dfb4bf3c04b7b5e19296576cac740e"
    ],
    [
      "Lib.RawIntTypes.uint_to_nat",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "fdb104b1c7a248e5ef0ffa8257ff0ad8"
    ]
  ]
]