[ "^\u0019恜Ri\n\u001c6", [ [ "Catala.DefaultCalculus.ty", 1, 2, 1, [ "@query" ], 0, "f9fc150dd19183938eeb34ba6bdbd657" ], [ "Catala.DefaultCalculus.__proj__TArrow__item__tin", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_6c84f3c20063b6c55689598b28b1a4ee" ], 0, "f3d2b8f547abda0782f87d707c869b8d" ], [ "Catala.DefaultCalculus.__proj__TArrow__item__tout", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_6c84f3c20063b6c55689598b28b1a4ee" ], 0, "ae852addd65be90b335b6bb218cd95e5" ], [ "Catala.DefaultCalculus.exp", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "assumption_Catala.DefaultCalculus.lit__uu___haseq", "assumption_Catala.DefaultCalculus.ty__uu___haseq", "assumption_Prims.list__uu___haseq", "equation_Catala.DefaultCalculus.var", "equation_Prims.eqtype", "equation_Prims.nat", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "kinding_Catala.DefaultCalculus.exp@tok", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "9d2a37207e7e44a0aa6f895ac36f1711" ], [ "Catala.DefaultCalculus.__proj__EVar__item__v", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_f7bcdc7958786fcb60dfc7f410094686" ], 0, "05f351ca93ca78b5c20d9328736cafe5" ], [ "Catala.DefaultCalculus.__proj__EApp__item__fn", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_1dc7fa6b1909b346c3b5a4d1713e7f4d" ], 0, "78ec509aeb281285063fdd61420f514c" ], [ "Catala.DefaultCalculus.__proj__EApp__item__arg", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_1dc7fa6b1909b346c3b5a4d1713e7f4d" ], 0, "32f71b14277a31a4820bb616728f3bd2" ], [ "Catala.DefaultCalculus.__proj__EApp__item__tau_arg", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_1dc7fa6b1909b346c3b5a4d1713e7f4d" ], 0, "fd0ed4fe677d8fede0d42bcbc67941cd" ], [ "Catala.DefaultCalculus.__proj__EAbs__item__vty", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_896bdd339800e419f43bc3a1f12b68b5" ], 0, "7826102b160ea54aa1f02dd7f88fa29d" ], [ "Catala.DefaultCalculus.__proj__EAbs__item__body", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_896bdd339800e419f43bc3a1f12b68b5" ], 0, "7075e86600a1b931d7638df53c3d7644" ], [ "Catala.DefaultCalculus.__proj__ELit__item__l", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_6ccee90986879ff2274b72e5bc3434cf" ], 0, "1fb7b5d0d6bbc1c9f454281a01f5d2e5" ], [ "Catala.DefaultCalculus.__proj__EIf__item__test", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_a1447562c281df3bff097b9d339c29e3" ], 0, "e0826990f2bf12b896b259ea7a29ef9c" ], [ "Catala.DefaultCalculus.__proj__EIf__item__btrue", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_a1447562c281df3bff097b9d339c29e3" ], 0, "3e0b50e34c3d0856d8063655fa3c78b9" ], [ "Catala.DefaultCalculus.__proj__EIf__item__bfalse", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_a1447562c281df3bff097b9d339c29e3" ], 0, "abe0700812430ee14bee827a916c4c36" ], [ "Catala.DefaultCalculus.__proj__EDefault__item__exceptions", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_64bbba607bea708c1ff8c3fa0d85aa12" ], 0, "2c8da04378b45ddc9e70997245b3d392" ], [ "Catala.DefaultCalculus.__proj__EDefault__item__just", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_64bbba607bea708c1ff8c3fa0d85aa12" ], 0, "71722c3137aef8a070db92954483c125" ], [ "Catala.DefaultCalculus.__proj__EDefault__item__cons", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_64bbba607bea708c1ff8c3fa0d85aa12" ], 0, "c9b5aa06f3d4f96ce9c2dd3b36b4e95e" ], [ "Catala.DefaultCalculus.__proj__EDefault__item__tau", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_64bbba607bea708c1ff8c3fa0d85aa12" ], 0, "fc5a0984f34fcd69654e5047e1be4a72" ], [ "Catala.DefaultCalculus.is_renaming_prop", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_Catala.DefaultCalculus.var", "equation_Prims.l_Forall", "equation_Prims.nat", "equation_Prims.squash", "equation_Prims.subtype_of", "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "47c120cc648999657f8b75f2e0dbf98d" ], [ "Catala.DefaultCalculus.is_renaming_size", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_1c1d1c6e28a4d07ae30d44381ee0d524" ], 0, "1646f35ef9996dc3507029920875e4cb" ], [ "Catala.DefaultCalculus.increment", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_Catala.DefaultCalculus.var", "equation_Prims.nat", "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "58c826601d51afd33df888b64778cf63" ], [ "Catala.DefaultCalculus.increment_is_renaming", 1, 2, 1, [ "@query", "constructor_distinct_Catala.DefaultCalculus.EVar", "disc_equation_Catala.DefaultCalculus.EVar", "equation_Catala.DefaultCalculus.increment", "equation_Catala.DefaultCalculus.is_renaming_prop", "projection_inverse_BoxBool_proj_0", "projection_inverse_Catala.DefaultCalculus.EVar_v" ], 0, "a33ba95b81f3dfeb49bb013dce518b46" ], [ "Catala.DefaultCalculus.subst", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "Catala.DefaultCalculus_interpretation_Tm_arrow_16e47229fa4f513e4aff966f842aa522", "Catala.DefaultCalculus_interpretation_Tm_arrow_e31a3c19683e8b2fd2b67c21ce8e4ced", "Catala.DefaultCalculus_pretyping_0ccd8e9cc590b3a6d39eb0752f03f688", "Prims_pretyping_ae567c2fb75be05905677af440075565", "binder_x_0ccd8e9cc590b3a6d39eb0752f03f688_1", "binder_x_6c50c515b77925886e3faaa30943f0fb_0", "bool_inversion", "constructor_distinct_Catala.DefaultCalculus.EAbs", "constructor_distinct_Catala.DefaultCalculus.EApp", "constructor_distinct_Catala.DefaultCalculus.EIf", "constructor_distinct_Catala.DefaultCalculus.ELit", "constructor_distinct_Catala.DefaultCalculus.EVar", "data_elim_Catala.DefaultCalculus.EVar", "disc_equation_Catala.DefaultCalculus.EAbs", "disc_equation_Catala.DefaultCalculus.EApp", "disc_equation_Catala.DefaultCalculus.EDefault", "disc_equation_Catala.DefaultCalculus.EIf", "disc_equation_Catala.DefaultCalculus.ELit", "disc_equation_Catala.DefaultCalculus.EVar", "equation_Catala.DefaultCalculus.is_renaming_prop", "equation_Catala.DefaultCalculus.is_renaming_size", "equation_Catala.DefaultCalculus.is_var_size", "equation_Catala.DefaultCalculus.var", "equation_Catala.DefaultCalculus.var_to_exp", "equation_Prims.nat", "equation_Prims.prop", "fuel_guarded_inversion_Catala.DefaultCalculus.exp", "function_token_typing_Catala.DefaultCalculus.subst_abs", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Catala.DefaultCalculus.EAbs_body", "projection_inverse_Catala.DefaultCalculus.EApp_arg", "projection_inverse_Catala.DefaultCalculus.EApp_fn", "projection_inverse_Catala.DefaultCalculus.EDefault_cons", "projection_inverse_Catala.DefaultCalculus.EDefault_exceptions", "projection_inverse_Catala.DefaultCalculus.EDefault_just", "projection_inverse_Catala.DefaultCalculus.EIf_bfalse", "projection_inverse_Catala.DefaultCalculus.EIf_btrue", "projection_inverse_Catala.DefaultCalculus.EIf_test", "projection_inverse_Catala.DefaultCalculus.EVar_v", "refinement_interpretation_Tm_refine_2c7ecebd8a41d0890aab4251b61d6458", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_73f210ca6e0061ed4a3150f69b8f33bf", "refinement_interpretation_Tm_refine_796ea366a949e0b57c08263b6d4daad3", "refinement_interpretation_Tm_refine_829234be963617554f5a7b8433c93f5c", "refinement_interpretation_Tm_refine_bcced13304791c2e1ef0eb3c0488e66c", "subterm_ordering_Catala.DefaultCalculus.EAbs", "subterm_ordering_Catala.DefaultCalculus.EApp", "subterm_ordering_Catala.DefaultCalculus.EDefault", "subterm_ordering_Catala.DefaultCalculus.EIf", "token_correspondence_Catala.DefaultCalculus.subst_abs", "typing_Catala.DefaultCalculus.is_renaming_prop", "typing_Catala.DefaultCalculus.is_renaming_size", "typing_Catala.DefaultCalculus.is_var_size", "typing_Catala.DefaultCalculus.uu___is_EVar", "typing_FStar.StrongExcludedMiddle.strong_excluded_middle", "well-founded-ordering-on-nat" ], 0, "d204a4c04ff4bc41a8e408f2c793af32" ], [ "Catala.DefaultCalculus.subst", 2, 2, 1, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "binder_x_374a7fe1e57403f158e71980a97ecb0e_1", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "equation_Catala.DefaultCalculus.is_var_size", "fuel_guarded_inversion_Prims.list", "function_token_typing_Prims.__cache_version_number__", "int_typing", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "subterm_ordering_Prims.Cons", "typing_Catala.DefaultCalculus.is_var_size", "well-founded-ordering-on-nat" ], 0, "f33db5ddb71da97242c740564a00705e" ], [ "Catala.DefaultCalculus.subst", 3, 2, 1, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "binder_x_6c50c515b77925886e3faaa30943f0fb_0", "binder_x_c7c057bcb1ada4a7fe94b1a061987144_1", "bool_inversion", "constructor_distinct_Catala.DefaultCalculus.EVar", "disc_equation_Catala.DefaultCalculus.EVar", "equation_Catala.DefaultCalculus.increment", "equation_Catala.DefaultCalculus.is_renaming_prop", "equation_Catala.DefaultCalculus.is_renaming_size", "equation_Catala.DefaultCalculus.is_var_size", "equation_Catala.DefaultCalculus.var", "equation_Prims.nat", "equation_Prims.prop", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Catala.DefaultCalculus.EVar_v", "refinement_interpretation_Tm_refine_2c7ecebd8a41d0890aab4251b61d6458", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_73f210ca6e0061ed4a3150f69b8f33bf", "refinement_interpretation_Tm_refine_796ea366a949e0b57c08263b6d4daad3", "typing_Catala.DefaultCalculus.increment", "typing_Catala.DefaultCalculus.is_renaming_prop", "typing_Catala.DefaultCalculus.is_renaming_size", "typing_Catala.DefaultCalculus.is_var_size", "typing_Catala.DefaultCalculus.uu___is_EVar", "typing_FStar.StrongExcludedMiddle.strong_excluded_middle", "well-founded-ordering-on-nat" ], 0, "999f67f38fe11e22b56ff48356f22e05" ], [ "Catala.DefaultCalculus.var_to_exp_beta", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_Catala.DefaultCalculus.var", "equation_Prims.nat", "int_inversion", "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "dfbbef2a7fec7f91a01db5caddc3f504" ], [ "Catala.DefaultCalculus.empty_count_result", 1, 2, 1, [ "@query", "assumption_Catala.DefaultCalculus.exp__uu___haseq" ], 0, "454de250dadf437ce9064f8c2faea487" ], [ "Catala.DefaultCalculus.__proj__OneNonEmpty__item___0", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_73db3433a5536656aa27657eb477efcf" ], 0, "ae7f3ffcfdaa53938d6fe23884ff4317" ], [ "Catala.DefaultCalculus.exceptions_count_result", 1, 2, 1, [ "@query", "assumption_Catala.DefaultCalculus.exp__uu___haseq" ], 0, "3bbdf3db8159f245ce2f2b1c10d6f185" ], [ "Catala.DefaultCalculus.__proj__SomeStep__item___0", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_562b75d472a96c36a24c70375d81f26c" ], 0, "f118d5761b19e05ce48da02ba76c2f6b" ], [ "Catala.DefaultCalculus.empty_count", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "Catala.DefaultCalculus_pretyping_ddbfacc376d73d0ca810e3fd46e827d6", "binder_x_374a7fe1e57403f158e71980a97ecb0e_1", "binder_x_ddbfacc376d73d0ca810e3fd46e827d6_0", "data_typing_intro_Catala.DefaultCalculus.Conflict@tok", "disc_equation_Catala.DefaultCalculus.AllEmpty", "disc_equation_Catala.DefaultCalculus.Conflict", "disc_equation_Catala.DefaultCalculus.OneNonEmpty", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "fuel_guarded_inversion_Catala.DefaultCalculus.empty_count_result", "fuel_guarded_inversion_Prims.list", "proj_equation_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "subterm_ordering_Prims.Cons" ], 0, "f6427a407f48df6b59262b4edde385d8" ], [ "Catala.DefaultCalculus.step_app", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "Catala.DefaultCalculus_pretyping_0ccd8e9cc590b3a6d39eb0752f03f688", "binder_x_0ccd8e9cc590b3a6d39eb0752f03f688_0", "disc_equation_FStar.Pervasives.Native.None", "disc_equation_FStar.Pervasives.Native.Some", "kinding_Catala.DefaultCalculus.exp@tok", "lemma_FStar.Pervasives.invertOption" ], 0, "bc2f87497f995ee90a31614799faef5d" ], [ "Catala.DefaultCalculus.step_app", 2, 2, 1, [ "@query", "kinding_Catala.DefaultCalculus.exp@tok", "lemma_FStar.Pervasives.invertOption" ], 0, "b11c90217682aba8d32a382aa9725984" ], [ "Catala.DefaultCalculus.step_app", 3, 2, 1, [ "@MaxIFuel_assumption", "@query", "Catala.DefaultCalculus_pretyping_0ccd8e9cc590b3a6d39eb0752f03f688", "binder_x_0ccd8e9cc590b3a6d39eb0752f03f688_0", "binder_x_57403813bce408351cc0e70737e314ef_1", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "fuel_guarded_inversion_Prims.list", "projection_inverse_BoxBool_proj_0", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "refinement_interpretation_Tm_refine_adf079fdab7afb98eae06afbf41efee1", "subterm_ordering_Prims.Cons" ], 0, "24f79481280d552251146950686604be" ], [ "Catala.DefaultCalculus.step_app", 4, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.DefaultCalculus.empty_count.fuel_instrumented", "@query", "Catala.DefaultCalculus_pretyping_0ccd8e9cc590b3a6d39eb0752f03f688", "Prims_pretyping_ae567c2fb75be05905677af440075565", "binder_x_0ccd8e9cc590b3a6d39eb0752f03f688_0", "binder_x_57403813bce408351cc0e70737e314ef_1", "constructor_distinct_Catala.DefaultCalculus.AllEmpty", "disc_equation_Catala.DefaultCalculus.AllEmpty", "disc_equation_Catala.DefaultCalculus.Conflict", "disc_equation_Catala.DefaultCalculus.OneNonEmpty", "equality_tok_Catala.DefaultCalculus.AllEmpty@tok", "equation_with_fuel_Catala.DefaultCalculus.empty_count.fuel_instrumented", "fuel_guarded_inversion_Catala.DefaultCalculus.empty_count_result", "function_token_typing_Prims.__cache_version_number__", "int_typing", "kinding_Catala.DefaultCalculus.exp@tok", "lemma_FStar.Pervasives.invertOption", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_adf079fdab7afb98eae06afbf41efee1", "typing_Catala.DefaultCalculus.empty_count", "typing_tok_Catala.DefaultCalculus.AllEmpty@tok", "well-founded-ordering-on-nat" ], 0, "0b662622406376d0a2bd18937e18ed5e" ], [ "Catala.DefaultCalculus.step_app", 5, 2, 1, [ "@MaxIFuel_assumption", "@query", "Catala.DefaultCalculus_pretyping_0ccd8e9cc590b3a6d39eb0752f03f688", "Prims_pretyping_ae567c2fb75be05905677af440075565", "binder_x_0ccd8e9cc590b3a6d39eb0752f03f688_0", "disc_equation_Catala.DefaultCalculus.IllFormed", "disc_equation_Catala.DefaultCalculus.NoStep", "disc_equation_Catala.DefaultCalculus.SomeStep", "disc_equation_FStar.Pervasives.Native.None", "disc_equation_FStar.Pervasives.Native.Some", "fuel_guarded_inversion_Catala.DefaultCalculus.exceptions_count_result", "function_token_typing_Prims.__cache_version_number__", "int_typing", "kinding_Catala.DefaultCalculus.exp@tok", "lemma_FStar.Pervasives.invertOption", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "well-founded-ordering-on-nat" ], 0, "0d237febd87140396125c39c4ddc415b" ], [ "Catala.DefaultCalculus.step_app", 6, 2, 1, [ "@MaxIFuel_assumption", "@query", "Catala.DefaultCalculus_pretyping_0ccd8e9cc590b3a6d39eb0752f03f688", "Catala.DefaultCalculus_pretyping_6aa41574d40712b03e0367a1a3c256b3", "Prims_pretyping_ae567c2fb75be05905677af440075565", "binder_x_0ccd8e9cc590b3a6d39eb0752f03f688_0", "data_typing_intro_Catala.DefaultCalculus.TUnit@tok", "function_token_typing_Prims.__cache_version_number__", "int_typing", "projection_inverse_BoxInt_proj_0", "subterm_ordering_Catala.DefaultCalculus.EApp", "subterm_ordering_Catala.DefaultCalculus.EDefault", "subterm_ordering_Catala.DefaultCalculus.EIf", "well-founded-ordering-on-nat" ], 0, "0cd9555520b3ca27b77b9ee22f77a1a3" ], [ "Catala.DefaultCalculus.extend", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_Catala.DefaultCalculus.var", "equation_Prims.nat", "int_inversion", "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "b4d7124ea3722a753e1998e8e1c6eb80" ], [ "Catala.DefaultCalculus.typing", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "Catala.DefaultCalculus_pretyping_0ccd8e9cc590b3a6d39eb0752f03f688", "Catala.DefaultCalculus_pretyping_6aa41574d40712b03e0367a1a3c256b3", "assumption_Catala.DefaultCalculus.ty__uu___haseq", "assumption_FStar.Pervasives.Native.option__uu___haseq", "binder_x_0ccd8e9cc590b3a6d39eb0752f03f688_1", "data_typing_intro_Catala.DefaultCalculus.TUnit@tok", "kinding_Catala.DefaultCalculus.ty@tok", "subterm_ordering_Catala.DefaultCalculus.EAbs", "subterm_ordering_Catala.DefaultCalculus.EApp", "subterm_ordering_Catala.DefaultCalculus.EDefault", "subterm_ordering_Catala.DefaultCalculus.EIf" ], 0, "0cab940a4adca30ec6c107f4bd65ab7e" ], [ "Catala.DefaultCalculus.typing", 2, 2, 1, [ "@MaxIFuel_assumption", "@query", "binder_x_374a7fe1e57403f158e71980a97ecb0e_1", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "fuel_guarded_inversion_Prims.list", "projection_inverse_BoxBool_proj_0", "subterm_ordering_Prims.Cons" ], 0, "4e3b314f9599171e039bda02fbe32288" ], [ "Catala.DefaultCalculus.is_bool_value_cannot_be_abs", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.DefaultCalculus.typing.fuel_instrumented", "@query", "Catala.DefaultCalculus_pretyping_6aa41574d40712b03e0367a1a3c256b3", "bool_inversion", "constructor_distinct_Catala.DefaultCalculus.TBool", "constructor_distinct_Catala.DefaultCalculus.TUnit", "data_typing_intro_Catala.DefaultCalculus.TUnit@tok", "equality_tok_Catala.DefaultCalculus.TBool@tok", "equality_tok_Catala.DefaultCalculus.TUnit@tok", "equation_Catala.DefaultCalculus.is_value", "equation_with_fuel_Catala.DefaultCalculus.typing.fuel_instrumented", "primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0", "typing_Catala.DefaultCalculus.is_value", "typing_Catala.DefaultCalculus.typing", "typing_tok_Catala.DefaultCalculus.TBool@tok" ], 0, "96fcf67d7e9d68c08815d5b863cc5d75" ], [ "Catala.DefaultCalculus.typing_conserved_by_list_reduction", 1, 2, 1, [ "@MaxFuel_assumption", "@fuel_correspondence_Catala.DefaultCalculus.typing_list.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.typing_list.fuel_instrumented", "@query", "disc_equation_Prims.Cons", "equation_with_fuel_Catala.DefaultCalculus.typing_list.fuel_instrumented", "primitive_Prims.op_AmpAmp", "proj_equation_Prims.Cons_tl", "projection_inverse_BoxBool_proj_0" ], 0, "26ee0e9ab80a19918e4ab06c7aee8d1d" ], [ "Catala.DefaultCalculus.progress", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.DefaultCalculus.step.fuel_instrumented", "@fuel_correspondence_Catala.DefaultCalculus.step_default.fuel_instrumented", "@fuel_correspondence_Catala.DefaultCalculus.typing.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.step.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.step_default.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.typing.fuel_instrumented", "@query", "Catala.DefaultCalculus_interpretation_Tm_arrow_32dd48e99b1b3e0992650610d5f5cce9", "Catala.DefaultCalculus_interpretation_Tm_arrow_8475db58406619dab75f3a7141d50841", "Catala.DefaultCalculus_pretyping_0ccd8e9cc590b3a6d39eb0752f03f688", "Catala.DefaultCalculus_pretyping_6aa41574d40712b03e0367a1a3c256b3", "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Prims_pretyping_ae567c2fb75be05905677af440075565", "binder_x_0ccd8e9cc590b3a6d39eb0752f03f688_0", "binder_x_6aa41574d40712b03e0367a1a3c256b3_1", "bool_inversion", "constructor_distinct_Catala.DefaultCalculus.EApp", "constructor_distinct_Catala.DefaultCalculus.EDefault", "constructor_distinct_Catala.DefaultCalculus.EIf", "constructor_distinct_Catala.DefaultCalculus.TArrow", "constructor_distinct_Catala.DefaultCalculus.TBool", "constructor_distinct_Catala.DefaultCalculus.TUnit", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_FStar.Pervasives.Native.Some", "data_elim_Catala.DefaultCalculus.EVar", "data_typing_intro_Catala.DefaultCalculus.TUnit@tok", "disc_equation_Catala.DefaultCalculus.EApp", "disc_equation_Catala.DefaultCalculus.EDefault", "disc_equation_Catala.DefaultCalculus.EIf", "disc_equation_FStar.Pervasives.Native.None", "disc_equation_FStar.Pervasives.Native.Some", "equality_tok_Catala.DefaultCalculus.TBool@tok", "equality_tok_Catala.DefaultCalculus.TUnit@tok", "equation_Catala.DefaultCalculus.empty", "equation_Catala.DefaultCalculus.is_value", "equation_Catala.DefaultCalculus.var", "equation_FStar.FunctionalExtensionality.feq", "equation_Prims.nat", "equation_with_fuel_Catala.DefaultCalculus.step.fuel_instrumented", "equation_with_fuel_Catala.DefaultCalculus.step_app.fuel_instrumented", "equation_with_fuel_Catala.DefaultCalculus.step_if.fuel_instrumented", "equation_with_fuel_Catala.DefaultCalculus.typing.fuel_instrumented", "fuel_guarded_inversion_Catala.DefaultCalculus.exp", "function_token_typing_Prims.__cache_version_number__", "int_typing", "interpretation_Tm_abs_1df2ad5da40b1dd4a17c31d2cebba95a", "interpretation_Tm_abs_85708d064e5d0dbdd7c749ea62f421af", "kinding_Catala.DefaultCalculus.exp@tok", "lemma_FStar.FunctionalExtensionality.feq_on_domain", "lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Catala.DefaultCalculus.EApp_arg", "projection_inverse_Catala.DefaultCalculus.EApp_fn", "projection_inverse_Catala.DefaultCalculus.EApp_tau_arg", "projection_inverse_Catala.DefaultCalculus.EDefault_cons", "projection_inverse_Catala.DefaultCalculus.EDefault_exceptions", "projection_inverse_Catala.DefaultCalculus.EDefault_just", "projection_inverse_Catala.DefaultCalculus.EDefault_tau", "projection_inverse_Catala.DefaultCalculus.EIf_bfalse", "projection_inverse_Catala.DefaultCalculus.EIf_btrue", "projection_inverse_Catala.DefaultCalculus.EIf_test", "refinement_interpretation_Tm_refine_1f79706984431459041a6f7851223328", "refinement_interpretation_Tm_refine_2aceacac479fb56248306a969addd084", "refinement_interpretation_Tm_refine_bc236faac1238ac3ee32de7f5026c212", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "subterm_ordering_Catala.DefaultCalculus.EApp", "subterm_ordering_Catala.DefaultCalculus.EDefault", "subterm_ordering_Catala.DefaultCalculus.EIf", "token_correspondence_Catala.DefaultCalculus.typing.fuel_instrumented", "typing_Catala.DefaultCalculus.empty", "typing_Catala.DefaultCalculus.is_value", "typing_Catala.DefaultCalculus.step", "typing_Catala.DefaultCalculus.typing", "typing_Tm_abs_1df2ad5da40b1dd4a17c31d2cebba95a", "typing_Tm_abs_85708d064e5d0dbdd7c749ea62f421af", "typing_tok_Catala.DefaultCalculus.TBool@tok", "unit_inversion", "unit_typing", "well-founded-ordering-on-nat" ], 0, "dd491009ff9878ade2d35c8a0b85322d" ], [ "Catala.DefaultCalculus.progress", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.DefaultCalculus.step.fuel_instrumented", "@fuel_correspondence_Catala.DefaultCalculus.step_default.fuel_instrumented", "@fuel_correspondence_Catala.DefaultCalculus.step_exceptions.fuel_instrumented", "@fuel_correspondence_Catala.DefaultCalculus.step_exceptions_left_to_right.fuel_instrumented", "@fuel_correspondence_Catala.DefaultCalculus.typing.fuel_instrumented", "@fuel_correspondence_Catala.DefaultCalculus.typing_list.fuel_instrumented", "@fuel_correspondence_FStar.List.Tot.Base.for_all.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.step_app.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.step_default.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.step_exceptions.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.step_exceptions_left_to_right.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.step_if.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.typing.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.typing_list.fuel_instrumented", "@query", "Catala.DefaultCalculus_interpretation_Tm_arrow_32dd48e99b1b3e0992650610d5f5cce9", "Catala.DefaultCalculus_interpretation_Tm_arrow_5401141756166ef64ba94940663272f3", "Catala.DefaultCalculus_interpretation_Tm_arrow_8475db58406619dab75f3a7141d50841", "Catala.DefaultCalculus_pretyping_0ccd8e9cc590b3a6d39eb0752f03f688", "Catala.DefaultCalculus_pretyping_6228a1bba9fe5ca24a1c0a49c31d0d53", "Catala.DefaultCalculus_pretyping_6aa41574d40712b03e0367a1a3c256b3", "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a", "FStar.List.Tot.Base_interpretation_Tm_arrow_84543425b818e2d10a976186b8e8c250", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Prims_pretyping_ae567c2fb75be05905677af440075565", "binder_x_0ccd8e9cc590b3a6d39eb0752f03f688_0", "binder_x_57403813bce408351cc0e70737e314ef_1", "binder_x_6aa41574d40712b03e0367a1a3c256b3_4", "binder_x_9d898a02527d03c282f289aa9ecae7fc_2", "binder_x_9d898a02527d03c282f289aa9ecae7fc_3", "bool_inversion", "constructor_distinct_Catala.DefaultCalculus.EDefault", "constructor_distinct_Catala.DefaultCalculus.ELit", "constructor_distinct_Catala.DefaultCalculus.IllFormed", "constructor_distinct_Catala.DefaultCalculus.LConflictError", "constructor_distinct_Catala.DefaultCalculus.LEmptyError", "constructor_distinct_Catala.DefaultCalculus.LFalse", "constructor_distinct_Catala.DefaultCalculus.LTrue", "constructor_distinct_Catala.DefaultCalculus.NoStep", "constructor_distinct_Catala.DefaultCalculus.SomeStep", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_FStar.Pervasives.Native.Some", "constructor_distinct_Tm_unit", "data_elim_Catala.DefaultCalculus.ELit", "data_elim_Catala.DefaultCalculus.EVar", "data_typing_intro_Catala.DefaultCalculus.LConflictError@tok", "data_typing_intro_Catala.DefaultCalculus.TUnit@tok", "disc_equation_Catala.DefaultCalculus.ELit", "disc_equation_Catala.DefaultCalculus.IllFormed", "disc_equation_Catala.DefaultCalculus.LConflictError", "disc_equation_Catala.DefaultCalculus.LEmptyError", "disc_equation_Catala.DefaultCalculus.LFalse", "disc_equation_Catala.DefaultCalculus.LTrue", "disc_equation_Catala.DefaultCalculus.NoStep", "disc_equation_Catala.DefaultCalculus.SomeStep", "disc_equation_FStar.Pervasives.Native.None", "disc_equation_FStar.Pervasives.Native.Some", "equality_tok_Catala.DefaultCalculus.IllFormed@tok", "equality_tok_Catala.DefaultCalculus.LConflictError@tok", "equality_tok_Catala.DefaultCalculus.LEmptyError@tok", "equality_tok_Catala.DefaultCalculus.LFalse@tok", "equality_tok_Catala.DefaultCalculus.LTrue@tok", "equality_tok_Catala.DefaultCalculus.NoStep@tok", "equality_tok_Catala.DefaultCalculus.TBool@tok", "equation_Catala.DefaultCalculus.empty", "equation_Catala.DefaultCalculus.is_value", "equation_Catala.DefaultCalculus.var", "equation_FStar.FunctionalExtensionality.feq", "equation_Prims.nat", "equation_with_fuel_Catala.DefaultCalculus.step.fuel_instrumented", "equation_with_fuel_Catala.DefaultCalculus.step_default.fuel_instrumented", "equation_with_fuel_Catala.DefaultCalculus.step_exceptions.fuel_instrumented", "equation_with_fuel_Catala.DefaultCalculus.typing.fuel_instrumented", "fuel_guarded_inversion_Catala.DefaultCalculus.exceptions_count_result", "fuel_guarded_inversion_Catala.DefaultCalculus.exp", "fuel_guarded_inversion_Catala.DefaultCalculus.lit", "fuel_guarded_inversion_FStar.Pervasives.Native.option", "function_token_typing_Catala.DefaultCalculus.is_value", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "interpretation_Tm_abs_1df2ad5da40b1dd4a17c31d2cebba95a", "interpretation_Tm_abs_85708d064e5d0dbdd7c749ea62f421af", "kinding_Catala.DefaultCalculus.exp@tok", "lemma_FStar.FunctionalExtensionality.feq_on_domain", "lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "proj_equation_Catala.DefaultCalculus.ELit_l", "proj_equation_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Catala.DefaultCalculus.EDefault_cons", "projection_inverse_Catala.DefaultCalculus.EDefault_exceptions", "projection_inverse_Catala.DefaultCalculus.EDefault_just", "projection_inverse_Catala.DefaultCalculus.EDefault_tau", "projection_inverse_Catala.DefaultCalculus.ELit_l", "projection_inverse_Catala.DefaultCalculus.SomeStep__0", "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_2aceacac479fb56248306a969addd084", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8adbef10d645a4d9aac0702fe91040be", "refinement_interpretation_Tm_refine_94ff508dba60a98364daca65da372e14", "refinement_interpretation_Tm_refine_adf079fdab7afb98eae06afbf41efee1", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "token_correspondence_Catala.DefaultCalculus.typing.fuel_instrumented", "token_correspondence_Catala.DefaultCalculus.typing_list.fuel_instrumented", "typing_Catala.DefaultCalculus.empty", "typing_Catala.DefaultCalculus.step_default", "typing_Catala.DefaultCalculus.step_exceptions", "typing_Catala.DefaultCalculus.step_exceptions_left_to_right", "typing_Catala.DefaultCalculus.typing", "typing_FStar.List.Tot.Base.for_all", "typing_Tm_abs_1df2ad5da40b1dd4a17c31d2cebba95a", "typing_Tm_abs_85708d064e5d0dbdd7c749ea62f421af", "typing_tok_Catala.DefaultCalculus.TBool@tok", "unit_inversion", "unit_typing", "well-founded-ordering-on-nat" ], 0, "679a7f3e7e17536eec0ea6f54aff9c71" ], [ "Catala.DefaultCalculus.progress", 3, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.DefaultCalculus.step.fuel_instrumented", "@fuel_correspondence_Catala.DefaultCalculus.step_exceptions_left_to_right.fuel_instrumented", "@fuel_correspondence_Catala.DefaultCalculus.typing.fuel_instrumented", "@fuel_correspondence_Catala.DefaultCalculus.typing_list.fuel_instrumented", "@fuel_correspondence_FStar.List.Tot.Base.for_all.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.step.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.step_exceptions_left_to_right.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.typing.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.typing_list.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.for_all.fuel_instrumented", "@query", "Catala.DefaultCalculus_interpretation_Tm_arrow_5401141756166ef64ba94940663272f3", "FStar.List.Tot.Base_interpretation_Tm_arrow_84543425b818e2d10a976186b8e8c250", "binder_x_0ccd8e9cc590b3a6d39eb0752f03f688_0", "binder_x_57403813bce408351cc0e70737e314ef_1", "binder_x_6aa41574d40712b03e0367a1a3c256b3_4", "binder_x_9d898a02527d03c282f289aa9ecae7fc_2", "binder_x_9d898a02527d03c282f289aa9ecae7fc_3", "bool_inversion", "constructor_distinct_Catala.DefaultCalculus.EDefault", "constructor_distinct_Catala.DefaultCalculus.LConflictError", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_FStar.Pervasives.Native.Some", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "constructor_distinct_Tm_unit", "data_elim_Prims.Cons", "disc_equation_FStar.Pervasives.Native.Some", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "equality_tok_Catala.DefaultCalculus.LConflictError@tok", "equation_Catala.DefaultCalculus.c_err", "equation_Catala.DefaultCalculus.empty", "equation_Catala.DefaultCalculus.is_value", "equation_with_fuel_Catala.DefaultCalculus.step_exceptions_left_to_right.fuel_instrumented", "equation_with_fuel_Catala.DefaultCalculus.typing.fuel_instrumented", "equation_with_fuel_Catala.DefaultCalculus.typing_list.fuel_instrumented", "equation_with_fuel_FStar.List.Tot.Base.for_all.fuel_instrumented", "fuel_guarded_inversion_Catala.DefaultCalculus.exp", "fuel_guarded_inversion_FStar.Pervasives.Native.option", "fuel_guarded_inversion_Prims.list", "function_token_typing_Catala.DefaultCalculus.is_value", "kinding_Catala.DefaultCalculus.exp@tok", "primitive_Prims.op_AmpAmp", "projection_inverse_BoxBool_proj_0", "projection_inverse_Catala.DefaultCalculus.EDefault_cons", "projection_inverse_Catala.DefaultCalculus.EDefault_exceptions", "projection_inverse_Catala.DefaultCalculus.EDefault_just", "projection_inverse_Catala.DefaultCalculus.EDefault_tau", "projection_inverse_FStar.Pervasives.Native.Some_v", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a", "refinement_interpretation_Tm_refine_2aceacac479fb56248306a969addd084", "refinement_interpretation_Tm_refine_8adbef10d645a4d9aac0702fe91040be", "refinement_interpretation_Tm_refine_94ff508dba60a98364daca65da372e14", "refinement_interpretation_Tm_refine_adf079fdab7afb98eae06afbf41efee1", "subterm_ordering_Prims.Cons", "token_correspondence_Catala.DefaultCalculus.is_value", "token_correspondence_Catala.DefaultCalculus.typing.fuel_instrumented", "token_correspondence_Catala.DefaultCalculus.typing_list.fuel_instrumented", "typing_Catala.DefaultCalculus.empty", "typing_Catala.DefaultCalculus.step_exceptions_left_to_right", "typing_Catala.DefaultCalculus.typing_list", "typing_FStar.List.Tot.Base.for_all" ], 0, "08a419c32cc4a72f098d5ba10436fdfc" ], [ "Catala.DefaultCalculus.empty_count_preserves_type", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.DefaultCalculus.empty_count.fuel_instrumented", "@fuel_correspondence_Catala.DefaultCalculus.typing.fuel_instrumented", "@fuel_correspondence_Catala.DefaultCalculus.typing_list.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.empty_count.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.typing.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.typing_list.fuel_instrumented", "@query", "Catala.DefaultCalculus_pretyping_ddbfacc376d73d0ca810e3fd46e827d6", "binder_x_374a7fe1e57403f158e71980a97ecb0e_1", "binder_x_5fb06af9e7383e6ae83424b64f7b9e82_2", "binder_x_6aa41574d40712b03e0367a1a3c256b3_3", "binder_x_ddbfacc376d73d0ca810e3fd46e827d6_0", "bool_inversion", "constructor_distinct_Catala.DefaultCalculus.AllEmpty", "constructor_distinct_Catala.DefaultCalculus.Conflict", "constructor_distinct_Catala.DefaultCalculus.ELit", "constructor_distinct_Catala.DefaultCalculus.LEmptyError", "constructor_distinct_Catala.DefaultCalculus.OneNonEmpty", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "constructor_distinct_Tm_unit", "data_elim_Catala.DefaultCalculus.OneNonEmpty", "data_typing_intro_Catala.DefaultCalculus.Conflict@tok", "disc_equation_Catala.DefaultCalculus.AllEmpty", "disc_equation_Catala.DefaultCalculus.Conflict", "disc_equation_Catala.DefaultCalculus.ELit", "disc_equation_Catala.DefaultCalculus.LEmptyError", "disc_equation_Catala.DefaultCalculus.OneNonEmpty", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "equality_tok_Catala.DefaultCalculus.AllEmpty@tok", "equality_tok_Catala.DefaultCalculus.Conflict@tok", "equality_tok_Catala.DefaultCalculus.LEmptyError@tok", "equation_with_fuel_Catala.DefaultCalculus.empty_count.fuel_instrumented", "equation_with_fuel_Catala.DefaultCalculus.typing.fuel_instrumented", "equation_with_fuel_Catala.DefaultCalculus.typing_list.fuel_instrumented", "fuel_guarded_inversion_Catala.DefaultCalculus.empty_count_result", "primitive_Prims.op_AmpAmp", "proj_equation_Catala.DefaultCalculus.ELit_l", "proj_equation_FStar.Pervasives.Native.Mktuple2__1", "proj_equation_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_BoxBool_proj_0", "projection_inverse_Catala.DefaultCalculus.ELit_l", "projection_inverse_Catala.DefaultCalculus.OneNonEmpty__0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a", "subterm_ordering_Prims.Cons", "token_correspondence_Catala.DefaultCalculus.typing.fuel_instrumented", "token_correspondence_Catala.DefaultCalculus.typing_list.fuel_instrumented", "typing_Catala.DefaultCalculus.empty_count", "typing_Catala.DefaultCalculus.typing", "typing_Catala.DefaultCalculus.typing_list", "typing_tok_Catala.DefaultCalculus.AllEmpty@tok", "typing_tok_Catala.DefaultCalculus.Conflict@tok", "unit_inversion", "unit_typing" ], 0, "244f9100ad5c28fa85f738e2670fd162" ], [ "Catala.DefaultCalculus.substitution_extensionnal", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.DefaultCalculus.subst.fuel_instrumented", "@fuel_correspondence_Catala.DefaultCalculus.subst_abs.fuel_instrumented", "@fuel_correspondence_Catala.DefaultCalculus.subst_list.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.subst.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.subst_list.fuel_instrumented", "@query", "Catala.DefaultCalculus_pretyping_0ccd8e9cc590b3a6d39eb0752f03f688", "Prims_pretyping_ae567c2fb75be05905677af440075565", "binder_x_0ccd8e9cc590b3a6d39eb0752f03f688_2", "binder_x_458e1207db65a065f90af5aa9bc6edd7_1", "binder_x_6c50c515b77925886e3faaa30943f0fb_0", "constructor_distinct_Catala.DefaultCalculus.EApp", "constructor_distinct_Catala.DefaultCalculus.EDefault", "constructor_distinct_Catala.DefaultCalculus.EIf", "constructor_distinct_Catala.DefaultCalculus.ELit", "constructor_distinct_Catala.DefaultCalculus.EVar", "disc_equation_Catala.DefaultCalculus.EAbs", "disc_equation_Catala.DefaultCalculus.EApp", "disc_equation_Catala.DefaultCalculus.EDefault", "disc_equation_Catala.DefaultCalculus.EIf", "disc_equation_Catala.DefaultCalculus.ELit", "disc_equation_Catala.DefaultCalculus.EVar", "equation_Catala.DefaultCalculus.var", "equation_FStar.FunctionalExtensionality.feq", "equation_Prims.nat", "equation_with_fuel_Catala.DefaultCalculus.subst.fuel_instrumented", "equation_with_fuel_Catala.DefaultCalculus.subst_abs.fuel_instrumented", "fuel_guarded_inversion_Catala.DefaultCalculus.exp", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Catala.DefaultCalculus.EApp_arg", "projection_inverse_Catala.DefaultCalculus.EApp_fn", "projection_inverse_Catala.DefaultCalculus.EApp_tau_arg", "projection_inverse_Catala.DefaultCalculus.EDefault_cons", "projection_inverse_Catala.DefaultCalculus.EDefault_exceptions", "projection_inverse_Catala.DefaultCalculus.EDefault_just", "projection_inverse_Catala.DefaultCalculus.EDefault_tau", "projection_inverse_Catala.DefaultCalculus.EIf_bfalse", "projection_inverse_Catala.DefaultCalculus.EIf_btrue", "projection_inverse_Catala.DefaultCalculus.EIf_test", "projection_inverse_Catala.DefaultCalculus.ELit_l", "projection_inverse_Catala.DefaultCalculus.EVar_v", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_e34d62365b53d6f78f1144ed17941a7b", "subterm_ordering_Catala.DefaultCalculus.EAbs", "subterm_ordering_Catala.DefaultCalculus.EApp", "subterm_ordering_Catala.DefaultCalculus.EDefault", "subterm_ordering_Catala.DefaultCalculus.EIf", "token_correspondence_Catala.DefaultCalculus.subst_abs", "true_interp" ], 0, "988376e56f3be5f5faa5177a5f4bce4b" ], [ "Catala.DefaultCalculus.substitution_extensionnal", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.DefaultCalculus.subst.fuel_instrumented", "@fuel_correspondence_Catala.DefaultCalculus.subst_list.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.subst.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.subst_list.fuel_instrumented", "@query", "binder_x_374a7fe1e57403f158e71980a97ecb0e_2", "binder_x_458e1207db65a065f90af5aa9bc6edd7_1", "binder_x_6c50c515b77925886e3faaa30943f0fb_0", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "equation_with_fuel_Catala.DefaultCalculus.subst_list.fuel_instrumented", "fuel_guarded_inversion_Prims.list", "projection_inverse_BoxBool_proj_0", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a", "refinement_interpretation_Tm_refine_e34d62365b53d6f78f1144ed17941a7b", "subterm_ordering_Prims.Cons" ], 0, "9fccb768658c208db732cb784b5ae99a" ], [ "Catala.DefaultCalculus.subst_typing", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.squash", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "a9581b31b098f8c6ed0c28a5af28af64" ], [ "Catala.DefaultCalculus.substitution_preserves_typing", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.DefaultCalculus.subst.fuel_instrumented", "@fuel_correspondence_Catala.DefaultCalculus.subst_abs.fuel_instrumented", "@fuel_correspondence_Catala.DefaultCalculus.subst_list.fuel_instrumented", "@fuel_correspondence_Catala.DefaultCalculus.typing.fuel_instrumented", "@fuel_correspondence_Catala.DefaultCalculus.typing_list.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.subst.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.subst_abs.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.subst_list.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.typing.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.typing_list.fuel_instrumented", "@query", "Catala.DefaultCalculus_interpretation_Tm_arrow_16e47229fa4f513e4aff966f842aa522", "Catala.DefaultCalculus_interpretation_Tm_arrow_32dd48e99b1b3e0992650610d5f5cce9", "Catala.DefaultCalculus_interpretation_Tm_arrow_5153a86c3b84f2f129d4da674d5d28c1", "Catala.DefaultCalculus_interpretation_Tm_arrow_8475db58406619dab75f3a7141d50841", "Catala.DefaultCalculus_pretyping_0ccd8e9cc590b3a6d39eb0752f03f688", "Catala.DefaultCalculus_pretyping_6aa41574d40712b03e0367a1a3c256b3", "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Prims_pretyping_ae567c2fb75be05905677af440075565", "assumption_Catala.DefaultCalculus.ty__uu___haseq", "binder_x_0ccd8e9cc590b3a6d39eb0752f03f688_1", "binder_x_5fb06af9e7383e6ae83424b64f7b9e82_0", "binder_x_5fb06af9e7383e6ae83424b64f7b9e82_4", "binder_x_6aa41574d40712b03e0367a1a3c256b3_2", "binder_x_6c50c515b77925886e3faaa30943f0fb_3", "bool_inversion", "bool_typing", "constructor_distinct_Catala.DefaultCalculus.EAbs", "constructor_distinct_Catala.DefaultCalculus.EApp", "constructor_distinct_Catala.DefaultCalculus.EDefault", "constructor_distinct_Catala.DefaultCalculus.EIf", "constructor_distinct_Catala.DefaultCalculus.ELit", "constructor_distinct_Catala.DefaultCalculus.EVar", "constructor_distinct_Catala.DefaultCalculus.TArrow", "constructor_distinct_FStar.Pervasives.Native.Some", "data_elim_Catala.DefaultCalculus.EVar", "data_elim_FStar.Pervasives.Native.Some", "data_typing_intro_Catala.DefaultCalculus.TUnit@tok", "disc_equation_Catala.DefaultCalculus.EAbs", "disc_equation_Catala.DefaultCalculus.EApp", "disc_equation_Catala.DefaultCalculus.EDefault", "disc_equation_Catala.DefaultCalculus.EIf", "disc_equation_Catala.DefaultCalculus.ELit", "disc_equation_Catala.DefaultCalculus.EVar", "disc_equation_Catala.DefaultCalculus.TArrow", "disc_equation_FStar.Pervasives.Native.Some", "equality_tok_Catala.DefaultCalculus.TBool@tok", "equation_Catala.DefaultCalculus.env", "equation_Catala.DefaultCalculus.extend", "equation_Catala.DefaultCalculus.increment", "equation_Catala.DefaultCalculus.is_renaming_prop", "equation_Catala.DefaultCalculus.is_renaming_size", "equation_Catala.DefaultCalculus.is_var_size", "equation_Catala.DefaultCalculus.var", "equation_Catala.DefaultCalculus.var_to_exp", "equation_FStar.FunctionalExtensionality.feq", "equation_FStar.FunctionalExtensionality.restricted_t", "equation_Prims.nat", "equation_Prims.prop", "equation_with_fuel_Catala.DefaultCalculus.subst.fuel_instrumented", "equation_with_fuel_Catala.DefaultCalculus.subst_abs.fuel_instrumented", "equation_with_fuel_Catala.DefaultCalculus.subst_list.fuel_instrumented", "equation_with_fuel_Catala.DefaultCalculus.typing.fuel_instrumented", "equation_with_fuel_Catala.DefaultCalculus.typing_list.fuel_instrumented", "fuel_guarded_inversion_Catala.DefaultCalculus.exp", "fuel_guarded_inversion_Catala.DefaultCalculus.lit", "fuel_guarded_inversion_FStar.Pervasives.Native.option", "fuel_token_correspondence_Catala.DefaultCalculus.subst_abs.fuel_instrumented_token", "function_token_typing_Catala.DefaultCalculus.extend", "function_token_typing_Catala.DefaultCalculus.subst_abs", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "interpretation_Tm_abs_1df2ad5da40b1dd4a17c31d2cebba95a", "interpretation_Tm_abs_9b0fb98b88819d883b74246421860dc1", "lemma_Catala.DefaultCalculus.substitution_extensionnal", "lemma_FStar.FunctionalExtensionality.feq_on_domain", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction", "primitive_Prims.op_disEquality", "proj_equation_FStar.Pervasives.Native.Some_v", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Catala.DefaultCalculus.EAbs_body", "projection_inverse_Catala.DefaultCalculus.EAbs_vty", "projection_inverse_Catala.DefaultCalculus.EApp_arg", "projection_inverse_Catala.DefaultCalculus.EApp_fn", "projection_inverse_Catala.DefaultCalculus.EApp_tau_arg", "projection_inverse_Catala.DefaultCalculus.EDefault_cons", "projection_inverse_Catala.DefaultCalculus.EDefault_exceptions", "projection_inverse_Catala.DefaultCalculus.EDefault_just", "projection_inverse_Catala.DefaultCalculus.EDefault_tau", "projection_inverse_Catala.DefaultCalculus.EIf_bfalse", "projection_inverse_Catala.DefaultCalculus.EIf_btrue", "projection_inverse_Catala.DefaultCalculus.EIf_test", "projection_inverse_Catala.DefaultCalculus.ELit_l", "projection_inverse_Catala.DefaultCalculus.EVar_v", "projection_inverse_Catala.DefaultCalculus.TArrow_tin", "projection_inverse_Catala.DefaultCalculus.TArrow_tout", "projection_inverse_FStar.Pervasives.Native.Some_a", "projection_inverse_FStar.Pervasives.Native.Some_v", "refinement_interpretation_Tm_refine_2c7ecebd8a41d0890aab4251b61d6458", "refinement_interpretation_Tm_refine_4572a4f2c61a47ef86084a21730a7db0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_73f210ca6e0061ed4a3150f69b8f33bf", "refinement_interpretation_Tm_refine_796ea366a949e0b57c08263b6d4daad3", "refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e", "refinement_interpretation_Tm_refine_bcced13304791c2e1ef0eb3c0488e66c", "refinement_interpretation_Tm_refine_d67758a13faa7f83563fc253808b2c51", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "subterm_ordering_Catala.DefaultCalculus.EAbs", "subterm_ordering_Catala.DefaultCalculus.EApp", "subterm_ordering_Catala.DefaultCalculus.EDefault", "subterm_ordering_Catala.DefaultCalculus.EIf", "token_correspondence_Catala.DefaultCalculus.subst_abs", "token_correspondence_Catala.DefaultCalculus.subst_abs.fuel_instrumented", "token_correspondence_Catala.DefaultCalculus.typing.fuel_instrumented", "token_correspondence_Catala.DefaultCalculus.typing_list.fuel_instrumented", "typing_Catala.DefaultCalculus.extend", "typing_Catala.DefaultCalculus.increment", "typing_Catala.DefaultCalculus.is_renaming_prop", "typing_Catala.DefaultCalculus.is_renaming_size", "typing_Catala.DefaultCalculus.is_var_size", "typing_Catala.DefaultCalculus.subst", "typing_Catala.DefaultCalculus.subst_abs", "typing_Catala.DefaultCalculus.subst_list", "typing_Catala.DefaultCalculus.typing", "typing_Catala.DefaultCalculus.typing_list", "typing_Catala.DefaultCalculus.uu___is_EVar", "typing_FStar.StrongExcludedMiddle.strong_excluded_middle", "typing_Tm_abs_1df2ad5da40b1dd4a17c31d2cebba95a", "typing_Tm_abs_9b0fb98b88819d883b74246421860dc1", "typing_tok_Catala.DefaultCalculus.TBool@tok", "unit_inversion", "unit_typing", "well-founded-ordering-on-nat" ], 0, "17d841d14a1131d163065fbd7aabaaba" ], [ "Catala.DefaultCalculus.substitution_preserves_typing", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.DefaultCalculus.subst.fuel_instrumented", "@fuel_correspondence_Catala.DefaultCalculus.subst_list.fuel_instrumented", "@fuel_correspondence_Catala.DefaultCalculus.typing.fuel_instrumented", "@fuel_correspondence_Catala.DefaultCalculus.typing_list.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.subst.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.subst_list.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.typing.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.typing_list.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "binder_x_374a7fe1e57403f158e71980a97ecb0e_1", "binder_x_5fb06af9e7383e6ae83424b64f7b9e82_0", "binder_x_5fb06af9e7383e6ae83424b64f7b9e82_4", "binder_x_6aa41574d40712b03e0367a1a3c256b3_2", "binder_x_6c50c515b77925886e3faaa30943f0fb_3", "bool_inversion", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "constructor_distinct_Tm_unit", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "equation_Catala.DefaultCalculus.is_var_size", "equation_with_fuel_Catala.DefaultCalculus.subst.fuel_instrumented", "equation_with_fuel_Catala.DefaultCalculus.subst_list.fuel_instrumented", "equation_with_fuel_Catala.DefaultCalculus.typing.fuel_instrumented", "equation_with_fuel_Catala.DefaultCalculus.typing_list.fuel_instrumented", "function_token_typing_Prims.__cache_version_number__", "int_typing", "primitive_Prims.op_AmpAmp", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a", "refinement_interpretation_Tm_refine_4572a4f2c61a47ef86084a21730a7db0", "subterm_ordering_Prims.Cons", "token_correspondence_Catala.DefaultCalculus.typing.fuel_instrumented", "token_correspondence_Catala.DefaultCalculus.typing_list.fuel_instrumented", "typing_Catala.DefaultCalculus.is_var_size", "typing_Catala.DefaultCalculus.subst", "typing_Catala.DefaultCalculus.subst_list", "typing_Catala.DefaultCalculus.typing", "typing_Catala.DefaultCalculus.typing_list", "well-founded-ordering-on-nat" ], 0, "b393907a80bc0e092e77f702ffaf264a" ], [ "Catala.DefaultCalculus.preservation", 1, 3, 1, [ "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.l_and", "equation_Prims.squash", "l_and-interp", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "2caf5bf722b94a214563c4b58dfd0592" ], [ "Catala.DefaultCalculus.preservation", 2, 3, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.DefaultCalculus.empty_count.fuel_instrumented", "@fuel_correspondence_Catala.DefaultCalculus.step.fuel_instrumented", "@fuel_correspondence_Catala.DefaultCalculus.step_exceptions_left_to_right.fuel_instrumented", "@fuel_correspondence_Catala.DefaultCalculus.subst.fuel_instrumented", "@fuel_correspondence_Catala.DefaultCalculus.typing.fuel_instrumented", "@fuel_correspondence_Catala.DefaultCalculus.typing_list.fuel_instrumented", "@fuel_correspondence_FStar.List.Tot.Base.for_all.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.step.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.step_app.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.step_default.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.step_exceptions_left_to_right.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.step_if.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.typing.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.typing_list.fuel_instrumented", "@query", "Catala.DefaultCalculus_interpretation_Tm_arrow_0d43cd04dcb6adc76343f25ff3f92639", "Catala.DefaultCalculus_interpretation_Tm_arrow_16e47229fa4f513e4aff966f842aa522", "Catala.DefaultCalculus_interpretation_Tm_arrow_32dd48e99b1b3e0992650610d5f5cce9", "Catala.DefaultCalculus_interpretation_Tm_arrow_5401141756166ef64ba94940663272f3", "Catala.DefaultCalculus_interpretation_Tm_arrow_8475db58406619dab75f3a7141d50841", "Catala.DefaultCalculus_interpretation_Tm_arrow_89d0b3d44c0d7d897277e5ab0495686d", "Catala.DefaultCalculus_pretyping_0ccd8e9cc590b3a6d39eb0752f03f688", "Catala.DefaultCalculus_pretyping_287308be9a2dd6fe272526e35f960e02", "Catala.DefaultCalculus_pretyping_6aa41574d40712b03e0367a1a3c256b3", "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a", "FStar.List.Tot.Base_interpretation_Tm_arrow_84543425b818e2d10a976186b8e8c250", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def", "binder_x_0ccd8e9cc590b3a6d39eb0752f03f688_0", "binder_x_6aa41574d40712b03e0367a1a3c256b3_1", "bool_inversion", "bool_typing", "constructor_distinct_Catala.DefaultCalculus.AllEmpty", "constructor_distinct_Catala.DefaultCalculus.Conflict", "constructor_distinct_Catala.DefaultCalculus.EAbs", "constructor_distinct_Catala.DefaultCalculus.EApp", "constructor_distinct_Catala.DefaultCalculus.EDefault", "constructor_distinct_Catala.DefaultCalculus.EIf", "constructor_distinct_Catala.DefaultCalculus.ELit", "constructor_distinct_Catala.DefaultCalculus.EVar", "constructor_distinct_Catala.DefaultCalculus.IllFormed", "constructor_distinct_Catala.DefaultCalculus.LConflictError", "constructor_distinct_Catala.DefaultCalculus.LEmptyError", "constructor_distinct_Catala.DefaultCalculus.LTrue", "constructor_distinct_Catala.DefaultCalculus.NoStep", "constructor_distinct_Catala.DefaultCalculus.OneNonEmpty", "constructor_distinct_Catala.DefaultCalculus.SomeStep", "constructor_distinct_Catala.DefaultCalculus.TArrow", "constructor_distinct_Catala.DefaultCalculus.TBool", "constructor_distinct_Catala.DefaultCalculus.TUnit", "constructor_distinct_Catala.DefaultCalculus.exceptions_count_result", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_FStar.Pervasives.Native.Some", "constructor_distinct_Prims.unit", "constructor_distinct_Tm_unit", "data_elim_Catala.DefaultCalculus.EVar", "data_elim_FStar.Pervasives.Native.Some", "data_typing_intro_Catala.DefaultCalculus.TArrow@tok", "data_typing_intro_Catala.DefaultCalculus.TUnit@tok", "disc_equation_Catala.DefaultCalculus.AllEmpty", "disc_equation_Catala.DefaultCalculus.Conflict", "disc_equation_Catala.DefaultCalculus.EAbs", "disc_equation_Catala.DefaultCalculus.EApp", "disc_equation_Catala.DefaultCalculus.EDefault", "disc_equation_Catala.DefaultCalculus.EIf", "disc_equation_Catala.DefaultCalculus.ELit", "disc_equation_Catala.DefaultCalculus.EVar", "disc_equation_Catala.DefaultCalculus.LConflictError", "disc_equation_Catala.DefaultCalculus.LEmptyError", "disc_equation_Catala.DefaultCalculus.LTrue", "disc_equation_Catala.DefaultCalculus.OneNonEmpty", "disc_equation_FStar.Pervasives.Native.None", "disc_equation_FStar.Pervasives.Native.Some", "disc_equation_Prims.Nil", "equality_tok_Catala.DefaultCalculus.AllEmpty@tok", "equality_tok_Catala.DefaultCalculus.Conflict@tok", "equality_tok_Catala.DefaultCalculus.IllFormed@tok", "equality_tok_Catala.DefaultCalculus.LConflictError@tok", "equality_tok_Catala.DefaultCalculus.LEmptyError@tok", "equality_tok_Catala.DefaultCalculus.LTrue@tok", "equality_tok_Catala.DefaultCalculus.NoStep@tok", "equality_tok_Catala.DefaultCalculus.TBool@tok", "equality_tok_Catala.DefaultCalculus.TUnit@tok", "equation_Catala.DefaultCalculus.c_err", "equation_Catala.DefaultCalculus.e_err", "equation_Catala.DefaultCalculus.empty", "equation_Catala.DefaultCalculus.env", "equation_Catala.DefaultCalculus.extend", "equation_Catala.DefaultCalculus.is_value", "equation_Catala.DefaultCalculus.var", "equation_Catala.DefaultCalculus.var_to_exp", "equation_Catala.DefaultCalculus.var_to_exp_beta", "equation_FStar.FunctionalExtensionality.feq", "equation_FStar.FunctionalExtensionality.restricted_t", "equation_Prims.l_and", "equation_Prims.nat", "equation_Prims.squash", "equation_with_fuel_Catala.DefaultCalculus.empty_count.fuel_instrumented", "equation_with_fuel_Catala.DefaultCalculus.step.fuel_instrumented", "equation_with_fuel_Catala.DefaultCalculus.step_app.fuel_instrumented", "equation_with_fuel_Catala.DefaultCalculus.step_default.fuel_instrumented", "equation_with_fuel_Catala.DefaultCalculus.step_exceptions.fuel_instrumented", "equation_with_fuel_Catala.DefaultCalculus.step_exceptions_left_to_right.fuel_instrumented", "equation_with_fuel_Catala.DefaultCalculus.step_if.fuel_instrumented", "equation_with_fuel_Catala.DefaultCalculus.typing.fuel_instrumented", "equation_with_fuel_Catala.DefaultCalculus.typing_list.fuel_instrumented", "equation_with_fuel_FStar.List.Tot.Base.for_all.fuel_instrumented", "fuel_guarded_inversion_Catala.DefaultCalculus.exp", "fuel_guarded_inversion_Catala.DefaultCalculus.lit", "fuel_guarded_inversion_FStar.Pervasives.Native.option", "fuel_guarded_inversion_Prims.list", "function_token_typing_Catala.DefaultCalculus.extend", "function_token_typing_Catala.DefaultCalculus.is_value", "function_token_typing_Catala.DefaultCalculus.var_to_exp_beta", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "interpretation_Tm_abs_1df2ad5da40b1dd4a17c31d2cebba95a", "interpretation_Tm_abs_85708d064e5d0dbdd7c749ea62f421af", "interpretation_Tm_abs_88a3eeb445d1bcada942dc04cac3e8d7", "interpretation_Tm_abs_9b0fb98b88819d883b74246421860dc1", "kinding_Catala.DefaultCalculus.exp@tok", "l_and-interp", "lemma_FStar.FunctionalExtensionality.feq_on_domain", "lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_Negation", "proj_equation_Catala.DefaultCalculus.ELit_l", "proj_equation_FStar.Pervasives.Native.Some_v", "projection_inverse_BoxBool_proj_0", "projection_inverse_Catala.DefaultCalculus.EAbs_body", "projection_inverse_Catala.DefaultCalculus.EAbs_vty", "projection_inverse_Catala.DefaultCalculus.EApp_arg", "projection_inverse_Catala.DefaultCalculus.EApp_fn", "projection_inverse_Catala.DefaultCalculus.EApp_tau_arg", "projection_inverse_Catala.DefaultCalculus.EDefault_cons", "projection_inverse_Catala.DefaultCalculus.EDefault_exceptions", "projection_inverse_Catala.DefaultCalculus.EDefault_just", "projection_inverse_Catala.DefaultCalculus.EDefault_tau", "projection_inverse_Catala.DefaultCalculus.EIf_bfalse", "projection_inverse_Catala.DefaultCalculus.EIf_btrue", "projection_inverse_Catala.DefaultCalculus.EIf_test", "projection_inverse_Catala.DefaultCalculus.ELit_l", "projection_inverse_Catala.DefaultCalculus.EVar_v", "projection_inverse_Catala.DefaultCalculus.OneNonEmpty__0", "projection_inverse_Catala.DefaultCalculus.SomeStep__0", "projection_inverse_Catala.DefaultCalculus.TArrow_tin", "projection_inverse_Catala.DefaultCalculus.TArrow_tout", "projection_inverse_FStar.Pervasives.Native.Some_v", "refinement_interpretation_Tm_refine_1f79706984431459041a6f7851223328", "refinement_interpretation_Tm_refine_2aceacac479fb56248306a969addd084", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_4572a4f2c61a47ef86084a21730a7db0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6ccee90986879ff2274b72e5bc3434cf", "refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e", "refinement_interpretation_Tm_refine_8adbef10d645a4d9aac0702fe91040be", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "subterm_ordering_Catala.DefaultCalculus.EApp", "subterm_ordering_Catala.DefaultCalculus.EDefault", "subterm_ordering_Catala.DefaultCalculus.EIf", "token_correspondence_Catala.DefaultCalculus.extend", "token_correspondence_Catala.DefaultCalculus.step_exceptions.fuel_instrumented", "token_correspondence_Catala.DefaultCalculus.typing.fuel_instrumented", "token_correspondence_Catala.DefaultCalculus.typing_list.fuel_instrumented", "token_correspondence_Catala.DefaultCalculus.var_to_exp_beta", "typing_Catala.DefaultCalculus.__proj__ELit__item__l", "typing_Catala.DefaultCalculus.empty", "typing_Catala.DefaultCalculus.is_value", "typing_Catala.DefaultCalculus.step", "typing_Catala.DefaultCalculus.subst", "typing_Catala.DefaultCalculus.typing", "typing_Catala.DefaultCalculus.uu___is_ELit", "typing_Catala.DefaultCalculus.var_to_exp_beta", "typing_Tm_abs_1df2ad5da40b1dd4a17c31d2cebba95a", "typing_Tm_abs_85708d064e5d0dbdd7c749ea62f421af", "typing_Tm_abs_9b0fb98b88819d883b74246421860dc1", "typing_tok_Catala.DefaultCalculus.AllEmpty@tok", "typing_tok_Catala.DefaultCalculus.TBool@tok", "unit_inversion", "unit_typing" ], 0, "1f5c06cb5572febc9e2355e796f50834" ], [ "Catala.DefaultCalculus.preservation", 3, 3, 1, [ "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.l_and", "equation_Prims.squash", "l_and-interp", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "b3bcc3a1d16fea99e6f6a223fe293e0f" ], [ "Catala.DefaultCalculus.preservation", 4, 4, 2, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Catala.DefaultCalculus.step.fuel_instrumented", "@fuel_correspondence_Catala.DefaultCalculus.step_exceptions_left_to_right.fuel_instrumented", "@fuel_correspondence_Catala.DefaultCalculus.typing.fuel_instrumented", "@fuel_correspondence_Catala.DefaultCalculus.typing_list.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.step.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.step_exceptions_left_to_right.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.typing.fuel_instrumented", "@fuel_irrelevance_Catala.DefaultCalculus.typing_list.fuel_instrumented", "@query", "Catala.DefaultCalculus_pretyping_0ccd8e9cc590b3a6d39eb0752f03f688", "Catala.DefaultCalculus_pretyping_6aa41574d40712b03e0367a1a3c256b3", "b2t_def", "binder_x_0ccd8e9cc590b3a6d39eb0752f03f688_0", "binder_x_57403813bce408351cc0e70737e314ef_1", "binder_x_6aa41574d40712b03e0367a1a3c256b3_4", "binder_x_9d898a02527d03c282f289aa9ecae7fc_2", "binder_x_9d898a02527d03c282f289aa9ecae7fc_3", "bool_inversion", "bool_typing", "constructor_distinct_Catala.DefaultCalculus.EDefault", "constructor_distinct_Catala.DefaultCalculus.ELit", "constructor_distinct_Catala.DefaultCalculus.LConflictError", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "data_elim_Catala.DefaultCalculus.EDefault", "data_elim_FStar.Pervasives.Native.Some", "data_typing_intro_Catala.DefaultCalculus.EDefault@tok", "data_typing_intro_Catala.DefaultCalculus.TUnit@tok", "disc_equation_FStar.Pervasives.Native.None", "disc_equation_FStar.Pervasives.Native.Some", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "equality_tok_Catala.DefaultCalculus.LConflictError@tok", "equality_tok_Catala.DefaultCalculus.TBool@tok", "equation_Catala.DefaultCalculus.c_err", "equation_Catala.DefaultCalculus.empty", "equation_Catala.DefaultCalculus.is_value", "equation_Prims.l_and", "equation_Prims.squash", "equation_with_fuel_Catala.DefaultCalculus.step.fuel_instrumented", "equation_with_fuel_Catala.DefaultCalculus.step_exceptions_left_to_right.fuel_instrumented", "equation_with_fuel_Catala.DefaultCalculus.typing.fuel_instrumented", "equation_with_fuel_Catala.DefaultCalculus.typing_list.fuel_instrumented", "fuel_guarded_inversion_Catala.DefaultCalculus.exp", "fuel_guarded_inversion_FStar.Pervasives.Native.option", "fuel_guarded_inversion_Prims.list", "kinding_Catala.DefaultCalculus.exp@tok", "l_and-interp", "lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "proj_equation_FStar.Pervasives.Native.Some_v", "projection_inverse_BoxBool_proj_0", "projection_inverse_Catala.DefaultCalculus.EDefault_cons", "projection_inverse_Catala.DefaultCalculus.EDefault_exceptions", "projection_inverse_Catala.DefaultCalculus.EDefault_just", "projection_inverse_Catala.DefaultCalculus.EDefault_tau", "projection_inverse_Catala.DefaultCalculus.ELit_l", "projection_inverse_FStar.Pervasives.Native.None_a", "projection_inverse_FStar.Pervasives.Native.Some_v", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a", "refinement_interpretation_Tm_refine_2aceacac479fb56248306a969addd084", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_8adbef10d645a4d9aac0702fe91040be", "refinement_interpretation_Tm_refine_94ff508dba60a98364daca65da372e14", "refinement_interpretation_Tm_refine_adf079fdab7afb98eae06afbf41efee1", "subterm_ordering_Prims.Cons", "token_correspondence_Catala.DefaultCalculus.step_exceptions_left_to_right.fuel_instrumented", "token_correspondence_Catala.DefaultCalculus.typing.fuel_instrumented", "token_correspondence_Catala.DefaultCalculus.typing_list.fuel_instrumented", "typing_Catala.DefaultCalculus.empty", "typing_Catala.DefaultCalculus.step", "typing_Catala.DefaultCalculus.step_exceptions_left_to_right", "typing_Catala.DefaultCalculus.typing", "typing_tok_Catala.DefaultCalculus.TBool@tok", "unit_inversion", "unit_typing" ], 0, "0ffcc137baddae54cd5223d99bb5fffa" ] ] ]