lean4-htt/src/boot/init/core.cpp

// Lean compiler output
// Module: init.core
// Imports:
#include "runtime/object.h"
#include "runtime/apply.h"
#include "kernel/builtin.h"
typedef lean::object obj;
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
#endif
obj* _l_s4_psum_s6_sizeof(obj*, obj*);
obj* _l_s5_sigma_s6_sizeof_s6___main_s6___rarg(obj*, obj*, obj*);
obj* _l_s2_eq_s9_ndrec__on_s6___rarg(obj*);
obj* _l_s5_thunk_s3_map(obj*, obj*);
obj* _l_s4_bool_s11_has__sizeof;
obj* _l_s4_quot_s21_rec__on__subsingleton_s6___rarg(obj*, obj*);
obj* _l_s5_total;
obj* _l_s7_implies_s9_decidable_s6___rarg(obj*, obj*);
obj* _l_s6_psigma_s11_has__sizeof(obj*, obj*);
obj* _l_s3_nat_s3_add_s6___main(obj*, obj*);
obj* _l_s8_quotient_s27_rec__on__subsingleton_u2082_s4___at_s8_quotient_s13_decidable__eq_s9___spec__1_s6___rarg(obj*, obj*, obj*);
obj* _l_s5_thunk_s4_bind_s6___rarg(obj*, obj*, unsigned char);
obj* _l_s2_eq_s5_ndrec(obj*, obj*, obj*);
obj* _l_s4_prod_s9_inhabited_s6___rarg(obj*, obj*);
obj* _l_s4_prod_s6_sizeof_s6___main(obj*, obj*);
obj* _l_s7_subtype_s9_inhabited_s6___rarg(obj*, obj*);
obj* _l_s9_decidable_s8_to__bool(obj*);
obj* _l_s5_thunk_s4_pure_s6___rarg_s7___boxed(obj*, obj*);
obj* _l_s3_sum_s6_sizeof_s6___main(obj*, obj*);
obj* _l_s5_punit_s6_sizeof(unsigned char);
obj* _l_s6_inline(obj*);
obj* _l_s2_or_s9_decidable(obj*, obj*);
obj* _l_s5_sigma_s6_sizeof_s6___rarg(obj*, obj*, obj*);
obj* _l_s6_option_s11_has__sizeof_s6___rarg(obj*);
obj* _l_s8_quotient_s10_lift_u2082(obj*, obj*, obj*, obj*, obj*);
obj* _l_s4_task_s3_map(obj*, obj*);
obj* _l_s18_setoid__has__equiv(obj*, obj*);
obj* _l_s4_dite(obj*);
obj* _l_s28_decidable__of__decidable__eq(obj*);
obj* _l_s4_unit_s4_star_s7___boxed;
obj* _l_s9___private_3425436377__s15_fun__to__extfun(obj*, obj*);
obj* _l_s4_dite_s6___rarg(obj*, obj*, obj*, obj*);
obj* _l_s3_bor_s6___main_s7___boxed(obj*, obj*);
obj* _l_s2_or_s4_symm;
obj* _l_s6_absurd(obj*, obj*, obj*, obj*);
obj* _l_s8_quotient_s21_rec__on__subsingleton(obj*, obj*, obj*, obj*);
obj* _l_s8_quotient_s3_rec(obj*, obj*, obj*);
obj* _l_s8_quotient_s21_rec__on__subsingleton_s6___rarg(obj*, obj*);
obj* _l_s5_sigma_s6_sizeof_s4___at_s5_sigma_s11_has__sizeof_s9___spec__1_s6___rarg(obj*, obj*, obj*);
obj* _l_s18_right__cancelative;
obj* _l_s23_forall__prop__decidable(obj*, obj*);
obj* _l_s28_decidable__of__decidable__eq_s6___rarg(obj*, obj*, obj*);
obj* _l_s8_quotient_s8_hrec__on_s6___rarg(obj*, obj*, obj*);
obj* _l_s4_prod_s6_sizeof(obj*, obj*);
unsigned char _l_s4_bxor_s6___main(unsigned char, unsigned char);
unsigned char _l_s4_unit_s4_star;
obj* _l_s6_exists_s5_intro;
obj* _l_s5_thunk_s3_map_s6___rarg(obj*, obj*, unsigned char);
obj* _l_s9___private_2312050019__s11_extfun__app(obj*, obj*);
obj* _l_s2_or_s12_intro__right;
obj* _l_s4_bit1(obj*);
obj* _l_s3_sum_s13_decidable__eq(obj*, obj*);
obj* _l_s2_or_s9_decidable_s6___rarg(obj*, obj*);
obj* _l_s20_default__has__sizeof_s11___closed__1;
obj* _l_s24_prod__has__decidable__lt_s6___rarg(obj*, obj*, obj*, obj*, obj*, obj*);
obj* _l_s3_xor_s9_decidable_s6___rarg(obj*, obj*);
obj* _l_s9_decidable_s14_rec__on__false_s6___rarg(obj*, obj*, obj*, obj*, obj*);
obj* _l_s3_and_s9_decidable(obj*, obj*);
obj* _l_s4_task_s4_pure_s6___rarg_s7___boxed(obj*, obj*);
obj* _l_s7_subtype_s6_sizeof(obj*);
obj* _l_s9_decidable_s9_by__cases(obj*, obj*);
obj* _l_s3_sum_s11_has__sizeof_s6___rarg(obj*, obj*);
obj* _l_s9___private_3425436377__s15_fun__to__extfun_s6___rarg(obj*);
obj* _l_s9_symmetric;
obj* _l_s32_decidable__of__decidable__of__eq(obj*, obj*);
obj* _l_s4_prod_s11_has__sizeof_s6___rarg(obj*, obj*);
obj* _l_s7_default_s6_sizeof_s6___main(obj*, obj*);
obj* _l_s9___private_1845649337__s3_rel;
obj* _l_s2_pi_s9_inhabited(obj*, obj*);
obj* _l_s4_list_s11_has__sizeof_s6___rarg(obj*);
obj* _l_s9_id__delta_s6___rarg(obj*);
obj* _l_s8_quotient_s13_decidable__eq_s6___rarg(obj*, obj*, obj*, obj*);
obj* _l_s4_list_s6_sizeof_s6___main_s6___rarg(obj*, obj*);
obj* _l_s4_cond(obj*);
obj* _l_s9_arbitrary_s6___rarg(obj*);
obj* _l_s3_fun_s9_inhabited(obj*, obj*);
obj* _l_s4_cond_s6___main_s6___rarg_s7___boxed(obj*, obj*, obj*);
obj* _l_s3_sum_s11_has__sizeof(obj*, obj*);
obj* _l_s4_task_s4_bind_s6___rarg_s7___boxed(obj*, obj*, obj*);
obj* _l_s4_prop_s9_inhabited;
obj* _l_s8_quotient_s13_decidable__eq_s6___rarg_s11___lambda__1(obj*, obj*, obj*);
obj* _l_s5_sigma_s6_sizeof_s6___main_s4___at_s5_sigma_s11_has__sizeof_s9___spec__2_s6___rarg(obj*, obj*, obj*);
obj* _l_s3_and_s9_decidable_s6___rarg(obj*, obj*);
obj* _l_s20_default__has__sizeof(obj*);
obj* _l_s6_option_s6_sizeof_s6___main_s6___rarg(obj*, obj*);
obj* _l_s4_bnot_s7___boxed(obj*);
obj* _l_s8_quotient_s2_mk_s6___rarg(obj*);
obj* _l_s4_true_s9_decidable;
obj* _l_s4_psum_s6_sizeof_s6___main(obj*, obj*);
obj* _l_s3_sum_s15_inhabited__left_s6___rarg(obj*);
obj* _l_s4_task_s4_bind_s6___rarg(obj*, obj*, unsigned char);
obj* _l_s3_iff_s9_decidable(obj*, obj*);
obj* _l_s29_decidable__eq__of__bool__pred(obj*);
obj* _l_s5_false_s4_elim_s7___boxed(obj*, obj*);
unsigned char _l_s4_band(unsigned char, unsigned char);
obj* _l_s5_false_s4_elim(obj*, unsigned char);
obj* _l_s3_std_s8_priority_s3_max;
obj* _l_s5_thunk_s4_pure(obj*);
obj* _l_s5_punit_s6_sizeof_s6___main(unsigned char);
unsigned char _l_s3_bor(unsigned char, unsigned char);
obj* _l_s6_option_s6_sizeof_s6___main(obj*);
obj* _l_s10_opt__param;
obj* _l_s5_sigma_s6_sizeof(obj*, obj*);
obj* _l_s4_list_s6_sizeof_s6___rarg(obj*, obj*);
obj* _l_s3_nat_s4_prio;
obj* _l_s7_subtype_s6_sizeof_s6___rarg(obj*, obj*, obj*);
obj* _l_s3_not;
obj* _l_s4_prod_s13_decidable__eq_s6___rarg(obj*, obj*, obj*, obj*);
obj* _l_s4_psum_s11_has__sizeof(obj*, obj*);
obj* _l_s2_id_s6___rarg(obj*);
obj* _l_s4_psum_s6_sizeof_s6___main_s6___rarg(obj*, obj*, obj*);
obj* _l_s11_subrelation;
obj* _l_s4_quot_s7_rec__on_s6___rarg(obj*, obj*, obj*);
obj* _l_s3_bor_s7___boxed(obj*, obj*);
obj* _l_s5_thunk_s4_bind(obj*, obj*);
obj* _l_s3_ite(obj*);
obj* _l_s2_eq_s5_ndrec_s6___rarg(obj*, obj*, obj*);
obj* _l_s2_or_s9_by__cases_s6___rarg(obj*, obj*, obj*, obj*, obj*, obj*);
obj* _l_s15_right__identity;
obj* _l_s8_function_s5_equiv;
obj* _l_s3_sum_s16_inhabited__right_s6___rarg(obj*);
obj* _l_s33_decidable__of__decidable__of__iff_s6___rarg(obj*, obj*);
obj* _l_s5_punit_s13_decidable__eq_s7___boxed(obj*, obj*);
obj* _l_s6_psigma_s6_sizeof_s4___at_s6_psigma_s11_has__sizeof_s9___spec__1_s6___rarg(obj*, obj*, obj*);
obj* _l_s4_cond_s6___rarg_s7___boxed(obj*, obj*, obj*);
obj* _l_s3_nat_s8_has__one;
obj* _l_s3_sum_s6_sizeof(obj*, obj*);
obj* _l_s17_type__eq__of__heq;
obj* _l_s10_inv__image;
obj* _l_s5_punit_s12_subsingleton;
obj* _l_s5_thunk_s3_get_s6___rarg(obj*);
obj* _l_s4_bool_s9_inhabited_s7___boxed;
obj* _l_s4_list_s6_sizeof_s6___main(obj*);
obj* _l_s3_xor;
obj* _l_s4_task_s3_map_s6___rarg(obj*, obj*, unsigned char);
obj* _l_s3_not_s9_decidable_s6___rarg(obj*);
obj* _l_s10_combinator_s1_K(obj*, obj*);
obj* _l_s2_ne;
obj* _l_s4_task_s3_get(obj*);
obj* _l_s4_quot_s8_lift__on_s6___rarg(obj*, obj*, obj*);
obj* _l_s3_ite_s6___rarg(obj*, obj*, obj*, obj*);
obj* _l_s4_cond_s6___main(obj*);
unsigned char _l_s3_bor_s6___main(unsigned char, unsigned char);
obj* _l_s4_cond_s6___rarg(unsigned char, obj*, obj*);
obj* _l_s3_rfl;
obj* _l_s8_quotient_s7_rec__on(obj*, obj*, obj*);
obj* _l_s4_quot_s5_indep_s6___rarg(obj*, obj*);
obj* _l_s8_eqv__gen_s6_setoid(obj*, obj*);
obj* _l_s11_irreflexive;
obj* _l_s15_empty__relation;
obj* _l_s15_infer__instance(obj*);
obj* _l_s4_prod_s3_map(obj*, obj*, obj*, obj*);
obj* _l_s4_quot_s7_rec__on(obj*, obj*, obj*);
obj* _l_s2_eq_s3_mpr_s6___rarg(obj*);
obj* _l_s3_and_s10_elim__left;
obj* _l_s7_subtype_s13_decidable__eq_s6___rarg(obj*, obj*, obj*);
obj* _l_s8_quotient_s4_lift(obj*, obj*, obj*);
obj* _l_s32_decidable__of__decidable__of__eq_s6___rarg(obj*, obj*);
obj* _l_s7_subtype_s11_has__sizeof_s6___rarg(obj*, obj*);
obj* _l_s3_heq_s3_rfl;
obj* _l_s23_nonempty__of__inhabited;
obj* _l_s6_psigma_s6_sizeof_s6___rarg(obj*, obj*, obj*);
obj* _l_s4_prod_s7_has__lt(obj*, obj*, obj*, obj*);
obj* _l_s4_prod_s3_map_s6___main(obj*, obj*, obj*, obj*);
unsigned char _l_s4_bxor(unsigned char, unsigned char);
obj* _l_s4_quot_s5_indep(obj*, obj*, obj*);
obj* _l_s7_subtype_s6_sizeof_s6___main(obj*);
obj* _l_s10_out__param;
obj* _l_s7_subtype_s11_has__sizeof(obj*);
obj* _l_s8_quotient_s3_rec_s6___rarg(obj*, obj*, obj*);
obj* _l_s8_quotient_s8_lift__on(obj*, obj*, obj*);
obj* _l_s4_task_s4_pure(obj*);
obj* _l_s3_fun_s9_inhabited_s6___rarg(obj*, obj*);
obj* _l_s5_punit_s6_sizeof_s6___main_s7___boxed(obj*);
obj* _l_s4_bit1_s6___rarg(obj*, obj*, obj*);
obj* _l_s10_combinator_s1_S_s6___rarg(obj*, obj*, obj*);
obj* _l_s4_dite_s9_decidable_s6___rarg(obj*, obj*, obj*);
obj* _l_s2_or_s11_intro__left;
obj* _l_s3_nat_s9_inhabited;
obj* _l_s29_decidable__eq__of__bool__pred_s6___rarg(obj*, obj*, obj*, obj*, obj*);
obj* _l_s18_subsingleton__prop;
obj* _l_s4_unit;
obj* _l_s7_subtype_s9_inhabited(obj*, obj*);
obj* _l_s3_iff_s9_decidable_s6___rarg(obj*, obj*);
obj* _l_s3_std_s4_prec_s9_max__plus;
obj* _l_s4_bit0(obj*);
obj* _l_s23_exists__prop__decidable_s6___rarg(obj*, obj*);
obj* _l_s5_thunk_s4_bind_s6___rarg_s7___boxed(obj*, obj*, obj*);
obj* _l_s4_prod_s11_has__sizeof(obj*, obj*);
obj* _l_s9_decidable_s13_rec__on__true_s6___rarg(obj*, obj*, obj*, obj*, obj*);
obj* _l_s9_decidable_s8_to__bool_s6___rarg_s7___boxed(obj*);
obj* _l_s15_mk__equivalence;
obj* _l_s5_sigma_s6_sizeof_s6___main(obj*, obj*);
obj* _l_s2_eq_s3_mpr(obj*, obj*, obj*);
obj* _l_s4_psum_s11_has__sizeof_s6___rarg(obj*, obj*);
obj* _l_s3_nat_s11_has__sizeof;
obj* _l_s4_prod_s6_sizeof_s6___rarg(obj*, obj*, obj*);
obj* _l_s9_singleton_s6___rarg(obj*, obj*, obj*);
obj* _l_s11_equivalence;
obj* _l_s9_ssuperset;
obj* _l_s2_gt;
obj* _l_s14_decidable__rel;
obj* _l_s5_sigma_s6_sizeof_s4___at_s5_sigma_s11_has__sizeof_s9___spec__1(obj*, obj*);
obj* _l_s4_bool_s6_sizeof_s6___main(unsigned char);
obj* _l_s6_inline_s6___rarg(obj*);
obj* _l_s9_decidable_s12_subsingleton;
obj* _l_s7_implies;
obj* _l_s4_prod_s9_inhabited(obj*, obj*);
obj* _l_s3_std_s4_prec_s3_max;
obj* _l_s4_psum_s6_sizeof_s6___rarg(obj*, obj*, obj*);
obj* _l_s19_right__distributive;
obj* _l_s4_bnot_s6___main_s7___boxed(obj*);
obj* _l_s7_subtype_s13_decidable__eq(obj*, obj*);
obj* _l_s2_ge;
obj* _l_s14_right__inverse;
obj* _l_s4_quot_s3_rec(obj*, obj*, obj*);
unsigned char _l_s9_decidable_s8_to__bool_s6___rarg(obj*);
obj* _l_s4_bit0_s6___rarg(obj*, obj*);
obj* _l_s3_std_s4_prec_s5_arrow;
obj* _l_s18_left__distributive;
obj* _l_s3_sum_s16_inhabited__right(obj*, obj*);
obj* _l_s9_decidable_s14_rec__on__false(obj*);
obj* _l_s7_subtype_s19_exists__of__subtype;
obj* _l_s19_infer__instance__as_s6___rarg(obj*);
unsigned char _l_s4_band_s6___main(unsigned char, unsigned char);
obj* _l_s17_left__cancelative;
obj* _l_s2_eq_s2_mp(obj*, obj*, obj*);
obj* _l_s3_nat_s8_has__add;
obj* _l_s4_quot_s21_rec__on__subsingleton(obj*, obj*, obj*, obj*);
obj* _l_s4_quot_s3_rec_s6___rarg(obj*, obj*, obj*);
obj* _l_s3_sum_s6_sizeof_s6___main_s6___rarg(obj*, obj*, obj*);
obj* _l_s4_band_s7___boxed(obj*, obj*);
obj* _l_s6_psigma_s11_has__sizeof_s6___rarg(obj*, obj*);
obj* _l_s5_sigma_s11_has__sizeof_s6___rarg(obj*, obj*);
obj* _l_s4_true_s9_inhabited;
obj* _l_s2_pi_s12_subsingleton;
obj* _l_s23_forall__prop__decidable_s6___rarg(obj*, obj*);
obj* _l_s5_thunk_s3_get(obj*);
obj* _l_s2_ne_s9_decidable_s6___rarg(obj*, obj*, obj*);
obj* _l_s12_and__implies;
obj* _l_s15_anti__symmetric;
obj* _l_s4_quot_s8_lift__on(obj*, obj*, obj*);
obj* _l_s10_combinator_s1_S(obj*, obj*, obj*);
obj* _l_s4_flip_s6___rarg(obj*, obj*, obj*);
obj* _l_s8_quotient_s5_sound;
obj* _l_s14_left__identity;
obj* _l_s10_combinator_s1_I(obj*);
obj* _l_s12_of__as__true;
obj* _l_s3_ite_s9_decidable_s6___rarg(obj*, obj*, obj*);
unsigned char _l_s5_punit_s9_inhabited;
obj* _l_s7_trivial;
obj* _l_s4_task_s3_get_s6___rarg(obj*);
obj* _l_s4_prod_s6_sizeof_s6___main_s6___rarg(obj*, obj*, obj*);
obj* _l_s5_punit_s6_sizeof_s7___boxed(obj*);
obj* _l_s5_sigma_s6_sizeof_s6___main_s4___at_s5_sigma_s11_has__sizeof_s9___spec__2(obj*, obj*);
obj* _l_s3_nat_s6_sizeof(obj*);
obj* _l_s3_nat_s6_sizeof_s6___main(obj*);
obj* _l_s4_bool_s6_sizeof_s6___main_s7___boxed(obj*);
obj* _l_s5_sigma_s11_has__sizeof(obj*, obj*);
obj* _l_s19_infer__instance__as(obj*);
obj* _l_s14_not__true__iff;
obj* _l_s3_nat_s9_has__zero;
unsigned char _l_s4_bool_s9_inhabited;
obj* _l_s6_psigma_s6_sizeof(obj*, obj*);
obj* _l_s8_quotient_s14_lift__on_u2082(obj*, obj*, obj*, obj*, obj*);
obj* _l_s24_prod__has__decidable__lt(obj*, obj*, obj*, obj*);
obj* _l_s4_bool_s6_sizeof_s7___boxed(obj*);
obj* _l_s8_quotient_s27_rec__on__subsingleton_u2082_s6___rarg(obj*, obj*, obj*);
obj* _l_s4_quot_s8_hrec__on_s6___rarg(obj*, obj*, obj*);
obj* _l_s4_band_s6___main_s7___boxed(obj*, obj*);
obj* _l_s4_quot_s8_hrec__on(obj*, obj*, obj*);
obj* _l_s3_xor_s9_decidable(obj*, obj*);
obj* _l_s6_psigma_s6_sizeof_s6___main_s4___at_s6_psigma_s11_has__sizeof_s9___spec__2(obj*, obj*);
obj* _l_s8_quotient_s2_mk(obj*, obj*);
obj* _l_s11_typed__expr(obj*);
obj* _l_s3_not_s9_decidable(obj*);
obj* _l_s5_thunk_s4_pure_s6___rarg(obj*, unsigned char);
obj* _l_s3_sum_s13_decidable__eq_s6___rarg(obj*, obj*, obj*, obj*);
obj* _l_s4_cast(obj*, obj*, obj*);
obj* _l_s8_quotient_s13_decidable__eq(obj*);
obj* _l_s10_combinator_s1_K_s6___rarg(obj*, obj*);
obj* _l_s4_bool_s6_sizeof(unsigned char);
obj* _l_s3_sum_s15_inhabited__left(obj*, obj*);
obj* _l_s7_default_s6___rarg(obj*);
obj* _l_s10_combinator_s1_I_s6___rarg(obj*);
obj* _l_s7_implies_s9_decidable(obj*, obj*);
obj* _l_s8_nonempty_s4_elim;
obj* _l_s8_quotient_s27_rec__on__subsingleton_u2082_s4___at_s8_quotient_s13_decidable__eq_s9___spec__1(obj*, obj*);
obj* _l_s3_and_s4_symm;
obj* _l_s7_subtype_s19_exists__of__subtype_s6___main;
obj* _l_s4_bxor_s7___boxed(obj*, obj*);
obj* _l_s13_is__dec__refl;
obj* _l_s8_quotient_s10_lift_u2082_s6___rarg(obj*, obj*, obj*, obj*);
obj* _l_s8_quotient_s8_hrec__on(obj*, obj*, obj*);
obj* _l_s2_eq_s9_ndrec__on(obj*, obj*, obj*, obj*, obj*);
obj* _l_s3_std_s8_priority_s7_default;
obj* _l_s5_punit_s11_has__sizeof;
obj* _l_s11_typed__expr_s6___rarg(obj*);
obj* _l_s4_bool_s13_decidable__eq(unsigned char, unsigned char);
obj* _l_s2_pi_s9_inhabited_s6___rarg(obj*, obj*);
obj* _l_s6_psigma_s6_sizeof_s4___at_s6_psigma_s11_has__sizeof_s9___spec__1(obj*, obj*);
obj* _l_s9_reflexive;
obj* _l_s9_singleton(obj*, obj*);
obj* _l_s4_dite_s9_decidable(obj*, obj*, obj*);
obj* _l_s17_left__commutative;
obj* _l_s11_associative;
obj* _l_s6_psigma_s6_sizeof_s6___main_s4___at_s6_psigma_s11_has__sizeof_s9___spec__2_s6___rarg(obj*, obj*, obj*);
obj* _l_s9_arbitrary(obj*);
obj* _l_s9___private_2312050019__s11_extfun__app_s6___rarg(obj*, obj*);
obj* _l_s2_id(obj*);
obj* _l_s3_sum_s6_sizeof_s6___rarg(obj*, obj*, obj*);
obj* _l_s4_list_s6_sizeof(obj*);
obj* _l_s4_flip(obj*, obj*, obj*);
obj* _l_s4_list_s11_has__sizeof(obj*);
obj* _l_s4_prod_s3_map_s6___main_s6___rarg(obj*, obj*, obj*);
obj* _l_s11_is__dec__eq;
obj* _l_s4_task_s4_bind(obj*, obj*);
obj* _l_s6_option_s6_sizeof(obj*);
obj* _l_s8_quotient_s27_rec__on__subsingleton_u2082(obj*, obj*, obj*, obj*, obj*, obj*);
obj* _l_s6_psigma_s6_sizeof_s6___main(obj*, obj*);
obj* _l_s4_task_s4_pure_s6___rarg(obj*, unsigned char);
obj* _l_s5_punit_s9_inhabited_s7___boxed;
obj* _l_s2_or_s9_by__cases(obj*, obj*);
obj* _l_s2_eq_s2_mp_s6___rarg(obj*);
obj* _l_s4_bool_s13_decidable__eq_s7___boxed(obj*, obj*);
obj* _l_s9___private_1597490181__s6_extfun;
obj* _l_s8_quotient_s8_lift__on_s6___rarg(obj*, obj*, obj*);
obj* _l_s2_ne_s9_decidable(obj*);
obj* _l_s9_decidable_s13_rec__on__true(obj*);
obj* _l_s9_id__delta(obj*);
obj* _l_s15_infer__instance_s6___rarg(obj*);
obj* _l_s9_classical_s9_by__cases;
obj* _l_s7_id__rhs(obj*);
obj* _l_s8_quotient;
obj* _l_s9___private_1944762901__s11_fun__setoid(obj*, obj*);
obj* _l_s8_quotient_s4_lift_s6___rarg(obj*, obj*, obj*);
obj* _l_s8_quotient_s7_rec__on_s6___rarg(obj*, obj*, obj*);
obj* _l_s4_cond_s6___main_s6___rarg(unsigned char, obj*, obj*);
obj* _l_s6_psigma_s6_sizeof_s6___main_s6___rarg(obj*, obj*, obj*);
obj* _l_s7_default(obj*);
obj* _l_s4_prod_s3_map_s6___rarg(obj*, obj*, obj*);
obj* _l_s12_subsingleton_s5_helim;
obj* _l_s7_id__rhs_s6___rarg(obj*);
unsigned char _l_s4_bnot(unsigned char);
obj* _l_s5_thunk_s3_map_s6___rarg_s7___boxed(obj*, obj*, obj*);
obj* _l_s9_decidable_s9_by__cases_s6___rarg(obj*, obj*, obj*);
obj* _l_s33_decidable__of__decidable__of__iff(obj*, obj*);
obj* _l_s18_right__commutative;
obj* _l_s8_superset;
obj* _l_s8_as__true;
obj* _l_s12_subsingleton_s4_elim;
obj* _l_s7_default_s6_sizeof(obj*, obj*);
obj* _l_s4_cast_s6___rarg(obj*);
obj* _l_s3_ite_s9_decidable(obj*, obj*, obj*);
obj* _l_s23_exists__prop__decidable(obj*, obj*);
obj* _l_s4_prod_s13_decidable__eq(obj*, obj*);
obj* _l_s7_subtype_s6_sizeof_s6___main_s6___rarg(obj*, obj*, obj*);
obj* _l_s8_quotient_s14_lift__on_u2082_s6___rarg(obj*, obj*, obj*, obj*);
obj* _l_s12_not__not__em;
obj* _l_s11_commutative;
obj* _l_s5_punit_s13_decidable__eq(unsigned char, unsigned char);
unsigned char _l_s4_bnot_s6___main(unsigned char);
obj* _l_s6_option_s11_has__sizeof(obj*);
obj* _l_s6_option_s6_sizeof_s6___rarg(obj*, obj*);
obj* _l_s10_transitive;
obj* _l_s9_as__false;
obj* _l_s4_bxor_s6___main_s7___boxed(obj*, obj*);
obj* _l_s3_and_s11_elim__right;
obj* _l_s15_decidable__pred;
obj* _l_s4_task_s3_map_s6___rarg_s7___boxed(obj*, obj*, obj*);
obj* _l_s5_false_s9_decidable;
obj* _l_s2_id_s6___rarg(obj* x_0) {
{

return x_0;
}
}
obj* _l_s2_id(obj* x_0) {
{
obj* x_2; 
lean::dec(x_0);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s2_id_s6___rarg), 1, 0);
return x_2;
}
}
obj* _l_s6_inline_s6___rarg(obj* x_0) {
{

return x_0;
}
}
obj* _l_s6_inline(obj* x_0) {
{
obj* x_2; 
lean::dec(x_0);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s6_inline_s6___rarg), 1, 0);
return x_2;
}
}
obj* _l_s4_flip_s6___rarg(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_3; 
x_3 = lean::apply_2(x_0, x_2, x_1);
return x_3;
}
}
obj* _l_s4_flip(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_6; 
lean::dec(x_2);
lean::dec(x_1);
lean::dec(x_0);
x_6 = lean::alloc_closure(reinterpret_cast<void*>(_l_s4_flip_s6___rarg), 3, 0);
return x_6;
}
}
obj* _l_s9_id__delta_s6___rarg(obj* x_0) {
{

return x_0;
}
}
obj* _l_s9_id__delta(obj* x_0) {
{
obj* x_2; 
lean::dec(x_0);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s9_id__delta_s6___rarg), 1, 0);
return x_2;
}
}
obj* _init__l_s10_opt__param() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s10_out__param() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _l_s11_typed__expr_s6___rarg(obj* x_0) {
{

return x_0;
}
}
obj* _l_s11_typed__expr(obj* x_0) {
{
obj* x_2; 
lean::dec(x_0);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s11_typed__expr_s6___rarg), 1, 0);
return x_2;
}
}
obj* _l_s7_id__rhs_s6___rarg(obj* x_0) {
{

return x_0;
}
}
obj* _l_s7_id__rhs(obj* x_0) {
{
obj* x_2; 
lean::dec(x_0);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s7_id__rhs_s6___rarg), 1, 0);
return x_2;
}
}
obj* _init__l_s4_unit() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
unsigned char _init__l_s4_unit_s4_star() {
{
unsigned char x_0; 
x_0 = 0;
return x_0;
}
}
obj* _init__l_s4_unit_s4_star_s7___boxed() {
{
unsigned char x_0; obj* x_1; 
x_0 = _l_s4_unit_s4_star;
x_1 = lean::box(x_0);
return x_1;
}
}
obj* _l_s5_thunk_s4_pure_s6___rarg(obj* x_0, unsigned char x_1) {
{

return x_0;
}
}
obj* _l_s5_thunk_s4_pure(obj* x_0) {
{
obj* x_2; 
lean::dec(x_0);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s5_thunk_s4_pure_s6___rarg_s7___boxed), 2, 0);
return x_2;
}
}
obj* _l_s5_thunk_s4_pure_s6___rarg_s7___boxed(obj* x_0, obj* x_1) {
{
unsigned char x_2; obj* x_3; 
x_2 = lean::unbox(x_1);
x_3 = _l_s5_thunk_s4_pure_s6___rarg(x_0, x_2);
return x_3;
}
}
obj* _l_s5_thunk_s3_get_s6___rarg(obj* x_0) {
{
unsigned char x_1; obj* x_2; obj* x_3; 
x_1 = 0;
x_2 = lean::box(x_1);
x_3 = lean::apply_1(x_0, x_2);
return x_3;
}
}
obj* _l_s5_thunk_s3_get(obj* x_0) {
{
obj* x_2; 
lean::dec(x_0);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s5_thunk_s3_get_s6___rarg), 1, 0);
return x_2;
}
}
obj* _l_s5_thunk_s3_map_s6___rarg(obj* x_0, obj* x_1, unsigned char x_2) {
{
obj* x_3; obj* x_4; obj* x_5; 
x_3 = _l_s5_thunk_s3_get(lean::box(0));
x_4 = lean::apply_1(x_3, x_1);
x_5 = lean::apply_1(x_0, x_4);
return x_5;
}
}
obj* _l_s5_thunk_s3_map(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s5_thunk_s3_map_s6___rarg_s7___boxed), 3, 0);
return x_4;
}
}
obj* _l_s5_thunk_s3_map_s6___rarg_s7___boxed(obj* x_0, obj* x_1, obj* x_2) {
{
unsigned char x_3; obj* x_4; 
x_3 = lean::unbox(x_2);
x_4 = _l_s5_thunk_s3_map_s6___rarg(x_0, x_1, x_3);
return x_4;
}
}
obj* _l_s5_thunk_s4_bind_s6___rarg(obj* x_0, obj* x_1, unsigned char x_2) {
{
obj* x_3; obj* x_5; obj* x_6; obj* x_7; 
x_3 = _l_s5_thunk_s3_get(lean::box(0));
lean::inc(x_3);
x_5 = lean::apply_1(x_3, x_0);
x_6 = lean::apply_1(x_1, x_5);
x_7 = lean::apply_1(x_3, x_6);
return x_7;
}
}
obj* _l_s5_thunk_s4_bind(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s5_thunk_s4_bind_s6___rarg_s7___boxed), 3, 0);
return x_4;
}
}
obj* _l_s5_thunk_s4_bind_s6___rarg_s7___boxed(obj* x_0, obj* x_1, obj* x_2) {
{
unsigned char x_3; obj* x_4; 
x_3 = lean::unbox(x_2);
x_4 = _l_s5_thunk_s4_bind_s6___rarg(x_0, x_1, x_3);
return x_4;
}
}
obj* _l_s4_task_s4_pure_s6___rarg(obj* x_0, unsigned char x_1) {
{

return x_0;
}
}
obj* _l_s4_task_s4_pure(obj* x_0) {
{
obj* x_2; 
lean::dec(x_0);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s4_task_s4_pure_s6___rarg_s7___boxed), 2, 0);
return x_2;
}
}
obj* _l_s4_task_s4_pure_s6___rarg_s7___boxed(obj* x_0, obj* x_1) {
{
unsigned char x_2; obj* x_3; 
x_2 = lean::unbox(x_1);
x_3 = _l_s4_task_s4_pure_s6___rarg(x_0, x_2);
return x_3;
}
}
obj* _l_s4_task_s3_get_s6___rarg(obj* x_0) {
{
unsigned char x_1; obj* x_2; obj* x_3; 
x_1 = 0;
x_2 = lean::box(x_1);
x_3 = lean::apply_1(x_0, x_2);
return x_3;
}
}
obj* _l_s4_task_s3_get(obj* x_0) {
{
obj* x_2; 
lean::dec(x_0);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s4_task_s3_get_s6___rarg), 1, 0);
return x_2;
}
}
obj* _l_s4_task_s3_map_s6___rarg(obj* x_0, obj* x_1, unsigned char x_2) {
{
obj* x_3; obj* x_4; obj* x_5; 
x_3 = _l_s4_task_s3_get(lean::box(0));
x_4 = lean::apply_1(x_3, x_1);
x_5 = lean::apply_1(x_0, x_4);
return x_5;
}
}
obj* _l_s4_task_s3_map(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s4_task_s3_map_s6___rarg_s7___boxed), 3, 0);
return x_4;
}
}
obj* _l_s4_task_s3_map_s6___rarg_s7___boxed(obj* x_0, obj* x_1, obj* x_2) {
{
unsigned char x_3; obj* x_4; 
x_3 = lean::unbox(x_2);
x_4 = _l_s4_task_s3_map_s6___rarg(x_0, x_1, x_3);
return x_4;
}
}
obj* _l_s4_task_s4_bind_s6___rarg(obj* x_0, obj* x_1, unsigned char x_2) {
{
obj* x_3; obj* x_5; obj* x_6; obj* x_7; 
x_3 = _l_s4_task_s3_get(lean::box(0));
lean::inc(x_3);
x_5 = lean::apply_1(x_3, x_0);
x_6 = lean::apply_1(x_1, x_5);
x_7 = lean::apply_1(x_3, x_6);
return x_7;
}
}
obj* _l_s4_task_s4_bind(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s4_task_s4_bind_s6___rarg_s7___boxed), 3, 0);
return x_4;
}
}
obj* _l_s4_task_s4_bind_s6___rarg_s7___boxed(obj* x_0, obj* x_1, obj* x_2) {
{
unsigned char x_3; obj* x_4; 
x_3 = lean::unbox(x_2);
x_4 = _l_s4_task_s4_bind_s6___rarg(x_0, x_1, x_3);
return x_4;
}
}
obj* _init__l_s3_not() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _l_s2_eq_s5_ndrec_s6___rarg(obj* x_0, obj* x_1, obj* x_2) {
{

lean::dec(x_2);
lean::dec(x_1);
return x_0;
}
}
obj* _l_s2_eq_s5_ndrec(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_6; 
lean::dec(x_2);
lean::dec(x_1);
lean::dec(x_0);
x_6 = lean::alloc_closure(reinterpret_cast<void*>(_l_s2_eq_s5_ndrec_s6___rarg), 3, 0);
return x_6;
}
}
obj* _l_s2_eq_s9_ndrec__on_s6___rarg(obj* x_0) {
{

return x_0;
}
}
obj* _l_s2_eq_s9_ndrec__on(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
{
obj* x_10; 
lean::dec(x_4);
lean::dec(x_3);
lean::dec(x_2);
lean::dec(x_1);
lean::dec(x_0);
x_10 = lean::alloc_closure(reinterpret_cast<void*>(_l_s2_eq_s9_ndrec__on_s6___rarg), 1, 0);
return x_10;
}
}
obj* _init__l_s3_and_s10_elim__left() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s3_and_s11_elim__right() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s3_rfl() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s3_heq_s3_rfl() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s2_or_s11_intro__left() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s2_or_s12_intro__right() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s15_decidable__pred() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s14_decidable__rel() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _l_s28_decidable__of__decidable__eq_s6___rarg(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_3; 
x_3 = lean::apply_2(x_2, x_0, x_1);
return x_3;
}
}
obj* _l_s28_decidable__of__decidable__eq(obj* x_0) {
{
obj* x_2; 
lean::dec(x_0);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s28_decidable__of__decidable__eq_s6___rarg), 3, 0);
return x_2;
}
}
obj* _init__l_s2_ge() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s2_gt() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s8_superset() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s9_ssuperset() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _l_s4_bit0_s6___rarg(obj* x_0, obj* x_1) {
{
obj* x_3; 
lean::inc(x_1);
x_3 = lean::apply_2(x_0, x_1, x_1);
return x_3;
}
}
obj* _l_s4_bit0(obj* x_0) {
{
obj* x_2; 
lean::dec(x_0);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s4_bit0_s6___rarg), 2, 0);
return x_2;
}
}
obj* _l_s4_bit1_s6___rarg(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_5; obj* x_6; 
lean::inc(x_2);
lean::inc(x_1);
x_5 = lean::apply_2(x_1, x_2, x_2);
x_6 = lean::apply_2(x_1, x_5, x_0);
return x_6;
}
}
obj* _l_s4_bit1(obj* x_0) {
{
obj* x_2; 
lean::dec(x_0);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s4_bit1_s6___rarg), 3, 0);
return x_2;
}
}
obj* _l_s9_singleton_s6___rarg(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_3; 
x_3 = lean::apply_2(x_1, x_2, x_0);
return x_3;
}
}
obj* _l_s9_singleton(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s9_singleton_s6___rarg), 3, 0);
return x_4;
}
}
obj* _l_s3_nat_s3_add_s6___main(obj* x_0, obj* x_1) {
{
obj* x_2; obj* x_3; 
x_2 = lean::mk_nat_obj(0u);
x_3 = lean::nat_dec_eq(x_1, x_2);
lean::dec(x_2);
if (lean::obj_tag(x_3) == 0)
{
obj* x_6; obj* x_7; obj* x_9; obj* x_10; 
lean::dec(x_3);
x_6 = lean::mk_nat_obj(1u);
x_7 = lean::nat_sub(x_1, x_6);
lean::dec(x_1);
x_9 = _l_s3_nat_s3_add_s6___main(x_0, x_7);
x_10 = lean::nat_add(x_9, x_6);
lean::dec(x_6);
lean::dec(x_9);
return x_10;
}
else
{

lean::dec(x_1);
lean::dec(x_3);
return x_0;
}
}
}
obj* _init__l_s3_nat_s9_has__zero() {
{
obj* x_0; 
x_0 = lean::mk_nat_obj(0u);
return x_0;
}
}
obj* _init__l_s3_nat_s8_has__one() {
{
obj* x_0; 
x_0 = lean::mk_nat_obj(1u);
return x_0;
}
}
obj* _init__l_s3_nat_s8_has__add() {
{
obj* x_0; 
x_0 = lean::alloc_closure(reinterpret_cast<void*>(lean::nat_add), 2, 0);
return x_0;
}
}
obj* _init__l_s3_std_s8_priority_s7_default() {
{
obj* x_0; 
x_0 = lean::mk_nat_obj(1000u);
return x_0;
}
}
obj* _init__l_s3_std_s8_priority_s3_max() {
{
obj* x_0; 
x_0 = lean::mk_nat_obj(lean::mpz("4294967295"));
return x_0;
}
}
obj* _init__l_s3_nat_s4_prio() {
{
obj* x_0; obj* x_1; obj* x_2; 
x_0 = _l_s3_std_s8_priority_s7_default;
x_1 = lean::mk_nat_obj(100u);
x_2 = lean::nat_add(x_0, x_1);
lean::dec(x_1);
return x_2;
}
}
obj* _init__l_s3_std_s4_prec_s3_max() {
{
obj* x_0; 
x_0 = lean::mk_nat_obj(1024u);
return x_0;
}
}
obj* _init__l_s3_std_s4_prec_s5_arrow() {
{
obj* x_0; 
x_0 = lean::mk_nat_obj(25u);
return x_0;
}
}
obj* _init__l_s3_std_s4_prec_s9_max__plus() {
{
obj* x_0; obj* x_1; obj* x_2; 
x_0 = _l_s3_std_s4_prec_s3_max;
x_1 = lean::mk_nat_obj(10u);
x_2 = lean::nat_add(x_0, x_1);
lean::dec(x_1);
return x_2;
}
}
obj* _l_s7_default_s6_sizeof_s6___main(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::mk_nat_obj(0u);
return x_4;
}
}
obj* _l_s7_default_s6_sizeof(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::mk_nat_obj(0u);
return x_4;
}
}
obj* _l_s20_default__has__sizeof(obj* x_0) {
{
obj* x_2; 
lean::dec(x_0);
x_2 = _l_s20_default__has__sizeof_s11___closed__1;
lean::inc(x_2);
return x_2;
}
}
obj* _init__l_s20_default__has__sizeof_s11___closed__1() {
{
obj* x_0; 
x_0 = lean::alloc_closure(reinterpret_cast<void*>(_l_s7_default_s6_sizeof), 2, 1);
lean::closure_set(x_0, 0, lean::box(0));
return x_0;
}
}
obj* _l_s3_nat_s6_sizeof_s6___main(obj* x_0) {
{

return x_0;
}
}
obj* _l_s3_nat_s6_sizeof(obj* x_0) {
{

return x_0;
}
}
obj* _init__l_s3_nat_s11_has__sizeof() {
{
obj* x_0; 
x_0 = lean::alloc_closure(reinterpret_cast<void*>(_l_s3_nat_s6_sizeof), 1, 0);
return x_0;
}
}
obj* _l_s4_prod_s6_sizeof_s6___main_s6___rarg(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_3; obj* x_5; obj* x_8; obj* x_9; obj* x_10; obj* x_13; obj* x_14; 
x_3 = lean::cnstr_get(x_2, 0);
lean::inc(x_3);
x_5 = lean::cnstr_get(x_2, 1);
lean::inc(x_5);
lean::dec(x_2);
x_8 = lean::apply_1(x_0, x_3);
x_9 = lean::mk_nat_obj(1u);
x_10 = lean::nat_add(x_9, x_8);
lean::dec(x_8);
lean::dec(x_9);
x_13 = lean::apply_1(x_1, x_5);
x_14 = lean::nat_add(x_10, x_13);
lean::dec(x_13);
lean::dec(x_10);
return x_14;
}
}
obj* _l_s4_prod_s6_sizeof_s6___main(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s4_prod_s6_sizeof_s6___main_s6___rarg), 3, 0);
return x_4;
}
}
obj* _l_s4_prod_s6_sizeof_s6___rarg(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_3; 
x_3 = _l_s4_prod_s6_sizeof_s6___main_s6___rarg(x_0, x_1, x_2);
return x_3;
}
}
obj* _l_s4_prod_s6_sizeof(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s4_prod_s6_sizeof_s6___rarg), 3, 0);
return x_4;
}
}
obj* _l_s4_prod_s11_has__sizeof_s6___rarg(obj* x_0, obj* x_1) {
{
obj* x_2; 
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s4_prod_s6_sizeof_s6___rarg), 3, 2);
lean::closure_set(x_2, 0, x_0);
lean::closure_set(x_2, 1, x_1);
return x_2;
}
}
obj* _l_s4_prod_s11_has__sizeof(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s4_prod_s11_has__sizeof_s6___rarg), 2, 0);
return x_4;
}
}
obj* _l_s3_sum_s6_sizeof_s6___main_s6___rarg(obj* x_0, obj* x_1, obj* x_2) {
{

if (lean::obj_tag(x_2) == 0)
{
obj* x_4; obj* x_7; obj* x_8; obj* x_9; 
lean::dec(x_1);
x_4 = lean::cnstr_get(x_2, 0);
lean::inc(x_4);
lean::dec(x_2);
x_7 = lean::apply_1(x_0, x_4);
x_8 = lean::mk_nat_obj(1u);
x_9 = lean::nat_add(x_8, x_7);
lean::dec(x_7);
lean::dec(x_8);
return x_9;
}
else
{
obj* x_13; obj* x_16; obj* x_17; obj* x_18; 
lean::dec(x_0);
x_13 = lean::cnstr_get(x_2, 0);
lean::inc(x_13);
lean::dec(x_2);
x_16 = lean::apply_1(x_1, x_13);
x_17 = lean::mk_nat_obj(1u);
x_18 = lean::nat_add(x_17, x_16);
lean::dec(x_16);
lean::dec(x_17);
return x_18;
}
}
}
obj* _l_s3_sum_s6_sizeof_s6___main(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s3_sum_s6_sizeof_s6___main_s6___rarg), 3, 0);
return x_4;
}
}
obj* _l_s3_sum_s6_sizeof_s6___rarg(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_3; 
x_3 = _l_s3_sum_s6_sizeof_s6___main_s6___rarg(x_0, x_1, x_2);
return x_3;
}
}
obj* _l_s3_sum_s6_sizeof(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s3_sum_s6_sizeof_s6___rarg), 3, 0);
return x_4;
}
}
obj* _l_s3_sum_s11_has__sizeof_s6___rarg(obj* x_0, obj* x_1) {
{
obj* x_2; 
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s3_sum_s6_sizeof_s6___rarg), 3, 2);
lean::closure_set(x_2, 0, x_0);
lean::closure_set(x_2, 1, x_1);
return x_2;
}
}
obj* _l_s3_sum_s11_has__sizeof(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s3_sum_s11_has__sizeof_s6___rarg), 2, 0);
return x_4;
}
}
obj* _l_s4_psum_s6_sizeof_s6___main_s6___rarg(obj* x_0, obj* x_1, obj* x_2) {
{

if (lean::obj_tag(x_2) == 0)
{
obj* x_4; obj* x_7; obj* x_8; obj* x_9; 
lean::dec(x_1);
x_4 = lean::cnstr_get(x_2, 0);
lean::inc(x_4);
lean::dec(x_2);
x_7 = lean::apply_1(x_0, x_4);
x_8 = lean::mk_nat_obj(1u);
x_9 = lean::nat_add(x_8, x_7);
lean::dec(x_7);
lean::dec(x_8);
return x_9;
}
else
{
obj* x_13; obj* x_16; obj* x_17; obj* x_18; 
lean::dec(x_0);
x_13 = lean::cnstr_get(x_2, 0);
lean::inc(x_13);
lean::dec(x_2);
x_16 = lean::apply_1(x_1, x_13);
x_17 = lean::mk_nat_obj(1u);
x_18 = lean::nat_add(x_17, x_16);
lean::dec(x_16);
lean::dec(x_17);
return x_18;
}
}
}
obj* _l_s4_psum_s6_sizeof_s6___main(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s4_psum_s6_sizeof_s6___main_s6___rarg), 3, 0);
return x_4;
}
}
obj* _l_s4_psum_s6_sizeof_s6___rarg(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_3; 
x_3 = _l_s4_psum_s6_sizeof_s6___main_s6___rarg(x_0, x_1, x_2);
return x_3;
}
}
obj* _l_s4_psum_s6_sizeof(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s4_psum_s6_sizeof_s6___rarg), 3, 0);
return x_4;
}
}
obj* _l_s4_psum_s11_has__sizeof_s6___rarg(obj* x_0, obj* x_1) {
{
obj* x_2; 
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s4_psum_s6_sizeof_s6___rarg), 3, 2);
lean::closure_set(x_2, 0, x_0);
lean::closure_set(x_2, 1, x_1);
return x_2;
}
}
obj* _l_s4_psum_s11_has__sizeof(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s4_psum_s11_has__sizeof_s6___rarg), 2, 0);
return x_4;
}
}
obj* _l_s5_sigma_s6_sizeof_s6___main_s6___rarg(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_3; obj* x_5; obj* x_9; obj* x_10; obj* x_11; obj* x_14; obj* x_15; 
x_3 = lean::cnstr_get(x_2, 0);
lean::inc(x_3);
x_5 = lean::cnstr_get(x_2, 1);
lean::inc(x_5);
lean::dec(x_2);
lean::inc(x_3);
x_9 = lean::apply_1(x_0, x_3);
x_10 = lean::mk_nat_obj(1u);
x_11 = lean::nat_add(x_10, x_9);
lean::dec(x_9);
lean::dec(x_10);
x_14 = lean::apply_2(x_1, x_3, x_5);
x_15 = lean::nat_add(x_11, x_14);
lean::dec(x_14);
lean::dec(x_11);
return x_15;
}
}
obj* _l_s5_sigma_s6_sizeof_s6___main(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s5_sigma_s6_sizeof_s6___main_s6___rarg), 3, 0);
return x_4;
}
}
obj* _l_s5_sigma_s6_sizeof_s6___rarg(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_3; 
x_3 = _l_s5_sigma_s6_sizeof_s6___main_s6___rarg(x_0, x_1, x_2);
return x_3;
}
}
obj* _l_s5_sigma_s6_sizeof(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s5_sigma_s6_sizeof_s6___rarg), 3, 0);
return x_4;
}
}
obj* _l_s5_sigma_s11_has__sizeof_s6___rarg(obj* x_0, obj* x_1) {
{
obj* x_2; 
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s5_sigma_s6_sizeof_s4___at_s5_sigma_s11_has__sizeof_s9___spec__1_s6___rarg), 3, 2);
lean::closure_set(x_2, 0, x_0);
lean::closure_set(x_2, 1, x_1);
return x_2;
}
}
obj* _l_s5_sigma_s11_has__sizeof(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s5_sigma_s11_has__sizeof_s6___rarg), 2, 0);
return x_4;
}
}
obj* _l_s5_sigma_s6_sizeof_s6___main_s4___at_s5_sigma_s11_has__sizeof_s9___spec__2_s6___rarg(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_3; obj* x_5; obj* x_9; obj* x_10; obj* x_11; obj* x_14; obj* x_15; 
x_3 = lean::cnstr_get(x_2, 0);
lean::inc(x_3);
x_5 = lean::cnstr_get(x_2, 1);
lean::inc(x_5);
lean::dec(x_2);
lean::inc(x_3);
x_9 = lean::apply_1(x_0, x_3);
x_10 = lean::mk_nat_obj(1u);
x_11 = lean::nat_add(x_10, x_9);
lean::dec(x_9);
lean::dec(x_10);
x_14 = lean::apply_2(x_1, x_3, x_5);
x_15 = lean::nat_add(x_11, x_14);
lean::dec(x_14);
lean::dec(x_11);
return x_15;
}
}
obj* _l_s5_sigma_s6_sizeof_s6___main_s4___at_s5_sigma_s11_has__sizeof_s9___spec__2(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s5_sigma_s6_sizeof_s6___main_s4___at_s5_sigma_s11_has__sizeof_s9___spec__2_s6___rarg), 3, 0);
return x_4;
}
}
obj* _l_s5_sigma_s6_sizeof_s4___at_s5_sigma_s11_has__sizeof_s9___spec__1_s6___rarg(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_3; 
x_3 = _l_s5_sigma_s6_sizeof_s6___main_s4___at_s5_sigma_s11_has__sizeof_s9___spec__2_s6___rarg(x_0, x_1, x_2);
return x_3;
}
}
obj* _l_s5_sigma_s6_sizeof_s4___at_s5_sigma_s11_has__sizeof_s9___spec__1(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s5_sigma_s6_sizeof_s4___at_s5_sigma_s11_has__sizeof_s9___spec__1_s6___rarg), 3, 0);
return x_4;
}
}
obj* _l_s6_psigma_s6_sizeof_s6___main_s6___rarg(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_3; obj* x_5; obj* x_9; obj* x_10; obj* x_11; obj* x_14; obj* x_15; 
x_3 = lean::cnstr_get(x_2, 0);
lean::inc(x_3);
x_5 = lean::cnstr_get(x_2, 1);
lean::inc(x_5);
lean::dec(x_2);
lean::inc(x_3);
x_9 = lean::apply_1(x_0, x_3);
x_10 = lean::mk_nat_obj(1u);
x_11 = lean::nat_add(x_10, x_9);
lean::dec(x_9);
lean::dec(x_10);
x_14 = lean::apply_2(x_1, x_3, x_5);
x_15 = lean::nat_add(x_11, x_14);
lean::dec(x_14);
lean::dec(x_11);
return x_15;
}
}
obj* _l_s6_psigma_s6_sizeof_s6___main(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s6_psigma_s6_sizeof_s6___main_s6___rarg), 3, 0);
return x_4;
}
}
obj* _l_s6_psigma_s6_sizeof_s6___rarg(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_3; 
x_3 = _l_s6_psigma_s6_sizeof_s6___main_s6___rarg(x_0, x_1, x_2);
return x_3;
}
}
obj* _l_s6_psigma_s6_sizeof(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s6_psigma_s6_sizeof_s6___rarg), 3, 0);
return x_4;
}
}
obj* _l_s6_psigma_s11_has__sizeof_s6___rarg(obj* x_0, obj* x_1) {
{
obj* x_2; 
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s6_psigma_s6_sizeof_s4___at_s6_psigma_s11_has__sizeof_s9___spec__1_s6___rarg), 3, 2);
lean::closure_set(x_2, 0, x_0);
lean::closure_set(x_2, 1, x_1);
return x_2;
}
}
obj* _l_s6_psigma_s11_has__sizeof(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s6_psigma_s11_has__sizeof_s6___rarg), 2, 0);
return x_4;
}
}
obj* _l_s6_psigma_s6_sizeof_s6___main_s4___at_s6_psigma_s11_has__sizeof_s9___spec__2_s6___rarg(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_3; obj* x_5; obj* x_9; obj* x_10; obj* x_11; obj* x_14; obj* x_15; 
x_3 = lean::cnstr_get(x_2, 0);
lean::inc(x_3);
x_5 = lean::cnstr_get(x_2, 1);
lean::inc(x_5);
lean::dec(x_2);
lean::inc(x_3);
x_9 = lean::apply_1(x_0, x_3);
x_10 = lean::mk_nat_obj(1u);
x_11 = lean::nat_add(x_10, x_9);
lean::dec(x_9);
lean::dec(x_10);
x_14 = lean::apply_2(x_1, x_3, x_5);
x_15 = lean::nat_add(x_11, x_14);
lean::dec(x_14);
lean::dec(x_11);
return x_15;
}
}
obj* _l_s6_psigma_s6_sizeof_s6___main_s4___at_s6_psigma_s11_has__sizeof_s9___spec__2(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s6_psigma_s6_sizeof_s6___main_s4___at_s6_psigma_s11_has__sizeof_s9___spec__2_s6___rarg), 3, 0);
return x_4;
}
}
obj* _l_s6_psigma_s6_sizeof_s4___at_s6_psigma_s11_has__sizeof_s9___spec__1_s6___rarg(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_3; 
x_3 = _l_s6_psigma_s6_sizeof_s6___main_s4___at_s6_psigma_s11_has__sizeof_s9___spec__2_s6___rarg(x_0, x_1, x_2);
return x_3;
}
}
obj* _l_s6_psigma_s6_sizeof_s4___at_s6_psigma_s11_has__sizeof_s9___spec__1(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s6_psigma_s6_sizeof_s4___at_s6_psigma_s11_has__sizeof_s9___spec__1_s6___rarg), 3, 0);
return x_4;
}
}
obj* _l_s5_punit_s6_sizeof_s6___main(unsigned char x_0) {
{
obj* x_1; 
x_1 = lean::mk_nat_obj(1u);
return x_1;
}
}
obj* _l_s5_punit_s6_sizeof_s6___main_s7___boxed(obj* x_0) {
{
unsigned char x_1; obj* x_2; 
x_1 = lean::unbox(x_0);
x_2 = _l_s5_punit_s6_sizeof_s6___main(x_1);
return x_2;
}
}
obj* _l_s5_punit_s6_sizeof(unsigned char x_0) {
{
obj* x_1; 
x_1 = lean::mk_nat_obj(1u);
return x_1;
}
}
obj* _l_s5_punit_s6_sizeof_s7___boxed(obj* x_0) {
{
unsigned char x_1; obj* x_2; 
x_1 = lean::unbox(x_0);
x_2 = _l_s5_punit_s6_sizeof(x_1);
return x_2;
}
}
obj* _init__l_s5_punit_s11_has__sizeof() {
{
obj* x_0; 
x_0 = lean::alloc_closure(reinterpret_cast<void*>(_l_s5_punit_s6_sizeof_s7___boxed), 1, 0);
return x_0;
}
}
obj* _l_s4_bool_s6_sizeof_s6___main(unsigned char x_0) {
{
obj* x_1; 
x_1 = lean::mk_nat_obj(1u);
return x_1;
}
}
obj* _l_s4_bool_s6_sizeof_s6___main_s7___boxed(obj* x_0) {
{
unsigned char x_1; obj* x_2; 
x_1 = lean::unbox(x_0);
x_2 = _l_s4_bool_s6_sizeof_s6___main(x_1);
return x_2;
}
}
obj* _l_s4_bool_s6_sizeof(unsigned char x_0) {
{
obj* x_1; 
x_1 = lean::mk_nat_obj(1u);
return x_1;
}
}
obj* _l_s4_bool_s6_sizeof_s7___boxed(obj* x_0) {
{
unsigned char x_1; obj* x_2; 
x_1 = lean::unbox(x_0);
x_2 = _l_s4_bool_s6_sizeof(x_1);
return x_2;
}
}
obj* _init__l_s4_bool_s11_has__sizeof() {
{
obj* x_0; 
x_0 = lean::alloc_closure(reinterpret_cast<void*>(_l_s4_bool_s6_sizeof_s7___boxed), 1, 0);
return x_0;
}
}
obj* _l_s6_option_s6_sizeof_s6___main_s6___rarg(obj* x_0, obj* x_1) {
{

if (lean::obj_tag(x_1) == 0)
{
obj* x_4; 
lean::dec(x_0);
lean::dec(x_1);
x_4 = lean::mk_nat_obj(1u);
return x_4;
}
else
{
obj* x_5; obj* x_8; obj* x_9; obj* x_10; 
x_5 = lean::cnstr_get(x_1, 0);
lean::inc(x_5);
lean::dec(x_1);
x_8 = lean::apply_1(x_0, x_5);
x_9 = lean::mk_nat_obj(1u);
x_10 = lean::nat_add(x_9, x_8);
lean::dec(x_8);
lean::dec(x_9);
return x_10;
}
}
}
obj* _l_s6_option_s6_sizeof_s6___main(obj* x_0) {
{
obj* x_2; 
lean::dec(x_0);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s6_option_s6_sizeof_s6___main_s6___rarg), 2, 0);
return x_2;
}
}
obj* _l_s6_option_s6_sizeof_s6___rarg(obj* x_0, obj* x_1) {
{
obj* x_2; 
x_2 = _l_s6_option_s6_sizeof_s6___main_s6___rarg(x_0, x_1);
return x_2;
}
}
obj* _l_s6_option_s6_sizeof(obj* x_0) {
{
obj* x_2; 
lean::dec(x_0);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s6_option_s6_sizeof_s6___rarg), 2, 0);
return x_2;
}
}
obj* _l_s6_option_s11_has__sizeof_s6___rarg(obj* x_0) {
{
obj* x_1; 
x_1 = lean::alloc_closure(reinterpret_cast<void*>(_l_s6_option_s6_sizeof_s6___rarg), 2, 1);
lean::closure_set(x_1, 0, x_0);
return x_1;
}
}
obj* _l_s6_option_s11_has__sizeof(obj* x_0) {
{
obj* x_2; 
lean::dec(x_0);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s6_option_s11_has__sizeof_s6___rarg), 1, 0);
return x_2;
}
}
obj* _l_s4_list_s6_sizeof_s6___main_s6___rarg(obj* x_0, obj* x_1) {
{

if (lean::obj_tag(x_1) == 0)
{
obj* x_4; 
lean::dec(x_0);
lean::dec(x_1);
x_4 = lean::mk_nat_obj(1u);
return x_4;
}
else
{
obj* x_5; obj* x_7; obj* x_11; obj* x_12; obj* x_13; obj* x_16; obj* x_17; 
x_5 = lean::cnstr_get(x_1, 0);
lean::inc(x_5);
x_7 = lean::cnstr_get(x_1, 1);
lean::inc(x_7);
lean::dec(x_1);
lean::inc(x_0);
x_11 = lean::apply_1(x_0, x_5);
x_12 = lean::mk_nat_obj(1u);
x_13 = lean::nat_add(x_12, x_11);
lean::dec(x_11);
lean::dec(x_12);
x_16 = _l_s4_list_s6_sizeof_s6___main_s6___rarg(x_0, x_7);
x_17 = lean::nat_add(x_13, x_16);
lean::dec(x_16);
lean::dec(x_13);
return x_17;
}
}
}
obj* _l_s4_list_s6_sizeof_s6___main(obj* x_0) {
{
obj* x_2; 
lean::dec(x_0);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s4_list_s6_sizeof_s6___main_s6___rarg), 2, 0);
return x_2;
}
}
obj* _l_s4_list_s6_sizeof_s6___rarg(obj* x_0, obj* x_1) {
{
obj* x_2; 
x_2 = _l_s4_list_s6_sizeof_s6___main_s6___rarg(x_0, x_1);
return x_2;
}
}
obj* _l_s4_list_s6_sizeof(obj* x_0) {
{
obj* x_2; 
lean::dec(x_0);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s4_list_s6_sizeof_s6___rarg), 2, 0);
return x_2;
}
}
obj* _l_s4_list_s11_has__sizeof_s6___rarg(obj* x_0) {
{
obj* x_1; 
x_1 = lean::alloc_closure(reinterpret_cast<void*>(_l_s4_list_s6_sizeof_s6___rarg), 2, 1);
lean::closure_set(x_1, 0, x_0);
return x_1;
}
}
obj* _l_s4_list_s11_has__sizeof(obj* x_0) {
{
obj* x_2; 
lean::dec(x_0);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s4_list_s11_has__sizeof_s6___rarg), 1, 0);
return x_2;
}
}
obj* _l_s7_subtype_s6_sizeof_s6___main_s6___rarg(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_4; 
lean::dec(x_1);
x_4 = lean::apply_1(x_0, x_2);
return x_4;
}
}
obj* _l_s7_subtype_s6_sizeof_s6___main(obj* x_0) {
{
obj* x_2; 
lean::dec(x_0);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s7_subtype_s6_sizeof_s6___main_s6___rarg), 3, 0);
return x_2;
}
}
obj* _l_s7_subtype_s6_sizeof_s6___rarg(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_4; 
lean::dec(x_1);
x_4 = lean::apply_1(x_0, x_2);
return x_4;
}
}
obj* _l_s7_subtype_s6_sizeof(obj* x_0) {
{
obj* x_2; 
lean::dec(x_0);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s7_subtype_s6_sizeof_s6___rarg), 3, 0);
return x_2;
}
}
obj* _l_s7_subtype_s11_has__sizeof_s6___rarg(obj* x_0, obj* x_1) {
{
obj* x_3; 
lean::dec(x_1);
x_3 = lean::alloc_closure(reinterpret_cast<void*>(_l_s7_subtype_s6_sizeof_s6___rarg), 3, 2);
lean::closure_set(x_3, 0, x_0);
lean::closure_set(x_3, 1, lean::box(0));
return x_3;
}
}
obj* _l_s7_subtype_s11_has__sizeof(obj* x_0) {
{
obj* x_2; 
lean::dec(x_0);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s7_subtype_s11_has__sizeof_s6___rarg), 2, 0);
return x_2;
}
}
obj* _l_s10_combinator_s1_I_s6___rarg(obj* x_0) {
{

return x_0;
}
}
obj* _l_s10_combinator_s1_I(obj* x_0) {
{
obj* x_2; 
lean::dec(x_0);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s10_combinator_s1_I_s6___rarg), 1, 0);
return x_2;
}
}
obj* _l_s10_combinator_s1_K_s6___rarg(obj* x_0, obj* x_1) {
{

lean::dec(x_1);
return x_0;
}
}
obj* _l_s10_combinator_s1_K(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s10_combinator_s1_K_s6___rarg), 2, 0);
return x_4;
}
}
obj* _l_s10_combinator_s1_S_s6___rarg(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_4; obj* x_5; 
lean::inc(x_2);
x_4 = lean::apply_1(x_1, x_2);
x_5 = lean::apply_2(x_0, x_2, x_4);
return x_5;
}
}
obj* _l_s10_combinator_s1_S(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_6; 
lean::dec(x_2);
lean::dec(x_1);
lean::dec(x_0);
x_6 = lean::alloc_closure(reinterpret_cast<void*>(_l_s10_combinator_s1_S_s6___rarg), 3, 0);
return x_6;
}
}
obj* _l_s15_infer__instance_s6___rarg(obj* x_0) {
{

return x_0;
}
}
obj* _l_s15_infer__instance(obj* x_0) {
{
obj* x_2; 
lean::dec(x_0);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s15_infer__instance_s6___rarg), 1, 0);
return x_2;
}
}
obj* _l_s19_infer__instance__as_s6___rarg(obj* x_0) {
{

return x_0;
}
}
obj* _l_s19_infer__instance__as(obj* x_0) {
{
obj* x_2; 
lean::dec(x_0);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s19_infer__instance__as_s6___rarg), 1, 0);
return x_2;
}
}
obj* _l_s4_cond_s6___main_s6___rarg(unsigned char x_0, obj* x_1, obj* x_2) {
{

if (x_0 == 0)
{

lean::dec(x_1);
return x_2;
}
else
{

lean::dec(x_2);
return x_1;
}
}
}
obj* _l_s4_cond_s6___main(obj* x_0) {
{
obj* x_2; 
lean::dec(x_0);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s4_cond_s6___main_s6___rarg_s7___boxed), 3, 0);
return x_2;
}
}
obj* _l_s4_cond_s6___main_s6___rarg_s7___boxed(obj* x_0, obj* x_1, obj* x_2) {
{
unsigned char x_3; obj* x_4; 
x_3 = lean::unbox(x_0);
x_4 = _l_s4_cond_s6___main_s6___rarg(x_3, x_1, x_2);
return x_4;
}
}
obj* _l_s4_cond_s6___rarg(unsigned char x_0, obj* x_1, obj* x_2) {
{
obj* x_3; 
x_3 = _l_s4_cond_s6___main_s6___rarg(x_0, x_1, x_2);
return x_3;
}
}
obj* _l_s4_cond(obj* x_0) {
{
obj* x_2; 
lean::dec(x_0);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s4_cond_s6___rarg_s7___boxed), 3, 0);
return x_2;
}
}
obj* _l_s4_cond_s6___rarg_s7___boxed(obj* x_0, obj* x_1, obj* x_2) {
{
unsigned char x_3; obj* x_4; 
x_3 = lean::unbox(x_0);
x_4 = _l_s4_cond_s6___rarg(x_3, x_1, x_2);
return x_4;
}
}
unsigned char _l_s3_bor_s6___main(unsigned char x_0, unsigned char x_1) {
{

if (x_0 == 0)
{

return x_1;
}
else
{

return x_0;
}
}
}
obj* _l_s3_bor_s6___main_s7___boxed(obj* x_0, obj* x_1) {
{
unsigned char x_2; unsigned char x_3; unsigned char x_4; obj* x_5; 
x_2 = lean::unbox(x_0);
x_3 = lean::unbox(x_1);
x_4 = _l_s3_bor_s6___main(x_2, x_3);
x_5 = lean::box(x_4);
return x_5;
}
}
unsigned char _l_s3_bor(unsigned char x_0, unsigned char x_1) {
{
unsigned char x_2; 
x_2 = _l_s3_bor_s6___main(x_0, x_1);
return x_2;
}
}
obj* _l_s3_bor_s7___boxed(obj* x_0, obj* x_1) {
{
unsigned char x_2; unsigned char x_3; unsigned char x_4; obj* x_5; 
x_2 = lean::unbox(x_0);
x_3 = lean::unbox(x_1);
x_4 = _l_s3_bor(x_2, x_3);
x_5 = lean::box(x_4);
return x_5;
}
}
unsigned char _l_s4_band_s6___main(unsigned char x_0, unsigned char x_1) {
{

if (x_0 == 0)
{

return x_0;
}
else
{

return x_1;
}
}
}
obj* _l_s4_band_s6___main_s7___boxed(obj* x_0, obj* x_1) {
{
unsigned char x_2; unsigned char x_3; unsigned char x_4; obj* x_5; 
x_2 = lean::unbox(x_0);
x_3 = lean::unbox(x_1);
x_4 = _l_s4_band_s6___main(x_2, x_3);
x_5 = lean::box(x_4);
return x_5;
}
}
unsigned char _l_s4_band(unsigned char x_0, unsigned char x_1) {
{
unsigned char x_2; 
x_2 = _l_s4_band_s6___main(x_0, x_1);
return x_2;
}
}
obj* _l_s4_band_s7___boxed(obj* x_0, obj* x_1) {
{
unsigned char x_2; unsigned char x_3; unsigned char x_4; obj* x_5; 
x_2 = lean::unbox(x_0);
x_3 = lean::unbox(x_1);
x_4 = _l_s4_band(x_2, x_3);
x_5 = lean::box(x_4);
return x_5;
}
}
unsigned char _l_s4_bnot_s6___main(unsigned char x_0) {
{

if (x_0 == 0)
{
unsigned char x_1; 
x_1 = 1;
return x_1;
}
else
{
unsigned char x_2; 
x_2 = 0;
return x_2;
}
}
}
obj* _l_s4_bnot_s6___main_s7___boxed(obj* x_0) {
{
unsigned char x_1; unsigned char x_2; obj* x_3; 
x_1 = lean::unbox(x_0);
x_2 = _l_s4_bnot_s6___main(x_1);
x_3 = lean::box(x_2);
return x_3;
}
}
unsigned char _l_s4_bnot(unsigned char x_0) {
{
unsigned char x_1; 
x_1 = _l_s4_bnot_s6___main(x_0);
return x_1;
}
}
obj* _l_s4_bnot_s7___boxed(obj* x_0) {
{
unsigned char x_1; unsigned char x_2; obj* x_3; 
x_1 = lean::unbox(x_0);
x_2 = _l_s4_bnot(x_1);
x_3 = lean::box(x_2);
return x_3;
}
}
unsigned char _l_s4_bxor_s6___main(unsigned char x_0, unsigned char x_1) {
{

if (x_0 == 0)
{

return x_1;
}
else
{

if (x_1 == 0)
{

return x_0;
}
else
{
unsigned char x_2; 
x_2 = 0;
return x_2;
}
}
}
}
obj* _l_s4_bxor_s6___main_s7___boxed(obj* x_0, obj* x_1) {
{
unsigned char x_2; unsigned char x_3; unsigned char x_4; obj* x_5; 
x_2 = lean::unbox(x_0);
x_3 = lean::unbox(x_1);
x_4 = _l_s4_bxor_s6___main(x_2, x_3);
x_5 = lean::box(x_4);
return x_5;
}
}
unsigned char _l_s4_bxor(unsigned char x_0, unsigned char x_1) {
{
unsigned char x_2; 
x_2 = _l_s4_bxor_s6___main(x_0, x_1);
return x_2;
}
}
obj* _l_s4_bxor_s7___boxed(obj* x_0, obj* x_1) {
{
unsigned char x_2; unsigned char x_3; unsigned char x_4; obj* x_5; 
x_2 = lean::unbox(x_0);
x_3 = lean::unbox(x_1);
x_4 = _l_s4_bxor(x_2, x_3);
x_5 = lean::box(x_4);
return x_5;
}
}
obj* _init__l_s7_implies() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s7_trivial() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _l_s5_false_s4_elim(obj* x_0, unsigned char x_1) {
{
obj* x_3; 
lean::dec(x_0);
lean_unreachable();
x_3 = lean::box(0);
lean::inc(x_3);
return x_3;
}
}
obj* _l_s5_false_s4_elim_s7___boxed(obj* x_0, obj* x_1) {
{
unsigned char x_2; obj* x_3; 
x_2 = lean::unbox(x_1);
x_3 = _l_s5_false_s4_elim(x_0, x_2);
return x_3;
}
}
obj* _l_s6_absurd(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
{
obj* x_8; 
lean::dec(x_3);
lean::dec(x_2);
lean::dec(x_1);
lean::dec(x_0);
lean_unreachable();
x_8 = lean::box(0);
lean::inc(x_8);
return x_8;
}
}
obj* _l_s2_eq_s2_mp_s6___rarg(obj* x_0) {
{

return x_0;
}
}
obj* _l_s2_eq_s2_mp(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_6; 
lean::dec(x_2);
lean::dec(x_1);
lean::dec(x_0);
x_6 = lean::alloc_closure(reinterpret_cast<void*>(_l_s2_eq_s2_mp_s6___rarg), 1, 0);
return x_6;
}
}
obj* _l_s2_eq_s3_mpr_s6___rarg(obj* x_0) {
{

return x_0;
}
}
obj* _l_s2_eq_s3_mpr(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_6; 
lean::dec(x_2);
lean::dec(x_1);
lean::dec(x_0);
x_6 = lean::alloc_closure(reinterpret_cast<void*>(_l_s2_eq_s3_mpr_s6___rarg), 1, 0);
return x_6;
}
}
obj* _l_s4_cast_s6___rarg(obj* x_0) {
{

return x_0;
}
}
obj* _l_s4_cast(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_6; 
lean::dec(x_2);
lean::dec(x_1);
lean::dec(x_0);
x_6 = lean::alloc_closure(reinterpret_cast<void*>(_l_s4_cast_s6___rarg), 1, 0);
return x_6;
}
}
obj* _init__l_s2_ne() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s17_type__eq__of__heq() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s3_and_s4_symm() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s12_not__not__em() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s2_or_s4_symm() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s3_xor() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s14_not__true__iff() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s12_and__implies() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s6_exists_s5_intro() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
unsigned char _l_s9_decidable_s8_to__bool_s6___rarg(obj* x_0) {
{

if (lean::obj_tag(x_0) == 0)
{
unsigned char x_2; 
lean::dec(x_0);
x_2 = 0;
return x_2;
}
else
{
unsigned char x_4; 
lean::dec(x_0);
x_4 = 1;
return x_4;
}
}
}
obj* _l_s9_decidable_s8_to__bool(obj* x_0) {
{
obj* x_2; 
lean::dec(x_0);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s9_decidable_s8_to__bool_s6___rarg_s7___boxed), 1, 0);
return x_2;
}
}
obj* _l_s9_decidable_s8_to__bool_s6___rarg_s7___boxed(obj* x_0) {
{
unsigned char x_1; obj* x_2; 
x_1 = _l_s9_decidable_s8_to__bool_s6___rarg(x_0);
x_2 = lean::box(x_1);
return x_2;
}
}
obj* _init__l_s4_true_s9_decidable() {
{
obj* x_0; 
x_0 = lean::alloc_cnstr(1, 0, 0);
;
return x_0;
}
}
obj* _init__l_s5_false_s9_decidable() {
{
obj* x_0; 
x_0 = lean::alloc_cnstr(0, 0, 0);
;
return x_0;
}
}
obj* _l_s4_dite_s6___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
{

lean::dec(x_1);
if (lean::obj_tag(x_0) == 0)
{
obj* x_7; 
lean::dec(x_0);
lean::dec(x_2);
x_7 = lean::apply_1(x_3, lean::box(0));
return x_7;
}
else
{
obj* x_10; 
lean::dec(x_0);
lean::dec(x_3);
x_10 = lean::apply_1(x_2, lean::box(0));
return x_10;
}
}
}
obj* _l_s4_dite(obj* x_0) {
{
obj* x_2; 
lean::dec(x_0);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s4_dite_s6___rarg), 4, 0);
return x_2;
}
}
obj* _l_s3_ite_s6___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
{

lean::dec(x_1);
if (lean::obj_tag(x_0) == 0)
{

lean::dec(x_0);
lean::dec(x_2);
return x_3;
}
else
{

lean::dec(x_0);
lean::dec(x_3);
return x_2;
}
}
}
obj* _l_s3_ite(obj* x_0) {
{
obj* x_2; 
lean::dec(x_0);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s3_ite_s6___rarg), 4, 0);
return x_2;
}
}
obj* _l_s9_decidable_s13_rec__on__true_s6___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
{

lean::dec(x_3);
lean::dec(x_2);
lean::dec(x_1);
lean::dec(x_0);
return x_4;
}
}
obj* _l_s9_decidable_s13_rec__on__true(obj* x_0) {
{
obj* x_2; 
lean::dec(x_0);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s9_decidable_s13_rec__on__true_s6___rarg), 5, 0);
return x_2;
}
}
obj* _l_s9_decidable_s14_rec__on__false_s6___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
{

lean::dec(x_3);
lean::dec(x_2);
lean::dec(x_1);
lean::dec(x_0);
return x_4;
}
}
obj* _l_s9_decidable_s14_rec__on__false(obj* x_0) {
{
obj* x_2; 
lean::dec(x_0);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s9_decidable_s14_rec__on__false_s6___rarg), 5, 0);
return x_2;
}
}
obj* _l_s9_decidable_s9_by__cases_s6___rarg(obj* x_0, obj* x_1, obj* x_2) {
{

if (lean::obj_tag(x_0) == 0)
{
obj* x_5; 
lean::dec(x_0);
lean::dec(x_1);
x_5 = lean::apply_1(x_2, lean::box(0));
return x_5;
}
else
{
obj* x_8; 
lean::dec(x_0);
lean::dec(x_2);
x_8 = lean::apply_1(x_1, lean::box(0));
return x_8;
}
}
}
obj* _l_s9_decidable_s9_by__cases(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s9_decidable_s9_by__cases_s6___rarg), 3, 0);
return x_4;
}
}
obj* _l_s33_decidable__of__decidable__of__iff_s6___rarg(obj* x_0, obj* x_1) {
{

lean::dec(x_1);
return x_0;
}
}
obj* _l_s33_decidable__of__decidable__of__iff(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s33_decidable__of__decidable__of__iff_s6___rarg), 2, 0);
return x_4;
}
}
obj* _l_s32_decidable__of__decidable__of__eq_s6___rarg(obj* x_0, obj* x_1) {
{

lean::dec(x_1);
return x_0;
}
}
obj* _l_s32_decidable__of__decidable__of__eq(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s32_decidable__of__decidable__of__eq_s6___rarg), 2, 0);
return x_4;
}
}
obj* _l_s2_or_s9_by__cases_s6___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
{

lean::dec(x_3);
lean::dec(x_2);
lean::dec(x_1);
if (lean::obj_tag(x_0) == 0)
{
obj* x_11; 
lean::dec(x_4);
lean::dec(x_0);
x_11 = lean::apply_1(x_5, lean::box(0));
return x_11;
}
else
{
obj* x_14; 
lean::dec(x_5);
lean::dec(x_0);
x_14 = lean::apply_1(x_4, lean::box(0));
return x_14;
}
}
}
obj* _l_s2_or_s9_by__cases(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s2_or_s9_by__cases_s6___rarg), 6, 0);
return x_4;
}
}
obj* _l_s3_and_s9_decidable_s6___rarg(obj* x_0, obj* x_1) {
{

if (lean::obj_tag(x_0) == 0)
{
obj* x_4; 
lean::dec(x_0);
lean::dec(x_1);
x_4 = lean::alloc_cnstr(0, 0, 0);
;
return x_4;
}
else
{

lean::dec(x_0);
return x_1;
}
}
}
obj* _l_s3_and_s9_decidable(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s3_and_s9_decidable_s6___rarg), 2, 0);
return x_4;
}
}
obj* _l_s2_or_s9_decidable_s6___rarg(obj* x_0, obj* x_1) {
{

if (lean::obj_tag(x_0) == 0)
{

lean::dec(x_0);
return x_1;
}
else
{
obj* x_5; 
lean::dec(x_0);
lean::dec(x_1);
x_5 = lean::alloc_cnstr(1, 0, 0);
;
return x_5;
}
}
}
obj* _l_s2_or_s9_decidable(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s2_or_s9_decidable_s6___rarg), 2, 0);
return x_4;
}
}
obj* _l_s3_not_s9_decidable_s6___rarg(obj* x_0) {
{

if (lean::obj_tag(x_0) == 0)
{
obj* x_2; 
lean::dec(x_0);
x_2 = lean::alloc_cnstr(1, 0, 0);
;
return x_2;
}
else
{
obj* x_4; 
lean::dec(x_0);
x_4 = lean::alloc_cnstr(0, 0, 0);
;
return x_4;
}
}
}
obj* _l_s3_not_s9_decidable(obj* x_0) {
{
obj* x_2; 
lean::dec(x_0);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s3_not_s9_decidable_s6___rarg), 1, 0);
return x_2;
}
}
obj* _l_s7_implies_s9_decidable_s6___rarg(obj* x_0, obj* x_1) {
{

if (lean::obj_tag(x_0) == 0)
{
obj* x_4; 
lean::dec(x_0);
lean::dec(x_1);
x_4 = lean::alloc_cnstr(1, 0, 0);
;
return x_4;
}
else
{

lean::dec(x_0);
return x_1;
}
}
}
obj* _l_s7_implies_s9_decidable(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s7_implies_s9_decidable_s6___rarg), 2, 0);
return x_4;
}
}
obj* _l_s3_iff_s9_decidable_s6___rarg(obj* x_0, obj* x_1) {
{

if (lean::obj_tag(x_0) == 0)
{

lean::dec(x_0);
if (lean::obj_tag(x_1) == 0)
{
obj* x_4; 
lean::dec(x_1);
x_4 = lean::alloc_cnstr(1, 0, 0);
;
return x_4;
}
else
{
obj* x_6; 
lean::dec(x_1);
x_6 = lean::alloc_cnstr(0, 0, 0);
;
return x_6;
}
}
else
{

lean::dec(x_0);
return x_1;
}
}
}
obj* _l_s3_iff_s9_decidable(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s3_iff_s9_decidable_s6___rarg), 2, 0);
return x_4;
}
}
obj* _l_s3_xor_s9_decidable_s6___rarg(obj* x_0, obj* x_1) {
{

if (lean::obj_tag(x_0) == 0)
{

lean::dec(x_0);
return x_1;
}
else
{

lean::dec(x_0);
if (lean::obj_tag(x_1) == 0)
{
obj* x_5; 
lean::dec(x_1);
x_5 = lean::alloc_cnstr(1, 0, 0);
;
return x_5;
}
else
{
obj* x_7; 
lean::dec(x_1);
x_7 = lean::alloc_cnstr(0, 0, 0);
;
return x_7;
}
}
}
}
obj* _l_s3_xor_s9_decidable(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s3_xor_s9_decidable_s6___rarg), 2, 0);
return x_4;
}
}
obj* _l_s23_exists__prop__decidable_s6___rarg(obj* x_0, obj* x_1) {
{

if (lean::obj_tag(x_0) == 0)
{
obj* x_4; 
lean::dec(x_0);
lean::dec(x_1);
x_4 = lean::alloc_cnstr(0, 0, 0);
;
return x_4;
}
else
{
obj* x_6; 
lean::dec(x_0);
x_6 = lean::apply_1(x_1, lean::box(0));
return x_6;
}
}
}
obj* _l_s23_exists__prop__decidable(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s23_exists__prop__decidable_s6___rarg), 2, 0);
return x_4;
}
}
obj* _l_s23_forall__prop__decidable_s6___rarg(obj* x_0, obj* x_1) {
{

if (lean::obj_tag(x_0) == 0)
{
obj* x_4; 
lean::dec(x_0);
lean::dec(x_1);
x_4 = lean::alloc_cnstr(1, 0, 0);
;
return x_4;
}
else
{
obj* x_6; 
lean::dec(x_0);
x_6 = lean::apply_1(x_1, lean::box(0));
return x_6;
}
}
}
obj* _l_s23_forall__prop__decidable(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s23_forall__prop__decidable_s6___rarg), 2, 0);
return x_4;
}
}
obj* _l_s2_ne_s9_decidable_s6___rarg(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_3; 
x_3 = lean::apply_2(x_0, x_1, x_2);
if (lean::obj_tag(x_3) == 0)
{
obj* x_5; 
lean::dec(x_3);
x_5 = lean::alloc_cnstr(1, 0, 0);
;
return x_5;
}
else
{
obj* x_7; 
lean::dec(x_3);
x_7 = lean::alloc_cnstr(0, 0, 0);
;
return x_7;
}
}
}
obj* _l_s2_ne_s9_decidable(obj* x_0) {
{
obj* x_2; 
lean::dec(x_0);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s2_ne_s9_decidable_s6___rarg), 3, 0);
return x_2;
}
}
obj* _init__l_s11_is__dec__eq() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s13_is__dec__refl() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _l_s4_bool_s13_decidable__eq(unsigned char x_0, unsigned char x_1) {
{

if (x_0 == 0)
{

if (x_1 == 0)
{
obj* x_2; 
x_2 = lean::alloc_cnstr(1, 0, 0);
;
return x_2;
}
else
{
obj* x_3; 
x_3 = lean::alloc_cnstr(0, 0, 0);
;
return x_3;
}
}
else
{
obj* x_4; 
x_4 = lean::box(x_1);
return x_4;
}
}
}
obj* _l_s4_bool_s13_decidable__eq_s7___boxed(obj* x_0, obj* x_1) {
{
unsigned char x_2; unsigned char x_3; obj* x_4; 
x_2 = lean::unbox(x_0);
x_3 = lean::unbox(x_1);
x_4 = _l_s4_bool_s13_decidable__eq(x_2, x_3);
return x_4;
}
}
obj* _l_s29_decidable__eq__of__bool__pred_s6___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
{
obj* x_7; 
lean::dec(x_2);
lean::dec(x_1);
x_7 = lean::apply_2(x_0, x_3, x_4);
return x_7;
}
}
obj* _l_s29_decidable__eq__of__bool__pred(obj* x_0) {
{
obj* x_2; 
lean::dec(x_0);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s29_decidable__eq__of__bool__pred_s6___rarg), 5, 0);
return x_2;
}
}
obj* _l_s3_ite_s9_decidable_s6___rarg(obj* x_0, obj* x_1, obj* x_2) {
{

if (lean::obj_tag(x_0) == 0)
{

lean::dec(x_0);
lean::dec(x_1);
return x_2;
}
else
{

lean::dec(x_0);
lean::dec(x_2);
return x_1;
}
}
}
obj* _l_s3_ite_s9_decidable(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_6; 
lean::dec(x_2);
lean::dec(x_1);
lean::dec(x_0);
x_6 = lean::alloc_closure(reinterpret_cast<void*>(_l_s3_ite_s9_decidable_s6___rarg), 3, 0);
return x_6;
}
}
obj* _l_s4_dite_s9_decidable_s6___rarg(obj* x_0, obj* x_1, obj* x_2) {
{

if (lean::obj_tag(x_0) == 0)
{
obj* x_5; 
lean::dec(x_0);
lean::dec(x_1);
x_5 = lean::apply_1(x_2, lean::box(0));
return x_5;
}
else
{
obj* x_8; 
lean::dec(x_0);
lean::dec(x_2);
x_8 = lean::apply_1(x_1, lean::box(0));
return x_8;
}
}
}
obj* _l_s4_dite_s9_decidable(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_6; 
lean::dec(x_2);
lean::dec(x_1);
lean::dec(x_0);
x_6 = lean::alloc_closure(reinterpret_cast<void*>(_l_s4_dite_s9_decidable_s6___rarg), 3, 0);
return x_6;
}
}
obj* _init__l_s8_as__true() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s9_as__false() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s12_of__as__true() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _l_s7_default_s6___rarg(obj* x_0) {
{

return x_0;
}
}
obj* _l_s7_default(obj* x_0) {
{
obj* x_2; 
lean::dec(x_0);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s7_default_s6___rarg), 1, 0);
return x_2;
}
}
obj* _l_s9_arbitrary_s6___rarg(obj* x_0) {
{

return x_0;
}
}
obj* _l_s9_arbitrary(obj* x_0) {
{
obj* x_2; 
lean::dec(x_0);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s9_arbitrary_s6___rarg), 1, 0);
return x_2;
}
}
obj* _init__l_s4_prop_s9_inhabited() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _l_s3_fun_s9_inhabited_s6___rarg(obj* x_0, obj* x_1) {
{

lean::dec(x_1);
return x_0;
}
}
obj* _l_s3_fun_s9_inhabited(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s3_fun_s9_inhabited_s6___rarg), 2, 0);
return x_4;
}
}
obj* _l_s2_pi_s9_inhabited_s6___rarg(obj* x_0, obj* x_1) {
{
obj* x_2; 
x_2 = lean::apply_1(x_0, x_1);
return x_2;
}
}
obj* _l_s2_pi_s9_inhabited(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s2_pi_s9_inhabited_s6___rarg), 2, 0);
return x_4;
}
}
unsigned char _init__l_s4_bool_s9_inhabited() {
{
unsigned char x_0; 
x_0 = 0;
return x_0;
}
}
obj* _init__l_s4_bool_s9_inhabited_s7___boxed() {
{
unsigned char x_0; obj* x_1; 
x_0 = _l_s4_bool_s9_inhabited;
x_1 = lean::box(x_0);
return x_1;
}
}
obj* _init__l_s4_true_s9_inhabited() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s3_nat_s9_inhabited() {
{
obj* x_0; 
x_0 = lean::mk_nat_obj(0u);
return x_0;
}
}
obj* _init__l_s8_nonempty_s4_elim() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s23_nonempty__of__inhabited() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s12_subsingleton_s4_elim() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s12_subsingleton_s5_helim() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s18_subsingleton__prop() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s9_decidable_s12_subsingleton() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s9_reflexive() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s9_symmetric() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s10_transitive() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s11_equivalence() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s5_total() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s15_mk__equivalence() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s11_irreflexive() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s15_anti__symmetric() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s15_empty__relation() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s11_subrelation() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s10_inv__image() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s11_commutative() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s11_associative() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s14_left__identity() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s15_right__identity() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s14_right__inverse() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s17_left__cancelative() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s18_right__cancelative() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s18_left__distributive() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s19_right__distributive() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s18_right__commutative() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s17_left__commutative() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s7_subtype_s19_exists__of__subtype_s6___main() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s7_subtype_s19_exists__of__subtype() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _l_s7_subtype_s9_inhabited_s6___rarg(obj* x_0, obj* x_1) {
{

lean::dec(x_1);
return x_0;
}
}
obj* _l_s7_subtype_s9_inhabited(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s7_subtype_s9_inhabited_s6___rarg), 2, 0);
return x_4;
}
}
obj* _l_s7_subtype_s13_decidable__eq_s6___rarg(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_3; 
x_3 = lean::apply_2(x_0, x_1, x_2);
return x_3;
}
}
obj* _l_s7_subtype_s13_decidable__eq(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s7_subtype_s13_decidable__eq_s6___rarg), 3, 0);
return x_4;
}
}
obj* _l_s3_sum_s15_inhabited__left_s6___rarg(obj* x_0) {
{
obj* x_1; 
x_1 = lean::alloc_cnstr(0, 1, 0);
lean::cnstr_set(x_1, 0, x_0);
return x_1;
}
}
obj* _l_s3_sum_s15_inhabited__left(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s3_sum_s15_inhabited__left_s6___rarg), 1, 0);
return x_4;
}
}
obj* _l_s3_sum_s16_inhabited__right_s6___rarg(obj* x_0) {
{
obj* x_1; 
x_1 = lean::alloc_cnstr(1, 1, 0);
lean::cnstr_set(x_1, 0, x_0);
return x_1;
}
}
obj* _l_s3_sum_s16_inhabited__right(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s3_sum_s16_inhabited__right_s6___rarg), 1, 0);
return x_4;
}
}
obj* _l_s3_sum_s13_decidable__eq_s6___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
{

if (lean::obj_tag(x_2) == 0)
{
obj* x_5; 
lean::dec(x_1);
x_5 = lean::cnstr_get(x_2, 0);
lean::inc(x_5);
lean::dec(x_2);
if (lean::obj_tag(x_3) == 0)
{
obj* x_8; obj* x_11; 
x_8 = lean::cnstr_get(x_3, 0);
lean::inc(x_8);
lean::dec(x_3);
x_11 = lean::apply_2(x_0, x_5, x_8);
return x_11;
}
else
{
obj* x_15; 
lean::dec(x_5);
lean::dec(x_0);
lean::dec(x_3);
x_15 = lean::alloc_cnstr(0, 0, 0);
;
return x_15;
}
}
else
{
obj* x_17; 
lean::dec(x_0);
x_17 = lean::cnstr_get(x_2, 0);
lean::inc(x_17);
lean::dec(x_2);
if (lean::obj_tag(x_3) == 0)
{
obj* x_23; 
lean::dec(x_1);
lean::dec(x_3);
lean::dec(x_17);
x_23 = lean::alloc_cnstr(0, 0, 0);
;
return x_23;
}
else
{
obj* x_24; obj* x_27; 
x_24 = lean::cnstr_get(x_3, 0);
lean::inc(x_24);
lean::dec(x_3);
x_27 = lean::apply_2(x_1, x_17, x_24);
return x_27;
}
}
}
}
obj* _l_s3_sum_s13_decidable__eq(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s3_sum_s13_decidable__eq_s6___rarg), 4, 0);
return x_4;
}
}
obj* _l_s4_prod_s9_inhabited_s6___rarg(obj* x_0, obj* x_1) {
{
obj* x_2; 
x_2 = lean::alloc_cnstr(0, 2, 0);
lean::cnstr_set(x_2, 0, x_0);
lean::cnstr_set(x_2, 1, x_1);
return x_2;
}
}
obj* _l_s4_prod_s9_inhabited(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s4_prod_s9_inhabited_s6___rarg), 2, 0);
return x_4;
}
}
obj* _l_s4_prod_s13_decidable__eq_s6___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
{
obj* x_4; obj* x_6; obj* x_9; obj* x_11; obj* x_14; 
x_4 = lean::cnstr_get(x_2, 0);
lean::inc(x_4);
x_6 = lean::cnstr_get(x_2, 1);
lean::inc(x_6);
lean::dec(x_2);
x_9 = lean::cnstr_get(x_3, 0);
lean::inc(x_9);
x_11 = lean::cnstr_get(x_3, 1);
lean::inc(x_11);
lean::dec(x_3);
x_14 = lean::apply_2(x_0, x_4, x_9);
if (lean::obj_tag(x_14) == 0)
{
obj* x_19; 
lean::dec(x_14);
lean::dec(x_6);
lean::dec(x_11);
lean::dec(x_1);
x_19 = lean::alloc_cnstr(0, 0, 0);
;
return x_19;
}
else
{
obj* x_21; 
lean::dec(x_14);
x_21 = lean::apply_2(x_1, x_6, x_11);
return x_21;
}
}
}
obj* _l_s4_prod_s13_decidable__eq(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s4_prod_s13_decidable__eq_s6___rarg), 4, 0);
return x_4;
}
}
obj* _l_s4_prod_s7_has__lt(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
{
obj* x_8; 
lean::dec(x_3);
lean::dec(x_2);
lean::dec(x_1);
lean::dec(x_0);
x_8 = lean::alloc_cnstr(0, 0, 0);
;
return x_8;
}
}
obj* _l_s24_prod__has__decidable__lt_s6___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
{
obj* x_7; obj* x_9; obj* x_13; 
lean::dec(x_1);
x_7 = lean::cnstr_get(x_4, 0);
lean::inc(x_7);
x_9 = lean::cnstr_get(x_5, 0);
lean::inc(x_9);
lean::inc(x_9);
lean::inc(x_7);
x_13 = lean::apply_2(x_2, x_7, x_9);
if (lean::obj_tag(x_13) == 0)
{
obj* x_15; 
lean::dec(x_13);
x_15 = lean::apply_2(x_0, x_7, x_9);
if (lean::obj_tag(x_15) == 0)
{
obj* x_20; 
lean::dec(x_15);
lean::dec(x_4);
lean::dec(x_5);
lean::dec(x_3);
x_20 = lean::alloc_cnstr(0, 0, 0);
;
return x_20;
}
else
{
obj* x_22; obj* x_25; obj* x_28; 
lean::dec(x_15);
x_22 = lean::cnstr_get(x_4, 1);
lean::inc(x_22);
lean::dec(x_4);
x_25 = lean::cnstr_get(x_5, 1);
lean::inc(x_25);
lean::dec(x_5);
x_28 = lean::apply_2(x_3, x_22, x_25);
return x_28;
}
}
else
{
obj* x_36; 
lean::dec(x_13);
lean::dec(x_4);
lean::dec(x_5);
lean::dec(x_7);
lean::dec(x_9);
lean::dec(x_0);
lean::dec(x_3);
x_36 = lean::alloc_cnstr(1, 0, 0);
;
return x_36;
}
}
}
obj* _l_s24_prod__has__decidable__lt(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
{
obj* x_8; 
lean::dec(x_3);
lean::dec(x_2);
lean::dec(x_1);
lean::dec(x_0);
x_8 = lean::alloc_closure(reinterpret_cast<void*>(_l_s24_prod__has__decidable__lt_s6___rarg), 6, 0);
return x_8;
}
}
obj* _l_s4_prod_s3_map_s6___main_s6___rarg(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_3; obj* x_5; obj* x_7; obj* x_8; obj* x_9; obj* x_10; 
x_3 = lean::cnstr_get(x_2, 0);
lean::inc(x_3);
x_5 = lean::cnstr_get(x_2, 1);
lean::inc(x_5);
if (lean::is_shared(x_2)) {
 lean::dec(x_2);
 x_7 = lean::box(0);
} else {
 lean::cnstr_release(x_2, 0);
 lean::cnstr_release(x_2, 1);
 x_7 = x_2;
}
x_8 = lean::apply_1(x_0, x_3);
x_9 = lean::apply_1(x_1, x_5);
if (lean::is_scalar(x_7)) {
 x_10 = lean::alloc_cnstr(0, 2, 0);
} else {
 x_10 = x_7;
}
lean::cnstr_set(x_10, 0, x_8);
lean::cnstr_set(x_10, 1, x_9);
return x_10;
}
}
obj* _l_s4_prod_s3_map_s6___main(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
{
obj* x_8; 
lean::dec(x_3);
lean::dec(x_2);
lean::dec(x_1);
lean::dec(x_0);
x_8 = lean::alloc_closure(reinterpret_cast<void*>(_l_s4_prod_s3_map_s6___main_s6___rarg), 3, 0);
return x_8;
}
}
obj* _l_s4_prod_s3_map_s6___rarg(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_3; 
x_3 = _l_s4_prod_s3_map_s6___main_s6___rarg(x_0, x_1, x_2);
return x_3;
}
}
obj* _l_s4_prod_s3_map(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
{
obj* x_8; 
lean::dec(x_3);
lean::dec(x_2);
lean::dec(x_1);
lean::dec(x_0);
x_8 = lean::alloc_closure(reinterpret_cast<void*>(_l_s4_prod_s3_map_s6___rarg), 3, 0);
return x_8;
}
}
obj* _init__l_s5_punit_s12_subsingleton() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
unsigned char _init__l_s5_punit_s9_inhabited() {
{
unsigned char x_0; 
x_0 = 0;
return x_0;
}
}
obj* _init__l_s5_punit_s9_inhabited_s7___boxed() {
{
unsigned char x_0; obj* x_1; 
x_0 = _l_s5_punit_s9_inhabited;
x_1 = lean::box(x_0);
return x_1;
}
}
obj* _l_s5_punit_s13_decidable__eq(unsigned char x_0, unsigned char x_1) {
{
obj* x_2; 
x_2 = lean::alloc_cnstr(1, 0, 0);
;
return x_2;
}
}
obj* _l_s5_punit_s13_decidable__eq_s7___boxed(obj* x_0, obj* x_1) {
{
unsigned char x_2; unsigned char x_3; obj* x_4; 
x_2 = lean::unbox(x_0);
x_3 = lean::unbox(x_1);
x_4 = _l_s5_punit_s13_decidable__eq(x_2, x_3);
return x_4;
}
}
obj* _l_s18_setoid__has__equiv(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_cnstr(0, 0, 0);
;
return x_4;
}
}
obj* _l_s4_quot_s8_lift__on_s6___rarg(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_4; 
lean::dec(x_2);
x_4 = lean::apply_1(x_1, x_0);
return x_4;
}
}
obj* _l_s4_quot_s8_lift__on(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_6; 
lean::dec(x_2);
lean::dec(x_1);
lean::dec(x_0);
x_6 = lean::alloc_closure(reinterpret_cast<void*>(_l_s4_quot_s8_lift__on_s6___rarg), 3, 0);
return x_6;
}
}
obj* _l_s4_quot_s5_indep_s6___rarg(obj* x_0, obj* x_1) {
{
obj* x_3; obj* x_4; 
lean::inc(x_1);
x_3 = lean::apply_1(x_0, x_1);
x_4 = lean::alloc_cnstr(0, 2, 0);
lean::cnstr_set(x_4, 0, x_1);
lean::cnstr_set(x_4, 1, x_3);
return x_4;
}
}
obj* _l_s4_quot_s5_indep(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_6; 
lean::dec(x_2);
lean::dec(x_1);
lean::dec(x_0);
x_6 = lean::alloc_closure(reinterpret_cast<void*>(_l_s4_quot_s5_indep_s6___rarg), 2, 0);
return x_6;
}
}
obj* _l_s4_quot_s3_rec_s6___rarg(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_4; 
lean::dec(x_1);
x_4 = lean::apply_1(x_0, x_2);
return x_4;
}
}
obj* _l_s4_quot_s3_rec(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_6; 
lean::dec(x_2);
lean::dec(x_1);
lean::dec(x_0);
x_6 = lean::alloc_closure(reinterpret_cast<void*>(_l_s4_quot_s3_rec_s6___rarg), 3, 0);
return x_6;
}
}
obj* _l_s4_quot_s7_rec__on_s6___rarg(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_4; 
lean::dec(x_2);
x_4 = lean::apply_1(x_1, x_0);
return x_4;
}
}
obj* _l_s4_quot_s7_rec__on(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_6; 
lean::dec(x_2);
lean::dec(x_1);
lean::dec(x_0);
x_6 = lean::alloc_closure(reinterpret_cast<void*>(_l_s4_quot_s7_rec__on_s6___rarg), 3, 0);
return x_6;
}
}
obj* _l_s4_quot_s21_rec__on__subsingleton_s6___rarg(obj* x_0, obj* x_1) {
{
obj* x_2; 
x_2 = lean::apply_1(x_1, x_0);
return x_2;
}
}
obj* _l_s4_quot_s21_rec__on__subsingleton(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
{
obj* x_8; 
lean::dec(x_3);
lean::dec(x_2);
lean::dec(x_1);
lean::dec(x_0);
x_8 = lean::alloc_closure(reinterpret_cast<void*>(_l_s4_quot_s21_rec__on__subsingleton_s6___rarg), 2, 0);
return x_8;
}
}
obj* _l_s4_quot_s8_hrec__on_s6___rarg(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_4; 
lean::dec(x_2);
x_4 = lean::apply_1(x_1, x_0);
return x_4;
}
}
obj* _l_s4_quot_s8_hrec__on(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_6; 
lean::dec(x_2);
lean::dec(x_1);
lean::dec(x_0);
x_6 = lean::alloc_closure(reinterpret_cast<void*>(_l_s4_quot_s8_hrec__on_s6___rarg), 3, 0);
return x_6;
}
}
obj* _init__l_s8_quotient() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _l_s8_quotient_s2_mk_s6___rarg(obj* x_0) {
{

return x_0;
}
}
obj* _l_s8_quotient_s2_mk(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s8_quotient_s2_mk_s6___rarg), 1, 0);
return x_4;
}
}
obj* _init__l_s8_quotient_s5_sound() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _l_s8_quotient_s4_lift_s6___rarg(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_4; 
lean::dec(x_1);
x_4 = lean::apply_1(x_0, x_2);
return x_4;
}
}
obj* _l_s8_quotient_s4_lift(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_6; 
lean::dec(x_2);
lean::dec(x_1);
lean::dec(x_0);
x_6 = lean::alloc_closure(reinterpret_cast<void*>(_l_s8_quotient_s4_lift_s6___rarg), 3, 0);
return x_6;
}
}
obj* _l_s8_quotient_s8_lift__on_s6___rarg(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_4; 
lean::dec(x_2);
x_4 = lean::apply_1(x_1, x_0);
return x_4;
}
}
obj* _l_s8_quotient_s8_lift__on(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_6; 
lean::dec(x_2);
lean::dec(x_1);
lean::dec(x_0);
x_6 = lean::alloc_closure(reinterpret_cast<void*>(_l_s8_quotient_s8_lift__on_s6___rarg), 3, 0);
return x_6;
}
}
obj* _l_s8_quotient_s3_rec_s6___rarg(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_4; 
lean::dec(x_1);
x_4 = lean::apply_1(x_0, x_2);
return x_4;
}
}
obj* _l_s8_quotient_s3_rec(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_6; 
lean::dec(x_2);
lean::dec(x_1);
lean::dec(x_0);
x_6 = lean::alloc_closure(reinterpret_cast<void*>(_l_s8_quotient_s3_rec_s6___rarg), 3, 0);
return x_6;
}
}
obj* _l_s8_quotient_s7_rec__on_s6___rarg(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_4; 
lean::dec(x_2);
x_4 = lean::apply_1(x_1, x_0);
return x_4;
}
}
obj* _l_s8_quotient_s7_rec__on(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_6; 
lean::dec(x_2);
lean::dec(x_1);
lean::dec(x_0);
x_6 = lean::alloc_closure(reinterpret_cast<void*>(_l_s8_quotient_s7_rec__on_s6___rarg), 3, 0);
return x_6;
}
}
obj* _l_s8_quotient_s21_rec__on__subsingleton_s6___rarg(obj* x_0, obj* x_1) {
{
obj* x_2; 
x_2 = lean::apply_1(x_1, x_0);
return x_2;
}
}
obj* _l_s8_quotient_s21_rec__on__subsingleton(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
{
obj* x_8; 
lean::dec(x_3);
lean::dec(x_2);
lean::dec(x_1);
lean::dec(x_0);
x_8 = lean::alloc_closure(reinterpret_cast<void*>(_l_s8_quotient_s21_rec__on__subsingleton_s6___rarg), 2, 0);
return x_8;
}
}
obj* _l_s8_quotient_s8_hrec__on_s6___rarg(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_4; 
lean::dec(x_2);
x_4 = lean::apply_1(x_1, x_0);
return x_4;
}
}
obj* _l_s8_quotient_s8_hrec__on(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_6; 
lean::dec(x_2);
lean::dec(x_1);
lean::dec(x_0);
x_6 = lean::alloc_closure(reinterpret_cast<void*>(_l_s8_quotient_s8_hrec__on_s6___rarg), 3, 0);
return x_6;
}
}
obj* _l_s8_quotient_s10_lift_u2082_s6___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
{
obj* x_5; 
lean::dec(x_1);
x_5 = lean::apply_2(x_0, x_2, x_3);
return x_5;
}
}
obj* _l_s8_quotient_s10_lift_u2082(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
{
obj* x_10; 
lean::dec(x_4);
lean::dec(x_3);
lean::dec(x_2);
lean::dec(x_1);
lean::dec(x_0);
x_10 = lean::alloc_closure(reinterpret_cast<void*>(_l_s8_quotient_s10_lift_u2082_s6___rarg), 4, 0);
return x_10;
}
}
obj* _l_s8_quotient_s14_lift__on_u2082_s6___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
{
obj* x_5; 
lean::dec(x_3);
x_5 = lean::apply_2(x_2, x_0, x_1);
return x_5;
}
}
obj* _l_s8_quotient_s14_lift__on_u2082(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
{
obj* x_10; 
lean::dec(x_4);
lean::dec(x_3);
lean::dec(x_2);
lean::dec(x_1);
lean::dec(x_0);
x_10 = lean::alloc_closure(reinterpret_cast<void*>(_l_s8_quotient_s14_lift__on_u2082_s6___rarg), 4, 0);
return x_10;
}
}
obj* _init__l_s9___private_1845649337__s3_rel() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _l_s8_quotient_s27_rec__on__subsingleton_u2082_s6___rarg(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_3; 
x_3 = lean::apply_2(x_2, x_0, x_1);
return x_3;
}
}
obj* _l_s8_quotient_s27_rec__on__subsingleton_u2082(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
{
obj* x_12; 
lean::dec(x_5);
lean::dec(x_4);
lean::dec(x_3);
lean::dec(x_2);
lean::dec(x_1);
lean::dec(x_0);
x_12 = lean::alloc_closure(reinterpret_cast<void*>(_l_s8_quotient_s27_rec__on__subsingleton_u2082_s6___rarg), 3, 0);
return x_12;
}
}
obj* _l_s8_eqv__gen_s6_setoid(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_cnstr(0, 0, 0);
;
return x_4;
}
}
obj* _l_s8_quotient_s13_decidable__eq_s6___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
{
obj* x_5; 
lean::dec(x_0);
x_5 = _l_s8_quotient_s13_decidable__eq_s6___rarg_s11___lambda__1(x_1, x_2, x_3);
return x_5;
}
}
obj* _l_s8_quotient_s13_decidable__eq_s6___rarg_s11___lambda__1(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_3; 
x_3 = lean::apply_2(x_0, x_1, x_2);
return x_3;
}
}
obj* _l_s8_quotient_s13_decidable__eq(obj* x_0) {
{
obj* x_2; 
lean::dec(x_0);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(_l_s8_quotient_s13_decidable__eq_s6___rarg), 4, 0);
return x_2;
}
}
obj* _l_s8_quotient_s27_rec__on__subsingleton_u2082_s4___at_s8_quotient_s13_decidable__eq_s9___spec__1_s6___rarg(obj* x_0, obj* x_1, obj* x_2) {
{
obj* x_3; 
x_3 = lean::apply_2(x_2, x_0, x_1);
return x_3;
}
}
obj* _l_s8_quotient_s27_rec__on__subsingleton_u2082_s4___at_s8_quotient_s13_decidable__eq_s9___spec__1(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s8_quotient_s27_rec__on__subsingleton_u2082_s4___at_s8_quotient_s13_decidable__eq_s9___spec__1_s6___rarg), 3, 0);
return x_4;
}
}
obj* _init__l_s8_function_s5_equiv() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _l_s9___private_1944762901__s11_fun__setoid(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_cnstr(0, 0, 0);
;
return x_4;
}
}
obj* _init__l_s9___private_1597490181__s6_extfun() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _l_s9___private_3425436377__s15_fun__to__extfun_s6___rarg(obj* x_0) {
{

return x_0;
}
}
obj* _l_s9___private_3425436377__s15_fun__to__extfun(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s9___private_3425436377__s15_fun__to__extfun_s6___rarg), 1, 0);
return x_4;
}
}
obj* _l_s9___private_2312050019__s11_extfun__app_s6___rarg(obj* x_0, obj* x_1) {
{
obj* x_2; 
x_2 = lean::apply_1(x_0, x_1);
return x_2;
}
}
obj* _l_s9___private_2312050019__s11_extfun__app(obj* x_0, obj* x_1) {
{
obj* x_4; 
lean::dec(x_1);
lean::dec(x_0);
x_4 = lean::alloc_closure(reinterpret_cast<void*>(_l_s9___private_2312050019__s11_extfun__app_s6___rarg), 2, 0);
return x_4;
}
}
obj* _init__l_s2_pi_s12_subsingleton() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
obj* _init__l_s9_classical_s9_by__cases() {
{
obj* x_0; 
x_0 = lean::box(0);
lean::inc(x_0);
return x_0;
}
}
static bool _G_initialized = false;
void _l_initialize__l_s4_init_s4_core() {
 if (_G_initialized) return;
 _G_initialized = true;
 _l_s10_opt__param = _init__l_s10_opt__param();
 _l_s10_out__param = _init__l_s10_out__param();
 _l_s4_unit = _init__l_s4_unit();
 _l_s4_unit_s4_star = _init__l_s4_unit_s4_star();
 _l_s4_unit_s4_star_s7___boxed = _init__l_s4_unit_s4_star_s7___boxed();
 _l_s3_not = _init__l_s3_not();
 _l_s3_and_s10_elim__left = _init__l_s3_and_s10_elim__left();
 _l_s3_and_s11_elim__right = _init__l_s3_and_s11_elim__right();
 _l_s3_rfl = _init__l_s3_rfl();
 _l_s3_heq_s3_rfl = _init__l_s3_heq_s3_rfl();
 _l_s2_or_s11_intro__left = _init__l_s2_or_s11_intro__left();
 _l_s2_or_s12_intro__right = _init__l_s2_or_s12_intro__right();
 _l_s15_decidable__pred = _init__l_s15_decidable__pred();
 _l_s14_decidable__rel = _init__l_s14_decidable__rel();
 _l_s2_ge = _init__l_s2_ge();
 _l_s2_gt = _init__l_s2_gt();
 _l_s8_superset = _init__l_s8_superset();
 _l_s9_ssuperset = _init__l_s9_ssuperset();
 _l_s3_nat_s9_has__zero = _init__l_s3_nat_s9_has__zero();
 _l_s3_nat_s8_has__one = _init__l_s3_nat_s8_has__one();
 _l_s3_nat_s8_has__add = _init__l_s3_nat_s8_has__add();
 _l_s3_std_s8_priority_s7_default = _init__l_s3_std_s8_priority_s7_default();
 _l_s3_std_s8_priority_s3_max = _init__l_s3_std_s8_priority_s3_max();
 _l_s3_nat_s4_prio = _init__l_s3_nat_s4_prio();
 _l_s3_std_s4_prec_s3_max = _init__l_s3_std_s4_prec_s3_max();
 _l_s3_std_s4_prec_s5_arrow = _init__l_s3_std_s4_prec_s5_arrow();
 _l_s3_std_s4_prec_s9_max__plus = _init__l_s3_std_s4_prec_s9_max__plus();
 _l_s20_default__has__sizeof_s11___closed__1 = _init__l_s20_default__has__sizeof_s11___closed__1();
 _l_s3_nat_s11_has__sizeof = _init__l_s3_nat_s11_has__sizeof();
 _l_s5_punit_s11_has__sizeof = _init__l_s5_punit_s11_has__sizeof();
 _l_s4_bool_s11_has__sizeof = _init__l_s4_bool_s11_has__sizeof();
 _l_s7_implies = _init__l_s7_implies();
 _l_s7_trivial = _init__l_s7_trivial();
 _l_s2_ne = _init__l_s2_ne();
 _l_s17_type__eq__of__heq = _init__l_s17_type__eq__of__heq();
 _l_s3_and_s4_symm = _init__l_s3_and_s4_symm();
 _l_s12_not__not__em = _init__l_s12_not__not__em();
 _l_s2_or_s4_symm = _init__l_s2_or_s4_symm();
 _l_s3_xor = _init__l_s3_xor();
 _l_s14_not__true__iff = _init__l_s14_not__true__iff();
 _l_s12_and__implies = _init__l_s12_and__implies();
 _l_s6_exists_s5_intro = _init__l_s6_exists_s5_intro();
 _l_s4_true_s9_decidable = _init__l_s4_true_s9_decidable();
 _l_s5_false_s9_decidable = _init__l_s5_false_s9_decidable();
 _l_s11_is__dec__eq = _init__l_s11_is__dec__eq();
 _l_s13_is__dec__refl = _init__l_s13_is__dec__refl();
 _l_s8_as__true = _init__l_s8_as__true();
 _l_s9_as__false = _init__l_s9_as__false();
 _l_s12_of__as__true = _init__l_s12_of__as__true();
 _l_s4_prop_s9_inhabited = _init__l_s4_prop_s9_inhabited();
 _l_s4_bool_s9_inhabited = _init__l_s4_bool_s9_inhabited();
 _l_s4_bool_s9_inhabited_s7___boxed = _init__l_s4_bool_s9_inhabited_s7___boxed();
 _l_s4_true_s9_inhabited = _init__l_s4_true_s9_inhabited();
 _l_s3_nat_s9_inhabited = _init__l_s3_nat_s9_inhabited();
 _l_s8_nonempty_s4_elim = _init__l_s8_nonempty_s4_elim();
 _l_s23_nonempty__of__inhabited = _init__l_s23_nonempty__of__inhabited();
 _l_s12_subsingleton_s4_elim = _init__l_s12_subsingleton_s4_elim();
 _l_s12_subsingleton_s5_helim = _init__l_s12_subsingleton_s5_helim();
 _l_s18_subsingleton__prop = _init__l_s18_subsingleton__prop();
 _l_s9_decidable_s12_subsingleton = _init__l_s9_decidable_s12_subsingleton();
 _l_s9_reflexive = _init__l_s9_reflexive();
 _l_s9_symmetric = _init__l_s9_symmetric();
 _l_s10_transitive = _init__l_s10_transitive();
 _l_s11_equivalence = _init__l_s11_equivalence();
 _l_s5_total = _init__l_s5_total();
 _l_s15_mk__equivalence = _init__l_s15_mk__equivalence();
 _l_s11_irreflexive = _init__l_s11_irreflexive();
 _l_s15_anti__symmetric = _init__l_s15_anti__symmetric();
 _l_s15_empty__relation = _init__l_s15_empty__relation();
 _l_s11_subrelation = _init__l_s11_subrelation();
 _l_s10_inv__image = _init__l_s10_inv__image();
 _l_s11_commutative = _init__l_s11_commutative();
 _l_s11_associative = _init__l_s11_associative();
 _l_s14_left__identity = _init__l_s14_left__identity();
 _l_s15_right__identity = _init__l_s15_right__identity();
 _l_s14_right__inverse = _init__l_s14_right__inverse();
 _l_s17_left__cancelative = _init__l_s17_left__cancelative();
 _l_s18_right__cancelative = _init__l_s18_right__cancelative();
 _l_s18_left__distributive = _init__l_s18_left__distributive();
 _l_s19_right__distributive = _init__l_s19_right__distributive();
 _l_s18_right__commutative = _init__l_s18_right__commutative();
 _l_s17_left__commutative = _init__l_s17_left__commutative();
 _l_s7_subtype_s19_exists__of__subtype_s6___main = _init__l_s7_subtype_s19_exists__of__subtype_s6___main();
 _l_s7_subtype_s19_exists__of__subtype = _init__l_s7_subtype_s19_exists__of__subtype();
 _l_s5_punit_s12_subsingleton = _init__l_s5_punit_s12_subsingleton();
 _l_s5_punit_s9_inhabited = _init__l_s5_punit_s9_inhabited();
 _l_s5_punit_s9_inhabited_s7___boxed = _init__l_s5_punit_s9_inhabited_s7___boxed();
 _l_s8_quotient = _init__l_s8_quotient();
 _l_s8_quotient_s5_sound = _init__l_s8_quotient_s5_sound();
 _l_s9___private_1845649337__s3_rel = _init__l_s9___private_1845649337__s3_rel();
 _l_s8_function_s5_equiv = _init__l_s8_function_s5_equiv();
 _l_s9___private_1597490181__s6_extfun = _init__l_s9___private_1597490181__s6_extfun();
 _l_s2_pi_s12_subsingleton = _init__l_s2_pi_s12_subsingleton();
 _l_s9_classical_s9_by__cases = _init__l_s9_classical_s9_by__cases();
}