[
  "Z\\clÎ>ý­„\rèG†\u001dãP",
  [
    [
      "Lib.NTuple.ntuple_",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "binder_x_fbb855052fbcadaa14f24d60952144ef_1",
        "equation_Lib.NTuple.flen", "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_774ba3f728d91ead8ef40be66c9802e5",
        "well-founded-ordering-on-nat"
      ],
      0,
      "531c2effed0aeed7ac631b089d8ce53e"
    ],
    [
      "Lib.NTuple.rest",
      1,
      0,
      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,
      "8e5838c9c1ad3ff344683ecea8b38ac2"
    ],
    [
      "Lib.NTuple.index_fst_lemma",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Lib.NTuple.flen",
        "equation_Prims.pos",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "4608f68b81f38894c370b8ca32499d82"
    ],
    [
      "Lib.NTuple.to_lseq",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "fa646e999ea5dc2e89cbb1b7bc613864"
    ],
    [
      "Lib.NTuple.to_lseq_index",
      1,
      0,
      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,
      "e769a04feb5b38a1bf5a06276edd2e41"
    ],
    [
      "Lib.NTuple.from_lseq",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "b4507649f82955d86919d5afd336a38b"
    ],
    [
      "Lib.NTuple.concat",
      1,
      0,
      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,
      "930700a0eeea13a339ffe2c6b0776bf0"
    ],
    [
      "Lib.NTuple.concat_lemma",
      1,
      0,
      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,
      "e37ca12677ce3abd517d730d0e2cb567"
    ],
    [
      "Lib.NTuple.eq_intro",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "9314bd66b00f538f020d17cd18aa406c"
    ],
    [
      "Lib.NTuple.upd_lemma",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "fabaa4d8ff704e2e4732f5d79d5adae2"
    ],
    [
      "Lib.NTuple.index_sub_lemma",
      1,
      0,
      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,
      "6840a87c8de04611f43c8e00d12cea02"
    ],
    [
      "Lib.NTuple.index_update_sub_lemma",
      1,
      0,
      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,
      "1bb129dd5fc36f86320f48105107edb4"
    ],
    [
      "Lib.NTuple.ntup1",
      1,
      0,
      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,
      "1926a9c81685224f094d2bd7e9de8de1"
    ],
    [
      "Lib.NTuple.ntup1_lemma",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_bded595d5c675d20923ebf7eee58cd50"
      ],
      0,
      "0795a392bda41541984fc9c73ed195ce"
    ],
    [
      "Lib.NTuple.tup1",
      1,
      0,
      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,
      "cfe1835f1a404ba5c1cab043e3759669"
    ],
    [
      "Lib.NTuple.tup1_lemma",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_bded595d5c675d20923ebf7eee58cd50"
      ],
      0,
      "15f4e3025b6866dec633ab0222e72cb6"
    ],
    [
      "Lib.NTuple.ntup4",
      1,
      2,
      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,
      "eba212027cafc9ec2ce8287936a54614"
    ],
    [
      "Lib.NTuple.ntup4_lemma",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_528b876405e78507cc8ed31848385919"
      ],
      0,
      "38d474dc39e8aed2b6375f00586f05a9"
    ],
    [
      "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,
      "4dfbdab9c6dd979823b0c4176d9cfe20"
    ],
    [
      "Lib.NTuple.tup4_lemma",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_528b876405e78507cc8ed31848385919"
      ],
      0,
      "2db69c9e7c8f4b47b08b87095de3b20f"
    ],
    [
      "Lib.NTuple.ntup8",
      1,
      2,
      1,
      [
        "@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,
      "ae237d955cc36083a335db885e20c844"
    ],
    [
      "Lib.NTuple.ntup8_lemma",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_364e1096c6c138c9cc72351b5e5f6f33"
      ],
      0,
      "7e6ff4e1383f962d857142056931f9a9"
    ],
    [
      "Lib.NTuple.tup8",
      1,
      8,
      8,
      [
        "@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_Prims.pow2.fuel_instrumented",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "135cf45237f30859010a7cb5cab4abe2"
    ],
    [
      "Lib.NTuple.tup8_lemma",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_364e1096c6c138c9cc72351b5e5f6f33"
      ],
      0,
      "a2c134e712448005c0cfe61fe36a8a4a"
    ]
  ]
]