# Generated by tools/translator: qualified upstream name -> MoonBit name.
ABSORPTION absorption
ARB arb
ARBITRARY arbitrary
ARBITRARY_INTERSECTION_OF_COMPLEMENT arbitrary_intersection_of_complement
ARBITRARY_INTERSECTION_OF_EMPTY arbitrary_intersection_of_empty
ARBITRARY_INTERSECTION_OF_IDEMPOT arbitrary_intersection_of_idempot
ARBITRARY_INTERSECTION_OF_INC arbitrary_intersection_of_inc
ARBITRARY_INTERSECTION_OF_INTER arbitrary_intersection_of_inter
ARBITRARY_INTERSECTION_OF_INTERS arbitrary_intersection_of_inters
ARBITRARY_INTERSECTION_OF_UNION arbitrary_intersection_of_union
ARBITRARY_INTERSECTION_OF_UNION_EQ arbitrary_intersection_of_union_eq
ARBITRARY_UNION_OF_ALT arbitrary_union_of_alt
ARBITRARY_UNION_OF_COMPLEMENT arbitrary_union_of_complement
ARBITRARY_UNION_OF_EMPTY arbitrary_union_of_empty
ARBITRARY_UNION_OF_IDEMPOT arbitrary_union_of_idempot
ARBITRARY_UNION_OF_INC arbitrary_union_of_inc
ARBITRARY_UNION_OF_INTER arbitrary_union_of_inter
ARBITRARY_UNION_OF_INTER_EQ arbitrary_union_of_inter_eq
ARBITRARY_UNION_OF_UNION arbitrary_union_of_union
ARBITRARY_UNION_OF_UNIONS arbitrary_union_of_unions
BIJ bij
BIJECTIONS_CARD_EQ bijections_card_eq
BIJECTIONS_HAS_SIZE bijections_has_size
BIJECTIONS_HAS_SIZE_EQ bijections_has_size_eq
BIJECTIVE_LEFT_RIGHT_INVERSE bijective_left_right_inverse
BIJECTIVE_ON_LEFT_RIGHT_INVERSE bijective_on_left_right_inverse
CARD card
CARD_BOOL card_bool
CARD_CLAUSES card_clauses
CARD_CROSS card_cross
CARD_DELETE card_delete
CARD_DIFF card_diff
CARD_EQ_0 card_eq_0
CARD_EQ_BIJECTION card_eq_bijection
CARD_EQ_BIJECTIONS card_eq_bijections
CARD_EQ_BIJECTIONS_SPECIAL card_eq_bijections_special
CARD_FUNSPACE card_funspace
CARD_FUNSPACE_UNIV card_funspace_univ
CARD_IMAGE_EQ_INJ card_image_eq_inj
CARD_IMAGE_INJ card_image_inj
CARD_IMAGE_INJ_EQ card_image_inj_eq
CARD_IMAGE_LE card_image_le
CARD_IMAGE_LE2 card_image_le2
CARD_IMAGE_LT2 card_image_lt2
CARD_LE_1 card_le_1
CARD_LE_2 card_le_2
CARD_LE_3 card_le_3
CARD_LE_4 card_le_4
CARD_LE_INJ card_le_inj
CARD_LE_UNIONS_CHAIN card_le_unions_chain
CARD_NUMSEG_LE card_numseg_le
CARD_NUMSEG_LT card_numseg_lt
CARD_POWERSET card_powerset
CARD_PRODUCT card_product
CARD_PSUBSET card_psubset
CARD_PSUBSET_EQ card_psubset_eq
CARD_PSUBSET_IMP card_psubset_imp
CARD_SET_OF_LIST_LE card_set_of_list_le
CARD_SING card_sing
CARD_SUBSET card_subset
CARD_SUBSET_EQ card_subset_eq
CARD_SUBSET_IMAGE card_subset_image
CARD_SUBSET_LE card_subset_le
CARD_UNION card_union
CARD_UNIONS_LE card_unions_le
CARD_UNION_EQ card_union_eq
CARD_UNION_GEN card_union_gen
CARD_UNION_LE card_union_le
CARD_UNION_OVERLAP card_union_overlap
CARD_UNION_OVERLAP_EQ card_union_overlap_eq
CARTESIAN_PRODUCT cartesian_product_v1
CARTESIAN_PRODUCT_AS_RESTRICTIONS cartesian_product_as_restrictions
CARTESIAN_PRODUCT_EMPTY cartesian_product_empty
CARTESIAN_PRODUCT_EQ cartesian_product_eq
CARTESIAN_PRODUCT_EQ_EMPTY cartesian_product_eq_empty
CARTESIAN_PRODUCT_EQ_MEMBERS cartesian_product_eq_members
CARTESIAN_PRODUCT_EQ_MEMBERS_EQ cartesian_product_eq_members_eq
CARTESIAN_PRODUCT_SINGS cartesian_product_sings
CARTESIAN_PRODUCT_SINGS_GEN cartesian_product_sings_gen
CARTESIAN_PRODUCT_UNIV cartesian_product_univ
CHOICE choice
CHOICE_DEF choice_def
CHOOSE_SUBSET choose_subset
CHOOSE_SUBSET_BETWEEN choose_subset_between
CHOOSE_SUBSET_EQ choose_subset_eq
CHOOSE_SUBSET_STRONG choose_subset_strong
COMPL_COMPL compl_compl
COMPONENT component
COUNTABLE countable
CROSS cross
CROSS_DIFF cross_diff
CROSS_EMPTY cross_empty
CROSS_EQ cross_eq
CROSS_EQ_EMPTY cross_eq_empty
CROSS_INTER cross_inter
CROSS_INTERS cross_inters
CROSS_INTERS_INTERS cross_inters_inters
CROSS_MONO cross_mono
CROSS_SING cross_sing
CROSS_UNION cross_union
CROSS_UNIONS cross_unions
CROSS_UNIONS_UNIONS cross_unions_unions
CROSS_UNIV cross_univ
DECOMPOSITION decomposition
DELETE delete
DELETE_COMM delete_comm
DELETE_DELETE delete_delete
DELETE_INSERT delete_insert
DELETE_INTER delete_inter
DELETE_NON_ELEMENT delete_non_element
DELETE_SUBSET delete_subset
DIFF diff
DIFF_DIFF diff_diff
DIFF_EMPTY diff_empty
DIFF_EQ_EMPTY diff_eq_empty
DIFF_INSERT diff_insert
DIFF_INTERS diff_inters
DIFF_RESTRICT diff_restrict
DIFF_UNIONS diff_unions
DIFF_UNIONS_NONEMPTY diff_unions_nonempty
DIFF_UNIONS_PAIRWISE_DISJOINT diff_unions_pairwise_disjoint
DIFF_UNIV diff_univ
DISJOINT disjoint
DISJOINT_CROSS disjoint_cross
DISJOINT_DELETE_SYM disjoint_delete_sym
DISJOINT_DISJOINT_UNION disjoint_disjoint_union
DISJOINT_EMPTY disjoint_empty
DISJOINT_EMPTY_REFL disjoint_empty_refl
DISJOINT_INSERT disjoint_insert
DISJOINT_SING disjoint_sing
DISJOINT_SYM disjoint_sym
DISJOINT_UNION disjoint_union
DISJOINT_UNION_EQ disjoint_union_eq
DISJOINT_UNION_EQ_EMPTY disjoint_union_eq_empty
ELEMENT_LE_SUP element_le_sup
EMPTY empty
EMPTY_DELETE empty_delete
EMPTY_DIFF empty_diff
EMPTY_GSPEC empty_gspec
EMPTY_NOT_UNIV empty_not_univ
EMPTY_SUBSET empty_subset
EMPTY_UNION empty_union
EMPTY_UNIONS empty_unions
EQ_UNIV eq_univ
EXISTS_CARTESIAN_PRODUCT_ELEMENT exists_cartesian_product_element
EXISTS_FINITE_SUBSET_IMAGE exists_finite_subset_image
EXISTS_FINITE_SUBSET_IMAGE_INJ exists_finite_subset_image_inj
EXISTS_IN_CLAUSES exists_in_clauses
EXISTS_IN_CROSS exists_in_cross
EXISTS_IN_GSPEC exists_in_gspec
EXISTS_IN_IMAGE exists_in_image
EXISTS_IN_INSERT exists_in_insert
EXISTS_IN_UNION exists_in_union
EXISTS_IN_UNIONS exists_in_unions
EXISTS_SMALL_SUBSET_IMAGE exists_small_subset_image
EXISTS_SMALL_SUBSET_IMAGE_INJ exists_small_subset_image_inj
EXISTS_SUBSET_IMAGE exists_subset_image
EXISTS_SUBSET_IMAGE_INJ exists_subset_image_inj
EXISTS_SUBSET_INSERT exists_subset_insert
EXISTS_SUBSET_UNION exists_subset_union
EXISTS_UNIQUE_UNIONS_INTERS exists_unique_unions_inters
EXTENSION extension
EXTENSIONAL extensional
EXTENSIONAL_EMPTY extensional_empty
EXTENSIONAL_EQ extensional_eq
EXTENSIONAL_UNIV extensional_univ
FINITE_BOOL finite_bool
FINITE_CARD_LE_IMAGE finite_card_le_image
FINITE_CARD_LE_SUBSET finite_card_le_subset
FINITE_CARD_LE_UNION finite_card_le_union
FINITE_CARD_LE_UNIONS finite_card_le_unions
FINITE_CASES finite_cases
FINITE_CROSS finite_cross
FINITE_CROSS_EQ finite_cross_eq
FINITE_CROSS_UNIV finite_cross_univ
FINITE_DELETE finite_delete
FINITE_DELETE_IMP finite_delete_imp
FINITE_DIFF finite_diff
FINITE_EMPTY finite_empty
FINITE_FINITE_PREIMAGE finite_finite_preimage
FINITE_FINITE_PREIMAGE_GENERAL finite_finite_preimage_general
FINITE_FINITE_UNIONS finite_finite_unions
FINITE_FUNSPACE finite_funspace
FINITE_FUNSPACE_UNIV finite_funspace_univ
FINITE_HAS_SIZE finite_has_size
FINITE_IMAGE finite_image
FINITE_IMAGE_EQ finite_image_eq
FINITE_IMAGE_EQ_INJ finite_image_eq_inj
FINITE_IMAGE_EXPAND finite_image_expand
FINITE_IMAGE_GEN finite_image_gen
FINITE_IMAGE_INFINITE finite_image_infinite
FINITE_IMAGE_INJ finite_image_inj
FINITE_IMAGE_INJ_EQ finite_image_inj_eq
FINITE_IMAGE_INJ_GENERAL finite_image_inj_general
FINITE_INDUCT finite_induct
FINITE_INDUCT_DELETE finite_induct_delete
FINITE_INDUCT_STRONG finite_induct_strong
FINITE_INSERT finite_insert
FINITE_INTER finite_inter
FINITE_INTERSECTION_OF_COMPLEMENT finite_intersection_of_complement
FINITE_INTERSECTION_OF_EMPTY finite_intersection_of_empty
FINITE_INTERSECTION_OF_IDEMPOT finite_intersection_of_idempot
FINITE_INTERSECTION_OF_INC finite_intersection_of_inc
FINITE_INTERSECTION_OF_INTER finite_intersection_of_inter
FINITE_INTERSECTION_OF_INTERS finite_intersection_of_inters
FINITE_INTERSECTION_OF_UNION finite_intersection_of_union
FINITE_INTERSECTION_OF_UNION_EQ finite_intersection_of_union_eq
FINITE_NUMSEG_LE finite_numseg_le
FINITE_NUMSEG_LT finite_numseg_lt
FINITE_POWERSET finite_powerset
FINITE_POWERSET_EQ finite_powerset_eq
FINITE_PRODUCT finite_product
FINITE_PRODUCT_DEPENDENT finite_product_dependent
FINITE_REAL_INTERVAL finite_real_interval
FINITE_RECURSION finite_recursion
FINITE_RECURSION_DELETE finite_recursion_delete
FINITE_RESTRICT finite_restrict
FINITE_RESTRICTED_FUNSPACE finite_restricted_funspace
FINITE_RESTRICTED_POWERSET finite_restricted_powerset
FINITE_RESTRICTED_SUBSETS finite_restricted_subsets
FINITE_RULES finite_rules
FINITE_SET_OF_LIST finite_set_of_list
FINITE_SING finite_sing
FINITE_SUBSET finite_subset
FINITE_SUBSET_IMAGE finite_subset_image
FINITE_SUBSET_IMAGE_IMP finite_subset_image_imp
FINITE_SUBSET_UNIONS finite_subset_unions
FINITE_SUBSET_UNIONS_CHAIN finite_subset_unions_chain
FINITE_SUBSET_UNIONS_CHAIN_EQ finite_subset_unions_chain_eq
FINITE_SUBSET_UNIONS_DIRECTED_EQ finite_subset_unions_directed_eq
FINITE_TRANSITIVITY_CHAIN finite_transitivity_chain
FINITE_UNION finite_union
FINITE_UNIONS finite_unions
FINITE_UNION_IMP finite_union_imp
FINITE_UNION_OF_COMPLEMENT finite_union_of_complement
FINITE_UNION_OF_EMPTY finite_union_of_empty
FINITE_UNION_OF_IDEMPOT finite_union_of_idempot
FINITE_UNION_OF_INC finite_union_of_inc
FINITE_UNION_OF_INTER finite_union_of_inter
FINITE_UNION_OF_INTER_EQ finite_union_of_inter_eq
FINITE_UNION_OF_UNION finite_union_of_union
FINITE_UNION_OF_UNIONS finite_union_of_unions
FINITE_UNIV_PAIR finite_univ_pair
FINREC finrec
FINREC_1_LEMMA finrec_1_lemma
FINREC_EXISTS_LEMMA finrec_exists_lemma
FINREC_FUN finrec_fun
FINREC_FUN_LEMMA finrec_fun_lemma
FINREC_SUC_LEMMA finrec_suc_lemma
FINREC_UNIQUE_LEMMA finrec_unique_lemma
FORALL_CARTESIAN_PRODUCT_ELEMENTS forall_cartesian_product_elements
FORALL_CARTESIAN_PRODUCT_ELEMENTS_EQ forall_cartesian_product_elements_eq
FORALL_FINITE_SUBSET_IMAGE forall_finite_subset_image
FORALL_FINITE_SUBSET_IMAGE_INJ forall_finite_subset_image_inj
FORALL_INTERSECTION_OF forall_intersection_of
FORALL_IN_CLAUSES forall_in_clauses
FORALL_IN_CROSS forall_in_cross
FORALL_IN_GSPEC forall_in_gspec
FORALL_IN_IMAGE forall_in_image
FORALL_IN_IMAGE_2 forall_in_image_2
FORALL_IN_INSERT forall_in_insert
FORALL_IN_UNION forall_in_union
FORALL_IN_UNIONS forall_in_unions
FORALL_SMALL_SUBSET_IMAGE forall_small_subset_image
FORALL_SMALL_SUBSET_IMAGE_INJ forall_small_subset_image_inj
FORALL_SUBSET_IMAGE forall_subset_image
FORALL_SUBSET_IMAGE_INJ forall_subset_image_inj
FORALL_SUBSET_INSERT forall_subset_insert
FORALL_SUBSET_UNION forall_subset_union
FORALL_UNION_OF forall_union_of
FUNCTION_FACTORS_LEFT function_factors_left
FUNCTION_FACTORS_LEFT_GEN function_factors_left_gen
FUNCTION_FACTORS_RIGHT function_factors_right
FUNCTION_FACTORS_RIGHT_GEN function_factors_right_gen
FUN_IN_IMAGE fun_in_image
GE_C ge_c_v1
GSPEC gspec
HAS_INF has_inf_v1
HAS_INF_APPROACH has_inf_approach
HAS_INF_INF has_inf_inf
HAS_INF_LBOUND has_inf_lbound
HAS_INF_LE has_inf_le
HAS_SIZE has_size
HAS_SIZE_0 has_size_0
HAS_SIZE_BOOL has_size_bool
HAS_SIZE_CARD has_size_card
HAS_SIZE_CLAUSES has_size_clauses
HAS_SIZE_CONV has_size_conv
HAS_SIZE_CROSS has_size_cross
HAS_SIZE_DIFF has_size_diff
HAS_SIZE_FUNSPACE has_size_funspace
HAS_SIZE_FUNSPACE_UNIV has_size_funspace_univ
HAS_SIZE_IMAGE_INJ has_size_image_inj
HAS_SIZE_IMAGE_INJ_EQ has_size_image_inj_eq
HAS_SIZE_IMAGE_INJ_RESTRICT has_size_image_inj_restrict
HAS_SIZE_INDEX has_size_index
HAS_SIZE_NUMSEG_LE has_size_numseg_le
HAS_SIZE_NUMSEG_LT has_size_numseg_lt
HAS_SIZE_POWERSET has_size_powerset
HAS_SIZE_PRODUCT has_size_product
HAS_SIZE_PRODUCT_DEPENDENT has_size_product_dependent
HAS_SIZE_SET_OF_LIST has_size_set_of_list
HAS_SIZE_SUC has_size_suc
HAS_SIZE_UNION has_size_union
HAS_SIZE_UNIONS has_size_unions
HAS_SUP has_sup_v1
HAS_SUP_APPROACH has_sup_approach
HAS_SUP_LE has_sup_le
HAS_SUP_SUP has_sup_sup
HAS_SUP_UBOUND has_sup_ubound
IMAGE image
IMAGE_CLAUSES image_clauses
IMAGE_CONST image_const
IMAGE_DELETE_INJ image_delete_inj
IMAGE_DELETE_INJ_ALT image_delete_inj_alt
IMAGE_DIFF_INJ image_diff_inj
IMAGE_DIFF_INJ_ALT image_diff_inj_alt
IMAGE_EQ image_eq
IMAGE_EQ_EMPTY image_eq_empty
IMAGE_FST_CROSS image_fst_cross
IMAGE_I image_i
IMAGE_ID image_id
IMAGE_IMP_INJECTIVE image_imp_injective
IMAGE_IMP_INJECTIVE_GEN image_imp_injective_gen
IMAGE_INJECTIVE_IMAGE_OF_SUBSET image_injective_image_of_subset
IMAGE_INTERS image_inters
IMAGE_INTERS_SATURATED image_inters_saturated
IMAGE_INTERS_SATURATED_GEN image_inters_saturated_gen
IMAGE_INTERS_SUBSET image_inters_subset
IMAGE_INTER_INJ image_inter_inj
IMAGE_INTER_SATURATED image_inter_saturated
IMAGE_INTER_SATURATED_GEN image_inter_saturated_gen
IMAGE_INTER_SUBSET image_inter_subset
IMAGE_PAIRED_CROSS image_paired_cross
IMAGE_PRODUCT_MAP image_product_map
IMAGE_PROJECTION_CARTESIAN_PRODUCT image_projection_cartesian_product
IMAGE_RESTRICTION image_restriction
IMAGE_SND_CROSS image_snd_cross
IMAGE_SUBSET image_subset
IMAGE_UNION image_union
IMAGE_UNIONS image_unions
IMAGE_o image_o
IN in_
INF inf_v1
INFINITE infinite
INFINITE_CROSS_EQ infinite_cross_eq
INFINITE_CROSS_UNIV infinite_cross_univ
INFINITE_DIFF_FINITE infinite_diff_finite
INFINITE_ENUMERATE infinite_enumerate
INFINITE_ENUMERATE_EQ infinite_enumerate_eq
INFINITE_ENUMERATE_SUBSET infinite_enumerate_subset
INFINITE_IMAGE infinite_image
INFINITE_IMAGE_INJ infinite_image_inj
INFINITE_NONEMPTY infinite_nonempty
INFINITE_SUPERSET infinite_superset
INFINITE_UNIV_PAIR infinite_univ_pair
INF_APPROACH inf_approach
INF_EQ inf_eq
INF_EXISTS inf_exists
INF_FINITE inf_finite
INF_FINITE_LEMMA inf_finite_lemma
INF_INSERT_FINITE inf_insert_finite
INF_INSERT_INSERT inf_insert_insert
INF_LE_ELEMENT inf_le_element
INF_SING inf_sing
INF_UNION inf_union
INF_UNIQUE inf_unique
INF_UNIQUE_FINITE inf_unique_finite
INJ inj
INJECTIVE_ALT injective_alt
INJECTIVE_IMAGE injective_image
INJECTIVE_LEFT_INVERSE injective_left_inverse
INJECTIVE_ON_ALT injective_on_alt
INJECTIVE_ON_IMAGE injective_on_image
INJECTIVE_ON_LEFT_INVERSE injective_on_left_inverse
INJECTIVE_ON_PREIMAGE injective_on_preimage
INJECTIVE_PREIMAGE injective_preimage
INSERT insert
INSERT_AC insert_ac
INSERT_COMM insert_comm
INSERT_DEF insert_def
INSERT_DELETE insert_delete
INSERT_DIFF insert_diff
INSERT_INSERT insert_insert
INSERT_INTER insert_inter
INSERT_RESTRICT insert_restrict
INSERT_SUBSET insert_subset
INSERT_UNION insert_union
INSERT_UNION_EQ insert_union_eq
INSERT_UNIV insert_univ
INTER inter
INTERS inters
INTERSECTION_OF intersection_of
INTERSECTION_OF_EMPTY intersection_of_empty
INTERSECTION_OF_INC intersection_of_inc
INTERSECTION_OF_MONO intersection_of_mono
INTERS_0 inters_0
INTERS_1 inters_1
INTERS_2 inters_2
INTERS_ANTIMONO inters_antimono
INTERS_ANTIMONO_GEN inters_antimono_gen
INTERS_EQ_UNIV inters_eq_univ
INTERS_GSPEC inters_gspec
INTERS_IMAGE inters_image
INTERS_INSERT inters_insert
INTERS_IN_CHAIN inters_in_chain
INTERS_OVER_UNIONS inters_over_unions
INTERS_SUBSET inters_subset
INTERS_SUBSET_STRONG inters_subset_strong
INTERS_UNION inters_union
INTERS_UNIONS inters_unions
INTER_ACI inter_aci
INTER_ASSOC inter_assoc
INTER_CARTESIAN_PRODUCT inter_cartesian_product
INTER_COMM inter_comm
INTER_CROSS inter_cross
INTER_DISJOINT_UNION inter_disjoint_union
INTER_EMPTY inter_empty
INTER_IDEMPOT inter_idempot
INTER_INTERS inter_inters
INTER_OVER_UNION inter_over_union
INTER_RESTRICT inter_restrict
INTER_SUBSET inter_subset
INTER_UNIONS inter_unions
INTER_UNIONS_PAIRWISE_DISJOINT inter_unions_pairwise_disjoint
INTER_UNIV inter_univ
INVOLUTION_EVEN_FIXPOINTS involution_even_fixpoints
INVOLUTION_EVEN_NOFIXPOINTS involution_even_nofixpoints
IN_CARTESIAN_PRODUCT in_cartesian_product
IN_CROSS in_cross
IN_DELETE in_delete
IN_DELETE_EQ in_delete_eq
IN_DIFF in_diff
IN_DISJOINT in_disjoint
IN_ELIM_PAIR_THM in_elim_pair_thm
IN_ELIM_QUAD_THM in_elim_quad_thm
IN_ELIM_THM in_elim_thm
IN_ELIM_TRIPLE_THM in_elim_triple_thm
IN_EXTENSIONAL in_extensional
IN_EXTENSIONAL_UNDEFINED in_extensional_undefined
IN_GSPEC in_gspec
IN_IMAGE in_image
IN_INSERT in_insert
IN_INTER in_inter
IN_INTERS in_inters
IN_REST in_rest
IN_SET_OF_LIST in_set_of_list
IN_SING in_sing
IN_UNION in_union
IN_UNIONS in_unions
IN_UNIV in_univ
ITSET itset
ITSET_EQ itset_eq
LENGTH_LIST_OF_SET length_list_of_set
LE_C le_c_v1
LIST_OF_SET_EMPTY list_of_set_empty
LIST_OF_SET_PROPERTIES list_of_set_properties
LIST_OF_SET_SING list_of_set_sing
MEMBER_NOT_EMPTY member_not_empty
MEM_LIST_OF_SET mem_list_of_set
NOT_EMPTY_INSERT not_empty_insert
NOT_EQUAL_SETS not_equal_sets
NOT_INSERT_EMPTY not_insert_empty
NOT_IN_EMPTY not_in_empty
NOT_PSUBSET_EMPTY not_psubset_empty
NOT_UNIV_PSUBSET not_univ_psubset
NUMSEG_CLAUSES_LE numseg_clauses_le
NUMSEG_CLAUSES_LT numseg_clauses_lt
PAIRWISE_AND pairwise_and
PAIRWISE_CHAIN_UNIONS pairwise_chain_unions
PAIRWISE_EMPTY pairwise_empty
PAIRWISE_IMAGE pairwise_image
PAIRWISE_IMP pairwise_imp
PAIRWISE_INSERT pairwise_insert
PAIRWISE_INSERT_SYMMETRIC pairwise_insert_symmetric
PAIRWISE_MONO pairwise_mono
PAIRWISE_SING pairwise_sing
PAIRWISE_UNION pairwise_union
POWERSET_CLAUSES powerset_clauses
PRODUCT_MAP_RESTRICTION product_map_restriction
PSUBSET psubset
PSUBSET_ALT psubset_alt
PSUBSET_INSERT_SUBSET psubset_insert_subset
PSUBSET_IRREFL psubset_irrefl
PSUBSET_SUBSET_TRANS psubset_subset_trans
PSUBSET_TRANS psubset_trans
PSUBSET_UNIONS_PAIRWISE_DISJOINT psubset_unions_pairwise_disjoint
PSUBSET_UNIV psubset_univ
REAL_ABS_INF_LE real_abs_inf_le
REAL_ABS_SUP_LE real_abs_sup_le
REAL_INF_ASCLOSE real_inf_asclose
REAL_INF_BOUNDS real_inf_bounds
REAL_INF_LE real_inf_le
REAL_INF_LE_FINITE real_inf_le_finite
REAL_INF_LT_FINITE real_inf_lt_finite
REAL_INF_UNIQUE real_inf_unique
REAL_LE_INF real_le_inf
REAL_LE_INF_EQ real_le_inf_eq
REAL_LE_INF_FINITE real_le_inf_finite
REAL_LE_INF_SUBSET real_le_inf_subset
REAL_LE_SUP real_le_sup
REAL_LE_SUP_FINITE real_le_sup_finite
REAL_LT_INF_FINITE real_lt_inf_finite
REAL_LT_SUP_FINITE real_lt_sup_finite
REAL_MAX_SUP real_max_sup
REAL_MIN_INF real_min_inf
REAL_SUP_ASCLOSE real_sup_asclose
REAL_SUP_BOUNDS real_sup_bounds
REAL_SUP_EQ_INF real_sup_eq_inf
REAL_SUP_LE real_sup_le
REAL_SUP_LE_EQ real_sup_le_eq
REAL_SUP_LE_FINITE real_sup_le_finite
REAL_SUP_LE_SUBSET real_sup_le_subset
REAL_SUP_LT_FINITE real_sup_lt_finite
REAL_SUP_UNIQUE real_sup_unique
REST rest
RESTRICTION restriction
RESTRICTION_COMPOSE restriction_compose
RESTRICTION_COMPOSE_LEFT restriction_compose_left
RESTRICTION_COMPOSE_RIGHT restriction_compose_right
RESTRICTION_DEFINED restriction_defined
RESTRICTION_EQ restriction_eq
RESTRICTION_EXTENSION restriction_extension
RESTRICTION_FIXPOINT restriction_fixpoint
RESTRICTION_IDEMP restriction_idemp
RESTRICTION_IN_CARTESIAN_PRODUCT restriction_in_cartesian_product
RESTRICTION_IN_EXTENSIONAL restriction_in_extensional
RESTRICTION_RESTRICTION restriction_restriction
RESTRICTION_THM restriction_thm
RESTRICTION_UNDEFINED restriction_undefined
RESTRICTION_UNIQUE restriction_unique
RESTRICTION_UNIQUE_ALT restriction_unique_alt
RESTRICTION_UNIV restriction_univ
SETSPEC setspec
SET_CASES set_cases
SET_OF_LIST_APPEND set_of_list_append
SET_OF_LIST_EQ_EMPTY set_of_list_eq_empty
SET_OF_LIST_MAP set_of_list_map
SET_OF_LIST_OF_SET set_of_list_of_set
SET_PAIR_THM set_pair_thm
SET_PROVE_CASES set_prove_cases
SET_RECURSION_LEMMA set_recursion_lemma
SET_RULE set_rule
SET_TAC set_tac
SIMPLE_IMAGE simple_image
SIMPLE_IMAGE_GEN simple_image_gen
SING sing
SING_ALT sing_alt
SING_GSPEC sing_gspec
SING_SUBSET sing_subset
SUBSET subset
SUBSET_ANTISYM subset_antisym
SUBSET_ANTISYM_EQ subset_antisym_eq
SUBSET_CARD_EQ subset_card_eq
SUBSET_CARTESIAN_PRODUCT subset_cartesian_product
SUBSET_CROSS subset_cross
SUBSET_DELETE subset_delete
SUBSET_DIFF subset_diff
SUBSET_DISJOINT_UNION subset_disjoint_union
SUBSET_DISJOINT_UNION_EXISTS subset_disjoint_union_exists
SUBSET_EMPTY subset_empty
SUBSET_IMAGE subset_image
SUBSET_IMAGE_INJ subset_image_inj
SUBSET_INSERT subset_insert
SUBSET_INSERT_DELETE subset_insert_delete
SUBSET_INTER subset_inter
SUBSET_INTERS subset_inters
SUBSET_INTER_ABSORPTION subset_inter_absorption
SUBSET_PSUBSET_TRANS subset_psubset_trans
SUBSET_REFL subset_refl
SUBSET_RESTRICT subset_restrict
SUBSET_TRANS subset_trans
SUBSET_UNION subset_union
SUBSET_UNIONS subset_unions
SUBSET_UNION_ABSORPTION subset_union_absorption
SUBSET_UNIV subset_univ
SUP sup_v1
SUP_APPROACH sup_approach
SUP_EQ sup_eq
SUP_EXISTS sup_exists
SUP_FINITE sup_finite
SUP_FINITE_LEMMA sup_finite_lemma
SUP_INSERT_FINITE sup_insert_finite
SUP_INSERT_INSERT sup_insert_insert
SUP_SING sup_sing
SUP_UNION sup_union
SUP_UNIQUE sup_unique
SUP_UNIQUE_FINITE sup_unique_finite
SURJ surj
SURJECTIVE_EXISTS_THM surjective_exists_thm
SURJECTIVE_FORALL_THM surjective_forall_thm
SURJECTIVE_IFF_INJECTIVE surjective_iff_injective
SURJECTIVE_IFF_INJECTIVE_GEN surjective_iff_injective_gen
SURJECTIVE_IMAGE surjective_image
SURJECTIVE_IMAGE_EQ surjective_image_eq
SURJECTIVE_IMAGE_THM surjective_image_thm
SURJECTIVE_ON_IMAGE surjective_on_image
SURJECTIVE_ON_PREIMAGE surjective_on_preimage
SURJECTIVE_ON_RIGHT_INVERSE surjective_on_right_inverse
SURJECTIVE_PREIMAGE surjective_preimage
SURJECTIVE_RIGHT_INVERSE surjective_right_inverse
UNION union
UNIONS unions
UNIONS_0 unions_0
UNIONS_1 unions_1
UNIONS_2 unions_2
UNIONS_DELETE_EMPTY unions_delete_empty
UNIONS_DIFF unions_diff
UNIONS_EQ_INTERS unions_eq_inters
UNIONS_GSPEC unions_gspec
UNIONS_IMAGE unions_image
UNIONS_INSERT unions_insert
UNIONS_INSERT_EMPTY unions_insert_empty
UNIONS_INTERS unions_inters
UNIONS_IN_CHAIN unions_in_chain
UNIONS_MAXIMAL_SETS unions_maximal_sets
UNIONS_MONO unions_mono
UNIONS_MONO_IMAGE unions_mono_image
UNIONS_OVER_INTERS unions_over_inters
UNIONS_SINGS unions_sings
UNIONS_SINGS_GEN unions_sings_gen
UNIONS_SUBSET unions_subset
UNIONS_UNION unions_union
UNIONS_UNIV unions_univ
UNION_ACI union_aci
UNION_ASSOC union_assoc
UNION_COMM union_comm
UNION_DISJOINT_UNION union_disjoint_union
UNION_EMPTY union_empty
UNION_IDEMPOT union_idempot
UNION_OF union_of
UNION_OF_EMPTY union_of_empty
UNION_OF_INC union_of_inc
UNION_OF_MONO union_of_mono
UNION_OVER_INTER union_over_inter
UNION_RESTRICT union_restrict
UNION_SUBSET union_subset
UNION_UNIV union_univ
UNIV univ
UNIV_1 univ_1
UNIV_GSPEC univ_gspec
UNIV_NOT_EMPTY univ_not_empty
UNIV_SUBSET univ_subset
WF_FINITE wf_finite
WF_PSUBSET wf_psubset
cartesian_product cartesian_product
dest_setenum dest_setenum
disjoint_union disjoint_union_v1
eq_c eq_c
ge_c ge_c
gt_c gt_c
has_inf has_inf
has_sup has_sup
inf inf
is_setenum is_setenum
le_c le_c
list_of_set list_of_set
lt_c lt_c
mk_fset mk_fset
mk_setenum mk_setenum
new_inductive_set new_inductive_set
num_FINITE num_finite
num_FINITE_AVOID num_finite_avoid
num_INFINITE num_infinite
num_INFINITE_EQ num_infinite_eq
pairwise pairwise
product_map product_map
real_INFINITE real_infinite
set_of_list set_of_list
string_INFINITE string_infinite
sup sup
