[
  "<'c\u007fE\u0018\u0004\u001c½R€ç\fbj'",
  [
    [
      "MerkleTree.New.High.Correct.Base.seq_prefix",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81746e462692213c028719b75d01a164",
        "typing_FStar.Seq.Base.length"
      ],
      0,
      "7430ecaee7c026dceddbfc24db00273b"
    ],
    [
      "MerkleTree.New.High.Correct.Base.seq_head_cons",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_FStar.Seq.Properties.cons", "equation_Prims.nat",
        "int_typing", "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length"
      ],
      0,
      "f9a4f48af20a6e6ed329898d02c92c3d"
    ],
    [
      "MerkleTree.New.High.Correct.Base.seq_head_cons",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_FStar.Seq.Properties.cons",
        "equation_FStar.Seq.Properties.head", "equation_Prims.nat",
        "int_typing", "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.Seq.Base.lemma_index_app1",
        "lemma_FStar.Seq.Base.lemma_index_create",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.create"
      ],
      0,
      "80f6112e51667eae298ea13410cd9f2a"
    ],
    [
      "MerkleTree.New.High.Correct.Base.seq_tail_cons",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_FStar.Seq.Properties.cons", "equation_Prims.nat",
        "int_typing", "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length"
      ],
      0,
      "eaa8144c20feab44f579e7fac8e008b7"
    ],
    [
      "MerkleTree.New.High.Correct.Base.seq_tail_cons",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_FStar.Seq.Properties.cons",
        "equation_FStar.Seq.Properties.tail", "equation_Prims.nat",
        "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "lemma_FStar.Seq.Base.lemma_index_app2",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "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_167ef714932ec832fb671890fc3eee6c",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length",
        "typing_FStar.Seq.Properties.cons",
        "typing_FStar.Seq.Properties.tail"
      ],
      0,
      "875e5aa298a7244267d5095c0dcea162"
    ],
    [
      "MerkleTree.New.High.Correct.Base.empty_hashes",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "373a2d31f568c9b960fdf23ab1065f36"
    ],
    [
      "MerkleTree.New.High.Correct.Base.empty_hashes",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes",
        "lemma_FStar.Seq.Base.lemma_create_len",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "typing_FStar.Seq.Base.empty", "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.New.High.hashes"
      ],
      0,
      "93c3dc70b8eaed2c246d4f356d6a05c6"
    ],
    [
      "MerkleTree.New.High.Correct.Base.empty_hashes_head",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001"
      ],
      0,
      "173399cf40c8cce3da07b15a974fa912"
    ],
    [
      "MerkleTree.New.High.Correct.Base.empty_hashes_head",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_FStar.Seq.Properties.head",
        "equation_MerkleTree.New.High.Correct.Base.empty_hashes",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes", "equation_Prims.nat",
        "int_inversion", "lemma_FStar.Seq.Base.lemma_index_create",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length",
        "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.New.High.hashes"
      ],
      0,
      "fb07534772a24e9f47ee2a9218433d51"
    ],
    [
      "MerkleTree.New.High.Correct.Base.empty_hashes_tail",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_53437d4a0ad8fab977060c348adb649c",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001"
      ],
      0,
      "df4f7490d0da379593f6857e84ede81f"
    ],
    [
      "MerkleTree.New.High.Correct.Base.empty_hashes_tail",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_FStar.Seq.Properties.tail",
        "equation_MerkleTree.New.High.Correct.Base.empty_hashes",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes", "equation_Prims.nat",
        "equation_Prims.pos", "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "lemma_FStar.Seq.Base.lemma_index_create",
        "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_167ef714932ec832fb671890fc3eee6c",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_4af030e7a84d9598a12163975248d0c3",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.empty",
        "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Properties.tail",
        "typing_MerkleTree.New.High.Correct.Base.empty_hashes",
        "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.New.High.hashes"
      ],
      0,
      "676505d4f5885fab049f4cdc87614aff"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91"
      ],
      0,
      "fb5ba79a366d561f2ef5e8e7594f779f"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91"
      ],
      0,
      "c9ab0e7ae5ca17e53aff532527bf260d"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv",
      3,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_51fba9034a886564fb18a29fa7a6025b_2",
        "binder_x_6e1290e37a6b4e437f899d72093932a2_1",
        "binder_x_89dfa9cb1583ae31cce9fe730922098c_3",
        "equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Division", "primitive_Prims.op_Equality",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_3275c6670c647fe05603aaa27ba49f71",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_85623b7d0d334235021ea957a454d881",
        "well-founded-ordering-on-nat"
      ],
      0,
      "bce175e1ce3bf55608bba00a5d1bbfab"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_empty",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "equation_Prims.nat", "equation_Prims.pos", "int_typing",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_Prims.pow2"
      ],
      0,
      "d72cdb3d95699281b28d7151cc2c9360"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_empty",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "equation_Prims.nat", "equation_Prims.pos", "int_typing",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_e958996f510ec2b31d199ad7ccb9e063",
        "typing_Prims.pow2"
      ],
      0,
      "b02f2d5b52dab2fe48b5a8a64185da0c"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_empty",
      3,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_6e1290e37a6b4e437f899d72093932a2_1",
        "binder_x_f26957a7e62b271a8736230b1e9c83c1_0", "eq2-interp",
        "equality_tok_Prims.LexTop@tok",
        "equation_MerkleTree.New.High.Correct.Base.empty_hashes",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "l_and-interp",
        "lemma_FStar.Seq.Base.lemma_index_create",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Division",
        "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_1ae2a0d6b2f4da2d4b0194885669f804",
        "refinement_interpretation_Tm_refine_4af030e7a84d9598a12163975248d0c3",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
        "true_interp", "typing_FStar.Seq.Base.empty",
        "typing_FStar.Seq.Base.length",
        "typing_MerkleTree.New.High.Correct.Base.empty_hashes",
        "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.New.High.hashes", "typing_Prims.pow2",
        "well-founded-ordering-on-nat"
      ],
      0,
      "47759005860a81ac2698031bc3c1b713"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_next_rel",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "1ed78b286fa6f62c14b842d0f019eb6c"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_next_rel",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "abd61716ee6235c03ec72faf87142ef1"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_next_rel",
      3,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Division", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_59122260c77179a912aff4679b32096c",
        "refinement_interpretation_Tm_refine_cdc09d6032c37371558f1d5d77d7bd2c",
        "refinement_interpretation_Tm_refine_f97fad2c1fb2db1c8f88c401525f4a64"
      ],
      0,
      "512887e6d465c10a3693150a535d0b1b"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_inv",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_da1b0dfb8283502ec162998a8bbb6431"
      ],
      0,
      "938d2b0382a9ff1471761dfdc00a7ddb"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_inv",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_da1b0dfb8283502ec162998a8bbb6431"
      ],
      0,
      "656d5a8187548cd149d439da8496f787"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_inv",
      3,
      2,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_667d454c60eed0d66023b4d83352da53_3",
        "binder_x_a3597293d3fb700646795c4d8a2718b7_4",
        "binder_x_a3a9d1e443789a10c20ec8f7e2fe66e3_2",
        "binder_x_f26957a7e62b271a8736230b1e9c83c1_0", "eq2-interp",
        "equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "l_and-interp",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Division",
        "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_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_1ae2a0d6b2f4da2d4b0194885669f804",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_572efb46e082aa1b039cb74ce53f80ae",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_c331dc32158dc69a8b1476deb62a0360",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
        "refinement_interpretation_Tm_refine_da1b0dfb8283502ec162998a8bbb6431",
        "well-founded-ordering-on-nat"
      ],
      0,
      "26c8511f55163435cb1abc71ad509b4d"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_inv_empty",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "equation_MerkleTree.New.High.Correct.Base.empty_hashes",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Spec.Poly1305.size_key", "int_typing",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_53437d4a0ad8fab977060c348adb649c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_a78e81a34494fa620ef91991a1267b1f",
        "refinement_interpretation_Tm_refine_da1b0dfb8283502ec162998a8bbb6431",
        "typing_MerkleTree.New.High.Correct.Base.empty_hashes",
        "typing_Prims.pow2", "typing_Spec.Poly1305.size_key"
      ],
      0,
      "9c072d5671d7aca2e4610884450468a2"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_inv_empty",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "equation_MerkleTree.New.High.Correct.Base.empty_hashes",
        "equation_Prims.nat", "equation_Prims.pos", "int_inversion",
        "int_typing", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_4af030e7a84d9598a12163975248d0c3",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_a6863cbab56db687492a9bd3a4f56cb6",
        "typing_MerkleTree.New.High.Correct.Base.empty_hashes",
        "typing_Prims.pow2"
      ],
      0,
      "52a0e38424c38d387671f224eca2767d"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_inv_empty",
      3,
      2,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_inv.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.mt_hashes_inv.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_5e20d151293c9e40e5203cbcff29aebe_1",
        "binder_x_a3a9d1e443789a10c20ec8f7e2fe66e3_2",
        "binder_x_f26957a7e62b271a8736230b1e9c83c1_0", "eq2-interp",
        "equality_tok_Prims.LexTop@tok",
        "equation_MerkleTree.New.High.Correct.Base.empty_hashes",
        "equation_MerkleTree.New.High.Correct.Base.mt_hashes_next_rel",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_inv.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "l_and-interp",
        "lemma_FStar.Seq.Base.lemma_index_create",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Division", "primitive_Prims.op_Equality",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_1ae2a0d6b2f4da2d4b0194885669f804",
        "refinement_interpretation_Tm_refine_4af030e7a84d9598a12163975248d0c3",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
        "refinement_interpretation_Tm_refine_da1b0dfb8283502ec162998a8bbb6431",
        "refinement_interpretation_Tm_refine_eeb34a6663fec3915a03d46b7a3fadb8",
        "refinement_interpretation_Tm_refine_f97fad2c1fb2db1c8f88c401525f4a64",
        "true_interp", "typing_FStar.Seq.Base.empty",
        "typing_FStar.Seq.Base.length",
        "typing_MerkleTree.New.High.Correct.Base.empty_hashes",
        "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.New.High.hashes", "typing_Prims.pow2",
        "well-founded-ordering-on-nat"
      ],
      0,
      "574f5aaf65f9d960b7b54fc56697066f"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_equiv",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
        "refinement_interpretation_Tm_refine_da1b0dfb8283502ec162998a8bbb6431"
      ],
      0,
      "51af834b15aa49c5bfd2d1bdd48e2784"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_equiv",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_a590ef17d004eb5c1f048c9a013c53bd",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
        "refinement_interpretation_Tm_refine_da1b0dfb8283502ec162998a8bbb6431"
      ],
      0,
      "36ab67c39e29ee801d950dc042a03646"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_equiv",
      3,
      2,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_667d454c60eed0d66023b4d83352da53_3",
        "binder_x_89dfa9cb1583ae31cce9fe730922098c_4",
        "binder_x_89dfa9cb1583ae31cce9fe730922098c_5",
        "binder_x_a3a9d1e443789a10c20ec8f7e2fe66e3_2",
        "binder_x_f26957a7e62b271a8736230b1e9c83c1_0", "eq2-interp",
        "equality_tok_Prims.LexTop@tok",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "l_and-interp",
        "lemma_FStar.UInt.pow2_values",
        "lemma_MerkleTree.New.High.seq_slice_equal_index",
        "lemma_MerkleTree.New.High.seq_slice_more_equal",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Division", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThan", "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_0545ca68af3b2fc8df509fb388f7f2ee",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_1ae2a0d6b2f4da2d4b0194885669f804",
        "refinement_interpretation_Tm_refine_3275c6670c647fe05603aaa27ba49f71",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
        "refinement_interpretation_Tm_refine_572efb46e082aa1b039cb74ce53f80ae",
        "refinement_interpretation_Tm_refine_5a8634b460d149c76a5c0476662af1d0",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_cc7ec1228e62f637b46417d43aae0cfa",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
        "refinement_interpretation_Tm_refine_da1b0dfb8283502ec162998a8bbb6431",
        "typing_FStar.Seq.Base.length", "typing_MerkleTree.New.High.hashes",
        "well-founded-ordering-on-nat"
      ],
      0,
      "00b68cf5b971f99b91f0925df1675763"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_inv_equiv",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_da1b0dfb8283502ec162998a8bbb6431",
        "refinement_interpretation_Tm_refine_eeb34a6663fec3915a03d46b7a3fadb8"
      ],
      0,
      "1b3223517c91ff98026f481be91469e7"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_inv_equiv",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_15c40252e327b36142063e4afa84a885",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_da1b0dfb8283502ec162998a8bbb6431",
        "refinement_interpretation_Tm_refine_eeb34a6663fec3915a03d46b7a3fadb8"
      ],
      0,
      "1083649db196bd0a3d03e0ce668ac7dd"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_inv_equiv",
      3,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_inv.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.mt_hashes_inv.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_5e20d151293c9e40e5203cbcff29aebe_1",
        "binder_x_667d454c60eed0d66023b4d83352da53_3",
        "binder_x_a3597293d3fb700646795c4d8a2718b7_4",
        "binder_x_a3597293d3fb700646795c4d8a2718b7_5",
        "binder_x_a3a9d1e443789a10c20ec8f7e2fe66e3_2",
        "binder_x_f26957a7e62b271a8736230b1e9c83c1_0", "eq2-interp",
        "equality_tok_Prims.LexTop@tok",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_inv.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "l_and-interp",
        "lemma_MerkleTree.New.High.seq_slice_equal_index",
        "lemma_MerkleTree.New.High.seq_slice_more_equal",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Division", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThan", "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_0545ca68af3b2fc8df509fb388f7f2ee",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_1ae2a0d6b2f4da2d4b0194885669f804",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
        "refinement_interpretation_Tm_refine_572efb46e082aa1b039cb74ce53f80ae",
        "refinement_interpretation_Tm_refine_5a8634b460d149c76a5c0476662af1d0",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_c331dc32158dc69a8b1476deb62a0360",
        "refinement_interpretation_Tm_refine_cc7ec1228e62f637b46417d43aae0cfa",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
        "refinement_interpretation_Tm_refine_da1b0dfb8283502ec162998a8bbb6431",
        "refinement_interpretation_Tm_refine_eeb34a6663fec3915a03d46b7a3fadb8",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_FStar.Seq.Base.length", "typing_MerkleTree.New.High.hashes",
        "well-founded-ordering-on-nat"
      ],
      0,
      "74742d53a64e4b39d7b837867e2bf34a"
    ],
    [
      "MerkleTree.New.High.Correct.Base.merge_hs",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "38dafd5b4947d9f02ba55d7cf3d7b709"
    ],
    [
      "MerkleTree.New.High.Correct.Base.merge_hs",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "6a66305025b3bfd84ea2791124eb482e"
    ],
    [
      "MerkleTree.New.High.Correct.Base.merge_hs",
      3,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_117efdf2115292854bfcfb870cda5779_2",
        "binder_x_de80495d94c249ded13bcd114e104211_3",
        "binder_x_f26957a7e62b271a8736230b1e9c83c1_0",
        "equality_tok_Prims.LexTop@tok",
        "equation_FStar.Seq.Properties.cons",
        "equation_FStar.Seq.Properties.tail",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess", "equation_Prims.eqtype",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "int_typing", "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_82e94a4e396280bbafb488e22d340334",
        "refinement_interpretation_Tm_refine_ffa192ffd24031081463a09af5033bc6",
        "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length",
        "typing_MerkleTree.New.High.hashes", "well-founded-ordering-on-nat"
      ],
      0,
      "81f7123a161c5541087509cd011cd091"
    ],
    [
      "MerkleTree.New.High.Correct.Base.merge_hs_empty",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.merge_hs.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.merge_hs.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_5e20d151293c9e40e5203cbcff29aebe_1",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2",
        "binder_x_f26957a7e62b271a8736230b1e9c83c1_0",
        "equation_MerkleTree.New.High.Correct.Base.empty_hashes",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess", "equation_Prims.nat",
        "equation_Prims.op_Equals_Equals_Equals", "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.merge_hs.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "lemma_FStar.Seq.Base.lemma_eq_refl",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.Seq.Properties.cons_head_tail",
        "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_167ef714932ec832fb671890fc3eee6c",
        "refinement_interpretation_Tm_refine_4af030e7a84d9598a12163975248d0c3",
        "refinement_interpretation_Tm_refine_4ef5ae8f18db40d112891674c999b23e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_79b1f96066f565b13f91f5d0e354834c",
        "refinement_interpretation_Tm_refine_9b2b3e7ac5f300ddc6add4181948ef22",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_Tm_refine_bf3340443d6edf0ae4bc4b37060534fb",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
        "typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Properties.tail",
        "typing_MerkleTree.New.High.Correct.Base.empty_hashes",
        "typing_MerkleTree.New.High.Correct.Base.merge_hs",
        "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.New.High.hashes", "well-founded-ordering-on-nat"
      ],
      0,
      "8b5363ab1872b4a4ed53d06740f87892"
    ],
    [
      "MerkleTree.New.High.Correct.Base.merge_hs_index",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_22125f28c20990597c03dac8bb18819e",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_9b2b3e7ac5f300ddc6add4181948ef22",
        "refinement_interpretation_Tm_refine_bf3340443d6edf0ae4bc4b37060534fb",
        "typing_MerkleTree.New.High.Correct.Base.merge_hs"
      ],
      0,
      "ed63b3a3e1ba30a5df0fd91da68b2882"
    ],
    [
      "MerkleTree.New.High.Correct.Base.merge_hs_index",
      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",
        "refinement_interpretation_Tm_refine_6426f4b52fc8d121f4c6b1a8f9ade6c4",
        "refinement_interpretation_Tm_refine_9b2b3e7ac5f300ddc6add4181948ef22",
        "refinement_interpretation_Tm_refine_bf3340443d6edf0ae4bc4b37060534fb",
        "typing_MerkleTree.New.High.Correct.Base.merge_hs"
      ],
      0,
      "3bf41414afb3bd7474c22bae80553b61"
    ],
    [
      "MerkleTree.New.High.Correct.Base.merge_hs_index",
      3,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.merge_hs.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.merge_hs.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_117efdf2115292854bfcfb870cda5779_2",
        "binder_x_5e20d151293c9e40e5203cbcff29aebe_1",
        "binder_x_abd453175ea86d2496fbbe2a1cc1b73b_4",
        "binder_x_de80495d94c249ded13bcd114e104211_3",
        "binder_x_f26957a7e62b271a8736230b1e9c83c1_0",
        "equality_tok_Prims.LexTop@tok",
        "equation_FStar.Seq.Properties.cons",
        "equation_FStar.Seq.Properties.head",
        "equation_FStar.Seq.Properties.tail",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.merge_hs.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_refl",
        "lemma_FStar.Seq.Base.lemma_index_app2",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_MerkleTree.New.High.Correct.Base.seq_head_cons",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_167ef714932ec832fb671890fc3eee6c",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_9b2b3e7ac5f300ddc6add4181948ef22",
        "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
        "refinement_interpretation_Tm_refine_bc0173bc8aadefdfb2d77d3e7f673d00",
        "refinement_interpretation_Tm_refine_bf3340443d6edf0ae4bc4b37060534fb",
        "refinement_interpretation_Tm_refine_ca5c7261637708c151f3c71ffceab8fc",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_ffa192ffd24031081463a09af5033bc6",
        "token_correspondence_MerkleTree.New.High.Correct.Base.merge_hs.fuel_instrumented",
        "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
        "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
        "typing_FStar.Seq.Properties.head",
        "typing_FStar.Seq.Properties.tail",
        "typing_MerkleTree.New.High.Correct.Base.merge_hs",
        "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.New.High.hashes", "unit_inversion", "unit_typing",
        "well-founded-ordering-on-nat"
      ],
      0,
      "b0e72c3f0fec0fe0e5fe92251d4c0cc7"
    ],
    [
      "MerkleTree.New.High.Correct.Base.merge_hs_slice_equal",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion", "bool_typing",
        "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_8e05722fd967b5d9d7dc88775094d25b",
        "refinement_interpretation_Tm_refine_9b2b3e7ac5f300ddc6add4181948ef22",
        "refinement_interpretation_Tm_refine_bf3340443d6edf0ae4bc4b37060534fb",
        "typing_MerkleTree.New.High.Correct.Base.merge_hs"
      ],
      0,
      "0341bc2fb8be139c82a37c5d6ef140fb"
    ],
    [
      "MerkleTree.New.High.Correct.Base.merge_hs_slice_equal",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion", "bool_typing",
        "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_46306474f4b38cca5abd64ae8ee28ba3",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_8e05722fd967b5d9d7dc88775094d25b",
        "refinement_interpretation_Tm_refine_9b2b3e7ac5f300ddc6add4181948ef22",
        "refinement_interpretation_Tm_refine_bf3340443d6edf0ae4bc4b37060534fb",
        "typing_MerkleTree.New.High.Correct.Base.merge_hs"
      ],
      0,
      "3b2c468d39036fec13b5d0a42196f073"
    ],
    [
      "MerkleTree.New.High.Correct.Base.merge_hs_slice_equal",
      3,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.merge_hs.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.merge_hs.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_0488ca017eb55a869da97ace526de0cb_7",
        "binder_x_117efdf2115292854bfcfb870cda5779_2",
        "binder_x_117efdf2115292854bfcfb870cda5779_4",
        "binder_x_5e20d151293c9e40e5203cbcff29aebe_1",
        "binder_x_8318cc8eba1052ae772493598bf20ef0_5",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_6",
        "binder_x_de80495d94c249ded13bcd114e104211_3",
        "binder_x_f26957a7e62b271a8736230b1e9c83c1_0", "bool_inversion",
        "bool_typing", "equality_tok_Prims.LexTop@tok",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Prims.pos",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "lemma_FStar.Seq.Base.lemma_eq_refl",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.slice_is_empty",
        "lemma_MerkleTree.New.High.Correct.Base.merge_hs_index",
        "lemma_MerkleTree.New.High.seq_slice_equal_index",
        "lemma_MerkleTree.New.High.seq_slice_more_equal",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Equality", "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_0545ca68af3b2fc8df509fb388f7f2ee",
        "refinement_interpretation_Tm_refine_22125f28c20990597c03dac8bb18819e",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
        "refinement_interpretation_Tm_refine_5a8634b460d149c76a5c0476662af1d0",
        "refinement_interpretation_Tm_refine_72e833853911f17d47de5c800ef08fda",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_9b2b3e7ac5f300ddc6add4181948ef22",
        "refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1",
        "refinement_interpretation_Tm_refine_bd51bed75116cdbe1676b147260314ad",
        "refinement_interpretation_Tm_refine_bf3340443d6edf0ae4bc4b37060534fb",
        "refinement_interpretation_Tm_refine_cc7ec1228e62f637b46417d43aae0cfa",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_ffa192ffd24031081463a09af5033bc6",
        "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.index",
        "typing_FStar.Seq.Base.slice",
        "typing_MerkleTree.New.High.Correct.Base.merge_hs",
        "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.New.High.hashes", "well-founded-ordering-on-nat"
      ],
      0,
      "49dbec27acaedf5bc3021d07a75e0919"
    ],
    [
      "MerkleTree.New.High.Correct.Base.merge_hs_upd",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "lemma_FStar.Seq.Base.lemma_len_upd",
        "refinement_interpretation_Tm_refine_22125f28c20990597c03dac8bb18819e",
        "refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_9b2b3e7ac5f300ddc6add4181948ef22",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_MerkleTree.New.High.hashes"
      ],
      0,
      "2e6de3a4ae7b2b7974adf2539fa41eaa"
    ],
    [
      "MerkleTree.New.High.Correct.Base.merge_hs_upd",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "lemma_FStar.Seq.Base.lemma_len_upd",
        "refinement_interpretation_Tm_refine_22125f28c20990597c03dac8bb18819e",
        "refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7c8cf29e89958b30a7b7bf3d4bf62fce",
        "refinement_interpretation_Tm_refine_9b2b3e7ac5f300ddc6add4181948ef22",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_MerkleTree.New.High.hashes"
      ],
      0,
      "3c890862896d8321e054919ac4aebd08"
    ],
    [
      "MerkleTree.New.High.Correct.Base.merge_hs_upd",
      3,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.merge_hs.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.merge_hs.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_117efdf2115292854bfcfb870cda5779_2",
        "binder_x_5e20d151293c9e40e5203cbcff29aebe_1",
        "binder_x_abd453175ea86d2496fbbe2a1cc1b73b_4",
        "binder_x_de57e94726f1653c4e53f75ab929ebb4_5",
        "binder_x_de57e94726f1653c4e53f75ab929ebb4_6",
        "binder_x_de80495d94c249ded13bcd114e104211_3",
        "binder_x_f26957a7e62b271a8736230b1e9c83c1_0",
        "equality_tok_Prims.LexTop@tok",
        "equation_FStar.Seq.Properties.head",
        "equation_FStar.Seq.Properties.tail",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.merge_hs.fuel_instrumented",
        "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_eq_refl",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_index_upd1",
        "lemma_FStar.Seq.Base.lemma_index_upd2",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Base.lemma_len_upd",
        "lemma_FStar.Seq.Properties.slice_upd",
        "lemma_MerkleTree.New.High.Correct.Base.merge_hs_index",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_22125f28c20990597c03dac8bb18819e",
        "refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_67afcdeaccc1e07b22a6eebaca0b8719",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_9b2b3e7ac5f300ddc6add4181948ef22",
        "refinement_interpretation_Tm_refine_bf3340443d6edf0ae4bc4b37060534fb",
        "refinement_interpretation_Tm_refine_ca5c7261637708c151f3c71ffceab8fc",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_df81b3f17797c6f405c1dbb191651292",
        "refinement_interpretation_Tm_refine_ffa192ffd24031081463a09af5033bc6",
        "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.index",
        "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.upd",
        "typing_MerkleTree.New.High.Correct.Base.merge_hs",
        "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.New.High.hashes", "unit_inversion", "unit_typing",
        "well-founded-ordering-on-nat"
      ],
      0,
      "2163941b19999f2d39218dbcae02ad42"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_olds_inv",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_6e1290e37a6b4e437f899d72093932a2_1",
        "binder_x_89dfa9cb1583ae31cce9fe730922098c_3",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2",
        "equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Division", "primitive_Prims.op_Equality",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_3275c6670c647fe05603aaa27ba49f71",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "well-founded-ordering-on-nat"
      ],
      0,
      "92e1b5adaa939b267a9d6d05e04e2086"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_olds_inv_equiv",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b"
      ],
      0,
      "91569362fddfbb983c99c850b536e907"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_olds_inv_equiv",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_53fcb38e35e8c3daec41b3e0757a75e0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b"
      ],
      0,
      "86b6a872c9f69bc6afa97bcd41071ce2"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_olds_inv_equiv",
      3,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_olds_inv.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.mt_olds_inv.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_6e1290e37a6b4e437f899d72093932a2_2",
        "binder_x_89dfa9cb1583ae31cce9fe730922098c_4",
        "binder_x_89dfa9cb1583ae31cce9fe730922098c_5",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_3",
        "binder_x_f26957a7e62b271a8736230b1e9c83c1_0",
        "equality_tok_Prims.LexTop@tok",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess", "equation_Prims.eq2",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_olds_inv.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "l_and-interp",
        "lemma_MerkleTree.New.High.seq_slice_equal_index",
        "lemma_MerkleTree.New.High.seq_slice_more_equal",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Division", "primitive_Prims.op_Equality",
        "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_0545ca68af3b2fc8df509fb388f7f2ee",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_3275c6670c647fe05603aaa27ba49f71",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
        "refinement_interpretation_Tm_refine_5a8634b460d149c76a5c0476662af1d0",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_cc7ec1228e62f637b46417d43aae0cfa",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
        "typing_FStar.Seq.Base.length", "typing_MerkleTree.New.High.hashes",
        "well-founded-ordering-on-nat"
      ],
      0,
      "8d5573298235afa8a5592652cafbb971"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_olds_hs_lth_inv_ok",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_4d0ab6134173bbad75f08ef14247f657",
        "refinement_interpretation_Tm_refine_5664991902867dbaea8455604edd6227"
      ],
      0,
      "f331058b8ee5a682e657fff20bc84fb2"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_olds_hs_lth_inv_ok",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_1606d1df6ee07c1cff5370105a60c0b6",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_4d0ab6134173bbad75f08ef14247f657",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "23cd99b0c84123e9c49bb7c1a04f3766"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_olds_hs_lth_inv_ok",
      3,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.merge_hs.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_olds_inv.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.merge_hs.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.mt_olds_inv.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_5e20d151293c9e40e5203cbcff29aebe_1",
        "binder_x_6e1290e37a6b4e437f899d72093932a2_2",
        "binder_x_8cf65b3b9d91dec7086970aa4543f287_5",
        "binder_x_abefe0b518359a5a388975bd4374c4d4_6",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_3",
        "binder_x_cbac39ab364bbcc08dab587ac968871a_4",
        "binder_x_f26957a7e62b271a8736230b1e9c83c1_0", "eq2-interp",
        "equality_tok_Prims.LexTop@tok", "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess",
        "equation_MerkleTree.New.High.offset_of", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_olds_inv.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "l_and-interp",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_MerkleTree.New.High.Correct.Base.merge_hs_index",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Division",
        "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_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_1ae2a0d6b2f4da2d4b0194885669f804",
        "refinement_interpretation_Tm_refine_22125f28c20990597c03dac8bb18819e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_6ecc26d260b07cd8c8333ca61d7545ba",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_9b2b3e7ac5f300ddc6add4181948ef22",
        "refinement_interpretation_Tm_refine_ad53f3413fd15db5258446e997071714",
        "refinement_interpretation_Tm_refine_bf3340443d6edf0ae4bc4b37060534fb",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_d87d99f22d4a7ec1b20cbca92c993502",
        "refinement_interpretation_Tm_refine_db1f7a375601e94233b330488ad7e8aa",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.index",
        "typing_FStar.Seq.Base.length",
        "typing_MerkleTree.New.High.Correct.Base.merge_hs",
        "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.New.High.hashes", "well-founded-ordering-on-nat"
      ],
      0,
      "e46238f0550f5ee02bb552ef04898ded"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_olds_hs_inv",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_da1b0dfb8283502ec162998a8bbb6431"
      ],
      0,
      "87d3122edb75abb34ad003d046e84d81"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_olds_hs_inv",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_da1b0dfb8283502ec162998a8bbb6431"
      ],
      0,
      "585562ecdf56de76adaa14ae59c1f983"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_olds_hs_inv",
      3,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_4d0ab6134173bbad75f08ef14247f657",
        "refinement_interpretation_Tm_refine_5664991902867dbaea8455604edd6227",
        "refinement_interpretation_Tm_refine_da1b0dfb8283502ec162998a8bbb6431"
      ],
      0,
      "761f73af2966e4d3b87865b9566ea3b2"
    ],
    [
      "MerkleTree.New.High.Correct.Base.log2",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "a0c44169a6a457e6931b556b8b2db8cb"
    ],
    [
      "MerkleTree.New.High.Correct.Base.log2",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "4b01ebca7c8e72362e283b0f8529f4d5"
    ],
    [
      "MerkleTree.New.High.Correct.Base.log2",
      3,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_c9f70ab639c9ae669e58190eb4c1b5c9_0",
        "constructor_distinct_FStar.Integers.W16",
        "constructor_distinct_FStar.Integers.W31",
        "constructor_distinct_FStar.Integers.W8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_FStar.Integers.W16@tok",
        "equality_tok_FStar.Integers.W31@tok",
        "equality_tok_FStar.Integers.W8@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Prims.nat", "equation_Spec.Poly1305.size_key",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_Lib.IntTypes.pow2_values",
        "lemma_Spec.Curve25519.Lemmas.lemma_div_n",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Division",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Integers.Signed__0",
        "projection_inverse_FStar.Integers.Unsigned__0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_a78e81a34494fa620ef91991a1267b1f",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "refinement_interpretation_Tm_refine_d428a3134600e4183ddf3caf7b45c5ad",
        "typing_Spec.Poly1305.size_key", "well-founded-ordering-on-nat"
      ],
      0,
      "273327b0adcd8d9fa114769ffd35065b"
    ],
    [
      "MerkleTree.New.High.Correct.Base.log2_bound",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_07fa1cd77897687fff6fd60f063ba592_1",
        "binder_x_c9f70ab639c9ae669e58190eb4c1b5c9_0", "equation_Prims.nat",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.log2.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",
        "lemma_Spec.Curve25519.Lemmas.lemma_div_n",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Division",
        "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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7041c6269e46b31230115ee689cc06f1",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "well-founded-ordering-on-nat"
      ],
      0,
      "3aabc1f5aaff83ce09765ec6e07bd6b5"
    ],
    [
      "MerkleTree.New.High.Correct.Base.log2_div",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_Division",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_99c44f87e8db7c2b2518f780068deb58"
      ],
      0,
      "e2be7c316792906001e21c1cd4f7d224"
    ],
    [
      "MerkleTree.New.High.Correct.Base.log2_div",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.nat",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Division", "primitive_Prims.op_Equality",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_99c44f87e8db7c2b2518f780068deb58",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "typing_MerkleTree.New.High.Correct.Base.log2"
      ],
      0,
      "ac4e7e1af73e2b6a975236ecdb11ba7e"
    ],
    [
      "MerkleTree.New.High.Correct.Base.log2c",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "0a2f44c0328f82d9258fab5d2e188e43"
    ],
    [
      "MerkleTree.New.High.Correct.Base.log2c",
      2,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "bool_inversion", "bool_typing", "equation_Prims.nat",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_Addition",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
        "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_13d357a23a5e1099db9eb784ff83d223",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001"
      ],
      0,
      "48ff228660dfbb2e709db3c2dc7164a7"
    ],
    [
      "MerkleTree.New.High.Correct.Base.log2c_div",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "primitive_Prims.op_Division",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001"
      ],
      0,
      "49a027c562d84bbba4c034e2cabf6daf"
    ],
    [
      "MerkleTree.New.High.Correct.Base.log2c_div",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.log2.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_Division",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan",
        "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_13d357a23a5e1099db9eb784ff83d223",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "token_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_MerkleTree.New.High.Correct.Base.log2",
        "typing_MerkleTree.New.High.Correct.Base.log2c"
      ],
      0,
      "b11add13c09b53f395219404e7382d20"
    ],
    [
      "MerkleTree.New.High.Correct.Base.log2c_bound",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_aaef4192d81eba81460a4fe1d83adf13_1",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.log2.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_Division",
        "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_13d357a23a5e1099db9eb784ff83d223",
        "refinement_interpretation_Tm_refine_3f20fe758236b0de966c5a8c64b63929",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_MerkleTree.New.High.Correct.Base.log2",
        "well-founded-ordering-on-nat"
      ],
      0,
      "b9c838ad03db7ca68a64ca48abfb29f1"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "36ea17f1ccdb77f3fd0209c620bf2ffe"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "f7506a7a7fb6e2d54ed00de40420b10f"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log",
      3,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_9367128ae882c35c606ce68e9e77dbe9_2",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
        "binder_x_f26957a7e62b271a8736230b1e9c83c1_0",
        "equality_tok_Prims.LexTop@tok",
        "equation_FStar.Seq.Properties.tail",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan",
        "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_13d357a23a5e1099db9eb784ff83d223",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "refinement_interpretation_Tm_refine_d06a4002a04168375747565fa0c2dc0f",
        "token_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_FStar.Seq.Base.length",
        "typing_MerkleTree.New.High.Correct.Base.log2",
        "typing_MerkleTree.New.High.Correct.Base.log2c",
        "typing_MerkleTree.New.High.hashes", "well-founded-ordering-on-nat"
      ],
      0,
      "8a4b00ff4aefa331ae1ff8bddfda899e"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log_next",
      1,
      2,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_FStar.Seq.Properties.tail",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess", "equation_Prims.eqtype",
        "equation_Prims.nat",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "int_typing", "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThan", "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_13d357a23a5e1099db9eb784ff83d223",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_43a51d2a8f887f961c9753eac43d02b7",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_99c44f87e8db7c2b2518f780068deb58",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "typing_FStar.Seq.Base.length",
        "typing_MerkleTree.New.High.Correct.Base.log2",
        "typing_MerkleTree.New.High.hashes"
      ],
      0,
      "7cd1fcb967f48fc7a55e80c5df9fdfdc"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log_next",
      2,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_FStar.Integers.W31",
        "constructor_distinct_FStar.Integers.W8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_FStar.Integers.W31@tok",
        "equality_tok_FStar.Integers.W8@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_FStar.Seq.Properties.tail",
        "equation_Lib.IntTypes.unsigned",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hash_seq",
        "equation_MerkleTree.New.High.hash_ss", "equation_Prims.eqtype",
        "equation_Prims.nat",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_MerkleTree.New.High.hash_seq",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "int_typing", "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Integers.Signed__0",
        "projection_inverse_FStar.Integers.Unsigned__0",
        "refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_99c44f87e8db7c2b2518f780068deb58",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "refinement_interpretation_Tm_refine_c5ba2a69ac9e1106e03d09a14fef85ae",
        "typing_FStar.Seq.Base.length",
        "typing_MerkleTree.New.High.Correct.Base.log2"
      ],
      0,
      "ee2ae0481c02cc64e0ce9dadeaca52b2"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log_next",
      3,
      2,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "eq2-interp", "equation_FStar.Seq.Properties.tail",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "l_and-interp",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Division",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
        "refinement_interpretation_Tm_refine_167ef714932ec832fb671890fc3eee6c",
        "refinement_interpretation_Tm_refine_43a51d2a8f887f961c9753eac43d02b7",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_99c44f87e8db7c2b2518f780068deb58",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "token_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Properties.tail",
        "typing_MerkleTree.New.High.Correct.Base.log2",
        "typing_MerkleTree.New.High.hashes"
      ],
      0,
      "a694e96d0ca5fb42a51a087453ff0f93"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_inv_log",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "40e4e512f0e3b172e303be8ad1f246dd"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_inv_log",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "0443c5006dee246556477a647bab4d5d"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_inv_log",
      3,
      2,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_aabbf0a5d49093a6b07e3e5a24007535_3",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2",
        "binder_x_f26957a7e62b271a8736230b1e9c83c1_0", "eq2-interp",
        "equality_tok_Prims.LexTop@tok",
        "equation_FStar.Seq.Properties.head",
        "equation_FStar.Seq.Properties.tail",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "l_and-interp",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Division", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
        "refinement_interpretation_Tm_refine_167ef714932ec832fb671890fc3eee6c",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_43a51d2a8f887f961c9753eac43d02b7",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7381b22713068fe22fae5f1ab9c6c30a",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "token_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Properties.tail",
        "typing_MerkleTree.New.High.Correct.Base.log2",
        "typing_MerkleTree.New.High.hashes", "well-founded-ordering-on-nat"
      ],
      0,
      "8497eb2fefbb105ed9057a66ce85be68"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log_converted_",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess", "equation_Prims.nat",
        "equation_Prims.pos", "int_inversion",
        "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_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_1ae2a0d6b2f4da2d4b0194885669f804",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_b76b169d628564fe0d562183a2374774",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
        "typing_FStar.Seq.Base.length",
        "typing_MerkleTree.New.High.Correct.Base.log2c",
        "typing_MerkleTree.New.High.hashes"
      ],
      0,
      "1e575a4a44023a0e16d3f057557b3e44"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log_converted_",
      2,
      2,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan",
        "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_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_1ae2a0d6b2f4da2d4b0194885669f804",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_75181eeb67c60a598ff554ed274cf85e",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "refinement_interpretation_Tm_refine_b76b169d628564fe0d562183a2374774",
        "typing_FStar.Seq.Base.length",
        "typing_MerkleTree.New.High.Correct.Base.log2c",
        "typing_MerkleTree.New.High.hashes"
      ],
      0,
      "1598aea841350c851a9fa1db1428fcec"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log_converted_",
      3,
      2,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_6e1290e37a6b4e437f899d72093932a2_2",
        "binder_x_89dfa9cb1583ae31cce9fe730922098c_4",
        "binder_x_937f6720cb70e9f19325af7af446ce41_3",
        "binder_x_f26957a7e62b271a8736230b1e9c83c1_0", "eq2-interp",
        "equality_tok_Prims.LexTop@tok",
        "equation_FStar.Seq.Properties.head",
        "equation_FStar.Seq.Properties.tail",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "l_and-interp",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.lemma_tail_slice",
        "lemma_FStar.Seq.Properties.slice_is_empty",
        "lemma_FStar.Seq.Properties.slice_slice",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Division", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThan", "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_13d357a23a5e1099db9eb784ff83d223",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_167ef714932ec832fb671890fc3eee6c",
        "refinement_interpretation_Tm_refine_1ae2a0d6b2f4da2d4b0194885669f804",
        "refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5",
        "refinement_interpretation_Tm_refine_3275c6670c647fe05603aaa27ba49f71",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_43a51d2a8f887f961c9753eac43d02b7",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "refinement_interpretation_Tm_refine_b138bd5848d4184f7632587e6e4bcf9f",
        "refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_fd00a3cd1d1731fad0b4624cc07e2a72",
        "token_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "token_correspondence_Prims.pow2.fuel_instrumented", "true_interp",
        "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
        "typing_FStar.Seq.Properties.tail",
        "typing_MerkleTree.New.High.Correct.Base.log2",
        "typing_MerkleTree.New.High.Correct.Base.log2c",
        "typing_MerkleTree.New.High.hashes", "well-founded-ordering-on-nat"
      ],
      0,
      "2b37b2fefa63a7d58055f8f5bc2c8401"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log_converted",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess", "equation_Prims.nat",
        "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_54b601985451a2432a353b711858af42",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
        "typing_MerkleTree.New.High.hashes"
      ],
      0,
      "7ffd27a19e11e6d87686d91861c91faa"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log_converted",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_Prims.nat", "int_inversion", "primitive_Prims.op_Addition",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_54b601985451a2432a353b711858af42",
        "typing_MerkleTree.New.High.Correct.Base.log2c"
      ],
      0,
      "279a1aaa1b82a54b58b276648d25b50c"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_inv_log_converted_",
      1,
      2,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_GreaterThan", "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_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_95b3ada44cf62e5139914056c335f5ce",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "refinement_interpretation_Tm_refine_b76b169d628564fe0d562183a2374774",
        "refinement_interpretation_Tm_refine_eeb34a6663fec3915a03d46b7a3fadb8",
        "typing_MerkleTree.New.High.Correct.Base.log2c",
        "typing_MerkleTree.New.High.hashes"
      ],
      0,
      "147753ef6172921c78d316e7ec9722cf"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_inv_log_converted_",
      2,
      2,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess", "equation_Prims.nat",
        "equation_Prims.pos", "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_GreaterThan", "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_11aac687a17585bf4353f1ce9679520f",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_95b3ada44cf62e5139914056c335f5ce",
        "refinement_interpretation_Tm_refine_b76b169d628564fe0d562183a2374774",
        "typing_MerkleTree.New.High.Correct.Base.log2c",
        "typing_MerkleTree.New.High.hashes"
      ],
      0,
      "2277e19b1e62ca0cb65f75bf6812f312"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_inv_log_converted_",
      3,
      2,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_inv.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_inv_log.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.mt_hashes_inv.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.mt_hashes_inv_log.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_5e20d151293c9e40e5203cbcff29aebe_1",
        "binder_x_6e1290e37a6b4e437f899d72093932a2_2",
        "binder_x_7366e78b0557d93261fa59449d67a4f4_3",
        "binder_x_ac6efc433989deefa86f3df7c09123f0_4",
        "binder_x_f26957a7e62b271a8736230b1e9c83c1_0", "bool_inversion",
        "bool_typing", "eq2-interp", "equality_tok_Prims.LexTop@tok",
        "equation_FStar.Seq.Properties.head",
        "equation_FStar.Seq.Properties.tail",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_inv.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_inv_log.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "l_and-interp",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.lemma_tail_slice",
        "lemma_FStar.Seq.Properties.slice_slice",
        "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_2",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Division", "primitive_Prims.op_Equality",
        "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThan",
        "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_13d357a23a5e1099db9eb784ff83d223",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_167ef714932ec832fb671890fc3eee6c",
        "refinement_interpretation_Tm_refine_1ae2a0d6b2f4da2d4b0194885669f804",
        "refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5",
        "refinement_interpretation_Tm_refine_319130ca780c778653844ecfc44d9c4d",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_3af864a8d79f95a13ea6e1f5b534a63e",
        "refinement_interpretation_Tm_refine_43a51d2a8f887f961c9753eac43d02b7",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "refinement_interpretation_Tm_refine_b138bd5848d4184f7632587e6e4bcf9f",
        "refinement_interpretation_Tm_refine_c931a3602a0fba1a90727d7f737258ec",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_da1b0dfb8283502ec162998a8bbb6431",
        "refinement_interpretation_Tm_refine_eeb34a6663fec3915a03d46b7a3fadb8",
        "token_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "token_correspondence_Prims.pow2.fuel_instrumented", "true_interp",
        "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
        "typing_FStar.Seq.Properties.tail",
        "typing_MerkleTree.New.High.Correct.Base.log2",
        "typing_MerkleTree.New.High.Correct.Base.log2c",
        "typing_MerkleTree.New.High.hashes", "well-founded-ordering-on-nat"
      ],
      0,
      "c1b4bb411fe7d6373ca5057a461a79e7"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_inv_log_converted",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess", "equation_Prims.nat",
        "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "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_01931cc5b3f69d2d0bf4a7813a1448f8",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_b44fa187a56ba3501fc0af40734dcf78",
        "typing_MerkleTree.New.High.hashes"
      ],
      0,
      "14f04893db1f330a50d9f784bb63b1d1"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_inv_log_converted",
      2,
      2,
      1,
      [
        "@query", "primitive_Prims.op_LessThan",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "59f0659c224ae2494222e6effd9e42e1"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_inv_log_converted",
      3,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_Prims.nat", "int_inversion", "primitive_Prims.op_Addition",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b44fa187a56ba3501fc0af40734dcf78",
        "typing_MerkleTree.New.High.Correct.Base.log2c"
      ],
      0,
      "df38e0efb32527738465dbdede2cc0c8"
    ],
    [
      "MerkleTree.New.High.Correct.Base.hash_seq_lift",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "6d6d1080f7689667a72167ef999057b8"
    ],
    [
      "MerkleTree.New.High.Correct.Base.hash_seq_lift",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "b7244cd43f26dcc6233727568cbfc052"
    ],
    [
      "MerkleTree.New.High.Correct.Base.hash_seq_lift",
      3,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_de57e94726f1653c4e53f75ab929ebb4_1",
        "binder_x_f26957a7e62b271a8736230b1e9c83c1_0",
        "equality_tok_Prims.LexTop@tok",
        "equation_FStar.Seq.Properties.cons",
        "equation_FStar.Seq.Properties.tail",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.Spec.hashes", "equation_Prims.eqtype",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "int_typing", "kinding_MerkleTree.Spec.padded_hash@tok",
        "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_410063e53bf3eaf2e0e7e89fc8ca98c5",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length",
        "typing_MerkleTree.New.High.hash", "well-founded-ordering-on-nat"
      ],
      0,
      "5c58a5a3fcdfa36173dca85ed004c8d6"
    ],
    [
      "MerkleTree.New.High.Correct.Base.hash_seq_lift_index",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_e498fb51261db037ef331c43a4bc992d",
        "typing_MerkleTree.New.High.Correct.Base.hash_seq_lift"
      ],
      0,
      "40138fe733992e2d10ce958598b0179c"
    ],
    [
      "MerkleTree.New.High.Correct.Base.hash_seq_lift_index",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "int_inversion",
        "refinement_interpretation_Tm_refine_29d14ee2bb9cf524df1872435a3550b1",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_e498fb51261db037ef331c43a4bc992d",
        "typing_MerkleTree.New.High.Correct.Base.hash_seq_lift"
      ],
      0,
      "597f86c88e799c101fe7ff705b90acc6"
    ],
    [
      "MerkleTree.New.High.Correct.Base.hash_seq_lift_index",
      3,
      2,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.hash_seq_lift.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.hash_seq_lift.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_de57e94726f1653c4e53f75ab929ebb4_1",
        "binder_x_f26957a7e62b271a8736230b1e9c83c1_0",
        "data_typing_intro_MerkleTree.Spec.HRaw@tok",
        "equality_tok_Prims.LexTop@tok",
        "equation_FStar.Seq.Properties.cons",
        "equation_FStar.Seq.Properties.head",
        "equation_FStar.Seq.Properties.tail",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.Spec.hash", "equation_MerkleTree.Spec.hashes",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.hash_seq_lift.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "kinding_MerkleTree.Spec.padded_hash@tok",
        "lemma_FStar.Seq.Base.lemma_create_len",
        "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_index_slice",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0e6f721cd0df666a9f5eccd102658f1e",
        "refinement_interpretation_Tm_refine_167ef714932ec832fb671890fc3eee6c",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
        "refinement_interpretation_Tm_refine_baff442d34964c1f9d59a57f597a5da1",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_e498fb51261db037ef331c43a4bc992d",
        "token_correspondence_MerkleTree.New.High.Correct.Base.hash_seq_lift.fuel_instrumented",
        "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length",
        "typing_FStar.Seq.Properties.head",
        "typing_MerkleTree.New.High.Correct.Base.hash_seq_lift",
        "typing_MerkleTree.New.High.hash", "well-founded-ordering-on-nat"
      ],
      0,
      "700996f5f8db8804d92be84de4976b16"
    ],
    [
      "MerkleTree.New.High.Correct.Base.create_pads",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "7c57bd774e7f207e75476d23c987c5f6"
    ],
    [
      "MerkleTree.New.High.Correct.Base.create_pads",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "data_typing_intro_MerkleTree.Spec.HPad@tok",
        "kinding_MerkleTree.Spec.padded_hash@tok",
        "lemma_FStar.Seq.Base.lemma_create_len"
      ],
      0,
      "702a90246cfc17672c0b08c39f49a771"
    ],
    [
      "MerkleTree.New.High.Correct.Base.hash_seq_spec",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.Spec.hashes", "equation_Prims.nat",
        "equation_Prims.pos", "int_inversion",
        "kinding_MerkleTree.Spec.padded_hash@tok",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0feb76eeb65cc099e0a482acd65b1bcc",
        "refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
        "refinement_interpretation_Tm_refine_33e9e47c0adfd5c76673081bc3b1f7a6",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "refinement_interpretation_Tm_refine_e498fb51261db037ef331c43a4bc992d",
        "typing_FStar.Seq.Base.length",
        "typing_MerkleTree.New.High.Correct.Base.hash_seq_lift",
        "typing_MerkleTree.New.High.Correct.Base.log2",
        "typing_MerkleTree.New.High.Correct.Base.log2c",
        "typing_MerkleTree.New.High.hash", "typing_Prims.pow2"
      ],
      0,
      "78a2c74e7af5613e3470f8473b6eb3da"
    ],
    [
      "MerkleTree.New.High.Correct.Base.hash_seq_spec_index_raw",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.hash_seq_lift.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.Spec.merkle_tree", "equation_Prims.pos",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
        "refinement_interpretation_Tm_refine_33e9e47c0adfd5c76673081bc3b1f7a6",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "refinement_interpretation_Tm_refine_e166b70fde2cd9152c503654048d8315",
        "refinement_interpretation_Tm_refine_e498fb51261db037ef331c43a4bc992d",
        "typing_FStar.Seq.Base.length",
        "typing_MerkleTree.New.High.Correct.Base.hash_seq_lift",
        "typing_MerkleTree.New.High.Correct.Base.hash_seq_spec",
        "typing_MerkleTree.New.High.Correct.Base.log2",
        "typing_MerkleTree.New.High.Correct.Base.log2c",
        "typing_MerkleTree.New.High.hash", "typing_Prims.pow2"
      ],
      0,
      "19a3be1512d9282ca3c8cc588fb8c43e"
    ],
    [
      "MerkleTree.New.High.Correct.Base.hash_seq_spec_index_raw",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.hash_seq_lift.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_MerkleTree.New.High.Correct.Base.create_pads",
        "equation_MerkleTree.New.High.Correct.Base.hash_seq_spec",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.Spec.hashes", "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "kinding_MerkleTree.Spec.padded_hash@tok",
        "lemma_FStar.Seq.Base.lemma_index_app1",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
        "refinement_interpretation_Tm_refine_33e9e47c0adfd5c76673081bc3b1f7a6",
        "refinement_interpretation_Tm_refine_3a643af648e0e51f8493b1b7e51bd56c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_6f92e8c304c36f55e42632b60c82c691",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_e498fb51261db037ef331c43a4bc992d",
        "typing_FStar.Seq.Base.length",
        "typing_MerkleTree.New.High.Correct.Base.create_pads",
        "typing_MerkleTree.New.High.Correct.Base.hash_seq_lift",
        "typing_MerkleTree.New.High.Correct.Base.log2",
        "typing_MerkleTree.New.High.hash"
      ],
      0,
      "ff0ecfa110a1c757ec847dec6b6d6a02"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_next_rel_lift_even",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "b2t_def", "bool_inversion", "bool_typing",
        "data_typing_intro_MerkleTree.Spec.HRaw@tok",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.Spec.hash",
        "equation_MerkleTree.Spec.merkle_tree", "equation_Prims.eqtype",
        "equation_Prims.l_and", "equation_Prims.nat", "equation_Prims.pos",
        "equation_Prims.squash",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "int_typing", "kinding_MerkleTree.Spec.padded_hash@tok",
        "l_and-interp", "lemma_FStar.Seq.Base.lemma_create_len",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Division",
        "primitive_Prims.op_Equality", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
        "refinement_interpretation_Tm_refine_167ef714932ec832fb671890fc3eee6c",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_59122260c77179a912aff4679b32096c",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_99c44f87e8db7c2b2518f780068deb58",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "refinement_interpretation_Tm_refine_cdc09d6032c37371558f1d5d77d7bd2c",
        "refinement_interpretation_Tm_refine_e166b70fde2cd9152c503654048d8315",
        "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Properties.head",
        "typing_MerkleTree.New.High.Correct.Base.log2",
        "typing_MerkleTree.New.High.Correct.Base.log2c",
        "typing_MerkleTree.New.High.hash"
      ],
      0,
      "27d5a9c4c387bfedb19eaaab4fb7e4a8"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_next_rel_lift_even",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "13284f21beccfc692b5ceb5ca690ca90"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_next_rel_lift_even",
      3,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.hash_seq_lift.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_MerkleTree.Spec.HPad",
        "constructor_distinct_MerkleTree.Spec.HRaw",
        "data_typing_intro_MerkleTree.Spec.HPad@tok",
        "equation_MerkleTree.New.High.Correct.Base.create_pads",
        "equation_MerkleTree.New.High.Correct.Base.hash_seq_spec",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.Correct.Base.mt_hashes_next_rel",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.Spec.hashes",
        "equation_MerkleTree.Spec.hs_next_rel",
        "equation_MerkleTree.Spec.merkle_tree",
        "equation_MerkleTree.Spec.mt_next_rel",
        "equation_MerkleTree.Spec.padded_hash_fun", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "kinding_MerkleTree.Spec.padded_hash@tok",
        "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_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Division", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_MerkleTree.Spec.HPad_hsz",
        "projection_inverse_MerkleTree.Spec.HRaw_hr",
        "projection_inverse_MerkleTree.Spec.HRaw_hsz",
        "refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
        "refinement_interpretation_Tm_refine_33e9e47c0adfd5c76673081bc3b1f7a6",
        "refinement_interpretation_Tm_refine_3a643af648e0e51f8493b1b7e51bd56c",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_59122260c77179a912aff4679b32096c",
        "refinement_interpretation_Tm_refine_6f92e8c304c36f55e42632b60c82c691",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_99c44f87e8db7c2b2518f780068deb58",
        "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_cdc09d6032c37371558f1d5d77d7bd2c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_e166b70fde2cd9152c503654048d8315",
        "refinement_interpretation_Tm_refine_e498fb51261db037ef331c43a4bc992d",
        "refinement_interpretation_Tm_refine_f97fad2c1fb2db1c8f88c401525f4a64",
        "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
        "typing_MerkleTree.New.High.Correct.Base.create_pads",
        "typing_MerkleTree.New.High.Correct.Base.hash_seq_lift",
        "typing_MerkleTree.New.High.Correct.Base.hash_seq_spec",
        "typing_MerkleTree.New.High.Correct.Base.log2",
        "typing_MerkleTree.New.High.Correct.Base.log2c",
        "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.Spec.padded_hash_fun", "typing_Prims.pow2"
      ],
      0,
      "c0d49fa96085add7110914f304fd75d3"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_next_rel_lift_odd",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "bool_typing",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.Spec.hashes",
        "equation_MerkleTree.Spec.merkle_tree", "equation_Prims.eqtype",
        "equation_Prims.l_and", "equation_Prims.nat", "equation_Prims.pos",
        "equation_Prims.squash",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "kinding_MerkleTree.Spec.padded_hash@tok", "l_and-interp",
        "lemma_FStar.Seq.Base.lemma_len_upd", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Division",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
        "refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_59122260c77179a912aff4679b32096c",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_99c44f87e8db7c2b2518f780068deb58",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "refinement_interpretation_Tm_refine_cdc09d6032c37371558f1d5d77d7bd2c",
        "refinement_interpretation_Tm_refine_e166b70fde2cd9152c503654048d8315",
        "typing_FStar.Seq.Base.length",
        "typing_MerkleTree.New.High.Correct.Base.log2",
        "typing_MerkleTree.New.High.Correct.Base.log2c",
        "typing_MerkleTree.New.High.hash", "typing_Prims.pow2"
      ],
      0,
      "6ab44c471f819719abd4ac1dc5ffc94d"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_next_rel_lift_odd",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "a07645150275bdc896554488018b2657"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_next_rel_lift_odd",
      3,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.hash_seq_lift.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_MerkleTree.Spec.HPad",
        "constructor_distinct_MerkleTree.Spec.HRaw",
        "data_typing_intro_MerkleTree.Spec.HPad@tok",
        "data_typing_intro_MerkleTree.Spec.HRaw@tok",
        "equation_FStar.Seq.Properties.cons",
        "equation_FStar.Seq.Properties.head",
        "equation_FStar.Seq.Properties.last",
        "equation_FStar.Seq.Properties.tail",
        "equation_MerkleTree.New.High.Correct.Base.create_pads",
        "equation_MerkleTree.New.High.Correct.Base.hash_seq_spec",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.Correct.Base.mt_hashes_next_rel",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.Spec.hash", "equation_MerkleTree.Spec.hashes",
        "equation_MerkleTree.Spec.hs_next_rel",
        "equation_MerkleTree.Spec.merkle_tree",
        "equation_MerkleTree.Spec.mt_next_rel",
        "equation_MerkleTree.Spec.padded_hash_fun", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.hash_seq_lift.fuel_instrumented",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
        "int_typing", "kinding_MerkleTree.Spec.padded_hash@tok",
        "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_app2",
        "lemma_FStar.Seq.Base.lemma_index_create",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_index_upd1",
        "lemma_FStar.Seq.Base.lemma_index_upd2",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.cons_index_slice",
        "lemma_MerkleTree.New.High.Correct.Base.seq_head_cons",
        "lemma_MerkleTree.New.High.Correct.Base.seq_tail_cons",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Division",
        "primitive_Prims.op_LessThan", "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",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_MerkleTree.Spec.HPad_hsz",
        "projection_inverse_MerkleTree.Spec.HRaw_hr",
        "projection_inverse_MerkleTree.Spec.HRaw_hsz",
        "refinement_interpretation_Tm_refine_09d2e9ab3b9c121b24316d151747e281",
        "refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
        "refinement_interpretation_Tm_refine_167ef714932ec832fb671890fc3eee6c",
        "refinement_interpretation_Tm_refine_33e9e47c0adfd5c76673081bc3b1f7a6",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_3a643af648e0e51f8493b1b7e51bd56c",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_59122260c77179a912aff4679b32096c",
        "refinement_interpretation_Tm_refine_6f92e8c304c36f55e42632b60c82c691",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_99c44f87e8db7c2b2518f780068deb58",
        "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_cdc09d6032c37371558f1d5d77d7bd2c",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_df81b3f17797c6f405c1dbb191651292",
        "refinement_interpretation_Tm_refine_e166b70fde2cd9152c503654048d8315",
        "refinement_interpretation_Tm_refine_e498fb51261db037ef331c43a4bc992d",
        "refinement_interpretation_Tm_refine_f97fad2c1fb2db1c8f88c401525f4a64",
        "token_correspondence_MerkleTree.New.High.Correct.Base.hash_seq_lift.fuel_instrumented",
        "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
        "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
        "typing_FStar.Seq.Properties.head",
        "typing_FStar.Seq.Properties.last",
        "typing_FStar.Seq.Properties.tail",
        "typing_MerkleTree.New.High.Correct.Base.create_pads",
        "typing_MerkleTree.New.High.Correct.Base.hash_seq_lift",
        "typing_MerkleTree.New.High.Correct.Base.hash_seq_spec",
        "typing_MerkleTree.New.High.Correct.Base.log2",
        "typing_MerkleTree.New.High.Correct.Base.log2c",
        "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.Spec.padded_hash_fun"
      ],
      0,
      "46ce681590d098debbb0dbce1d7df3ea"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_next_rel_next_even",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_Prims.eqtype", "equation_Prims.l_and",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "l_and-interp", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Division", "primitive_Prims.op_Equality",
        "primitive_Prims.op_Modulus", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_59122260c77179a912aff4679b32096c",
        "refinement_interpretation_Tm_refine_99c44f87e8db7c2b2518f780068deb58",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "refinement_interpretation_Tm_refine_cdc09d6032c37371558f1d5d77d7bd2c",
        "typing_MerkleTree.New.High.Correct.Base.log2"
      ],
      0,
      "c9546763aaac29371d1a954b947ca04e"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_next_rel_next_even",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "73ae6aa25964be71a81059fc57eb3b85"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_hashes_next_rel_next_even",
      3,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_MerkleTree.New.High.Correct.Base.hash_seq_spec",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.Spec.merkle_tree", "equation_Prims.nat",
        "equation_Prims.pos", "int_inversion", "primitive_Prims.op_Division",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_59122260c77179a912aff4679b32096c",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_99c44f87e8db7c2b2518f780068deb58",
        "refinement_interpretation_Tm_refine_cdc09d6032c37371558f1d5d77d7bd2c",
        "refinement_interpretation_Tm_refine_e166b70fde2cd9152c503654048d8315",
        "typing_FStar.Seq.Base.length",
        "typing_MerkleTree.New.High.Correct.Base.log2c",
        "typing_MerkleTree.New.High.hash"
      ],
      0,
      "ed2bed40466a9c0f616896742acfa6e0"
    ],
    [
      "MerkleTree.New.High.Correct.Base.hash_seq_spec_full",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "data_typing_intro_MerkleTree.Spec.HRaw@tok",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.Spec.hash",
        "equation_MerkleTree.Spec.merkle_tree", "equation_Prims.pos",
        "function_token_typing_Prims.__cache_version_number__",
        "kinding_MerkleTree.Spec.padded_hash@tok",
        "lemma_FStar.Seq.Base.lemma_len_upd", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
        "refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
        "refinement_interpretation_Tm_refine_33e9e47c0adfd5c76673081bc3b1f7a6",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "refinement_interpretation_Tm_refine_e166b70fde2cd9152c503654048d8315",
        "typing_FStar.Seq.Base.length",
        "typing_MerkleTree.New.High.Correct.Base.hash_seq_spec",
        "typing_MerkleTree.New.High.Correct.Base.log2",
        "typing_MerkleTree.New.High.Correct.Base.log2c",
        "typing_MerkleTree.New.High.hash", "typing_Prims.pow2"
      ],
      0,
      "1ea75a13b9a8d76223653dcec5592d54"
    ],
    [
      "MerkleTree.New.High.Correct.Base.hash_seq_spec_full_index_raw",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.Spec.merkle_tree", "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "kinding_MerkleTree.Spec.padded_hash@tok",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
        "refinement_interpretation_Tm_refine_33e9e47c0adfd5c76673081bc3b1f7a6",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "refinement_interpretation_Tm_refine_e166b70fde2cd9152c503654048d8315",
        "typing_FStar.Seq.Base.length",
        "typing_MerkleTree.New.High.Correct.Base.hash_seq_spec_full",
        "typing_MerkleTree.New.High.Correct.Base.log2",
        "typing_MerkleTree.New.High.hash"
      ],
      0,
      "be89748eb6764804933960a14f8b4006"
    ],
    [
      "MerkleTree.New.High.Correct.Base.hash_seq_spec_full_index_raw",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "data_typing_intro_MerkleTree.Spec.HRaw@tok",
        "equation_MerkleTree.New.High.Correct.Base.hash_seq_spec",
        "equation_MerkleTree.New.High.Correct.Base.hash_seq_spec_full",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.Spec.hash", "equation_MerkleTree.Spec.hashes",
        "equation_MerkleTree.Spec.merkle_tree", "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "kinding_MerkleTree.Spec.padded_hash@tok",
        "lemma_FStar.Seq.Base.lemma_index_upd2",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
        "refinement_interpretation_Tm_refine_33e9e47c0adfd5c76673081bc3b1f7a6",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_6f92e8c304c36f55e42632b60c82c691",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_df81b3f17797c6f405c1dbb191651292",
        "refinement_interpretation_Tm_refine_e166b70fde2cd9152c503654048d8315",
        "typing_FStar.Seq.Base.length",
        "typing_MerkleTree.New.High.Correct.Base.hash_seq_spec",
        "typing_MerkleTree.New.High.Correct.Base.log2",
        "typing_MerkleTree.New.High.hash"
      ],
      0,
      "31b1b8130ac33dade2706cc9e8213b0e"
    ],
    [
      "MerkleTree.New.High.Correct.Base.hash_seq_spec_full_case_true",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_typing",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.Spec.merkle_tree", "equation_Prims.pos",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
        "refinement_interpretation_Tm_refine_33e9e47c0adfd5c76673081bc3b1f7a6",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "refinement_interpretation_Tm_refine_e166b70fde2cd9152c503654048d8315",
        "typing_FStar.Seq.Base.length",
        "typing_MerkleTree.New.High.Correct.Base.hash_seq_spec_full",
        "typing_MerkleTree.New.High.Correct.Base.log2",
        "typing_MerkleTree.New.High.Correct.Base.log2c",
        "typing_MerkleTree.New.High.hash", "typing_Prims.pow2"
      ],
      0,
      "d09585788f380836084b1b7f7ae53248"
    ],
    [
      "MerkleTree.New.High.Correct.Base.hash_seq_spec_full_case_true",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "data_typing_intro_MerkleTree.Spec.HRaw@tok",
        "equation_MerkleTree.New.High.Correct.Base.hash_seq_spec",
        "equation_MerkleTree.New.High.Correct.Base.hash_seq_spec_full",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.Spec.hash", "equation_MerkleTree.Spec.hashes",
        "equation_MerkleTree.Spec.merkle_tree",
        "function_token_typing_Prims.__cache_version_number__",
        "kinding_MerkleTree.Spec.padded_hash@tok",
        "lemma_FStar.Seq.Base.lemma_index_upd1",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
        "refinement_interpretation_Tm_refine_33e9e47c0adfd5c76673081bc3b1f7a6",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_e166b70fde2cd9152c503654048d8315",
        "typing_FStar.Seq.Base.length",
        "typing_MerkleTree.New.High.Correct.Base.hash_seq_spec",
        "typing_MerkleTree.New.High.Correct.Base.log2",
        "typing_MerkleTree.New.High.hash"
      ],
      0,
      "09c7b191d8d92cd6ddeb512fdf8e4f46"
    ],
    [
      "MerkleTree.New.High.Correct.Base.hash_seq_spec_full_even_next",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_Prims.eqtype", "equation_Prims.l_and",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "l_and-interp", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Division", "primitive_Prims.op_Equality",
        "primitive_Prims.op_Modulus", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_59122260c77179a912aff4679b32096c",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "refinement_interpretation_Tm_refine_cdc09d6032c37371558f1d5d77d7bd2c",
        "typing_MerkleTree.New.High.Correct.Base.log2"
      ],
      0,
      "6fec8e59de6a1e7cccd2768ab6328e98"
    ],
    [
      "MerkleTree.New.High.Correct.Base.hash_seq_spec_full_even_next",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "c196296d91e4f00b6e33a88d810b29e0"
    ],
    [
      "MerkleTree.New.High.Correct.Base.hash_seq_spec_full_even_next",
      3,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.hash_seq_lift.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "bool_inversion", "data_typing_intro_MerkleTree.Spec.HPad@tok",
        "data_typing_intro_MerkleTree.Spec.HRaw@tok",
        "equation_MerkleTree.New.High.Correct.Base.create_pads",
        "equation_MerkleTree.New.High.Correct.Base.hash_seq_spec",
        "equation_MerkleTree.New.High.Correct.Base.hash_seq_spec_full",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.Spec.hash", "equation_MerkleTree.Spec.hashes",
        "equation_MerkleTree.Spec.hs_next_rel",
        "equation_MerkleTree.Spec.merkle_tree",
        "equation_MerkleTree.Spec.mt_next_rel", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.hash_seq_lift.fuel_instrumented",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
        "int_typing", "kinding_MerkleTree.Spec.padded_hash@tok",
        "lemma_FStar.Seq.Base.lemma_index_app2",
        "lemma_FStar.Seq.Base.lemma_index_create",
        "lemma_FStar.Seq.Base.lemma_index_upd1",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.Seq.Base.lemma_len_upd", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Division", "primitive_Prims.op_LessThan",
        "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_13d357a23a5e1099db9eb784ff83d223",
        "refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
        "refinement_interpretation_Tm_refine_3a643af648e0e51f8493b1b7e51bd56c",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_59122260c77179a912aff4679b32096c",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_cdc09d6032c37371558f1d5d77d7bd2c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_e166b70fde2cd9152c503654048d8315",
        "refinement_interpretation_Tm_refine_e498fb51261db037ef331c43a4bc992d",
        "token_correspondence_MerkleTree.New.High.Correct.Base.hash_seq_lift.fuel_instrumented",
        "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.length",
        "typing_MerkleTree.New.High.Correct.Base.create_pads",
        "typing_MerkleTree.New.High.Correct.Base.log2",
        "typing_MerkleTree.New.High.Correct.Base.log2c",
        "typing_MerkleTree.New.High.hash"
      ],
      0,
      "2f8f10edee91922bbb8292ee9c02f6b2"
    ],
    [
      "MerkleTree.New.High.Correct.Base.hash_seq_spec_full_odd_next",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Prims.squash",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "l_and-interp", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Division", "primitive_Prims.op_Equality",
        "primitive_Prims.op_Modulus", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_59122260c77179a912aff4679b32096c",
        "refinement_interpretation_Tm_refine_99c44f87e8db7c2b2518f780068deb58",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "refinement_interpretation_Tm_refine_cdc09d6032c37371558f1d5d77d7bd2c",
        "typing_MerkleTree.New.High.Correct.Base.log2"
      ],
      0,
      "6b0f0bc169d4ab09a4da9719344b7b41"
    ],
    [
      "MerkleTree.New.High.Correct.Base.hash_seq_spec_full_odd_next",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "ca94b46c2dfc6f7a5f09634caac42f8d"
    ],
    [
      "MerkleTree.New.High.Correct.Base.hash_seq_spec_full_odd_next",
      3,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.hash_seq_lift.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
        "constructor_distinct_MerkleTree.Spec.HPad",
        "constructor_distinct_MerkleTree.Spec.HRaw",
        "data_typing_intro_MerkleTree.Spec.HPad@tok",
        "data_typing_intro_MerkleTree.Spec.HRaw@tok",
        "equation_FStar.Seq.Properties.cons",
        "equation_FStar.Seq.Properties.head",
        "equation_FStar.Seq.Properties.tail",
        "equation_MerkleTree.New.High.Correct.Base.create_pads",
        "equation_MerkleTree.New.High.Correct.Base.hash_seq_spec",
        "equation_MerkleTree.New.High.Correct.Base.hash_seq_spec_full",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.Spec.hash", "equation_MerkleTree.Spec.hashes",
        "equation_MerkleTree.Spec.hs_next_rel",
        "equation_MerkleTree.Spec.merkle_tree",
        "equation_MerkleTree.Spec.mt_next_rel",
        "equation_MerkleTree.Spec.padded_hash_fun", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.hash_seq_lift.fuel_instrumented",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "kinding_MerkleTree.Spec.padded_hash@tok",
        "lemma_FStar.Seq.Base.lemma_create_len",
        "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_index_upd1",
        "lemma_FStar.Seq.Base.lemma_index_upd2",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.Seq.Base.lemma_len_upd", "lemma_FStar.UInt.pow2_values",
        "lemma_Lib.IntTypes.pow2_2",
        "lemma_MerkleTree.New.High.Correct.Base.seq_head_cons",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Division", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThan", "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",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_MerkleTree.Spec.HPad_hsz",
        "projection_inverse_MerkleTree.Spec.HRaw_hr",
        "projection_inverse_MerkleTree.Spec.HRaw_hsz",
        "refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
        "refinement_interpretation_Tm_refine_167ef714932ec832fb671890fc3eee6c",
        "refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
        "refinement_interpretation_Tm_refine_3a643af648e0e51f8493b1b7e51bd56c",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_59122260c77179a912aff4679b32096c",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_99c44f87e8db7c2b2518f780068deb58",
        "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_cdc09d6032c37371558f1d5d77d7bd2c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_df81b3f17797c6f405c1dbb191651292",
        "refinement_interpretation_Tm_refine_e166b70fde2cd9152c503654048d8315",
        "refinement_interpretation_Tm_refine_e498fb51261db037ef331c43a4bc992d",
        "token_correspondence_MerkleTree.New.High.Correct.Base.hash_seq_lift.fuel_instrumented",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.index",
        "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Properties.head",
        "typing_FStar.Seq.Properties.tail",
        "typing_MerkleTree.New.High.Correct.Base.create_pads",
        "typing_MerkleTree.New.High.Correct.Base.log2",
        "typing_MerkleTree.New.High.Correct.Base.log2c",
        "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.Spec.padded_hash_fun"
      ],
      0,
      "b08c1bf30358978c220f9daf3c3c8236"
    ],
    [
      "MerkleTree.New.High.Correct.Base.hash_seq_spec_full_next",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Division",
        "primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_59122260c77179a912aff4679b32096c",
        "refinement_interpretation_Tm_refine_99c44f87e8db7c2b2518f780068deb58",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "refinement_interpretation_Tm_refine_cdc09d6032c37371558f1d5d77d7bd2c",
        "typing_MerkleTree.New.High.Correct.Base.log2"
      ],
      0,
      "cc2c31151c48675eed398af9b422b2f0"
    ],
    [
      "MerkleTree.New.High.Correct.Base.hash_seq_spec_full_next",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "3dafdb5ffa395533882d13218bb954bd"
    ],
    [
      "MerkleTree.New.High.Correct.Base.hash_seq_spec_full_next",
      3,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
        "primitive_Prims.op_Modulus", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_99c44f87e8db7c2b2518f780068deb58"
      ],
      0,
      "99460815140beb3267b472e9a3c6dc9e"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_rhs_inv",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "f8d895d6900bb23b3492b9801344b19f"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_rhs_inv",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "2b48ea9ea4f637b524c5cd26eb36c6b5"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_rhs_inv",
      3,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_53091569903cae77b4a60be8a17a11bc_4",
        "binder_x_7802c6c7540d3455819384f8c2a0a0c8_3",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2",
        "binder_x_f26957a7e62b271a8736230b1e9c83c1_0",
        "binder_x_f537159ed795b314b4e58c260361ae86_5", "bool_inversion",
        "equality_tok_Prims.LexTop@tok",
        "equation_FStar.Seq.Properties.tail",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.Spec.merkle_tree", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan",
        "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_13d357a23a5e1099db9eb784ff83d223",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_765c5038a14ad1a170ebaf2c2e8ec7c8",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "refinement_interpretation_Tm_refine_e166b70fde2cd9152c503654048d8315",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_MerkleTree.New.High.Correct.Base.log2",
        "typing_MerkleTree.New.High.Correct.Base.log2c",
        "typing_MerkleTree.New.High.hash", "typing_Prims.pow2",
        "well-founded-ordering-on-nat"
      ],
      0,
      "946ed8f9ddb5b0d4f7d60006d03009c0"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_base",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "a69c9e8cb1cda66034e9bb784e7ee099"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_base",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.merge_hs.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_olds_inv.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.merge_hs.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "eq2-interp", "equation_FStar.Seq.Properties.head",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess",
        "equation_MerkleTree.New.High.mt_wf_elts",
        "equation_MerkleTree.New.High.offset_of", "equation_Prims.nat",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_olds_inv.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "fuel_guarded_inversion_MerkleTree.New.High.merkle_tree",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "l_and-interp",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_MerkleTree.New.High.Correct.Base.merge_hs_index",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "proj_equation_MerkleTree.New.High.MT_hash_fun",
        "proj_equation_MerkleTree.New.High.MT_hs",
        "proj_equation_MerkleTree.New.High.MT_i",
        "proj_equation_MerkleTree.New.High.MT_j",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_167ef714932ec832fb671890fc3eee6c",
        "refinement_interpretation_Tm_refine_22125f28c20990597c03dac8bb18819e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7f59e1d21662a5bb0549ee09247e1710",
        "refinement_interpretation_Tm_refine_881298fb0dff2db17e4149fcf49ad4b9",
        "refinement_interpretation_Tm_refine_995516c5fe04fd93611e610195bbf9ba",
        "refinement_interpretation_Tm_refine_9b2b3e7ac5f300ddc6add4181948ef22",
        "refinement_interpretation_Tm_refine_ad53f3413fd15db5258446e997071714",
        "refinement_interpretation_Tm_refine_bf3340443d6edf0ae4bc4b37060534fb",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.index",
        "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Properties.head",
        "typing_MerkleTree.New.High.__proj__MT__item__hash_fun",
        "typing_MerkleTree.New.High.__proj__MT__item__hs",
        "typing_MerkleTree.New.High.__proj__MT__item__i",
        "typing_MerkleTree.New.High.__proj__MT__item__j",
        "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.New.High.hashes"
      ],
      0,
      "adbf7bd1e027cdaf573b271ad11ffde7"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_spec",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_2a7fb093a521f1abbc6b16d257336c97",
        "refinement_interpretation_Tm_refine_9e2cc9c9dac6b0e7d2a3400258c6016f"
      ],
      0,
      "552e3e194ffa74b3330aca80aabd0780"
    ],
    [
      "MerkleTree.New.High.Correct.Base.mt_inv",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess",
        "equation_MerkleTree.New.High.mt_wf_elts", "equation_Prims.eqtype",
        "equation_Prims.nat",
        "fuel_guarded_inversion_MerkleTree.New.High.merkle_tree",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "int_typing", "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThan",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "proj_equation_MerkleTree.New.High.MT_hs",
        "proj_equation_MerkleTree.New.High.MT_i",
        "proj_equation_MerkleTree.New.High.MT_j",
        "proj_equation_MerkleTree.New.High.MT_rhs",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_42ab70f52fa85ce7b7f41db78958e96d",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7f59e1d21662a5bb0549ee09247e1710",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_881298fb0dff2db17e4149fcf49ad4b9",
        "refinement_interpretation_Tm_refine_995516c5fe04fd93611e610195bbf9ba",
        "refinement_interpretation_Tm_refine_bf3340443d6edf0ae4bc4b37060534fb",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
        "typing_MerkleTree.New.High.Correct.Base.log2c",
        "typing_MerkleTree.New.High.__proj__MT__item__j",
        "typing_MerkleTree.New.High.__proj__MT__item__rhs",
        "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.New.High.hashes"
      ],
      0,
      "d1534a4e5a631f2f263527207d7749b2"
    ]
  ]
]