environ
vocabularies HIDDEN, XBOOLE_0, STRUCT_0, MSUALG_1, CARD_3, RELAT_1, FUNCT_1, SUBSET_1, PBOOLE, MSUALG_3, TARSKI, FUNCT_6, MEMBER_1, CATALG_1, ZF_MODEL, MSUALG_2, MSAFREE, FUNCOP_1, CARD_1, LANG1, ZFMISC_1, TREES_4, MCART_1, MARGREL1, FINSEQ_1, MSATERM, UNIALG_2, DTCONSTR, FINSET_1, TREES_2, TREES_9, ZF_LANG1, TREES_3, TREES_A, NUMBERS, ARYTM_3, ORDINAL4, XXREAL_0, NAT_1, PARTFUN1, MSUALG_6, PRELAMB, SETLIM_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, DOMAIN_1, RELAT_1, FUNCT_1, RELSET_1, STRUCT_0, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, MCART_1, FINSET_1, CARD_3, FINSEQ_1, FINSEQ_2, TREES_1, TREES_2, FUNCT_6, TREES_3, TREES_4, DTCONSTR, LANG1, PBOOLE, TREES_9, MSUALG_1, MSUALG_2, MSAFREE, FUNCOP_1, MSUALG_3, EQUATION, MSATERM, MSUALG_6, CATALG_1, XXREAL_0;
definitions TARSKI, XBOOLE_0, PBOOLE, MSUALG_2, MSUALG_6, CATALG_1;
theorems TARSKI, ZFMISC_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_3, NAT_1, MCART_1, PBOOLE, RELAT_1, CARD_3, CARD_5, FUNCT_6, TREES_3, MSUALG_1, INSTALG1, TREES_4, PRE_CIRC, TREES_1, TREES_2, MSUALG_2, MSUALG_3, MSAFREE, MSATERM, EQUATION, MSUALG_6, XBOOLE_0, XBOOLE_1, ORDINAL1, PARTFUN1, TREES_9, FINSEQ_2, XTUPLE_0;
schemes PBOOLE, MSATERM;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, XREAL_0, FINSEQ_1, TREES_2, TREES_3, TREES_9, STRUCT_0, RELSET_1, MSUALG_1, MSUALG_2, MSUALG_3, MSAFREE, MSATERM, INDEX_1, MSUALG_6, MSUALG_9, INSTALG1, CATALG_1, MSSUBFAM, PBOOLE, XTUPLE_0;
constructors HIDDEN, DOMAIN_1, TREES_9, MSUALG_3, MSATERM, MSUALG_6, CATALG_1, EQUATION, SEQ_4, RELSET_1, XTUPLE_0;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS;
equalities TARSKI;
expansions TARSKI, PBOOLE, MSUALG_2;