[
  "V��yK���v~I\u0000=9�(",
  [
    [
      "Lib.IntTypes.bits",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "disc_equation_Lib.IntTypes.U1",
        "disc_equation_Lib.IntTypes.U128", "disc_equation_Lib.IntTypes.U16",
        "disc_equation_Lib.IntTypes.U32", "disc_equation_Lib.IntTypes.U64",
        "disc_equation_Lib.IntTypes.U8",
        "fuel_guarded_inversion_Lib.IntTypes.inttype"
      ],
      0,
      "bfe698fc8461ecae72f6610fb1883d8e"
    ],
    [
      "Lib.IntTypes.numbytes",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "disc_equation_Lib.IntTypes.U1",
        "disc_equation_Lib.IntTypes.U128", "disc_equation_Lib.IntTypes.U16",
        "disc_equation_Lib.IntTypes.U32", "disc_equation_Lib.IntTypes.U64",
        "disc_equation_Lib.IntTypes.U8",
        "fuel_guarded_inversion_Lib.IntTypes.inttype"
      ],
      0,
      "151fc2020d32c75d8c703bcb98d32a33"
    ],
    [
      "Lib.IntTypes.modulus",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Lib.IntTypes.bits",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "22e0e4eee307a83e7c5e21c29a25f09e"
    ],
    [
      "Lib.IntTypes.pub_int_t",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "disc_equation_Lib.IntTypes.U1",
        "disc_equation_Lib.IntTypes.U128", "disc_equation_Lib.IntTypes.U16",
        "disc_equation_Lib.IntTypes.U32", "disc_equation_Lib.IntTypes.U64",
        "disc_equation_Lib.IntTypes.U8",
        "fuel_guarded_inversion_Lib.IntTypes.inttype"
      ],
      0,
      "1493d7a5c7d8233a3ce4bcc4cc79b024"
    ],
    [
      "Lib.IntTypes.pub_int_v",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "disc_equation_Lib.IntTypes.U1", "disc_equation_Lib.IntTypes.U128",
        "disc_equation_Lib.IntTypes.U16", "disc_equation_Lib.IntTypes.U32",
        "disc_equation_Lib.IntTypes.U64", "disc_equation_Lib.IntTypes.U8",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt128.n", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.pub_int_t", "equation_Prims.nat",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2abe54c0722e4776377a18255264b233",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "c9d1a3546afd2a17fcb4179ccb0b3e6c"
    ],
    [
      "Lib.IntTypes.uint_t",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "disc_equation_Lib.IntTypes.PUB",
        "disc_equation_Lib.IntTypes.SEC",
        "fuel_guarded_inversion_Lib.IntTypes.secrecy_level"
      ],
      0,
      "b369fcc45759bb2ae19f05837e8540b6"
    ],
    [
      "Lib.IntTypes.uint_v",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "disc_equation_Lib.IntTypes.PUB",
        "disc_equation_Lib.IntTypes.SEC", "equation_Lib.IntTypes.uint_t",
        "fuel_guarded_inversion_Lib.IntTypes.secrecy_level",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "83a586a6b71cca96c5de3492c150d05e"
    ],
    [
      "Lib.IntTypes.uintv_extensionality",
      1,
      2,
      1,
      [ "@query" ],
      0,
      "fb53879aa411b474da183bd4f4828663"
    ],
    [
      "Lib.IntTypes.secret",
      1,
      2,
      1,
      [ "@query" ],
      0,
      "5842b00e2118227aaed7a9da6417a8cb"
    ],
    [
      "Lib.IntTypes.uint",
      1,
      2,
      1,
      [ "@query" ],
      0,
      "76d97a579529e7e5210d282fd38388f4"
    ],
    [
      "Lib.IntTypes.u1",
      1,
      2,
      1,
      [ "@query" ],
      0,
      "93bc401bcad6cea055ed131ac902c8ef"
    ],
    [
      "Lib.IntTypes.u8",
      1,
      2,
      1,
      [ "@query" ],
      0,
      "f763ca2dba10e5289b086887759a81d7"
    ],
    [
      "Lib.IntTypes.u16",
      1,
      2,
      1,
      [ "@query" ],
      0,
      "68b4405a81989eba28c239270af4e7ee"
    ],
    [
      "Lib.IntTypes.u32",
      1,
      2,
      1,
      [ "@query" ],
      0,
      "e527ff4860608c8814d11905e92b3bef"
    ],
    [
      "Lib.IntTypes.u64",
      1,
      2,
      1,
      [ "@query" ],
      0,
      "1bc22faed8774cceb3060c6ca14d81b6"
    ],
    [
      "Lib.IntTypes.u128",
      1,
      2,
      1,
      [ "@query" ],
      0,
      "19121469868e28c2c6aedcaf17f91594"
    ],
    [
      "Lib.IntTypes.size_v_size_lemma",
      1,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "3e59140c56a60290d3c271a11b8b7cad"
    ],
    [
      "Lib.IntTypes.uint_v_size_lemma",
      1,
      2,
      1,
      [ "@query" ],
      0,
      "764d457314246f2fc6d3f6909aea1253"
    ],
    [
      "Lib.IntTypes.byte",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "7a87e559543dc355c9aa8811b2ae799c"
    ],
    [
      "Lib.IntTypes.byte_v",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.uint_v", "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "f7dbd1aa41727869a67893aee4a9758f"
    ],
    [
      "Lib.IntTypes.byte_to_uint8",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Prims.nat",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "typing_Lib.IntTypes.uint_v", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "1fd2498c833c033e9bfb6ad28d727697"
    ],
    [
      "Lib.IntTypes.nat_to_uint",
      1,
      2,
      1,
      [ "@query" ],
      0,
      "19e1ba65172ffa546cc9666adce7a0b9"
    ],
    [
      "Lib.IntTypes.cast",
      1,
      2,
      1,
      [ "@query" ],
      0,
      "541a1ace5db124550832d0ad9d27cd99"
    ],
    [
      "Lib.IntTypes.to_u8",
      1,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.SEC",
        "disc_equation_Lib.IntTypes.SEC",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "cb6fdfa95295c80a3651b97ef3d5d9d1"
    ],
    [
      "Lib.IntTypes.to_u16",
      1,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.SEC",
        "disc_equation_Lib.IntTypes.SEC",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "552f636394fd045ca37daaa32395c038"
    ],
    [
      "Lib.IntTypes.to_u32",
      1,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.SEC",
        "disc_equation_Lib.IntTypes.SEC",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "aedc19a4e89545ec33745515e31b2e77"
    ],
    [
      "Lib.IntTypes.to_u64",
      1,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.SEC",
        "disc_equation_Lib.IntTypes.SEC",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "212e26e305947088d70888c1f1b33906"
    ],
    [
      "Lib.IntTypes.to_u128",
      1,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.SEC",
        "disc_equation_Lib.IntTypes.SEC",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "b8d226fcd7675156f5d8f9e53452ee4b"
    ],
    [
      "Lib.IntTypes.add_mod_lemma",
      1,
      2,
      1,
      [ "@query" ],
      0,
      "357d46d0a93fef6c89c2ad9b1b5fbd08"
    ],
    [
      "Lib.IntTypes.mul_mod",
      1,
      2,
      1,
      [ "@query", "assumption_Lib.IntTypes.inttype__uu___haseq" ],
      0,
      "9c649cbeceb15d2759fa4306ce88147c"
    ],
    [
      "Lib.IntTypes.mul_mod_lemma",
      1,
      2,
      1,
      [ "@query", "assumption_Lib.IntTypes.inttype__uu___haseq" ],
      0,
      "91fad22e604df129b3bd6f23f6fe5dad"
    ],
    [
      "Lib.IntTypes.mul",
      1,
      2,
      1,
      [ "@query", "assumption_Lib.IntTypes.inttype__uu___haseq" ],
      0,
      "279d8a04148584b5599cb2b9cdc3bf27"
    ],
    [
      "Lib.IntTypes.mul_lemma",
      1,
      2,
      1,
      [ "@query", "assumption_Lib.IntTypes.inttype__uu___haseq" ],
      0,
      "216c695646574dfd6f69ed01152e2719"
    ],
    [
      "Lib.IntTypes.sub_mod_lemma",
      1,
      2,
      1,
      [ "@query" ],
      0,
      "7e57c41551e6909b82042d74d497db97"
    ],
    [
      "Lib.IntTypes.logand_spec",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "disc_equation_Lib.IntTypes.U1", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.uint_v",
        "equation_Prims.pos", "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_70769f76f84273b3587aeaec18364fbc",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b"
      ],
      0,
      "823a036b196af258447e30ada5d66fff"
    ],
    [
      "Lib.IntTypes.shift_right_lemma",
      1,
      2,
      1,
      [ "@query" ],
      0,
      "fec9ce6f6873abeca6c878948de8e81c"
    ],
    [
      "Lib.IntTypes.shift_left_lemma",
      1,
      2,
      1,
      [ "@query" ],
      0,
      "95dff4c3bc9ac46b34d7b2e7fac5fcb8"
    ],
    [
      "Lib.IntTypes.eq_mask_lemma",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Lib.IntTypes.bits", "equation_Prims.eqtype",
        "equation_Prims.nat", "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "9bf55903ee612ed1e768d5f4776c47ae"
    ],
    [
      "Lib.IntTypes.mod_mask",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Prims.nat", "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "function_token_typing_Prims.__cache_version_number__",
        "lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "5b332c13dcff8b171681c6849d95db97"
    ],
    [
      "Lib.IntTypes.mod_mask_lemma",
      1,
      2,
      1,
      [ "@query" ],
      0,
      "61e16bc2f240c2be8a73bdddb4ea19dd"
    ],
    [
      "Lib.IntTypes.op_Star_Bang",
      1,
      2,
      1,
      [ "@query", "assumption_Lib.IntTypes.inttype__uu___haseq" ],
      0,
      "60862871bcc3c8c9605a0ab06523e0d5"
    ],
    [
      "Lib.IntTypes.op_Star_Dot",
      1,
      2,
      1,
      [ "@query", "assumption_Lib.IntTypes.inttype__uu___haseq" ],
      0,
      "dd85653fd27e9f528ba0e96999c83202"
    ],
    [
      "Lib.IntTypes.div",
      1,
      2,
      1,
      [ "@query", "assumption_Lib.IntTypes.inttype__uu___haseq" ],
      0,
      "607d5fde996fa40ee7877423ae1e5695"
    ],
    [
      "Lib.IntTypes.div_lemma",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "assumption_Lib.IntTypes.inttype__uu___haseq",
        "refinement_interpretation_Tm_refine_4a34935eeba50b27dccb698391a74562"
      ],
      0,
      "4a64b0c943d892b20898233ce73fa28b"
    ],
    [
      "Lib.IntTypes.mod",
      1,
      2,
      1,
      [ "@query", "assumption_Lib.IntTypes.inttype__uu___haseq" ],
      0,
      "2f7947e998d495e8d38d378147aece65"
    ],
    [
      "Lib.IntTypes.mod_lemma",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "assumption_Lib.IntTypes.inttype__uu___haseq",
        "refinement_interpretation_Tm_refine_4a34935eeba50b27dccb698391a74562"
      ],
      0,
      "5f3afabf887698c281b922937d3ca4e0"
    ],
    [
      "Lib.IntTypes.eq_lemma",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "f4a81df52ae5930764b5e7b9f0f26e99"
    ],
    [
      "Lib.IntTypes.ne_lemma",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "def9771d350cdaad6e71883b060aa9df"
    ],
    [
      "Lib.IntTypes.op_Slash_Dot",
      1,
      2,
      1,
      [ "@query", "assumption_Lib.IntTypes.inttype__uu___haseq" ],
      0,
      "e21a2cfdac9ab6b5e64bc718765439a8"
    ],
    [
      "Lib.IntTypes.op_Percent_Dot",
      1,
      2,
      1,
      [ "@query", "assumption_Lib.IntTypes.inttype__uu___haseq" ],
      0,
      "c20ad8a5e0e9cc6630de7313cec02e45"
    ]
  ]
]