[
  "4ľ%zvĚ\u0002¬ó0\u0019„q<…°",
  [
    [
      "MerkleTree.New.High.hash",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "e2629defb5357798ad15553b65b897a3"
    ],
    [
      "MerkleTree.New.High.hash_init",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_FStar.Integers.W32",
        "constructor_distinct_FStar.Integers.W63",
        "constructor_distinct_FStar.Integers.W8",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_FStar.Integers.W32@tok",
        "equality_tok_FStar.Integers.W63@tok",
        "equality_tok_FStar.Integers.W8@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
        "equation_MerkleTree.Spec.hash_alg",
        "equation_MerkleTree.Spec.hash_size", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Spec.Hash.Definitions.hash_length",
        "equation_Spec.Hash.Definitions.hash_word_length",
        "equation_Spec.Hash.Definitions.word_length",
        "function_token_typing_Lib.IntTypes.uint8", "int_inversion",
        "lemma_FStar.Seq.Base.lemma_create_len",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "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_64007e4a8c187c3787ce4f8705e9db35",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_Lib.IntTypes.bits", "typing_MerkleTree.Spec.hash_size",
        "typing_Prims.pow2", "typing_Spec.Hash.Definitions.hash_length",
        "typing_tok_Lib.IntTypes.U8@tok",
        "typing_tok_Spec.Hash.Definitions.SHA2_256@tok"
      ],
      0,
      "1d68a6169852770c5f841dde91c2c18d"
    ],
    [
      "MerkleTree.New.High.seq_slice_equal_index",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_0545ca68af3b2fc8df509fb388f7f2ee",
        "refinement_interpretation_Tm_refine_5a8634b460d149c76a5c0476662af1d0"
      ],
      0,
      "3ca8cbb0d9344b4317bd4e50dd38f7f2"
    ],
    [
      "MerkleTree.New.High.seq_slice_equal_index",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion", "bool_typing",
        "equation_Prims.nat", "int_inversion",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "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_0fd1ee098f6569eb754a703d7e7e9875",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5a8634b460d149c76a5c0476662af1d0",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "typing_FStar.Seq.Base.slice"
      ],
      0,
      "7a3a6360d98240f250e28ba0a6e4e00d"
    ],
    [
      "MerkleTree.New.High.seq_slice_more_equal",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5a8634b460d149c76a5c0476662af1d0",
        "refinement_interpretation_Tm_refine_cc7ec1228e62f637b46417d43aae0cfa",
        "typing_FStar.Seq.Base.length"
      ],
      0,
      "3b4b272ba6a14845e1eed74a8acff0b3"
    ],
    [
      "MerkleTree.New.High.seq_slice_more_equal",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_eq_intro",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_MerkleTree.New.High.seq_slice_equal_index",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "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_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
        "refinement_interpretation_Tm_refine_5a8634b460d149c76a5c0476662af1d0",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_cc7ec1228e62f637b46417d43aae0cfa",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice"
      ],
      0,
      "63f8f20240a6102add257110b1f7c5ab"
    ],
    [
      "MerkleTree.New.High.remainder_2_not_1_div",
      1,
      2,
      1,
      [
        "@query", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "138d8e2c872d6a55b903f697c064bfb6"
    ],
    [
      "MerkleTree.New.High.remainder_2_1_div",
      1,
      2,
      1,
      [
        "@query", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "8b49040ce99e096ace404141a1a0b79a"
    ],
    [
      "MerkleTree.New.High.__proj__MT__item__j",
      1,
      2,
      1,
      [
        "@query", "proj_equation_MerkleTree.New.High.MT_i",
        "projection_inverse_MerkleTree.New.High.MT_i"
      ],
      0,
      "207fc2434afdf246692306b2f87ceaad"
    ],
    [
      "MerkleTree.New.High.offset_of",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "primitive_Prims.op_Equality", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "31da290ee9b849bbd5673005aa35f2e3"
    ],
    [
      "MerkleTree.New.High.hs_wf_elts",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_20ef783cabfdc90ae174ed55c128717b_4",
        "binder_x_6e1290e37a6b4e437f899d72093932a2_1",
        "binder_x_89dfa9cb1583ae31cce9fe730922098c_2",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_3",
        "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_11ff5223149858a6ed39dcb0f334332c",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_3275c6670c647fe05603aaa27ba49f71",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "well-founded-ordering-on-nat"
      ],
      0,
      "3ba3f6363a40a49445c40689307f991c"
    ],
    [
      "MerkleTree.New.High.hs_wf_elts_equal",
      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,
      "ebb6736c2ffd01d83345c1e42bdb191a"
    ],
    [
      "MerkleTree.New.High.hs_wf_elts_equal",
      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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b"
      ],
      0,
      "f06ac01b2c8a628c41b6bf8a0ca59cff"
    ],
    [
      "MerkleTree.New.High.hs_wf_elts_equal",
      3,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_38841de65da3d7e9ec6be1f063a8e30a_5",
        "binder_x_6e1290e37a6b4e437f899d72093932a2_1",
        "binder_x_89dfa9cb1583ae31cce9fe730922098c_2",
        "binder_x_89dfa9cb1583ae31cce9fe730922098c_3",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_4",
        "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.hs_wf_elts.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_eq_refl",
        "lemma_MerkleTree.New.High.seq_slice_equal_index",
        "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_03ad6c395cd586145d09934af4be99c5",
        "refinement_interpretation_Tm_refine_0545ca68af3b2fc8df509fb388f7f2ee",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_3275c6670c647fe05603aaa27ba49f71",
        "refinement_interpretation_Tm_refine_3a05cfee9574d769a800024db56a06b2",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5a8634b460d149c76a5c0476662af1d0",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_ad53f3413fd15db5258446e997071714",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
        "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
        "typing_MerkleTree.New.High.hashes", "well-founded-ordering-on-nat"
      ],
      0,
      "ed20b71bdc4b0dacb60b57c7fa3f6d46"
    ],
    [
      "MerkleTree.New.High.mt_wf_elts",
      1,
      2,
      1,
      [
        "@query", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "d1632f66dd2d845f317de7217c854701"
    ],
    [
      "MerkleTree.New.High.hs_wf_elts_empty",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes", "equation_Prims.nat",
        "int_typing", "lemma_FStar.Seq.Base.lemma_create_len",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "typing_FStar.Seq.Base.empty", "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.New.High.hashes"
      ],
      0,
      "518bf322646d1d49a790c1bd1a164ab2"
    ],
    [
      "MerkleTree.New.High.hs_wf_elts_empty",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes", "equation_Prims.nat",
        "int_typing", "lemma_FStar.Seq.Base.lemma_create_len",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "typing_FStar.Seq.Base.empty", "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.New.High.hashes"
      ],
      0,
      "7eb25327f994f682c507bae936c90b7b"
    ],
    [
      "MerkleTree.New.High.hs_wf_elts_empty",
      3,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.hs_wf_elts.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.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.hs_wf_elts.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "l_and-interp",
        "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.Seq.Base.lemma_index_create",
        "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_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_ad53f3413fd15db5258446e997071714",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
        "true_interp", "typing_FStar.Seq.Base.create",
        "typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length",
        "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.New.High.hashes",
        "typing_MerkleTree.New.High.offset_of",
        "well-founded-ordering-on-nat"
      ],
      0,
      "5a2a277989582f049bd0b28e1270b3a1"
    ],
    [
      "MerkleTree.New.High.create_empty_mt",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.mt_wf_elts", "equation_Prims.nat",
        "equation_Prims.pos", "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_create_len",
        "primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_MerkleTree.New.High.MT_hs",
        "projection_inverse_MerkleTree.New.High.MT_i",
        "projection_inverse_MerkleTree.New.High.MT_j",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "typing_FStar.Seq.Base.empty", "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.New.High.hash_init",
        "typing_MerkleTree.New.High.hashes", "typing_Prims.pow2"
      ],
      0,
      "60d812319d3d8802f5f259bff8a6fa3c"
    ],
    [
      "MerkleTree.New.High.hashess_insert",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Division", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5bd34bf04340340b1bef17bcddc72002",
        "refinement_interpretation_Tm_refine_ad53f3413fd15db5258446e997071714",
        "refinement_interpretation_Tm_refine_da1b0dfb8283502ec162998a8bbb6431"
      ],
      0,
      "061319ba46be7e17256a2c05a6be793f"
    ],
    [
      "MerkleTree.New.High.hashess_insert",
      2,
      1,
      0,
      [
        "@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,
      "98d1efe949ea9ad000239b92a41599f1"
    ],
    [
      "MerkleTree.New.High.hashess_insert",
      3,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "l_and-interp",
        "lemma_FStar.Seq.Base.lemma_eq_refl",
        "lemma_FStar.Seq.Base.lemma_len_upd",
        "lemma_FStar.Seq.Properties.slice_upd",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Division",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5664991902867dbaea8455604edd6227",
        "refinement_interpretation_Tm_refine_5bd34bf04340340b1bef17bcddc72002",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_ad53f3413fd15db5258446e997071714",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_da1b0dfb8283502ec162998a8bbb6431",
        "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
        "typing_MerkleTree.New.High.hashes"
      ],
      0,
      "007b18eece2e65f6f97388995282ce7b"
    ],
    [
      "MerkleTree.New.High.insert_",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "int_inversion", "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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5664991902867dbaea8455604edd6227",
        "refinement_interpretation_Tm_refine_5bd34bf04340340b1bef17bcddc72002",
        "refinement_interpretation_Tm_refine_da1b0dfb8283502ec162998a8bbb6431"
      ],
      0,
      "135713c218567544a16f666dd4e50743"
    ],
    [
      "MerkleTree.New.High.insert_",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "int_inversion", "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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5664991902867dbaea8455604edd6227",
        "refinement_interpretation_Tm_refine_5bd34bf04340340b1bef17bcddc72002",
        "refinement_interpretation_Tm_refine_da1b0dfb8283502ec162998a8bbb6431"
      ],
      0,
      "262de7573eaa9aec4a413b1eb1c62974"
    ],
    [
      "MerkleTree.New.High.insert_",
      3,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_4e45ffb596fe5eb4880eecea8024fe6f_4",
        "binder_x_7df3b3ce71ac0f95b834d29aa2f6700f_6",
        "binder_x_a3a9d1e443789a10c20ec8f7e2fe66e3_2",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_3",
        "binder_x_df2abc7452f72e525d1268e48951b5a9_5",
        "binder_x_f26957a7e62b271a8736230b1e9c83c1_0", "eq2-interp",
        "equality_tok_Prims.LexTop@tok",
        "equation_FStar.Seq.Properties.snoc",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess",
        "equation_MerkleTree.New.High.hashess_insert",
        "equation_MerkleTree.New.High.offset_of",
        "equation_MerkleTree.Spec.hash", "equation_Prims.nat",
        "equation_Prims.pos",
        "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_create_len",
        "lemma_FStar.Seq.Base.lemma_eq_refl",
        "lemma_FStar.Seq.Base.lemma_index_upd1",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.Seq.Properties.slice_upd",
        "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_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_037f1ad81b929724beac1258376a29a3",
        "refinement_interpretation_Tm_refine_0545ca68af3b2fc8df509fb388f7f2ee",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_29c27ac7c716b2238749315b70c9eca3",
        "refinement_interpretation_Tm_refine_40673d01fb13306535934c3b172c1134",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
        "refinement_interpretation_Tm_refine_5a8634b460d149c76a5c0476662af1d0",
        "refinement_interpretation_Tm_refine_76e82777dee381ea1df3bde8ab5956c6",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_8c0da31ad94507db704c5dd9ebc390a0",
        "refinement_interpretation_Tm_refine_ad53f3413fd15db5258446e997071714",
        "refinement_interpretation_Tm_refine_cc7ec1228e62f637b46417d43aae0cfa",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_da1b0dfb8283502ec162998a8bbb6431",
        "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.index",
        "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.seq",
        "typing_FStar.Seq.Properties.snoc",
        "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.New.High.offset_of",
        "well-founded-ordering-on-nat"
      ],
      0,
      "62a9a566bcc5ba8054fc037756d354f8"
    ],
    [
      "MerkleTree.New.High.insert_base",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "equation_Prims.nat", "equation_Prims.squash",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "l_and-interp", "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_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "2636579d02f07bb63ecb3455f85bf732"
    ],
    [
      "MerkleTree.New.High.insert_base",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.insert_.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess",
        "equation_MerkleTree.New.High.hashess_insert", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.insert_.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "lemma_FStar.Seq.Base.lemma_eq_refl",
        "primitive_Prims.op_Equality", "primitive_Prims.op_Modulus",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_415f66b36bf9db4e21e520bb0a30c0c2",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5664991902867dbaea8455604edd6227",
        "refinement_interpretation_Tm_refine_5bd34bf04340340b1bef17bcddc72002",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_ad53f3413fd15db5258446e997071714",
        "refinement_interpretation_Tm_refine_da1b0dfb8283502ec162998a8bbb6431",
        "refinement_interpretation_Tm_refine_ec7556075e2dd9aa116b8d4e21458205",
        "typing_MerkleTree.New.High.hashes",
        "typing_MerkleTree.New.High.hashess_insert",
        "typing_MerkleTree.New.High.insert_"
      ],
      0,
      "b8efc2029fc90912bf67ee0473be0c33"
    ],
    [
      "MerkleTree.New.High.insert_rec",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "eq2-interp", "equation_FStar.Seq.Properties.snoc",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess",
        "equation_MerkleTree.New.High.hashess_insert",
        "equation_MerkleTree.New.High.offset_of", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Prims.squash",
        "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_refl",
        "lemma_FStar.Seq.Properties.slice_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_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_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_ad53f3413fd15db5258446e997071714",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
        "typing_FStar.Seq.Base.slice", "typing_FStar.Seq.Properties.snoc",
        "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.New.High.hashes"
      ],
      0,
      "d25852b2e54b743a74329410226a53f7"
    ],
    [
      "MerkleTree.New.High.insert_rec",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.insert_.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.insert_.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess",
        "equation_MerkleTree.New.High.hashess_insert", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.insert_.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "lemma_FStar.Seq.Base.lemma_eq_refl",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Division",
        "primitive_Prims.op_Equality",
        "refinement_interpretation_Tm_refine_415f66b36bf9db4e21e520bb0a30c0c2",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5664991902867dbaea8455604edd6227",
        "refinement_interpretation_Tm_refine_5bd34bf04340340b1bef17bcddc72002",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_ad53f3413fd15db5258446e997071714",
        "refinement_interpretation_Tm_refine_da1b0dfb8283502ec162998a8bbb6431",
        "typing_MerkleTree.New.High.hashes",
        "typing_MerkleTree.New.High.insert_"
      ],
      0,
      "16343ac654510849226417f13f8c9e20"
    ],
    [
      "MerkleTree.New.High.mt_insert",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "bool_inversion", "equation_MerkleTree.New.High.mt_not_full",
        "equation_MerkleTree.New.High.mt_wf_elts", "equation_Prims.nat",
        "fuel_guarded_inversion_MerkleTree.New.High.merkle_tree",
        "primitive_Prims.op_Addition", "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",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_MerkleTree.New.High.MT_hs",
        "projection_inverse_MerkleTree.New.High.MT_i",
        "projection_inverse_MerkleTree.New.High.MT_j",
        "refinement_interpretation_Tm_refine_2fb140eeeb3dedac16f53b39260b0172",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_881298fb0dff2db17e4149fcf49ad4b9",
        "refinement_interpretation_Tm_refine_8a3da341c52f9ae12694ec5b3b33d9c0",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
        "typing_MerkleTree.New.High.__proj__MT__item__hs",
        "typing_MerkleTree.New.High.__proj__MT__item__j",
        "typing_MerkleTree.New.High.mt_not_full"
      ],
      0,
      "8cf2341a1b2684228f0ae442fa4d2930"
    ],
    [
      "MerkleTree.New.High.mt_create",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "equation_MerkleTree.New.High.create_empty_mt",
        "equation_MerkleTree.New.High.mt_not_full", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_typing",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "proj_equation_MerkleTree.New.High.MT_j",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_MerkleTree.New.High.MT_j",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "token_correspondence_Prims.pow2.fuel_instrumented"
      ],
      0,
      "f155f456de43f11d855f2114b357cbae"
    ],
    [
      "MerkleTree.New.High.construct_rhs",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91"
      ],
      0,
      "fa368542abc2653f2ae2ad601deb4e9f"
    ],
    [
      "MerkleTree.New.High.construct_rhs",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91"
      ],
      0,
      "27dd105eb23b9c10aef8d2bb93f25937"
    ],
    [
      "MerkleTree.New.High.construct_rhs",
      3,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_50de4ae25ca368b5de4d3ad61f7cc222_4",
        "binder_x_6e1290e37a6b4e437f899d72093932a2_2",
        "binder_x_7df3b3ce71ac0f95b834d29aa2f6700f_7",
        "binder_x_89dfa9cb1583ae31cce9fe730922098c_3",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_5",
        "binder_x_f0c2f5f0b61a8813760e74514fb47adf_6",
        "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.offset_of", "equation_Prims.nat",
        "equation_Prims.pos",
        "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_len_upd", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Division",
        "primitive_Prims.op_Equality", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
        "refinement_interpretation_Tm_refine_3275c6670c647fe05603aaa27ba49f71",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_843fa255df18c5621d60b239ca3b1ddf",
        "refinement_interpretation_Tm_refine_ad53f3413fd15db5258446e997071714",
        "refinement_interpretation_Tm_refine_c5f0d88a3da0ddeb45db9810df49fce9",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
        "typing_MerkleTree.New.High.hash", "well-founded-ordering-on-nat"
      ],
      0,
      "58341eb8647b8935adc981adbb868b32"
    ],
    [
      "MerkleTree.New.High.construct_rhs_unchanged",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "equation_MerkleTree.New.High.hash", "equation_Prims.nat",
        "equation_Prims.pos", "int_inversion",
        "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_42ab70f52fa85ce7b7f41db78958e96d",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_f5dcb5f7d87461830fead189c46dd01b",
        "refinement_kinding_Tm_refine_42ab70f52fa85ce7b7f41db78958e96d",
        "typing_FStar.Pervasives.Native.fst",
        "typing_MerkleTree.New.High.construct_rhs",
        "typing_MerkleTree.New.High.hash"
      ],
      0,
      "5b9fbe1b897129c926534193b1919f81"
    ],
    [
      "MerkleTree.New.High.construct_rhs_unchanged",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "equation_MerkleTree.New.High.hash", "equation_Prims.nat",
        "equation_Prims.pos", "int_inversion",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0a26d7fc4ea129b9a872a71cbced8694",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_42ab70f52fa85ce7b7f41db78958e96d",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_f5dcb5f7d87461830fead189c46dd01b",
        "refinement_kinding_Tm_refine_42ab70f52fa85ce7b7f41db78958e96d",
        "typing_FStar.Pervasives.Native.fst",
        "typing_MerkleTree.New.High.construct_rhs",
        "typing_MerkleTree.New.High.hash"
      ],
      0,
      "80f285281ebf7c667a8039374349aa3c"
    ],
    [
      "MerkleTree.New.High.construct_rhs_unchanged",
      3,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.construct_rhs.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.construct_rhs.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_50de4ae25ca368b5de4d3ad61f7cc222_4",
        "binder_x_5e20d151293c9e40e5203cbcff29aebe_1",
        "binder_x_6e1290e37a6b4e437f899d72093932a2_2",
        "binder_x_7df3b3ce71ac0f95b834d29aa2f6700f_7",
        "binder_x_89dfa9cb1583ae31cce9fe730922098c_3",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_5",
        "binder_x_f0c2f5f0b61a8813760e74514fb47adf_6",
        "binder_x_f26957a7e62b271a8736230b1e9c83c1_0",
        "binder_x_f537159ed795b314b4e58c260361ae86_8", "bool_inversion",
        "bool_typing", "eq2-interp", "equality_tok_Prims.LexTop@tok",
        "equation_FStar.Pervasives.Native.fst",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.offset_of", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.construct_rhs.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "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_eq_refl",
        "lemma_FStar.Seq.Base.lemma_len_upd",
        "lemma_FStar.Seq.Properties.slice_upd",
        "lemma_FStar.UInt.pow2_values",
        "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_LessThanOrEqual", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
        "refinement_interpretation_Tm_refine_3275c6670c647fe05603aaa27ba49f71",
        "refinement_interpretation_Tm_refine_42ab70f52fa85ce7b7f41db78958e96d",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
        "refinement_interpretation_Tm_refine_5a8634b460d149c76a5c0476662af1d0",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_843fa255df18c5621d60b239ca3b1ddf",
        "refinement_interpretation_Tm_refine_ad53f3413fd15db5258446e997071714",
        "refinement_interpretation_Tm_refine_c5f0d88a3da0ddeb45db9810df49fce9",
        "refinement_interpretation_Tm_refine_cc7ec1228e62f637b46417d43aae0cfa",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_f5dcb5f7d87461830fead189c46dd01b",
        "typing_FStar.Seq.Base.slice", "typing_FStar.Seq.Base.upd",
        "typing_MerkleTree.New.High.hash", "unit_inversion", "unit_typing",
        "well-founded-ordering-on-nat"
      ],
      0,
      "9d9ba43012b7aaeaf4cc91d277d03bb7"
    ],
    [
      "MerkleTree.New.High.construct_rhs_even",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "bool_typing", "equation_Prims.l_and",
        "equation_Prims.nat", "equation_Prims.pos", "equation_Prims.squash",
        "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.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Division", "primitive_Prims.op_Equality",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "primitive_Prims.op_disEquality",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_ad53f3413fd15db5258446e997071714",
        "refinement_interpretation_Tm_refine_f5dcb5f7d87461830fead189c46dd01b"
      ],
      0,
      "59e35f7b557f0af8ea1770813f69f905"
    ],
    [
      "MerkleTree.New.High.construct_rhs_even",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91"
      ],
      0,
      "4adaac597fa82f25532d2ff6d313865b"
    ],
    [
      "MerkleTree.New.High.construct_rhs_even",
      3,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.construct_rhs.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.construct_rhs.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "bool_inversion",
        "equation_with_fuel_MerkleTree.New.High.construct_rhs.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Division",
        "primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "a11129e0de5908e042da8ceeb8af883b"
    ],
    [
      "MerkleTree.New.High.construct_rhs_odd",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "bool_typing", "eq2-interp",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.offset_of", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Prims.squash",
        "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_len_upd", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Division",
        "primitive_Prims.op_Equality", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_42ab70f52fa85ce7b7f41db78958e96d",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_ad53f3413fd15db5258446e997071714",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
        "refinement_interpretation_Tm_refine_f5dcb5f7d87461830fead189c46dd01b",
        "typing_MerkleTree.New.High.hash"
      ],
      0,
      "aef14c29e40d5cb16f7b493c02a84f44"
    ],
    [
      "MerkleTree.New.High.construct_rhs_odd",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91"
      ],
      0,
      "cc065612128312d7828bf8b2a8ef14e9"
    ],
    [
      "MerkleTree.New.High.construct_rhs_odd",
      3,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.construct_rhs.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.construct_rhs.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "bool_inversion", "equation_Prims.nat",
        "equation_with_fuel_MerkleTree.New.High.construct_rhs.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "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_116339fd1727358a67e4504891c96c9b",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "9b4c4d2ad1c265e61ecb5f432fcedf16"
    ],
    [
      "MerkleTree.New.High.mt_get_root",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_MerkleTree.New.High.mt_wf_elts",
        "fuel_guarded_inversion_MerkleTree.New.High.merkle_tree",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "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",
        "refinement_interpretation_Tm_refine_7f59e1d21662a5bb0549ee09247e1710"
      ],
      0,
      "afb2dbde6ef74f619dd6254a0477ddab"
    ],
    [
      "MerkleTree.New.High.mt_get_root_rhs_ok_true",
      1,
      2,
      1,
      [ "@query", "equation_MerkleTree.New.High.mt_get_root" ],
      0,
      "f15dde57a8b19bc58e66e0dd72c9a5aa"
    ],
    [
      "MerkleTree.New.High.mt_get_root_rhs_ok_false",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_MerkleTree.New.High.mt_wf_elts",
        "fuel_guarded_inversion_MerkleTree.New.High.merkle_tree",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "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",
        "refinement_interpretation_Tm_refine_7f59e1d21662a5bb0549ee09247e1710"
      ],
      0,
      "3954996c09952496cdfe2b95ae03c73e"
    ],
    [
      "MerkleTree.New.High.mt_get_root_rhs_ok_false",
      2,
      2,
      1,
      [
        "@query", "equation_MerkleTree.New.High.mt_get_root",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "33c95d51c5f20bce72d023452c4dc815"
    ],
    [
      "MerkleTree.New.High.mt_path_length_step",
      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,
      "2e6a881e2d282ba5ded304caaacc2d95"
    ],
    [
      "MerkleTree.New.High.mt_path_length",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "binder_x_8398694cd93cdf584a90faddba74ff40_1",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
        "binder_x_f537159ed795b314b4e58c260361ae86_2", "equation_Prims.nat",
        "equation_Prims.op_Equals_Equals_Equals", "int_inversion",
        "int_typing", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Division", "primitive_Prims.op_Equality",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
        "refinement_interpretation_Tm_refine_730f09f30cda5cc9df2484cc11178d65",
        "typing_MerkleTree.New.High.mt_path_length_step",
        "well-founded-ordering-on-nat"
      ],
      0,
      "b3c819049bc7d29a08153f66b0f335b0"
    ],
    [
      "MerkleTree.New.High.mt_make_path_step",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91"
      ],
      0,
      "f0d0df783501539550f8840eeb5cdf52"
    ],
    [
      "MerkleTree.New.High.mt_make_path_step",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91"
      ],
      0,
      "74787afd184360062a5dcb0e44ab3a2f"
    ],
    [
      "MerkleTree.New.High.mt_make_path_step",
      3,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "eq2-interp",
        "equation_MerkleTree.New.High.offset_of", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "int_typing", "l_and-interp", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_42ab70f52fa85ce7b7f41db78958e96d",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_85b48fc854200a815ea472c3088d071c",
        "refinement_interpretation_Tm_refine_ad53f3413fd15db5258446e997071714",
        "refinement_interpretation_Tm_refine_cc7ec1228e62f637b46417d43aae0cfa",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b"
      ],
      0,
      "bab1bc2f9a57b62ff37012bbdea8aa7f"
    ],
    [
      "MerkleTree.New.High.mt_get_path_",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "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_cc7ec1228e62f637b46417d43aae0cfa"
      ],
      0,
      "5a1e34c119f08ebd19d6a8b46be134ce"
    ],
    [
      "MerkleTree.New.High.mt_get_path_",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "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_cc7ec1228e62f637b46417d43aae0cfa"
      ],
      0,
      "dcb8262233c43f4191543b00229341b4"
    ],
    [
      "MerkleTree.New.High.mt_get_path_",
      3,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.mt_path_length.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.mt_path_length.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_50de4ae25ca368b5de4d3ad61f7cc222_3",
        "binder_x_6e1290e37a6b4e437f899d72093932a2_1",
        "binder_x_89dfa9cb1583ae31cce9fe730922098c_2",
        "binder_x_954d2fd593ae84a715f3a1e4ec8b7c6b_5",
        "binder_x_abda421e48b5c84421ca729d856d67d6_7",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_4",
        "binder_x_ecb1afee7236cbd1e72258c33f56f1bf_6",
        "binder_x_f26957a7e62b271a8736230b1e9c83c1_0",
        "binder_x_f537159ed795b314b4e58c260361ae86_8", "bool_inversion",
        "bool_typing", "eq2-interp", "equality_tok_Prims.LexTop@tok",
        "equation_FStar.Seq.Properties.snoc",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess",
        "equation_MerkleTree.New.High.mt_make_path_step",
        "equation_MerkleTree.New.High.mt_path_length_step",
        "equation_MerkleTree.New.High.offset_of",
        "equation_MerkleTree.New.High.path",
        "equation_MerkleTree.New.High.path_insert", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.mt_path_length.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_create_len",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
        "primitive_Prims.op_Division", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Negation",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_3275c6670c647fe05603aaa27ba49f71",
        "refinement_interpretation_Tm_refine_3568d7f08856471af33d1f5679303601",
        "refinement_interpretation_Tm_refine_46221ef3565997e3bd8cebeee4165f2c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_ad53f3413fd15db5258446e997071714",
        "refinement_interpretation_Tm_refine_c5f0d88a3da0ddeb45db9810df49fce9",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_f307540f575140fb07355fe34ecda795",
        "refinement_interpretation_Tm_refine_f741409d867521e0e46e9b18e063f3dc",
        "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.index",
        "typing_FStar.Seq.Base.length", "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.New.High.hashes",
        "typing_MerkleTree.New.High.mt_path_length",
        "typing_MerkleTree.New.High.mt_path_length_step",
        "well-founded-ordering-on-nat"
      ],
      0,
      "cd65ae8e10ba0d2def4f5a693748319d"
    ],
    [
      "MerkleTree.New.High.mt_get_path_unchanged",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.mt_path_length.fuel_instrumented",
        "@query", "bool_inversion", "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.path", "equation_Prims.nat",
        "int_inversion", "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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
        "refinement_interpretation_Tm_refine_6e9e552283a82d93959794627615c964",
        "refinement_interpretation_Tm_refine_cc7ec1228e62f637b46417d43aae0cfa",
        "refinement_interpretation_Tm_refine_f5dcb5f7d87461830fead189c46dd01b",
        "typing_FStar.Seq.Base.length", "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.New.High.mt_get_path_",
        "typing_MerkleTree.New.High.mt_path_length"
      ],
      0,
      "e45049b5b7d5cec7093370b3b991050f"
    ],
    [
      "MerkleTree.New.High.mt_get_path_unchanged",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.mt_path_length.fuel_instrumented",
        "@query", "bool_inversion", "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.path", "equation_Prims.nat",
        "equation_Prims.pos", "int_inversion", "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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
        "refinement_interpretation_Tm_refine_6e9e552283a82d93959794627615c964",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_cc7ec1228e62f637b46417d43aae0cfa",
        "refinement_interpretation_Tm_refine_e5897805d267187c64946b859bf9b4da",
        "refinement_interpretation_Tm_refine_f5dcb5f7d87461830fead189c46dd01b",
        "typing_FStar.Seq.Base.length", "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.New.High.mt_get_path_",
        "typing_MerkleTree.New.High.mt_path_length"
      ],
      0,
      "93eb5912c2d53a35b0d9164111f6c9f3"
    ],
    [
      "MerkleTree.New.High.mt_get_path_unchanged",
      3,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.mt_get_path_.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.mt_path_length.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.mt_get_path_.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_1910ef5262f2ee8e712b6609a232b1ea",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_50de4ae25ca368b5de4d3ad61f7cc222_3",
        "binder_x_6e1290e37a6b4e437f899d72093932a2_1",
        "binder_x_89dfa9cb1583ae31cce9fe730922098c_2",
        "binder_x_954d2fd593ae84a715f3a1e4ec8b7c6b_5",
        "binder_x_abda421e48b5c84421ca729d856d67d6_7",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_4",
        "binder_x_ecb1afee7236cbd1e72258c33f56f1bf_6",
        "binder_x_f26957a7e62b271a8736230b1e9c83c1_0",
        "binder_x_f537159ed795b314b4e58c260361ae86_8", "bool_inversion",
        "bool_typing", "eq2-interp", "equality_tok_Prims.LexTop@tok",
        "equation_FStar.Seq.Properties.snoc",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess",
        "equation_MerkleTree.New.High.mt_make_path_step",
        "equation_MerkleTree.New.High.offset_of",
        "equation_MerkleTree.New.High.path",
        "equation_MerkleTree.New.High.path_insert", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.mt_get_path_.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.mt_path_length.fuel_instrumented",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_FStar.Seq.Base.index",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "l_and-interp",
        "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_index_app1",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.slice_length",
        "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_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_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5",
        "refinement_interpretation_Tm_refine_3275c6670c647fe05603aaa27ba49f71",
        "refinement_interpretation_Tm_refine_3568d7f08856471af33d1f5679303601",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_42ab70f52fa85ce7b7f41db78958e96d",
        "refinement_interpretation_Tm_refine_46221ef3565997e3bd8cebeee4165f2c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
        "refinement_interpretation_Tm_refine_6e9e552283a82d93959794627615c964",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_ad53f3413fd15db5258446e997071714",
        "refinement_interpretation_Tm_refine_c5f0d88a3da0ddeb45db9810df49fce9",
        "refinement_interpretation_Tm_refine_cc7ec1228e62f637b46417d43aae0cfa",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_f307540f575140fb07355fe34ecda795",
        "refinement_interpretation_Tm_refine_f5dcb5f7d87461830fead189c46dd01b",
        "token_correspondence_MerkleTree.New.High.mt_get_path_.fuel_instrumented",
        "token_correspondence_MerkleTree.New.High.mt_path_length.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.Base.slice",
        "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.New.High.hashes",
        "typing_MerkleTree.New.High.mt_get_path_",
        "well-founded-ordering-on-nat"
      ],
      0,
      "4d4deafe0f97a2d60893f689968a74e8"
    ],
    [
      "MerkleTree.New.High.mt_get_path_pull",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91"
      ],
      0,
      "f30ae326b2644d46bee201d21db4f614"
    ],
    [
      "MerkleTree.New.High.mt_get_path_pull",
      2,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91"
      ],
      0,
      "8313539b5c6cfe0176c7c3a84779b14d"
    ],
    [
      "MerkleTree.New.High.mt_get_path_pull",
      3,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.mt_get_path_.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.mt_path_length.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.mt_get_path_.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.mt_path_length.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_1910ef5262f2ee8e712b6609a232b1ea",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_50de4ae25ca368b5de4d3ad61f7cc222_3",
        "binder_x_6e1290e37a6b4e437f899d72093932a2_1",
        "binder_x_89dfa9cb1583ae31cce9fe730922098c_2",
        "binder_x_954d2fd593ae84a715f3a1e4ec8b7c6b_5",
        "binder_x_abda421e48b5c84421ca729d856d67d6_7",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_4",
        "binder_x_ecb1afee7236cbd1e72258c33f56f1bf_6",
        "binder_x_f26957a7e62b271a8736230b1e9c83c1_0",
        "binder_x_f537159ed795b314b4e58c260361ae86_8", "bool_inversion",
        "bool_typing", "eq2-interp", "equality_tok_Prims.LexTop@tok",
        "equation_FStar.Seq.Properties.snoc",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess",
        "equation_MerkleTree.New.High.mt_make_path_step",
        "equation_MerkleTree.New.High.mt_path_length_step",
        "equation_MerkleTree.New.High.offset_of",
        "equation_MerkleTree.New.High.path",
        "equation_MerkleTree.New.High.path_insert", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.mt_get_path_.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.mt_path_length.fuel_instrumented",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_FStar.Seq.Base.index",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "l_and-interp",
        "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_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_AmpAmp", "primitive_Prims.op_BarBar",
        "primitive_Prims.op_Division", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Negation",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_3275c6670c647fe05603aaa27ba49f71",
        "refinement_interpretation_Tm_refine_3568d7f08856471af33d1f5679303601",
        "refinement_interpretation_Tm_refine_42ab70f52fa85ce7b7f41db78958e96d",
        "refinement_interpretation_Tm_refine_46221ef3565997e3bd8cebeee4165f2c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
        "refinement_interpretation_Tm_refine_6e9e552283a82d93959794627615c964",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
        "refinement_interpretation_Tm_refine_ad53f3413fd15db5258446e997071714",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_c5f0d88a3da0ddeb45db9810df49fce9",
        "refinement_interpretation_Tm_refine_cc7ec1228e62f637b46417d43aae0cfa",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_f307540f575140fb07355fe34ecda795",
        "refinement_interpretation_Tm_refine_f5dcb5f7d87461830fead189c46dd01b",
        "refinement_interpretation_Tm_refine_f741409d867521e0e46e9b18e063f3dc",
        "token_correspondence_MerkleTree.New.High.mt_get_path_.fuel_instrumented",
        "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
        "typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.index",
        "typing_FStar.Seq.Base.length", "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.New.High.hashes",
        "typing_MerkleTree.New.High.mt_get_path_",
        "typing_MerkleTree.New.High.mt_path_length",
        "typing_MerkleTree.New.High.mt_path_length_step",
        "typing_MerkleTree.New.High.path_insert",
        "well-founded-ordering-on-nat"
      ],
      0,
      "3189883fc640878552fd1b58e7dc2745"
    ],
    [
      "MerkleTree.New.High.mt_get_path_slice",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.mt_path_length.fuel_instrumented",
        "@query", "bool_inversion", "equation_MerkleTree.New.High.hash",
        "equation_Prims.nat", "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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_6e9e552283a82d93959794627615c964",
        "refinement_interpretation_Tm_refine_cc7ec1228e62f637b46417d43aae0cfa",
        "typing_FStar.Seq.Base.length", "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.New.High.mt_get_path_"
      ],
      0,
      "23c5078c3355d45e7c79ccf6b8846b9f"
    ],
    [
      "MerkleTree.New.High.mt_get_path_slice",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.Spec.hash_raw", "equation_Prims.nat",
        "function_token_typing_MerkleTree.Spec.hash_raw", "int_inversion",
        "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_24912c01ee0f03c322e8fd592da5df56",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_be04426f825e7082f2beda6d03ac2ec5",
        "refinement_interpretation_Tm_refine_cc7ec1228e62f637b46417d43aae0cfa",
        "typing_FStar.Seq.Base.length",
        "typing_MerkleTree.New.High.mt_get_path_"
      ],
      0,
      "7bafa84d0fe5dc043afa3a28748f7d05"
    ],
    [
      "MerkleTree.New.High.mt_get_path_slice",
      3,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.mt_get_path_.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.mt_path_length.fuel_instrumented",
        "@query", "bool_inversion", "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.path", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.mt_get_path_.fuel_instrumented",
        "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "lemma_FStar.Seq.Base.lemma_index_app2",
        "lemma_FStar.Seq.Base.lemma_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_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
        "refinement_interpretation_Tm_refine_6e9e552283a82d93959794627615c964",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_Tm_refine_cc7ec1228e62f637b46417d43aae0cfa",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_f5dcb5f7d87461830fead189c46dd01b",
        "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.empty",
        "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
        "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.New.High.mt_get_path_",
        "typing_MerkleTree.New.High.mt_path_length"
      ],
      0,
      "c0db8764da6f6bbb85f6147e2768b4de"
    ],
    [
      "MerkleTree.New.High.mt_get_path",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_a9d60c8c7de4937910f5b34f519c7b2b"
      ],
      0,
      "cdd1a97da6ea0b143a06eb8a87f32702"
    ],
    [
      "MerkleTree.New.High.mt_get_path",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "eq2-interp",
        "equation_FStar.Seq.Properties.snoc",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.mt_get_root",
        "equation_MerkleTree.New.High.mt_wf_elts",
        "equation_MerkleTree.New.High.offset_of",
        "equation_MerkleTree.New.High.path_insert", "equation_Prims.nat",
        "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_create_len",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "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",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_MerkleTree.New.High.MT_hs",
        "projection_inverse_MerkleTree.New.High.MT_i",
        "projection_inverse_MerkleTree.New.High.MT_j",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7f59e1d21662a5bb0549ee09247e1710",
        "refinement_interpretation_Tm_refine_881298fb0dff2db17e4149fcf49ad4b9",
        "refinement_interpretation_Tm_refine_a9d60c8c7de4937910f5b34f519c7b2b",
        "refinement_interpretation_Tm_refine_ad53f3413fd15db5258446e997071714",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
        "refinement_interpretation_Tm_refine_dc275e75190e1d8c6a7a72dda4f9b4b6",
        "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.empty",
        "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"
      ],
      0,
      "1f5e70426a9934f06001f71926818eb6"
    ],
    [
      "MerkleTree.New.High.mt_flush_to_",
      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_ad53f3413fd15db5258446e997071714",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
        "refinement_interpretation_Tm_refine_da1b0dfb8283502ec162998a8bbb6431"
      ],
      0,
      "7237c9bcbf1702b25f2e5dfdfe8fd616"
    ],
    [
      "MerkleTree.New.High.mt_flush_to_",
      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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_ad53f3413fd15db5258446e997071714",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
        "refinement_interpretation_Tm_refine_da1b0dfb8283502ec162998a8bbb6431"
      ],
      0,
      "2da83aeb09ded6ebc875eecab63e27e6"
    ],
    [
      "MerkleTree.New.High.mt_flush_to_",
      3,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_20ef783cabfdc90ae174ed55c128717b_4",
        "binder_x_89dfa9cb1583ae31cce9fe730922098c_2",
        "binder_x_a3a9d1e443789a10c20ec8f7e2fe66e3_1",
        "binder_x_b9501129bf8af5491c1474484168d2cd_5",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_3",
        "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.eqtype",
        "equation_Prims.nat", "equation_Prims.pos",
        "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__",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "int_typing", "l_and-interp", "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_FStar.UInt.pow2_values",
        "lemma_MerkleTree.New.High.seq_slice_equal_index",
        "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_0545ca68af3b2fc8df509fb388f7f2ee",
        "refinement_interpretation_Tm_refine_11ff5223149858a6ed39dcb0f334332c",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
        "refinement_interpretation_Tm_refine_3275c6670c647fe05603aaa27ba49f71",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5a8634b460d149c76a5c0476662af1d0",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_ad53f3413fd15db5258446e997071714",
        "refinement_interpretation_Tm_refine_b5bc85c11830c41ccecb153a52a51c26",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_da1b0dfb8283502ec162998a8bbb6431",
        "refinement_interpretation_Tm_refine_df81b3f17797c6f405c1dbb191651292",
        "refinement_interpretation_Tm_refine_fcd595c29bbf91c47d4de5edaed33637",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
        "typing_FStar.Seq.Base.slice", "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.New.High.hashes",
        "typing_MerkleTree.New.High.offset_of",
        "well-founded-ordering-on-nat"
      ],
      0,
      "419808f5e236f0e9aedfa2c04c475409"
    ],
    [
      "MerkleTree.New.High.mt_flush_to_rec",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "eq2-interp", "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess",
        "equation_MerkleTree.New.High.offset_of", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Prims.pos", "equation_Prims.squash",
        "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__",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "int_typing", "l_and-interp", "lemma_FStar.Seq.Base.lemma_eq_refl",
        "lemma_FStar.Seq.Base.lemma_len_upd",
        "lemma_FStar.Seq.Properties.slice_upd",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Division", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "primitive_Prims.op_disEquality",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_72a6e6d3eb60f86cdad2dd40aa09f653",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_7d7fbea8a1aa1c987d727318058634ac",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_ad53f3413fd15db5258446e997071714",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_da1b0dfb8283502ec162998a8bbb6431",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
        "typing_FStar.Seq.Base.slice", "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.New.High.hashes",
        "typing_MerkleTree.New.High.mt_flush_to_",
        "typing_MerkleTree.New.High.offset_of"
      ],
      0,
      "69cc44444e632ee063226af4eacd87fa"
    ],
    [
      "MerkleTree.New.High.mt_flush_to_rec",
      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_ad53f3413fd15db5258446e997071714",
        "refinement_interpretation_Tm_refine_da1b0dfb8283502ec162998a8bbb6431"
      ],
      0,
      "4dc618dab120e6ff1ad43fd4a5c303ba"
    ],
    [
      "MerkleTree.New.High.mt_flush_to_rec",
      3,
      2,
      1,
      [
        "@MaxFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.mt_flush_to_.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.mt_flush_to_.fuel_instrumented",
        "@query", "equation_MerkleTree.New.High.offset_of",
        "equation_Prims.nat",
        "equation_with_fuel_MerkleTree.New.High.mt_flush_to_.fuel_instrumented",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Division",
        "primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "c6ab8c4da3ca891b7503342b128b941b"
    ],
    [
      "MerkleTree.New.High.mt_flush_to",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_MerkleTree.New.High.hashess",
        "equation_MerkleTree.New.High.mt_wf_elts", "equation_Prims.nat",
        "fuel_guarded_inversion_MerkleTree.New.High.merkle_tree",
        "int_inversion", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_LessThanOrEqual",
        "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_MerkleTree.New.High.MT_hs",
        "projection_inverse_MerkleTree.New.High.MT_i",
        "projection_inverse_MerkleTree.New.High.MT_j",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7f59e1d21662a5bb0549ee09247e1710",
        "refinement_interpretation_Tm_refine_881298fb0dff2db17e4149fcf49ad4b9",
        "refinement_interpretation_Tm_refine_a767aeb3e8a386f8149ca78110faaa32",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
        "refinement_interpretation_Tm_refine_db428869743ec15a24716674df186f66",
        "refinement_interpretation_Tm_refine_de2646114958fcaac38b7f7890283524",
        "typing_FStar.Seq.Base.length",
        "typing_MerkleTree.New.High.__proj__MT__item__hs",
        "typing_MerkleTree.New.High.__proj__MT__item__j",
        "typing_MerkleTree.New.High.hashes"
      ],
      0,
      "fbe4b0b4ff98f60066a6c56991151b04"
    ],
    [
      "MerkleTree.New.High.mt_flush",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "primitive_Prims.op_Subtraction",
        "proj_equation_MerkleTree.New.High.MT_i",
        "proj_equation_MerkleTree.New.High.MT_j",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_35cb22bdedbebf7b43fef791c588be43",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_MerkleTree.New.High.__proj__MT__item__i"
      ],
      0,
      "6dc2a4e2b85d680100303ee8c2ae24f9"
    ],
    [
      "MerkleTree.New.High.mt_retract_to_",
      1,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "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_2836c1aa0394cd6a310bf67b2eb5ba77",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b"
      ],
      0,
      "302a496a6601fd78d5b3b1713b59aee5"
    ],
    [
      "MerkleTree.New.High.mt_retract_to_",
      2,
      2,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Prims.pos",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "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_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
        "refinement_interpretation_Tm_refine_f863766dd52b84931c27ff1375fcdc0b"
      ],
      0,
      "35bd62f35f28502e802781ef83df8d4a"
    ],
    [
      "MerkleTree.New.High.mt_retract_to_",
      3,
      2,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_1bf1458a2b16b75524237b7cf638ee76_5",
        "binder_x_89dfa9cb1583ae31cce9fe730922098c_1",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_3",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_4",
        "binder_x_eacd128836d336dcd27d229643cf4d0e_2",
        "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.eqtype",
        "equation_Prims.nat", "equation_Prims.pos",
        "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__",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "int_typing", "l_and-interp", "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_length",
        "lemma_FStar.Seq.Properties.slice_upd",
        "lemma_FStar.UInt.pow2_values",
        "lemma_MerkleTree.New.High.seq_slice_equal_index",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Division", "primitive_Prims.op_Equality",
        "primitive_Prims.op_GreaterThanOrEqual",
        "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_0545ca68af3b2fc8df509fb388f7f2ee",
        "refinement_interpretation_Tm_refine_0c5607686b89742ca6db73e6f3756284",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
        "refinement_interpretation_Tm_refine_3275c6670c647fe05603aaa27ba49f71",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5a8634b460d149c76a5c0476662af1d0",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_a2d0a3931d4fe090e54ed0ac3ce177c4",
        "refinement_interpretation_Tm_refine_ad53f3413fd15db5258446e997071714",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_df81b3f17797c6f405c1dbb191651292",
        "refinement_interpretation_Tm_refine_f4c27ae2c29a3aebda6b5ec0ca3f80c6",
        "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
        "typing_FStar.Seq.Base.slice", "typing_FStar.Seq.Base.upd",
        "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.New.High.hashes",
        "typing_MerkleTree.New.High.offset_of",
        "well-founded-ordering-on-nat"
      ],
      0,
      "1c8fcd082a5c4d123dba773f88606d9f"
    ],
    [
      "MerkleTree.New.High.mt_retract_to",
      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,
      "52907d0bc1078e8443ce32dcc948d096"
    ],
    [
      "MerkleTree.New.High.mt_retract_to",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "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",
        "primitive_Prims.op_Addition", "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",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_MerkleTree.New.High.MT_hs",
        "projection_inverse_MerkleTree.New.High.MT_i",
        "projection_inverse_MerkleTree.New.High.MT_j",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7f59e1d21662a5bb0549ee09247e1710",
        "refinement_interpretation_Tm_refine_881298fb0dff2db17e4149fcf49ad4b9",
        "refinement_interpretation_Tm_refine_a9d60c8c7de4937910f5b34f519c7b2b",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
        "refinement_interpretation_Tm_refine_e1db4ece26674ee2cf19b464731f2f5e",
        "typing_FStar.Seq.Base.length",
        "typing_MerkleTree.New.High.__proj__MT__item__hs",
        "typing_MerkleTree.New.High.__proj__MT__item__j",
        "typing_MerkleTree.New.High.hashes"
      ],
      0,
      "dfa34e58d527c03b2dda89f0c5ddd737"
    ],
    [
      "MerkleTree.New.High.mt_verify_",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.mt_path_length.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.mt_path_length.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_3ecda020b5cf79d02cc346b352c50370_3",
        "binder_x_86bec0662121c4d7f8e2b57f9b893dbb_7",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_5",
        "binder_x_f26957a7e62b271a8736230b1e9c83c1_0", "bool_inversion",
        "bool_typing", "equation_MerkleTree.New.High.mt_path_length_step",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Prims.op_Equals_Equals_Equals", "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.mt_path_length.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "int_typing", "primitive_Prims.op_Addition",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
        "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_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_7d7ea0e457464ee9d02e8475aa297a7a",
        "refinement_interpretation_Tm_refine_dc48f78fca6f8433edb3d5a9ad647892",
        "typing_MerkleTree.New.High.mt_path_length",
        "typing_MerkleTree.New.High.mt_path_length_step",
        "well-founded-ordering-on-nat"
      ],
      0,
      "8169f5e6d5005e23f2b61560af552fa5"
    ],
    [
      "MerkleTree.New.High.mt_verify",
      1,
      2,
      1,
      [ "@query" ],
      0,
      "5d29bec2d72e76c23617b4df1ff76039"
    ],
    [
      "MerkleTree.New.High.mt_verify",
      2,
      2,
      1,
      [ "@query" ],
      0,
      "2bef5bc7907407004facf0ac87b31871"
    ],
    [
      "MerkleTree.New.High.mt_verify",
      3,
      1,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.mt_path_length.fuel_instrumented",
        "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "bool_typing", "equation_MerkleTree.New.High.hash",
        "equation_Prims.eq2", "equation_Prims.nat", "equation_Prims.squash",
        "equation_Prims.subtype_of", "int_inversion",
        "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a",
        "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
        "refinement_interpretation_Tm_refine_8233d76b57e95451540fc312b717fa79",
        "refinement_interpretation_Tm_refine_87faf900dfa0d2b4c1716c6e280af26b",
        "typing_MerkleTree.New.High.mt_path_length", "unit_typing"
      ],
      0,
      "e2f8ea47f750986e6f92695126179f97"
    ]
  ]
]