[ "XW;$\u0003ug", [ [ "Catala.Translation.Helpers.typ_process_exceptions_f", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "Catala.LambdaCalculus_interpretation_Tm_arrow_0afe855ee0dd04a9f1572a7d68b10fa7", "Catala.LambdaCalculus_interpretation_Tm_arrow_ed0c592d82dfd5a47d39e42cf9d52a55", "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Prims_pretyping_ae567c2fb75be05905677af440075565", "equation_Catala.LambdaCalculus.extend", "equation_Catala.LambdaCalculus.var", "equation_FStar.FunctionalExtensionality.feq", "equation_Prims.nat", "function_token_typing_Prims.__cache_version_number__", "int_typing", "interpretation_Tm_abs_1312e4782c558ee50ab7a5e0bfd49851", "interpretation_Tm_abs_683fecef0f32ab9df689545bd34ec676", "lemma_FStar.FunctionalExtensionality.feq_on_domain", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "token_correspondence_Catala.LambdaCalculus.extend", "typing_Tm_abs_1312e4782c558ee50ab7a5e0bfd49851", "typing_Tm_abs_683fecef0f32ab9df689545bd34ec676" ], 0, "143b9302181ab46ccd0e5d15c2e0941f" ], [ "Catala.Translation.Helpers.build_default_translation_typing", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.typing_list.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.typing.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.typing_list.fuel_instrumented", "@query", "Catala.LambdaCalculus_interpretation_Tm_arrow_0afe855ee0dd04a9f1572a7d68b10fa7", "Catala.LambdaCalculus_interpretation_Tm_arrow_ed0c592d82dfd5a47d39e42cf9d52a55", "Catala.LambdaCalculus_pretyping_8ab521cb5d1069fb182eea898efa7c42", "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion", "constructor_distinct_Catala.LambdaCalculus.EAbs", "constructor_distinct_Catala.LambdaCalculus.TBool", "constructor_distinct_Catala.LambdaCalculus.TOption", "constructor_distinct_Catala.LambdaCalculus.TUnit", "data_typing_intro_Catala.LambdaCalculus.TArrow@tok", "data_typing_intro_Catala.LambdaCalculus.TOption@tok", "equality_tok_Catala.LambdaCalculus.TBool@tok", "equality_tok_Catala.LambdaCalculus.TUnit@tok", "equation_Catala.LambdaCalculus.extend", "equation_Catala.LambdaCalculus.var", "equation_Catala.Translation.Helpers.process_exceptions_f", "equation_FStar.FunctionalExtensionality.feq", "equation_Prims.nat", "equation_with_fuel_Catala.LambdaCalculus.typing.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.typing_list.fuel_instrumented", "function_token_typing_Prims.__cache_version_number__", "int_typing", "interpretation_Tm_abs_1312e4782c558ee50ab7a5e0bfd49851", "interpretation_Tm_abs_683fecef0f32ab9df689545bd34ec676", "lemma_FStar.FunctionalExtensionality.feq_on_domain", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0", "projection_inverse_Catala.LambdaCalculus.EAbs_body", "projection_inverse_Catala.LambdaCalculus.EAbs_vty", "projection_inverse_Catala.LambdaCalculus.TArrow_tin", "projection_inverse_Catala.LambdaCalculus.TOption_a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "token_correspondence_Catala.LambdaCalculus.extend", "typing_Catala.LambdaCalculus.typing", "typing_Catala.LambdaCalculus.typing_list", "typing_Catala.Translation.Helpers.process_exceptions_f", "typing_Tm_abs_1312e4782c558ee50ab7a5e0bfd49851", "typing_Tm_abs_683fecef0f32ab9df689545bd34ec676", "typing_tok_Catala.LambdaCalculus.TBool@tok", "typing_tok_Catala.LambdaCalculus.TUnit@tok" ], 0, "33e0affa7261e9067cdbce3ddcddf4e2" ], [ "Catala.Translation.Helpers.process_exceptions_untouched_by_subst", 1, 9, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.LambdaCalculus.subst.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.subst.fuel_instrumented", "@query", "Catala.LambdaCalculus_interpretation_Tm_arrow_732ef78b9bfa783d08279e5be1df507c", "Prims_pretyping_ae567c2fb75be05905677af440075565", "constructor_distinct_Catala.LambdaCalculus.EAbs", "constructor_distinct_Catala.LambdaCalculus.EApp", "constructor_distinct_Catala.LambdaCalculus.ECatchEmptyError", "constructor_distinct_Catala.LambdaCalculus.ELit", "constructor_distinct_Catala.LambdaCalculus.EMatchOption", "constructor_distinct_Catala.LambdaCalculus.ENone", "constructor_distinct_Catala.LambdaCalculus.ESome", "constructor_distinct_Catala.LambdaCalculus.EVar", "data_typing_intro_Catala.LambdaCalculus.EAbs@tok", "data_typing_intro_Catala.LambdaCalculus.EApp@tok", "data_typing_intro_Catala.LambdaCalculus.ECatchEmptyError@tok", "data_typing_intro_Catala.LambdaCalculus.ELit@tok", "data_typing_intro_Catala.LambdaCalculus.EMatchOption@tok", "data_typing_intro_Catala.LambdaCalculus.ESome@tok", "data_typing_intro_Catala.LambdaCalculus.EVar@tok", "data_typing_intro_Catala.LambdaCalculus.LError@tok", "data_typing_intro_Catala.LambdaCalculus.TArrow@tok", "data_typing_intro_Catala.LambdaCalculus.TOption@tok", "equality_tok_Catala.LambdaCalculus.ConflictError@tok", "equality_tok_Catala.LambdaCalculus.ENone@tok", "equality_tok_Catala.LambdaCalculus.LUnit@tok", "equality_tok_Catala.LambdaCalculus.TUnit@tok", "equation_Catala.LambdaCalculus.increment", "equation_Catala.LambdaCalculus.var", "equation_Catala.LambdaCalculus.var_to_exp", "equation_Catala.Translation.Helpers.process_exceptions_f", "equation_Prims.nat", "equation_with_fuel_Catala.LambdaCalculus.subst.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.subst_abs.fuel_instrumented", "fuel_token_correspondence_Catala.LambdaCalculus.subst_abs.fuel_instrumented_token", "function_token_typing_Prims.__cache_version_number__", "int_typing", "primitive_Prims.op_Addition", "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Catala.LambdaCalculus.EAbs_body", "projection_inverse_Catala.LambdaCalculus.EAbs_vty", "projection_inverse_Catala.LambdaCalculus.EApp_arg", "projection_inverse_Catala.LambdaCalculus.EApp_fn", "projection_inverse_Catala.LambdaCalculus.EApp_tau_arg", "projection_inverse_Catala.LambdaCalculus.ECatchEmptyError_catch_with", "projection_inverse_Catala.LambdaCalculus.ECatchEmptyError_to_try", "projection_inverse_Catala.LambdaCalculus.ELit_l", "projection_inverse_Catala.LambdaCalculus.EMatchOption_arg", "projection_inverse_Catala.LambdaCalculus.EMatchOption_none", "projection_inverse_Catala.LambdaCalculus.EMatchOption_some", "projection_inverse_Catala.LambdaCalculus.EMatchOption_tau_some", "projection_inverse_Catala.LambdaCalculus.ESome_s", "projection_inverse_Catala.LambdaCalculus.EVar_v", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_66a04fe873406083a229e09b1c833909", "refinement_interpretation_Tm_refine_a392bfba80da306fafdb3d849a464ab4", "token_correspondence_Catala.LambdaCalculus.subst.fuel_instrumented", "token_correspondence_Catala.LambdaCalculus.subst_abs.fuel_instrumented", "typing_Catala.LambdaCalculus.increment", "typing_Catala.Translation.Helpers.process_exceptions_f", "typing_tok_Catala.LambdaCalculus.ConflictError@tok", "typing_tok_Catala.LambdaCalculus.ENone@tok", "typing_tok_Catala.LambdaCalculus.LUnit@tok", "typing_tok_Catala.LambdaCalculus.TUnit@tok" ], 0, "5964f8288c016f27611188cfa97624a6" ], [ "Catala.Translation.Helpers.take_l_steps", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.LambdaCalculus.step.fuel_instrumented", "@query", "Catala.LambdaCalculus_pretyping_fabd258754d8bab26d9bc0ad1a882a83", "Prims_pretyping_ae567c2fb75be05905677af440075565", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2", "binder_x_f80c75f1bb9a1307efb471ddc3570834_1", "data_typing_intro_Catala.LambdaCalculus.ENone@tok", "disc_equation_FStar.Pervasives.Native.None", "disc_equation_FStar.Pervasives.Native.Some", "equation_Catala.Translation.Helpers.typed_l_exp", "equation_Prims.nat", "equation_with_fuel_Catala.LambdaCalculus.step.fuel_instrumented", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "kinding_Catala.LambdaCalculus.exp@tok", "lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction", "proj_equation_FStar.Pervasives.Native.Some_v", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Some_v", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_d5485f8c94130f85952cddf1019830bb", "typing_Catala.LambdaCalculus.step", "well-founded-ordering-on-nat" ], 0, "0ebf747631c6235c501b01bbd431d70f" ], [ "Catala.Translation.Helpers.take_l_steps_transitive", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2d1d82d8e7b45c4b826c650f2ee22c70", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "fb0875233a6681c0bf006b58f08a0338" ], [ "Catala.Translation.Helpers.take_l_steps_transitive", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", "@fuel_correspondence_Catala.Translation.Helpers.take_l_steps.fuel_instrumented", "@fuel_irrelevance_Catala.Translation.Helpers.take_l_steps.fuel_instrumented", "@query", "Catala.LambdaCalculus_pretyping_fabd258754d8bab26d9bc0ad1a882a83", "Prims_pretyping_ae567c2fb75be05905677af440075565", "binder_x_8ab521cb5d1069fb182eea898efa7c42_0", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_3", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_4", "binder_x_f80c75f1bb9a1307efb471ddc3570834_1", "bool_inversion", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_FStar.Pervasives.Native.Some", "constructor_distinct_Tm_unit", "data_typing_intro_Catala.LambdaCalculus.ENone@tok", "disc_equation_FStar.Pervasives.Native.None", "disc_equation_FStar.Pervasives.Native.Some", "equation_Catala.Translation.Helpers.typed_l_exp", "equation_Prims.nat", "equation_with_fuel_Catala.Translation.Helpers.take_l_steps.fuel_instrumented", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "kinding_Catala.LambdaCalculus.exp@tok", "lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_Addition", "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction", "proj_equation_FStar.Pervasives.Native.Some_v", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.None_a", "projection_inverse_FStar.Pervasives.Native.Some_a", "projection_inverse_FStar.Pervasives.Native.Some_v", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_d5485f8c94130f85952cddf1019830bb", "typing_Catala.LambdaCalculus.empty", "typing_Catala.LambdaCalculus.step", "typing_Catala.LambdaCalculus.typing", "unit_inversion", "unit_typing", "well-founded-ordering-on-nat" ], 0, "efd12261adda6a797b529668c6c40d06" ], [ "Catala.Translation.Helpers.step_lift_commute_non_value", 1, 2, 1, [ "@MaxIFuel_assumption", "@fuel_correspondence_Catala.LambdaCalculus.step.fuel_instrumented", "@query", "Prims_pretyping_0da546199211a769a972571cdb3aec67", "bool_inversion", "equality_tok_Prims.T@tok", "equation_Catala.Translation.Helpers.typed_l_exp", "equation_Prims.eq2", "equation_Prims.l_True", "equation_Prims.squash", "equation_Prims.subtype_of", "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_d5485f8c94130f85952cddf1019830bb", "typing_tok_Prims.T@tok" ], 0, "7ca2a4bf2f69213d17aa0a2471759ad4" ], [ "Catala.Translation.Helpers.is_stepping_agnostic_lift", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_Prims.l_Forall", "equation_Prims.squash", "equation_Prims.subtype_of", "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "6eb5f22d8aa332b43c7ca8b6f0bbe7c4" ], [ "Catala.Translation.Helpers.l_values_dont_step", 1, 2, 1, [ "@query", "assumption_Catala.LambdaCalculus.exp__uu___haseq", "assumption_Catala.LambdaCalculus.list_step_result__uu___haseq", "assumption_FStar.Pervasives.Native.option__uu___haseq", "kinding_Catala.LambdaCalculus.exp@tok" ], 0, "ae5ed7f5f262164fd7b5647f2113bf69" ], [ "Catala.Translation.Helpers.l_values_dont_step", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.LambdaCalculus.is_value.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.step.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.step_list.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.is_value.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.step_list.fuel_instrumented", "@query", "Catala.LambdaCalculus_pretyping_fabd258754d8bab26d9bc0ad1a882a83", "Prims_pretyping_ae567c2fb75be05905677af440075565", "assumption_Catala.LambdaCalculus.exp__uu___haseq", "assumption_FStar.Pervasives.Native.option__uu___haseq", "binder_x_fabd258754d8bab26d9bc0ad1a882a83_0", "bool_inversion", "constructor_distinct_Catala.LambdaCalculus.Bad", "constructor_distinct_Catala.LambdaCalculus.EAbs", "constructor_distinct_Catala.LambdaCalculus.ELit", "constructor_distinct_Catala.LambdaCalculus.ENone", "constructor_distinct_Catala.LambdaCalculus.ESome", "constructor_distinct_Catala.LambdaCalculus.EThunk", "constructor_distinct_Prims.Nil", "data_typing_intro_Catala.LambdaCalculus.ENone@tok", "data_typing_intro_Prims.Nil@tok", "disc_equation_Catala.LambdaCalculus.EAbs", "disc_equation_Catala.LambdaCalculus.EList", "disc_equation_Catala.LambdaCalculus.ELit", "disc_equation_Catala.LambdaCalculus.ENone", "disc_equation_Catala.LambdaCalculus.ESome", "disc_equation_Catala.LambdaCalculus.EThunk", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "equality_tok_Catala.LambdaCalculus.Bad@tok", "equality_tok_Catala.LambdaCalculus.ENone@tok", "equation_with_fuel_Catala.LambdaCalculus.is_value.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step_list.fuel_instrumented", "fuel_guarded_inversion_Prims.list", "function_token_typing_Prims.__cache_version_number__", "int_typing", "kinding_Catala.LambdaCalculus.exp@tok", "proj_equation_Catala.LambdaCalculus.EList_l", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Catala.LambdaCalculus.EList_l", "projection_inverse_Catala.LambdaCalculus.ESome_s", "projection_inverse_Prims.Nil_a", "refinement_interpretation_Tm_refine_1db4fb469fdb010f95d88ae1c86e1d1d", "subterm_ordering_Catala.LambdaCalculus.EList", "subterm_ordering_Catala.LambdaCalculus.ESome", "typing_Catala.LambdaCalculus.is_value", "typing_Catala.LambdaCalculus.uu___is_EAbs", "typing_tok_Catala.LambdaCalculus.ENone@tok", "well-founded-ordering-on-nat" ], 0, "f8e5f4b23fe3908178cc11be93bc8620" ], [ "Catala.Translation.Helpers.l_values_dont_step", 3, 2, 1, [ "@query", "assumption_Catala.LambdaCalculus.exp__uu___haseq", "assumption_Catala.LambdaCalculus.list_step_result__uu___haseq", "assumption_FStar.Pervasives.Native.option__uu___haseq", "kinding_Catala.LambdaCalculus.exp@tok" ], 0, "d21803a41f4927e9b583c59e18188f3c" ], [ "Catala.Translation.Helpers.l_values_dont_step", 4, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.LambdaCalculus.is_value.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.step_list.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.is_value.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.step_list.fuel_instrumented", "@query", "Catala.LambdaCalculus_pretyping_fabd258754d8bab26d9bc0ad1a882a83", "assumption_Catala.LambdaCalculus.list_step_result__uu___haseq", "binder_x_b2d129bfb669b2dbbce6b10cf9a879e4_1", "binder_x_fabd258754d8bab26d9bc0ad1a882a83_0", "bool_inversion", "constructor_distinct_Catala.LambdaCalculus.Bad", "constructor_distinct_Prims.Nil", "data_typing_intro_Catala.LambdaCalculus.ENone@tok", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "equality_tok_Catala.LambdaCalculus.Bad@tok", "equation_with_fuel_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step_list.fuel_instrumented", "fuel_guarded_inversion_Catala.LambdaCalculus.exp", "fuel_guarded_inversion_Prims.list", "primitive_Prims.op_AmpAmp", "proj_equation_Prims.Cons_tl", "projection_inverse_BoxBool_proj_0", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a", "refinement_interpretation_Tm_refine_1db4fb469fdb010f95d88ae1c86e1d1d", "refinement_interpretation_Tm_refine_9a26a25b0efdc4ca31d9ba5d36ef77f5", "subterm_ordering_Prims.Cons", "token_correspondence_Catala.LambdaCalculus.is_value.fuel_instrumented", "token_correspondence_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "typing_Catala.LambdaCalculus.is_value_list" ], 0, "3e25f8d2e0e087deea78daa3f5e63aaa" ], [ "Catala.Translation.Helpers.lift_multiple_l_steps", 1, 2, 1, [ "@query" ], 0, "c802c133f612226c1374acdfa8324bc7" ], [ "Catala.Translation.Helpers.lift_multiple_l_steps", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.LambdaCalculus.step.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", "@fuel_correspondence_Catala.Translation.Helpers.take_l_steps.fuel_instrumented", "@fuel_irrelevance_Catala.Translation.Helpers.take_l_steps.fuel_instrumented", "@query", "Catala.LambdaCalculus_pretyping_fabd258754d8bab26d9bc0ad1a882a83", "Catala.Translation.Helpers_interpretation_Tm_arrow_38fe97801abd7169d6afa4da52bdb68d", "Prims_pretyping_ae567c2fb75be05905677af440075565", "binder_x_8ab521cb5d1069fb182eea898efa7c42_0", "binder_x_8ab521cb5d1069fb182eea898efa7c42_1", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_4", "binder_x_cfda227c666c2b0ca46650203c1c4ecf_5", "binder_x_f80c75f1bb9a1307efb471ddc3570834_2", "binder_x_f80c75f1bb9a1307efb471ddc3570834_3", "bool_inversion", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_FStar.Pervasives.Native.Some", "data_typing_intro_Catala.LambdaCalculus.ENone@tok", "disc_equation_FStar.Pervasives.Native.None", "disc_equation_FStar.Pervasives.Native.Some", "eq2-interp", "equation_Catala.Translation.Helpers.is_stepping_agnostic_lift", "equation_Catala.Translation.Helpers.not_l_value", "equation_Catala.Translation.Helpers.step_lift_commute_non_value", "equation_Catala.Translation.Helpers.stepping_agnostic_lift", "equation_Catala.Translation.Helpers.stepping_context", "equation_Catala.Translation.Helpers.typed_l_exp", "equation_Prims.nat", "equation_with_fuel_Catala.LambdaCalculus.step.fuel_instrumented", "equation_with_fuel_Catala.Translation.Helpers.take_l_steps.fuel_instrumented", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "kinding_Catala.LambdaCalculus.exp@tok", "lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction", "proj_equation_FStar.Pervasives.Native.Some_v", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.None_a", "projection_inverse_FStar.Pervasives.Native.Some_a", "projection_inverse_FStar.Pervasives.Native.Some_v", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c788a929583bc5fd370780c42b0ee234", "refinement_interpretation_Tm_refine_d5485f8c94130f85952cddf1019830bb", "refinement_interpretation_Tm_refine_e1e5cfe7267eb04a8960036ae88380cb", "typing_Catala.LambdaCalculus.empty", "typing_Catala.LambdaCalculus.step", "typing_Catala.LambdaCalculus.typing", "unit_inversion", "unit_typing", "well-founded-ordering-on-nat" ], 0, "b11f10cda30c9c61b3501c24f3b8c310" ], [ "Catala.Translation.Helpers.if_cond_lift'", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.LambdaCalculus.is_value.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.typing.fuel_instrumented", "@query", "bool_inversion", "constructor_distinct_Catala.LambdaCalculus.EIf", "data_typing_intro_Catala.LambdaCalculus.EIf@tok", "equality_tok_Catala.LambdaCalculus.TBool@tok", "equation_Catala.LambdaCalculus.empty", "equation_Catala.Translation.Helpers.typed_l_exp", "equation_with_fuel_Catala.LambdaCalculus.is_value.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.typing.fuel_instrumented", "primitive_Prims.op_AmpAmp", "projection_inverse_BoxBool_proj_0", "projection_inverse_Catala.LambdaCalculus.EIf_bfalse", "projection_inverse_Catala.LambdaCalculus.EIf_btrue", "projection_inverse_Catala.LambdaCalculus.EIf_test", "refinement_interpretation_Tm_refine_d5485f8c94130f85952cddf1019830bb", "typing_Catala.LambdaCalculus.empty", "typing_Catala.LambdaCalculus.typing", "typing_tok_Catala.LambdaCalculus.TBool@tok" ], 0, "3076e194fecd0a04ba5711e9d7670385" ], [ "Catala.Translation.Helpers.if_cond_lift_is_stepping_agnostic", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.LambdaCalculus.step.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.step.fuel_instrumented", "@query", "Catala.LambdaCalculus_pretyping_fabd258754d8bab26d9bc0ad1a882a83", "Catala.Translation.Helpers_interpretation_Tm_arrow_38fe97801abd7169d6afa4da52bdb68d", "bool_inversion", "constructor_distinct_Catala.LambdaCalculus.EIf", "data_typing_intro_Catala.LambdaCalculus.ENone@tok", "disc_equation_FStar.Pervasives.Native.Some", "eq2-interp", "equality_tok_Catala.LambdaCalculus.TBool@tok", "equation_Catala.Translation.Helpers.if_cond_lift_", "equation_Catala.Translation.Helpers.not_l_value", "equation_Catala.Translation.Helpers.step_lift_commute_non_value", "equation_Catala.Translation.Helpers.stepping_context", "equation_Catala.Translation.Helpers.typed_l_exp", "equation_with_fuel_Catala.LambdaCalculus.step.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step_if.fuel_instrumented", "interpretation_Tm_abs_641cf861833e1c856e82a38e30e14275", "proj_equation_FStar.Pervasives.Native.Some_v", "projection_inverse_BoxBool_proj_0", "projection_inverse_Catala.LambdaCalculus.EIf_bfalse", "projection_inverse_Catala.LambdaCalculus.EIf_btrue", "projection_inverse_Catala.LambdaCalculus.EIf_test", "refinement_interpretation_Tm_refine_8572abaf58b0908690b4c77b9bd5038b", "refinement_interpretation_Tm_refine_d5485f8c94130f85952cddf1019830bb", "refinement_interpretation_Tm_refine_e1e5cfe7267eb04a8960036ae88380cb", "subterm_ordering_Catala.LambdaCalculus.EIf", "true_interp", "typing_Catala.Translation.Helpers.if_cond_lift_" ], 0, "d00dd8bb9ad0636706d568784576c9cc" ], [ "Catala.Translation.Helpers.if_cond_lift", 1, 2, 1, [ "@query", "equality_tok_Catala.LambdaCalculus.TBool@tok", "equation_Catala.Translation.Helpers.is_stepping_agnostic_lift" ], 0, "86174ad51352d43d77b93c4a1db2dc34" ], [ "Catala.Translation.Helpers.app_f_lift'", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.LambdaCalculus.is_value.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.typing.fuel_instrumented", "@query", "constructor_distinct_Catala.LambdaCalculus.EApp", "data_typing_intro_Catala.LambdaCalculus.EApp@tok", "equation_Catala.LambdaCalculus.empty", "equation_Catala.Translation.Helpers.typed_l_exp", "equation_with_fuel_Catala.LambdaCalculus.is_value.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.typing.fuel_instrumented", "primitive_Prims.op_AmpAmp", "projection_inverse_BoxBool_proj_0", "projection_inverse_Catala.LambdaCalculus.EApp_arg", "projection_inverse_Catala.LambdaCalculus.EApp_fn", "projection_inverse_Catala.LambdaCalculus.EApp_tau_arg", "refinement_interpretation_Tm_refine_d5485f8c94130f85952cddf1019830bb", "typing_Catala.LambdaCalculus.empty" ], 0, "e43d70be6d1d2dcd9ddf562c95c009bd" ], [ "Catala.Translation.Helpers.app_f_lift_is_stepping_agnostic", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.LambdaCalculus.step.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.step.fuel_instrumented", "@query", "Catala.LambdaCalculus_pretyping_8ab521cb5d1069fb182eea898efa7c42", "Catala.LambdaCalculus_pretyping_fabd258754d8bab26d9bc0ad1a882a83", "Catala.Translation.Helpers_interpretation_Tm_arrow_38fe97801abd7169d6afa4da52bdb68d", "bool_inversion", "constructor_distinct_Catala.LambdaCalculus.EApp", "data_typing_intro_Catala.LambdaCalculus.ENone@tok", "data_typing_intro_Catala.LambdaCalculus.TUnit@tok", "disc_equation_FStar.Pervasives.Native.Some", "eq2-interp", "equation_Catala.Translation.Helpers.app_f_lift_", "equation_Catala.Translation.Helpers.not_l_value", "equation_Catala.Translation.Helpers.step_lift_commute_non_value", "equation_Catala.Translation.Helpers.stepping_context", "equation_Catala.Translation.Helpers.typed_l_exp", "equation_with_fuel_Catala.LambdaCalculus.step.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step_app.fuel_instrumented", "interpretation_Tm_abs_99d97efd08018271b544197c3d6fb673", "proj_equation_FStar.Pervasives.Native.Some_v", "projection_inverse_BoxBool_proj_0", "projection_inverse_Catala.LambdaCalculus.EApp_arg", "projection_inverse_Catala.LambdaCalculus.EApp_fn", "projection_inverse_Catala.LambdaCalculus.EApp_tau_arg", "refinement_interpretation_Tm_refine_8572abaf58b0908690b4c77b9bd5038b", "refinement_interpretation_Tm_refine_9d7619fada7e7cc3e29055f7763724da", "refinement_interpretation_Tm_refine_d5485f8c94130f85952cddf1019830bb", "refinement_interpretation_Tm_refine_e1e5cfe7267eb04a8960036ae88380cb", "subterm_ordering_Catala.LambdaCalculus.EApp", "true_interp", "typing_Catala.Translation.Helpers.app_f_lift_" ], 0, "3a6b677653f08ceebdd2c993e5751e75" ], [ "Catala.Translation.Helpers.app_f_lift", 1, 2, 1, [ "@query", "equation_Catala.Translation.Helpers.is_stepping_agnostic_lift" ], 0, "5b62797a4131996b4b308c346d5017e3" ], [ "Catala.Translation.Helpers.app_arg_lift'", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.LambdaCalculus.is_value.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.typing.fuel_instrumented", "@query", "bool_inversion", "constructor_distinct_Catala.LambdaCalculus.EApp", "data_typing_intro_Catala.LambdaCalculus.EApp@tok", "equation_Catala.LambdaCalculus.empty", "equation_Catala.Translation.Helpers.l_value", "equation_Catala.Translation.Helpers.typed_l_exp", "equation_with_fuel_Catala.LambdaCalculus.is_value.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.typing.fuel_instrumented", "primitive_Prims.op_AmpAmp", "projection_inverse_BoxBool_proj_0", "projection_inverse_Catala.LambdaCalculus.EApp_arg", "projection_inverse_Catala.LambdaCalculus.EApp_fn", "projection_inverse_Catala.LambdaCalculus.EApp_tau_arg", "refinement_interpretation_Tm_refine_b2a2b52af28538faeded9eec695638d7", "refinement_interpretation_Tm_refine_d5485f8c94130f85952cddf1019830bb", "token_correspondence_Catala.LambdaCalculus.is_value.fuel_instrumented", "typing_Catala.LambdaCalculus.empty", "typing_Catala.LambdaCalculus.typing" ], 0, "1eb479df49f9bd44d04668ead937ea1f" ], [ "Catala.Translation.Helpers.app_arg_lift_is_stepping_agnostic", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.LambdaCalculus.is_value.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.step.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.step.fuel_instrumented", "@query", "Catala.LambdaCalculus_pretyping_8ab521cb5d1069fb182eea898efa7c42", "Catala.LambdaCalculus_pretyping_fabd258754d8bab26d9bc0ad1a882a83", "Catala.Translation.Helpers_interpretation_Tm_arrow_38fe97801abd7169d6afa4da52bdb68d", "bool_inversion", "constructor_distinct_Catala.LambdaCalculus.EApp", "data_typing_intro_Catala.LambdaCalculus.ENone@tok", "data_typing_intro_Catala.LambdaCalculus.TUnit@tok", "disc_equation_FStar.Pervasives.Native.Some", "eq2-interp", "equation_Catala.Translation.Helpers.app_arg_lift_", "equation_Catala.Translation.Helpers.l_value", "equation_Catala.Translation.Helpers.not_l_value", "equation_Catala.Translation.Helpers.step_lift_commute_non_value", "equation_Catala.Translation.Helpers.typed_l_exp", "equation_with_fuel_Catala.LambdaCalculus.is_value.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step_app.fuel_instrumented", "interpretation_Tm_abs_e963bfe47364f5aa72ea70ed36eb1677", "proj_equation_FStar.Pervasives.Native.Some_v", "projection_inverse_BoxBool_proj_0", "projection_inverse_Catala.LambdaCalculus.EApp_arg", "projection_inverse_Catala.LambdaCalculus.EApp_fn", "projection_inverse_Catala.LambdaCalculus.EApp_tau_arg", "refinement_interpretation_Tm_refine_8572abaf58b0908690b4c77b9bd5038b", "refinement_interpretation_Tm_refine_9d7619fada7e7cc3e29055f7763724da", "refinement_interpretation_Tm_refine_b2a2b52af28538faeded9eec695638d7", "refinement_interpretation_Tm_refine_d5485f8c94130f85952cddf1019830bb", "refinement_interpretation_Tm_refine_e1e5cfe7267eb04a8960036ae88380cb", "refinement_interpretation_Tm_refine_f09c0cd2375f016f9430c14101a7da23", "subterm_ordering_Catala.LambdaCalculus.EApp", "token_correspondence_Catala.LambdaCalculus.is_value.fuel_instrumented", "true_interp", "typing_Tm_abs_e963bfe47364f5aa72ea70ed36eb1677" ], 0, "8cda1d30ae820910243655e6f58eae95" ], [ "Catala.Translation.Helpers.app_arg_lift", 1, 2, 1, [ "@query", "equation_Catala.Translation.Helpers.is_stepping_agnostic_lift" ], 0, "e93629647176b0bfbbea807bd5a2aca6" ], [ "Catala.Translation.Helpers.exceptions_head_lift'", 1, 9, 2, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.LambdaCalculus.is_value.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.typing_list.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.typing.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.typing_list.fuel_instrumented", "@query", "Catala.LambdaCalculus_interpretation_Tm_arrow_0afe855ee0dd04a9f1572a7d68b10fa7", "Catala.LambdaCalculus_interpretation_Tm_arrow_ed0c592d82dfd5a47d39e42cf9d52a55", "Catala.LambdaCalculus_pretyping_8ab521cb5d1069fb182eea898efa7c42", "Catala.LambdaCalculus_pretyping_fabd258754d8bab26d9bc0ad1a882a83", "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion", "constructor_distinct_Catala.LambdaCalculus.EAbs", "constructor_distinct_Catala.LambdaCalculus.EApp", "constructor_distinct_Catala.LambdaCalculus.ECatchEmptyError", "constructor_distinct_Catala.LambdaCalculus.EFoldLeft", "constructor_distinct_Catala.LambdaCalculus.EIf", "constructor_distinct_Catala.LambdaCalculus.EList", "constructor_distinct_Catala.LambdaCalculus.ELit", "constructor_distinct_Catala.LambdaCalculus.EMatchOption", "constructor_distinct_Catala.LambdaCalculus.ENone", "constructor_distinct_Catala.LambdaCalculus.ESome", "constructor_distinct_Catala.LambdaCalculus.EVar", "constructor_distinct_Catala.LambdaCalculus.LError", "constructor_distinct_Catala.LambdaCalculus.TArrow", "constructor_distinct_Catala.LambdaCalculus.TList", "constructor_distinct_Catala.LambdaCalculus.TOption", "constructor_distinct_FStar.Pervasives.Native.Some", "data_elim_Catala.LambdaCalculus.EAbs", "data_elim_Catala.LambdaCalculus.EApp", "data_elim_Catala.LambdaCalculus.EMatchOption", "data_elim_Catala.LambdaCalculus.EVar", "data_typing_intro_Catala.LambdaCalculus.EAbs@tok", "data_typing_intro_Catala.LambdaCalculus.EApp@tok", "data_typing_intro_Catala.LambdaCalculus.ECatchEmptyError@tok", "data_typing_intro_Catala.LambdaCalculus.EFoldLeft@tok", "data_typing_intro_Catala.LambdaCalculus.EIf@tok", "data_typing_intro_Catala.LambdaCalculus.EList@tok", "data_typing_intro_Catala.LambdaCalculus.ELit@tok", "data_typing_intro_Catala.LambdaCalculus.EMatchOption@tok", "data_typing_intro_Catala.LambdaCalculus.ENone@tok", "data_typing_intro_Catala.LambdaCalculus.ESome@tok", "data_typing_intro_Catala.LambdaCalculus.LError@tok", "data_typing_intro_Catala.LambdaCalculus.TArrow@tok", "data_typing_intro_Catala.LambdaCalculus.TList@tok", "data_typing_intro_Catala.LambdaCalculus.TOption@tok", "data_typing_intro_Catala.LambdaCalculus.TUnit@tok", "disc_equation_FStar.Pervasives.Native.None", "equality_tok_Catala.LambdaCalculus.ConflictError@tok", "equality_tok_Catala.LambdaCalculus.ENone@tok", "equality_tok_Catala.LambdaCalculus.EmptyError@tok", "equality_tok_Catala.LambdaCalculus.TBool@tok", "equality_tok_Catala.LambdaCalculus.TUnit@tok", "equation_Catala.LambdaCalculus.empty", "equation_Catala.LambdaCalculus.extend", "equation_Catala.LambdaCalculus.var", "equation_Catala.Translation.Helpers.process_exceptions_f", "equation_Catala.Translation.Helpers.typed_l_exp", "equation_FStar.FunctionalExtensionality.feq", "equation_Prims.nat", "equation_with_fuel_Catala.LambdaCalculus.is_value.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.typing.fuel_instrumented", "function_token_typing_Prims.__cache_version_number__", "int_typing", "interpretation_Tm_abs_1312e4782c558ee50ab7a5e0bfd49851", "interpretation_Tm_abs_683fecef0f32ab9df689545bd34ec676", "lemma_FStar.FunctionalExtensionality.feq_on_domain", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_Catala.LambdaCalculus.EAbs_body", "projection_inverse_Catala.LambdaCalculus.EAbs_vty", "projection_inverse_Catala.LambdaCalculus.EApp_arg", "projection_inverse_Catala.LambdaCalculus.EApp_fn", "projection_inverse_Catala.LambdaCalculus.EApp_tau_arg", "projection_inverse_Catala.LambdaCalculus.ECatchEmptyError_catch_with", "projection_inverse_Catala.LambdaCalculus.ECatchEmptyError_to_try", "projection_inverse_Catala.LambdaCalculus.EFoldLeft_f", "projection_inverse_Catala.LambdaCalculus.EFoldLeft_init", "projection_inverse_Catala.LambdaCalculus.EFoldLeft_l", "projection_inverse_Catala.LambdaCalculus.EFoldLeft_tau_elt", "projection_inverse_Catala.LambdaCalculus.EFoldLeft_tau_init", "projection_inverse_Catala.LambdaCalculus.EIf_bfalse", "projection_inverse_Catala.LambdaCalculus.EIf_btrue", "projection_inverse_Catala.LambdaCalculus.EIf_test", "projection_inverse_Catala.LambdaCalculus.EList_l", "projection_inverse_Catala.LambdaCalculus.ELit_l", "projection_inverse_Catala.LambdaCalculus.EMatchOption_arg", "projection_inverse_Catala.LambdaCalculus.EMatchOption_none", "projection_inverse_Catala.LambdaCalculus.EMatchOption_some", "projection_inverse_Catala.LambdaCalculus.EMatchOption_tau_some", "projection_inverse_Catala.LambdaCalculus.ESome_s", "projection_inverse_Catala.LambdaCalculus.EVar_v", "projection_inverse_Catala.LambdaCalculus.LError_err", "projection_inverse_Catala.LambdaCalculus.TArrow_tin", "projection_inverse_Catala.LambdaCalculus.TArrow_tout", "projection_inverse_Catala.LambdaCalculus.TList_elts", "projection_inverse_Catala.LambdaCalculus.TOption_a", "refinement_interpretation_Tm_refine_377a881fa421745480e4b59bb1779ae5", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_d5485f8c94130f85952cddf1019830bb", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "token_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", "typing_Catala.LambdaCalculus.empty", "typing_Catala.LambdaCalculus.extend", "typing_Catala.LambdaCalculus.typing", "typing_Catala.LambdaCalculus.typing_list", "typing_Catala.Translation.Helpers.process_exceptions_f", "typing_Tm_abs_1312e4782c558ee50ab7a5e0bfd49851", "typing_Tm_abs_683fecef0f32ab9df689545bd34ec676", "typing_tok_Catala.LambdaCalculus.ENone@tok", "typing_tok_Catala.LambdaCalculus.EmptyError@tok", "typing_tok_Catala.LambdaCalculus.TBool@tok", "typing_tok_Catala.LambdaCalculus.TUnit@tok" ], 0, "df1298f3aadddbdb4d3bb3e586a360c0" ], [ "Catala.Translation.Helpers.exceptions_head_lift_is_stepping_agnostic", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.LambdaCalculus.is_value.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.step.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.step_app.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.step_catch.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.step_fold_left.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.step_if.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.step_list.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.step_match.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.step.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.step_app.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.step_catch.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.step_fold_left.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.step_if.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.step_list.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.step_match.fuel_instrumented", "@query", "Catala.LambdaCalculus_pretyping_fabd258754d8bab26d9bc0ad1a882a83", "bool_inversion", "constructor_distinct_Catala.LambdaCalculus.Bad", "constructor_distinct_Catala.LambdaCalculus.ESome", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_FStar.Pervasives.Native.Some", "constructor_distinct_Tm_unit", "data_typing_intro_Catala.LambdaCalculus.ENone@tok", "data_typing_intro_Catala.LambdaCalculus.ESome@tok", "disc_equation_FStar.Pervasives.Native.Some", "eq2-interp", "equation_Catala.Translation.Helpers.exceptions_head_lift_", "equation_Catala.Translation.Helpers.process_exceptions_f", "equation_Catala.Translation.Helpers.step_lift_commute_non_value", "equation_Catala.Translation.Helpers.typed_l_exp", "equation_with_fuel_Catala.LambdaCalculus.is_value.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step.fuel_instrumented", "fuel_guarded_inversion_FStar.Pervasives.Native.option", "interpretation_Tm_abs_7041a26a87a3fce24dbf917ff7f2a6ff", "proj_equation_FStar.Pervasives.Native.Some_v", "projection_inverse_BoxBool_proj_0", "projection_inverse_Catala.LambdaCalculus.ESome_s", "projection_inverse_FStar.Pervasives.Native.Some_a", "projection_inverse_FStar.Pervasives.Native.Some_v", "refinement_interpretation_Tm_refine_d5485f8c94130f85952cddf1019830bb", "token_correspondence_Catala.LambdaCalculus.step.fuel_instrumented", "token_correspondence_Catala.Translation.Helpers.exceptions_head_lift_", "true_interp", "typing_Catala.LambdaCalculus.step" ], 0, "dfb16d5a0e38d3c28889619783287c64" ], [ "Catala.Translation.Helpers.exceptions_head_lift", 1, 2, 1, [ "@query", "equation_Catala.Translation.Helpers.is_stepping_agnostic_lift" ], 0, "65358c88d6fc4d6ce800f6db696619ec" ], [ "Catala.Translation.Helpers.exceptions_init_lift'", 1, 3, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.LambdaCalculus.is_value.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.typing_list.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.typing.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.typing_list.fuel_instrumented", "@query", "Catala.LambdaCalculus_interpretation_Tm_arrow_0afe855ee0dd04a9f1572a7d68b10fa7", "Catala.LambdaCalculus_interpretation_Tm_arrow_ed0c592d82dfd5a47d39e42cf9d52a55", "Catala.LambdaCalculus_pretyping_8ab521cb5d1069fb182eea898efa7c42", "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion", "constructor_distinct_Catala.LambdaCalculus.EAbs", "constructor_distinct_Catala.LambdaCalculus.EFoldLeft", "constructor_distinct_Catala.LambdaCalculus.EIf", "constructor_distinct_Catala.LambdaCalculus.EList", "constructor_distinct_Catala.LambdaCalculus.ELit", "constructor_distinct_Catala.LambdaCalculus.EMatchOption", "constructor_distinct_Catala.LambdaCalculus.EVar", "constructor_distinct_Catala.LambdaCalculus.LError", "constructor_distinct_Catala.LambdaCalculus.TArrow", "constructor_distinct_Catala.LambdaCalculus.TList", "data_typing_intro_Catala.LambdaCalculus.EAbs@tok", "data_typing_intro_Catala.LambdaCalculus.EFoldLeft@tok", "data_typing_intro_Catala.LambdaCalculus.EIf@tok", "data_typing_intro_Catala.LambdaCalculus.EList@tok", "data_typing_intro_Catala.LambdaCalculus.ELit@tok", "data_typing_intro_Catala.LambdaCalculus.EMatchOption@tok", "data_typing_intro_Catala.LambdaCalculus.EVar@tok", "data_typing_intro_Catala.LambdaCalculus.LError@tok", "data_typing_intro_Catala.LambdaCalculus.TArrow@tok", "data_typing_intro_Catala.LambdaCalculus.TList@tok", "data_typing_intro_Catala.LambdaCalculus.TOption@tok", "equality_tok_Catala.LambdaCalculus.EmptyError@tok", "equality_tok_Catala.LambdaCalculus.TBool@tok", "equality_tok_Catala.LambdaCalculus.TUnit@tok", "equation_Catala.LambdaCalculus.empty", "equation_Catala.LambdaCalculus.extend", "equation_Catala.LambdaCalculus.var", "equation_Catala.Translation.Helpers.process_exceptions_f", "equation_Catala.Translation.Helpers.typed_l_exp", "equation_FStar.FunctionalExtensionality.feq", "equation_Prims.nat", "equation_with_fuel_Catala.LambdaCalculus.is_value.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.typing.fuel_instrumented", "function_token_typing_Prims.__cache_version_number__", "int_typing", "interpretation_Tm_abs_1312e4782c558ee50ab7a5e0bfd49851", "interpretation_Tm_abs_683fecef0f32ab9df689545bd34ec676", "lemma_FStar.FunctionalExtensionality.feq_on_domain", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0", "projection_inverse_Catala.LambdaCalculus.EAbs_body", "projection_inverse_Catala.LambdaCalculus.EAbs_vty", "projection_inverse_Catala.LambdaCalculus.EFoldLeft_f", "projection_inverse_Catala.LambdaCalculus.EFoldLeft_init", "projection_inverse_Catala.LambdaCalculus.EFoldLeft_l", "projection_inverse_Catala.LambdaCalculus.EFoldLeft_tau_elt", "projection_inverse_Catala.LambdaCalculus.EFoldLeft_tau_init", "projection_inverse_Catala.LambdaCalculus.EIf_bfalse", "projection_inverse_Catala.LambdaCalculus.EIf_btrue", "projection_inverse_Catala.LambdaCalculus.EIf_test", "projection_inverse_Catala.LambdaCalculus.EList_l", "projection_inverse_Catala.LambdaCalculus.ELit_l", "projection_inverse_Catala.LambdaCalculus.EMatchOption_arg", "projection_inverse_Catala.LambdaCalculus.EMatchOption_none", "projection_inverse_Catala.LambdaCalculus.EMatchOption_some", "projection_inverse_Catala.LambdaCalculus.EMatchOption_tau_some", "projection_inverse_Catala.LambdaCalculus.EVar_v", "projection_inverse_Catala.LambdaCalculus.LError_err", "projection_inverse_Catala.LambdaCalculus.TArrow_tin", "projection_inverse_Catala.LambdaCalculus.TArrow_tout", "projection_inverse_Catala.LambdaCalculus.TList_elts", "refinement_interpretation_Tm_refine_377a881fa421745480e4b59bb1779ae5", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_d5485f8c94130f85952cddf1019830bb", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "token_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", "typing_Catala.LambdaCalculus.empty", "typing_Catala.LambdaCalculus.extend", "typing_Catala.LambdaCalculus.typing", "typing_Catala.LambdaCalculus.typing_list", "typing_Catala.Translation.Helpers.process_exceptions_f", "typing_Tm_abs_1312e4782c558ee50ab7a5e0bfd49851", "typing_Tm_abs_683fecef0f32ab9df689545bd34ec676", "typing_tok_Catala.LambdaCalculus.EmptyError@tok", "typing_tok_Catala.LambdaCalculus.TBool@tok", "typing_tok_Catala.LambdaCalculus.TUnit@tok" ], 0, "a4528e796a162796e72facc3a4db8aef" ], [ "Catala.Translation.Helpers.exceptions_init_lift_is_stepping_agnostic", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.LambdaCalculus.is_value.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.step.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.step_app.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.step_catch.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.step_fold_left.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.step_if.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.step_match.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.is_value.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.step.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.step_app.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.step_catch.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.step_fold_left.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.step_if.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.step_match.fuel_instrumented", "@query", "Catala.LambdaCalculus_pretyping_fabd258754d8bab26d9bc0ad1a882a83", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion", "constructor_distinct_Catala.LambdaCalculus.EMatchOption", "constructor_distinct_Catala.LambdaCalculus.TOption", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_FStar.Pervasives.Native.Some", "constructor_distinct_Tm_unit", "data_elim_Catala.LambdaCalculus.ESome", "data_typing_intro_Catala.LambdaCalculus.ENone@tok", "data_typing_intro_Catala.LambdaCalculus.TOption@tok", "disc_equation_FStar.Pervasives.Native.Some", "eq2-interp", "equation_Catala.LambdaCalculus.empty", "equation_Catala.Translation.Helpers.exceptions_init_lift_", "equation_Catala.Translation.Helpers.process_exceptions_f", "equation_Catala.Translation.Helpers.step_lift_commute_non_value", "equation_Catala.Translation.Helpers.typed_l_exp", "equation_with_fuel_Catala.LambdaCalculus.is_value.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.typing.fuel_instrumented", "fuel_guarded_inversion_FStar.Pervasives.Native.option", "interpretation_Tm_abs_396aa62eba4eabe2ab867a6b4ae34fc9", "proj_equation_FStar.Pervasives.Native.Some_v", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Some_a", "projection_inverse_FStar.Pervasives.Native.Some_v", "refinement_interpretation_Tm_refine_d5485f8c94130f85952cddf1019830bb", "token_correspondence_Catala.Translation.Helpers.exceptions_init_lift_", "true_interp", "typing_Catala.LambdaCalculus.empty", "typing_Catala.LambdaCalculus.step", "typing_Catala.LambdaCalculus.typing" ], 0, "12130b4ed57f71ea866b34b6388a2fe7" ], [ "Catala.Translation.Helpers.exceptions_init_lift", 1, 2, 1, [ "@query", "equation_Catala.Translation.Helpers.is_stepping_agnostic_lift" ], 0, "668a4a3f5d9fe58c7d25849b1c8229c3" ], [ "Catala.Translation.Helpers.stepping_lemma", 1, 10, 2, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.LambdaCalculus.is_value.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.step.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.subst.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", "@fuel_correspondence_Catala.Translation.Helpers.take_l_steps.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.subst.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.typing.fuel_instrumented", "@query", "Catala.LambdaCalculus_interpretation_Tm_arrow_0afe855ee0dd04a9f1572a7d68b10fa7", "Catala.LambdaCalculus_interpretation_Tm_arrow_732ef78b9bfa783d08279e5be1df507c", "Catala.LambdaCalculus_interpretation_Tm_arrow_ed0c592d82dfd5a47d39e42cf9d52a55", "Catala.LambdaCalculus_pretyping_8ab521cb5d1069fb182eea898efa7c42", "Catala.LambdaCalculus_pretyping_fabd258754d8bab26d9bc0ad1a882a83", "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion", "constructor_distinct_Catala.LambdaCalculus.EAbs", "constructor_distinct_Catala.LambdaCalculus.EApp", "constructor_distinct_Catala.LambdaCalculus.ECatchEmptyError", "constructor_distinct_Catala.LambdaCalculus.EFoldLeft", "constructor_distinct_Catala.LambdaCalculus.EIf", "constructor_distinct_Catala.LambdaCalculus.EList", "constructor_distinct_Catala.LambdaCalculus.ELit", "constructor_distinct_Catala.LambdaCalculus.EMatchOption", "constructor_distinct_Catala.LambdaCalculus.ENone", "constructor_distinct_Catala.LambdaCalculus.ESome", "constructor_distinct_Catala.LambdaCalculus.EThunk", "constructor_distinct_Catala.LambdaCalculus.EVar", "constructor_distinct_Catala.LambdaCalculus.LError", "constructor_distinct_Catala.LambdaCalculus.LUnit", "constructor_distinct_Catala.LambdaCalculus.TArrow", "constructor_distinct_Catala.LambdaCalculus.TOption", "constructor_distinct_Catala.LambdaCalculus.TUnit", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_FStar.Pervasives.Native.Some", "constructor_distinct_Tm_unit", "data_elim_Catala.LambdaCalculus.EAbs", "data_elim_Catala.LambdaCalculus.EVar", "data_typing_intro_Catala.LambdaCalculus.EAbs@tok", "data_typing_intro_Catala.LambdaCalculus.EApp@tok", "data_typing_intro_Catala.LambdaCalculus.ECatchEmptyError@tok", "data_typing_intro_Catala.LambdaCalculus.ELit@tok", "data_typing_intro_Catala.LambdaCalculus.EMatchOption@tok", "data_typing_intro_Catala.LambdaCalculus.ENone@tok", "data_typing_intro_Catala.LambdaCalculus.ESome@tok", "data_typing_intro_Catala.LambdaCalculus.EThunk@tok", "data_typing_intro_Catala.LambdaCalculus.EVar@tok", "data_typing_intro_Catala.LambdaCalculus.LError@tok", "data_typing_intro_Catala.LambdaCalculus.TArrow@tok", "data_typing_intro_Catala.LambdaCalculus.TOption@tok", "data_typing_intro_Catala.LambdaCalculus.TUnit@tok", "disc_equation_Catala.LambdaCalculus.EVar", "disc_equation_FStar.Pervasives.Native.None", "equality_tok_Catala.LambdaCalculus.ConflictError@tok", "equality_tok_Catala.LambdaCalculus.ENone@tok", "equality_tok_Catala.LambdaCalculus.LUnit@tok", "equality_tok_Catala.LambdaCalculus.TUnit@tok", "equation_Catala.LambdaCalculus.empty", "equation_Catala.LambdaCalculus.extend", "equation_Catala.LambdaCalculus.increment", "equation_Catala.LambdaCalculus.is_error", "equation_Catala.LambdaCalculus.is_renaming_prop", "equation_Catala.LambdaCalculus.var", "equation_Catala.LambdaCalculus.var_to_exp", "equation_Catala.LambdaCalculus.var_to_exp_beta", "equation_Catala.Translation.Helpers.process_exceptions_f", "equation_Catala.Translation.Helpers.typed_l_exp", "equation_FStar.FunctionalExtensionality.feq", "equation_Prims.nat", "equation_with_fuel_Catala.LambdaCalculus.is_value.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step_app.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.subst.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.subst_abs.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.typing.fuel_instrumented", "equation_with_fuel_Catala.Translation.Helpers.take_l_steps.fuel_instrumented", "fuel_token_correspondence_Catala.LambdaCalculus.subst_abs.fuel_instrumented_token", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "interpretation_Tm_abs_1312e4782c558ee50ab7a5e0bfd49851", "interpretation_Tm_abs_44e059f7416b8cb4267e0f7a598f0380", "interpretation_Tm_abs_591e432507f9fc0b2baad4ac5bad3427", "interpretation_Tm_abs_683fecef0f32ab9df689545bd34ec676", "kinding_Catala.LambdaCalculus.exp@tok", "lemma_FStar.FunctionalExtensionality.feq_on_domain", "lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction", "proj_equation_FStar.Pervasives.Native.Some_v", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Catala.LambdaCalculus.EAbs_body", "projection_inverse_Catala.LambdaCalculus.EAbs_vty", "projection_inverse_Catala.LambdaCalculus.EApp_arg", "projection_inverse_Catala.LambdaCalculus.EApp_fn", "projection_inverse_Catala.LambdaCalculus.EApp_tau_arg", "projection_inverse_Catala.LambdaCalculus.ECatchEmptyError_catch_with", "projection_inverse_Catala.LambdaCalculus.ECatchEmptyError_to_try", "projection_inverse_Catala.LambdaCalculus.ELit_l", "projection_inverse_Catala.LambdaCalculus.EMatchOption_arg", "projection_inverse_Catala.LambdaCalculus.EMatchOption_none", "projection_inverse_Catala.LambdaCalculus.EMatchOption_some", "projection_inverse_Catala.LambdaCalculus.EMatchOption_tau_some", "projection_inverse_Catala.LambdaCalculus.ESome_s", "projection_inverse_Catala.LambdaCalculus.EThunk_body", "projection_inverse_Catala.LambdaCalculus.EVar_v", "projection_inverse_Catala.LambdaCalculus.LError_err", "projection_inverse_Catala.LambdaCalculus.TArrow_tin", "projection_inverse_Catala.LambdaCalculus.TArrow_tout", "projection_inverse_Catala.LambdaCalculus.TOption_a", "projection_inverse_FStar.Pervasives.Native.Some_a", "projection_inverse_FStar.Pervasives.Native.Some_v", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_66a04fe873406083a229e09b1c833909", "refinement_interpretation_Tm_refine_8572abaf58b0908690b4c77b9bd5038b", "refinement_interpretation_Tm_refine_9d7619fada7e7cc3e29055f7763724da", "refinement_interpretation_Tm_refine_a392bfba80da306fafdb3d849a464ab4", "refinement_interpretation_Tm_refine_d5485f8c94130f85952cddf1019830bb", "refinement_interpretation_Tm_refine_d8dd43e05db2d11a4a14435baf3ab736", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "subterm_ordering_Catala.LambdaCalculus.EApp", "token_correspondence_Catala.LambdaCalculus.subst.fuel_instrumented", "token_correspondence_Catala.LambdaCalculus.subst_abs.fuel_instrumented", "token_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", "true_interp", "typing_Catala.LambdaCalculus.empty", "typing_Catala.LambdaCalculus.extend", "typing_Catala.LambdaCalculus.increment", "typing_Catala.LambdaCalculus.is_error", "typing_Catala.LambdaCalculus.is_value", "typing_Catala.LambdaCalculus.step", "typing_Catala.LambdaCalculus.typing", "typing_Catala.LambdaCalculus.var_to_exp_beta", "typing_Catala.Translation.Helpers.process_exceptions_f", "typing_Tm_abs_1312e4782c558ee50ab7a5e0bfd49851", "typing_Tm_abs_44e059f7416b8cb4267e0f7a598f0380", "typing_Tm_abs_683fecef0f32ab9df689545bd34ec676", "typing_tok_Catala.LambdaCalculus.ConflictError@tok", "typing_tok_Catala.LambdaCalculus.ENone@tok", "typing_tok_Catala.LambdaCalculus.LUnit@tok", "typing_tok_Catala.LambdaCalculus.TUnit@tok" ], 0, "87f7c608e239ce2ca96d28b468c9495a" ], [ "Catala.Translation.Helpers.stepping_lemma", 2, 10, 2, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.LambdaCalculus.is_value.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.is_value.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "@query", "bool_inversion", "constructor_distinct_FStar.Pervasives.Native.Some", "equation_Catala.LambdaCalculus.empty", "equation_Catala.LambdaCalculus.is_error", "equation_Catala.Translation.Helpers.typed_l_exp", "equation_with_fuel_Catala.LambdaCalculus.is_value.fuel_instrumented", "projection_inverse_FStar.Pervasives.Native.Some_a", "projection_inverse_FStar.Pervasives.Native.Some_v", "refinement_interpretation_Tm_refine_d5485f8c94130f85952cddf1019830bb", "refinement_interpretation_Tm_refine_d8dd43e05db2d11a4a14435baf3ab736", "typing_Catala.LambdaCalculus.empty", "typing_Catala.LambdaCalculus.is_error", "typing_Catala.LambdaCalculus.is_value", "typing_Catala.LambdaCalculus.typing" ], 0, "0f8c86cdaa61e9c3aeca800afa856db1" ], [ "Catala.Translation.Helpers.lift_multiple_l_steps_exceptions_head", 1, 7, 2, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.LambdaCalculus.is_value.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.step.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.typing_list.fuel_instrumented", "@fuel_correspondence_Catala.Translation.Helpers.take_l_steps.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.typing.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.typing_list.fuel_instrumented", "@query", "Catala.LambdaCalculus_interpretation_Tm_arrow_0afe855ee0dd04a9f1572a7d68b10fa7", "Catala.LambdaCalculus_interpretation_Tm_arrow_ed0c592d82dfd5a47d39e42cf9d52a55", "Catala.LambdaCalculus_pretyping_8ab521cb5d1069fb182eea898efa7c42", "Catala.LambdaCalculus_pretyping_fabd258754d8bab26d9bc0ad1a882a83", "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion", "constructor_distinct_Catala.LambdaCalculus.EAbs", "constructor_distinct_Catala.LambdaCalculus.EApp", "constructor_distinct_Catala.LambdaCalculus.ECatchEmptyError", "constructor_distinct_Catala.LambdaCalculus.EFoldLeft", "constructor_distinct_Catala.LambdaCalculus.EIf", "constructor_distinct_Catala.LambdaCalculus.EList", "constructor_distinct_Catala.LambdaCalculus.ELit", "constructor_distinct_Catala.LambdaCalculus.EMatchOption", "constructor_distinct_Catala.LambdaCalculus.ENone", "constructor_distinct_Catala.LambdaCalculus.ESome", "constructor_distinct_Catala.LambdaCalculus.EThunk", "constructor_distinct_Catala.LambdaCalculus.EVar", "constructor_distinct_Catala.LambdaCalculus.LError", "constructor_distinct_Catala.LambdaCalculus.LUnit", "constructor_distinct_Catala.LambdaCalculus.TArrow", "constructor_distinct_Catala.LambdaCalculus.TBool", "constructor_distinct_Catala.LambdaCalculus.TList", "constructor_distinct_Catala.LambdaCalculus.TOption", "constructor_distinct_Catala.LambdaCalculus.TUnit", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_FStar.Pervasives.Native.Some", "constructor_distinct_Prims.Cons", "constructor_distinct_Tm_unit", "data_elim_Catala.LambdaCalculus.EAbs", "data_elim_Catala.LambdaCalculus.EApp", "data_elim_Catala.LambdaCalculus.ECatchEmptyError", "data_elim_Catala.LambdaCalculus.ELit", "data_elim_Catala.LambdaCalculus.EMatchOption", "data_elim_Catala.LambdaCalculus.ESome", "data_elim_Catala.LambdaCalculus.EVar", "data_elim_FStar.Pervasives.Native.Some", "data_typing_intro_Catala.LambdaCalculus.EAbs@tok", "data_typing_intro_Catala.LambdaCalculus.EApp@tok", "data_typing_intro_Catala.LambdaCalculus.ECatchEmptyError@tok", "data_typing_intro_Catala.LambdaCalculus.EFoldLeft@tok", "data_typing_intro_Catala.LambdaCalculus.EList@tok", "data_typing_intro_Catala.LambdaCalculus.ELit@tok", "data_typing_intro_Catala.LambdaCalculus.EMatchOption@tok", "data_typing_intro_Catala.LambdaCalculus.ENone@tok", "data_typing_intro_Catala.LambdaCalculus.ESome@tok", "data_typing_intro_Catala.LambdaCalculus.EThunk@tok", "data_typing_intro_Catala.LambdaCalculus.TArrow@tok", "data_typing_intro_Catala.LambdaCalculus.TList@tok", "data_typing_intro_Catala.LambdaCalculus.TOption@tok", "data_typing_intro_Catala.LambdaCalculus.TUnit@tok", "data_typing_intro_Prims.Cons@tok", "disc_equation_FStar.Pervasives.Native.None", "disc_equation_FStar.Pervasives.Native.Some", "equality_tok_Catala.LambdaCalculus.ConflictError@tok", "equality_tok_Catala.LambdaCalculus.ENone@tok", "equality_tok_Catala.LambdaCalculus.EmptyError@tok", "equality_tok_Catala.LambdaCalculus.LUnit@tok", "equality_tok_Catala.LambdaCalculus.TBool@tok", "equality_tok_Catala.LambdaCalculus.TUnit@tok", "equation_Catala.LambdaCalculus.empty", "equation_Catala.LambdaCalculus.extend", "equation_Catala.LambdaCalculus.var", "equation_Catala.Translation.Helpers.build_default_translation", "equation_Catala.Translation.Helpers.exceptions_head_lift", "equation_Catala.Translation.Helpers.exceptions_head_lift_", "equation_Catala.Translation.Helpers.exceptions_init_lift", "equation_Catala.Translation.Helpers.exceptions_init_lift_", "equation_Catala.Translation.Helpers.process_exceptions_f", "equation_Catala.Translation.Helpers.typed_l_exp", "equation_FStar.FunctionalExtensionality.feq", "equation_Prims.nat", "equation_with_fuel_Catala.LambdaCalculus.is_value.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step_app.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step_catch.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step_fold_left.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step_match.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.typing.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.typing_list.fuel_instrumented", "equation_with_fuel_Catala.Translation.Helpers.take_l_steps.fuel_instrumented", "fuel_guarded_inversion_Catala.LambdaCalculus.lit", "fuel_guarded_inversion_FStar.Pervasives.Native.option", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "interpretation_Tm_abs_1312e4782c558ee50ab7a5e0bfd49851", "interpretation_Tm_abs_396aa62eba4eabe2ab867a6b4ae34fc9", "interpretation_Tm_abs_44e059f7416b8cb4267e0f7a598f0380", "interpretation_Tm_abs_683fecef0f32ab9df689545bd34ec676", "interpretation_Tm_abs_7041a26a87a3fce24dbf917ff7f2a6ff", "kinding_Catala.LambdaCalculus.exp@tok", "lemma_FStar.FunctionalExtensionality.feq_on_domain", "lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction", "proj_equation_FStar.Pervasives.Native.Some_v", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Catala.LambdaCalculus.EAbs_body", "projection_inverse_Catala.LambdaCalculus.EAbs_vty", "projection_inverse_Catala.LambdaCalculus.EApp_arg", "projection_inverse_Catala.LambdaCalculus.EApp_fn", "projection_inverse_Catala.LambdaCalculus.EApp_tau_arg", "projection_inverse_Catala.LambdaCalculus.ECatchEmptyError_catch_with", "projection_inverse_Catala.LambdaCalculus.ECatchEmptyError_to_try", "projection_inverse_Catala.LambdaCalculus.EFoldLeft_f", "projection_inverse_Catala.LambdaCalculus.EFoldLeft_init", "projection_inverse_Catala.LambdaCalculus.EFoldLeft_l", "projection_inverse_Catala.LambdaCalculus.EFoldLeft_tau_elt", "projection_inverse_Catala.LambdaCalculus.EFoldLeft_tau_init", "projection_inverse_Catala.LambdaCalculus.EList_l", "projection_inverse_Catala.LambdaCalculus.ELit_l", "projection_inverse_Catala.LambdaCalculus.EMatchOption_arg", "projection_inverse_Catala.LambdaCalculus.EMatchOption_none", "projection_inverse_Catala.LambdaCalculus.EMatchOption_some", "projection_inverse_Catala.LambdaCalculus.EMatchOption_tau_some", "projection_inverse_Catala.LambdaCalculus.ESome_s", "projection_inverse_Catala.LambdaCalculus.EThunk_body", "projection_inverse_Catala.LambdaCalculus.EVar_v", "projection_inverse_Catala.LambdaCalculus.LError_err", "projection_inverse_Catala.LambdaCalculus.TArrow_tin", "projection_inverse_Catala.LambdaCalculus.TArrow_tout", "projection_inverse_Catala.LambdaCalculus.TList_elts", "projection_inverse_Catala.LambdaCalculus.TOption_a", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "projection_inverse_FStar.Pervasives.Native.Some_a", "projection_inverse_FStar.Pervasives.Native.Some_v", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "refinement_interpretation_Tm_refine_0e20cbcd7c3d88df2290aa242d006288", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8572abaf58b0908690b4c77b9bd5038b", "refinement_interpretation_Tm_refine_9d7619fada7e7cc3e29055f7763724da", "refinement_interpretation_Tm_refine_d5485f8c94130f85952cddf1019830bb", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "subterm_ordering_Catala.LambdaCalculus.EApp", "subterm_ordering_Catala.LambdaCalculus.ECatchEmptyError", "subterm_ordering_Catala.LambdaCalculus.EFoldLeft", "subterm_ordering_Catala.LambdaCalculus.EMatchOption", "token_correspondence_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "token_correspondence_Catala.LambdaCalculus.step.fuel_instrumented", "token_correspondence_Catala.LambdaCalculus.step_app.fuel_instrumented", "token_correspondence_Catala.LambdaCalculus.step_catch.fuel_instrumented", "token_correspondence_Catala.LambdaCalculus.step_fold_left.fuel_instrumented", "token_correspondence_Catala.LambdaCalculus.step_match.fuel_instrumented", "token_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", "token_correspondence_Catala.LambdaCalculus.typing_list.fuel_instrumented", "token_correspondence_Catala.Translation.Helpers.exceptions_head_lift", "token_correspondence_Catala.Translation.Helpers.exceptions_init_lift", "typing_Catala.LambdaCalculus.empty", "typing_Catala.LambdaCalculus.extend", "typing_Catala.LambdaCalculus.is_value", "typing_Catala.LambdaCalculus.step", "typing_Catala.LambdaCalculus.typing", "typing_Catala.LambdaCalculus.typing_list", "typing_Catala.Translation.Helpers.build_default_translation", "typing_Catala.Translation.Helpers.process_exceptions_f", "typing_Tm_abs_1312e4782c558ee50ab7a5e0bfd49851", "typing_Tm_abs_44e059f7416b8cb4267e0f7a598f0380", "typing_Tm_abs_683fecef0f32ab9df689545bd34ec676", "typing_tok_Catala.LambdaCalculus.ENone@tok", "typing_tok_Catala.LambdaCalculus.LUnit@tok", "typing_tok_Catala.LambdaCalculus.TUnit@tok" ], 0, "90375b98f78397c3f602a928ae1297a7" ], [ "Catala.Translation.Helpers.process_exceptions_applied", 1, 7, 2, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.typing.fuel_instrumented", "@query", "Catala.LambdaCalculus_pretyping_8ab521cb5d1069fb182eea898efa7c42", "Catala.LambdaCalculus_pretyping_fabd258754d8bab26d9bc0ad1a882a83", "bool_inversion", "constructor_distinct_Catala.LambdaCalculus.EAbs", "constructor_distinct_Catala.LambdaCalculus.EApp", "constructor_distinct_Catala.LambdaCalculus.EThunk", "constructor_distinct_Catala.LambdaCalculus.TArrow", "constructor_distinct_Catala.LambdaCalculus.TUnit", "data_elim_Catala.LambdaCalculus.EAbs", "data_typing_intro_Catala.LambdaCalculus.EApp@tok", "data_typing_intro_Catala.LambdaCalculus.ENone@tok", "data_typing_intro_Catala.LambdaCalculus.EThunk@tok", "data_typing_intro_Catala.LambdaCalculus.TArrow@tok", "data_typing_intro_Catala.LambdaCalculus.TOption@tok", "data_typing_intro_Catala.LambdaCalculus.TUnit@tok", "equality_tok_Catala.LambdaCalculus.TUnit@tok", "equation_Catala.LambdaCalculus.empty", "equation_Catala.Translation.Helpers.process_exceptions_f", "equation_Catala.Translation.Helpers.typed_l_exp", "equation_with_fuel_Catala.LambdaCalculus.typing.fuel_instrumented", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0", "projection_inverse_Catala.LambdaCalculus.EAbs_body", "projection_inverse_Catala.LambdaCalculus.EAbs_vty", "projection_inverse_Catala.LambdaCalculus.EApp_arg", "projection_inverse_Catala.LambdaCalculus.EApp_fn", "projection_inverse_Catala.LambdaCalculus.EApp_tau_arg", "projection_inverse_Catala.LambdaCalculus.EThunk_body", "projection_inverse_Catala.LambdaCalculus.TArrow_tin", "projection_inverse_Catala.LambdaCalculus.TArrow_tout", "refinement_interpretation_Tm_refine_d5485f8c94130f85952cddf1019830bb", "token_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", "typing_Catala.LambdaCalculus.empty", "typing_Catala.LambdaCalculus.extend", "typing_Catala.LambdaCalculus.typing", "typing_Catala.Translation.Helpers.process_exceptions_f", "typing_tok_Catala.LambdaCalculus.TUnit@tok" ], 0, "1351745ed59b26a0eb38fdd007f6de23" ], [ "Catala.Translation.Helpers.process_exceptions_applied_stepped", 1, 7, 2, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.typing.fuel_instrumented", "@query", "Catala.LambdaCalculus_interpretation_Tm_arrow_0afe855ee0dd04a9f1572a7d68b10fa7", "Catala.LambdaCalculus_interpretation_Tm_arrow_ed0c592d82dfd5a47d39e42cf9d52a55", "Catala.LambdaCalculus_pretyping_8ab521cb5d1069fb182eea898efa7c42", "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion", "constructor_distinct_Catala.LambdaCalculus.EAbs", "constructor_distinct_Catala.LambdaCalculus.EApp", "constructor_distinct_Catala.LambdaCalculus.ECatchEmptyError", "constructor_distinct_Catala.LambdaCalculus.ELit", "constructor_distinct_Catala.LambdaCalculus.EMatchOption", "constructor_distinct_Catala.LambdaCalculus.ENone", "constructor_distinct_Catala.LambdaCalculus.ESome", "constructor_distinct_Catala.LambdaCalculus.EVar", "constructor_distinct_Catala.LambdaCalculus.LError", "constructor_distinct_Catala.LambdaCalculus.TArrow", "constructor_distinct_Catala.LambdaCalculus.TOption", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_FStar.Pervasives.Native.Some", "data_elim_Catala.LambdaCalculus.EVar", "data_typing_intro_Catala.LambdaCalculus.EAbs@tok", "data_typing_intro_Catala.LambdaCalculus.EApp@tok", "data_typing_intro_Catala.LambdaCalculus.ECatchEmptyError@tok", "data_typing_intro_Catala.LambdaCalculus.ELit@tok", "data_typing_intro_Catala.LambdaCalculus.EMatchOption@tok", "data_typing_intro_Catala.LambdaCalculus.ESome@tok", "data_typing_intro_Catala.LambdaCalculus.EVar@tok", "data_typing_intro_Catala.LambdaCalculus.LError@tok", "data_typing_intro_Catala.LambdaCalculus.TArrow@tok", "data_typing_intro_Catala.LambdaCalculus.TOption@tok", "data_typing_intro_Catala.LambdaCalculus.TUnit@tok", "equality_tok_Catala.LambdaCalculus.ConflictError@tok", "equality_tok_Catala.LambdaCalculus.ENone@tok", "equation_Catala.LambdaCalculus.empty", "equation_Catala.LambdaCalculus.extend", "equation_Catala.LambdaCalculus.var", "equation_Catala.Translation.Helpers.typed_l_exp", "equation_FStar.FunctionalExtensionality.feq", "equation_Prims.nat", "equation_with_fuel_Catala.LambdaCalculus.typing.fuel_instrumented", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "interpretation_Tm_abs_1312e4782c558ee50ab7a5e0bfd49851", "interpretation_Tm_abs_44e059f7416b8cb4267e0f7a598f0380", "interpretation_Tm_abs_683fecef0f32ab9df689545bd34ec676", "lemma_FStar.FunctionalExtensionality.feq_on_domain", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Catala.LambdaCalculus.EAbs_body", "projection_inverse_Catala.LambdaCalculus.EAbs_vty", "projection_inverse_Catala.LambdaCalculus.EApp_arg", "projection_inverse_Catala.LambdaCalculus.EApp_fn", "projection_inverse_Catala.LambdaCalculus.EApp_tau_arg", "projection_inverse_Catala.LambdaCalculus.ECatchEmptyError_catch_with", "projection_inverse_Catala.LambdaCalculus.ECatchEmptyError_to_try", "projection_inverse_Catala.LambdaCalculus.ELit_l", "projection_inverse_Catala.LambdaCalculus.EMatchOption_arg", "projection_inverse_Catala.LambdaCalculus.EMatchOption_none", "projection_inverse_Catala.LambdaCalculus.EMatchOption_some", "projection_inverse_Catala.LambdaCalculus.EMatchOption_tau_some", "projection_inverse_Catala.LambdaCalculus.ESome_s", "projection_inverse_Catala.LambdaCalculus.EVar_v", "projection_inverse_Catala.LambdaCalculus.LError_err", "projection_inverse_Catala.LambdaCalculus.TArrow_tin", "projection_inverse_Catala.LambdaCalculus.TArrow_tout", "projection_inverse_Catala.LambdaCalculus.TOption_a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_d5485f8c94130f85952cddf1019830bb", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "token_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", "typing_Catala.LambdaCalculus.empty", "typing_Catala.LambdaCalculus.extend", "typing_Catala.LambdaCalculus.typing", "typing_Tm_abs_1312e4782c558ee50ab7a5e0bfd49851", "typing_Tm_abs_44e059f7416b8cb4267e0f7a598f0380", "typing_Tm_abs_683fecef0f32ab9df689545bd34ec676", "typing_tok_Catala.LambdaCalculus.ConflictError@tok", "typing_tok_Catala.LambdaCalculus.ENone@tok" ], 0, "81ec8c9b094595193c0d4fa9c9e0f67e" ], [ "Catala.Translation.Helpers.process_exceptions_applied_stepping", 1, 9, 2, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.LambdaCalculus.is_value.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.step.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.subst.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", "@fuel_correspondence_Catala.Translation.Helpers.take_l_steps.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.is_value.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.subst.fuel_instrumented", "@query", "Catala.LambdaCalculus_interpretation_Tm_arrow_732ef78b9bfa783d08279e5be1df507c", "Catala.LambdaCalculus_pretyping_8ab521cb5d1069fb182eea898efa7c42", "Catala.LambdaCalculus_pretyping_fabd258754d8bab26d9bc0ad1a882a83", "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion", "constructor_distinct_Catala.LambdaCalculus.EAbs", "constructor_distinct_Catala.LambdaCalculus.EApp", "constructor_distinct_Catala.LambdaCalculus.ECatchEmptyError", "constructor_distinct_Catala.LambdaCalculus.ELit", "constructor_distinct_Catala.LambdaCalculus.EMatchOption", "constructor_distinct_Catala.LambdaCalculus.ENone", "constructor_distinct_Catala.LambdaCalculus.ESome", "constructor_distinct_Catala.LambdaCalculus.EThunk", "constructor_distinct_Catala.LambdaCalculus.EVar", "constructor_distinct_Catala.LambdaCalculus.LUnit", "constructor_distinct_Catala.LambdaCalculus.TBool", "constructor_distinct_Catala.LambdaCalculus.TOption", "constructor_distinct_Catala.LambdaCalculus.TUnit", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_FStar.Pervasives.Native.Some", "constructor_distinct_Tm_unit", "data_elim_Catala.LambdaCalculus.EApp", "data_elim_Catala.LambdaCalculus.ELit", "data_elim_Catala.LambdaCalculus.ESome", "data_elim_FStar.Pervasives.Native.Some", "data_typing_intro_Catala.LambdaCalculus.EAbs@tok", "data_typing_intro_Catala.LambdaCalculus.EApp@tok", "data_typing_intro_Catala.LambdaCalculus.ECatchEmptyError@tok", "data_typing_intro_Catala.LambdaCalculus.ELit@tok", "data_typing_intro_Catala.LambdaCalculus.EMatchOption@tok", "data_typing_intro_Catala.LambdaCalculus.ENone@tok", "data_typing_intro_Catala.LambdaCalculus.ESome@tok", "data_typing_intro_Catala.LambdaCalculus.EThunk@tok", "data_typing_intro_Catala.LambdaCalculus.EVar@tok", "data_typing_intro_Catala.LambdaCalculus.LError@tok", "data_typing_intro_Catala.LambdaCalculus.TArrow@tok", "data_typing_intro_Catala.LambdaCalculus.TOption@tok", "data_typing_intro_Catala.LambdaCalculus.TUnit@tok", "disc_equation_Catala.LambdaCalculus.EVar", "disc_equation_FStar.Pervasives.Native.None", "disc_equation_FStar.Pervasives.Native.Some", "equality_tok_Catala.LambdaCalculus.ConflictError@tok", "equality_tok_Catala.LambdaCalculus.ENone@tok", "equality_tok_Catala.LambdaCalculus.LUnit@tok", "equality_tok_Catala.LambdaCalculus.TBool@tok", "equality_tok_Catala.LambdaCalculus.TUnit@tok", "equation_Catala.LambdaCalculus.empty", "equation_Catala.LambdaCalculus.increment", "equation_Catala.LambdaCalculus.is_error", "equation_Catala.LambdaCalculus.var", "equation_Catala.LambdaCalculus.var_to_exp", "equation_Catala.LambdaCalculus.var_to_exp_beta", "equation_Catala.Translation.Helpers.process_exceptions_applied", "equation_Catala.Translation.Helpers.process_exceptions_applied_stepped", "equation_Catala.Translation.Helpers.process_exceptions_f", "equation_Catala.Translation.Helpers.typed_l_exp", "equation_Prims.nat", "equation_with_fuel_Catala.LambdaCalculus.is_value.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step_app.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step_catch.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.subst.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.subst_abs.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.typing.fuel_instrumented", "equation_with_fuel_Catala.Translation.Helpers.take_l_steps.fuel_instrumented", "fuel_guarded_inversion_Catala.LambdaCalculus.lit", "fuel_guarded_inversion_FStar.Pervasives.Native.option", "fuel_token_correspondence_Catala.LambdaCalculus.subst_abs.fuel_instrumented_token", "function_token_typing_Prims.__cache_version_number__", "int_typing", "interpretation_Tm_abs_591e432507f9fc0b2baad4ac5bad3427", "kinding_Catala.LambdaCalculus.exp@tok", "lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_Addition", "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction", "proj_equation_FStar.Pervasives.Native.Some_v", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Catala.LambdaCalculus.EAbs_body", "projection_inverse_Catala.LambdaCalculus.EAbs_vty", "projection_inverse_Catala.LambdaCalculus.EApp_arg", "projection_inverse_Catala.LambdaCalculus.EApp_fn", "projection_inverse_Catala.LambdaCalculus.EApp_tau_arg", "projection_inverse_Catala.LambdaCalculus.ECatchEmptyError_catch_with", "projection_inverse_Catala.LambdaCalculus.ECatchEmptyError_to_try", "projection_inverse_Catala.LambdaCalculus.ELit_l", "projection_inverse_Catala.LambdaCalculus.EMatchOption_arg", "projection_inverse_Catala.LambdaCalculus.EMatchOption_none", "projection_inverse_Catala.LambdaCalculus.EMatchOption_some", "projection_inverse_Catala.LambdaCalculus.EMatchOption_tau_some", "projection_inverse_Catala.LambdaCalculus.ESome_s", "projection_inverse_Catala.LambdaCalculus.EThunk_body", "projection_inverse_Catala.LambdaCalculus.EVar_v", "projection_inverse_FStar.Pervasives.Native.Some_a", "projection_inverse_FStar.Pervasives.Native.Some_v", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_66a04fe873406083a229e09b1c833909", "refinement_interpretation_Tm_refine_8572abaf58b0908690b4c77b9bd5038b", "refinement_interpretation_Tm_refine_9d7619fada7e7cc3e29055f7763724da", "refinement_interpretation_Tm_refine_a392bfba80da306fafdb3d849a464ab4", "refinement_interpretation_Tm_refine_d5485f8c94130f85952cddf1019830bb", "refinement_interpretation_Tm_refine_d8dd43e05db2d11a4a14435baf3ab736", "subterm_ordering_Catala.LambdaCalculus.EApp", "subterm_ordering_Catala.LambdaCalculus.ECatchEmptyError", "token_correspondence_Catala.LambdaCalculus.step.fuel_instrumented", "token_correspondence_Catala.LambdaCalculus.subst.fuel_instrumented", "token_correspondence_Catala.LambdaCalculus.subst_abs.fuel_instrumented", "typing_Catala.LambdaCalculus.empty", "typing_Catala.LambdaCalculus.increment", "typing_Catala.LambdaCalculus.is_error", "typing_Catala.LambdaCalculus.is_value", "typing_Catala.LambdaCalculus.step", "typing_Catala.LambdaCalculus.subst", "typing_Catala.LambdaCalculus.typing", "typing_Catala.LambdaCalculus.var_to_exp_beta", "typing_Catala.Translation.Helpers.process_exceptions_applied", "typing_Catala.Translation.Helpers.process_exceptions_applied_stepped", "typing_Catala.Translation.Helpers.process_exceptions_f", "typing_Tm_abs_591e432507f9fc0b2baad4ac5bad3427", "typing_tok_Catala.LambdaCalculus.ConflictError@tok", "typing_tok_Catala.LambdaCalculus.ENone@tok", "typing_tok_Catala.LambdaCalculus.LUnit@tok", "typing_tok_Catala.LambdaCalculus.TUnit@tok" ], 0, "a998c17c4c0d368c49d68724a81a066d" ], [ "Catala.Translation.Helpers.exceptions_head_lift_steps_to_error", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.LambdaCalculus.is_value.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.step.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", "@fuel_correspondence_Catala.Translation.Helpers.take_l_steps.fuel_instrumented", "@query", "Catala.LambdaCalculus_pretyping_fabd258754d8bab26d9bc0ad1a882a83", "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion", "bool_typing", "constructor_distinct_Catala.LambdaCalculus.ELit", "constructor_distinct_Catala.LambdaCalculus.EMatchOption", "constructor_distinct_Catala.LambdaCalculus.LError", "constructor_distinct_FStar.Pervasives.Native.Some", "data_elim_Catala.LambdaCalculus.EMatchOption", "data_typing_intro_Catala.LambdaCalculus.ELit@tok", "data_typing_intro_Catala.LambdaCalculus.EMatchOption@tok", "data_typing_intro_Catala.LambdaCalculus.ENone@tok", "data_typing_intro_Catala.LambdaCalculus.LError@tok", "data_typing_intro_Catala.LambdaCalculus.TOption@tok", "disc_equation_FStar.Pervasives.Native.Some", "equality_tok_Catala.LambdaCalculus.ConflictError@tok", "equation_Catala.LambdaCalculus.empty", "equation_Catala.Translation.Helpers.exceptions_head_lift", "equation_Catala.Translation.Helpers.exceptions_head_lift_", "equation_Catala.Translation.Helpers.exceptions_init_lift", "equation_Catala.Translation.Helpers.exceptions_init_lift_", "equation_Catala.Translation.Helpers.not_l_value", "equation_Catala.Translation.Helpers.typed_l_exp", "equation_Prims.nat", "equation_with_fuel_Catala.LambdaCalculus.is_value.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step_match.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.typing.fuel_instrumented", "equation_with_fuel_Catala.Translation.Helpers.take_l_steps.fuel_instrumented", "function_token_typing_Prims.__cache_version_number__", "int_typing", "interpretation_Tm_abs_396aa62eba4eabe2ab867a6b4ae34fc9", "interpretation_Tm_abs_7041a26a87a3fce24dbf917ff7f2a6ff", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction", "proj_equation_FStar.Pervasives.Native.Some_v", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Catala.LambdaCalculus.ELit_l", "projection_inverse_Catala.LambdaCalculus.EMatchOption_arg", "projection_inverse_Catala.LambdaCalculus.EMatchOption_none", "projection_inverse_Catala.LambdaCalculus.EMatchOption_some", "projection_inverse_Catala.LambdaCalculus.EMatchOption_tau_some", "projection_inverse_Catala.LambdaCalculus.LError_err", "projection_inverse_FStar.Pervasives.Native.Some_a", "projection_inverse_FStar.Pervasives.Native.Some_v", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8572abaf58b0908690b4c77b9bd5038b", "refinement_interpretation_Tm_refine_cb93ec9919d1810ec52a555a1c229683", "refinement_interpretation_Tm_refine_d5485f8c94130f85952cddf1019830bb", "refinement_interpretation_Tm_refine_e1e5cfe7267eb04a8960036ae88380cb", "subterm_ordering_Catala.LambdaCalculus.EMatchOption", "token_correspondence_Catala.LambdaCalculus.is_value.fuel_instrumented", "token_correspondence_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "token_correspondence_Catala.Translation.Helpers.exceptions_head_lift", "token_correspondence_Catala.Translation.Helpers.exceptions_init_lift", "true_interp", "typing_Catala.LambdaCalculus.empty", "typing_Catala.LambdaCalculus.typing", "typing_tok_Catala.LambdaCalculus.ConflictError@tok" ], 0, "0b5e2044806ac6b3e9099ca056be806a" ], [ "Catala.Translation.Helpers.exceptions_head_lift_steps_to_error", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.LambdaCalculus.is_value.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.is_value.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "@query", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion", "constructor_distinct_FStar.Pervasives.Native.Some", "equation_Catala.Translation.Helpers.not_l_value", "equation_with_fuel_Catala.LambdaCalculus.is_value.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "fuel_guarded_inversion_Prims.list", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "projection_inverse_FStar.Pervasives.Native.Some_a", "projection_inverse_FStar.Pervasives.Native.Some_v", "refinement_interpretation_Tm_refine_0dee8cb03258a67c2f7ec66427696212", "refinement_interpretation_Tm_refine_cb93ec9919d1810ec52a555a1c229683", "refinement_interpretation_Tm_refine_e1e5cfe7267eb04a8960036ae88380cb", "typing_Catala.LambdaCalculus.is_value", "typing_Catala.LambdaCalculus.is_value_list" ], 0, "bd9092a179ef07e37a2a90cc2ba80e77" ], [ "Catala.Translation.Helpers.exception_init_lift_conflict_error", 1, 4, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.LambdaCalculus.is_value.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.step.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", "@fuel_correspondence_Catala.Translation.Helpers.take_l_steps.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "@query", "Catala.LambdaCalculus_pretyping_8ab521cb5d1069fb182eea898efa7c42", "Catala.LambdaCalculus_pretyping_fabd258754d8bab26d9bc0ad1a882a83", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion", "constructor_distinct_Catala.LambdaCalculus.EAbs", "constructor_distinct_Catala.LambdaCalculus.EFoldLeft", "constructor_distinct_Catala.LambdaCalculus.EList", "constructor_distinct_Catala.LambdaCalculus.ELit", "constructor_distinct_Catala.LambdaCalculus.EMatchOption", "constructor_distinct_Catala.LambdaCalculus.LError", "constructor_distinct_FStar.Pervasives.Native.Some", "data_elim_Catala.LambdaCalculus.EMatchOption", "data_typing_intro_Catala.LambdaCalculus.EList@tok", "data_typing_intro_Catala.LambdaCalculus.ELit@tok", "data_typing_intro_Catala.LambdaCalculus.EMatchOption@tok", "data_typing_intro_Catala.LambdaCalculus.ENone@tok", "data_typing_intro_Catala.LambdaCalculus.LError@tok", "data_typing_intro_Catala.LambdaCalculus.TArrow@tok", "data_typing_intro_Catala.LambdaCalculus.TOption@tok", "data_typing_intro_Catala.LambdaCalculus.TUnit@tok", "disc_equation_FStar.Pervasives.Native.None", "disc_equation_FStar.Pervasives.Native.Some", "equality_tok_Catala.LambdaCalculus.ConflictError@tok", "equality_tok_Catala.LambdaCalculus.TUnit@tok", "equation_Catala.LambdaCalculus.empty", "equation_Catala.Translation.Helpers.exceptions_init_lift", "equation_Catala.Translation.Helpers.exceptions_init_lift_", "equation_Catala.Translation.Helpers.not_l_value", "equation_Catala.Translation.Helpers.process_exceptions_f", "equation_Catala.Translation.Helpers.typed_l_exp", "equation_Prims.nat", "equation_with_fuel_Catala.LambdaCalculus.is_value.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step_fold_left.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step_match.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.typing.fuel_instrumented", "equation_with_fuel_Catala.Translation.Helpers.take_l_steps.fuel_instrumented", "function_token_typing_Prims.__cache_version_number__", "int_typing", "interpretation_Tm_abs_396aa62eba4eabe2ab867a6b4ae34fc9", "kinding_Catala.LambdaCalculus.exp@tok", "lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction", "proj_equation_FStar.Pervasives.Native.Some_v", "projection_inverse_BoxInt_proj_0", "projection_inverse_Catala.LambdaCalculus.EAbs_body", "projection_inverse_Catala.LambdaCalculus.EAbs_vty", "projection_inverse_Catala.LambdaCalculus.EFoldLeft_f", "projection_inverse_Catala.LambdaCalculus.EFoldLeft_init", "projection_inverse_Catala.LambdaCalculus.EFoldLeft_l", "projection_inverse_Catala.LambdaCalculus.EFoldLeft_tau_elt", "projection_inverse_Catala.LambdaCalculus.EFoldLeft_tau_init", "projection_inverse_Catala.LambdaCalculus.EList_l", "projection_inverse_Catala.LambdaCalculus.ELit_l", "projection_inverse_Catala.LambdaCalculus.EMatchOption_arg", "projection_inverse_Catala.LambdaCalculus.EMatchOption_none", "projection_inverse_Catala.LambdaCalculus.EMatchOption_some", "projection_inverse_Catala.LambdaCalculus.EMatchOption_tau_some", "projection_inverse_Catala.LambdaCalculus.LError_err", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "projection_inverse_FStar.Pervasives.Native.Some_a", "projection_inverse_FStar.Pervasives.Native.Some_v", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8572abaf58b0908690b4c77b9bd5038b", "refinement_interpretation_Tm_refine_cb93ec9919d1810ec52a555a1c229683", "refinement_interpretation_Tm_refine_d5485f8c94130f85952cddf1019830bb", "refinement_interpretation_Tm_refine_e1e5cfe7267eb04a8960036ae88380cb", "subterm_ordering_Catala.LambdaCalculus.EFoldLeft", "subterm_ordering_Catala.LambdaCalculus.EMatchOption", "token_correspondence_Catala.LambdaCalculus.is_value.fuel_instrumented", "token_correspondence_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "token_correspondence_Catala.LambdaCalculus.step_match.fuel_instrumented", "token_correspondence_Catala.Translation.Helpers.exceptions_init_lift", "typing_Catala.LambdaCalculus.empty", "typing_Catala.Translation.Helpers.process_exceptions_f", "typing_tok_Catala.LambdaCalculus.ConflictError@tok", "typing_tok_Catala.LambdaCalculus.TUnit@tok" ], 0, "64ddb595dcc317a512102e50ae2df213" ], [ "Catala.Translation.Helpers.is_option_value", 1, 7, 2, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.LambdaCalculus.is_value.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", "@query", "Catala.LambdaCalculus_pretyping_8ab521cb5d1069fb182eea898efa7c42", "bool_inversion", "constructor_distinct_Catala.LambdaCalculus.TBool", "constructor_distinct_Catala.LambdaCalculus.TOption", "constructor_distinct_Catala.LambdaCalculus.TUnit", "data_elim_Catala.LambdaCalculus.ELit", "data_typing_intro_Catala.LambdaCalculus.TOption@tok", "data_typing_intro_Catala.LambdaCalculus.TUnit@tok", "equality_tok_Catala.LambdaCalculus.TBool@tok", "equality_tok_Catala.LambdaCalculus.TUnit@tok", "equation_with_fuel_Catala.LambdaCalculus.is_value.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.typing.fuel_instrumented", "fuel_guarded_inversion_Catala.LambdaCalculus.lit", "primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0", "typing_Catala.LambdaCalculus.is_value", "typing_Catala.LambdaCalculus.typing" ], 0, "836f2939f9ea1c7599ba6e3347bfa9b5" ], [ "Catala.Translation.Helpers.step_exceptions_head_value_error", 1, 8, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.LambdaCalculus.is_value.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.step.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.subst.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", "@fuel_correspondence_Catala.Translation.Helpers.take_l_steps.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.is_value.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.subst.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.typing.fuel_instrumented", "@query", "Catala.LambdaCalculus_interpretation_Tm_arrow_0afe855ee0dd04a9f1572a7d68b10fa7", "Catala.LambdaCalculus_interpretation_Tm_arrow_732ef78b9bfa783d08279e5be1df507c", "Catala.LambdaCalculus_interpretation_Tm_arrow_ed0c592d82dfd5a47d39e42cf9d52a55", "Catala.LambdaCalculus_pretyping_8ab521cb5d1069fb182eea898efa7c42", "Catala.LambdaCalculus_pretyping_fabd258754d8bab26d9bc0ad1a882a83", "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Prims_pretyping_ae567c2fb75be05905677af440075565", "assumption_Catala.LambdaCalculus.exp__uu___haseq", "bool_inversion", "constructor_distinct_Catala.LambdaCalculus.ConflictError", "constructor_distinct_Catala.LambdaCalculus.EAbs", "constructor_distinct_Catala.LambdaCalculus.EApp", "constructor_distinct_Catala.LambdaCalculus.ECatchEmptyError", "constructor_distinct_Catala.LambdaCalculus.ELit", "constructor_distinct_Catala.LambdaCalculus.EMatchOption", "constructor_distinct_Catala.LambdaCalculus.ENone", "constructor_distinct_Catala.LambdaCalculus.ESome", "constructor_distinct_Catala.LambdaCalculus.EVar", "constructor_distinct_Catala.LambdaCalculus.EmptyError", "constructor_distinct_Catala.LambdaCalculus.LError", "constructor_distinct_Catala.LambdaCalculus.TArrow", "constructor_distinct_Catala.LambdaCalculus.TBool", "constructor_distinct_Catala.LambdaCalculus.TOption", "constructor_distinct_Catala.LambdaCalculus.TUnit", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_FStar.Pervasives.Native.Some", "constructor_distinct_Tm_unit", "data_elim_Catala.LambdaCalculus.EAbs", "data_elim_Catala.LambdaCalculus.EApp", "data_elim_Catala.LambdaCalculus.EMatchOption", "data_elim_Catala.LambdaCalculus.EVar", "data_typing_intro_Catala.LambdaCalculus.EAbs@tok", "data_typing_intro_Catala.LambdaCalculus.EApp@tok", "data_typing_intro_Catala.LambdaCalculus.ECatchEmptyError@tok", "data_typing_intro_Catala.LambdaCalculus.ELit@tok", "data_typing_intro_Catala.LambdaCalculus.EMatchOption@tok", "data_typing_intro_Catala.LambdaCalculus.ENone@tok", "data_typing_intro_Catala.LambdaCalculus.ESome@tok", "data_typing_intro_Catala.LambdaCalculus.EVar@tok", "data_typing_intro_Catala.LambdaCalculus.LError@tok", "data_typing_intro_Catala.LambdaCalculus.TArrow@tok", "data_typing_intro_Catala.LambdaCalculus.TOption@tok", "data_typing_intro_Catala.LambdaCalculus.TUnit@tok", "disc_equation_Catala.LambdaCalculus.ConflictError", "disc_equation_Catala.LambdaCalculus.ELit", "disc_equation_Catala.LambdaCalculus.ENone", "disc_equation_Catala.LambdaCalculus.ESome", "disc_equation_Catala.LambdaCalculus.EmptyError", "disc_equation_Catala.LambdaCalculus.LError", "disc_equation_FStar.Pervasives.Native.None", "disc_equation_FStar.Pervasives.Native.Some", "equality_tok_Catala.LambdaCalculus.ConflictError@tok", "equality_tok_Catala.LambdaCalculus.ENone@tok", "equality_tok_Catala.LambdaCalculus.EmptyError@tok", "equality_tok_Catala.LambdaCalculus.TBool@tok", "equality_tok_Catala.LambdaCalculus.TUnit@tok", "equation_Catala.LambdaCalculus.empty", "equation_Catala.LambdaCalculus.extend", "equation_Catala.LambdaCalculus.is_error", "equation_Catala.LambdaCalculus.var", "equation_Catala.LambdaCalculus.var_to_exp", "equation_Catala.LambdaCalculus.var_to_exp_beta", "equation_Catala.Translation.Helpers.exceptions_head_lift", "equation_Catala.Translation.Helpers.exceptions_head_lift_", "equation_Catala.Translation.Helpers.exceptions_init_lift", "equation_Catala.Translation.Helpers.exceptions_init_lift_", "equation_Catala.Translation.Helpers.not_l_value", "equation_Catala.Translation.Helpers.process_exceptions_f", "equation_Catala.Translation.Helpers.typed_l_exp", "equation_FStar.FunctionalExtensionality.feq", "equation_Prims.nat", "equation_with_fuel_Catala.LambdaCalculus.is_value.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step_app.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step_catch.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step_match.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.subst.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.subst_abs.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.typing.fuel_instrumented", "equation_with_fuel_Catala.Translation.Helpers.take_l_steps.fuel_instrumented", "fuel_guarded_inversion_Catala.LambdaCalculus.err", "fuel_guarded_inversion_FStar.Pervasives.Native.option", "fuel_token_correspondence_Catala.LambdaCalculus.subst_abs.fuel_instrumented_token", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "interpretation_Tm_abs_1312e4782c558ee50ab7a5e0bfd49851", "interpretation_Tm_abs_396aa62eba4eabe2ab867a6b4ae34fc9", "interpretation_Tm_abs_44e059f7416b8cb4267e0f7a598f0380", "interpretation_Tm_abs_591e432507f9fc0b2baad4ac5bad3427", "interpretation_Tm_abs_683fecef0f32ab9df689545bd34ec676", "interpretation_Tm_abs_7041a26a87a3fce24dbf917ff7f2a6ff", "kinding_Catala.LambdaCalculus.exp@tok", "lemma_FStar.FunctionalExtensionality.feq_on_domain", "lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction", "proj_equation_Catala.LambdaCalculus.ELit_l", "proj_equation_FStar.Pervasives.Native.Some_v", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Catala.LambdaCalculus.EAbs_body", "projection_inverse_Catala.LambdaCalculus.EAbs_vty", "projection_inverse_Catala.LambdaCalculus.EApp_arg", "projection_inverse_Catala.LambdaCalculus.EApp_fn", "projection_inverse_Catala.LambdaCalculus.EApp_tau_arg", "projection_inverse_Catala.LambdaCalculus.ECatchEmptyError_catch_with", "projection_inverse_Catala.LambdaCalculus.ECatchEmptyError_to_try", "projection_inverse_Catala.LambdaCalculus.ELit_l", "projection_inverse_Catala.LambdaCalculus.EMatchOption_arg", "projection_inverse_Catala.LambdaCalculus.EMatchOption_none", "projection_inverse_Catala.LambdaCalculus.EMatchOption_some", "projection_inverse_Catala.LambdaCalculus.EMatchOption_tau_some", "projection_inverse_Catala.LambdaCalculus.ESome_s", "projection_inverse_Catala.LambdaCalculus.EVar_v", "projection_inverse_Catala.LambdaCalculus.LError_err", "projection_inverse_Catala.LambdaCalculus.TArrow_tin", "projection_inverse_Catala.LambdaCalculus.TArrow_tout", "projection_inverse_Catala.LambdaCalculus.TOption_a", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Some_a", "projection_inverse_FStar.Pervasives.Native.Some_v", "refinement_interpretation_Tm_refine_4d5241eb6fe198666a8101195bbd4a2a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_66a04fe873406083a229e09b1c833909", "refinement_interpretation_Tm_refine_8572abaf58b0908690b4c77b9bd5038b", "refinement_interpretation_Tm_refine_9d7619fada7e7cc3e29055f7763724da", "refinement_interpretation_Tm_refine_a392bfba80da306fafdb3d849a464ab4", "refinement_interpretation_Tm_refine_cb93ec9919d1810ec52a555a1c229683", "refinement_interpretation_Tm_refine_d5485f8c94130f85952cddf1019830bb", "refinement_interpretation_Tm_refine_e1e5cfe7267eb04a8960036ae88380cb", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "subterm_ordering_Catala.LambdaCalculus.EApp", "subterm_ordering_Catala.LambdaCalculus.ECatchEmptyError", "subterm_ordering_Catala.LambdaCalculus.EMatchOption", "token_correspondence_Catala.LambdaCalculus.is_value.fuel_instrumented", "token_correspondence_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "token_correspondence_Catala.LambdaCalculus.step.fuel_instrumented", "token_correspondence_Catala.LambdaCalculus.step_catch.fuel_instrumented", "token_correspondence_Catala.LambdaCalculus.subst.fuel_instrumented", "token_correspondence_Catala.LambdaCalculus.subst_abs.fuel_instrumented", "token_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", "token_correspondence_Catala.Translation.Helpers.exceptions_head_lift", "token_correspondence_Catala.Translation.Helpers.exceptions_init_lift", "typing_Catala.LambdaCalculus.empty", "typing_Catala.LambdaCalculus.extend", "typing_Catala.LambdaCalculus.increment", "typing_Catala.LambdaCalculus.is_value", "typing_Catala.LambdaCalculus.step", "typing_Catala.LambdaCalculus.subst", "typing_Catala.LambdaCalculus.typing", "typing_Catala.LambdaCalculus.var_to_exp_beta", "typing_Catala.Translation.Helpers.process_exceptions_f", "typing_FStar.Pervasives.Native.__proj__Some__item__v", "typing_Tm_abs_1312e4782c558ee50ab7a5e0bfd49851", "typing_Tm_abs_44e059f7416b8cb4267e0f7a598f0380", "typing_Tm_abs_683fecef0f32ab9df689545bd34ec676", "typing_tok_Catala.LambdaCalculus.ConflictError@tok", "typing_tok_Catala.LambdaCalculus.ENone@tok", "typing_tok_Catala.LambdaCalculus.TUnit@tok" ], 0, "ab38acf3ac1ed6287a545e9e282f06c6" ], [ "Catala.Translation.Helpers.step_exceptions_head_value_non_error", 1, 8, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.LambdaCalculus.is_value.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.step.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.subst.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.subst_abs.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.subst_list.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", "@fuel_correspondence_Catala.Translation.Helpers.take_l_steps.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.is_value.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.subst.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.subst_abs.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.subst_list.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.typing.fuel_instrumented", "@query", "Catala.LambdaCalculus_interpretation_Tm_arrow_0afe855ee0dd04a9f1572a7d68b10fa7", "Catala.LambdaCalculus_interpretation_Tm_arrow_732ef78b9bfa783d08279e5be1df507c", "Catala.LambdaCalculus_interpretation_Tm_arrow_dd74cc4a2c76fb3652280bf9d670f4d1", "Catala.LambdaCalculus_interpretation_Tm_arrow_ed0c592d82dfd5a47d39e42cf9d52a55", "Catala.LambdaCalculus_pretyping_8ab521cb5d1069fb182eea898efa7c42", "Catala.LambdaCalculus_pretyping_fabd258754d8bab26d9bc0ad1a882a83", "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Prims_pretyping_ae567c2fb75be05905677af440075565", "assumption_Catala.LambdaCalculus.exp__uu___haseq", "bool_inversion", "constructor_distinct_Catala.LambdaCalculus.ConflictError", "constructor_distinct_Catala.LambdaCalculus.EAbs", "constructor_distinct_Catala.LambdaCalculus.EApp", "constructor_distinct_Catala.LambdaCalculus.ECatchEmptyError", "constructor_distinct_Catala.LambdaCalculus.EFoldLeft", "constructor_distinct_Catala.LambdaCalculus.EIf", "constructor_distinct_Catala.LambdaCalculus.EList", "constructor_distinct_Catala.LambdaCalculus.ELit", "constructor_distinct_Catala.LambdaCalculus.EMatchOption", "constructor_distinct_Catala.LambdaCalculus.ENone", "constructor_distinct_Catala.LambdaCalculus.ESome", "constructor_distinct_Catala.LambdaCalculus.EVar", "constructor_distinct_Catala.LambdaCalculus.EmptyError", "constructor_distinct_Catala.LambdaCalculus.LError", "constructor_distinct_Catala.LambdaCalculus.TArrow", "constructor_distinct_Catala.LambdaCalculus.TBool", "constructor_distinct_Catala.LambdaCalculus.TOption", "constructor_distinct_Catala.LambdaCalculus.TUnit", "constructor_distinct_FStar.Pervasives.Native.Some", "constructor_distinct_Tm_unit", "data_elim_Catala.LambdaCalculus.EAbs", "data_elim_Catala.LambdaCalculus.EApp", "data_elim_Catala.LambdaCalculus.ECatchEmptyError", "data_elim_Catala.LambdaCalculus.EMatchOption", "data_elim_Catala.LambdaCalculus.ESome", "data_elim_Catala.LambdaCalculus.EVar", "data_typing_intro_Catala.LambdaCalculus.EAbs@tok", "data_typing_intro_Catala.LambdaCalculus.EApp@tok", "data_typing_intro_Catala.LambdaCalculus.ECatchEmptyError@tok", "data_typing_intro_Catala.LambdaCalculus.EMatchOption@tok", "data_typing_intro_Catala.LambdaCalculus.ENone@tok", "data_typing_intro_Catala.LambdaCalculus.ESome@tok", "data_typing_intro_Catala.LambdaCalculus.TArrow@tok", "data_typing_intro_Catala.LambdaCalculus.TOption@tok", "data_typing_intro_Catala.LambdaCalculus.TUnit@tok", "disc_equation_Catala.LambdaCalculus.ELit", "disc_equation_Catala.LambdaCalculus.ENone", "disc_equation_Catala.LambdaCalculus.ESome", "disc_equation_Catala.LambdaCalculus.LError", "disc_equation_FStar.Pervasives.Native.None", "disc_equation_FStar.Pervasives.Native.Some", "equality_tok_Catala.LambdaCalculus.ConflictError@tok", "equality_tok_Catala.LambdaCalculus.ENone@tok", "equality_tok_Catala.LambdaCalculus.EmptyError@tok", "equality_tok_Catala.LambdaCalculus.TBool@tok", "equality_tok_Catala.LambdaCalculus.TUnit@tok", "equation_Catala.LambdaCalculus.empty", "equation_Catala.LambdaCalculus.extend", "equation_Catala.LambdaCalculus.is_error", "equation_Catala.LambdaCalculus.var", "equation_Catala.LambdaCalculus.var_to_exp", "equation_Catala.LambdaCalculus.var_to_exp_beta", "equation_Catala.Translation.Helpers.exceptions_head_lift", "equation_Catala.Translation.Helpers.exceptions_head_lift_", "equation_Catala.Translation.Helpers.exceptions_init_lift", "equation_Catala.Translation.Helpers.exceptions_init_lift_", "equation_Catala.Translation.Helpers.not_l_value", "equation_Catala.Translation.Helpers.process_exceptions_f", "equation_Catala.Translation.Helpers.typed_l_exp", "equation_FStar.FunctionalExtensionality.feq", "equation_Prims.nat", "equation_with_fuel_Catala.LambdaCalculus.is_value.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step_app.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step_catch.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step_match.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.subst.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.subst_abs.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.typing.fuel_instrumented", "equation_with_fuel_Catala.Translation.Helpers.take_l_steps.fuel_instrumented", "fuel_guarded_inversion_Catala.LambdaCalculus.err", "fuel_guarded_inversion_Catala.LambdaCalculus.exp", "fuel_guarded_inversion_FStar.Pervasives.Native.option", "fuel_token_correspondence_Catala.LambdaCalculus.subst_abs.fuel_instrumented_token", "function_token_typing_Catala.LambdaCalculus.subst_abs", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "interpretation_Tm_abs_1312e4782c558ee50ab7a5e0bfd49851", "interpretation_Tm_abs_396aa62eba4eabe2ab867a6b4ae34fc9", "interpretation_Tm_abs_591e432507f9fc0b2baad4ac5bad3427", "interpretation_Tm_abs_683fecef0f32ab9df689545bd34ec676", "interpretation_Tm_abs_7041a26a87a3fce24dbf917ff7f2a6ff", "kinding_Catala.LambdaCalculus.exp@tok", "lemma_Catala.LambdaCalculus.substitution_extensionnal", "lemma_FStar.FunctionalExtensionality.feq_on_domain", "lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction", "proj_equation_Catala.LambdaCalculus.ELit_l", "proj_equation_FStar.Pervasives.Native.Some_v", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Catala.LambdaCalculus.EAbs_body", "projection_inverse_Catala.LambdaCalculus.EAbs_vty", "projection_inverse_Catala.LambdaCalculus.EApp_arg", "projection_inverse_Catala.LambdaCalculus.EApp_fn", "projection_inverse_Catala.LambdaCalculus.EApp_tau_arg", "projection_inverse_Catala.LambdaCalculus.ECatchEmptyError_catch_with", "projection_inverse_Catala.LambdaCalculus.ECatchEmptyError_to_try", "projection_inverse_Catala.LambdaCalculus.EList_l", "projection_inverse_Catala.LambdaCalculus.ELit_l", "projection_inverse_Catala.LambdaCalculus.EMatchOption_arg", "projection_inverse_Catala.LambdaCalculus.EMatchOption_none", "projection_inverse_Catala.LambdaCalculus.EMatchOption_some", "projection_inverse_Catala.LambdaCalculus.EMatchOption_tau_some", "projection_inverse_Catala.LambdaCalculus.ESome_s", "projection_inverse_Catala.LambdaCalculus.EThunk_body", "projection_inverse_Catala.LambdaCalculus.EVar_v", "projection_inverse_Catala.LambdaCalculus.LError_err", "projection_inverse_Catala.LambdaCalculus.TArrow_tin", "projection_inverse_Catala.LambdaCalculus.TArrow_tout", "projection_inverse_Catala.LambdaCalculus.TOption_a", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Some_a", "projection_inverse_FStar.Pervasives.Native.Some_v", "refinement_interpretation_Tm_refine_4d5241eb6fe198666a8101195bbd4a2a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_66a04fe873406083a229e09b1c833909", "refinement_interpretation_Tm_refine_8572abaf58b0908690b4c77b9bd5038b", "refinement_interpretation_Tm_refine_9d7619fada7e7cc3e29055f7763724da", "refinement_interpretation_Tm_refine_a392bfba80da306fafdb3d849a464ab4", "refinement_interpretation_Tm_refine_cb93ec9919d1810ec52a555a1c229683", "refinement_interpretation_Tm_refine_d5485f8c94130f85952cddf1019830bb", "refinement_interpretation_Tm_refine_e1e5cfe7267eb04a8960036ae88380cb", "refinement_interpretation_Tm_refine_f33f995a4ed5542fd07641311dffcd2c", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "subterm_ordering_Catala.LambdaCalculus.EApp", "subterm_ordering_Catala.LambdaCalculus.ECatchEmptyError", "subterm_ordering_Catala.LambdaCalculus.EMatchOption", "token_correspondence_Catala.LambdaCalculus.is_value.fuel_instrumented", "token_correspondence_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "token_correspondence_Catala.LambdaCalculus.step.fuel_instrumented", "token_correspondence_Catala.LambdaCalculus.subst.fuel_instrumented", "token_correspondence_Catala.LambdaCalculus.subst_abs", "token_correspondence_Catala.LambdaCalculus.subst_abs.fuel_instrumented", "token_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", "token_correspondence_Catala.Translation.Helpers.exceptions_head_lift", "token_correspondence_Catala.Translation.Helpers.exceptions_init_lift", "typing_Catala.LambdaCalculus.empty", "typing_Catala.LambdaCalculus.extend", "typing_Catala.LambdaCalculus.increment", "typing_Catala.LambdaCalculus.is_error", "typing_Catala.LambdaCalculus.is_value", "typing_Catala.LambdaCalculus.step", "typing_Catala.LambdaCalculus.subst", "typing_Catala.LambdaCalculus.typing", "typing_Catala.LambdaCalculus.var_to_exp_beta", "typing_Catala.Translation.Helpers.process_exceptions_f", "typing_FStar.Pervasives.Native.__proj__Some__item__v", "typing_Tm_abs_1312e4782c558ee50ab7a5e0bfd49851", "typing_Tm_abs_591e432507f9fc0b2baad4ac5bad3427", "typing_Tm_abs_683fecef0f32ab9df689545bd34ec676", "typing_tok_Catala.LambdaCalculus.ENone@tok", "typing_tok_Catala.LambdaCalculus.TUnit@tok" ], 0, "5053a5ebb4dd3639b539de6e78500118" ], [ "Catala.Translation.Helpers.step_exceptions_head_value", 1, 7, 2, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "@query", "assumption_Catala.LambdaCalculus.exp__uu___haseq", "bool_inversion", "disc_equation_Catala.LambdaCalculus.ELit", "disc_equation_Catala.LambdaCalculus.LError", "equation_Catala.LambdaCalculus.is_error", "equation_Catala.Translation.Helpers.typed_l_exp", "equation_with_fuel_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "proj_equation_Catala.LambdaCalculus.ELit_l", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_cb93ec9919d1810ec52a555a1c229683", "refinement_interpretation_Tm_refine_d5485f8c94130f85952cddf1019830bb", "token_correspondence_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "typing_Catala.LambdaCalculus.is_error", "typing_Catala.LambdaCalculus.uu___is_ELit" ], 0, "2b5d722d46440cfad7471440df32d11a" ], [ "Catala.Translation.Helpers.step_exceptions_head_value_same_acc_result", 1, 7, 2, [ "@query", "assumption_Catala.LambdaCalculus.exp__uu___haseq" ], 0, "e05f6308cdce42d7b81337591cb1f396" ], [ "Catala.Translation.Helpers.step_exceptions_head_value_same_acc_result", 2, 7, 2, [ "@MaxIFuel_assumption", "@query", "equation_Catala.Translation.Helpers.step_exceptions_head_value", "equation_Catala.Translation.Helpers.step_exceptions_head_value_error", "equation_Catala.Translation.Helpers.step_exceptions_head_value_non_error", "refinement_interpretation_Tm_refine_490a77d8724dba478516c70d0d037b5b", "refinement_interpretation_Tm_refine_cdbe32eb48421474d9b70d61150eebfe" ], 0, "7ce3f98595d41dc52a0c9aad7b178f72" ], [ "Catala.Translation.Helpers.step_exceptions_head_value_go_through", 1, 7, 2, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.LambdaCalculus.is_value.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", "@query", "assumption_Catala.LambdaCalculus.exp__uu___haseq", "bool_inversion", "constructor_distinct_Catala.LambdaCalculus.ELit", "constructor_distinct_Catala.LambdaCalculus.ENone", "constructor_distinct_Catala.LambdaCalculus.EmptyError", "constructor_distinct_Catala.LambdaCalculus.LError", "constructor_distinct_Catala.LambdaCalculus.TOption", "data_typing_intro_Catala.LambdaCalculus.ELit@tok", "data_typing_intro_Catala.LambdaCalculus.LError@tok", "data_typing_intro_Catala.LambdaCalculus.TOption@tok", "equality_tok_Catala.LambdaCalculus.ENone@tok", "equality_tok_Catala.LambdaCalculus.EmptyError@tok", "equation_Catala.LambdaCalculus.empty", "equation_Catala.Translation.Helpers.step_exceptions_head_value", "equation_Catala.Translation.Helpers.step_exceptions_head_value_error", "equation_Catala.Translation.Helpers.typed_l_exp", "equation_Prims.nat", "equation_with_fuel_Catala.LambdaCalculus.is_value.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.typing.fuel_instrumented", "projection_inverse_Catala.LambdaCalculus.ELit_l", "projection_inverse_Catala.LambdaCalculus.LError_err", "projection_inverse_Catala.LambdaCalculus.TOption_a", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "refinement_interpretation_Tm_refine_cb93ec9919d1810ec52a555a1c229683", "token_correspondence_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "typing_Catala.LambdaCalculus.empty", "typing_tok_Catala.LambdaCalculus.ENone@tok", "typing_tok_Catala.LambdaCalculus.EmptyError@tok" ], 0, "fd39ad81dcdf53ccdce3c204c9485e57" ], [ "Catala.Translation.Helpers.step_exceptions_empty_conflict_error", 1, 7, 2, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.typing_list.fuel_instrumented", "@query", "Catala.LambdaCalculus_pretyping_fabd258754d8bab26d9bc0ad1a882a83", "bool_inversion", "constructor_distinct_Catala.LambdaCalculus.ELit", "constructor_distinct_Catala.LambdaCalculus.LError", "constructor_distinct_Prims.Nil", "data_typing_intro_Catala.LambdaCalculus.ELit@tok", "data_typing_intro_Catala.LambdaCalculus.ENone@tok", "data_typing_intro_Catala.LambdaCalculus.LError@tok", "data_typing_intro_Catala.LambdaCalculus.TArrow@tok", "data_typing_intro_Catala.LambdaCalculus.TOption@tok", "data_typing_intro_Prims.Nil@tok", "equality_tok_Catala.LambdaCalculus.ConflictError@tok", "equality_tok_Catala.LambdaCalculus.TBool@tok", "equality_tok_Catala.LambdaCalculus.TUnit@tok", "equation_Catala.LambdaCalculus.empty", "equation_Catala.Translation.Helpers.typed_l_exp", "equation_with_fuel_Catala.LambdaCalculus.typing.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.typing_list.fuel_instrumented", "kinding_Catala.LambdaCalculus.exp@tok", "projection_inverse_Catala.LambdaCalculus.ELit_l", "projection_inverse_Catala.LambdaCalculus.LError_err", "projection_inverse_Prims.Nil_a", "refinement_interpretation_Tm_refine_d5485f8c94130f85952cddf1019830bb", "typing_Catala.LambdaCalculus.empty", "typing_Catala.LambdaCalculus.typing", "typing_tok_Catala.LambdaCalculus.ConflictError@tok", "typing_tok_Catala.LambdaCalculus.TBool@tok", "typing_tok_Catala.LambdaCalculus.TUnit@tok" ], 0, "964a7b7a9f0052d73330917f701ab7a8" ], [ "Catala.Translation.Helpers.step_exceptions_empty_some_acc", 1, 4, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.LambdaCalculus.is_value.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.step.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.subst.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.typing_list.fuel_instrumented", "@fuel_correspondence_Catala.Translation.Helpers.take_l_steps.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.is_value.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.typing.fuel_instrumented", "@query", "Catala.LambdaCalculus_interpretation_Tm_arrow_0afe855ee0dd04a9f1572a7d68b10fa7", "Catala.LambdaCalculus_interpretation_Tm_arrow_ed0c592d82dfd5a47d39e42cf9d52a55", "Catala.LambdaCalculus_pretyping_8ab521cb5d1069fb182eea898efa7c42", "Catala.LambdaCalculus_pretyping_fabd258754d8bab26d9bc0ad1a882a83", "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion", "constructor_distinct_Catala.LambdaCalculus.EAbs", "constructor_distinct_Catala.LambdaCalculus.EApp", "constructor_distinct_Catala.LambdaCalculus.EFoldLeft", "constructor_distinct_Catala.LambdaCalculus.EIf", "constructor_distinct_Catala.LambdaCalculus.EList", "constructor_distinct_Catala.LambdaCalculus.ELit", "constructor_distinct_Catala.LambdaCalculus.EMatchOption", "constructor_distinct_Catala.LambdaCalculus.ESome", "constructor_distinct_Catala.LambdaCalculus.EVar", "constructor_distinct_Catala.LambdaCalculus.LError", "constructor_distinct_Catala.LambdaCalculus.TArrow", "constructor_distinct_Catala.LambdaCalculus.TOption", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_FStar.Pervasives.Native.Some", "constructor_distinct_Prims.Nil", "constructor_distinct_Tm_unit", "data_elim_Catala.LambdaCalculus.EMatchOption", "data_typing_intro_Catala.LambdaCalculus.EAbs@tok", "data_typing_intro_Catala.LambdaCalculus.EApp@tok", "data_typing_intro_Catala.LambdaCalculus.EIf@tok", "data_typing_intro_Catala.LambdaCalculus.EList@tok", "data_typing_intro_Catala.LambdaCalculus.ELit@tok", "data_typing_intro_Catala.LambdaCalculus.EMatchOption@tok", "data_typing_intro_Catala.LambdaCalculus.ENone@tok", "data_typing_intro_Catala.LambdaCalculus.ESome@tok", "data_typing_intro_Catala.LambdaCalculus.EVar@tok", "data_typing_intro_Catala.LambdaCalculus.LError@tok", "data_typing_intro_Catala.LambdaCalculus.TArrow@tok", "data_typing_intro_Catala.LambdaCalculus.TOption@tok", "data_typing_intro_Catala.LambdaCalculus.TUnit@tok", "data_typing_intro_Prims.Nil@tok", "equality_tok_Catala.LambdaCalculus.EmptyError@tok", "equality_tok_Catala.LambdaCalculus.TBool@tok", "equality_tok_Catala.LambdaCalculus.TUnit@tok", "equation_Catala.LambdaCalculus.empty", "equation_Catala.LambdaCalculus.extend", "equation_Catala.LambdaCalculus.is_error", "equation_Catala.LambdaCalculus.var", "equation_Catala.LambdaCalculus.var_to_exp_beta", "equation_Catala.Translation.Helpers.build_default_translation", "equation_Catala.Translation.Helpers.process_exceptions_f", "equation_Catala.Translation.Helpers.typed_l_exp", "equation_FStar.FunctionalExtensionality.feq", "equation_Prims.nat", "equation_with_fuel_Catala.LambdaCalculus.is_value.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step_app.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step_fold_left.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step_match.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.subst.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.typing.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.typing_list.fuel_instrumented", "equation_with_fuel_Catala.Translation.Helpers.take_l_steps.fuel_instrumented", "fuel_guarded_inversion_FStar.Pervasives.Native.option", "function_token_typing_Prims.__cache_version_number__", "int_typing", "interpretation_Tm_abs_1312e4782c558ee50ab7a5e0bfd49851", "interpretation_Tm_abs_591e432507f9fc0b2baad4ac5bad3427", "interpretation_Tm_abs_683fecef0f32ab9df689545bd34ec676", "kinding_Catala.LambdaCalculus.exp@tok", "lemma_FStar.FunctionalExtensionality.feq_on_domain", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Catala.LambdaCalculus.EAbs_body", "projection_inverse_Catala.LambdaCalculus.EAbs_vty", "projection_inverse_Catala.LambdaCalculus.EApp_arg", "projection_inverse_Catala.LambdaCalculus.EApp_fn", "projection_inverse_Catala.LambdaCalculus.EApp_tau_arg", "projection_inverse_Catala.LambdaCalculus.EFoldLeft_f", "projection_inverse_Catala.LambdaCalculus.EFoldLeft_init", "projection_inverse_Catala.LambdaCalculus.EFoldLeft_l", "projection_inverse_Catala.LambdaCalculus.EFoldLeft_tau_elt", "projection_inverse_Catala.LambdaCalculus.EFoldLeft_tau_init", "projection_inverse_Catala.LambdaCalculus.EIf_bfalse", "projection_inverse_Catala.LambdaCalculus.EIf_btrue", "projection_inverse_Catala.LambdaCalculus.EIf_test", "projection_inverse_Catala.LambdaCalculus.EList_l", "projection_inverse_Catala.LambdaCalculus.ELit_l", "projection_inverse_Catala.LambdaCalculus.EMatchOption_arg", "projection_inverse_Catala.LambdaCalculus.EMatchOption_none", "projection_inverse_Catala.LambdaCalculus.EMatchOption_some", "projection_inverse_Catala.LambdaCalculus.EMatchOption_tau_some", "projection_inverse_Catala.LambdaCalculus.ESome_s", "projection_inverse_Catala.LambdaCalculus.EVar_v", "projection_inverse_Catala.LambdaCalculus.LError_err", "projection_inverse_Catala.LambdaCalculus.TArrow_tin", "projection_inverse_Catala.LambdaCalculus.TArrow_tout", "projection_inverse_Catala.LambdaCalculus.TOption_a", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "projection_inverse_FStar.Pervasives.Native.Some_v", "projection_inverse_Prims.Nil_a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8572abaf58b0908690b4c77b9bd5038b", "refinement_interpretation_Tm_refine_9d7619fada7e7cc3e29055f7763724da", "refinement_interpretation_Tm_refine_d5485f8c94130f85952cddf1019830bb", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "subterm_ordering_Catala.LambdaCalculus.EApp", "subterm_ordering_Catala.LambdaCalculus.EFoldLeft", "subterm_ordering_Catala.LambdaCalculus.EMatchOption", "token_correspondence_Catala.LambdaCalculus.step_fold_left.fuel_instrumented", "token_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", "typing_Catala.LambdaCalculus.empty", "typing_Catala.LambdaCalculus.extend", "typing_Catala.LambdaCalculus.is_error", "typing_Catala.LambdaCalculus.is_value", "typing_Catala.LambdaCalculus.step", "typing_Catala.LambdaCalculus.typing", "typing_Catala.LambdaCalculus.var_to_exp_beta", "typing_Catala.Translation.Helpers.build_default_translation", "typing_Catala.Translation.Helpers.process_exceptions_f", "typing_Tm_abs_1312e4782c558ee50ab7a5e0bfd49851", "typing_Tm_abs_683fecef0f32ab9df689545bd34ec676", "typing_tok_Catala.LambdaCalculus.EmptyError@tok", "typing_tok_Catala.LambdaCalculus.TBool@tok", "typing_tok_Catala.LambdaCalculus.TUnit@tok" ], 0, "8b7eacb9ede89cadf60542b15ca48913" ], [ "Catala.Translation.Helpers.step_exceptions_empty_none", 1, 4, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.LambdaCalculus.is_value.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.step.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.typing_list.fuel_instrumented", "@fuel_correspondence_Catala.Translation.Helpers.take_l_steps.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.typing.fuel_instrumented", "@query", "Catala.LambdaCalculus_interpretation_Tm_arrow_0afe855ee0dd04a9f1572a7d68b10fa7", "Catala.LambdaCalculus_interpretation_Tm_arrow_ed0c592d82dfd5a47d39e42cf9d52a55", "Catala.LambdaCalculus_pretyping_8ab521cb5d1069fb182eea898efa7c42", "Catala.LambdaCalculus_pretyping_fabd258754d8bab26d9bc0ad1a882a83", "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion", "constructor_distinct_Catala.LambdaCalculus.EAbs", "constructor_distinct_Catala.LambdaCalculus.EFoldLeft", "constructor_distinct_Catala.LambdaCalculus.EIf", "constructor_distinct_Catala.LambdaCalculus.EList", "constructor_distinct_Catala.LambdaCalculus.ELit", "constructor_distinct_Catala.LambdaCalculus.EMatchOption", "constructor_distinct_Catala.LambdaCalculus.ENone", "constructor_distinct_Catala.LambdaCalculus.EVar", "constructor_distinct_Catala.LambdaCalculus.LError", "constructor_distinct_Catala.LambdaCalculus.TArrow", "constructor_distinct_Catala.LambdaCalculus.TOption", "constructor_distinct_FStar.Pervasives.Native.Some", "constructor_distinct_Prims.Nil", "constructor_distinct_Tm_unit", "data_elim_Catala.LambdaCalculus.EMatchOption", "data_typing_intro_Catala.LambdaCalculus.EAbs@tok", "data_typing_intro_Catala.LambdaCalculus.EIf@tok", "data_typing_intro_Catala.LambdaCalculus.EList@tok", "data_typing_intro_Catala.LambdaCalculus.ELit@tok", "data_typing_intro_Catala.LambdaCalculus.EMatchOption@tok", "data_typing_intro_Catala.LambdaCalculus.ENone@tok", "data_typing_intro_Catala.LambdaCalculus.EVar@tok", "data_typing_intro_Catala.LambdaCalculus.LError@tok", "data_typing_intro_Catala.LambdaCalculus.TArrow@tok", "data_typing_intro_Catala.LambdaCalculus.TOption@tok", "data_typing_intro_Catala.LambdaCalculus.TUnit@tok", "data_typing_intro_Prims.Nil@tok", "disc_equation_FStar.Pervasives.Native.None", "equality_tok_Catala.LambdaCalculus.ENone@tok", "equality_tok_Catala.LambdaCalculus.EmptyError@tok", "equality_tok_Catala.LambdaCalculus.TBool@tok", "equality_tok_Catala.LambdaCalculus.TUnit@tok", "equation_Catala.LambdaCalculus.empty", "equation_Catala.LambdaCalculus.extend", "equation_Catala.LambdaCalculus.var", "equation_Catala.Translation.Helpers.build_default_translation", "equation_Catala.Translation.Helpers.process_exceptions_f", "equation_Catala.Translation.Helpers.typed_l_exp", "equation_FStar.FunctionalExtensionality.feq", "equation_Prims.nat", "equation_with_fuel_Catala.LambdaCalculus.is_value.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step_fold_left.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step_match.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.typing.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.typing_list.fuel_instrumented", "equation_with_fuel_Catala.Translation.Helpers.take_l_steps.fuel_instrumented", "fuel_guarded_inversion_FStar.Pervasives.Native.option", "function_token_typing_Prims.__cache_version_number__", "int_typing", "interpretation_Tm_abs_1312e4782c558ee50ab7a5e0bfd49851", "interpretation_Tm_abs_683fecef0f32ab9df689545bd34ec676", "kinding_Catala.LambdaCalculus.exp@tok", "lemma_FStar.FunctionalExtensionality.feq_on_domain", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Catala.LambdaCalculus.EAbs_body", "projection_inverse_Catala.LambdaCalculus.EAbs_vty", "projection_inverse_Catala.LambdaCalculus.EFoldLeft_f", "projection_inverse_Catala.LambdaCalculus.EFoldLeft_init", "projection_inverse_Catala.LambdaCalculus.EFoldLeft_l", "projection_inverse_Catala.LambdaCalculus.EFoldLeft_tau_elt", "projection_inverse_Catala.LambdaCalculus.EFoldLeft_tau_init", "projection_inverse_Catala.LambdaCalculus.EIf_bfalse", "projection_inverse_Catala.LambdaCalculus.EIf_btrue", "projection_inverse_Catala.LambdaCalculus.EIf_test", "projection_inverse_Catala.LambdaCalculus.EList_l", "projection_inverse_Catala.LambdaCalculus.ELit_l", "projection_inverse_Catala.LambdaCalculus.EMatchOption_arg", "projection_inverse_Catala.LambdaCalculus.EMatchOption_none", "projection_inverse_Catala.LambdaCalculus.EMatchOption_some", "projection_inverse_Catala.LambdaCalculus.EMatchOption_tau_some", "projection_inverse_Catala.LambdaCalculus.EVar_v", "projection_inverse_Catala.LambdaCalculus.LError_err", "projection_inverse_Catala.LambdaCalculus.TArrow_tin", "projection_inverse_Catala.LambdaCalculus.TArrow_tout", "projection_inverse_Catala.LambdaCalculus.TOption_a", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "projection_inverse_FStar.Pervasives.Native.Some_a", "projection_inverse_FStar.Pervasives.Native.Some_v", "projection_inverse_Prims.Nil_a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8572abaf58b0908690b4c77b9bd5038b", "refinement_interpretation_Tm_refine_d5485f8c94130f85952cddf1019830bb", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "subterm_ordering_Catala.LambdaCalculus.EFoldLeft", "subterm_ordering_Catala.LambdaCalculus.EMatchOption", "token_correspondence_Catala.LambdaCalculus.step.fuel_instrumented", "typing_Catala.LambdaCalculus.empty", "typing_Catala.LambdaCalculus.extend", "typing_Catala.LambdaCalculus.step", "typing_Catala.LambdaCalculus.typing", "typing_Catala.Translation.Helpers.build_default_translation", "typing_Catala.Translation.Helpers.process_exceptions_f", "typing_Tm_abs_1312e4782c558ee50ab7a5e0bfd49851", "typing_Tm_abs_683fecef0f32ab9df689545bd34ec676", "typing_tok_Catala.LambdaCalculus.ENone@tok", "typing_tok_Catala.LambdaCalculus.EmptyError@tok", "typing_tok_Catala.LambdaCalculus.TBool@tok", "typing_tok_Catala.LambdaCalculus.TUnit@tok" ], 0, "04a3454dcfd63671c86c799d598c0404" ], [ "Catala.Translation.Helpers.step_exceptions_cons_conflict_error", 1, 4, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.LambdaCalculus.is_value.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.step.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.typing_list.fuel_instrumented", "@fuel_correspondence_Catala.Translation.Helpers.take_l_steps.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.typing.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.typing_list.fuel_instrumented", "@query", "Catala.LambdaCalculus_pretyping_fabd258754d8bab26d9bc0ad1a882a83", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion", "constructor_distinct_Catala.LambdaCalculus.EAbs", "constructor_distinct_Catala.LambdaCalculus.EFoldLeft", "constructor_distinct_Catala.LambdaCalculus.EList", "constructor_distinct_Catala.LambdaCalculus.ELit", "constructor_distinct_Catala.LambdaCalculus.EMatchOption", "constructor_distinct_Catala.LambdaCalculus.EThunk", "constructor_distinct_Catala.LambdaCalculus.LError", "constructor_distinct_Catala.LambdaCalculus.TArrow", "constructor_distinct_Catala.LambdaCalculus.TUnit", "constructor_distinct_FStar.Pervasives.Native.Some", "constructor_distinct_Prims.Cons", "constructor_distinct_Tm_unit", "data_elim_Catala.LambdaCalculus.EMatchOption", "data_typing_intro_Catala.LambdaCalculus.EList@tok", "data_typing_intro_Catala.LambdaCalculus.ELit@tok", "data_typing_intro_Catala.LambdaCalculus.EMatchOption@tok", "data_typing_intro_Catala.LambdaCalculus.ENone@tok", "data_typing_intro_Catala.LambdaCalculus.EThunk@tok", "data_typing_intro_Catala.LambdaCalculus.LError@tok", "data_typing_intro_Catala.LambdaCalculus.TArrow@tok", "data_typing_intro_Catala.LambdaCalculus.TOption@tok", "data_typing_intro_Prims.Cons@tok", "disc_equation_FStar.Pervasives.Native.None", "equality_tok_Catala.LambdaCalculus.ConflictError@tok", "equality_tok_Catala.LambdaCalculus.TBool@tok", "equality_tok_Catala.LambdaCalculus.TUnit@tok", "equation_Catala.LambdaCalculus.empty", "equation_Catala.Translation.Helpers.build_default_translation", "equation_Catala.Translation.Helpers.process_exceptions_f", "equation_Catala.Translation.Helpers.typed_l_exp", "equation_Prims.nat", "equation_with_fuel_Catala.LambdaCalculus.is_value.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step_fold_left.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step_match.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.typing.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.typing_list.fuel_instrumented", "equation_with_fuel_Catala.Translation.Helpers.take_l_steps.fuel_instrumented", "fuel_guarded_inversion_FStar.Pervasives.Native.option", "function_token_typing_Prims.__cache_version_number__", "int_typing", "kinding_Catala.LambdaCalculus.exp@tok", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Catala.LambdaCalculus.EAbs_body", "projection_inverse_Catala.LambdaCalculus.EAbs_vty", "projection_inverse_Catala.LambdaCalculus.EFoldLeft_f", "projection_inverse_Catala.LambdaCalculus.EFoldLeft_init", "projection_inverse_Catala.LambdaCalculus.EFoldLeft_l", "projection_inverse_Catala.LambdaCalculus.EFoldLeft_tau_elt", "projection_inverse_Catala.LambdaCalculus.EFoldLeft_tau_init", "projection_inverse_Catala.LambdaCalculus.EList_l", "projection_inverse_Catala.LambdaCalculus.ELit_l", "projection_inverse_Catala.LambdaCalculus.EMatchOption_arg", "projection_inverse_Catala.LambdaCalculus.EMatchOption_none", "projection_inverse_Catala.LambdaCalculus.EMatchOption_some", "projection_inverse_Catala.LambdaCalculus.EMatchOption_tau_some", "projection_inverse_Catala.LambdaCalculus.EThunk_body", "projection_inverse_Catala.LambdaCalculus.LError_err", "projection_inverse_Catala.LambdaCalculus.TArrow_tin", "projection_inverse_Catala.LambdaCalculus.TArrow_tout", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "projection_inverse_FStar.Pervasives.Native.Some_a", "projection_inverse_FStar.Pervasives.Native.Some_v", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8572abaf58b0908690b4c77b9bd5038b", "refinement_interpretation_Tm_refine_d5485f8c94130f85952cddf1019830bb", "refinement_interpretation_Tm_refine_e2c2f0efbfe8e38b59c86ddd5972bf09", "subterm_ordering_Catala.LambdaCalculus.EFoldLeft", "subterm_ordering_Catala.LambdaCalculus.EMatchOption", "token_correspondence_Catala.LambdaCalculus.step.fuel_instrumented", "token_correspondence_Catala.LambdaCalculus.step_fold_left.fuel_instrumented", "token_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", "token_correspondence_Catala.LambdaCalculus.typing_list.fuel_instrumented", "typing_Catala.LambdaCalculus.empty", "typing_Catala.LambdaCalculus.is_value_list", "typing_Catala.LambdaCalculus.step", "typing_Catala.LambdaCalculus.typing", "typing_Catala.LambdaCalculus.typing_list", "typing_Catala.Translation.Helpers.build_default_translation", "typing_Catala.Translation.Helpers.process_exceptions_f", "typing_tok_Catala.LambdaCalculus.ConflictError@tok", "typing_tok_Catala.LambdaCalculus.TBool@tok", "typing_tok_Catala.LambdaCalculus.TUnit@tok" ], 0, "8193afcb622515601d683c0439d272c6" ], [ "Catala.Translation.Helpers.step_exceptions_general_conflict_error", 1, 4, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.LambdaCalculus.is_value.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.step.fuel_instrumented", "@fuel_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", "@fuel_correspondence_Catala.Translation.Helpers.take_l_steps.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.is_value_list.fuel_instrumented", "@fuel_irrelevance_Catala.LambdaCalculus.typing.fuel_instrumented", "@query", "Catala.LambdaCalculus_pretyping_8ab521cb5d1069fb182eea898efa7c42", "Catala.LambdaCalculus_pretyping_fabd258754d8bab26d9bc0ad1a882a83", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion", "bool_typing", "constructor_distinct_Catala.LambdaCalculus.EAbs", "constructor_distinct_Catala.LambdaCalculus.EFoldLeft", "constructor_distinct_Catala.LambdaCalculus.EList", "constructor_distinct_Catala.LambdaCalculus.ELit", "constructor_distinct_Catala.LambdaCalculus.EMatchOption", "constructor_distinct_Catala.LambdaCalculus.LError", "constructor_distinct_FStar.Pervasives.Native.Some", "constructor_distinct_Tm_unit", "data_elim_Catala.LambdaCalculus.EMatchOption", "data_typing_intro_Catala.LambdaCalculus.EList@tok", "data_typing_intro_Catala.LambdaCalculus.ELit@tok", "data_typing_intro_Catala.LambdaCalculus.EMatchOption@tok", "data_typing_intro_Catala.LambdaCalculus.ENone@tok", "data_typing_intro_Catala.LambdaCalculus.LError@tok", "data_typing_intro_Catala.LambdaCalculus.TArrow@tok", "data_typing_intro_Catala.LambdaCalculus.TOption@tok", "data_typing_intro_Catala.LambdaCalculus.TUnit@tok", "disc_equation_FStar.Pervasives.Native.None", "equality_tok_Catala.LambdaCalculus.ConflictError@tok", "equality_tok_Catala.LambdaCalculus.TBool@tok", "equality_tok_Catala.LambdaCalculus.TUnit@tok", "equation_Catala.LambdaCalculus.empty", "equation_Catala.Translation.Helpers.build_default_translation", "equation_Catala.Translation.Helpers.process_exceptions_f", "equation_Catala.Translation.Helpers.typed_l_exp", "equation_Prims.nat", "equation_with_fuel_Catala.LambdaCalculus.is_value.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step_fold_left.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.step_match.fuel_instrumented", "equation_with_fuel_Catala.LambdaCalculus.typing.fuel_instrumented", "equation_with_fuel_Catala.Translation.Helpers.take_l_steps.fuel_instrumented", "fuel_guarded_inversion_FStar.Pervasives.Native.option", "function_token_typing_Prims.__cache_version_number__", "int_typing", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Catala.LambdaCalculus.EAbs_body", "projection_inverse_Catala.LambdaCalculus.EAbs_vty", "projection_inverse_Catala.LambdaCalculus.EFoldLeft_f", "projection_inverse_Catala.LambdaCalculus.EFoldLeft_init", "projection_inverse_Catala.LambdaCalculus.EFoldLeft_l", "projection_inverse_Catala.LambdaCalculus.EFoldLeft_tau_elt", "projection_inverse_Catala.LambdaCalculus.EFoldLeft_tau_init", "projection_inverse_Catala.LambdaCalculus.EList_l", "projection_inverse_Catala.LambdaCalculus.ELit_l", "projection_inverse_Catala.LambdaCalculus.EMatchOption_arg", "projection_inverse_Catala.LambdaCalculus.EMatchOption_none", "projection_inverse_Catala.LambdaCalculus.EMatchOption_some", "projection_inverse_Catala.LambdaCalculus.EMatchOption_tau_some", "projection_inverse_Catala.LambdaCalculus.LError_err", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "projection_inverse_FStar.Pervasives.Native.Some_a", "projection_inverse_FStar.Pervasives.Native.Some_v", "refinement_interpretation_Tm_refine_1ce4cf8402ca4362b3cefd5b2138fe7c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8572abaf58b0908690b4c77b9bd5038b", "refinement_interpretation_Tm_refine_d5485f8c94130f85952cddf1019830bb", "subterm_ordering_Catala.LambdaCalculus.EFoldLeft", "subterm_ordering_Catala.LambdaCalculus.EMatchOption", "token_correspondence_Catala.LambdaCalculus.step.fuel_instrumented", "token_correspondence_Catala.LambdaCalculus.typing.fuel_instrumented", "typing_Catala.LambdaCalculus.empty", "typing_Catala.LambdaCalculus.is_value_list", "typing_Catala.LambdaCalculus.step", "typing_Catala.LambdaCalculus.typing", "typing_Catala.Translation.Helpers.build_default_translation", "typing_Catala.Translation.Helpers.process_exceptions_f", "typing_tok_Catala.LambdaCalculus.ConflictError@tok", "typing_tok_Catala.LambdaCalculus.TBool@tok", "typing_tok_Catala.LambdaCalculus.TUnit@tok" ], 0, "ae623444f9eab8e4819f002af7dbe5e6" ] ] ]