[
  "f<\t\\ª$\u0018ît\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,
      "30a9cabff81a01e18c29b27f0ab1824b"
    ],
    [
      "Lib.RawIntTypes.u8_from_UInt8",
      2,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.sec_int_v",
        "equation_Lib.IntTypes.v"
      ],
      0,
      "3c4432afef0fbfb8f44164f590bc67f2"
    ],
    [
      "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,
      "f657fd373f6c52d9c3af56e7a764f38b"
    ],
    [
      "Lib.RawIntTypes.u16_from_UInt16",
      2,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U16",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U16@tok",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.sec_int_v",
        "equation_Lib.IntTypes.v"
      ],
      0,
      "42dba69b2001193c8a8bad5581a990b3"
    ],
    [
      "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,
      "1eb096c98d2fd4dcc01cf4d57fe50383"
    ],
    [
      "Lib.RawIntTypes.u32_from_UInt32",
      2,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.sec_int_v",
        "equation_Lib.IntTypes.v"
      ],
      0,
      "0761ea95c5d0a9f9ed0b2f0c3ac02e6f"
    ],
    [
      "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,
      "0a21cb00f592e971c97c5e0c1d644752"
    ],
    [
      "Lib.RawIntTypes.u64_from_UInt64",
      2,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.sec_int_v",
        "equation_Lib.IntTypes.v"
      ],
      0,
      "2bbc30db3b5ad951a9dea43c64186de0"
    ],
    [
      "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,
      "628c56e9d216d0eb297f67aac7e458b6"
    ],
    [
      "Lib.RawIntTypes.u128_from_UInt128",
      2,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U128",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.sec_int_v",
        "equation_Lib.IntTypes.v"
      ],
      0,
      "8740e396732c547b0647119b618fe8df"
    ],
    [
      "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,
      "35db8956852190542ff86354861dff57"
    ],
    [
      "Lib.RawIntTypes.size_from_UInt32",
      2,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.v"
      ],
      0,
      "a93d6fe958585b02ff01404409017a4e"
    ],
    [
      "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,
      "4eb59557e02910fe6cc68a727da1e51d"
    ],
    [
      "Lib.RawIntTypes.u8_to_UInt8",
      2,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.sec_int_v",
        "equation_Lib.IntTypes.v"
      ],
      0,
      "c4eb7675f602db5c40818443f6ac755d"
    ],
    [
      "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,
      "1dd121afa739a025d2163d38ad3d142c"
    ],
    [
      "Lib.RawIntTypes.u16_to_UInt16",
      2,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U16",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U16@tok",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.sec_int_v",
        "equation_Lib.IntTypes.v"
      ],
      0,
      "70e0181b52dcc7590d670bf2b694fb9a"
    ],
    [
      "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,
      "e5b96414bcbf35139fea8227163ed070"
    ],
    [
      "Lib.RawIntTypes.u32_to_UInt32",
      2,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.sec_int_v",
        "equation_Lib.IntTypes.v"
      ],
      0,
      "1497e7c114ef5f824ca36fba48a12da1"
    ],
    [
      "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,
      "ed0eb2e9a7972823c33824402093cda6"
    ],
    [
      "Lib.RawIntTypes.u64_to_UInt64",
      2,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.sec_int_v",
        "equation_Lib.IntTypes.v"
      ],
      0,
      "c2bd785ffd32779f939d8f75a49aef73"
    ],
    [
      "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,
      "d9fff1520f174bf5f8d864b847078221"
    ],
    [
      "Lib.RawIntTypes.u128_to_UInt128",
      2,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U128",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.sec_int_v",
        "equation_Lib.IntTypes.v"
      ],
      0,
      "43f9a3d97a1e88d6ac0a8d3f5efaaecf"
    ],
    [
      "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,
      "794dbec1a42d758a8b3097c57454924e"
    ],
    [
      "Lib.RawIntTypes.size_to_UInt32",
      2,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.v"
      ],
      0,
      "c7571c1e0afe4bcdcd4ecc5bf091918a"
    ],
    [
      "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,
      "0edf0743317bdd073c0fd939df351f8c"
    ],
    [
      "Lib.RawIntTypes.uint_to_nat",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.unsigned",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "typing_Lib.IntTypes.unsigned"
      ],
      0,
      "36ba649512c654c20271eaf8d7a118c0"
    ]
  ]
]