[
  "�B���Tg\u0014\u0003=�!�*�",
  [
    [
      "Collections.Seqs.lemma_slice_first_exactly_in_append",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "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_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Seq.Base.length"
      ],
      0,
      "c1269123fde34f5f374dfde969b3571c"
    ],
    [
      "Collections.Seqs.lemma_all_but_last_append",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "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_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Seq.Base.length"
      ],
      0,
      "a1fba863ac51bfd3b6a6b75191a0f5d2"
    ],
    [
      "Collections.Seqs.seq_map_i_indexed",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "e67da05aa6afa22370d911866e682b90"
    ],
    [
      "Collections.Seqs.seq_map_i",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "cf4d4e36428276e854950baa8ecf688a"
    ],
    [
      "Collections.Seqs.seq_map_internal_associative",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "a48ce9bbabaf9ac740377d0ae0a27b55"
    ],
    [
      "Collections.Seqs.slice_append_adds",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Seq.Base.length"
      ],
      0,
      "7d3c0755fb14b490733b15924e00852c"
    ],
    [
      "Collections.Seqs.slice_seq_map_commute",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
        "Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Collections.Seqs_s.compose",
        "equation_Collections.Seqs_s.seq_map", "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "lemma_FStar.Seq.Base.lemma_init_len",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3"
      ],
      0,
      "777df4afb8489225114c979c8820069d"
    ]
  ]
]