# Generated by tools/translator: qualified upstream name -> MoonBit name.
CARD_EQ_NSUM card_eq_nsum
CARD_EQ_SUM card_eq_sum
CARD_NUMSEG card_numseg
CARD_NUMSEG_1 card_numseg_1
CARD_NUMSEG_LEMMA card_numseg_lemma
CARD_UNIONS card_unions
CARD_UNIONS_IMAGE card_unions_image
CONG_NSUM cong_nsum
DISJOINT_NUMSEG disjoint_numseg
EMPTY_NUMSEG empty_numseg
EXPAND_NSUM_CONV expand_nsum_conv
EXPAND_SUM_CONV expand_sum_conv
FINITE_INDEX_NUMBERS finite_index_numbers
FINITE_INDEX_NUMSEG finite_index_numseg
FINITE_INT_SEG finite_int_seg
FINITE_NUMSEG finite_numseg
FINITE_SUBSET_NUMSEG finite_subset_numseg
FINITE_SUPPORT finite_support
FINITE_SUPPORT_DELTA finite_support_delta
HAS_SIZE_NUMSEG has_size_numseg
HAS_SIZE_NUMSEG_1 has_size_numseg_1
INTER_NUMSEG inter_numseg
IN_NUMSEG in_numseg
IN_NUMSEG_0 in_numseg_0
IN_SUPPORT in_support
IPRODUCT_CLAUSES iproduct_clauses
ISUM_CLAUSES isum_clauses
ITERATE_BIJECTION iterate_bijection
ITERATE_CASES iterate_cases
ITERATE_CLAUSES iterate_clauses
ITERATE_CLAUSES_GEN iterate_clauses_gen
ITERATE_CLAUSES_NUMSEG iterate_clauses_numseg
ITERATE_CLAUSES_NUMSEG_LE iterate_clauses_numseg_le
ITERATE_CLAUSES_NUMSEG_LT iterate_clauses_numseg_lt
ITERATE_CLOSED iterate_closed
ITERATE_CLOSED_NONEMPTY iterate_closed_nonempty
ITERATE_DELETE iterate_delete
ITERATE_DELTA iterate_delta
ITERATE_DIFF iterate_diff
ITERATE_DIFF_GEN iterate_diff_gen
ITERATE_EQ iterate_eq
ITERATE_EQ_GENERAL iterate_eq_general
ITERATE_EQ_GENERAL_INVERSES iterate_eq_general_inverses
ITERATE_EQ_NEUTRAL iterate_eq_neutral
ITERATE_EXPAND_CASES iterate_expand_cases
ITERATE_IMAGE iterate_image
ITERATE_IMAGE_GEN iterate_image_gen
ITERATE_IMAGE_NONZERO iterate_image_nonzero
ITERATE_INCL_EXCL iterate_incl_excl
ITERATE_INJECTION iterate_injection
ITERATE_ITERATE_PRODUCT iterate_iterate_product
ITERATE_OP iterate_op
ITERATE_OP_GEN iterate_op_gen
ITERATE_PAIR iterate_pair
ITERATE_REFLECT iterate_reflect
ITERATE_RELATED iterate_related
ITERATE_RELATED_NONEMPTY iterate_related_nonempty
ITERATE_RESTRICT_SET iterate_restrict_set
ITERATE_SING iterate_sing
ITERATE_SUPERSET iterate_superset
ITERATE_SUPPORT iterate_support
ITERATE_SWAP iterate_swap
ITERATE_UNION iterate_union
ITERATE_UNION_GEN iterate_union_gen
ITERATE_UNION_NONZERO iterate_union_nonzero
ITERATE_UNIV iterate_univ
ITERATO_CLAUSES iterato_clauses
ITERATO_CLAUSES_EXISTS iterato_clauses_exists
ITERATO_CLAUSES_GEN iterato_clauses_gen
ITERATO_CLAUSES_NUMSEG_LEFT iterato_clauses_numseg_left
ITERATO_CLOSED iterato_closed
ITERATO_EQ iterato_eq
ITERATO_EXPAND_CASES iterato_expand_cases
ITERATO_INDUCT iterato_induct
ITERATO_ITERATE iterato_iterate
ITERATO_SUPPORT iterato_support
MOD_NSUM_MOD mod_nsum_mod
MOD_NSUM_MOD_NUMSEG mod_nsum_mod_numseg
MONOIDAL_AC monoidal_ac
MONOIDAL_ADD monoidal_add
MONOIDAL_INT_ADD monoidal_int_add
MONOIDAL_INT_MUL monoidal_int_mul
MONOIDAL_MUL monoidal_mul
MONOIDAL_REAL_ADD monoidal_real_add
MONOIDAL_REAL_MUL monoidal_real_mul
NEUTRAL_ADD neutral_add
NEUTRAL_INT_ADD neutral_int_add
NEUTRAL_INT_MUL neutral_int_mul
NEUTRAL_MUL neutral_mul
NEUTRAL_REAL_ADD neutral_real_add
NEUTRAL_REAL_MUL neutral_real_mul
NPRODUCT_CLAUSES nproduct_clauses
NSUM_0 nsum_0
NSUM_ADD nsum_add
NSUM_ADD_GEN nsum_add_gen
NSUM_ADD_NUMSEG nsum_add_numseg
NSUM_ADD_SPLIT nsum_add_split
NSUM_BIJECTION nsum_bijection
NSUM_BOUND nsum_bound
NSUM_BOUND_GEN nsum_bound_gen
NSUM_BOUND_LT nsum_bound_lt
NSUM_BOUND_LT_ALL nsum_bound_lt_all
NSUM_BOUND_LT_GEN nsum_bound_lt_gen
NSUM_CASES nsum_cases
NSUM_CLAUSES nsum_clauses
NSUM_CLAUSES_LEFT nsum_clauses_left
NSUM_CLAUSES_NUMSEG nsum_clauses_numseg
NSUM_CLAUSES_NUMSEG_LE nsum_clauses_numseg_le
NSUM_CLAUSES_NUMSEG_LT nsum_clauses_numseg_lt
NSUM_CLAUSES_RIGHT nsum_clauses_right
NSUM_CLOSED nsum_closed
NSUM_CLOSED_NONEMPTY nsum_closed_nonempty
NSUM_CONST nsum_const
NSUM_CONST_NUMSEG nsum_const_numseg
NSUM_DEGENERATE nsum_degenerate
NSUM_DELETE nsum_delete
NSUM_DELTA nsum_delta
NSUM_DIFF nsum_diff
NSUM_EQ nsum_eq
NSUM_EQ_0 nsum_eq_0
NSUM_EQ_0_IFF nsum_eq_0_iff
NSUM_EQ_0_IFF_NUMSEG nsum_eq_0_iff_numseg
NSUM_EQ_0_NUMSEG nsum_eq_0_numseg
NSUM_EQ_GENERAL nsum_eq_general
NSUM_EQ_GENERAL_INVERSES nsum_eq_general_inverses
NSUM_EQ_NUMSEG nsum_eq_numseg
NSUM_EQ_SUPERSET nsum_eq_superset
NSUM_GROUP nsum_group
NSUM_GROUP_RELATION nsum_group_relation
NSUM_IMAGE nsum_image
NSUM_IMAGE_GEN nsum_image_gen
NSUM_IMAGE_NONZERO nsum_image_nonzero
NSUM_INCL_EXCL nsum_incl_excl
NSUM_INJECTION nsum_injection
NSUM_LE nsum_le
NSUM_LE_GEN nsum_le_gen
NSUM_LE_NUMSEG nsum_le_numseg
NSUM_LMUL nsum_lmul
NSUM_LT nsum_lt
NSUM_LT_ALL nsum_lt_all
NSUM_MULTICOUNT nsum_multicount
NSUM_MULTICOUNT_GEN nsum_multicount_gen
NSUM_MUL_BOUND nsum_mul_bound
NSUM_NSUM_PRODUCT nsum_nsum_product
NSUM_NSUM_RESTRICT nsum_nsum_restrict
NSUM_OFFSET nsum_offset
NSUM_OFFSET_0 nsum_offset_0
NSUM_PAIR nsum_pair
NSUM_POS_BOUND nsum_pos_bound
NSUM_POS_LT nsum_pos_lt
NSUM_POS_LT_ALL nsum_pos_lt_all
NSUM_REFLECT nsum_reflect
NSUM_RELATED nsum_related
NSUM_RELATED_NONEMPTY nsum_related_nonempty
NSUM_RESTRICT nsum_restrict
NSUM_RESTRICT_SET nsum_restrict_set
NSUM_RMUL nsum_rmul
NSUM_SING nsum_sing
NSUM_SING_NUMSEG nsum_sing_numseg
NSUM_SUBSET nsum_subset
NSUM_SUBSET_SIMPLE nsum_subset_simple
NSUM_SUPERSET nsum_superset
NSUM_SUPPORT nsum_support
NSUM_SWAP nsum_swap
NSUM_SWAP_NUMSEG nsum_swap_numseg
NSUM_TRIV_NUMSEG nsum_triv_numseg
NSUM_UNION nsum_union
NSUM_UNIONS_NONZERO nsum_unions_nonzero
NSUM_UNION_EQ nsum_union_eq
NSUM_UNION_LZERO nsum_union_lzero
NSUM_UNION_NONZERO nsum_union_nonzero
NSUM_UNION_RZERO nsum_union_rzero
NSUM_UNIV nsum_univ
NUMSEG_ADD_SPLIT numseg_add_split
NUMSEG_CLAUSES numseg_clauses
NUMSEG_COMBINE_L numseg_combine_l
NUMSEG_COMBINE_R numseg_combine_r
NUMSEG_CONV numseg_conv
NUMSEG_EMPTY numseg_empty
NUMSEG_LE numseg_le
NUMSEG_LREC numseg_lrec
NUMSEG_LT numseg_lt
NUMSEG_OFFSET_IMAGE numseg_offset_image
NUMSEG_REC numseg_rec
NUMSEG_RREC numseg_rrec
NUMSEG_SING numseg_sing
POLYNOMIAL_FUNCTION_ADD polynomial_function_add
POLYNOMIAL_FUNCTION_CONST polynomial_function_const
POLYNOMIAL_FUNCTION_FINITE_ROOTS polynomial_function_finite_roots
POLYNOMIAL_FUNCTION_I polynomial_function_i
POLYNOMIAL_FUNCTION_ID polynomial_function_id
POLYNOMIAL_FUNCTION_INDUCT polynomial_function_induct
POLYNOMIAL_FUNCTION_LMUL polynomial_function_lmul
POLYNOMIAL_FUNCTION_MUL polynomial_function_mul
POLYNOMIAL_FUNCTION_NEG polynomial_function_neg
POLYNOMIAL_FUNCTION_POW polynomial_function_pow
POLYNOMIAL_FUNCTION_RMUL polynomial_function_rmul
POLYNOMIAL_FUNCTION_SUB polynomial_function_sub
POLYNOMIAL_FUNCTION_SUM polynomial_function_sum
POLYNOMIAL_FUNCTION_o polynomial_function_o
PRODUCT_CLAUSES product_clauses
REAL_OF_NUM_SUM real_of_num_sum
REAL_OF_NUM_SUM_GEN real_of_num_sum_gen
REAL_OF_NUM_SUM_NUMSEG real_of_num_sum_numseg
REAL_POLYFUN_EQ_0 real_polyfun_eq_0
REAL_POLYFUN_EQ_CONST real_polyfun_eq_const
REAL_POLYFUN_FINITE_ROOTS real_polyfun_finite_roots
REAL_POLYFUN_ROOTBOUND real_polyfun_rootbound
REAL_SUB_POLYFUN real_sub_polyfun
REAL_SUB_POLYFUN_ALT real_sub_polyfun_alt
REAL_SUB_POW real_sub_pow
REAL_SUB_POW_L1 real_sub_pow_l1
REAL_SUB_POW_R1 real_sub_pow_r1
SUBSET_NUMSEG subset_numseg
SUM_0 sum_0
SUM_ABS sum_abs
SUM_ABS_BOUND sum_abs_bound
SUM_ABS_LE sum_abs_le
SUM_ABS_NUMSEG sum_abs_numseg
SUM_ADD sum_add
SUM_ADD_GEN sum_add_gen
SUM_ADD_NUMSEG sum_add_numseg
SUM_ADD_SPLIT sum_add_split
SUM_BIJECTION sum_bijection
SUM_BOUND sum_bound
SUM_BOUND_GEN sum_bound_gen
SUM_BOUND_LT sum_bound_lt
SUM_BOUND_LT_ALL sum_bound_lt_all
SUM_BOUND_LT_GEN sum_bound_lt_gen
SUM_CASES sum_cases
SUM_CASES_1 sum_cases_1
SUM_CLAUSES sum_clauses
SUM_CLAUSES_LEFT sum_clauses_left
SUM_CLAUSES_NUMSEG sum_clauses_numseg
SUM_CLAUSES_NUMSEG_LE sum_clauses_numseg_le
SUM_CLAUSES_NUMSEG_LT sum_clauses_numseg_lt
SUM_CLAUSES_RIGHT sum_clauses_right
SUM_CLOSED sum_closed
SUM_CLOSED_NONEMPTY sum_closed_nonempty
SUM_COMBINE_L sum_combine_l
SUM_COMBINE_R sum_combine_r
SUM_CONST sum_const
SUM_CONST_NUMSEG sum_const_numseg
SUM_DEGENERATE sum_degenerate
SUM_DELETE sum_delete
SUM_DELETE_CASES sum_delete_cases
SUM_DELTA sum_delta
SUM_DIFF sum_diff
SUM_DIFFS sum_diffs
SUM_DIFFS_ALT sum_diffs_alt
SUM_EQ sum_eq
SUM_EQ_0 sum_eq_0
SUM_EQ_0_NUMSEG sum_eq_0_numseg
SUM_EQ_GENERAL sum_eq_general
SUM_EQ_GENERAL_INVERSES sum_eq_general_inverses
SUM_EQ_NUMSEG sum_eq_numseg
SUM_EQ_SUPERSET sum_eq_superset
SUM_GROUP sum_group
SUM_GROUP_RELATION sum_group_relation
SUM_IMAGE sum_image
SUM_IMAGE_GEN sum_image_gen
SUM_IMAGE_LE sum_image_le
SUM_IMAGE_NONZERO sum_image_nonzero
SUM_INCL_EXCL sum_incl_excl
SUM_INJECTION sum_injection
SUM_LE sum_le
SUM_LE_INCLUDED sum_le_included
SUM_LE_NUMSEG sum_le_numseg
SUM_LMUL sum_lmul
SUM_LT sum_lt
SUM_LT_ALL sum_lt_all
SUM_MULTICOUNT sum_multicount
SUM_MULTICOUNT_GEN sum_multicount_gen
SUM_MUL_BOUND sum_mul_bound
SUM_NEG sum_neg
SUM_OFFSET sum_offset
SUM_OFFSET_0 sum_offset_0
SUM_PAIR sum_pair
SUM_PARTIAL_PRE sum_partial_pre
SUM_PARTIAL_SUC sum_partial_suc
SUM_POS_BOUND sum_pos_bound
SUM_POS_EQ_0 sum_pos_eq_0
SUM_POS_EQ_0_NUMSEG sum_pos_eq_0_numseg
SUM_POS_LE sum_pos_le
SUM_POS_LE_NUMSEG sum_pos_le_numseg
SUM_POS_LT sum_pos_lt
SUM_POS_LT_ALL sum_pos_lt_all
SUM_REFLECT sum_reflect
SUM_RELATED sum_related
SUM_RELATED_NONEMPTY sum_related_nonempty
SUM_RESTRICT sum_restrict
SUM_RESTRICT_SET sum_restrict_set
SUM_RMUL sum_rmul
SUM_SING sum_sing
SUM_SING_NUMSEG sum_sing_numseg
SUM_SUB sum_sub
SUM_SUBSET sum_subset
SUM_SUBSET_SIMPLE sum_subset_simple
SUM_SUB_NUMSEG sum_sub_numseg
SUM_SUM_PRODUCT sum_sum_product
SUM_SUM_RESTRICT sum_sum_restrict
SUM_SUPERSET sum_superset
SUM_SUPPORT sum_support
SUM_SWAP sum_swap
SUM_SWAP_NUMSEG sum_swap_numseg
SUM_TRIV_NUMSEG sum_triv_numseg
SUM_UNION sum_union
SUM_UNIONS_NONZERO sum_unions_nonzero
SUM_UNION_EQ sum_union_eq
SUM_UNION_LZERO sum_union_lzero
SUM_UNION_NONZERO sum_union_nonzero
SUM_UNION_RZERO sum_union_rzero
SUM_UNIV sum_univ
SUM_ZERO_EXISTS sum_zero_exists
SUPPORT_CLAUSES support_clauses
SUPPORT_DELTA support_delta
SUPPORT_EMPTY support_empty
SUPPORT_SUBSET support_subset
SUPPORT_SUPPORT support_support
TOPOLOGICAL_SORT topological_sort
iproduct iproduct
isum isum
iterate iterate
iterato iterato
monoidal monoidal
neutral neutral
nproduct nproduct
nsum nsum
numseg numseg
polynomial_function polynomial_function
product product
sum sum
support support
