[
"����\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"
]
]
]