[
  "Ý(ô(caTðžOe\u0018žßÜÀ",
  [
    [
      "Lib.NTuple.ntuple_",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_fbb855052fbcadaa14f24d60952144ef_1",
        "equation_Lib.NTuple.flen", "equation_Prims.pos",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_Equality",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "well-founded-ordering-on-nat"
      ],
      0,
      "57c9d7cf7f2681e954f0e1d4b2a1822a"
    ],
    [
      "Lib.NTuple.fst_",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.NTuple.ntuple_.fuel_instrumented",
        "@fuel_irrelevance_Lib.NTuple.ntuple_.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Lib.NTuple.flen", "equation_Prims.pos",
        "equation_with_fuel_Lib.NTuple.ntuple_.fuel_instrumented",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "primitive_Prims.op_Equality",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "6e44c1c49743401874febe87b0b63e62"
    ],
    [
      "Lib.NTuple.fst",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.NTuple.ntuple_.fuel_instrumented",
        "@fuel_irrelevance_Lib.NTuple.ntuple_.fuel_instrumented", "@query",
        "equation_Lib.NTuple.flen", "equation_Lib.NTuple.ntuple",
        "equation_Prims.pos",
        "equation_with_fuel_Lib.NTuple.ntuple_.fuel_instrumented",
        "int_inversion", "primitive_Prims.op_Subtraction",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "2221f34b93f06e8b71fb8f933e46cf53"
    ],
    [
      "Lib.NTuple.rest_",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.NTuple.ntuple_.fuel_instrumented",
        "@fuel_irrelevance_Lib.NTuple.ntuple_.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32", "equation_Lib.NTuple.flen",
        "equation_Prims.pos",
        "equation_with_fuel_Lib.NTuple.ntuple_.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "primitive_Prims.op_Equality",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_1b4848855b5d2f9c3d08284de9c11606",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "14eb7d12c79cdf85c7ac5a6a98eea829"
    ],
    [
      "Lib.NTuple.rest",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Lib.NTuple.flen",
        "equation_Prims.pos", "int_inversion",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_1b4848855b5d2f9c3d08284de9c11606",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "0a5f02419308b976c29bf7fb36917dfb"
    ],
    [
      "Lib.NTuple.rest",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.NTuple.ntuple_.fuel_instrumented",
        "@fuel_irrelevance_Lib.NTuple.ntuple_.fuel_instrumented", "@query",
        "equation_Lib.NTuple.flen", "equation_Lib.NTuple.ntuple",
        "equation_Prims.pos",
        "equation_with_fuel_Lib.NTuple.ntuple_.fuel_instrumented",
        "int_inversion", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_1b4848855b5d2f9c3d08284de9c11606",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "506ff21abccf85550338298b7780e462"
    ],
    [
      "Lib.NTuple.index_",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "binder_x_d69b96059acb340a6b564b4e425825b0_3",
        "binder_x_fbb855052fbcadaa14f24d60952144ef_1",
        "equation_Lib.NTuple.flen", "equation_Prims.nat",
        "equation_Prims.pos", "int_inversion", "int_typing",
        "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7063937694e59f1cde6b410ab29a9ecb",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "well-founded-ordering-on-nat"
      ],
      0,
      "fe02a03c9bc2889fafef4b5353776687"
    ],
    [
      "Lib.NTuple.index_fst_lemma",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Lib.NTuple.flen",
        "equation_Prims.pos",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "e81693086e4ab07396d691e478ca1282"
    ],
    [
      "Lib.NTuple.index_fst_lemma",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Lib.NTuple.index",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Equality"
      ],
      0,
      "82087b22b64382b1c0dcd9fdef9a0c67"
    ],
    [
      "Lib.NTuple.createi_",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Lib.NTuple.flen",
        "equation_Prims.nat", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_9ca104371a81dfac8fe41988e6e4e26d"
      ],
      0,
      "e54b6e8bac68ffb7451d40a279b3271c"
    ],
    [
      "Lib.NTuple.createi_",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.NTuple.ntuple_.fuel_instrumented",
        "@fuel_irrelevance_Lib.NTuple.ntuple_.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_156a1b97546f08fb754f8eed2589f409_2",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
        "binder_x_fe28d8bcde588226b4e538b35321de05_0",
        "constructor_distinct_Lib.IntTypes.U32", "equation_Lib.NTuple.flen",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_Lib.NTuple.ntuple_.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_b5aafe96635d3a096daf4019226e106d",
        "well-founded-ordering-on-nat"
      ],
      0,
      "4879893b2e96dd1f927bb5ad1282089a"
    ],
    [
      "Lib.NTuple.createi",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.NTuple.ntuple_.fuel_instrumented",
        "@fuel_irrelevance_Lib.NTuple.ntuple_.fuel_instrumented", "@query",
        "equation_Lib.NTuple.flen", "equation_Lib.NTuple.ntuple",
        "equation_Prims.pos",
        "equation_with_fuel_Lib.NTuple.ntuple_.fuel_instrumented",
        "int_inversion", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "a858fb62e262bb37d52a9e70bd66e399"
    ],
    [
      "Lib.NTuple.gcreatei_",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Lib.NTuple.flen",
        "equation_Prims.nat", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_9ca104371a81dfac8fe41988e6e4e26d"
      ],
      0,
      "fc21909029cb357bdc50da36c39491eb"
    ],
    [
      "Lib.NTuple.gcreatei_",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.NTuple.ntuple_.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Lib.NTuple.ntuple_.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_156a1b97546f08fb754f8eed2589f409_2",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
        "binder_x_fe28d8bcde588226b4e538b35321de05_0",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.NTuple.flen",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_Lib.NTuple.ntuple_.fuel_instrumented",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_b5aafe96635d3a096daf4019226e106d",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok",
        "well-founded-ordering-on-nat"
      ],
      0,
      "dbd365e6b96886cf793b4f12be02fef6"
    ],
    [
      "Lib.NTuple.gcreatei",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.NTuple.ntuple_.fuel_instrumented",
        "@fuel_irrelevance_Lib.NTuple.ntuple_.fuel_instrumented", "@query",
        "equation_Lib.NTuple.flen", "equation_Lib.NTuple.ntuple",
        "equation_Prims.pos",
        "equation_with_fuel_Lib.NTuple.ntuple_.fuel_instrumented",
        "int_inversion", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "30608029d0d6e38057cc4f653fde2967"
    ],
    [
      "Lib.NTuple.createi_lemma_",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.NTuple.ntuple_.fuel_instrumented",
        "@fuel_irrelevance_Lib.NTuple.ntuple_.fuel_instrumented", "@query",
        "equation_Lib.NTuple.flen", "equation_Lib.NTuple.ntuple",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_Lib.NTuple.ntuple_.fuel_instrumented",
        "int_inversion", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2fd235719e69f221af23c4e1176116e9",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_9ca104371a81dfac8fe41988e6e4e26d",
        "typing_Lib.NTuple.createi_"
      ],
      0,
      "252922e6c9252870f6703c5d4676516c"
    ],
    [
      "Lib.NTuple.createi_lemma_",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.NTuple.createi_.fuel_instrumented",
        "@fuel_correspondence_Lib.NTuple.index_.fuel_instrumented",
        "@fuel_correspondence_Lib.NTuple.ntuple_.fuel_instrumented",
        "@fuel_irrelevance_Lib.NTuple.createi_.fuel_instrumented",
        "@fuel_irrelevance_Lib.NTuple.index_.fuel_instrumented",
        "@fuel_irrelevance_Lib.NTuple.ntuple_.fuel_instrumented", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "Lib.NTuple_interpretation_Tm_arrow_3728a9ddf7632625a91f80bf2c9c7bc4",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_156a1b97546f08fb754f8eed2589f409_2",
        "binder_x_27b50b5e4daddbeed9e0814eb3efd017_4",
        "binder_x_33dc0da9c28b771ecad6a3bd40dbdda6_3",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
        "binder_x_fe28d8bcde588226b4e538b35321de05_0",
        "constructor_distinct_Lib.IntTypes.U32",
        "equation_FStar.Pervasives.Native.fst", "equation_Lib.NTuple.flen",
        "equation_Lib.NTuple.fst", "equation_Lib.NTuple.index",
        "equation_Lib.NTuple.ntuple", "equation_Lib.NTuple.rest",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_Lib.NTuple.createi_.fuel_instrumented",
        "equation_with_fuel_Lib.NTuple.index_.fuel_instrumented",
        "equation_with_fuel_Lib.NTuple.ntuple_.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Equality", "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",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_Tm_refine_1b4848855b5d2f9c3d08284de9c11606",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_84db9ea663ffd81ac8f41b8b66b0675e",
        "refinement_interpretation_Tm_refine_88108c16196cacd707cf70ba583939f2",
        "refinement_interpretation_Tm_refine_9ca104371a81dfac8fe41988e6e4e26d",
        "refinement_interpretation_Tm_refine_9f7d4edb183678e09b7842d89903f393",
        "refinement_interpretation_Tm_refine_b5aafe96635d3a096daf4019226e106d",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "typing_Lib.NTuple.createi_", "typing_Lib.NTuple.rest",
        "well-founded-ordering-on-nat"
      ],
      0,
      "5bf7d4c9191875646720226ca00e03fd"
    ],
    [
      "Lib.NTuple.createi_lemma",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.NTuple.createi_.fuel_instrumented",
        "@fuel_irrelevance_Lib.NTuple.createi_.fuel_instrumented", "@query",
        "equation_Lib.NTuple.createi", "equation_Lib.NTuple.flen",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_Lib.NTuple.createi_.fuel_instrumented",
        "int_inversion", "int_typing", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_9ca104371a81dfac8fe41988e6e4e26d",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "c04207a7dc16fbea2e5c693ce01846ac"
    ],
    [
      "Lib.NTuple.gcreatei_lemma_",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.NTuple.ntuple_.fuel_instrumented",
        "@fuel_irrelevance_Lib.NTuple.ntuple_.fuel_instrumented", "@query",
        "equation_Lib.NTuple.flen", "equation_Lib.NTuple.ntuple",
        "equation_Prims.nat",
        "equation_with_fuel_Lib.NTuple.ntuple_.fuel_instrumented",
        "int_inversion", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_3ebaf485c5f76acea28f2ab85eb73296",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_9ca104371a81dfac8fe41988e6e4e26d"
      ],
      0,
      "aad20b6e53d1b9dd6064cdc92db93196"
    ],
    [
      "Lib.NTuple.gcreatei_lemma_",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.NTuple.gcreatei_.fuel_instrumented",
        "@fuel_correspondence_Lib.NTuple.index_.fuel_instrumented",
        "@fuel_correspondence_Lib.NTuple.ntuple_.fuel_instrumented",
        "@fuel_irrelevance_Lib.NTuple.gcreatei_.fuel_instrumented",
        "@fuel_irrelevance_Lib.NTuple.index_.fuel_instrumented",
        "@fuel_irrelevance_Lib.NTuple.ntuple_.fuel_instrumented", "@query",
        "FStar.Seq.Base_interpretation_Tm_ghost_arrow_b7c239afcc620812134a759b53cafcc7",
        "Lib.NTuple_interpretation_Tm_ghost_arrow_9e57584a66bdf0ee3f4c7658883c3b96",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_156a1b97546f08fb754f8eed2589f409_2",
        "binder_x_27b50b5e4daddbeed9e0814eb3efd017_4",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
        "binder_x_df53d41f08da5196a49daa53d409e75c_3",
        "binder_x_fe28d8bcde588226b4e538b35321de05_0",
        "constructor_distinct_Lib.IntTypes.U32",
        "equation_FStar.Pervasives.Native.fst", "equation_Lib.NTuple.flen",
        "equation_Lib.NTuple.fst", "equation_Lib.NTuple.index",
        "equation_Lib.NTuple.ntuple", "equation_Lib.NTuple.rest",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_Lib.NTuple.gcreatei_.fuel_instrumented",
        "equation_with_fuel_Lib.NTuple.index_.fuel_instrumented",
        "equation_with_fuel_Lib.NTuple.ntuple_.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Equality", "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",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_88108c16196cacd707cf70ba583939f2",
        "refinement_interpretation_Tm_refine_9ca104371a81dfac8fe41988e6e4e26d",
        "refinement_interpretation_Tm_refine_9f7d4edb183678e09b7842d89903f393",
        "refinement_interpretation_Tm_refine_b5aafe96635d3a096daf4019226e106d",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_e7e88d1a6e062ba9c44f207fd46481b6",
        "typing_Lib.NTuple.gcreatei_", "well-founded-ordering-on-nat"
      ],
      0,
      "7cd516cea8bcce15be8533175675b6cb"
    ],
    [
      "Lib.NTuple.gcreatei_lemma",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.NTuple.gcreatei_.fuel_instrumented",
        "@fuel_irrelevance_Lib.NTuple.gcreatei_.fuel_instrumented", "@query",
        "equation_Lib.NTuple.flen", "equation_Lib.NTuple.gcreatei",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_Lib.NTuple.gcreatei_.fuel_instrumented",
        "int_inversion", "int_typing", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_9ca104371a81dfac8fe41988e6e4e26d",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "8295219c45ef6cac20df312e1e95d7a6"
    ],
    [
      "Lib.NTuple.to_lseq",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "48b09f4a0652897229e1023659d3bb81"
    ],
    [
      "Lib.NTuple.to_lseq",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Lib.NTuple.flen",
        "equation_Prims.pos",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "1deae755c061246170372664680f7dac"
    ],
    [
      "Lib.NTuple.to_lseq_index",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Lib.NTuple.flen",
        "equation_Prims.pos",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "82a333e74a8c27ea2a86dd12ddb856f5"
    ],
    [
      "Lib.NTuple.to_lseq_index",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "Lib.NTuple_interpretation_Tm_arrow_9a512b92d777781e1ace3a482095bb7f",
        "equation_Lib.NTuple.flen", "equation_Lib.NTuple.index",
        "equation_Lib.NTuple.ntuple", "equation_Lib.NTuple.to_lseq",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_Prims.nat", "equation_Prims.pos",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "int_inversion",
        "interpretation_Tm_abs_17d8185ede3b800e3849779eb2fbbe28",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan",
        "refinement_interpretation_Tm_refine_087abc8d482eedf69ab741bb5d8bc42d",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_abbfe228c7a3d1ae1f16ed243e0e6a67",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Seq.Base.length", "typing_Lib.NTuple.to_lseq",
        "typing_Lib.Sequence.createi",
        "typing_Tm_abs_17d8185ede3b800e3849779eb2fbbe28"
      ],
      0,
      "8df92a4024103a361200bc295f20bc89"
    ],
    [
      "Lib.NTuple.from_lseq",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "b28f92ea2483efbdd027dfde54db2350"
    ],
    [
      "Lib.NTuple.from_lseq",
      2,
      1,
      0,
      [ "@query" ],
      0,
      "1030c095ef27f2e22751ae76f0efe0b4"
    ],
    [
      "Lib.NTuple.from_lseq",
      3,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Lib.NTuple.flen",
        "equation_Prims.pos",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "f38eb23424a0cc873cef7f8d765f17da"
    ],
    [
      "Lib.NTuple.create_lemma",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.NTuple.createi_.fuel_instrumented",
        "@fuel_irrelevance_Lib.NTuple.createi_.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Lib.NTuple.create", "equation_Lib.NTuple.flen",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_Lib.NTuple.createi_.fuel_instrumented",
        "equation_with_fuel_Lib.NTuple.ntuple_.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "interpretation_Tm_abs_a127535694cbf3a3fa90a1d3a6f1b4c6",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_9ca104371a81dfac8fe41988e6e4e26d",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "typing_Tm_abs_a127535694cbf3a3fa90a1d3a6f1b4c6"
      ],
      0,
      "3cdf8d203973f02769ff3dceaa39b00d"
    ],
    [
      "Lib.NTuple.concat_",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Lib.NTuple.flen",
        "equation_Lib.NTuple.max_ntuple_len", "equation_Prims.pos",
        "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_3b8c5de4db63a3869a2e3cb5d9404e1e",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "588d7b772dba9b50644eed50bc6404a2"
    ],
    [
      "Lib.NTuple.concat_",
      2,
      2,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.NTuple.ntuple_.fuel_instrumented",
        "@fuel_irrelevance_Lib.NTuple.ntuple_.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_b7a8d01cc3a972f4fb18817607079cbd_4",
        "binder_x_ba81283e49fb5c8f2ebaa603402735f3_2",
        "binder_x_f7626ecbd08e0d345fe8f2a7f31d85cc_3",
        "binder_x_fbb855052fbcadaa14f24d60952144ef_1",
        "binder_x_fe28d8bcde588226b4e538b35321de05_0",
        "constructor_distinct_Lib.IntTypes.U32",
        "data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok",
        "equation_Lib.NTuple.flen", "equation_Lib.NTuple.max_ntuple_len",
        "equation_Lib.NTuple.ntuple", "equation_Prims.pos",
        "equation_with_fuel_Lib.NTuple.ntuple_.fuel_instrumented",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_3b3aafd3fa76cf2d5bce6d14956b2be7",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_Lib.NTuple.ntuple", "well-founded-ordering-on-nat"
      ],
      0,
      "58d305cd99492246443780f06a1d4e07"
    ],
    [
      "Lib.NTuple.concat",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Lib.NTuple.flen",
        "equation_Prims.pos", "primitive_Prims.op_Addition",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_e462e220c28fc5966eaaa66bb715a454"
      ],
      0,
      "eb727a1f8ba73d7c32b4b61d55966443"
    ],
    [
      "Lib.NTuple.concat",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.NTuple.ntuple_.fuel_instrumented",
        "@fuel_irrelevance_Lib.NTuple.ntuple_.fuel_instrumented", "@query",
        "equation_Lib.NTuple.flen", "equation_Lib.NTuple.max_ntuple_len",
        "equation_Lib.NTuple.ntuple", "equation_Prims.pos",
        "equation_with_fuel_Lib.NTuple.ntuple_.fuel_instrumented",
        "int_typing", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_e462e220c28fc5966eaaa66bb715a454"
      ],
      0,
      "25bac4ec472eeafca0091f79de0ff4ad"
    ],
    [
      "Lib.NTuple.concat_lemma1",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "equation_Lib.NTuple.flen", "equation_Lib.NTuple.max_ntuple_len",
        "equation_Prims.l_and", "equation_Prims.pos",
        "equation_Prims.squash", "l_and-interp",
        "primitive_Prims.op_Addition", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "b85481877c5ca8277107d61ac2c1422d"
    ],
    [
      "Lib.NTuple.concat_lemma1",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "equation_Lib.NTuple.flen", "equation_Lib.NTuple.max_ntuple_len",
        "equation_Prims.l_and", "equation_Prims.pos",
        "equation_Prims.squash", "l_and-interp",
        "primitive_Prims.op_Addition", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "9fe398895229c93776f21150f7e8c6c1"
    ],
    [
      "Lib.NTuple.concat_lemma1",
      3,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.NTuple.concat_.fuel_instrumented",
        "@fuel_correspondence_Lib.NTuple.index_.fuel_instrumented",
        "@fuel_correspondence_Lib.NTuple.ntuple_.fuel_instrumented",
        "@fuel_irrelevance_Lib.NTuple.concat_.fuel_instrumented",
        "@fuel_irrelevance_Lib.NTuple.index_.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_57301b89fb599f814ef22f0e648c2e5e_4",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_5",
        "binder_x_f7626ecbd08e0d345fe8f2a7f31d85cc_3",
        "binder_x_fbb855052fbcadaa14f24d60952144ef_1",
        "binder_x_fbb855052fbcadaa14f24d60952144ef_2",
        "binder_x_fe28d8bcde588226b4e538b35321de05_0",
        "constructor_distinct_Lib.IntTypes.U32",
        "equation_FStar.Pervasives.Native.fst", "equation_Lib.NTuple.concat",
        "equation_Lib.NTuple.flen", "equation_Lib.NTuple.fst",
        "equation_Lib.NTuple.index", "equation_Lib.NTuple.max_ntuple_len",
        "equation_Lib.NTuple.ntuple", "equation_Lib.NTuple.rest",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_Lib.NTuple.concat_.fuel_instrumented",
        "equation_with_fuel_Lib.NTuple.index_.fuel_instrumented",
        "equation_with_fuel_Lib.NTuple.ntuple_.fuel_instrumented",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Equality", "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",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_Tm_refine_1b4848855b5d2f9c3d08284de9c11606",
        "refinement_interpretation_Tm_refine_3b8c5de4db63a3869a2e3cb5d9404e1e",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_e462e220c28fc5966eaaa66bb715a454",
        "refinement_interpretation_Tm_refine_ed71166b702c992a75cba3332c88ac48",
        "typing_Lib.NTuple.concat", "typing_Lib.NTuple.concat_",
        "typing_Lib.NTuple.rest", "well-founded-ordering-on-nat"
      ],
      0,
      "57882921ca7597d586673354bf70d837"
    ],
    [
      "Lib.NTuple.concat_lemma2",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "equation_Lib.NTuple.flen", "equation_Lib.NTuple.max_ntuple_len",
        "equation_Prims.l_and", "equation_Prims.nat", "equation_Prims.pos",
        "equation_Prims.squash", "int_inversion", "l_and-interp",
        "primitive_Prims.op_Addition",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "1bea2b7ace1f0fd41acafe26ad59e299"
    ],
    [
      "Lib.NTuple.concat_lemma2",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "equation_Lib.NTuple.flen", "equation_Lib.NTuple.max_ntuple_len",
        "equation_Prims.l_and", "equation_Prims.nat", "equation_Prims.pos",
        "equation_Prims.squash", "int_inversion", "l_and-interp",
        "primitive_Prims.op_Addition",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_b537921bfda76757dd414baea3fe5deb"
      ],
      0,
      "5238c655b29a5db0b6bf38cc5b769198"
    ],
    [
      "Lib.NTuple.concat_lemma2",
      3,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.NTuple.concat_.fuel_instrumented",
        "@fuel_correspondence_Lib.NTuple.index_.fuel_instrumented",
        "@fuel_correspondence_Lib.NTuple.ntuple_.fuel_instrumented",
        "@fuel_irrelevance_Lib.NTuple.concat_.fuel_instrumented",
        "@fuel_irrelevance_Lib.NTuple.index_.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_57301b89fb599f814ef22f0e648c2e5e_4",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_5",
        "binder_x_f7626ecbd08e0d345fe8f2a7f31d85cc_3",
        "binder_x_fbb855052fbcadaa14f24d60952144ef_1",
        "binder_x_fbb855052fbcadaa14f24d60952144ef_2",
        "binder_x_fe28d8bcde588226b4e538b35321de05_0",
        "constructor_distinct_Lib.IntTypes.U32",
        "equation_Lib.NTuple.concat", "equation_Lib.NTuple.flen",
        "equation_Lib.NTuple.index", "equation_Lib.NTuple.max_ntuple_len",
        "equation_Lib.NTuple.ntuple", "equation_Lib.NTuple.rest",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_Lib.NTuple.concat_.fuel_instrumented",
        "equation_with_fuel_Lib.NTuple.index_.fuel_instrumented",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_Tm_refine_1b4848855b5d2f9c3d08284de9c11606",
        "refinement_interpretation_Tm_refine_3b8c5de4db63a3869a2e3cb5d9404e1e",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_a54d75d577590c51a91662406a30d72c",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_e462e220c28fc5966eaaa66bb715a454",
        "typing_Lib.NTuple.concat", "typing_Lib.NTuple.ntuple",
        "typing_Lib.NTuple.rest", "unit_inversion", "unit_typing",
        "well-founded-ordering-on-nat"
      ],
      0,
      "3bffde82324bc7cacc152bac324a3114"
    ],
    [
      "Lib.NTuple.concat_lemma",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "equation_Lib.NTuple.flen", "equation_Prims.l_and",
        "equation_Prims.nat", "equation_Prims.pos", "equation_Prims.squash",
        "int_inversion", "l_and-interp", "primitive_Prims.op_Addition",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "921563a84c62461d4e7544836078bda5"
    ],
    [
      "Lib.NTuple.concat_lemma",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U32", "equation_Lib.NTuple.flen",
        "equation_Lib.NTuple.max_ntuple_len", "equation_Prims.nat",
        "equation_Prims.pos", "int_inversion", "primitive_Prims.op_LessThan",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "4c0d84471500d785206f0eab2d479b3a"
    ],
    [
      "Lib.NTuple.equal",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "b273e94e08fc39bd2f09de03727a63f0"
    ],
    [
      "Lib.NTuple.eq_intro",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "447ae8af3599452c0bff08de8d925dab"
    ],
    [
      "Lib.NTuple.eq_intro",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Lib.NTuple.equal",
        "refinement_interpretation_Tm_refine_15f0687264c581284bdf37108526e858",
        "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45"
      ],
      0,
      "ae26d6471689bbbdbe15f5f3e26fef3b"
    ],
    [
      "Lib.NTuple.eq_elim",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.NTuple.index_.fuel_instrumented",
        "@fuel_correspondence_Lib.NTuple.ntuple_.fuel_instrumented",
        "@fuel_irrelevance_Lib.NTuple.index_.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_f7626ecbd08e0d345fe8f2a7f31d85cc_2",
        "binder_x_f7626ecbd08e0d345fe8f2a7f31d85cc_3",
        "binder_x_fbb855052fbcadaa14f24d60952144ef_1",
        "binder_x_fe28d8bcde588226b4e538b35321de05_0", "bool_inversion",
        "bool_typing", "constructor_distinct_Lib.IntTypes.U32",
        "equation_FStar.Pervasives.Native.fst", "equation_Lib.NTuple.equal",
        "equation_Lib.NTuple.flen", "equation_Lib.NTuple.fst",
        "equation_Lib.NTuple.index", "equation_Lib.NTuple.ntuple",
        "equation_Lib.NTuple.rest", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_Lib.NTuple.index_.fuel_instrumented",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "l_quant_interp_3a06deea105979862ad6ffae4ca859bd",
        "l_quant_interp_5a3b389dbd613215cd13abee09799d4e",
        "l_quant_interp_c582feb9d2412a054180812ce25e15ca",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "primitive_Prims.op_Subtraction",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
        "refinement_interpretation_Tm_refine_2cef8ec656713d091f840418ac4f4354",
        "refinement_interpretation_Tm_refine_40f182140e36f5041d6a48ddb49f46c0",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_6e8d7cad2b446cae369b9d10ada5f37f",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "well-founded-ordering-on-nat"
      ],
      0,
      "891c0d982958cdf7cd3e1085026e14a0"
    ],
    [
      "Lib.NTuple.upd_",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.NTuple.ntuple_.fuel_instrumented",
        "@fuel_irrelevance_Lib.NTuple.ntuple_.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_6781041e5072f14a03af8b07643f1f30_4",
        "binder_x_d69b96059acb340a6b564b4e425825b0_3",
        "binder_x_f7626ecbd08e0d345fe8f2a7f31d85cc_2",
        "binder_x_fbb855052fbcadaa14f24d60952144ef_1",
        "binder_x_fe28d8bcde588226b4e538b35321de05_0",
        "constructor_distinct_Lib.IntTypes.U32", "equation_Lib.NTuple.flen",
        "equation_Lib.NTuple.ntuple", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_Lib.NTuple.ntuple_.fuel_instrumented",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_Equality",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7063937694e59f1cde6b410ab29a9ecb",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_Lib.NTuple.ntuple", "well-founded-ordering-on-nat"
      ],
      0,
      "6f9c6bd6b98c5ce8fa52da0027cfd7d3"
    ],
    [
      "Lib.NTuple.upd",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.NTuple.ntuple_.fuel_instrumented",
        "@fuel_irrelevance_Lib.NTuple.ntuple_.fuel_instrumented", "@query",
        "equation_Lib.NTuple.flen", "equation_Lib.NTuple.ntuple",
        "equation_Prims.pos",
        "equation_with_fuel_Lib.NTuple.ntuple_.fuel_instrumented",
        "int_inversion", "primitive_Prims.op_Subtraction",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_Lib.NTuple.upd_"
      ],
      0,
      "17c59e77f299d76a1568c51577d85527"
    ],
    [
      "Lib.NTuple.upd_lemma",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "77a8aca4bc7058f767b519bcf77b850e"
    ],
    [
      "Lib.NTuple.upd_lemma",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "9baf94f5dbf238c22ac8fc2d556e744a"
    ],
    [
      "Lib.NTuple.upd_lemma",
      3,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.NTuple.index_.fuel_instrumented",
        "@fuel_correspondence_Lib.NTuple.ntuple_.fuel_instrumented",
        "@fuel_correspondence_Lib.NTuple.upd_.fuel_instrumented",
        "@fuel_irrelevance_Lib.NTuple.index_.fuel_instrumented",
        "@fuel_irrelevance_Lib.NTuple.ntuple_.fuel_instrumented",
        "@fuel_irrelevance_Lib.NTuple.upd_.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_6781041e5072f14a03af8b07643f1f30_4",
        "binder_x_d69b96059acb340a6b564b4e425825b0_3",
        "binder_x_d69b96059acb340a6b564b4e425825b0_5",
        "binder_x_f7626ecbd08e0d345fe8f2a7f31d85cc_2",
        "binder_x_fbb855052fbcadaa14f24d60952144ef_1",
        "binder_x_fe28d8bcde588226b4e538b35321de05_0",
        "constructor_distinct_Lib.IntTypes.U32",
        "equation_FStar.Pervasives.Native.fst", "equation_Lib.NTuple.flen",
        "equation_Lib.NTuple.fst", "equation_Lib.NTuple.index",
        "equation_Lib.NTuple.ntuple", "equation_Lib.NTuple.rest",
        "equation_Lib.NTuple.upd", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_Lib.NTuple.index_.fuel_instrumented",
        "equation_with_fuel_Lib.NTuple.ntuple_.fuel_instrumented",
        "equation_with_fuel_Lib.NTuple.upd_.fuel_instrumented",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_Lib.NTuple.index_fst_lemma",
        "primitive_Prims.op_Equality", "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",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7063937694e59f1cde6b410ab29a9ecb",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_e1383d9af8a6e5985fe40f820e201cb9",
        "refinement_interpretation_Tm_refine_f45c18673f4ab3876543431399fb07ea",
        "typing_Lib.NTuple.upd_", "unit_inversion", "unit_typing",
        "well-founded-ordering-on-nat"
      ],
      0,
      "e68841efb7124f6050efea83ec845688"
    ],
    [
      "Lib.NTuple.sub",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_Addition",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_285de3f46ec1a5e86f45b940cbcd115e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "2b3e59914dffcc5fe70b7669e8fd4e31"
    ],
    [
      "Lib.NTuple.index_sub_lemma",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_Addition",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_285de3f46ec1a5e86f45b940cbcd115e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "a52075ca7d7919512729ea7eb60ee477"
    ],
    [
      "Lib.NTuple.index_sub_lemma",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Lib.NTuple.createi",
        "equation_Lib.NTuple.flen", "equation_Lib.NTuple.ntuple",
        "equation_Lib.NTuple.sub", "equation_Prims.nat",
        "equation_Prims.pos",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "int_inversion",
        "interpretation_Tm_abs_ad19c0e54db9cdc4530cbc1b0e2801d9",
        "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_285de3f46ec1a5e86f45b940cbcd115e",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "8164322c3d7bc69b2c52c206370724d7"
    ],
    [
      "Lib.NTuple.slice",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Lib.NTuple.flen",
        "equation_Prims.nat", "equation_Prims.pos", "int_inversion",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_c10564e01d388b0672bda67fa15aaa2d"
      ],
      0,
      "c1088681aa938c0d9940da7788332822"
    ],
    [
      "Lib.NTuple.update_sub",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_Addition",
        "primitive_Prims.op_BarBar", "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "6d82ffe7db9f065ca476da5ad5d12c60"
    ],
    [
      "Lib.NTuple.index_update_sub_lemma",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_Addition",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_285de3f46ec1a5e86f45b940cbcd115e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "b49221fa56babee6b1a16cdcd4f54be9"
    ],
    [
      "Lib.NTuple.index_update_sub_lemma",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.NTuple.createi",
        "equation_Lib.NTuple.flen", "equation_Lib.NTuple.update_sub",
        "equation_Prims.nat", "equation_Prims.pos", "int_inversion",
        "interpretation_Tm_abs_0885a111cf88fd506709c73549b218f7",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_BarBar", "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_285de3f46ec1a5e86f45b940cbcd115e",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "a812607e3dbaf718694f882957941fd3"
    ],
    [
      "Lib.NTuple.update_slice",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Lib.NTuple.flen",
        "equation_Prims.nat", "equation_Prims.pos", "int_inversion",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_c10564e01d388b0672bda67fa15aaa2d"
      ],
      0,
      "807351e70d83c38bcb6aeed56b3c515e"
    ],
    [
      "Lib.NTuple.update_slice",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Lib.NTuple.flen",
        "equation_Prims.nat", "int_inversion", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c10564e01d388b0672bda67fa15aaa2d"
      ],
      0,
      "04ebab428b7e40fa291817d4a71bf3c9"
    ],
    [
      "Lib.NTuple.index_mapi_lemma",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Lib.NTuple.createi",
        "equation_Lib.NTuple.flen", "equation_Lib.NTuple.mapi",
        "equation_Prims.pos", "int_inversion",
        "interpretation_Tm_abs_ac6bca86da8101fd75dc2f706669dc8b",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "6dcf81fd4616ee490d878dd96805946f"
    ],
    [
      "Lib.NTuple.index_gmapi_lemma",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Lib.NTuple.flen",
        "equation_Lib.NTuple.gcreatei", "equation_Lib.NTuple.gmapi",
        "equation_Prims.pos", "int_inversion",
        "interpretation_Tm_abs_cba29e00866c21bfc3b9f30c40e4717d",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "1f82871298258b54f06ce53af9eb05ca"
    ],
    [
      "Lib.NTuple.index_map_lemma",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Lib.NTuple.createi",
        "equation_Lib.NTuple.flen", "equation_Lib.NTuple.map",
        "equation_Prims.pos", "int_inversion",
        "interpretation_Tm_abs_d26fe7e0aa18098e3c68cc3c597022b3",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "a36bd208c4b5c83bbcbd793697e37800"
    ],
    [
      "Lib.NTuple.index_gmap_lemma",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Lib.NTuple.flen",
        "equation_Lib.NTuple.gcreatei", "equation_Lib.NTuple.gmap",
        "equation_Prims.pos", "int_inversion",
        "interpretation_Tm_abs_b2279aa007c349caedd858f54f950e42",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "48268ee79579df1c49189f6d6218bee8"
    ],
    [
      "Lib.NTuple.index_map2i_lemma",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Lib.NTuple.createi",
        "equation_Lib.NTuple.flen", "equation_Lib.NTuple.map2i",
        "equation_Prims.pos", "int_inversion",
        "interpretation_Tm_abs_f609f69c9ff1fb205063d963b99912f7",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "84f21f8fef93d87d4dcb58d54eac7964"
    ],
    [
      "Lib.NTuple.index_map2_lemma",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Lib.NTuple.createi",
        "equation_Lib.NTuple.flen", "equation_Lib.NTuple.map2",
        "equation_Prims.pos", "int_inversion",
        "interpretation_Tm_abs_ec2ac7fef84ab3ff322ed45cf47dc30c",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "518d5142d8a94f1141cb64c6acf2bd04"
    ],
    [
      "Lib.NTuple.ntup1",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Lib.NTuple.flen", "equation_Lib.NTuple.ntuple",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Equality",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_bded595d5c675d20923ebf7eee58cd50"
      ],
      0,
      "48d932b0f6d994e579588e0d6089b86e"
    ],
    [
      "Lib.NTuple.ntup1_lemma",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_bded595d5c675d20923ebf7eee58cd50"
      ],
      0,
      "9f87d0d181efb101af75865e3c6febd1"
    ],
    [
      "Lib.NTuple.ntup1_lemma",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Lib.NTuple.flen", "equation_Lib.NTuple.fst",
        "equation_Lib.NTuple.index", "equation_Lib.NTuple.ntup1",
        "equation_Lib.NTuple.ntuple",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Equality",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_bded595d5c675d20923ebf7eee58cd50"
      ],
      0,
      "bb05560e8aefb8549f18318f931e48b5"
    ],
    [
      "Lib.NTuple.tup1",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Lib.NTuple.flen",
        "equation_Lib.NTuple.ntuple", "primitive_Prims.op_Equality",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_bded595d5c675d20923ebf7eee58cd50"
      ],
      0,
      "7aac5b9d37b29205c11e81bf8c0b4cdd"
    ],
    [
      "Lib.NTuple.tup1_lemma",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_bded595d5c675d20923ebf7eee58cd50"
      ],
      0,
      "43575435ec3bada139eef60beacc1351"
    ],
    [
      "Lib.NTuple.tup1_lemma",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Lib.NTuple.flen", "equation_Lib.NTuple.fst",
        "equation_Lib.NTuple.index", "equation_Lib.NTuple.tup1",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Equality",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_bded595d5c675d20923ebf7eee58cd50"
      ],
      0,
      "7c2d9d3c8df800e1bd6728d1cfbace87"
    ],
    [
      "Lib.NTuple.ntup4",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32", "equation_Lib.NTuple.flen",
        "equation_Lib.NTuple.ntuple",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_528b876405e78507cc8ed31848385919"
      ],
      0,
      "70dc17c3af954d578c9dc29fa988d324"
    ],
    [
      "Lib.NTuple.ntup4_lemma",
      1,
      4,
      0,
      [
        "@MaxIFuel_assumption", "@query", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_528b876405e78507cc8ed31848385919"
      ],
      0,
      "3965c40d0e2f0942676c71a7d507b608"
    ],
    [
      "Lib.NTuple.ntup4_lemma",
      2,
      4,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.NTuple.index_.fuel_instrumented",
        "@fuel_correspondence_Lib.NTuple.ntuple_.fuel_instrumented",
        "@fuel_irrelevance_Lib.NTuple.ntuple_.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_FStar.Pervasives.Native.fst", "equation_Lib.IntTypes.bits",
        "equation_Lib.NTuple.flen", "equation_Lib.NTuple.fst",
        "equation_Lib.NTuple.index", "equation_Lib.NTuple.ntup4",
        "equation_Lib.NTuple.ntuple", "equation_Lib.NTuple.rest",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_Lib.NTuple.index_.fuel_instrumented",
        "equation_with_fuel_Lib.NTuple.ntuple_.fuel_instrumented",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_2",
        "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_1b4848855b5d2f9c3d08284de9c11606",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_528b876405e78507cc8ed31848385919",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "token_correspondence_Lib.NTuple.ntuple_.fuel_instrumented",
        "typing_Lib.IntTypes.bits", "typing_Lib.NTuple.ntup4",
        "typing_Lib.NTuple.rest", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "cddbc4632d8aa237729b0a0b40358b2d"
    ],
    [
      "Lib.NTuple.tup4",
      1,
      4,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.NTuple.ntuple_.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.NTuple.flen", "equation_Lib.NTuple.ntuple",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_Lib.NTuple.ntuple_.fuel_instrumented",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_2",
        "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_528b876405e78507cc8ed31848385919",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "token_correspondence_FStar.Pervasives.Native.tuple2@tok",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "da0acd8d34f51d1dc370d39fe7578526"
    ],
    [
      "Lib.NTuple.tup4_lemma",
      1,
      4,
      0,
      [
        "@MaxIFuel_assumption", "@query", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_528b876405e78507cc8ed31848385919"
      ],
      0,
      "9bbe60b1ab13f79ce841bd4838d116a4"
    ],
    [
      "Lib.NTuple.tup4_lemma",
      2,
      4,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.NTuple.index_.fuel_instrumented",
        "@fuel_correspondence_Lib.NTuple.ntuple_.fuel_instrumented",
        "@fuel_irrelevance_Lib.NTuple.ntuple_.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_FStar.Pervasives.Native.fst", "equation_Lib.IntTypes.bits",
        "equation_Lib.NTuple.flen", "equation_Lib.NTuple.fst",
        "equation_Lib.NTuple.index", "equation_Lib.NTuple.ntuple",
        "equation_Lib.NTuple.rest", "equation_Lib.NTuple.tup4",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_Lib.NTuple.index_.fuel_instrumented",
        "equation_with_fuel_Lib.NTuple.ntuple_.fuel_instrumented",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_2",
        "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_1b4848855b5d2f9c3d08284de9c11606",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_528b876405e78507cc8ed31848385919",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "token_correspondence_Lib.NTuple.ntuple_.fuel_instrumented",
        "typing_Lib.IntTypes.bits", "typing_Lib.NTuple.rest",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "5f98a7e1ca72637e18ad71d718406a0a"
    ],
    [
      "Lib.NTuple.ntup8",
      1,
      4,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32", "equation_Lib.NTuple.flen",
        "equation_Lib.NTuple.ntuple",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_364e1096c6c138c9cc72351b5e5f6f33",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f"
      ],
      0,
      "de637f2edc082fc25f7c480d3aa352b1"
    ],
    [
      "Lib.NTuple.ntup8_lemma",
      1,
      8,
      0,
      [
        "@MaxIFuel_assumption", "@query", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_364e1096c6c138c9cc72351b5e5f6f33"
      ],
      0,
      "d4eaea4de2dc53fcdc26acb55ecbedf0"
    ],
    [
      "Lib.NTuple.ntup8_lemma",
      2,
      8,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.NTuple.index_.fuel_instrumented",
        "@fuel_correspondence_Lib.NTuple.ntuple_.fuel_instrumented",
        "@fuel_irrelevance_Lib.NTuple.ntuple_.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_FStar.Pervasives.Native.fst", "equation_Lib.IntTypes.bits",
        "equation_Lib.NTuple.flen", "equation_Lib.NTuple.fst",
        "equation_Lib.NTuple.index", "equation_Lib.NTuple.ntup8",
        "equation_Lib.NTuple.ntuple", "equation_Lib.NTuple.rest",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_Lib.NTuple.index_.fuel_instrumented",
        "equation_with_fuel_Lib.NTuple.ntuple_.fuel_instrumented",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_2",
        "lemma_Lib.IntTypes.pow2_3", "primitive_Prims.op_Equality",
        "primitive_Prims.op_Subtraction",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_1b4848855b5d2f9c3d08284de9c11606",
        "refinement_interpretation_Tm_refine_364e1096c6c138c9cc72351b5e5f6f33",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "token_correspondence_Lib.NTuple.ntuple_.fuel_instrumented",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_Lib.IntTypes.bits", "typing_Lib.NTuple.ntup8",
        "typing_Lib.NTuple.rest", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "0fbc1d802b2ab036b0f83bf2625ad0b3"
    ],
    [
      "Lib.NTuple.tup8",
      1,
      8,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.NTuple.ntuple_.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.NTuple.flen", "equation_Lib.NTuple.ntuple",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_Lib.NTuple.ntuple_.fuel_instrumented",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_2",
        "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_364e1096c6c138c9cc72351b5e5f6f33",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "token_correspondence_FStar.Pervasives.Native.tuple2@tok",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "8fbea4b30dcff1632119dba8ee4df31b"
    ],
    [
      "Lib.NTuple.tup8_lemma",
      1,
      8,
      0,
      [
        "@MaxIFuel_assumption", "@query", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_364e1096c6c138c9cc72351b5e5f6f33"
      ],
      0,
      "177a8b4ad9f5de4babd1fd4b76d0df06"
    ],
    [
      "Lib.NTuple.tup8_lemma",
      2,
      8,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.NTuple.index_.fuel_instrumented",
        "@fuel_correspondence_Lib.NTuple.ntuple_.fuel_instrumented",
        "@fuel_irrelevance_Lib.NTuple.ntuple_.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_FStar.Pervasives.Native.fst", "equation_Lib.IntTypes.bits",
        "equation_Lib.NTuple.flen", "equation_Lib.NTuple.fst",
        "equation_Lib.NTuple.index", "equation_Lib.NTuple.ntuple",
        "equation_Lib.NTuple.rest", "equation_Lib.NTuple.tup8",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_Lib.NTuple.index_.fuel_instrumented",
        "equation_with_fuel_Lib.NTuple.ntuple_.fuel_instrumented",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_2",
        "lemma_Lib.IntTypes.pow2_3", "primitive_Prims.op_Equality",
        "primitive_Prims.op_Subtraction",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_1b4848855b5d2f9c3d08284de9c11606",
        "refinement_interpretation_Tm_refine_364e1096c6c138c9cc72351b5e5f6f33",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "token_correspondence_Lib.NTuple.ntuple_.fuel_instrumented",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_Lib.IntTypes.bits", "typing_Lib.NTuple.rest",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "df334373be126998c335e8ebd3c81afc"
    ]
  ]
]