# Generated by tools/translator: qualified upstream name -> MoonBit name.
CARD_CART_UNIV card_cart_univ
CARD_FINITE_IMAGE card_finite_image
CART_EQ cart_eq
CART_EQ_FULL cart_eq_full
DIMINDEX_1 dimindex_1
DIMINDEX_2 dimindex_2
DIMINDEX_3 dimindex_3
DIMINDEX_4 dimindex_4
DIMINDEX_CLAUSES dimindex_clauses
DIMINDEX_CONV dimindex_conv
DIMINDEX_FINITE_DIFF dimindex_finite_diff
DIMINDEX_FINITE_IMAGE dimindex_finite_image
DIMINDEX_FINITE_PROD dimindex_finite_prod
DIMINDEX_FINITE_SUM dimindex_finite_sum
DIMINDEX_GE_1 dimindex_ge_1
DIMINDEX_HAS_SIZE_FINITE_DIFF dimindex_has_size_finite_diff
DIMINDEX_HAS_SIZE_FINITE_PROD dimindex_has_size_finite_prod
DIMINDEX_HAS_SIZE_FINITE_SUM dimindex_has_size_finite_sum
DIMINDEX_NONZERO dimindex_nonzero
DIMINDEX_TAC dimindex_tac
DIMINDEX_TYBIT0 dimindex_tybit0
DIMINDEX_TYBIT1 dimindex_tybit1
DIMINDEX_UNIQUE dimindex_unique
DIMINDEX_UNIV dimindex_univ
DISJOINT_PCROSS disjoint_pcross
EXISTS_IN_PCROSS exists_in_pcross
EXISTS_PASTECART exists_pastecart
FINITE_1 finite_1
FINITE_CART finite_cart
FINITE_CART_UNIV finite_cart_univ
FINITE_CLAUSES finite_clauses
FINITE_DIFF_IMAGE finite_diff_image
FINITE_FINITE_IMAGE finite_finite_image
FINITE_IMAGE_IMAGE finite_image_image
FINITE_INDEX_INJ finite_index_inj
FINITE_INDEX_INRANGE finite_index_inrange
FINITE_INDEX_INRANGE_2 finite_index_inrange_2
FINITE_INDEX_WORKS finite_index_works
FINITE_PCROSS finite_pcross
FINITE_PCROSS_EQ finite_pcross_eq
FINITE_PROD_IMAGE finite_prod_image
FINITE_SUM_IMAGE finite_sum_image
FINITE_TYBIT0 finite_tybit0
FINITE_TYBIT1 finite_tybit1
FORALL_FINITE_INDEX forall_finite_index
FORALL_IN_PCROSS forall_in_pcross
FORALL_PASTECART forall_pastecart
FSTCART_COMPONENT fstcart_component
FSTCART_PASTECART fstcart_pastecart
HAS_SIZE_1 has_size_1
HAS_SIZE_2 has_size_2
HAS_SIZE_3 has_size_3
HAS_SIZE_4 has_size_4
HAS_SIZE_CART_UNIV has_size_cart_univ
HAS_SIZE_DIMINDEX_RULE has_size_dimindex_rule
HAS_SIZE_FINITE_IMAGE has_size_finite_image
HAS_SIZE_PCROSS has_size_pcross
HAS_SIZE_TYBIT0 has_size_tybit0
HAS_SIZE_TYBIT1 has_size_tybit1
IMAGE_FSTCART_PCROSS image_fstcart_pcross
IMAGE_SNDCART_PCROSS image_sndcart_pcross
INTER_PCROSS inter_pcross
IN_ELIM_PASTECART_THM in_elim_pastecart_thm
LAMBDA_BETA lambda_beta
LAMBDA_ETA lambda_eta
LAMBDA_UNIQUE lambda_unique
NUMSEG_LT_DIMINDEX numseg_lt_dimindex
PASTECART_COMPONENT pastecart_component
PASTECART_EQ pastecart_eq
PASTECART_FST_SND pastecart_fst_snd
PASTECART_INJ pastecart_inj
PASTECART_IN_PCROSS pastecart_in_pcross
PCROSS pcross
PCROSS_DIFF pcross_diff
PCROSS_EMPTY pcross_empty
PCROSS_EQ pcross_eq
PCROSS_EQ_EMPTY pcross_eq_empty
PCROSS_INTER pcross_inter
PCROSS_INTERS pcross_inters
PCROSS_INTERS_INTERS pcross_inters_inters
PCROSS_MONO pcross_mono
PCROSS_SING pcross_sing
PCROSS_UNION pcross_union
PCROSS_UNIONS pcross_unions
PCROSS_UNIONS_UNIONS pcross_unions_unions
SNDCART_COMPONENT sndcart_component
SNDCART_PASTECART sndcart_pastecart
SUBSET_PCROSS subset_pcross
UNIV_HAS_SIZE_DIMINDEX univ_has_size_dimindex
UNIV_PCROSS_UNIV univ_pcross_univ
cart_tybij cart_tybij
dimindex dimindex
finite_diff_tybij finite_diff_tybij
finite_image_tybij finite_image_tybij
finite_index finite_index
finite_prod_tybij finite_prod_tybij
finite_sum_tybij finite_sum_tybij
fstcart fstcart
lambda lambda
pastecart pastecart
sndcart sndcart
tybit0_INDUCT tybit0_induct
tybit0_RECURSION tybit0_recursion
tybit1_INDUCT tybit1_induct
tybit1_RECURSION tybit1_recursion
vector vector
