Revision - aa1ca86 - Get to work on proving write-behavior for instructions

Revision aa1ca8698adfe929a9eff86ac143eaf90fc3e8ee authored by Jay Bosamiya on 03 June 2019, 21:51:38 UTC, committed by Jay Bosamiya on 03 June 2019, 21:51:38 UTC

Get to work on proving write-behavior for instructions

1 parent 6055e85

Files
Changes

Permalinks

Lib.ByteSequence.fst.hints

[
  "-��\u001a����*j�s��\u0006\u0012",
  [
    [
      "Lib.ByteSequence.lemma_not_equal_slice",
      1,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_7a77162142d68430332762c2d4753fc3",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Seq.Base.length"
      ],
      0,
      "248235d21b4714f497e021f100b783d3"
    ],
    [
      "Lib.ByteSequence.lemma_not_equal_slice",
      2,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_559c261b1c3777929ea329abfe70ab33",
        "refinement_interpretation_Tm_refine_7a77162142d68430332762c2d4753fc3",
        "refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice"
      ],
      0,
      "04eb0ca6ef69b3eb9c523c603bd34f1d"
    ],
    [
      "Lib.ByteSequence.lemma_not_equal_last",
      1,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_6141a09a517d0a516f151f12b71fedc1",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Seq.Base.length"
      ],
      0,
      "83e41ef19a82e0e8f86b28b8af431786"
    ],
    [
      "Lib.ByteSequence.lemma_not_equal_last",
      2,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "lemma_FStar.Seq.Base.lemma_eq_elim",
        "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_6141a09a517d0a516f151f12b71fedc1",
        "refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice"
      ],
      0,
      "3485c95dbad180c338e4a47864b2d8c3"
    ],
    [
      "Lib.ByteSequence.seq_eq_mask_inner",
      1,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.SEC@tok",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq",
        "equation_Prims.nat", "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "primitive_Prims.op_Addition",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_35b0365cab1c2712cc3147959a4baa36",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_5a4fe33be2b93c781e552e491bb9dd31",
        "refinement_interpretation_Tm_refine_623a96737f32a2450bcfa75183bab27d",
        "refinement_interpretation_Tm_refine_70769f76f84273b3587aeaec18364fbc",
        "refinement_interpretation_Tm_refine_78ea63ceb027a3f1c790955bc68a707b",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42"
      ],
      0,
      "3f538f7d1521c2bc200535821e9cb311"
    ],
    [
      "Lib.ByteSequence.seq_eq_mask_inner",
      2,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.SEC@tok",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq",
        "equation_Prims.nat", "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "primitive_Prims.op_Addition",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_35b0365cab1c2712cc3147959a4baa36",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_5a4fe33be2b93c781e552e491bb9dd31",
        "refinement_interpretation_Tm_refine_70769f76f84273b3587aeaec18364fbc",
        "refinement_interpretation_Tm_refine_78ea63ceb027a3f1c790955bc68a707b",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42"
      ],
      0,
      "a5ec829ea111f2c0c90f0dfb0e16f4f2"
    ],
    [
      "Lib.ByteSequence.seq_eq_mask_inner",
      3,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "constructor_distinct_Lib.IntTypes.U32",
        "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U16@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_FStar.Pervasives.Native.fst",
        "equation_FStar.Seq.Properties.split", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.ones", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_FStar.UInt.zero",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.op_Amp_Dot", "equation_Lib.IntTypes.uint128",
        "equation_Lib.IntTypes.uint16", "equation_Lib.IntTypes.uint32",
        "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.uint8",
        "equation_Lib.IntTypes.uint_t", "equation_Lib.IntTypes.uint_v",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_Lib.Sequence.to_seq", "equation_Prims.nat",
        "equation_Prims.pos", "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "function_token_typing_Lib.IntTypes.logand",
        "function_token_typing_Lib.IntTypes.uint128",
        "function_token_typing_Lib.IntTypes.uint16",
        "function_token_typing_Lib.IntTypes.uint32",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Lib.IntTypes.uint8",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_refl",
        "lemma_FStar.Seq.Base.lemma_index_app1",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.slice_slice",
        "lemma_Lib.IntTypes.eq_mask_lemma", "lemma_Lib.IntTypes.pow2_values",
        "lemma_Lib.Sequence.eq_elim", "lemma_Lib.Sequence.eq_intro",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "refinement_interpretation_Tm_refine_0a44a9c52461f7b29dab1fe1db7afc62",
        "refinement_interpretation_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
        "refinement_interpretation_Tm_refine_3421154546287b0f0c012dd3d63b4945",
        "refinement_interpretation_Tm_refine_35b0365cab1c2712cc3147959a4baa36",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_528d1ac7a4a801fe55aa0f436f85ad2a",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_5a4fe33be2b93c781e552e491bb9dd31",
        "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
        "refinement_interpretation_Tm_refine_623a96737f32a2450bcfa75183bab27d",
        "refinement_interpretation_Tm_refine_70769f76f84273b3587aeaec18364fbc",
        "refinement_interpretation_Tm_refine_78ea63ceb027a3f1c790955bc68a707b",
        "refinement_interpretation_Tm_refine_7d1f8052011b211126fe99890342ffdc",
        "refinement_interpretation_Tm_refine_7e18257c091b38e24e95eb8a0a0ec392",
        "refinement_interpretation_Tm_refine_8bdecfb5d16fa4a517d5fa57acd2da6d",
        "refinement_interpretation_Tm_refine_8dc2d2595aa405e8584c1773e70ba062",
        "refinement_interpretation_Tm_refine_99947ebb12a211d213d5bd2652c45b18",
        "refinement_interpretation_Tm_refine_9fa3c3f1b32e27669a46bed06f432c2f",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_deba80666445d53a7a351a543c3f7d37",
        "refinement_interpretation_Tm_refine_e52764b706a020e88426043704c96605",
        "refinement_interpretation_Tm_refine_ed552f6a1583c5b76f2db8a1d833e2f6",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "token_correspondence_Lib.IntTypes.op_Amp_Dot",
        "typing_FStar.Pervasives.Native.fst",
        "typing_FStar.Pervasives.Native.snd", "typing_FStar.Seq.Base.slice",
        "typing_FStar.Seq.Properties.split", "typing_FStar.UInt.fits",
        "typing_FStar.UInt.zero", "typing_Lib.IntTypes.bits",
        "typing_Lib.IntTypes.ones", "typing_Lib.IntTypes.uint_t",
        "typing_Lib.IntTypes.uint_v", "typing_Lib.IntTypes.uu___is_U1",
        "typing_Lib.IntTypes.zeroes", "typing_Lib.Sequence.index",
        "typing_Lib.Sequence.seq", "typing_Lib.Sequence.sub",
        "typing_Lib.Sequence.to_seq", "typing_tok_Lib.IntTypes.SEC@tok",
        "typing_tok_Lib.IntTypes.U128@tok",
        "typing_tok_Lib.IntTypes.U16@tok", "typing_tok_Lib.IntTypes.U32@tok",
        "typing_tok_Lib.IntTypes.U64@tok", "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "4818cc4ae35331622209ab8d06212734"
    ],
    [
      "Lib.ByteSequence.seq_eq_mask",
      1,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.SEC@tok",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq",
        "equation_Prims.nat", "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "primitive_Prims.op_Addition",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_35b0365cab1c2712cc3147959a4baa36",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_5a4fe33be2b93c781e552e491bb9dd31",
        "refinement_interpretation_Tm_refine_70769f76f84273b3587aeaec18364fbc",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42"
      ],
      0,
      "f9f0ddd6a88b1544285f58b243ceea3e"
    ],
    [
      "Lib.ByteSequence.seq_eq_mask",
      2,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U16@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.uint_t", "equation_Lib.IntTypes.uint_v",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_Lib.Sequence.to_seq", "equation_Prims.nat",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_FStar.Seq.Properties.slice_is_empty",
        "lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_35b0365cab1c2712cc3147959a4baa36",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_5a4fe33be2b93c781e552e491bb9dd31",
        "refinement_interpretation_Tm_refine_70769f76f84273b3587aeaec18364fbc",
        "refinement_interpretation_Tm_refine_8ae4abcfc6bc8d4903b7e1f40e070ec2",
        "refinement_interpretation_Tm_refine_8bdecfb5d16fa4a517d5fa57acd2da6d",
        "refinement_interpretation_Tm_refine_9fa3c3f1b32e27669a46bed06f432c2f",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_cd046bc4a887ee7e1b05946e0bf5772b",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_e52764b706a020e88426043704c96605",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.uint_t",
        "typing_Lib.IntTypes.uint_v", "typing_Lib.IntTypes.zeroes",
        "typing_Lib.Sequence.sub", "typing_Lib.Sequence.to_seq",
        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "0849d3bc3350a09c14108de01a0974ee"
    ],
    [
      "Lib.ByteSequence.lbytes_eq",
      1,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_FStar.UInt8.t__uu___haseq", "b2t_def", "bool_inversion",
        "bool_typing", "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.pub_int_t",
        "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.uint_v",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_Lib.Sequence.to_seq", "equation_Prims.nat",
        "function_token_typing_Lib.IntTypes.uint8",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_FStar.Seq.Properties.slice_length",
        "lemma_FStar.UInt8.uv_inv", "lemma_FStar.UInt8.vu_inv",
        "lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Addition",
        "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_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_5a4fe33be2b93c781e552e491bb9dd31",
        "refinement_interpretation_Tm_refine_8bdecfb5d16fa4a517d5fa57acd2da6d",
        "refinement_interpretation_Tm_refine_9557b9096af86cfe4c64a1d451f92e04",
        "refinement_interpretation_Tm_refine_9fa3c3f1b32e27669a46bed06f432c2f",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_b332b73f2a8fe5127dc62c665726acda",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_e52764b706a020e88426043704c96605",
        "refinement_interpretation_Tm_refine_ed552f6a1583c5b76f2db8a1d833e2f6",
        "typing_FStar.UInt8.v", "typing_Lib.IntTypes.bits",
        "typing_Lib.IntTypes.ones", "typing_Lib.IntTypes.uint_v",
        "typing_Lib.IntTypes.zeroes", "typing_Lib.RawIntTypes.u8_to_UInt8",
        "typing_Lib.Sequence.sub", "typing_tok_Lib.IntTypes.SEC@tok",
        "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "8f82c7e438e52d87b61d8db02f2abbc1"
    ],
    [
      "Lib.ByteSequence.lbytes_empty",
      1,
      1,
      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",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Prims.nat", "equation_Prims.pos",
        "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",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "typing_Lib.IntTypes.bits", "typing_Prims.pow2",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "5ffda5d6b895f403edbf3a8e8ece5a3b"
    ],
    [
      "Lib.ByteSequence.nat_from_intseq_be_",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Lib.IntTypes.bits",
        "equation_Lib.Sequence.length", "equation_Prims.nat",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Lib.IntTypes.uint_t", "typing_Lib.Sequence.length"
      ],
      0,
      "7586300c79f0a3b6e28253626fe972bb"
    ],
    [
      "Lib.ByteSequence.nat_from_intseq_be_",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Tm_unit", "equation_Lib.IntTypes.bits",
        "equation_Lib.Sequence.length", "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_a3b86906105a7b8b3c44b899858783ec",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.uint_t",
        "typing_Lib.Sequence.length"
      ],
      0,
      "33e220105ab58581d4525311504e2d80"
    ],
    [
      "Lib.ByteSequence.nat_from_intseq_be_",
      3,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_40562ba8f0b1c89794fd620c41172c8e_2",
        "binder_x_877cb84f86c77989c5c1e5a978e57417_1",
        "binder_x_d450aafb6f125538d0e96425faddef55_0",
        "constructor_distinct_Lib.IntTypes.PUB",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Prims.LexTop@tok",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.seq",
        "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "fuel_guarded_inversion_Lib.IntTypes.secrecy_level",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d", "int_inversion",
        "int_typing", "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Equality", "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_17f65e44d4b04f4fe94be5ec9efa9a37",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_622031dbb8d8710932d1c8b2e74dc196",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d7cebba064d865556a0c4a88f11625ce",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "typing_Lib.IntTypes.uint_t", "typing_Lib.IntTypes.uint_v",
        "typing_Lib.Sequence.length", "typing_Prims.pow2",
        "well-founded-ordering-on-nat"
      ],
      0,
      "1d57c9c154ae592c4ed03b1b257f5ff2"
    ],
    [
      "Lib.ByteSequence.nat_from_intseq_be",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Lib.IntTypes.bits",
        "equation_Lib.Sequence.length", "equation_Prims.nat",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Lib.IntTypes.uint_t", "typing_Lib.Sequence.length"
      ],
      0,
      "8f61b78a7e981a67bce7711bd4d14e9b"
    ],
    [
      "Lib.ByteSequence.nat_from_intseq_le_",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Lib.IntTypes.bits",
        "equation_Lib.Sequence.length", "equation_Prims.nat",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Lib.IntTypes.uint_t", "typing_Lib.Sequence.length"
      ],
      0,
      "abd018d76147346ffbab3644945bffef"
    ],
    [
      "Lib.ByteSequence.nat_from_intseq_le_",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Tm_unit", "equation_Lib.IntTypes.bits",
        "equation_Lib.Sequence.length", "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_62924c696007f52b1969f12c1a61519e",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.uint_t",
        "typing_Lib.Sequence.length"
      ],
      0,
      "7eaf3c8ec31b5ca857f0c861c05116bc"
    ],
    [
      "Lib.ByteSequence.nat_from_intseq_le_",
      3,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_40562ba8f0b1c89794fd620c41172c8e_2",
        "binder_x_877cb84f86c77989c5c1e5a978e57417_1",
        "binder_x_d450aafb6f125538d0e96425faddef55_0",
        "constructor_distinct_Lib.IntTypes.PUB",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Prims.LexTop@tok",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.seq",
        "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "fuel_guarded_inversion_Lib.IntTypes.secrecy_level",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d", "int_inversion",
        "int_typing", "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Equality", "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_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_8c94cec4bf2462312c27acaee2f39852",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_a3c2f390303e04ad4c10f40eb8240a10",
        "refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_Lib.IntTypes.uint_t", "typing_Lib.IntTypes.uint_v",
        "typing_Lib.Sequence.length", "typing_Prims.pow2",
        "well-founded-ordering-on-nat"
      ],
      0,
      "a68a209a1279d6d4146db13ac9164e45"
    ],
    [
      "Lib.ByteSequence.nat_from_intseq_le",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Lib.IntTypes.bits",
        "equation_Lib.Sequence.length", "equation_Prims.nat",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Lib.IntTypes.uint_t", "typing_Lib.Sequence.length"
      ],
      0,
      "013943a02be93c8b52efded64de30f86"
    ],
    [
      "Lib.ByteSequence.nat_from_bytes_be",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.Sequence.length",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Lib.IntTypes.uint_t", "typing_Lib.Sequence.length",
        "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "d92f4f3fb12abb3b32cbee070d8ce704"
    ],
    [
      "Lib.ByteSequence.nat_from_bytes_be",
      2,
      1,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits"
      ],
      0,
      "fe6043766652cc92617cfa5cc39d89ea"
    ],
    [
      "Lib.ByteSequence.nat_from_bytes_le",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.Sequence.length",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Lib.IntTypes.uint_t", "typing_Lib.Sequence.length",
        "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "2930e9fab1fabb65f7caef54d8e22e99"
    ],
    [
      "Lib.ByteSequence.nat_from_bytes_le",
      2,
      1,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits"
      ],
      0,
      "746fa2df43ffb434a5b2a64923295174"
    ],
    [
      "Lib.ByteSequence.nat_to_intseq_be_",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Lib.IntTypes.bits", "equation_Prims.nat",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "4394edbf4b86510a0f2c9f25e4a29854"
    ],
    [
      "Lib.ByteSequence.nat_to_intseq_be_",
      2,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Lib.IntTypes.bits", "equation_Prims.nat",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "85f78f7797508d9ecb2f31e81657cae2"
    ],
    [
      "Lib.ByteSequence.nat_to_intseq_be_",
      3,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.ByteSequence.nat_from_intseq_be_.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Lib.ByteSequence.nat_from_intseq_be_.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_2bcf54892ad8db1fbab9f05248dff6d9_3",
        "binder_x_877cb84f86c77989c5c1e5a978e57417_1",
        "binder_x_d450aafb6f125538d0e96425faddef55_0",
        "binder_x_e22ba7a032a73f6d0678d3d186686631_2",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U16@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Prims.LexTop@tok",
        "equation_Lib.ByteSequence.nat_from_intseq_be",
        "equation_Lib.IntTypes.bit_t", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.pub_uint128",
        "equation_Lib.IntTypes.pub_uint16",
        "equation_Lib.IntTypes.pub_uint64", "equation_Lib.IntTypes.size_t",
        "equation_Lib.IntTypes.uint1", "equation_Lib.IntTypes.uint128",
        "equation_Lib.IntTypes.uint16", "equation_Lib.IntTypes.uint32",
        "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.uint8",
        "equation_Lib.IntTypes.uint_t", "equation_Lib.Sequence.length",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_Lib.Sequence.to_seq", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_Lib.ByteSequence.nat_from_intseq_be_.fuel_instrumented",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "fuel_guarded_inversion_Lib.IntTypes.secrecy_level",
        "function_token_typing_Lib.IntTypes.bit_t",
        "function_token_typing_Lib.IntTypes.byte_t",
        "function_token_typing_Lib.IntTypes.pub_uint128",
        "function_token_typing_Lib.IntTypes.pub_uint16",
        "function_token_typing_Lib.IntTypes.pub_uint64",
        "function_token_typing_Lib.IntTypes.size_t",
        "function_token_typing_Lib.IntTypes.uint1",
        "function_token_typing_Lib.IntTypes.uint128",
        "function_token_typing_Lib.IntTypes.uint16",
        "function_token_typing_Lib.IntTypes.uint32",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Lib.IntTypes.uint8",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "haseqTm_refine_f048236b5f8051f83b495ea5eaa6127b", "int_inversion",
        "int_typing", "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_index_app2",
        "lemma_FStar.Seq.Base.lemma_index_create",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_values",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Division",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_03127b5d59ee3055620018693b4264e8",
        "refinement_interpretation_Tm_refine_0b87673bf6d23c6ae167105003176063",
        "refinement_interpretation_Tm_refine_14d4d4e69e6cbef54be273c7ee86484d",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_44a966717a608f89ae8ee886b58a3a46",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_5d32194992439d2231ec88c0916e1207",
        "refinement_interpretation_Tm_refine_5f8d6bc4c84837626e91b895d0ad0916",
        "refinement_interpretation_Tm_refine_96e72dd0e7834e6d8b82a458e1181612",
        "refinement_interpretation_Tm_refine_ad1eaaaa670899ae125c748e0226afe2",
        "refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_Tm_refine_af27ee4a225c1904de8f856aec47d813",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.index",
        "typing_FStar.Seq.Base.slice", "typing_Lib.IntTypes.uint_t",
        "typing_Lib.RawIntTypes.uint_to_nat", "typing_Lib.Sequence.length",
        "well-founded-ordering-on-nat"
      ],
      0,
      "d655211936cd32f902ecf810c5864d15"
    ],
    [
      "Lib.ByteSequence.nat_to_intseq_be",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Lib.IntTypes.bits", "equation_Prims.nat",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "90feef134ce33e533bfd2b383c4451fb"
    ],
    [
      "Lib.ByteSequence.nat_to_intseq_be",
      2,
      1,
      1,
      [ "@query" ],
      0,
      "ff8ee92564380d7302544392a64a78d5"
    ],
    [
      "Lib.ByteSequence.nat_to_intseq_le_",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Lib.IntTypes.bits", "equation_Prims.nat",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "7cf0fdc10d6f2b2cfd0d5ef91ca67aa6"
    ],
    [
      "Lib.ByteSequence.nat_to_intseq_le_",
      2,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Lib.IntTypes.bits", "equation_Prims.nat",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "3226a8c44f7f6d0e1ee604ccf7d5d1c1"
    ],
    [
      "Lib.ByteSequence.nat_to_intseq_le_",
      3,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.ByteSequence.nat_from_intseq_le_.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Lib.ByteSequence.nat_from_intseq_le_.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_2bcf54892ad8db1fbab9f05248dff6d9_3",
        "binder_x_877cb84f86c77989c5c1e5a978e57417_1",
        "binder_x_d450aafb6f125538d0e96425faddef55_0",
        "binder_x_e22ba7a032a73f6d0678d3d186686631_2",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U16@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Prims.LexTop@tok",
        "equation_Lib.ByteSequence.nat_from_intseq_le",
        "equation_Lib.IntTypes.bit_t", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.pub_uint128",
        "equation_Lib.IntTypes.pub_uint16",
        "equation_Lib.IntTypes.pub_uint64", "equation_Lib.IntTypes.size_t",
        "equation_Lib.IntTypes.uint1", "equation_Lib.IntTypes.uint128",
        "equation_Lib.IntTypes.uint16", "equation_Lib.IntTypes.uint32",
        "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.uint8",
        "equation_Lib.IntTypes.uint_t", "equation_Lib.Sequence.length",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_Lib.Sequence.to_seq", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_Lib.ByteSequence.nat_from_intseq_le_.fuel_instrumented",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "fuel_guarded_inversion_Lib.IntTypes.secrecy_level",
        "function_token_typing_Lib.IntTypes.bit_t",
        "function_token_typing_Lib.IntTypes.byte_t",
        "function_token_typing_Lib.IntTypes.pub_uint128",
        "function_token_typing_Lib.IntTypes.pub_uint16",
        "function_token_typing_Lib.IntTypes.pub_uint64",
        "function_token_typing_Lib.IntTypes.size_t",
        "function_token_typing_Lib.IntTypes.uint1",
        "function_token_typing_Lib.IntTypes.uint128",
        "function_token_typing_Lib.IntTypes.uint16",
        "function_token_typing_Lib.IntTypes.uint32",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Lib.IntTypes.uint8",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "haseqTm_refine_f048236b5f8051f83b495ea5eaa6127b", "int_inversion",
        "int_typing", "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_index_app1",
        "lemma_FStar.Seq.Base.lemma_index_create",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_values",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Division",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0b87673bf6d23c6ae167105003176063",
        "refinement_interpretation_Tm_refine_14d4d4e69e6cbef54be273c7ee86484d",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_44a966717a608f89ae8ee886b58a3a46",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_5d32194992439d2231ec88c0916e1207",
        "refinement_interpretation_Tm_refine_81e3bb4cbcd0653079cc70a18dfd5bcf",
        "refinement_interpretation_Tm_refine_96e72dd0e7834e6d8b82a458e1181612",
        "refinement_interpretation_Tm_refine_ad1eaaaa670899ae125c748e0226afe2",
        "refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_Tm_refine_af27ee4a225c1904de8f856aec47d813",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.index",
        "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
        "typing_Lib.IntTypes.uint_t", "typing_Lib.RawIntTypes.uint_to_nat",
        "typing_Prims.pow2", "well-founded-ordering-on-nat"
      ],
      0,
      "1b452e49fe1adeddc223c7f22930d52c"
    ],
    [
      "Lib.ByteSequence.nat_to_intseq_le",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Lib.IntTypes.bits", "equation_Prims.nat",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "22ae62af6381b0170d787fa80eacfb5b"
    ],
    [
      "Lib.ByteSequence.nat_to_intseq_le",
      2,
      1,
      1,
      [ "@query" ],
      0,
      "5e7c0e39634c5d09f3c4e86917848c1f"
    ],
    [
      "Lib.ByteSequence.nat_to_bytes_be",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@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__",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "3d3f40f5ee4332889d5b6211fa8782ba"
    ],
    [
      "Lib.ByteSequence.nat_to_bytes_be",
      2,
      1,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits"
      ],
      0,
      "b5ac4d50c129d3c328576a7caadb9180"
    ],
    [
      "Lib.ByteSequence.nat_to_bytes_le",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@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__",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "0539625cca04ba59a61521bb7702ab5c"
    ],
    [
      "Lib.ByteSequence.nat_to_bytes_le",
      2,
      1,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits"
      ],
      0,
      "72d0ee719cac54f63cc9fda9d8c5d884"
    ],
    [
      "Lib.ByteSequence.unfold_nat_to_intseq_le",
      1,
      1,
      0,
      [
        "@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",
        "constructor_distinct_Tm_unit", "equality_tok_Lib.IntTypes.U32@tok",
        "equation_Lib.IntTypes.bits", "equation_Prims.nat",
        "equation_Prims.pos",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "lemma_Lib.IntTypes.pow2_values",
        "primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_39fd33cf414d74e3361a179fa5bc2dc3",
        "refinement_interpretation_Tm_refine_3f2962d5b49cbb44cd45056c29e69cef",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "refinement_interpretation_Tm_refine_f16347476b439776210c3eceabc4f49d",
        "typing_Lib.IntTypes.bits", "typing_Prims.pow2",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "e58eb7414538eefc503feeb220ef7836"
    ],
    [
      "Lib.ByteSequence.unfold_nat_to_intseq_le",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Tm_unit", "equation_Lib.IntTypes.bits",
        "equation_Prims.nat", "int_inversion", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_f16347476b439776210c3eceabc4f49d",
        "typing_Lib.IntTypes.bits"
      ],
      0,
      "1b6eb0ce92f0db8bc6aaf8e6412858eb"
    ],
    [
      "Lib.ByteSequence.unfold_nat_to_intseq_le",
      3,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.ByteSequence.nat_to_intseq_le_.fuel_instrumented",
        "@fuel_irrelevance_Lib.ByteSequence.nat_to_intseq_le_.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Lib.ByteSequence.nat_to_intseq_le", "equation_Prims.nat",
        "equation_with_fuel_Lib.ByteSequence.nat_to_intseq_le_.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Division", "primitive_Prims.op_Equality",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_f16347476b439776210c3eceabc4f49d"
      ],
      0,
      "cb56bd9ba7e1773ae5fdcd2071dfac81"
    ],
    [
      "Lib.ByteSequence.index_nat_to_intseq_le",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Tm_unit",
        "equation_Lib.ByteSequence.nat_to_intseq_le",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.Sequence.length", "equation_Prims.nat",
        "equation_Prims.pos",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0a3deab6de0ff2f22cf53649d1f6ace2",
        "refinement_interpretation_Tm_refine_39fd33cf414d74e3361a179fa5bc2dc3",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_5a4fe33be2b93c781e552e491bb9dd31",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "typing_Lib.ByteSequence.nat_to_intseq_le",
        "typing_Lib.IntTypes.bits"
      ],
      0,
      "e7eea65c939b94b71da335cfe1744e14"
    ],
    [
      "Lib.ByteSequence.index_nat_to_intseq_le",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Tm_unit",
        "equation_Lib.ByteSequence.nat_to_intseq_le",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.Sequence.length", "equation_Prims.nat",
        "equation_Prims.pos",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0a3deab6de0ff2f22cf53649d1f6ace2",
        "refinement_interpretation_Tm_refine_39fd33cf414d74e3361a179fa5bc2dc3",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_5a4fe33be2b93c781e552e491bb9dd31",
        "refinement_interpretation_Tm_refine_77785ef26a8f49cf97349ae0baec5c99",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "typing_Lib.ByteSequence.nat_to_intseq_le",
        "typing_Lib.IntTypes.bits"
      ],
      0,
      "a4c5b50e95bd3f4780d3f203ed626349"
    ],
    [
      "Lib.ByteSequence.index_nat_to_intseq_le",
      3,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.ByteSequence.nat_to_intseq_le_.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Lib.IntTypes_pretyping_877cb84f86c77989c5c1e5a978e57417",
        "Lib.IntTypes_pretyping_d450aafb6f125538d0e96425faddef55",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_1f798466ae432316209c99ab8d617b9c_3",
        "binder_x_877cb84f86c77989c5c1e5a978e57417_1",
        "binder_x_b29492cee47c5a7077c6b9e6d99c7cd6_4",
        "binder_x_bdddb2d86f5a239ece3bb01dd191963e_2",
        "binder_x_d450aafb6f125538d0e96425faddef55_0",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Tm_unit", "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_Lib.ByteSequence.nat_to_intseq_le",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq",
        "equation_Prims.nat", "equation_Prims.pos",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_index_app1",
        "lemma_FStar.Seq.Base.lemma_index_app2",
        "lemma_FStar.Seq.Base.lemma_index_create",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Division", "primitive_Prims.op_Equality",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_03127b5d59ee3055620018693b4264e8",
        "refinement_interpretation_Tm_refine_0a3deab6de0ff2f22cf53649d1f6ace2",
        "refinement_interpretation_Tm_refine_25f4cacbd0f9c1a8a9df05cef2b4c213",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_39fd33cf414d74e3361a179fa5bc2dc3",
        "refinement_interpretation_Tm_refine_51db53796f2691fa1ec36f3c0abf1393",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_5a4fe33be2b93c781e552e491bb9dd31",
        "refinement_interpretation_Tm_refine_88196d5cf70d057c8c0e1608f23d8dc6",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d856f709de20bfa4e940d47b1570ef4d",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_e7baecf1446b738b3604b097069629a3",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "typing_FStar.Seq.Base.create",
        "typing_Lib.ByteSequence.nat_to_intseq_le",
        "typing_Lib.ByteSequence.nat_to_intseq_le_",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.uint",
        "typing_Lib.IntTypes.uint_t", "typing_Lib.Sequence.create",
        "typing_Prims.pow2", "typing_tok_Lib.IntTypes.SEC@tok",
        "typing_tok_Lib.IntTypes.U1@tok", "typing_tok_Lib.IntTypes.U32@tok",
        "well-founded-ordering-on-nat"
      ],
      0,
      "a1265236e57cb5d58d7406ebe16cf42f"
    ],
    [
      "Lib.ByteSequence.index_nat_to_intseq_le",
      4,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Tm_unit", "equation_Lib.IntTypes.bits",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Lib.IntTypes.bits"
      ],
      0,
      "8ba8d00819921bce6851077f6f930109"
    ],
    [
      "Lib.ByteSequence.index_nat_to_intseq_le",
      5,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Tm_unit", "equation_Lib.IntTypes.bits",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Lib.IntTypes.bits"
      ],
      0,
      "8ad8f02b1504fd3367d1e4068ef1c7ca"
    ],
    [
      "Lib.ByteSequence.uint_to_bytes_le",
      1,
      1,
      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_Lib.IntTypes.numbytes", "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,
      "a4876cdff3e106945748c828b41db6f4"
    ],
    [
      "Lib.ByteSequence.uint_to_bytes_le",
      2,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.Sequence.length", "equation_Prims.nat",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "typing_Lib.IntTypes.uint_v"
      ],
      0,
      "1975e6a5150231471045f66b218167c4"
    ],
    [
      "Lib.ByteSequence.index_uint_to_bytes_le",
      1,
      1,
      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",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq",
        "equation_Prims.nat", "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "lemma_Lib.IntTypes.pow2_values",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_7c0cec89d4816950a0b97037fb573d60",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_Lib.ByteSequence.uint_to_bytes_le",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "cf9f88ac584f403a5fe2858b4b3a2361"
    ],
    [
      "Lib.ByteSequence.index_uint_to_bytes_le",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Tm_unit", "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Lib.ByteSequence.nat_to_bytes_le",
        "equation_Lib.ByteSequence.nat_to_intseq_le",
        "equation_Lib.ByteSequence.uint_to_bytes_le",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.to_seq",
        "equation_Prims.nat", "equation_Prims.pos",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_Lib.IntTypes.pow2_values",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_425e4bc4b19967ca7e9cd812aeb5e33d",
        "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
        "refinement_interpretation_Tm_refine_78ea63ceb027a3f1c790955bc68a707b",
        "refinement_interpretation_Tm_refine_7c0cec89d4816950a0b97037fb573d60",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_af27ee4a225c1904de8f856aec47d813",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "typing_Lib.ByteSequence.uint_to_bytes_le",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.numbytes",
        "typing_Lib.IntTypes.uint_t", "typing_Lib.IntTypes.uint_v",
        "typing_Lib.RawIntTypes.uint_to_nat", "typing_Lib.Sequence.index",
        "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "9ccfa4b66f397afe3927fb54664488f8"
    ],
    [
      "Lib.ByteSequence.uint_to_bytes_be",
      1,
      1,
      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_Lib.IntTypes.numbytes", "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,
      "61ff09ac0f275c4669d3668ac2d2350d"
    ],
    [
      "Lib.ByteSequence.uint_to_bytes_be",
      2,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.Sequence.length", "equation_Prims.nat",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "typing_Lib.IntTypes.uint_v"
      ],
      0,
      "5e778235c028c5a26186d6481522f3b5"
    ],
    [
      "Lib.ByteSequence.uint_from_bytes_le",
      1,
      1,
      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.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.numbytes", "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_70597463dd221580f371f83615527f81",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "ef3501eef49307b0ffca9f537539b15a"
    ],
    [
      "Lib.ByteSequence.uint_from_bytes_le",
      2,
      1,
      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.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.numbytes", "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_70597463dd221580f371f83615527f81",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "8b6901edb1a7f42e66bd9273ad508ea0"
    ],
    [
      "Lib.ByteSequence.uint_from_bytes_le",
      3,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.seq", "equation_Prims.nat",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_70597463dd221580f371f83615527f81",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.uint_t",
        "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "94eed3382030a05b3db5fe41c4259871"
    ],
    [
      "Lib.ByteSequence.uint_from_bytes_be",
      1,
      1,
      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.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.numbytes", "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_70597463dd221580f371f83615527f81",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "47a473c81aaaaf8961d46fc63a1b0875"
    ],
    [
      "Lib.ByteSequence.uint_from_bytes_be",
      2,
      1,
      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.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.numbytes", "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_70597463dd221580f371f83615527f81",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "5e1ba0c98efea829545f7ddbcb6c4533"
    ],
    [
      "Lib.ByteSequence.uint_from_bytes_be",
      3,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.seq", "equation_Prims.nat",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_70597463dd221580f371f83615527f81",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.uint_t",
        "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "fe1ec2418b78316a871dcbb20912c5bd"
    ],
    [
      "Lib.ByteSequence.uints_to_bytes_le_inner",
      1,
      1,
      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_Lib.IntTypes.numbytes", "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_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_b7c6ab0416aa19b9be0f0ab3d684c8cc",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "20020f3339cd11aab306b97dc492c486"
    ],
    [
      "Lib.ByteSequence.uints_to_bytes_le_inner",
      2,
      1,
      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_Lib.IntTypes.numbytes", "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_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_b7c6ab0416aa19b9be0f0ab3d684c8cc",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "491cc91fed284bfac2a5f926149a33c7"
    ],
    [
      "Lib.ByteSequence.uints_to_bytes_le",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.numbytes", "equation_Prims.nat",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_b7c6ab0416aa19b9be0f0ab3d684c8cc",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "0877934ca0ede77581ef4e7517bd5877"
    ],
    [
      "Lib.ByteSequence.uints_to_bytes_le",
      2,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "constructor_distinct_Lib.IntTypes.U32",
        "data_elim_FStar.Pervasives.Native.Mktuple2",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.seq",
        "equation_Prims.nat",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_b7c6ab0416aa19b9be0f0ab3d684c8cc",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_ca6033dcb0061e64137e14b3cd31e549",
        "typing_Lib.IntTypes.uint_t", "typing_Lib.Sequence.length",
        "typing_tok_Lib.IntTypes.U8@tok", "unit_typing"
      ],
      0,
      "42592e52b2952dc0322e960faa2196be"
    ],
    [
      "Lib.ByteSequence.uints_to_bytes_be_inner",
      1,
      1,
      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_Lib.IntTypes.numbytes", "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_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_b7c6ab0416aa19b9be0f0ab3d684c8cc",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "55aa82ca08ded1c16fbe10d1e43ddc3c"
    ],
    [
      "Lib.ByteSequence.uints_to_bytes_be_inner",
      2,
      1,
      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_Lib.IntTypes.numbytes", "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_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_b7c6ab0416aa19b9be0f0ab3d684c8cc",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "8ee80bfe155996f030c9e6a9fab46bdc"
    ],
    [
      "Lib.ByteSequence.uints_to_bytes_be",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.numbytes", "equation_Prims.nat",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_b7c6ab0416aa19b9be0f0ab3d684c8cc",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "830085d2cc3e5e4d13471d63ea7c26fa"
    ],
    [
      "Lib.ByteSequence.uints_to_bytes_be",
      2,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "constructor_distinct_Lib.IntTypes.U32",
        "data_elim_FStar.Pervasives.Native.Mktuple2",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.seq",
        "equation_Prims.nat",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_b7c6ab0416aa19b9be0f0ab3d684c8cc",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_ca6033dcb0061e64137e14b3cd31e549",
        "typing_Lib.IntTypes.uint_t", "typing_Lib.Sequence.length",
        "typing_tok_Lib.IntTypes.U8@tok", "unit_typing"
      ],
      0,
      "cb107bea9e108383f4002de268ed3ceb"
    ],
    [
      "Lib.ByteSequence.uints_from_bytes_le",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.numbytes", "equation_Prims.nat",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_70597463dd221580f371f83615527f81",
        "refinement_interpretation_Tm_refine_b7c6ab0416aa19b9be0f0ab3d684c8cc",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "1091cde8be4926cf1e2c9fd903e771e8"
    ],
    [
      "Lib.ByteSequence.uints_from_bytes_le",
      2,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.numbytes", "equation_Prims.nat",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_70597463dd221580f371f83615527f81",
        "refinement_interpretation_Tm_refine_b7c6ab0416aa19b9be0f0ab3d684c8cc",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "f384cc4d079647d641cb0a37fb05a198"
    ],
    [
      "Lib.ByteSequence.uints_from_bytes_le",
      3,
      1,
      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.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_Prims.nat", "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_Lib.IntTypes.pow2_values",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_70597463dd221580f371f83615527f81",
        "refinement_interpretation_Tm_refine_b7c6ab0416aa19b9be0f0ab3d684c8cc",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.uint_t",
        "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "12f47550d79ff09bee7dd5c6b538ef5d"
    ],
    [
      "Lib.ByteSequence.uints_from_bytes_be",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.numbytes", "equation_Prims.nat",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_70597463dd221580f371f83615527f81",
        "refinement_interpretation_Tm_refine_b7c6ab0416aa19b9be0f0ab3d684c8cc",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "81257c69341a709ef1f936574073f082"
    ],
    [
      "Lib.ByteSequence.uints_from_bytes_be",
      2,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.numbytes", "equation_Prims.nat",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_70597463dd221580f371f83615527f81",
        "refinement_interpretation_Tm_refine_b7c6ab0416aa19b9be0f0ab3d684c8cc",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "723309352a0e92f34b0ac37df2bf7bc8"
    ],
    [
      "Lib.ByteSequence.uints_from_bytes_be",
      3,
      1,
      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.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_Prims.nat", "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_Lib.IntTypes.pow2_values",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_70597463dd221580f371f83615527f81",
        "refinement_interpretation_Tm_refine_b7c6ab0416aa19b9be0f0ab3d684c8cc",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.uint_t",
        "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "e9e600ff3c1232b000c04aa39503d4da"
    ],
    [
      "Lib.ByteSequence.nat_from_intseq_le_slice_lemma0",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.Sequence.lseq", "equation_Prims.nat",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "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_5077f55bb8c2178e0da6c05cda8379c0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42"
      ],
      0,
      "b90fba8eb8f9f8b3ee7a4592c25dfcc4"
    ],
    [
      "Lib.ByteSequence.nat_from_intseq_le_slice_lemma0",
      2,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.ByteSequence.nat_from_intseq_le_.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Lib.ByteSequence.nat_from_intseq_le_.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.PUB",
        "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",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U16@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bit_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.byte_t",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.pub_uint128",
        "equation_Lib.IntTypes.pub_uint16",
        "equation_Lib.IntTypes.pub_uint64", "equation_Lib.IntTypes.size_t",
        "equation_Lib.IntTypes.uint1", "equation_Lib.IntTypes.uint128",
        "equation_Lib.IntTypes.uint16", "equation_Lib.IntTypes.uint32",
        "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.uint8",
        "equation_Lib.IntTypes.uint_t", "equation_Lib.IntTypes.uint_v",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq",
        "equation_Prims.nat",
        "equation_with_fuel_Lib.ByteSequence.nat_from_intseq_le_.fuel_instrumented",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "fuel_guarded_inversion_Lib.IntTypes.secrecy_level",
        "function_token_typing_Lib.IntTypes.bit_t",
        "function_token_typing_Lib.IntTypes.byte_t",
        "function_token_typing_Lib.IntTypes.pub_uint128",
        "function_token_typing_Lib.IntTypes.pub_uint16",
        "function_token_typing_Lib.IntTypes.pub_uint64",
        "function_token_typing_Lib.IntTypes.size_t",
        "function_token_typing_Lib.IntTypes.uint1",
        "function_token_typing_Lib.IntTypes.uint128",
        "function_token_typing_Lib.IntTypes.uint16",
        "function_token_typing_Lib.IntTypes.uint32",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Lib.IntTypes.uint8",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.slice_slice",
        "lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Equality", "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_3321cbe2f573e3c988fd0895bf1f0cf9",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_5077f55bb8c2178e0da6c05cda8379c0",
        "refinement_interpretation_Tm_refine_528d1ac7a4a801fe55aa0f436f85ad2a",
        "refinement_interpretation_Tm_refine_559c261b1c3777929ea329abfe70ab33",
        "refinement_interpretation_Tm_refine_57683ab53ec5b7f6ea2dd6ddc8886f8f",
        "refinement_interpretation_Tm_refine_57685e11d25e58c1aa0fa18e05f8531c",
        "refinement_interpretation_Tm_refine_78ea63ceb027a3f1c790955bc68a707b",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_Tm_refine_af27ee4a225c1904de8f856aec47d813",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_be3dd9f91812b6e86fca463c4f393a8e",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.slice",
        "typing_Lib.ByteSequence.nat_from_intseq_le_",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.uint_t",
        "typing_Lib.IntTypes.uint_v", "typing_Lib.RawIntTypes.uint_to_nat",
        "typing_Lib.Sequence.length", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.SEC@tok",
        "typing_tok_Lib.IntTypes.U128@tok",
        "typing_tok_Lib.IntTypes.U16@tok", "typing_tok_Lib.IntTypes.U1@tok",
        "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok",
        "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "3f2a9a1921997007b825fb4097a3ef19"
    ],
    [
      "Lib.ByteSequence.nat_from_intseq_le_slice_lemma1",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.uint_t", "equation_Lib.Sequence.length",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_Prims.nat", "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "fuel_guarded_inversion_Lib.IntTypes.secrecy_level",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "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_5077f55bb8c2178e0da6c05cda8379c0",
        "refinement_interpretation_Tm_refine_5e337c55673fc06c3847583ecedcf28a",
        "refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_Lib.IntTypes.uint_t", "typing_Lib.Sequence.length"
      ],
      0,
      "d30429f38ce9cccfed977ce7fd4ee211"
    ],
    [
      "Lib.ByteSequence.nat_from_intseq_le_slice_lemma1",
      2,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.ByteSequence.nat_from_intseq_le_.fuel_instrumented",
        "@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.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",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U16@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bit_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.byte_t",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.pub_uint128",
        "equation_Lib.IntTypes.pub_uint16",
        "equation_Lib.IntTypes.pub_uint64", "equation_Lib.IntTypes.size_t",
        "equation_Lib.IntTypes.uint1", "equation_Lib.IntTypes.uint128",
        "equation_Lib.IntTypes.uint16", "equation_Lib.IntTypes.uint32",
        "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.uint8",
        "equation_Lib.IntTypes.uint_t", "equation_Lib.IntTypes.uint_v",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq",
        "equation_Prims.nat",
        "equation_with_fuel_Lib.ByteSequence.nat_from_intseq_le_.fuel_instrumented",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "fuel_guarded_inversion_Lib.IntTypes.secrecy_level",
        "function_token_typing_Lib.IntTypes.bit_t",
        "function_token_typing_Lib.IntTypes.byte_t",
        "function_token_typing_Lib.IntTypes.pub_uint128",
        "function_token_typing_Lib.IntTypes.pub_uint16",
        "function_token_typing_Lib.IntTypes.pub_uint64",
        "function_token_typing_Lib.IntTypes.size_t",
        "function_token_typing_Lib.IntTypes.uint1",
        "function_token_typing_Lib.IntTypes.uint128",
        "function_token_typing_Lib.IntTypes.uint16",
        "function_token_typing_Lib.IntTypes.uint32",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Lib.IntTypes.uint8",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.slice_is_empty",
        "lemma_FStar.Seq.Properties.slice_slice",
        "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_values",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "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_3321cbe2f573e3c988fd0895bf1f0cf9",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_5077f55bb8c2178e0da6c05cda8379c0",
        "refinement_interpretation_Tm_refine_528d1ac7a4a801fe55aa0f436f85ad2a",
        "refinement_interpretation_Tm_refine_559c261b1c3777929ea329abfe70ab33",
        "refinement_interpretation_Tm_refine_57683ab53ec5b7f6ea2dd6ddc8886f8f",
        "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
        "refinement_interpretation_Tm_refine_78ea63ceb027a3f1c790955bc68a707b",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_Tm_refine_af27ee4a225c1904de8f856aec47d813",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_cd046bc4a887ee7e1b05946e0bf5772b",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "token_correspondence_Lib.ByteSequence.nat_from_intseq_le_.fuel_instrumented",
        "typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.index",
        "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
        "typing_Lib.ByteSequence.nat_from_intseq_le_",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.uint_t",
        "typing_Lib.IntTypes.uint_v", "typing_Lib.RawIntTypes.uint_to_nat",
        "typing_Lib.Sequence.index", "typing_Lib.Sequence.length",
        "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.SEC@tok",
        "typing_tok_Lib.IntTypes.U128@tok",
        "typing_tok_Lib.IntTypes.U16@tok", "typing_tok_Lib.IntTypes.U1@tok",
        "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok",
        "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "554ca63d4b2c118e502f717475f845ab"
    ],
    [
      "Lib.ByteSequence.nat_from_intseq_le_slice_lemma_",
      1,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.ByteSequence.nat_from_intseq_le_.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U16@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.uint8",
        "equation_Lib.IntTypes.uint_t", "equation_Lib.Sequence.length",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_Prims.nat",
        "equation_with_fuel_Lib.ByteSequence.nat_from_intseq_le_.fuel_instrumented",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "fuel_guarded_inversion_Lib.IntTypes.secrecy_level",
        "function_token_typing_Lib.IntTypes.uint8",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.slice_slice",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "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_3321cbe2f573e3c988fd0895bf1f0cf9",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_528d1ac7a4a801fe55aa0f436f85ad2a",
        "refinement_interpretation_Tm_refine_5e069b8311ac894148a7ebf9b041db07",
        "refinement_interpretation_Tm_refine_8ae4abcfc6bc8d4903b7e1f40e070ec2",
        "refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Seq.Base.slice", "typing_Lib.IntTypes.uint_t",
        "typing_Lib.Sequence.length"
      ],
      0,
      "2543c747d6efc4b243084f2a72d6825d"
    ],
    [
      "Lib.ByteSequence.nat_from_intseq_le_slice_lemma_",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Tm_unit", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.uint_t", "equation_Lib.Sequence.lseq",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_397981180314460b93828d3558981d81",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_Lib.IntTypes.bits"
      ],
      0,
      "c0ad1a83613579690e01d5d2f7df7b1d"
    ],
    [
      "Lib.ByteSequence.nat_from_intseq_le_slice_lemma_",
      3,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.ByteSequence.nat_from_intseq_le_.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Lib.IntTypes_pretyping_877cb84f86c77989c5c1e5a978e57417",
        "Lib.IntTypes_pretyping_d450aafb6f125538d0e96425faddef55",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_0f5a39a89afb2caf19b5057c1bafd24d_3",
        "binder_x_877cb84f86c77989c5c1e5a978e57417_1",
        "binder_x_bdddb2d86f5a239ece3bb01dd191963e_2",
        "binder_x_be0c941c6d4fe936a5207c343b62c6d2_4",
        "binder_x_d450aafb6f125538d0e96425faddef55_0",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "data_typing_intro_Lib.IntTypes.PUB@tok",
        "data_typing_intro_Lib.IntTypes.U8@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U16@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Prims.LexTop@tok",
        "equation_Lib.IntTypes.bit_t", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.pub_uint128",
        "equation_Lib.IntTypes.pub_uint16",
        "equation_Lib.IntTypes.pub_uint64", "equation_Lib.IntTypes.size_t",
        "equation_Lib.IntTypes.uint1", "equation_Lib.IntTypes.uint128",
        "equation_Lib.IntTypes.uint16", "equation_Lib.IntTypes.uint32",
        "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.uint8",
        "equation_Lib.IntTypes.uint_t", "equation_Lib.Sequence.length",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_Prims.nat",
        "equation_with_fuel_Lib.ByteSequence.nat_from_intseq_le_.fuel_instrumented",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "fuel_guarded_inversion_Lib.IntTypes.secrecy_level",
        "function_token_typing_Lib.IntTypes.bit_t",
        "function_token_typing_Lib.IntTypes.byte_t",
        "function_token_typing_Lib.IntTypes.pub_uint128",
        "function_token_typing_Lib.IntTypes.pub_uint16",
        "function_token_typing_Lib.IntTypes.pub_uint64",
        "function_token_typing_Lib.IntTypes.size_t",
        "function_token_typing_Lib.IntTypes.uint1",
        "function_token_typing_Lib.IntTypes.uint128",
        "function_token_typing_Lib.IntTypes.uint16",
        "function_token_typing_Lib.IntTypes.uint32",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Lib.IntTypes.uint8",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.slice_length",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "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_57683ab53ec5b7f6ea2dd6ddc8886f8f",
        "refinement_interpretation_Tm_refine_5a4fe33be2b93c781e552e491bb9dd31",
        "refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_fd5707acfc9e9437411d3fd6464fa375",
        "typing_FStar.Seq.Base.slice",
        "typing_Lib.ByteSequence.nat_from_intseq_le_",
        "typing_Lib.IntTypes.uint_t", "unit_inversion", "unit_typing",
        "well-founded-ordering-on-nat"
      ],
      0,
      "ec27d868f23991307a7f37cb46c145de"
    ],
    [
      "Lib.ByteSequence.nat_from_intseq_le_slice_lemma",
      1,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.ByteSequence.nat_from_intseq_le_.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U16@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Lib.ByteSequence.nat_from_intseq_le",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.pub_int_t",
        "equation_Lib.IntTypes.uint_t", "equation_Lib.Sequence.length",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_Prims.nat",
        "equation_with_fuel_Lib.ByteSequence.nat_from_intseq_le_.fuel_instrumented",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "fuel_guarded_inversion_Lib.IntTypes.secrecy_level",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_Equality", "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_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_5e069b8311ac894148a7ebf9b041db07",
        "refinement_interpretation_Tm_refine_8ae4abcfc6bc8d4903b7e1f40e070ec2",
        "refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_Lib.IntTypes.uint_t"
      ],
      0,
      "a34fbf46c2eab1571ea63114f388de1f"
    ],
    [
      "Lib.ByteSequence.nat_from_intseq_le_slice_lemma",
      2,
      1,
      1,
      [ "@query", "equation_Lib.ByteSequence.nat_from_intseq_le" ],
      0,
      "6210ee5d32012db0c943398803de6edc"
    ],
    [
      "Lib.ByteSequence.nat_from_bytes_le_slice_lemma",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.Sequence.lseq", "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_8ae4abcfc6bc8d4903b7e1f40e070ec2",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42"
      ],
      0,
      "d0474c30ed201275d899faf3dede171c"
    ],
    [
      "Lib.ByteSequence.nat_from_bytes_le_slice_lemma",
      2,
      1,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Lib.ByteSequence.nat_from_bytes_le",
        "equation_Lib.ByteSequence.nat_from_intseq_le",
        "equation_Lib.IntTypes.bits"
      ],
      0,
      "52969867a3c280cad75c331716da035e"
    ],
    [
      "Lib.ByteSequence.uints_from_bytes_le_lemma0",
      1,
      1,
      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.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_Prims.nat", "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_Lib.IntTypes.pow2_values",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_70597463dd221580f371f83615527f81",
        "refinement_interpretation_Tm_refine_78ea63ceb027a3f1c790955bc68a707b",
        "refinement_interpretation_Tm_refine_b7c6ab0416aa19b9be0f0ab3d684c8cc",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.uint_t",
        "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "5f384b58810a52edec3565c0e18f00b7"
    ],
    [
      "Lib.ByteSequence.uints_from_bytes_le_lemma0",
      2,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.numbytes", "equation_Prims.nat",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_70597463dd221580f371f83615527f81",
        "refinement_interpretation_Tm_refine_b7c6ab0416aa19b9be0f0ab3d684c8cc",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "e708004318c42b561581b231d0751df4"
    ],
    [
      "Lib.ByteSequence.uints_from_bytes_le_lemma0",
      3,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
        "Lib.ByteSequence_interpretation_Tm_arrow_d1f54a45f77864e9cdebecf30e4a2f0e",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.PUB",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U16@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Lib.ByteSequence.uints_from_bytes_le",
        "equation_Lib.IntTypes.uint_t", "equation_Prims.nat",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "fuel_guarded_inversion_Lib.IntTypes.secrecy_level",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "interpretation_Tm_abs_c195bd9080359e043c42f5562b6d2df0",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_27686609265e41bc9c60bf85a827b5c4",
        "refinement_interpretation_Tm_refine_5a4fe33be2b93c781e552e491bb9dd31",
        "refinement_interpretation_Tm_refine_70597463dd221580f371f83615527f81",
        "refinement_interpretation_Tm_refine_b7c6ab0416aa19b9be0f0ab3d684c8cc",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Lib.IntTypes.uint_t", "typing_Lib.Sequence.createi",
        "typing_Tm_abs_c195bd9080359e043c42f5562b6d2df0"
      ],
      0,
      "7ee44003543d382526548f8215935f95"
    ],
    [
      "Lib.ByteSequence.uints_from_bytes_le_lemma1",
      1,
      1,
      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.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_Prims.nat", "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Addition",
        "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_0ec18f8d17586cc123656165790c35a7",
        "refinement_interpretation_Tm_refine_70597463dd221580f371f83615527f81",
        "refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.uint_t",
        "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "ad7d3fd4ac5472799825d408a7a76fcc"
    ],
    [
      "Lib.ByteSequence.uints_from_bytes_le_lemma1",
      2,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.numbytes", "equation_Prims.nat",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec18f8d17586cc123656165790c35a7",
        "refinement_interpretation_Tm_refine_70597463dd221580f371f83615527f81"
      ],
      0,
      "8f2bf5413daaaf132b0af04b915d9480"
    ],
    [
      "Lib.ByteSequence.uints_from_bytes_le_lemma1",
      3,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Lib.ByteSequence.uints_from_bytes_le",
        "equation_Lib.IntTypes.uint_t", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec18f8d17586cc123656165790c35a7",
        "refinement_interpretation_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
        "refinement_interpretation_Tm_refine_559c261b1c3777929ea329abfe70ab33",
        "refinement_interpretation_Tm_refine_5a4fe33be2b93c781e552e491bb9dd31",
        "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
        "refinement_interpretation_Tm_refine_70597463dd221580f371f83615527f81",
        "refinement_interpretation_Tm_refine_78ea63ceb027a3f1c790955bc68a707b",
        "refinement_interpretation_Tm_refine_b7c6ab0416aa19b9be0f0ab3d684c8cc",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_Lib.ByteSequence.uints_from_bytes_le",
        "typing_Lib.IntTypes.uint_t", "typing_Lib.Sequence.index"
      ],
      0,
      "2aa2fe2addd797a7a95e3d0e00c67e0d"
    ],
    [
      "Lib.ByteSequence.uints_from_bytes_le_slice_lemma",
      1,
      1,
      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",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_Prims.nat", "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "fuel_guarded_inversion_Lib.IntTypes.secrecy_level",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_Lib.IntTypes.pow2_values",
        "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_0ec18f8d17586cc123656165790c35a7",
        "refinement_interpretation_Tm_refine_70597463dd221580f371f83615527f81",
        "refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.uint_t",
        "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "921b3d2d907c9d120d058f6f67fad9a6"
    ],
    [
      "Lib.ByteSequence.uints_from_bytes_le_slice_lemma",
      2,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.numbytes", "equation_Prims.nat",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec18f8d17586cc123656165790c35a7",
        "refinement_interpretation_Tm_refine_70597463dd221580f371f83615527f81"
      ],
      0,
      "100c624ab6f1f7ec65a4c685d8447389"
    ],
    [
      "Lib.ByteSequence.uints_from_bytes_le_slice_lemma",
      3,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.ByteSequence.nat_from_intseq_le_.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
        "Lib.ByteSequence_interpretation_Tm_arrow_d1f54a45f77864e9cdebecf30e4a2f0e",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.PUB",
        "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",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U16@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Lib.ByteSequence.nat_from_intseq_le",
        "equation_Lib.ByteSequence.uint_from_bytes_le",
        "equation_Lib.ByteSequence.uints_from_bytes_le",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.byte_t",
        "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.pub_int_t",
        "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq",
        "equation_Prims.nat",
        "equation_with_fuel_Lib.ByteSequence.nat_from_intseq_le_.fuel_instrumented",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "fuel_guarded_inversion_Lib.IntTypes.secrecy_level",
        "function_token_typing_Lib.IntTypes.byte_t",
        "function_token_typing_Lib.IntTypes.uint8",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "interpretation_Tm_abs_c195bd9080359e043c42f5562b6d2df0",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.slice_is_empty",
        "lemma_FStar.Seq.Properties.slice_slice",
        "lemma_Lib.IntTypes.pow2_values", "lemma_Lib.Sequence.eq_elim",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "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_0a44a9c52461f7b29dab1fe1db7afc62",
        "refinement_interpretation_Tm_refine_0ec18f8d17586cc123656165790c35a7",
        "refinement_interpretation_Tm_refine_27686609265e41bc9c60bf85a827b5c4",
        "refinement_interpretation_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
        "refinement_interpretation_Tm_refine_528d1ac7a4a801fe55aa0f436f85ad2a",
        "refinement_interpretation_Tm_refine_559c261b1c3777929ea329abfe70ab33",
        "refinement_interpretation_Tm_refine_5a4fe33be2b93c781e552e491bb9dd31",
        "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
        "refinement_interpretation_Tm_refine_70597463dd221580f371f83615527f81",
        "refinement_interpretation_Tm_refine_78ea63ceb027a3f1c790955bc68a707b",
        "refinement_interpretation_Tm_refine_8bdecfb5d16fa4a517d5fa57acd2da6d",
        "refinement_interpretation_Tm_refine_92683919383128558df392539edfff77",
        "refinement_interpretation_Tm_refine_9fa3c3f1b32e27669a46bed06f432c2f",
        "refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_Tm_refine_b7c6ab0416aa19b9be0f0ab3d684c8cc",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_cd046bc4a887ee7e1b05946e0bf5772b",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.numbytes",
        "typing_Lib.IntTypes.uint_t", "typing_Lib.Sequence.createi",
        "typing_Lib.Sequence.index", "typing_Lib.Sequence.sub",
        "typing_Lib.Sequence.to_seq",
        "typing_Tm_abs_c195bd9080359e043c42f5562b6d2df0",
        "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "676bfd6309b1ef168a3fe2d87271f429"
    ],
    [
      "Lib.ByteSequence.uints_from_bytes_le_nat_lemma0",
      1,
      1,
      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.SEC@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_Prims.nat", "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "fuel_guarded_inversion_Lib.IntTypes.secrecy_level",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_Lib.IntTypes.pow2_values",
        "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_06d6ed1ad952e3cc064dfa1dcac87ee7",
        "refinement_interpretation_Tm_refine_0ec18f8d17586cc123656165790c35a7",
        "refinement_interpretation_Tm_refine_70597463dd221580f371f83615527f81",
        "refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_cc474c888d1f7a71bdef3f0c5b9a1f98",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.uint_t",
        "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "2d6d0da38a2fd9eb124b9f28fd40b4f4"
    ],
    [
      "Lib.ByteSequence.uints_from_bytes_le_nat_lemma0",
      2,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.numbytes", "equation_Prims.nat",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec18f8d17586cc123656165790c35a7",
        "refinement_interpretation_Tm_refine_70597463dd221580f371f83615527f81"
      ],
      0,
      "d534ab82f4ad8afcfdd0e053f731229e"
    ],
    [
      "Lib.ByteSequence.uints_from_bytes_le_nat_lemma0",
      3,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.ByteSequence.nat_from_intseq_le_.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Lib.ByteSequence.nat_from_intseq_le_.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
        "Lib.ByteSequence_interpretation_Tm_arrow_d1f54a45f77864e9cdebecf30e4a2f0e",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.PUB",
        "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",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U16@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Lib.ByteSequence.nat_from_intseq_le",
        "equation_Lib.ByteSequence.uint_from_bytes_le",
        "equation_Lib.ByteSequence.uints_from_bytes_le",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.byte_t",
        "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.pub_int_t",
        "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq",
        "equation_Prims.nat",
        "equation_with_fuel_Lib.ByteSequence.nat_from_intseq_le_.fuel_instrumented",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "fuel_guarded_inversion_Lib.IntTypes.secrecy_level",
        "function_token_typing_Lib.IntTypes.byte_t",
        "function_token_typing_Lib.IntTypes.uint8",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "interpretation_Tm_abs_c195bd9080359e043c42f5562b6d2df0",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.slice_is_empty",
        "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_values",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "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_0ec18f8d17586cc123656165790c35a7",
        "refinement_interpretation_Tm_refine_27686609265e41bc9c60bf85a827b5c4",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_57683ab53ec5b7f6ea2dd6ddc8886f8f",
        "refinement_interpretation_Tm_refine_5a4fe33be2b93c781e552e491bb9dd31",
        "refinement_interpretation_Tm_refine_70597463dd221580f371f83615527f81",
        "refinement_interpretation_Tm_refine_8bdecfb5d16fa4a517d5fa57acd2da6d",
        "refinement_interpretation_Tm_refine_9fa3c3f1b32e27669a46bed06f432c2f",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_Tm_refine_af27ee4a225c1904de8f856aec47d813",
        "refinement_interpretation_Tm_refine_b7c6ab0416aa19b9be0f0ab3d684c8cc",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_ba858eed7da9e98b76c6e7e6b5991c39",
        "refinement_interpretation_Tm_refine_bb3289e79bf84af56b7fcd3856b5bc88",
        "refinement_interpretation_Tm_refine_cc474c888d1f7a71bdef3f0c5b9a1f98",
        "refinement_interpretation_Tm_refine_cd046bc4a887ee7e1b05946e0bf5772b",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_e7baecf1446b738b3604b097069629a3",
        "refinement_interpretation_Tm_refine_ec67bfa143a5dc60fb676f67549fda0d",
        "token_correspondence_Lib.ByteSequence.nat_from_intseq_le_.fuel_instrumented",
        "typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.index",
        "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
        "typing_Lib.ByteSequence.nat_from_intseq_le_",
        "typing_Lib.IntTypes.nat_to_uint", "typing_Lib.IntTypes.numbytes",
        "typing_Lib.IntTypes.uint_t", "typing_Lib.IntTypes.uint_v",
        "typing_Lib.RawIntTypes.uint_to_nat", "typing_Lib.Sequence.createi",
        "typing_Lib.Sequence.length", "typing_Lib.Sequence.sub",
        "typing_Tm_abs_c195bd9080359e043c42f5562b6d2df0",
        "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.SEC@tok",
        "typing_tok_Lib.IntTypes.U128@tok",
        "typing_tok_Lib.IntTypes.U16@tok", "typing_tok_Lib.IntTypes.U32@tok",
        "typing_tok_Lib.IntTypes.U64@tok", "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "77dccebd5bccec8b73659c1f8e9de138"
    ],
    [
      "Lib.ByteSequence.uints_from_bytes_le_nat_lemma_",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Lib.ByteSequence.uints_from_bytes_le",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.uint_t", "equation_Lib.Sequence.length",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_Prims.nat", "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_70597463dd221580f371f83615527f81",
        "refinement_interpretation_Tm_refine_b7c6ab0416aa19b9be0f0ab3d684c8cc",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Seq.Base.length",
        "typing_Lib.ByteSequence.uints_from_bytes_le",
        "typing_Lib.IntTypes.uint_t", "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "3f9db60211dee227f957e5522f6bba2d"
    ],
    [
      "Lib.ByteSequence.uints_from_bytes_le_nat_lemma_",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Tm_unit", "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Lib.ByteSequence.uints_from_bytes_le",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.uint_t", "equation_Lib.Sequence.length",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_50c622548b3c656fad3118cb8619b128",
        "refinement_interpretation_Tm_refine_70597463dd221580f371f83615527f81",
        "refinement_interpretation_Tm_refine_b7c6ab0416aa19b9be0f0ab3d684c8cc",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Seq.Base.length",
        "typing_Lib.ByteSequence.uints_from_bytes_le",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.numbytes",
        "typing_Lib.IntTypes.uint_t", "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "a00310b2beefb5363fb4ee4506575f6a"
    ],
    [
      "Lib.ByteSequence.uints_from_bytes_le_nat_lemma_",
      3,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.ByteSequence.nat_from_intseq_le_.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Lib.ByteSequence.nat_from_intseq_le_.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Lib.IntTypes_pretyping_877cb84f86c77989c5c1e5a978e57417",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_2803b9576ce146e96eed6f6dcb89fa99_3",
        "binder_x_4f5e6e575ca537d750ab5e22c0754aaa_0",
        "binder_x_54d357157606c62a5ef32fa80f038904_2",
        "binder_x_877cb84f86c77989c5c1e5a978e57417_1",
        "constructor_distinct_Lib.IntTypes.PUB",
        "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",
        "data_typing_intro_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U16@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Lib.ByteSequence.nat_from_bytes_le",
        "equation_Lib.ByteSequence.nat_from_intseq_le",
        "equation_Lib.ByteSequence.uints_from_bytes_le",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.byte_t",
        "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.pub_int_t",
        "equation_Lib.IntTypes.uint_t", "equation_Lib.Sequence.length",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_Prims.nat",
        "equation_with_fuel_Lib.ByteSequence.nat_from_intseq_le_.fuel_instrumented",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "fuel_guarded_inversion_Lib.IntTypes.secrecy_level",
        "function_token_typing_Lib.IntTypes.byte_t",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.slice_length",
        "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_values",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "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_28f14a1da5afe86697ce8584895fe979",
        "refinement_interpretation_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_559c261b1c3777929ea329abfe70ab33",
        "refinement_interpretation_Tm_refine_57683ab53ec5b7f6ea2dd6ddc8886f8f",
        "refinement_interpretation_Tm_refine_70597463dd221580f371f83615527f81",
        "refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_Tm_refine_af27ee4a225c1904de8f856aec47d813",
        "refinement_interpretation_Tm_refine_b7c6ab0416aa19b9be0f0ab3d684c8cc",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_cd046bc4a887ee7e1b05946e0bf5772b",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "token_correspondence_Lib.ByteSequence.nat_from_intseq_le_.fuel_instrumented",
        "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
        "typing_FStar.Seq.Base.slice",
        "typing_Lib.ByteSequence.uints_from_bytes_le",
        "typing_Lib.IntTypes.numbytes", "typing_Lib.IntTypes.uint_t",
        "typing_Lib.RawIntTypes.uint_to_nat", "typing_Lib.Sequence.length",
        "typing_tok_Lib.IntTypes.U8@tok", "well-founded-ordering-on-nat"
      ],
      0,
      "043992a41a91cbe55aaf299e63a06b47"
    ],
    [
      "Lib.ByteSequence.uints_from_bytes_le_nat_lemma_",
      4,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.uint_t", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.seq", "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_b7c6ab0416aa19b9be0f0ab3d684c8cc",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.uint_t",
        "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "f553fa5b210b9b4201d7d58e6648b8eb"
    ],
    [
      "Lib.ByteSequence.uints_from_bytes_le_nat_lemma_",
      5,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.uint_t", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.seq", "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_b7c6ab0416aa19b9be0f0ab3d684c8cc",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.uint_t",
        "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "126f318fa7795124110e22428f8fde42"
    ],
    [
      "Lib.ByteSequence.uints_from_bytes_le_nat_lemma",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Lib.ByteSequence.uints_from_bytes_le",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.uint_t", "equation_Lib.Sequence.length",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_Prims.nat", "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_70597463dd221580f371f83615527f81",
        "refinement_interpretation_Tm_refine_b7c6ab0416aa19b9be0f0ab3d684c8cc",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Seq.Base.length",
        "typing_Lib.ByteSequence.uints_from_bytes_le",
        "typing_Lib.IntTypes.uint_t", "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "617967522468b4f2c9f4159d8b6535b7"
    ],
    [
      "Lib.ByteSequence.uints_from_bytes_le_nat_lemma",
      2,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.numbytes", "equation_Prims.nat",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_70597463dd221580f371f83615527f81",
        "refinement_interpretation_Tm_refine_b7c6ab0416aa19b9be0f0ab3d684c8cc",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "8791fa1dc64a1902f9e2781f777939f0"
    ],
    [
      "Lib.ByteSequence.uints_from_bytes_le_nat_lemma",
      3,
      1,
      1,
      [
        "@query", "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Lib.ByteSequence.nat_from_bytes_le",
        "equation_Lib.ByteSequence.nat_from_intseq_le",
        "equation_Lib.ByteSequence.uints_from_bytes_le"
      ],
      0,
      "55ffafd3176e36f18379c5c2814d1f45"
    ],
    [
      "Lib.ByteSequence.index_uints_to_bytes_le",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Tm_unit", "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_Lib.IntTypes.pow2_values",
        "primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0a15ef129892b40d14f4cb02497870b0",
        "refinement_interpretation_Tm_refine_0a3deab6de0ff2f22cf53649d1f6ace2",
        "refinement_interpretation_Tm_refine_0f19326361ea09782672194cb0d9c57c",
        "refinement_interpretation_Tm_refine_39fd33cf414d74e3361a179fa5bc2dc3",
        "refinement_interpretation_Tm_refine_5c4d302c36cf56e82489594831c334e9",
        "refinement_interpretation_Tm_refine_70597463dd221580f371f83615527f81",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d38a29fd3b1756d1b5484775ac696626",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_df037df1ff5c9732e1553031fc7dc18c",
        "typing_Lib.ByteSequence.nat_to_intseq_le",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.numbytes",
        "typing_Lib.IntTypes.uint_v"
      ],
      0,
      "279791523ddb8281e1b2189258e608a1"
    ],
    [
      "Lib.ByteSequence.index_uints_to_bytes_le",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Tm_unit", "equality_tok_Lib.IntTypes.U1@tok",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_70597463dd221580f371f83615527f81",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d38a29fd3b1756d1b5484775ac696626",
        "typing_Lib.IntTypes.numbytes"
      ],
      0,
      "64a32caa9f92ac7f231e3447dc04912e"
    ],
    [
      "Lib.ByteSequence.index_uints_to_bytes_le",
      3,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Tm_unit", "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_Lib.ByteSequence.uint_to_bytes_le",
        "equation_Lib.ByteSequence.uints_to_bytes_le",
        "equation_Lib.ByteSequence.uints_to_bytes_le_inner",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.Sequence.length", "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_Lib.IntTypes.pow2_values",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_Tm_refine_0a15ef129892b40d14f4cb02497870b0",
        "refinement_interpretation_Tm_refine_70597463dd221580f371f83615527f81",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d38a29fd3b1756d1b5484775ac696626",
        "typing_Lib.IntTypes.bits", "unit_typing"
      ],
      0,
      "62638a3f9afa20a50cdba69fa3d95055"
    ],
    [
      "Lib.ByteSequence.modulo_pow2_prop",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.nat", "equation_Prims.pos",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b"
      ],
      0,
      "d5ac554f891d253820e2c0093cc6e56b"
    ],
    [
      "Lib.ByteSequence.modulo_pow2_prop",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.nat", "equation_Prims.pos",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b"
      ],
      0,
      "aff474c1973cbb1a3580fbb9f04fa59e"
    ],
    [
      "Lib.ByteSequence.index_nat_to_intseq_to_bytes_le",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Tm_unit", "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.Sequence.length", "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_Lib.IntTypes.pow2_values",
        "primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0a15ef129892b40d14f4cb02497870b0",
        "refinement_interpretation_Tm_refine_0a3deab6de0ff2f22cf53649d1f6ace2",
        "refinement_interpretation_Tm_refine_0f19326361ea09782672194cb0d9c57c",
        "refinement_interpretation_Tm_refine_39fd33cf414d74e3361a179fa5bc2dc3",
        "refinement_interpretation_Tm_refine_5c4d302c36cf56e82489594831c334e9",
        "refinement_interpretation_Tm_refine_70597463dd221580f371f83615527f81",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_b0533f4a80c419d8eb70a3dd7493adfe",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d38a29fd3b1756d1b5484775ac696626",
        "refinement_interpretation_Tm_refine_df037df1ff5c9732e1553031fc7dc18c",
        "typing_Lib.ByteSequence.nat_to_intseq_le",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.numbytes",
        "typing_Lib.IntTypes.uint_v"
      ],
      0,
      "e3712112295c9bcb7a9cbc60ec41ee61"
    ],
    [
      "Lib.ByteSequence.index_nat_to_intseq_to_bytes_le",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Tm_unit", "equality_tok_Lib.IntTypes.U1@tok",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_70597463dd221580f371f83615527f81",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d38a29fd3b1756d1b5484775ac696626",
        "typing_Lib.IntTypes.numbytes"
      ],
      0,
      "94e2bead01ee6a1215580660d504cff8"
    ],
    [
      "Lib.ByteSequence.index_nat_to_intseq_to_bytes_le",
      3,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Tm_unit", "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Lib.ByteSequence.nat_to_bytes_le",
        "equation_Lib.ByteSequence.nat_to_intseq_le",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.uint_t", "equation_Lib.Sequence.length",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq",
        "equation_Prims.nat", "equation_Prims.pos",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_Lib.IntTypes.pow2_values",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Division",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_08a324b6ced3cb3fa1e03a383a218939",
        "refinement_interpretation_Tm_refine_0a15ef129892b40d14f4cb02497870b0",
        "refinement_interpretation_Tm_refine_0a3deab6de0ff2f22cf53649d1f6ace2",
        "refinement_interpretation_Tm_refine_0f19326361ea09782672194cb0d9c57c",
        "refinement_interpretation_Tm_refine_39fd33cf414d74e3361a179fa5bc2dc3",
        "refinement_interpretation_Tm_refine_5c4d302c36cf56e82489594831c334e9",
        "refinement_interpretation_Tm_refine_70597463dd221580f371f83615527f81",
        "refinement_interpretation_Tm_refine_7c0cec89d4816950a0b97037fb573d60",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_b0533f4a80c419d8eb70a3dd7493adfe",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d38a29fd3b1756d1b5484775ac696626",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_df037df1ff5c9732e1553031fc7dc18c",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "typing_Lib.ByteSequence.nat_to_intseq_le",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.numbytes",
        "typing_Lib.IntTypes.uint_v", "typing_Prims.pow2"
      ],
      0,
      "c4bc2a7d8f9e83a6a0301d7b84bbe010"
    ],
    [
      "Lib.ByteSequence.uints_to_bytes_le_nat_lemma",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.numbytes", "equation_Lib.Sequence.length",
        "equation_Prims.nat", "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_39fd33cf414d74e3361a179fa5bc2dc3",
        "refinement_interpretation_Tm_refine_70597463dd221580f371f83615527f81",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d38a29fd3b1756d1b5484775ac696626"
      ],
      0,
      "23f68af1a3431c11f0e16614ef217e98"
    ],
    [
      "Lib.ByteSequence.uints_to_bytes_le_nat_lemma",
      2,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equality_tok_Lib.IntTypes.U1@tok", "equation_Lib.IntTypes.bits",
        "equation_Prims.nat", "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_70597463dd221580f371f83615527f81",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d38a29fd3b1756d1b5484775ac696626"
      ],
      0,
      "6636d9e72591f1b2479d3f0465030d9c"
    ],
    [
      "Lib.ByteSequence.uints_to_bytes_le_nat_lemma",
      3,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Tm_unit", "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Lib.ByteSequence.nat_to_bytes_le",
        "equation_Lib.ByteSequence.nat_to_intseq_le",
        "equation_Lib.ByteSequence.uints_to_bytes_le",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.uint_t", "equation_Lib.Sequence.length",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Division",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0a15ef129892b40d14f4cb02497870b0",
        "refinement_interpretation_Tm_refine_0a3deab6de0ff2f22cf53649d1f6ace2",
        "refinement_interpretation_Tm_refine_0f19326361ea09782672194cb0d9c57c",
        "refinement_interpretation_Tm_refine_39fd33cf414d74e3361a179fa5bc2dc3",
        "refinement_interpretation_Tm_refine_5a9b07a98aac9ef86cf806048f3fefbd",
        "refinement_interpretation_Tm_refine_5c4d302c36cf56e82489594831c334e9",
        "refinement_interpretation_Tm_refine_70597463dd221580f371f83615527f81",
        "refinement_interpretation_Tm_refine_81aa92b7573e33eeaa7a335b747501de",
        "refinement_interpretation_Tm_refine_9085ef699cbbd0c208799b1de61f86f0",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_b0533f4a80c419d8eb70a3dd7493adfe",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d38a29fd3b1756d1b5484775ac696626",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_df037df1ff5c9732e1553031fc7dc18c",
        "typing_FStar.Seq.Base.length",
        "typing_Lib.ByteSequence.nat_to_bytes_le",
        "typing_Lib.ByteSequence.nat_to_intseq_le",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.numbytes",
        "typing_Lib.IntTypes.uint_t", "typing_Lib.IntTypes.uint_v",
        "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "63918c6391c7c788cb330fa596a7206b"
    ],
    [
      "Lib.ByteSequence.nat_from_intseq_le_inj",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.uint_t",
        "equation_Prims.nat", "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Lib.IntTypes.uint_t", "typing_Lib.Sequence.length"
      ],
      0,
      "2030e02b8420d26a99114bc853aae726"
    ],
    [
      "Lib.ByteSequence.nat_from_intseq_le_inj",
      2,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.uint_t",
        "equation_Prims.nat", "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Lib.IntTypes.uint_t", "typing_Lib.Sequence.length"
      ],
      0,
      "bb6c4748ad6252b27523df9ce22a1b9a"
    ],
    [
      "Lib.ByteSequence.nat_from_intseq_le_inj",
      3,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.ByteSequence.nat_from_intseq_le_.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Lib.ByteSequence.nat_from_intseq_le_.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_40562ba8f0b1c89794fd620c41172c8e_2",
        "binder_x_40562ba8f0b1c89794fd620c41172c8e_3",
        "binder_x_877cb84f86c77989c5c1e5a978e57417_1",
        "binder_x_d450aafb6f125538d0e96425faddef55_0",
        "constructor_distinct_Lib.IntTypes.PUB",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U16@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Prims.LexTop@tok",
        "equation_FStar.Pervasives.Native.fst",
        "equation_FStar.Pervasives.Native.snd",
        "equation_FStar.Seq.Properties.split",
        "equation_Lib.ByteSequence.nat_from_intseq_le",
        "equation_Lib.IntTypes.bit_t", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.pub_uint128",
        "equation_Lib.IntTypes.pub_uint16",
        "equation_Lib.IntTypes.pub_uint64", "equation_Lib.IntTypes.size_t",
        "equation_Lib.IntTypes.uint1", "equation_Lib.IntTypes.uint128",
        "equation_Lib.IntTypes.uint16", "equation_Lib.IntTypes.uint32",
        "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.uint8",
        "equation_Lib.IntTypes.uint_t", "equation_Lib.Sequence.length",
        "equation_Lib.Sequence.seq", "equation_Prims.nat",
        "equation_with_fuel_Lib.ByteSequence.nat_from_intseq_le_.fuel_instrumented",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "fuel_guarded_inversion_Lib.IntTypes.secrecy_level",
        "function_token_typing_Lib.IntTypes.bit_t",
        "function_token_typing_Lib.IntTypes.byte_t",
        "function_token_typing_Lib.IntTypes.pub_uint128",
        "function_token_typing_Lib.IntTypes.pub_uint16",
        "function_token_typing_Lib.IntTypes.pub_uint64",
        "function_token_typing_Lib.IntTypes.size_t",
        "function_token_typing_Lib.IntTypes.uint1",
        "function_token_typing_Lib.IntTypes.uint128",
        "function_token_typing_Lib.IntTypes.uint16",
        "function_token_typing_Lib.IntTypes.uint32",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Lib.IntTypes.uint8",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "lemma_FStar.Seq.Base.lemma_index_app2",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_Tm_refine_03127b5d59ee3055620018693b4264e8",
        "refinement_interpretation_Tm_refine_3421154546287b0f0c012dd3d63b4945",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_57683ab53ec5b7f6ea2dd6ddc8886f8f",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_Tm_refine_af27ee4a225c1904de8f856aec47d813",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "token_correspondence_Lib.ByteSequence.nat_from_intseq_le_.fuel_instrumented",
        "typing_FStar.Pervasives.Native.fst", "typing_FStar.Seq.Base.index",
        "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Properties.split",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.uint_t",
        "typing_Lib.IntTypes.uint_v", "typing_Lib.RawIntTypes.uint_to_nat",
        "typing_Lib.Sequence.length", "typing_Lib.Sequence.seq",
        "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.SEC@tok",
        "typing_tok_Lib.IntTypes.U128@tok",
        "typing_tok_Lib.IntTypes.U16@tok", "typing_tok_Lib.IntTypes.U1@tok",
        "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok",
        "typing_tok_Lib.IntTypes.U8@tok", "well-founded-ordering-on-nat"
      ],
      0,
      "7bf196400976e790c580f8086f8bf479"
    ]
  ]
]

Showing with 0 additions and 0 deletions (0 / 0 diffs computed)

Computing file changes ...