[
  "X�\u000e\f�F \u0016{\"B��S��",
  [
    [
      "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,
      "d0831004c106d4a6e491913df89c36c8"
    ],
    [
      "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,
      "8c4baecd1478860268fb4597c4430f11"
    ],
    [
      "Vale.Lib.Seqs.seq_map_i_indexed",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "208bff8090c141381c2f436c42b20ade"
    ],
    [
      "Vale.Lib.Seqs.seq_map_i",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "16aa0b661cca77d3b2d3ec018c57b79a"
    ],
    [
      "Vale.Lib.Seqs.seq_map_internal_associative",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "8af1de09b901252ab5d9cf0378c51ab1"
    ],
    [
      "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,
      "b2774833f23e012f9c6dcb6c7aa3a26f"
    ],
    [
      "Vale.Lib.Seqs.slice_seq_map_commute",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.FunctionalExtensionality_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,
      "c4c0d867d9a1156e08f86aadb5094af7"
    ]
  ]
]