# Generated by tools/translator: qualified upstream name -> MoonBit name.
BIJECTIVE_INJECTIVE_SURJECTIVE bijective_injective_surjective
BIJECTIVE_INVERSES bijective_inverses
CANTOR_THM cantor_thm
CANTOR_THM_UNIV cantor_thm_univ
CARD_ADD2_ABSORB_LE card_add2_absorb_le
CARD_ADD2_ABSORB_LT card_add2_absorb_lt
CARD_ADD_ABSORB_LE card_add_absorb_le
CARD_ADD_ABSORB_LEFT card_add_absorb_left
CARD_ADD_ABSORB_RIGHT card_add_absorb_right
CARD_ADD_ASSOC card_add_assoc
CARD_ADD_C card_add_c
CARD_ADD_CONG card_add_cong
CARD_ADD_FINITE card_add_finite
CARD_ADD_FINITE_EQ card_add_finite_eq
CARD_ADD_LE_MUL_INFINITE card_add_le_mul_infinite
CARD_ADD_SYM card_add_sym
CARD_COUNTABLE_CONG card_countable_cong
CARD_DIFF_ABSORB card_diff_absorb
CARD_DIFF_CONG card_diff_cong
CARD_DISJOINT_UNION card_disjoint_union
CARD_EMPTY_LE card_empty_le
CARD_EQ_ADD_LCANCEL card_eq_add_lcancel
CARD_EQ_ADD_LCANCEL_EQ card_eq_add_lcancel_eq
CARD_EQ_ADD_RCANCEL card_eq_add_rcancel
CARD_EQ_ADD_RCANCEL_EQ card_eq_add_rcancel_eq
CARD_EQ_CARD card_eq_card
CARD_EQ_CARD_IMP card_eq_card_imp
CARD_EQ_CART card_eq_cart
CARD_EQ_CARTESIAN_PRODUCT card_eq_cartesian_product
CARD_EQ_CARTESIAN_PRODUCT_DISJOINT_UNION card_eq_cartesian_product_disjoint_union
CARD_EQ_CONG card_eq_cong
CARD_EQ_COUNTABLE card_eq_countable
CARD_EQ_COUNTABLE_SUBSETS_REAL card_eq_countable_subsets_real
CARD_EQ_COUNTABLE_SUBSETS_SUBREAL card_eq_countable_subsets_subreal
CARD_EQ_DISJOINT_UNIONS card_eq_disjoint_unions
CARD_EQ_EMPTY card_eq_empty
CARD_EQ_EXP_INFINITE_FINITE card_eq_exp_infinite_finite
CARD_EQ_FINITE card_eq_finite
CARD_EQ_FINITE_SUBSETS card_eq_finite_subsets
CARD_EQ_FULLSIZE_POWERSET card_eq_fullsize_powerset
CARD_EQ_FUNSPACE card_eq_funspace
CARD_EQ_IMAGE card_eq_image
CARD_EQ_IMAGES card_eq_images
CARD_EQ_IMAGE_MUL_FIBRES card_eq_image_mul_fibres
CARD_EQ_IMP_LE card_eq_imp_le
CARD_EQ_INFINITE card_eq_infinite
CARD_EQ_INT_NUM card_eq_int_num
CARD_EQ_LIMITED_POWERSET card_eq_limited_powerset
CARD_EQ_LIST card_eq_list
CARD_EQ_LIST_GEN card_eq_list_gen
CARD_EQ_ORDINAL_EXISTS card_eq_ordinal_exists
CARD_EQ_PCROSS card_eq_pcross
CARD_EQ_PREIMAGE card_eq_preimage
CARD_EQ_REAL card_eq_real
CARD_EQ_REAL_IMP_UNCOUNTABLE card_eq_real_imp_uncountable
CARD_EQ_REAL_SEQUENCES card_eq_real_sequences
CARD_EQ_REAL_SUBSET card_eq_real_subset
CARD_EQ_REFL card_eq_refl
CARD_EQ_REFL_IMP card_eq_refl_imp
CARD_EQ_RESTRICTED_FUNSPACE_INFINITE card_eq_restricted_funspace_infinite
CARD_EQ_RESTRICTED_POWERSET card_eq_restricted_powerset
CARD_EQ_SYM card_eq_sym
CARD_EQ_TRANS card_eq_trans
CARD_EXP_0 card_exp_0
CARD_EXP_ABSORB card_exp_absorb
CARD_EXP_ADD card_exp_add
CARD_EXP_C card_exp_c
CARD_EXP_CANTOR card_exp_cantor
CARD_EXP_CONG card_exp_cong
CARD_EXP_EQ_REAL card_exp_eq_real
CARD_EXP_FINITE card_exp_finite
CARD_EXP_FINITE_EQ card_exp_finite_eq
CARD_EXP_GRAPH card_exp_graph
CARD_EXP_GRAPH_PAIRED card_exp_graph_paired
CARD_EXP_LE_REAL card_exp_le_real
CARD_EXP_MUL card_exp_mul
CARD_EXP_POWERSET card_exp_powerset
CARD_EXP_SING card_exp_sing
CARD_EXP_UNIV card_exp_univ
CARD_EXP_ZERO card_exp_zero
CARD_FINITE_CONG card_finite_cong
CARD_FUNSPACE_CONG card_funspace_cong
CARD_FUNSPACE_CURRY card_funspace_curry
CARD_FUNSPACE_LE card_funspace_le
CARD_GE_PREIMAGE card_ge_preimage
CARD_HAS_SIZE_CONG card_has_size_cong
CARD_INFINITE_CONG card_infinite_cong
CARD_LDISTRIB card_ldistrib
CARD_LET_TOTAL card_let_total
CARD_LET_TRANS card_let_trans
CARD_LE_ADD card_le_add
CARD_LE_ADDL card_le_addl
CARD_LE_ADDR card_le_addr
CARD_LE_ADD_LCANCEL card_le_add_lcancel
CARD_LE_ADD_LCANCEL_EQ card_le_add_lcancel_eq
CARD_LE_ADD_RCANCEL card_le_add_rcancel
CARD_LE_ADD_RCANCEL_EQ card_le_add_rcancel_eq
CARD_LE_ANTISYM card_le_antisym
CARD_LE_CARD card_le_card
CARD_LE_CARD_IMP card_le_card_imp
CARD_LE_CARTESIAN_PRODUCT card_le_cartesian_product
CARD_LE_CARTESIAN_PRODUCT_SUBINDEX card_le_cartesian_product_subindex
CARD_LE_CONG card_le_cong
CARD_LE_COUNTABLE card_le_countable
CARD_LE_COUNTABLE_INFINITE card_le_countable_infinite
CARD_LE_COUNTABLE_SUBSETS card_le_countable_subsets
CARD_LE_DISJOINT_UNIONS card_le_disjoint_unions
CARD_LE_EMPTY card_le_empty
CARD_LE_EQ_SUBSET card_le_eq_subset
CARD_LE_EQ_SUBSET_UNIV card_le_eq_subset_univ
CARD_LE_EXISTS card_le_exists
CARD_LE_EXP card_le_exp
CARD_LE_EXP_LEFT card_le_exp_left
CARD_LE_EXP_RIGHT card_le_exp_right
CARD_LE_FINITE card_le_finite
CARD_LE_FINITE_INFINITE card_le_finite_infinite
CARD_LE_FINITE_SUBSETS card_le_finite_subsets
CARD_LE_IMAGE card_le_image
CARD_LE_IMAGES card_le_images
CARD_LE_IMAGE_GEN card_le_image_gen
CARD_LE_INFINITE card_le_infinite
CARD_LE_LIST card_le_list
CARD_LE_LT card_le_lt
CARD_LE_MUL card_le_mul
CARD_LE_POWERSET card_le_powerset
CARD_LE_PREIMAGE card_le_preimage
CARD_LE_REFL card_le_refl
CARD_LE_RELATIONAL card_le_relational
CARD_LE_RELATIONAL_FULL card_le_relational_full
CARD_LE_RESTRICTED_FUNSPACE card_le_restricted_funspace
CARD_LE_RESTRICTED_FUNSPACE_INFINITE card_le_restricted_funspace_infinite
CARD_LE_SING card_le_sing
CARD_LE_SQUARE card_le_square
CARD_LE_SUBPOWERSET card_le_subpowerset
CARD_LE_SUBSET card_le_subset
CARD_LE_TOTAL card_le_total
CARD_LE_TRANS card_le_trans
CARD_LE_UNIONS card_le_unions
CARD_LE_UNIONS2 card_le_unions2
CARD_LE_UNIV card_le_univ
CARD_LTE_TOTAL card_lte_total
CARD_LTE_TRANS card_lte_trans
CARD_LT_ADD card_lt_add
CARD_LT_CARD card_lt_card
CARD_LT_CONG card_lt_cong
CARD_LT_COUNTABLE_UNCOUNTABLE card_lt_countable_uncountable
CARD_LT_FINITE_INFINITE card_lt_finite_infinite
CARD_LT_IMP_LE card_lt_imp_le
CARD_LT_IMP_SUC_LE card_lt_imp_suc_le
CARD_LT_LE card_lt_le
CARD_LT_NUM_REAL card_lt_num_real
CARD_LT_REFL card_lt_refl
CARD_LT_TOTAL card_lt_total
CARD_LT_TRANS card_lt_trans
CARD_MUL2_ABSORB_LE card_mul2_absorb_le
CARD_MUL2_ABSORB_LE_ALT card_mul2_absorb_le_alt
CARD_MUL_ABSORB card_mul_absorb
CARD_MUL_ABSORB_LE card_mul_absorb_le
CARD_MUL_ASSOC card_mul_assoc
CARD_MUL_C card_mul_c
CARD_MUL_CONG card_mul_cong
CARD_MUL_EXP card_mul_exp
CARD_MUL_FINITE card_mul_finite
CARD_MUL_FINITE_EQ card_mul_finite_eq
CARD_MUL_LID card_mul_lid
CARD_MUL_LT_INFINITE card_mul_lt_infinite
CARD_MUL_LT_LEMMA card_mul_lt_lemma
CARD_MUL_RID card_mul_rid
CARD_MUL_SYM card_mul_sym
CARD_NOT_LE card_not_le
CARD_NOT_LT card_not_lt
CARD_POWERSET_CONG card_powerset_cong
CARD_RDISTRIB card_rdistrib
CARD_SING_LE card_sing_le
CARD_SQUARE_INFINITE card_square_infinite
CARD_SQUARE_NUM card_square_num
CARD_UNION_ABSORB_LEFT card_union_absorb_left
CARD_UNION_ABSORB_RIGHT card_union_absorb_right
CARTESIAN_PRODUCT_CONST cartesian_product_const
COUNTABLE_ALT countable_alt
COUNTABLE_ASCENDING_CHAIN countable_ascending_chain
COUNTABLE_AS_IMAGE countable_as_image
COUNTABLE_AS_IMAGE_NUM_SUBSET countable_as_image_num_subset
COUNTABLE_AS_IMAGE_SUBSET countable_as_image_subset
COUNTABLE_AS_IMAGE_SUBSET_EQ countable_as_image_subset_eq
COUNTABLE_AS_INJECTIVE_IMAGE countable_as_injective_image
COUNTABLE_AS_INJECTIVE_IMAGE_SUBSET countable_as_injective_image_subset
COUNTABLE_CARD_ADD countable_card_add
COUNTABLE_CARD_ADD_EQ countable_card_add_eq
COUNTABLE_CARD_MUL countable_card_mul
COUNTABLE_CARD_MUL_EQ countable_card_mul_eq
COUNTABLE_CART countable_cart
COUNTABLE_CARTESIAN_PRODUCT countable_cartesian_product
COUNTABLE_CASES countable_cases
COUNTABLE_CROSS countable_cross
COUNTABLE_DELETE countable_delete
COUNTABLE_DESCENDING_CHAIN countable_descending_chain
COUNTABLE_DIFF countable_diff
COUNTABLE_DIFF_FINITE countable_diff_finite
COUNTABLE_DISJOINT_UNION_OF_IDEMPOT countable_disjoint_union_of_idempot
COUNTABLE_EMPTY countable_empty
COUNTABLE_FINITE_SUBSETS countable_finite_subsets
COUNTABLE_FLD countable_fld
COUNTABLE_IMAGE countable_image
COUNTABLE_IMAGE_EQ countable_image_eq
COUNTABLE_IMAGE_EQ_INJ countable_image_eq_inj
COUNTABLE_IMAGE_INJ countable_image_inj
COUNTABLE_IMAGE_INJ_EQ countable_image_inj_eq
COUNTABLE_IMAGE_INJ_GENERAL countable_image_inj_general
COUNTABLE_IMP_CARD_LT_REAL countable_imp_card_lt_real
COUNTABLE_INSERT countable_insert
COUNTABLE_INTER countable_inter
COUNTABLE_INTERSECTION_OF_COMPLEMENT countable_intersection_of_complement
COUNTABLE_INTERSECTION_OF_EMPTY countable_intersection_of_empty
COUNTABLE_INTERSECTION_OF_IDEMPOT countable_intersection_of_idempot
COUNTABLE_INTERSECTION_OF_INC countable_intersection_of_inc
COUNTABLE_INTERSECTION_OF_INTER countable_intersection_of_inter
COUNTABLE_INTERSECTION_OF_INTERS countable_intersection_of_inters
COUNTABLE_INTERSECTION_OF_UNION countable_intersection_of_union
COUNTABLE_INTERSECTION_OF_UNIONS countable_intersection_of_unions
COUNTABLE_INTERSECTION_OF_UNIONS_NONEMPTY countable_intersection_of_unions_nonempty
COUNTABLE_INTERSECTION_OF_UNION_EQ countable_intersection_of_union_eq
COUNTABLE_LIST countable_list
COUNTABLE_LIST_GEN countable_list_gen
COUNTABLE_PCROSS countable_pcross
COUNTABLE_PCROSS_EQ countable_pcross_eq
COUNTABLE_PRODUCT_DEPENDENT countable_product_dependent
COUNTABLE_RESTRICT countable_restrict
COUNTABLE_RESTRICTED_FUNSPACE countable_restricted_funspace
COUNTABLE_SING countable_sing
COUNTABLE_SUBSET countable_subset
COUNTABLE_SUBSET_IMAGE countable_subset_image
COUNTABLE_SUBSET_NUM countable_subset_num
COUNTABLE_UNION countable_union
COUNTABLE_UNIONS countable_unions
COUNTABLE_UNION_IMP countable_union_imp
COUNTABLE_UNION_OF_ASCENDING countable_union_of_ascending
COUNTABLE_UNION_OF_COMPLEMENT countable_union_of_complement
COUNTABLE_UNION_OF_EMPTY countable_union_of_empty
COUNTABLE_UNION_OF_EXPLICIT countable_union_of_explicit
COUNTABLE_UNION_OF_IDEMPOT countable_union_of_idempot
COUNTABLE_UNION_OF_INC countable_union_of_inc
COUNTABLE_UNION_OF_INTER countable_union_of_inter
COUNTABLE_UNION_OF_INTERS countable_union_of_inters
COUNTABLE_UNION_OF_INTERS_NONEMPTY countable_union_of_inters_nonempty
COUNTABLE_UNION_OF_INTER_EQ countable_union_of_inter_eq
COUNTABLE_UNION_OF_UNION countable_union_of_union
COUNTABLE_UNION_OF_UNIONS countable_union_of_unions
EQ_C eq_c
EQ_C_ALT eq_c_alt
EQ_C_BIJECTIONS eq_c_bijections
EQ_C_BIJECTIONS_DISJOINT eq_c_bijections_disjoint
EQ_C_BIJECTIONS_EXTEND eq_c_bijections_extend
EQ_C_BIJECTIONS_SUBSETS eq_c_bijections_subsets
EQ_C_BIJECTIONS_SUBSETS_LT eq_c_bijections_subsets_lt
EQ_C_INVOLUTION eq_c_involution
EXISTS_COUNTABLE_SUBSET_IMAGE exists_countable_subset_image
EXISTS_COUNTABLE_SUBSET_IMAGE_INJ exists_countable_subset_image_inj
EXISTS_SUM_THM exists_sum_thm
EXP_C exp_c_v1
FINITE_CARD_LT finite_card_lt
FINITE_CARTESIAN_PRODUCT finite_cartesian_product
FINITE_IMP_COUNTABLE finite_imp_countable
FLATTEN_LEMMA flatten_lemma
FORALL_COUNTABLE_AS_IMAGE forall_countable_as_image
FORALL_COUNTABLE_SUBSET_IMAGE forall_countable_subset_image
FORALL_COUNTABLE_SUBSET_IMAGE_INJ forall_countable_subset_image_inj
FORALL_SUM_THM forall_sum_thm
INFINITE_CARD_LE infinite_card_le
INJECTIVE_LEFT_INVERSE_NONEMPTY injective_left_inverse_nonempty
INT_COUNTABLE int_countable
IN_CARD_ADD in_card_add
IN_CARD_MUL in_card_mul
LE_C_IMAGE le_c_image
LE_C_IMAGE_SUBSET le_c_image_subset
MUL_C_UNIV mul_c_univ
NUMSEG_CARD_LE numseg_card_le
NUM_COUNTABLE num_countable
TARSKI_SET tarski_set
TRANS_CHAIN_TAC trans_chain_tac
UNCOUNTABLE_REAL uncountable_real
UNION_LE_ADD_C union_le_add_c
WF_CARD_LT wf_card_lt
add_c add_c
exp_c exp_c
int_INFINITE int_infinite
mul_c mul_c
sum_CASES sum_cases
sum_DISTINCT sum_distinct
sum_INJECTIVE sum_injective
