[
  "WÅ!‰˜\u001cBÀ*5\t ¯.ö+",
  [
    [
      "Hacl.Streaming.Lemmas.repeat_f",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "refinement_interpretation_Tm_refine_36fc4a3bd4656ab76ef7de64c5b7198c",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "03e417eb71bb6bfa92fba1f4422c79ea"
    ],
    [
      "Hacl.Streaming.Lemmas.repeat_l",
      1,
      2,
      1,
      [ "@query" ],
      0,
      "f6a6761b7a799c6d1a80bd5bcaa7a1d1"
    ],
    [
      "Hacl.Streaming.Lemmas.repeat_l",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "primitive_Prims.op_Modulus", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_36fc4a3bd4656ab76ef7de64c5b7198c",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_a85d2f9814c6432199ce1df848a1e99c"
      ],
      0,
      "c8c080aa8633bda18896b7a346847524"
    ],
    [
      "Hacl.Streaming.Lemmas.repeat_l_input",
      1,
      2,
      1,
      [ "@query" ],
      0,
      "5d76a974df1ef05f2b52f3d1a027ea09"
    ],
    [
      "Hacl.Streaming.Lemmas.repeat_l_input",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "eq2-interp",
        "equation_Hacl.Streaming.Lemmas.repeat_l", "equation_Prims.pos",
        "equation_Prims.squash",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_36fc4a3bd4656ab76ef7de64c5b7198c",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_a85d2f9814c6432199ce1df848a1e99c"
      ],
      0,
      "8a4082709e5c669b75fe514b236e34dc"
    ],
    [
      "Hacl.Streaming.Lemmas.update_full_is_repeat_blocks",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32", "eq2-interp",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_Hacl.Streaming.Lemmas.uint8", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
        "equation_Lib.UpdateMulti.uint8", "equation_Prims.pos",
        "equation_Prims.squash",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_36fc4a3bd4656ab76ef7de64c5b7198c",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "1d80e40115aea179522c483c943211cc"
    ],
    [
      "Hacl.Streaming.Lemmas.update_full_is_repeat_blocks",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32", "eq2-interp",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_Hacl.Streaming.Lemmas.uint8", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
        "equation_Lib.UpdateMulti.uint8", "equation_Prims.pos",
        "equation_Prims.squash",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_36fc4a3bd4656ab76ef7de64c5b7198c",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "68fff4c7c124635288bad1cb974494fa"
    ],
    [
      "Hacl.Streaming.Lemmas.update_full_is_repeat_blocks",
      3,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_84cd3cec5e8535714af03446bb2b6dd9_5",
        "binder_x_b72a68bdf8d51e4ab675643707e06c74_1",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Prims.LexTop@tok",
        "equation_FStar.Pervasives.Native.fst",
        "equation_FStar.Pervasives.Native.snd",
        "equation_FStar.Seq.Properties.split",
        "equation_Hacl.Streaming.Lemmas.repeat_f",
        "equation_Hacl.Streaming.Lemmas.repeat_l",
        "equation_Hacl.Streaming.Lemmas.uint8", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.length",
        "equation_Lib.Sequence.repeat_blocks_f",
        "equation_Lib.UpdateMulti.split_block",
        "equation_Lib.UpdateMulti.uint8",
        "equation_Lib.UpdateMulti.update_full", "equation_Prims.nat",
        "equation_Prims.pos", "function_token_typing_Lib.IntTypes.uint8",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "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_slice",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.slice_is_empty",
        "lemma_FStar.Seq.Properties.slice_length",
        "lemma_FStar.Seq.Properties.slice_slice",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "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_05cd8ba92400dbac4e4b5941c9adde11",
        "refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_36fc4a3bd4656ab76ef7de64c5b7198c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_6418319cfc67d818d590ac71a5206b3d",
        "refinement_interpretation_Tm_refine_69505886a99bc48ceeb322f859e1df81",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
        "refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1",
        "refinement_interpretation_Tm_refine_b8962fd0f5d8f8be2e7d640a92136bbe",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d79c091f9f8d535d3927be7ed43bc1ba",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_ebb6b88bcdebc331a6787f1f7d3095a2",
        "token_correspondence_Hacl.Streaming.Lemmas.repeat_f",
        "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.length",
        "well-founded-ordering-on-nat"
      ],
      0,
      "971a559544d4d8362e773ea1bc67caf1"
    ],
    [
      "Hacl.Streaming.Lemmas.repeat_blocks_extensionality",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
        "equation_Lib.Sequence.seq", "equation_Prims.nat",
        "equation_Prims.pos", "int_inversion",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Division",
        "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_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_7af7abfd9fa791df66706ab563886df2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "typing_Lib.IntTypes.bits", "typing_Lib.Sequence.length",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "6b46534ab4ebfd13933f24cc385fc022"
    ],
    [
      "Hacl.Streaming.Lemmas.repeat_blocks_extensionality",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "90fa7e88dad54e7828fa08dec91df714"
    ],
    [
      "Hacl.Streaming.Lemmas.repeat_blocks_extensionality",
      3,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.seq",
        "equation_Prims.nat", "equation_Prims.pos", "int_inversion",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_Division", "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_44540322a5aeeac77ad2eb12638c2b4f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "typing_FStar.Seq.Base.length", "typing_Lib.Sequence.length"
      ],
      0,
      "e264f016093bbffca12264346d174ab9"
    ]
  ]
]