environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, QC_LANG1, CQC_LANG, XBOOLE_0, VALUAT_1, FINSEQ_1, HENMODEL, CQC_THE1, XBOOLEAN, BVFUNC_2, FUNCT_1, ORDINAL4, ARYTM_3, RELAT_1, CARD_1, XXREAL_0, TARSKI, ZF_MODEL, REALSET1, ARYTM_1, CARD_3, ZFMISC_1, FINSET_1, MCART_1, NAT_1, ORDINAL1, GOEDELCP, MARGREL1, FUNCT_2, QC_TRANS, GOEDCPUC;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, XXREAL_0, CARD_1, CARD_3, FINSEQ_1, RELAT_1, QC_LANG1, QC_LANG2, ORDINAL1, NUMBERS, CQC_THE1, CQC_LANG, FUNCT_1, FINSET_1, VALUAT_1, RELSET_1, FUNCT_2, NAT_1, CQC_SIM1, DOMAIN_1, MCART_1, SUBSTUT1, SUBLEMMA, SUBSTUT2, CALCUL_1, HENMODEL, GOEDELCP, MARGREL1, QC_LANG3, FUNCT_4, FUNCOP_1, COHSP_1, QC_TRANS, XTUPLE_0;
definitions TARSKI;
theorems TARSKI, FUNCT_1, XBOOLE_0, XBOOLE_1, QC_LANG1, ZFMISC_1, QC_LANG2, HENMODEL, CALCUL_1, SUBLEMMA, NAT_1, FINSEQ_1, VALUAT_1, FUNCT_2, XXREAL_0, ORDINAL1, CARD_1, GOEDELCP, ORDERS_1, COHSP_1, QC_TRANS, XTUPLE_0;
schemes NAT_1, FUNCT_1, CQC_LANG, FINSET_1;
registrations SUBSET_1, RELAT_1, ORDINAL1, XXREAL_0, XREAL_0, FINSEQ_1, FINSET_1, XBOOLE_0, QC_LANG1, CQC_LANG, QC_TRANS, XTUPLE_0, NAT_1;
constructors HIDDEN, SETFAM_1, DOMAIN_1, XXREAL_0, NAT_1, NAT_D, FINSEQ_2, QC_LANG1, CQC_THE1, CQC_SIM1, SUBSTUT2, CALCUL_1, HENMODEL, CARD_3, RELSET_1, CARD_1, WELLORD2, GOEDELCP, VALUAT_1, MARGREL1, CQC_LANG, QC_LANG3, FUNCT_4, FUNCOP_1, COHSP_1, QC_TRANS;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities TARSKI;
expansions TARSKI;