[
  "\n\u0013e\u0004Ï<\"[z•\u007fHeŸS",
  [
    [
      "MerkleTree.New.High.Correct.Rhs.construct_rhs_acc",
      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,
      "b5828f553ec6dbf3d2fccfdbec59370c"
    ],
    [
      "MerkleTree.New.High.Correct.Rhs.construct_rhs_acc",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "2d03c251178ea39fb3b6b6e64fc91f1c"
    ],
    [
      "MerkleTree.New.High.Correct.Rhs.construct_rhs_acc",
      3,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_7df3b3ce71ac0f95b834d29aa2f6700f_4",
        "binder_x_aabbf0a5d49093a6b07e3e5a24007535_3",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2",
        "binder_x_f26957a7e62b271a8736230b1e9c83c1_0",
        "constructor_distinct_Lib.IntTypes.U8", "eq2-interp",
        "equality_tok_Prims.LexTop@tok",
        "equation_FStar.Pervasives.Native.fst",
        "equation_FStar.Seq.Properties.cons",
        "equation_FStar.Seq.Properties.head",
        "equation_FStar.Seq.Properties.tail", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.unsigned",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "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_len_append",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.cons_index_slice",
        "lemma_MerkleTree.New.High.Correct.Base.seq_head_cons",
        "lemma_MerkleTree.New.High.Correct.Base.seq_tail_cons",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Division",
        "primitive_Prims.op_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_09d2e9ab3b9c121b24316d151747e281",
        "refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
        "refinement_interpretation_Tm_refine_167ef714932ec832fb671890fc3eee6c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_43a51d2a8f887f961c9753eac43d02b7",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_65ac557370bf352d1810d1fdbf624a4f",
        "refinement_interpretation_Tm_refine_7381b22713068fe22fae5f1ab9c6c30a",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "token_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length",
        "typing_FStar.Seq.Base.seq", "typing_FStar.Seq.Properties.tail",
        "typing_MerkleTree.New.High.Correct.Base.log2",
        "typing_MerkleTree.New.High.Correct.Base.log2c",
        "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.New.High.hash_init",
        "well-founded-ordering-on-nat"
      ],
      0,
      "f5b153c33f939bb325831ba0000e0296"
    ],
    [
      "MerkleTree.New.High.Correct.Rhs.construct_rhs_acc_odd",
      1,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "bool_typing", "eq2-interp",
        "equation_FStar.Seq.Properties.tail",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Prims.pos", "equation_Prims.squash",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
        "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_len_slice",
        "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", "primitive_Prims.op_disEquality",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_319130ca780c778653844ecfc44d9c4d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_43a51d2a8f887f961c9753eac43d02b7",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "token_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_FStar.Seq.Base.length",
        "typing_MerkleTree.New.High.Correct.Base.log2",
        "typing_MerkleTree.New.High.Correct.Base.log2c",
        "typing_MerkleTree.New.High.hashes"
      ],
      0,
      "b1f66db82e54af2fb76bd5446e5adacd"
    ],
    [
      "MerkleTree.New.High.Correct.Rhs.construct_rhs_acc_odd",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "c57668de26b930ef039967f9f006e1b7"
    ],
    [
      "MerkleTree.New.High.Correct.Rhs.construct_rhs_acc_odd",
      3,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Rhs.construct_rhs_acc.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Rhs.construct_rhs_acc.fuel_instrumented",
        "@query",
        "MerkleTree.Spec_interpretation_Tm_ghost_arrow_c8d0d4ba83f86d009153aeb71f24bf67",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
        "bool_typing", "constructor_distinct_Lib.IntTypes.U8",
        "data_elim_FStar.Pervasives.Native.Mktuple2", "eq2-interp",
        "equation_FStar.Pervasives.Native.fst",
        "equation_FStar.Pervasives.Native.snd",
        "equation_FStar.Seq.Properties.tail", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.unsigned",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess",
        "equation_MerkleTree.Spec.hash",
        "equation_MerkleTree.Spec.hash_fun_t", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.Correct.Rhs.construct_rhs_acc.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_len_slice",
        "lemma_FStar.Seq.Properties.slice_is_empty",
        "lemma_MerkleTree.New.High.Correct.Base.seq_tail_cons",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Division",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Subtraction",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__1",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
        "refinement_interpretation_Tm_refine_167ef714932ec832fb671890fc3eee6c",
        "refinement_interpretation_Tm_refine_319130ca780c778653844ecfc44d9c4d",
        "refinement_interpretation_Tm_refine_43a51d2a8f887f961c9753eac43d02b7",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_Tm_refine_ec91eb7c63ff09d16d5762b9a6555d2c",
        "refinement_kinding_Tm_refine_ec91eb7c63ff09d16d5762b9a6555d2c",
        "token_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "typing_FStar.Pervasives.Native.fst", "typing_FStar.Seq.Base.empty",
        "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Properties.head",
        "typing_FStar.Seq.Properties.last",
        "typing_FStar.Seq.Properties.tail",
        "typing_MerkleTree.New.High.Correct.Rhs.construct_rhs_acc",
        "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.New.High.hash_init",
        "typing_MerkleTree.New.High.hashes"
      ],
      0,
      "8143c259c3ddecd3a5e71462a589a958"
    ],
    [
      "MerkleTree.New.High.Correct.Rhs.construct_rhs_acc_inv_ok_0",
      1,
      2,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "eq2-interp",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
        "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", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_43a51d2a8f887f961c9753eac43d02b7",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_adbb92a01eb41047cc27cbb91b3e49f5",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "typing_FStar.Seq.Base.length",
        "typing_MerkleTree.New.High.Correct.Base.log2c",
        "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.New.High.hashes"
      ],
      0,
      "ffa3c3c284489f191162798ebfba9c6c"
    ],
    [
      "MerkleTree.New.High.Correct.Rhs.construct_rhs_acc_inv_ok_0",
      2,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_FStar.Integers.W16",
        "constructor_distinct_FStar.Integers.W31",
        "constructor_distinct_FStar.Integers.W8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_FStar.Integers.W16@tok",
        "equality_tok_FStar.Integers.W31@tok",
        "equality_tok_FStar.Integers.W8@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hash_seq",
        "equation_MerkleTree.New.High.hash_ss", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Spec.Poly1305.size_key",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "function_token_typing_MerkleTree.New.High.hash_seq",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_Lib.IntTypes.pow2_values",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Integers.Signed__0",
        "projection_inverse_FStar.Integers.Unsigned__0",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_a78e81a34494fa620ef91991a1267b1f",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_FStar.Seq.Base.length",
        "typing_MerkleTree.New.High.Correct.Base.log2c",
        "typing_Spec.Poly1305.size_key"
      ],
      0,
      "2ea6a85ef2321094b0e3d9e97c781f47"
    ],
    [
      "MerkleTree.New.High.Correct.Rhs.construct_rhs_acc_inv_ok_0",
      3,
      2,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.hash_seq_lift.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_inv_log.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_rhs_inv.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Rhs.construct_rhs_acc.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.Spec.hs_next_lv.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.Spec.mt_get_root.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.hash_seq_lift.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Rhs.construct_rhs_acc.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "MerkleTree.Spec_interpretation_Tm_ghost_arrow_c8d0d4ba83f86d009153aeb71f24bf67",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
        "bool_typing", "constructor_distinct_MerkleTree.Spec.HPad",
        "constructor_distinct_MerkleTree.Spec.HRaw",
        "data_typing_intro_MerkleTree.Spec.HPad@tok",
        "data_typing_intro_MerkleTree.Spec.HRaw@tok", "eq2-interp",
        "equation_FStar.Pervasives.Native.fst",
        "equation_FStar.Pervasives.Native.snd",
        "equation_FStar.Seq.Properties.cons",
        "equation_FStar.Seq.Properties.head",
        "equation_FStar.Seq.Properties.last",
        "equation_FStar.Seq.Properties.tail",
        "equation_MerkleTree.New.High.Correct.Base.create_pads",
        "equation_MerkleTree.New.High.Correct.Base.hash_seq_spec",
        "equation_MerkleTree.New.High.Correct.Base.hash_seq_spec_full",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess",
        "equation_MerkleTree.Spec.hash",
        "equation_MerkleTree.Spec.hash_fun_t",
        "equation_MerkleTree.Spec.hashes",
        "equation_MerkleTree.Spec.merkle_tree",
        "equation_MerkleTree.Spec.mt_next_lv",
        "equation_MerkleTree.Spec.padded_hash_fun", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.hash_seq_lift.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_inv_log.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_rhs_inv.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.Correct.Rhs.construct_rhs_acc.fuel_instrumented",
        "equation_with_fuel_MerkleTree.Spec.hs_next_lv.fuel_instrumented",
        "equation_with_fuel_MerkleTree.Spec.mt_get_root.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",
        "kinding_MerkleTree.Spec.padded_hash@tok", "l_and-interp",
        "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_index_app1",
        "lemma_FStar.Seq.Base.lemma_index_app2",
        "lemma_FStar.Seq.Base.lemma_index_create",
        "lemma_FStar.Seq.Base.lemma_index_upd1",
        "lemma_FStar.Seq.Base.lemma_index_upd2",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.slice_is_empty",
        "lemma_FStar.UInt.pow2_values",
        "lemma_MerkleTree.New.High.Correct.Base.seq_head_cons",
        "lemma_MerkleTree.New.High.Correct.Base.seq_tail_cons",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_BarBar", "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",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__1",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_MerkleTree.Spec.HPad_hsz",
        "projection_inverse_MerkleTree.Spec.HRaw_hr",
        "projection_inverse_MerkleTree.Spec.HRaw_hsz",
        "refinement_interpretation_Tm_refine_12b3c434aa6b331065cea3dabb126837",
        "refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
        "refinement_interpretation_Tm_refine_167ef714932ec832fb671890fc3eee6c",
        "refinement_interpretation_Tm_refine_319130ca780c778653844ecfc44d9c4d",
        "refinement_interpretation_Tm_refine_33e9e47c0adfd5c76673081bc3b1f7a6",
        "refinement_interpretation_Tm_refine_43a51d2a8f887f961c9753eac43d02b7",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
        "refinement_interpretation_Tm_refine_adbb92a01eb41047cc27cbb91b3e49f5",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_df81b3f17797c6f405c1dbb191651292",
        "refinement_interpretation_Tm_refine_e166b70fde2cd9152c503654048d8315",
        "refinement_interpretation_Tm_refine_e498fb51261db037ef331c43a4bc992d",
        "refinement_interpretation_Tm_refine_ec91eb7c63ff09d16d5762b9a6555d2c",
        "token_correspondence_MerkleTree.New.High.Correct.Base.hash_seq_lift.fuel_instrumented",
        "token_correspondence_Prims.pow2.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_FStar.Seq.Base.slice",
        "typing_FStar.Seq.Properties.cons",
        "typing_FStar.Seq.Properties.head",
        "typing_FStar.Seq.Properties.last",
        "typing_FStar.Seq.Properties.tail",
        "typing_MerkleTree.New.High.Correct.Base.hash_seq_spec",
        "typing_MerkleTree.New.High.Correct.Base.hash_seq_spec_full",
        "typing_MerkleTree.New.High.Correct.Base.log2",
        "typing_MerkleTree.New.High.Correct.Base.log2c",
        "typing_MerkleTree.New.High.Correct.Rhs.construct_rhs_acc",
        "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.New.High.hash_init",
        "typing_MerkleTree.New.High.hashes",
        "typing_MerkleTree.Spec.mt_next_lv",
        "typing_MerkleTree.Spec.padded_hash_fun"
      ],
      0,
      "c4e29f59a3b81261dd61e4a110c5f3f3"
    ],
    [
      "MerkleTree.New.High.Correct.Rhs.construct_rhs_acc_inv_ok",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "eq2-interp", "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hashess", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "l_and-interp", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
        "refinement_interpretation_Tm_refine_1793ad5f7093b21b800b75ee82fa5f2f",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_43a51d2a8f887f961c9753eac43d02b7",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "typing_MerkleTree.New.High.Correct.Base.log2"
      ],
      0,
      "85f715b0eaec969a57ff4548fa2ebfac"
    ],
    [
      "MerkleTree.New.High.Correct.Rhs.construct_rhs_acc_inv_ok",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "eq2-interp", "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hashess", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "l_and-interp", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
        "refinement_interpretation_Tm_refine_1793ad5f7093b21b800b75ee82fa5f2f",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_43a51d2a8f887f961c9753eac43d02b7",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "typing_MerkleTree.New.High.Correct.Base.log2"
      ],
      0,
      "59f886292592df5a1541847b1a171d82"
    ],
    [
      "MerkleTree.New.High.Correct.Rhs.construct_rhs_acc_inv_ok",
      3,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_inv_log.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_rhs_inv.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Rhs.construct_rhs_acc.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.Spec.mt_get_root.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.mt_hashes_inv_log.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.mt_rhs_inv.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Rhs.construct_rhs_acc.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.Spec.mt_get_root.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_5e20d151293c9e40e5203cbcff29aebe_1",
        "binder_x_7df3b3ce71ac0f95b834d29aa2f6700f_4",
        "binder_x_c9f70ab639c9ae669e58190eb4c1b5c9_2",
        "binder_x_dd21c6cd421aa589233742f950c39f9f_3",
        "binder_x_f26957a7e62b271a8736230b1e9c83c1_0",
        "binder_x_f537159ed795b314b4e58c260361ae86_5", "bool_inversion",
        "bool_typing", "eq2-interp", "equality_tok_Prims.LexTop@tok",
        "equation_FStar.Pervasives.Native.fst",
        "equation_FStar.Pervasives.Native.snd",
        "equation_FStar.Seq.Properties.cons",
        "equation_FStar.Seq.Properties.head",
        "equation_FStar.Seq.Properties.tail",
        "equation_MerkleTree.New.High.Correct.Base.hash_seq_spec_full",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess",
        "equation_MerkleTree.Spec.hash", "equation_MerkleTree.Spec.hashes",
        "equation_MerkleTree.Spec.merkle_tree",
        "equation_MerkleTree.Spec.mt_next_lv", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_inv_log.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_rhs_inv.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.Correct.Rhs.construct_rhs_acc.fuel_instrumented",
        "equation_with_fuel_MerkleTree.Spec.mt_get_root.fuel_instrumented",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "int_typing", "kinding_MerkleTree.Spec.padded_hash@tok",
        "l_and-interp", "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_2",
        "lemma_MerkleTree.New.High.Correct.Base.seq_head_cons",
        "lemma_MerkleTree.New.High.Correct.Base.seq_tail_cons",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_BarBar", "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",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__1",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_Tm_refine_12b3c434aa6b331065cea3dabb126837",
        "refinement_interpretation_Tm_refine_1367e6e7a7cd8798660a6880ab217dc1",
        "refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
        "refinement_interpretation_Tm_refine_167ef714932ec832fb671890fc3eee6c",
        "refinement_interpretation_Tm_refine_29c27ac7c716b2238749315b70c9eca3",
        "refinement_interpretation_Tm_refine_319130ca780c778653844ecfc44d9c4d",
        "refinement_interpretation_Tm_refine_33e9e47c0adfd5c76673081bc3b1f7a6",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_3a643af648e0e51f8493b1b7e51bd56c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_43a51d2a8f887f961c9753eac43d02b7",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_79be99f2c954b098ecc6368f3143c426",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_e166b70fde2cd9152c503654048d8315",
        "refinement_interpretation_Tm_refine_ec91eb7c63ff09d16d5762b9a6555d2c",
        "refinement_kinding_Tm_refine_79be99f2c954b098ecc6368f3143c426",
        "token_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "token_correspondence_Prims.pow2.fuel_instrumented", "true_interp",
        "typing_FStar.Pervasives.Native.fst", "typing_FStar.Seq.Base.create",
        "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.seq",
        "typing_FStar.Seq.Base.slice", "typing_FStar.Seq.Properties.head",
        "typing_FStar.Seq.Properties.tail",
        "typing_MerkleTree.New.High.Correct.Base.hash_seq_spec_full",
        "typing_MerkleTree.New.High.Correct.Base.log2",
        "typing_MerkleTree.New.High.Correct.Base.log2c",
        "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.New.High.hash_init",
        "typing_MerkleTree.Spec.hs_next_lv",
        "typing_MerkleTree.Spec.mt_next_lv", "typing_Prims.pow2",
        "unit_inversion", "unit_typing", "well-founded-ordering-on-nat"
      ],
      0,
      "b1e422dd7ff0a4cc41a5ca92889b7227"
    ],
    [
      "MerkleTree.New.High.Correct.Rhs.rhs_equiv",
      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,
      "1ee09b5ea3d38ba4267429a16813175b"
    ],
    [
      "MerkleTree.New.High.Correct.Rhs.rhs_equiv",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "1d95eeac655be103b58b01c1270981d9"
    ],
    [
      "MerkleTree.New.High.Correct.Rhs.rhs_equiv",
      3,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
        "binder_x_dedb383d0fdfb7962e91acd9435031a5_2",
        "binder_x_dedb383d0fdfb7962e91acd9435031a5_3",
        "binder_x_f26957a7e62b271a8736230b1e9c83c1_0", "bool_inversion",
        "bool_typing", "equality_tok_Prims.LexTop@tok",
        "equation_FStar.Seq.Properties.tail",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_Lib.IntTypes.pow2_3",
        "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_13d357a23a5e1099db9eb784ff83d223",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_781bf0974940d7695f199f1bcaca8e4a",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "token_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_FStar.Seq.Base.length",
        "typing_MerkleTree.New.High.Correct.Base.log2",
        "typing_MerkleTree.New.High.hash", "well-founded-ordering-on-nat"
      ],
      0,
      "f30eb0fc306cb9f999bc3d598ac9feba"
    ],
    [
      "MerkleTree.New.High.Correct.Rhs.rhs_equiv_inv_preserved",
      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,
      "77f3e8877b27df5df9a99d349c1a9f01"
    ],
    [
      "MerkleTree.New.High.Correct.Rhs.rhs_equiv_inv_preserved",
      2,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "f661b8bc54e9363601fb385e566b0576"
    ],
    [
      "MerkleTree.New.High.Correct.Rhs.rhs_equiv_inv_preserved",
      3,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_rhs_inv.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Rhs.rhs_equiv.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.mt_rhs_inv.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Rhs.rhs_equiv.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_53091569903cae77b4a60be8a17a11bc_4",
        "binder_x_53091569903cae77b4a60be8a17a11bc_5",
        "binder_x_5e20d151293c9e40e5203cbcff29aebe_1",
        "binder_x_7802c6c7540d3455819384f8c2a0a0c8_3",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2",
        "binder_x_f26957a7e62b271a8736230b1e9c83c1_0",
        "binder_x_f537159ed795b314b4e58c260361ae86_6", "bool_inversion",
        "bool_typing", "eq2-interp", "equality_tok_Prims.LexTop@tok",
        "equation_FStar.Seq.Properties.tail",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.Spec.merkle_tree",
        "equation_MerkleTree.Spec.mt_next_lv", "equation_Prims.l_True",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_rhs_inv.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.Correct.Rhs.rhs_equiv.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_slice",
        "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_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_765c5038a14ad1a170ebaf2c2e8ec7c8",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "refinement_interpretation_Tm_refine_e166b70fde2cd9152c503654048d8315",
        "refinement_interpretation_Tm_refine_ec91eb7c63ff09d16d5762b9a6555d2c",
        "true_interp", "typing_MerkleTree.New.High.Correct.Base.log2",
        "typing_MerkleTree.New.High.Correct.Base.log2c",
        "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.Spec.mt_next_lv", "typing_Prims.pow2",
        "unit_inversion", "unit_typing", "well-founded-ordering-on-nat"
      ],
      0,
      "13c0969d3f2f83949bf279aa787b5243"
    ],
    [
      "MerkleTree.New.High.Correct.Rhs.construct_rhs_acc_consistent",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@query", "equation_FStar.Pervasives.Native.fst",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Prims.pos",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "int_typing", "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_06cb130490423446d04fd8da416162f0",
        "refinement_interpretation_Tm_refine_0b724b6f6a7953a53d5fb02ee8337e6a",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_42ab70f52fa85ce7b7f41db78958e96d",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_4d0ab6134173bbad75f08ef14247f657",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5664991902867dbaea8455604edd6227",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_bf3340443d6edf0ae4bc4b37060534fb",
        "refinement_kinding_Tm_refine_42ab70f52fa85ce7b7f41db78958e96d",
        "typing_FStar.Pervasives.Native.fst",
        "typing_MerkleTree.New.High.Correct.Base.log2c",
        "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.New.High.hashes"
      ],
      0,
      "6c8bb05c4f774c54d56938999b1d7fd2"
    ],
    [
      "MerkleTree.New.High.Correct.Rhs.construct_rhs_acc_consistent",
      2,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "data_elim_FStar.Pervasives.Native.Mktuple2",
        "equation_FStar.Pervasives.Native.fst",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Prims.pos",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "int_typing", "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_06cb130490423446d04fd8da416162f0",
        "refinement_interpretation_Tm_refine_0b724b6f6a7953a53d5fb02ee8337e6a",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_42ab70f52fa85ce7b7f41db78958e96d",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_4d0ab6134173bbad75f08ef14247f657",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5664991902867dbaea8455604edd6227",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_bf3340443d6edf0ae4bc4b37060534fb",
        "refinement_kinding_Tm_refine_42ab70f52fa85ce7b7f41db78958e96d",
        "typing_FStar.Pervasives.Native.fst",
        "typing_MerkleTree.New.High.Correct.Base.log2c",
        "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.New.High.hashes"
      ],
      0,
      "a72eb73fa71548828c0326e2dfdb47fc"
    ],
    [
      "MerkleTree.New.High.Correct.Rhs.construct_rhs_acc_consistent",
      3,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.merge_hs.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_olds_inv.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Rhs.construct_rhs_acc.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Rhs.rhs_equiv.fuel_instrumented",
        "@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.Correct.Base.merge_hs.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Base.mt_olds_inv.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Rhs.construct_rhs_acc.fuel_instrumented",
        "@fuel_irrelevance_MerkleTree.New.High.Correct.Rhs.rhs_equiv.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",
        "MerkleTree.Spec_interpretation_Tm_ghost_arrow_c8d0d4ba83f86d009153aeb71f24bf67",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_50de4ae25ca368b5de4d3ad61f7cc222_7",
        "binder_x_5e20d151293c9e40e5203cbcff29aebe_1",
        "binder_x_6e1290e37a6b4e437f899d72093932a2_2",
        "binder_x_7df3b3ce71ac0f95b834d29aa2f6700f_8",
        "binder_x_8cf65b3b9d91dec7086970aa4543f287_5",
        "binder_x_abefe0b518359a5a388975bd4374c4d4_6",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_3",
        "binder_x_cbac39ab364bbcc08dab587ac968871a_4",
        "binder_x_f26957a7e62b271a8736230b1e9c83c1_0",
        "binder_x_f537159ed795b314b4e58c260361ae86_9", "bool_inversion",
        "bool_typing", "constructor_distinct_Lib.IntTypes.U8",
        "data_elim_FStar.Pervasives.Native.Mktuple2", "eq2-interp",
        "equality_tok_Prims.LexTop@tok",
        "equation_FStar.Pervasives.Native.fst",
        "equation_FStar.Pervasives.Native.snd",
        "equation_FStar.Seq.Properties.cons",
        "equation_FStar.Seq.Properties.head",
        "equation_FStar.Seq.Properties.last",
        "equation_FStar.Seq.Properties.tail", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.unsigned",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hash_init",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess",
        "equation_MerkleTree.New.High.offset_of",
        "equation_MerkleTree.Spec.hash",
        "equation_MerkleTree.Spec.hash_fun_t", "equation_Prims.eqtype",
        "equation_Prims.l_True", "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_olds_inv.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.Correct.Rhs.construct_rhs_acc.fuel_instrumented",
        "equation_with_fuel_MerkleTree.New.High.Correct.Rhs.rhs_equiv.fuel_instrumented",
        "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__",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "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_app2",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_index_upd1",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Base.lemma_len_upd",
        "lemma_FStar.Seq.Properties.lemma_tail_slice",
        "lemma_FStar.Seq.Properties.slice_is_empty",
        "lemma_FStar.Seq.Properties.slice_length",
        "lemma_FStar.UInt.pow2_values",
        "lemma_MerkleTree.New.High.Correct.Base.merge_hs_index",
        "lemma_MerkleTree.New.High.Correct.Base.seq_head_cons",
        "lemma_MerkleTree.New.High.Correct.Base.seq_tail_cons",
        "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",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__1",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__a",
        "refinement_interpretation_Tm_refine_0545ca68af3b2fc8df509fb388f7f2ee",
        "refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_167ef714932ec832fb671890fc3eee6c",
        "refinement_interpretation_Tm_refine_1ae2a0d6b2f4da2d4b0194885669f804",
        "refinement_interpretation_Tm_refine_22125f28c20990597c03dac8bb18819e",
        "refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
        "refinement_interpretation_Tm_refine_319130ca780c778653844ecfc44d9c4d",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_41cb2b001ca1224f35927e055aaa989e",
        "refinement_interpretation_Tm_refine_42ab70f52fa85ce7b7f41db78958e96d",
        "refinement_interpretation_Tm_refine_43a51d2a8f887f961c9753eac43d02b7",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5a8634b460d149c76a5c0476662af1d0",
        "refinement_interpretation_Tm_refine_6ecc26d260b07cd8c8333ca61d7545ba",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "refinement_interpretation_Tm_refine_9b2b3e7ac5f300ddc6add4181948ef22",
        "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
        "refinement_interpretation_Tm_refine_ad53f3413fd15db5258446e997071714",
        "refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
        "refinement_interpretation_Tm_refine_b138bd5848d4184f7632587e6e4bcf9f",
        "refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1",
        "refinement_interpretation_Tm_refine_b8cfbff7b918d0d751ba0dc42b418fa8",
        "refinement_interpretation_Tm_refine_bb2cbefb6f9a8a50a7b780a0a53e7963",
        "refinement_interpretation_Tm_refine_bf77b71bea5b62c114437d8059286011",
        "refinement_interpretation_Tm_refine_c5f0d88a3da0ddeb45db9810df49fce9",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_d87d99f22d4a7ec1b20cbca92c993502",
        "refinement_interpretation_Tm_refine_db1f7a375601e94233b330488ad7e8aa",
        "refinement_interpretation_Tm_refine_ec91eb7c63ff09d16d5762b9a6555d2c",
        "refinement_interpretation_Tm_refine_f06701b369ea2ba5f20cf7ab3a9eaff7",
        "refinement_interpretation_Tm_refine_f5dcb5f7d87461830fead189c46dd01b",
        "refinement_kinding_Tm_refine_39590bd04172bfcc8f773d62c9a2dc7d",
        "refinement_kinding_Tm_refine_b8cfbff7b918d0d751ba0dc42b418fa8",
        "refinement_kinding_Tm_refine_c5f0d88a3da0ddeb45db9810df49fce9",
        "token_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
        "token_correspondence_MerkleTree.New.High.Correct.Rhs.construct_rhs_acc.fuel_instrumented",
        "true_interp", "typing_FStar.Pervasives.Native.fst",
        "typing_FStar.Pervasives.Native.snd", "typing_FStar.Seq.Base.append",
        "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.index",
        "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.seq",
        "typing_FStar.Seq.Base.slice", "typing_FStar.Seq.Base.upd",
        "typing_FStar.Seq.Properties.cons",
        "typing_FStar.Seq.Properties.head",
        "typing_FStar.Seq.Properties.last",
        "typing_FStar.Seq.Properties.tail",
        "typing_MerkleTree.New.High.Correct.Base.log2c",
        "typing_MerkleTree.New.High.Correct.Rhs.construct_rhs_acc",
        "typing_MerkleTree.New.High.construct_rhs",
        "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.New.High.hash_init",
        "typing_MerkleTree.New.High.offset_of", "unit_inversion",
        "unit_typing", "well-founded-ordering-on-nat"
      ],
      0,
      "9a90ce9e4639f9938e46f744c697a7c9"
    ],
    [
      "MerkleTree.New.High.Correct.Rhs.construct_rhs_inv_ok",
      1,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.merge_hs.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
        "data_elim_FStar.Pervasives.Native.Mktuple2", "eq2-interp",
        "equation_FStar.Pervasives.Native.fst",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
        "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_len_slice",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_1ae2a0d6b2f4da2d4b0194885669f804",
        "refinement_interpretation_Tm_refine_42ab70f52fa85ce7b7f41db78958e96d",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_4c6cdb6946a57f770e07008f14ffd053",
        "refinement_interpretation_Tm_refine_4d0ab6134173bbad75f08ef14247f657",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5664991902867dbaea8455604edd6227",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_bf3340443d6edf0ae4bc4b37060534fb",
        "refinement_interpretation_Tm_refine_c27bf65dd8fe7d87744990594d99330b",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
        "refinement_kinding_Tm_refine_42ab70f52fa85ce7b7f41db78958e96d",
        "typing_FStar.Pervasives.Native.fst",
        "typing_MerkleTree.New.High.Correct.Base.log2c",
        "typing_MerkleTree.New.High.hash"
      ],
      0,
      "c887f3f99c62f39834f71fb03f8c3cdb"
    ],
    [
      "MerkleTree.New.High.Correct.Rhs.construct_rhs_inv_ok",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91"
      ],
      0,
      "181ed237924b216761c247e82d9258b2"
    ],
    [
      "MerkleTree.New.High.Correct.Rhs.construct_rhs_inv_ok",
      3,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.merge_hs.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "data_elim_FStar.Pervasives.Native.Mktuple2", "eq2-interp",
        "equation_FStar.Pervasives.Native.fst",
        "equation_FStar.Seq.Properties.head",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess",
        "equation_MerkleTree.Spec.merkle_tree", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "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_index_slice",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Division",
        "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_06cb130490423446d04fd8da416162f0",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_1ae2a0d6b2f4da2d4b0194885669f804",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_42ab70f52fa85ce7b7f41db78958e96d",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_4c6cdb6946a57f770e07008f14ffd053",
        "refinement_interpretation_Tm_refine_4d0ab6134173bbad75f08ef14247f657",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5664991902867dbaea8455604edd6227",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_bf3340443d6edf0ae4bc4b37060534fb",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_e166b70fde2cd9152c503654048d8315",
        "refinement_kinding_Tm_refine_42ab70f52fa85ce7b7f41db78958e96d",
        "typing_FStar.Pervasives.Native.fst", "typing_FStar.Seq.Base.length",
        "typing_MerkleTree.New.High.Correct.Base.log2c",
        "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.New.High.hashes"
      ],
      0,
      "f4269cc4f13f9fbf1cacd6252f0dfb01"
    ],
    [
      "MerkleTree.New.High.Correct.Rhs.construct_rhs_base_inv_ok",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.merge_hs.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "eq2-interp", "equation_FStar.Pervasives.Native.fst",
        "equation_FStar.Seq.Properties.head",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
        "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_len_slice",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_1ae2a0d6b2f4da2d4b0194885669f804",
        "refinement_interpretation_Tm_refine_2664edc4633a71f01ee27214d3ada3bb",
        "refinement_interpretation_Tm_refine_42ab70f52fa85ce7b7f41db78958e96d",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5be08a2846f9929cfec140da85f9a5a3",
        "refinement_interpretation_Tm_refine_692824d7a922a649b2edb9f0e1afbf70",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_bf3340443d6edf0ae4bc4b37060534fb",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
        "refinement_kinding_Tm_refine_42ab70f52fa85ce7b7f41db78958e96d",
        "typing_FStar.Pervasives.Native.fst",
        "typing_MerkleTree.New.High.Correct.Base.log2c",
        "typing_MerkleTree.New.High.hash"
      ],
      0,
      "d432ebe2fb4847b09aa2131f8afa2b98"
    ],
    [
      "MerkleTree.New.High.Correct.Rhs.construct_rhs_base_inv_ok",
      2,
      2,
      1,
      [ "@query" ],
      0,
      "b74ce1082ccbca767caedcd204901a3d"
    ],
    [
      "MerkleTree.New.High.Correct.Rhs.construct_rhs_base_inv_ok",
      3,
      2,
      1,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.merge_hs.fuel_instrumented",
        "@query", "equation_FStar.Seq.Properties.head",
        "equation_MerkleTree.New.High.Correct.Base.log2c",
        "equation_MerkleTree.New.High.hash_seq", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_Addition",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2664edc4633a71f01ee27214d3ada3bb",
        "refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_MerkleTree.New.High.Correct.Base.log2c"
      ],
      0,
      "39f204a4fca65ce1f14b5f7111483dbc"
    ],
    [
      "MerkleTree.New.High.Correct.Rhs.construct_rhs_init_ignored",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91"
      ],
      0,
      "f57e5b6093470fa350e173c59cc9b591"
    ],
    [
      "MerkleTree.New.High.Correct.Rhs.construct_rhs_init_ignored",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91"
      ],
      0,
      "d2524feaee8ae9ca57a6eaf453e217d8"
    ],
    [
      "MerkleTree.New.High.Correct.Rhs.construct_rhs_init_ignored",
      3,
      1,
      1,
      [
        "@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_7df3b3ce71ac0f95b834d29aa2f6700f_8",
        "binder_x_89dfa9cb1583ae31cce9fe730922098c_3",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_5",
        "binder_x_f0c2f5f0b61a8813760e74514fb47adf_6",
        "binder_x_f26957a7e62b271a8736230b1e9c83c1_0", "bool_typing",
        "data_elim_FStar.Pervasives.Native.Mktuple2",
        "equality_tok_Prims.LexTop@tok",
        "equation_FStar.Pervasives.Native.fst",
        "equation_FStar.Pervasives.Native.snd",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hashes", "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.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",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__1",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "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_3275c6670c647fe05603aaa27ba49f71",
        "refinement_interpretation_Tm_refine_42ab70f52fa85ce7b7f41db78958e96d",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_715fa59b8217d000ff3843aa60c041ce",
        "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",
        "refinement_interpretation_Tm_refine_f5dcb5f7d87461830fead189c46dd01b",
        "typing_MerkleTree.New.High.construct_rhs",
        "typing_MerkleTree.New.High.hash", "well-founded-ordering-on-nat"
      ],
      0,
      "4075900a4fd29f6a0ed2fb970d3d5c1b"
    ],
    [
      "MerkleTree.New.High.Correct.Rhs.mt_get_root_inv_ok",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_MerkleTree.New.High.mt_wf_elts",
        "fuel_guarded_inversion_MerkleTree.New.High.merkle_tree",
        "proj_equation_MerkleTree.New.High.MT_hs",
        "proj_equation_MerkleTree.New.High.MT_i",
        "proj_equation_MerkleTree.New.High.MT_j",
        "refinement_interpretation_Tm_refine_7f59e1d21662a5bb0549ee09247e1710",
        "refinement_interpretation_Tm_refine_995516c5fe04fd93611e610195bbf9ba"
      ],
      0,
      "a749e6f853a08447ba13289e208479f0"
    ],
    [
      "MerkleTree.New.High.Correct.Rhs.mt_get_root_inv_ok",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_MerkleTree.New.High.Correct.Base.merge_hs.fuel_instrumented",
        "@fuel_correspondence_MerkleTree.New.High.construct_rhs.fuel_instrumented",
        "@query",
        "MerkleTree.New.High_pretyping_42b5f1434db9b9fcab9a3482ce626e35",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
        "bool_typing", "data_typing_intro_MerkleTree.New.High.MT@tok",
        "eq2-interp", "equation_FStar.Pervasives.Native.fst",
        "equation_FStar.Pervasives.Native.snd",
        "equation_FStar.Seq.Properties.head",
        "equation_MerkleTree.New.High.Correct.Base.hash_seq_spec_full",
        "equation_MerkleTree.New.High.Correct.Base.mt_base",
        "equation_MerkleTree.New.High.Correct.Base.mt_inv",
        "equation_MerkleTree.New.High.Correct.Base.mt_olds_hs_inv",
        "equation_MerkleTree.New.High.Correct.Base.mt_root_inv",
        "equation_MerkleTree.New.High.Correct.Base.mt_spec",
        "equation_MerkleTree.New.High.hash",
        "equation_MerkleTree.New.High.hash_init",
        "equation_MerkleTree.New.High.hashes",
        "equation_MerkleTree.New.High.hashess",
        "equation_MerkleTree.New.High.mt_get_root",
        "equation_MerkleTree.New.High.mt_wf_elts", "equation_Prims.nat",
        "fuel_guarded_inversion_MerkleTree.New.High.merkle_tree",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "l_and-interp",
        "lemma_FStar.Seq.Base.lemma_eq_elim", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__1",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "proj_equation_MerkleTree.New.High.MT_hash_fun",
        "proj_equation_MerkleTree.New.High.MT_hs",
        "proj_equation_MerkleTree.New.High.MT_i",
        "proj_equation_MerkleTree.New.High.MT_j",
        "proj_equation_MerkleTree.New.High.MT_mroot",
        "proj_equation_MerkleTree.New.High.MT_rhs",
        "proj_equation_MerkleTree.New.High.MT_rhs_ok",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_MerkleTree.New.High.MT_hash_fun",
        "projection_inverse_MerkleTree.New.High.MT_hs",
        "projection_inverse_MerkleTree.New.High.MT_i",
        "projection_inverse_MerkleTree.New.High.MT_j",
        "projection_inverse_MerkleTree.New.High.MT_mroot",
        "projection_inverse_MerkleTree.New.High.MT_rhs",
        "projection_inverse_MerkleTree.New.High.MT_rhs_ok",
        "refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
        "refinement_interpretation_Tm_refine_42ab70f52fa85ce7b7f41db78958e96d",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7f59e1d21662a5bb0549ee09247e1710",
        "refinement_interpretation_Tm_refine_881298fb0dff2db17e4149fcf49ad4b9",
        "refinement_interpretation_Tm_refine_995516c5fe04fd93611e610195bbf9ba",
        "refinement_interpretation_Tm_refine_9e2cc9c9dac6b0e7d2a3400258c6016f",
        "refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
        "refinement_interpretation_Tm_refine_e4c62a9b95223de40b5923788de79f98",
        "refinement_interpretation_Tm_refine_f5dcb5f7d87461830fead189c46dd01b",
        "refinement_kinding_Tm_refine_42ab70f52fa85ce7b7f41db78958e96d",
        "true_interp", "typing_FStar.Pervasives.Native.fst",
        "typing_FStar.Pervasives.Native.snd", "typing_FStar.Seq.Base.length",
        "typing_MerkleTree.New.High.Correct.Base.mt_base",
        "typing_MerkleTree.New.High.__proj__MT__item__hash_fun",
        "typing_MerkleTree.New.High.__proj__MT__item__hs",
        "typing_MerkleTree.New.High.__proj__MT__item__i",
        "typing_MerkleTree.New.High.__proj__MT__item__j",
        "typing_MerkleTree.New.High.__proj__MT__item__rhs",
        "typing_MerkleTree.New.High.__proj__MT__item__rhs_ok",
        "typing_MerkleTree.New.High.construct_rhs",
        "typing_MerkleTree.New.High.hash",
        "typing_MerkleTree.New.High.hash_init",
        "typing_MerkleTree.New.High.hashes", "unit_inversion", "unit_typing"
      ],
      0,
      "d321e5c92acb19545396cb5cb737def9"
    ]
  ]
]