import
import_segment "hol4"
def_maps
"count" > "count_primdef"
"UNIV" > "UNIV_def"
"UNION" > "UNION_def"
"SURJ" > "SURJ_def"
"SUBSET" > "SUBSET_def"
"SING" > "SING_def"
"RINV" > "RINV_def"
"REST" > "REST_def"
"PSUBSET" > "PSUBSET_def"
"LINV" > "LINV_def"
"ITSET_tupled" > "ITSET_tupled_def"
"ITSET" > "ITSET_def"
"INTER" > "INTER_def"
"INSERT" > "INSERT_def"
"INJ" > "INJ_def"
"INFINITE" > "INFINITE_def"
"IMAGE" > "IMAGE_def"
"GSPEC" > "GSPEC_def"
"FINITE" > "FINITE_def"
"EMPTY" > "EMPTY_def"
"DISJOINT" > "DISJOINT_def"
"DIFF" > "DIFF_def"
"DELETE" > "DELETE_def"
"CROSS" > "CROSS_def"
"COMPL" > "COMPL_def"
"CHOICE" > "CHOICE_def"
"CARD" > "CARD_def"
"BIJ" > "BIJ_def"
"BIGUNION" > "BIGUNION_def"
"BIGINTER" > "BIGINTER_def"
const_maps
"count" > "HOL4Base.pred_set.count"
"UNIV" > "HOL4Base.pred_set.UNIV"
"UNION" > "HOL4Base.pred_set.UNION"
"SURJ" > "HOL4Base.pred_set.SURJ"
"SUBSET" > "HOL4Base.pred_set.SUBSET"
"SING" > "HOL4Base.pred_set.SING"
"REST" > "HOL4Base.pred_set.REST"
"PSUBSET" > "HOL4Base.pred_set.PSUBSET"
"ITSET_tupled" > "HOL4Base.pred_set.ITSET_tupled"
"ITSET" > "HOL4Base.pred_set.ITSET"
"INTER" > "HOL4Base.pred_set.INTER"
"INSERT" > "HOL4Base.pred_set.INSERT"
"INJ" > "HOL4Base.pred_set.INJ"
"INFINITE" > "HOL4Base.pred_set.INFINITE"
"IMAGE" > "HOL4Base.pred_set.IMAGE"
"FINITE" > "HOL4Base.pred_set.FINITE"
"EMPTY" > "HOL4Base.pred_set.EMPTY"
"DISJOINT" > "HOL4Base.pred_set.DISJOINT"
"DIFF" > "HOL4Base.pred_set.DIFF"
"DELETE" > "HOL4Base.pred_set.DELETE"
"CROSS" > "HOL4Base.pred_set.CROSS"
"COMPL" > "HOL4Base.pred_set.COMPL"
"BIJ" > "HOL4Base.pred_set.BIJ"
"BIGUNION" > "HOL4Base.pred_set.BIGUNION"
"BIGINTER" > "HOL4Base.pred_set.BIGINTER"
thm_maps
"count_primdef" > "HOL4Base.pred_set.count_primdef"
"count_def" > "HOL4Base.pred_set.count_def"
"UNIV_def" > "HOL4Base.pred_set.UNIV_def"
"UNIV_SUBSET" > "HOL4Base.pred_set.UNIV_SUBSET"
"UNIV_NOT_EMPTY" > "HOL4Base.pred_set.UNIV_NOT_EMPTY"
"UNIV_DEF" > "HOL4Base.pred_set.UNIV_DEF"
"UNION_def" > "HOL4Base.pred_set.UNION_def"
"UNION_UNIV" > "HOL4Base.pred_set.UNION_UNIV"
"UNION_SUBSET" > "HOL4Base.pred_set.UNION_SUBSET"
"UNION_OVER_INTER" > "HOL4Base.pred_set.UNION_OVER_INTER"
"UNION_IDEMPOT" > "HOL4Base.pred_set.UNION_IDEMPOT"
"UNION_EMPTY" > "HOL4Base.pred_set.UNION_EMPTY"
"UNION_DEF" > "HOL4Base.pred_set.UNION_DEF"
"UNION_COMM" > "HOL4Base.pred_set.UNION_COMM"
"UNION_ASSOC" > "HOL4Base.pred_set.UNION_ASSOC"
"SURJ_def" > "HOL4Base.pred_set.SURJ_def"
"SURJ_ID" > "HOL4Base.pred_set.SURJ_ID"
"SURJ_EMPTY" > "HOL4Base.pred_set.SURJ_EMPTY"
"SURJ_DEF" > "HOL4Base.pred_set.SURJ_DEF"
"SURJ_COMPOSE" > "HOL4Base.pred_set.SURJ_COMPOSE"
"SUBSET_def" > "HOL4Base.pred_set.SUBSET_def"
"SUBSET_UNIV" > "HOL4Base.pred_set.SUBSET_UNIV"
"SUBSET_UNION_ABSORPTION" > "HOL4Base.pred_set.SUBSET_UNION_ABSORPTION"
"SUBSET_UNION" > "HOL4Base.pred_set.SUBSET_UNION"
"SUBSET_TRANS" > "HOL4Base.pred_set.SUBSET_TRANS"
"SUBSET_REFL" > "HOL4Base.pred_set.SUBSET_REFL"
"SUBSET_INTER_ABSORPTION" > "HOL4Base.pred_set.SUBSET_INTER_ABSORPTION"
"SUBSET_INTER" > "HOL4Base.pred_set.SUBSET_INTER"
"SUBSET_INSERT_DELETE" > "HOL4Base.pred_set.SUBSET_INSERT_DELETE"
"SUBSET_INSERT" > "HOL4Base.pred_set.SUBSET_INSERT"
"SUBSET_FINITE" > "HOL4Base.pred_set.SUBSET_FINITE"
"SUBSET_EMPTY" > "HOL4Base.pred_set.SUBSET_EMPTY"
"SUBSET_DELETE" > "HOL4Base.pred_set.SUBSET_DELETE"
"SUBSET_DEF" > "HOL4Base.pred_set.SUBSET_DEF"
"SUBSET_BIGINTER" > "HOL4Base.pred_set.SUBSET_BIGINTER"
"SUBSET_ANTISYM" > "HOL4Base.pred_set.SUBSET_ANTISYM"
"SPECIFICATION" > "HOL4Base.bool.IN_DEF"
"SING_def" > "HOL4Base.pred_set.SING_def"
"SING_IFF_EMPTY_REST" > "HOL4Base.pred_set.SING_IFF_EMPTY_REST"
"SING_IFF_CARD1" > "HOL4Base.pred_set.SING_IFF_CARD1"
"SING_FINITE" > "HOL4Base.pred_set.SING_FINITE"
"SING_DELETE" > "HOL4Base.pred_set.SING_DELETE"
"SING_DEF" > "HOL4Base.pred_set.SING_DEF"
"SING" > "HOL4Base.pred_set.SING"
"SET_MINIMUM" > "HOL4Base.pred_set.SET_MINIMUM"
"SET_CASES" > "HOL4Base.pred_set.SET_CASES"
"RINV_DEF" > "HOL4Base.pred_set.RINV_DEF"
"REST_def" > "HOL4Base.pred_set.REST_def"
"REST_SUBSET" > "HOL4Base.pred_set.REST_SUBSET"
"REST_SING" > "HOL4Base.pred_set.REST_SING"
"REST_PSUBSET" > "HOL4Base.pred_set.REST_PSUBSET"
"REST_DEF" > "HOL4Base.pred_set.REST_DEF"
"PSUBSET_def" > "HOL4Base.pred_set.PSUBSET_def"
"PSUBSET_UNIV" > "HOL4Base.pred_set.PSUBSET_UNIV"
"PSUBSET_TRANS" > "HOL4Base.pred_set.PSUBSET_TRANS"
"PSUBSET_MEMBER" > "HOL4Base.pred_set.PSUBSET_MEMBER"
"PSUBSET_IRREFL" > "HOL4Base.pred_set.PSUBSET_IRREFL"
"PSUBSET_INSERT_SUBSET" > "HOL4Base.pred_set.PSUBSET_INSERT_SUBSET"
"PSUBSET_FINITE" > "HOL4Base.pred_set.PSUBSET_FINITE"
"PSUBSET_DEF" > "HOL4Base.pred_set.PSUBSET_DEF"
"NUM_SET_WOP" > "HOL4Base.pred_set.NUM_SET_WOP"
"NOT_UNIV_PSUBSET" > "HOL4Base.pred_set.NOT_UNIV_PSUBSET"
"NOT_SING_EMPTY" > "HOL4Base.pred_set.NOT_SING_EMPTY"
"NOT_PSUBSET_EMPTY" > "HOL4Base.pred_set.NOT_PSUBSET_EMPTY"
"NOT_IN_FINITE" > "HOL4Base.pred_set.NOT_IN_FINITE"
"NOT_IN_EMPTY" > "HOL4Base.pred_set.NOT_IN_EMPTY"
"NOT_INSERT_EMPTY" > "HOL4Base.pred_set.NOT_INSERT_EMPTY"
"NOT_EQUAL_SETS" > "HOL4Base.pred_set.NOT_EQUAL_SETS"
"NOT_EMPTY_SING" > "HOL4Base.pred_set.NOT_EMPTY_SING"
"NOT_EMPTY_INSERT" > "HOL4Base.pred_set.NOT_EMPTY_INSERT"
"MEMBER_NOT_EMPTY" > "HOL4Base.pred_set.MEMBER_NOT_EMPTY"
"LINV_DEF" > "HOL4Base.pred_set.LINV_DEF"
"LESS_CARD_DIFF" > "HOL4Base.pred_set.LESS_CARD_DIFF"
"ITSET_tupled_primitive_def" > "HOL4Base.pred_set.ITSET_tupled_primitive_def"
"ITSET_tupled_def" > "HOL4Base.pred_set.ITSET_tupled_def"
"ITSET_def" > "HOL4Base.pred_set.ITSET_def"
"ITSET_curried_def" > "HOL4Base.pred_set.ITSET_curried_def"
"ITSET_THM" > "HOL4Base.pred_set.ITSET_THM"
"ITSET_IND" > "HOL4Base.pred_set.ITSET_IND"
"ITSET_EMPTY" > "HOL4Base.pred_set.ITSET_EMPTY"
"IN_UNIV" > "HOL4Base.pred_set.IN_UNIV"
"IN_UNION" > "HOL4Base.pred_set.IN_UNION"
"IN_SING" > "HOL4Base.pred_set.IN_SING"
"IN_INTER" > "HOL4Base.pred_set.IN_INTER"
"IN_INSERT" > "HOL4Base.pred_set.IN_INSERT"
"IN_INFINITE_NOT_FINITE" > "HOL4Base.pred_set.IN_INFINITE_NOT_FINITE"
"IN_IMAGE" > "HOL4Base.pred_set.IN_IMAGE"
"IN_DISJOINT" > "HOL4Base.pred_set.IN_DISJOINT"
"IN_DIFF" > "HOL4Base.pred_set.IN_DIFF"
"IN_DELETE_EQ" > "HOL4Base.pred_set.IN_DELETE_EQ"
"IN_DELETE" > "HOL4Base.pred_set.IN_DELETE"
"IN_CROSS" > "HOL4Base.pred_set.IN_CROSS"
"IN_COUNT" > "HOL4Base.pred_set.IN_COUNT"
"IN_COMPL" > "HOL4Base.pred_set.IN_COMPL"
"IN_BIGUNION" > "HOL4Base.pred_set.IN_BIGUNION"
"IN_BIGINTER" > "HOL4Base.pred_set.IN_BIGINTER"
"INTER_def" > "HOL4Base.pred_set.INTER_def"
"INTER_UNIV" > "HOL4Base.pred_set.INTER_UNIV"
"INTER_UNION_COMPL" > "HOL4Base.pred_set.INTER_UNION_COMPL"
"INTER_SUBSET" > "HOL4Base.pred_set.INTER_SUBSET"
"INTER_OVER_UNION" > "HOL4Base.pred_set.INTER_OVER_UNION"
"INTER_IDEMPOT" > "HOL4Base.pred_set.INTER_IDEMPOT"
"INTER_FINITE" > "HOL4Base.pred_set.INTER_FINITE"
"INTER_EMPTY" > "HOL4Base.pred_set.INTER_EMPTY"
"INTER_DEF" > "HOL4Base.pred_set.INTER_DEF"
"INTER_COMM" > "HOL4Base.pred_set.INTER_COMM"
"INTER_ASSOC" > "HOL4Base.pred_set.INTER_ASSOC"
"INSERT_def" > "HOL4Base.pred_set.INSERT_def"
"INSERT_UNIV" > "HOL4Base.pred_set.INSERT_UNIV"
"INSERT_UNION_EQ" > "HOL4Base.pred_set.INSERT_UNION_EQ"
"INSERT_UNION" > "HOL4Base.pred_set.INSERT_UNION"
"INSERT_SUBSET" > "HOL4Base.pred_set.INSERT_SUBSET"
"INSERT_SING_UNION" > "HOL4Base.pred_set.INSERT_SING_UNION"
"INSERT_INTER" > "HOL4Base.pred_set.INSERT_INTER"
"INSERT_INSERT" > "HOL4Base.pred_set.INSERT_INSERT"
"INSERT_DIFF" > "HOL4Base.pred_set.INSERT_DIFF"
"INSERT_DELETE" > "HOL4Base.pred_set.INSERT_DELETE"
"INSERT_DEF" > "HOL4Base.pred_set.INSERT_DEF"
"INSERT_COMM" > "HOL4Base.pred_set.INSERT_COMM"
"INJ_def" > "HOL4Base.pred_set.INJ_def"
"INJ_ID" > "HOL4Base.pred_set.INJ_ID"
"INJ_EMPTY" > "HOL4Base.pred_set.INJ_EMPTY"
"INJ_DEF" > "HOL4Base.pred_set.INJ_DEF"
"INJ_COMPOSE" > "HOL4Base.pred_set.INJ_COMPOSE"
"INFINITE_def" > "HOL4Base.pred_set.INFINITE_def"
"INFINITE_UNIV" > "HOL4Base.pred_set.INFINITE_UNIV"
"INFINITE_SUBSET" > "HOL4Base.pred_set.INFINITE_SUBSET"
"INFINITE_INHAB" > "HOL4Base.pred_set.INFINITE_INHAB"
"INFINITE_DIFF_FINITE" > "HOL4Base.pred_set.INFINITE_DIFF_FINITE"
"INFINITE_DEF" > "HOL4Base.pred_set.INFINITE_DEF"
"IMAGE_def" > "HOL4Base.pred_set.IMAGE_def"
"IMAGE_UNION" > "HOL4Base.pred_set.IMAGE_UNION"
"IMAGE_SURJ" > "HOL4Base.pred_set.IMAGE_SURJ"
"IMAGE_SUBSET" > "HOL4Base.pred_set.IMAGE_SUBSET"
"IMAGE_INTER" > "HOL4Base.pred_set.IMAGE_INTER"
"IMAGE_INSERT" > "HOL4Base.pred_set.IMAGE_INSERT"
"IMAGE_IN" > "HOL4Base.pred_set.IMAGE_IN"
"IMAGE_ID" > "HOL4Base.pred_set.IMAGE_ID"
"IMAGE_FINITE" > "HOL4Base.pred_set.IMAGE_FINITE"
"IMAGE_EQ_EMPTY" > "HOL4Base.pred_set.IMAGE_EQ_EMPTY"
"IMAGE_EMPTY" > "HOL4Base.pred_set.IMAGE_EMPTY"
"IMAGE_DELETE" > "HOL4Base.pred_set.IMAGE_DELETE"
"IMAGE_DEF" > "HOL4Base.pred_set.IMAGE_DEF"
"IMAGE_COMPOSE" > "HOL4Base.pred_set.IMAGE_COMPOSE"
"IMAGE_11_INFINITE" > "HOL4Base.pred_set.IMAGE_11_INFINITE"
"GSPECIFICATION" > "HOL4Base.pred_set.GSPECIFICATION"
"FINITE_def" > "HOL4Base.pred_set.FINITE_def"
"FINITE_WEAK_ENUMERATE" > "HOL4Base.pred_set.FINITE_WEAK_ENUMERATE"
"FINITE_UNION" > "HOL4Base.pred_set.FINITE_UNION"
"FINITE_SING" > "HOL4Base.pred_set.FINITE_SING"
"FINITE_PSUBSET_UNIV" > "HOL4Base.pred_set.FINITE_PSUBSET_UNIV"
"FINITE_PSUBSET_INFINITE" > "HOL4Base.pred_set.FINITE_PSUBSET_INFINITE"
"FINITE_ISO_NUM" > "HOL4Base.pred_set.FINITE_ISO_NUM"
"FINITE_INSERT" > "HOL4Base.pred_set.FINITE_INSERT"
"FINITE_INDUCT" > "HOL4Base.pred_set.FINITE_INDUCT"
"FINITE_EMPTY" > "HOL4Base.pred_set.FINITE_EMPTY"
"FINITE_DIFF" > "HOL4Base.pred_set.FINITE_DIFF"
"FINITE_DELETE" > "HOL4Base.pred_set.FINITE_DELETE"
"FINITE_DEF" > "HOL4Base.pred_set.FINITE_DEF"
"FINITE_CROSS_EQ" > "HOL4Base.pred_set.FINITE_CROSS_EQ"
"FINITE_CROSS" > "HOL4Base.pred_set.FINITE_CROSS"
"FINITE_COUNT" > "HOL4Base.pred_set.FINITE_COUNT"
"FINITE_COMPLETE_INDUCTION" > "HOL4Base.pred_set.FINITE_COMPLETE_INDUCTION"
"FINITE_BIGUNION" > "HOL4Base.pred_set.FINITE_BIGUNION"
"EXTENSION" > "HOL4Base.pred_set.EXTENSION"
"EQ_UNIV" > "HOL4Base.pred_set.EQ_UNIV"
"EQUAL_SING" > "HOL4Base.pred_set.EQUAL_SING"
"EMPTY_def" > "HOL4Base.pred_set.EMPTY_def"
"EMPTY_UNION" > "HOL4Base.pred_set.EMPTY_UNION"
"EMPTY_SUBSET" > "HOL4Base.pred_set.EMPTY_SUBSET"
"EMPTY_NOT_UNIV" > "HOL4Base.pred_set.EMPTY_NOT_UNIV"
"EMPTY_DIFF" > "HOL4Base.pred_set.EMPTY_DIFF"
"EMPTY_DELETE" > "HOL4Base.pred_set.EMPTY_DELETE"
"EMPTY_DEF" > "HOL4Base.pred_set.EMPTY_DEF"
"DISJOINT_def" > "HOL4Base.pred_set.DISJOINT_def"
"DISJOINT_UNION_BOTH" > "HOL4Base.pred_set.DISJOINT_UNION_BOTH"
"DISJOINT_UNION" > "HOL4Base.pred_set.DISJOINT_UNION"
"DISJOINT_SYM" > "HOL4Base.pred_set.DISJOINT_SYM"
"DISJOINT_SING_EMPTY" > "HOL4Base.pred_set.DISJOINT_SING_EMPTY"
"DISJOINT_INSERT" > "HOL4Base.pred_set.DISJOINT_INSERT"
"DISJOINT_EMPTY_REFL" > "HOL4Base.pred_set.DISJOINT_EMPTY_REFL"
"DISJOINT_EMPTY" > "HOL4Base.pred_set.DISJOINT_EMPTY"
"DISJOINT_DELETE_SYM" > "HOL4Base.pred_set.DISJOINT_DELETE_SYM"
"DISJOINT_DEF" > "HOL4Base.pred_set.DISJOINT_DEF"
"DISJOINT_BIGUNION" > "HOL4Base.pred_set.DISJOINT_BIGUNION"
"DISJOINT_BIGINTER" > "HOL4Base.pred_set.DISJOINT_BIGINTER"
"DIFF_def" > "HOL4Base.pred_set.DIFF_def"
"DIFF_UNIV" > "HOL4Base.pred_set.DIFF_UNIV"
"DIFF_INSERT" > "HOL4Base.pred_set.DIFF_INSERT"
"DIFF_EQ_EMPTY" > "HOL4Base.pred_set.DIFF_EQ_EMPTY"
"DIFF_EMPTY" > "HOL4Base.pred_set.DIFF_EMPTY"
"DIFF_DIFF" > "HOL4Base.pred_set.DIFF_DIFF"
"DIFF_DEF" > "HOL4Base.pred_set.DIFF_DEF"
"DELETE_def" > "HOL4Base.pred_set.DELETE_def"
"DELETE_SUBSET" > "HOL4Base.pred_set.DELETE_SUBSET"
"DELETE_NON_ELEMENT" > "HOL4Base.pred_set.DELETE_NON_ELEMENT"
"DELETE_INTER" > "HOL4Base.pred_set.DELETE_INTER"
"DELETE_INSERT" > "HOL4Base.pred_set.DELETE_INSERT"
"DELETE_EQ_SING" > "HOL4Base.pred_set.DELETE_EQ_SING"
"DELETE_DELETE" > "HOL4Base.pred_set.DELETE_DELETE"
"DELETE_DEF" > "HOL4Base.pred_set.DELETE_DEF"
"DELETE_COMM" > "HOL4Base.pred_set.DELETE_COMM"
"DECOMPOSITION" > "HOL4Base.pred_set.DECOMPOSITION"
"CROSS_def" > "HOL4Base.pred_set.CROSS_def"
"CROSS_SUBSET" > "HOL4Base.pred_set.CROSS_SUBSET"
"CROSS_SINGS" > "HOL4Base.pred_set.CROSS_SINGS"
"CROSS_INSERT_RIGHT" > "HOL4Base.pred_set.CROSS_INSERT_RIGHT"
"CROSS_INSERT_LEFT" > "HOL4Base.pred_set.CROSS_INSERT_LEFT"
"CROSS_EMPTY" > "HOL4Base.pred_set.CROSS_EMPTY"
"CROSS_DEF" > "HOL4Base.pred_set.CROSS_DEF"
"COUNT_ZERO" > "HOL4Base.pred_set.COUNT_ZERO"
"COUNT_SUC" > "HOL4Base.pred_set.COUNT_SUC"
"COMPONENT" > "HOL4Base.pred_set.COMPONENT"
"COMPL_def" > "HOL4Base.pred_set.COMPL_def"
"COMPL_SPLITS" > "HOL4Base.pred_set.COMPL_SPLITS"
"COMPL_EMPTY" > "HOL4Base.pred_set.COMPL_EMPTY"
"COMPL_DEF" > "HOL4Base.pred_set.COMPL_DEF"
"COMPL_COMPL" > "HOL4Base.pred_set.COMPL_COMPL"
"COMPL_CLAUSES" > "HOL4Base.pred_set.COMPL_CLAUSES"
"CHOICE_SING" > "HOL4Base.pred_set.CHOICE_SING"
"CHOICE_NOT_IN_REST" > "HOL4Base.pred_set.CHOICE_NOT_IN_REST"
"CHOICE_INSERT_REST" > "HOL4Base.pred_set.CHOICE_INSERT_REST"
"CHOICE_DEF" > "HOL4Base.pred_set.CHOICE_DEF"
"CARD_UNION" > "HOL4Base.pred_set.CARD_UNION"
"CARD_SUBSET" > "HOL4Base.pred_set.CARD_SUBSET"
"CARD_SING_CROSS" > "HOL4Base.pred_set.CARD_SING_CROSS"
"CARD_SING" > "HOL4Base.pred_set.CARD_SING"
"CARD_PSUBSET" > "HOL4Base.pred_set.CARD_PSUBSET"
"CARD_INTER_LESS_EQ" > "HOL4Base.pred_set.CARD_INTER_LESS_EQ"
"CARD_INSERT" > "HOL4Base.pred_set.CARD_INSERT"
"CARD_EQ_0" > "HOL4Base.pred_set.CARD_EQ_0"
"CARD_EMPTY" > "HOL4Base.pred_set.CARD_EMPTY"
"CARD_DIFF" > "HOL4Base.pred_set.CARD_DIFF"
"CARD_DELETE" > "HOL4Base.pred_set.CARD_DELETE"
"CARD_DEF" > "HOL4Base.pred_set.CARD_DEF"
"CARD_CROSS" > "HOL4Base.pred_set.CARD_CROSS"
"CARD_COUNT" > "HOL4Base.pred_set.CARD_COUNT"
"BIJ_def" > "HOL4Base.pred_set.BIJ_def"
"BIJ_ID" > "HOL4Base.pred_set.BIJ_ID"
"BIJ_EMPTY" > "HOL4Base.pred_set.BIJ_EMPTY"
"BIJ_DEF" > "HOL4Base.pred_set.BIJ_DEF"
"BIJ_COMPOSE" > "HOL4Base.pred_set.BIJ_COMPOSE"
"BIGUNION_def" > "HOL4Base.pred_set.BIGUNION_def"
"BIGUNION_UNION" > "HOL4Base.pred_set.BIGUNION_UNION"
"BIGUNION_SUBSET" > "HOL4Base.pred_set.BIGUNION_SUBSET"
"BIGUNION_SING" > "HOL4Base.pred_set.BIGUNION_SING"
"BIGUNION_INSERT" > "HOL4Base.pred_set.BIGUNION_INSERT"
"BIGUNION_EMPTY" > "HOL4Base.pred_set.BIGUNION_EMPTY"
"BIGUNION" > "HOL4Base.pred_set.BIGUNION"
"BIGINTER_def" > "HOL4Base.pred_set.BIGINTER_def"
"BIGINTER_SING" > "HOL4Base.pred_set.BIGINTER_SING"
"BIGINTER_INTER" > "HOL4Base.pred_set.BIGINTER_INTER"
"BIGINTER_INSERT" > "HOL4Base.pred_set.BIGINTER_INSERT"
"BIGINTER_EMPTY" > "HOL4Base.pred_set.BIGINTER_EMPTY"
"BIGINTER" > "HOL4Base.pred_set.BIGINTER"
"ABSORPTION" > "HOL4Base.pred_set.ABSORPTION"
end