[
  "����\u0019��o\u0013�\t�� �",
  [
    [
      "Vale.Lib.BufferViewHelpers.lemma_dv_equal",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_FStar.Seq.Properties.lseq",
        "fuel_guarded_inversion_LowStar.BufferView.Down.view",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_LowStar.BufferView.Down.as_buffer_mk_buffer_view",
        "lemma_LowStar.BufferView.Down.get_view_mk_buffer_view",
        "refinement_interpretation_Tm_refine_0420cb069f6b97cfb0e6fcf072dde420",
        "refinement_interpretation_Tm_refine_5c1a36192552df8b2e8ed84ee439c0a5",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e"
      ],
      0,
      "86c07147ca53528f59839bf76dd42460"
    ],
    [
      "Vale.Lib.BufferViewHelpers.lemma_uv_equal",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "eq2-interp",
        "equation_FStar.Seq.Properties.lseq",
        "equation_LowStar.BufferView.Down.buffer", "equation_Prims.pos",
        "equation_Prims.squash",
        "fuel_guarded_inversion_FStar.Pervasives.dtuple4",
        "fuel_guarded_inversion_LowStar.BufferView.Up.view",
        "function_token_typing_Prims.__cache_version_number__",
        "l_and-interp", "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_LowStar.BufferView.Up.as_buffer_mk_buffer",
        "primitive_Prims.op_Modulus",
        "proj_equation_LowStar.BufferView.Up.View_n",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_32a927c4be2ea7459bf10eff6091102f",
        "refinement_interpretation_Tm_refine_67af973f8e55596e52b910067cf246d5",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_78f8ef901dd86a539299c59796b61946",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "typing_LowStar.BufferView.Up.__proj__View__item__n"
      ],
      0,
      "1250f68899c48322ad45d3c13a95aff7"
    ],
    [
      "Vale.Lib.BufferViewHelpers.lemma_uv_equal",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "eq2-interp",
        "equation_Prims.pos", "equation_Prims.squash",
        "fuel_guarded_inversion_LowStar.BufferView.Up.view",
        "function_token_typing_Prims.__cache_version_number__",
        "l_and-interp", "proj_equation_LowStar.BufferView.Up.View_n",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_LowStar.BufferView.Up.__proj__View__item__n"
      ],
      0,
      "32ab07cdc41589ae486ed1ae5d72bb2d"
    ]
  ]
]