[
  "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,
      "4cf06d6985216de576341629e3d3144f"
    ],
    [
      "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,
      "a4fc215f5b0cc206029c97d664ae0f0e"
    ],
    [
      "Vale.Lib.Seqs.seq_map_i_indexed",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "71d60345d9bd23e00c5cf68f4e6316c3"
    ],
    [
      "Vale.Lib.Seqs.seq_map_i",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "2aaa17b5c8cf47f460a469eabe4a40d5"
    ],
    [
      "Vale.Lib.Seqs.seq_map_internal_associative",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "98e8a63cb2aecfe620a08602b2255b2e"
    ],
    [
      "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,
      "06567b5d92e10c0d608fe06db66f159c"
    ],
    [
      "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,
      "ebae279d91f8e24a759ca579b15dc38e"
    ]
  ]
]