[
  "\u007fyT�:\u0006�\fX��N:(Y\"",
  [
    [
      "Vale.Lib.Seqs.lemma_slice_first_exactly_in_append",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_FStar.Seq.Base.length"
      ],
      0,
      "552757b559e03754fe1d950a981f9b8d"
    ],
    [
      "Vale.Lib.Seqs.lemma_all_but_last_append",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_3e04674625ba1e90ddf6da6977508e33",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_FStar.Seq.Base.length"
      ],
      0,
      "4372ca3b599a093399fd775e47be3013"
    ],
    [
      "Vale.Lib.Seqs.seq_map_i_indexed",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "d54acc54ed5d3653eedd3c53997124e6"
    ],
    [
      "Vale.Lib.Seqs.seq_map_i",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "5d48e366877d933d1b0c030bf3a83e2c"
    ],
    [
      "Vale.Lib.Seqs.seq_map_internal_associative",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "58e05f959ac56b7521758d7b2c7049db"
    ],
    [
      "Vale.Lib.Seqs.slice_append_adds",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "int_inversion", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "typing_FStar.Seq.Base.length"
      ],
      0,
      "fdb20bf45450e2f406dac77b7696cd45"
    ],
    [
      "Vale.Lib.Seqs.slice_seq_map_commute",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "equation_Prims.nat", "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map", "int_inversion",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca"
      ],
      0,
      "b959e3bd34da3bef0817d49a48631462"
    ],
    [
      "Vale.Lib.Seqs.list_to_seq_post",
      1,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented",
        "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "binder_x_0a56e3de562c08d8ab59f4ac6f626a98_2",
        "binder_x_4ba5d02fdaa2a4e1a80f4f1dfd4982d6_3",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_4",
        "binder_x_fe28d8bcde588226b4e538b35321de05_1",
        "constructor_distinct_Prims.Cons", "constructor_distinct_Tm_unit",
        "disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
        "equality_tok_Prims.LexTop@tok", "equation_Prims.eq2",
        "equation_Prims.l_and", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Prims.subtype_of",
        "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
        "int_inversion", "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a",
        "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Prims.Cons_a",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "subterm_ordering_Prims.Cons",
        "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "typing_FStar.List.Tot.Base.length", "typing_FStar.Seq.Base.length",
        "unit_typing"
      ],
      0,
      "f7e4941cc10a68a64272995bc9f41432"
    ],
    [
      "Vale.Lib.Seqs.lemma_list_to_seq",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "int_inversion",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_FStar.List.Tot.Base.length"
      ],
      0,
      "8001dd6713ef9bc819bc5b5e06e5a68b"
    ]
  ]
]