[ "M\u0019:\u0011\u0007\nh", [ [ "Vale.Lib.Lists.singleton_list_rev", 1, 2, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.rev_acc.fuel_instrumented", "@query", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "data_typing_intro_Prims.Cons@tok", "data_typing_intro_Prims.Nil@tok", "equation_FStar.List.Tot.Base.rev", "equation_with_fuel_FStar.List.Tot.Base.rev_acc.fuel_instrumented", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a" ], 0, "e23613eeec10926df4386e13e675d73b" ], [ "Vale.Lib.Lists.list_cons_is_append", 1, 2, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented", "@query", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "data_typing_intro_Prims.Cons@tok", "data_typing_intro_Prims.Nil@tok", "equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a" ], 0, "ec90c6e9e8d5b54eb433eff39664b9ff" ], [ "Vale.Lib.Lists.singleton_list_seq", 1, 2, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.index.fuel_instrumented", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "data_typing_intro_Prims.Cons@tok", "data_typing_intro_Prims.Nil@tok", "equation_FStar.List.Tot.Base.hd", "equation_Prims.nat", "equation_with_fuel_FStar.List.Tot.Base.index.fuel_instrumented", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_create_len", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_eq_intro", "lemma_FStar.Seq.Base.lemma_index_create", "primitive_Prims.op_Addition", "primitive_Prims.op_Equality", "projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c86aba5c6243e6b7f9a4b0ad41b4e9a0", "refinement_interpretation_Tm_refine_d2d1ea66f2b3a92c2deb42edcbb784ce", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "typing_FStar.List.Tot.Base.index", "typing_FStar.List.Tot.Base.length", "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Properties.seq_of_list" ], 0, "8950ea4e0217e8c8766d3a46e8ec42c3" ], [ "Vale.Lib.Lists.list_append_length", 1, 1, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.append.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented", "@query", "binder_x_0a56e3de562c08d8ab59f4ac6f626a98_2", "binder_x_0a56e3de562c08d8ab59f4ac6f626a98_3", "binder_x_fe28d8bcde588226b4e538b35321de05_1", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "equation_Prims.nat", "equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "fuel_guarded_inversion_Prims.list", "int_inversion", "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "subterm_ordering_Prims.Cons", "typing_FStar.List.Tot.Base.append", "typing_FStar.List.Tot.Base.length" ], 0, "5ea45fcb34e9acdcfa138b77d075193c" ], [ "Vale.Lib.Lists.list_append_index", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "bool_typing", "equation_Prims.nat", "equation_Prims.squash", "int_inversion", "primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "36315ad9160b7a139b1c2e2006316dec" ], [ "Vale.Lib.Lists.list_append_index", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "bool_typing", "equation_Prims.squash", "primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "5638547c1243851dca7fb58fc4269aaa" ], [ "Vale.Lib.Lists.list_append_index", 3, 1, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented", "@fuel_correspondence_FStar.List.Tot.Base.index.fuel_instrumented", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.append.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.index.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "binder_x_0a56e3de562c08d8ab59f4ac6f626a98_2", "binder_x_0a56e3de562c08d8ab59f4ac6f626a98_3", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_4", "binder_x_fe28d8bcde588226b4e538b35321de05_1", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "equation_FStar.List.Tot.Base.hd", "equation_FStar.List.Tot.Base.tail", "equation_FStar.List.Tot.Base.tl", "equation_Prims.nat", "equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented", "equation_with_fuel_FStar.List.Tot.Base.index.fuel_instrumented", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "fuel_guarded_inversion_Prims.list", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "primitive_Prims.op_Addition", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThan", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c86aba5c6243e6b7f9a4b0ad41b4e9a0", "subterm_ordering_Prims.Cons", "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "typing_FStar.List.Tot.Base.append", "unit_inversion", "unit_typing" ], 0, "a2ba62d8076e8b84ebdf88f7e99a2f77" ], [ "Vale.Lib.Lists.append_list_seq", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@query", "binder_x_0a56e3de562c08d8ab59f4ac6f626a98_2", "binder_x_0a56e3de562c08d8ab59f4ac6f626a98_3", "binder_x_fe28d8bcde588226b4e538b35321de05_1", "constructor_distinct_Tm_unit", "equation_Prims.nat", "equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_eq_intro", "lemma_FStar.Seq.Base.lemma_index_app1", "lemma_FStar.Seq.Base.lemma_index_app2", "lemma_FStar.Seq.Base.lemma_len_append", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThan", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Cons_a", "refinement_interpretation_Tm_refine_29865b3e2df22a2c020de4bfd5a89179", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b", "refinement_interpretation_Tm_refine_c4ff8e69afa98d84e6a0fb3bbbc650c0", "refinement_interpretation_Tm_refine_c86aba5c6243e6b7f9a4b0ad41b4e9a0", "refinement_interpretation_Tm_refine_d2d1ea66f2b3a92c2deb42edcbb784ce", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "typing_FStar.List.Tot.Base.append", "typing_FStar.List.Tot.Base.length", "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Properties.seq_of_list" ], 0, "40e31d9597d9454c9635518fedbc1603" ], [ "Vale.Lib.Lists.from_list_le", 1, 1, 1, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "binder_x_0ac2f7b25dff899a09cad33bdd7540a2_0", "bool_typing", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "fuel_guarded_inversion_Prims.list", "projection_inverse_Prims.Cons_tl", "subterm_ordering_Prims.Cons" ], 0, "1fafc8a3a7d0e05779a6127740a747bc" ], [ "Vale.Lib.Lists.lemma_from_list_le", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "902394ac8e9978a1aa02cafb6d9189f3" ], [ "Vale.Lib.Lists.lemma_from_list_le", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "e526171deb72971a55fe975c0d63482b" ], [ "Vale.Lib.Lists.lemma_from_list_le", 3, 1, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_correspondence_FStar.List.Tot.Base.rev_acc.fuel_instrumented", "@fuel_correspondence_FStar.UInt.from_vec.fuel_instrumented", "@fuel_correspondence_Vale.Lib.Lists.from_list_le.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_irrelevance_FStar.UInt.from_vec.fuel_instrumented", "@fuel_irrelevance_Vale.Lib.Lists.from_list_le.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "binder_x_0ac2f7b25dff899a09cad33bdd7540a2_0", "bool_inversion", "bool_typing", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "data_elim_Prims.Cons", "data_typing_intro_Prims.Cons@tok", "data_typing_intro_Prims.Nil@tok", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "equation_FStar.BitVector.bv_t", "equation_FStar.List.Tot.Base.op_At", "equation_FStar.List.Tot.Base.rev", "equation_FStar.UInt.uint_t", "equation_Prims.eqtype", "equation_Prims.nat", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "equation_with_fuel_FStar.List.Tot.Base.rev_acc.fuel_instrumented", "equation_with_fuel_FStar.UInt.from_vec.fuel_instrumented", "equation_with_fuel_Vale.Lib.Lists.from_list_le.fuel_instrumented", "fuel_guarded_inversion_Prims.list", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.bool", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "lemma_FStar.List.Tot.Properties.append_length", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_eq_intro", "lemma_FStar.Seq.Base.lemma_index_app1", "lemma_FStar.Seq.Base.lemma_index_app2", "lemma_FStar.Seq.Base.lemma_index_create", "lemma_FStar.Seq.Base.lemma_index_slice", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.Seq.Base.lemma_len_slice", "primitive_Prims.op_Addition", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a", "refinement_interpretation_Tm_refine_3470787130ed719a6675e4c9599659d3", "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_4aa5c7e663f2b15889d438d88a10b639", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b", "refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d2d1ea66f2b3a92c2deb42edcbb784ce", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_e2d5d62a90ceed8a6faf9d20615f4e1e", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "subterm_ordering_Prims.Cons", "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "token_correspondence_Vale.Lib.Lists.from_list_le.fuel_instrumented", "typing_FStar.List.Tot.Base.length", "typing_FStar.List.Tot.Base.rev", "typing_FStar.List.Tot.Base.rev_acc", "typing_FStar.Seq.Properties.seq_of_list", "typing_FStar.UInt.from_vec" ], 0, "a83159d80f39abf7c8ec33197d9018ef" ], [ "Vale.Lib.Lists.lemma_from_list_be", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "0b21671b435fc116fab71bb56cb253fd" ], [ "Vale.Lib.Lists.lemma_from_list_be", 2, 1, 0, [ "@query", "equation_Vale.Lib.Lists.from_list_be" ], 0, "5e97b484585a1c39d79d63586f1e8e7c" ] ] ]