\chapter{Basic Set Theory}

\begin{definition}\label{def:ffafbgjgch}
$\mname{UPair}$ is the opaque object of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 74243828e4e6c9c0b467551f19c2ddaebf843f72e2437cc2dea41d079a31107f \\
Pure Object Address: & TMVRUmJTotqxWfVB8wE3prBP8W149nntsis \\
Theory Object Id: & dc313483331e27588bf1a1b69cd5f5c7e098db82519bb4f97f7410379392841d \\
Theory Object Address: & TMX4EvisNRDE5LYNME7fAsXyPiC8WnAhWDf
\end{tabular}
\end{center}

\end{definition}
{\bf{Notation.}} We write $\{x,y\}$ for $\mname{UPair}~x~y$.

\begin{verbatim}
UPairE
\end{verbatim}
\begin{theorem}\label{thm:ffafbgjgchfe} ${\unicdcdadad x y z : {\iota} .  {{{x} \in {\{{y},{z}\}}}\unicdbdjdcd{{{x}={y}}\unicdcdcdid{{x}={z}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 5009cc2fb54e181e885e6ba3ebb81d1e7e8a680ac7694595d03d2bae261e7b96 \\
Pure Prop Address: & TMGwnYYsQikhZ63aRncU1cXAkHjKyj9bmC5 \\
Theory Prop Id: & e67fc59933588258cbf12faa14d08a2171e75c4be3c6375f1c244269e8f0a620 \\
Theory Prop Address: & TMZokDUxWLSRz89jtEJyPSvuwJgZmLVRkEK
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
UPairI1
\end{verbatim}
\begin{theorem}\label{thm:ffafbgjgchjebd} ${\unicdcdadad y z : {\iota} .  {{y} \in {\{{y},{z}\}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & b1eea2f239b14cf1d5593f79c76232b611aa52ae4809066c3fff5897fe4a9d56 \\
Pure Prop Address: & TMPfeeVFA54LBD1V3Ejp5GiM71yeFdjdpEG \\
Theory Prop Id: & bf36495fbbdc72eb575c69fdfc681c506ae9eebfb94538f10549bc8f191ce07b \\
Theory Prop Address: & TMd3cJnuukmmggqVuKQroUQUyw9xFNmdytb
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
UPairI2
\end{verbatim}
\begin{theorem}\label{thm:ffafbgjgchjecd} ${\unicdcdadad y z : {\iota} .  {{z} \in {\{{y},{z}\}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 27455b29a050cd7d072a6fecd331e4463360653ad07926e47c46ee56e5b66f75 \\
Pure Prop Address: & TMdg8pGYbTqgx8xPL9PwPu2pJJbSoxCnRHy \\
Theory Prop Id: & a0a5b852859049d097662ba32a64381a0c4251956d0027ceea65617e12ec7e68 \\
Theory Prop Address: & TMTrsMdWZgjAwNgkT5uqy2DqzBnBXnxWupZ
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
UPair_com
\end{verbatim}
\begin{theorem}\label{thm:ffafbgjgchpfdgpgng} ${\unicdcdadad x y : {\iota} .  {{\{{x},{y}\}}={\{{y},{x}\}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & b0847098a703dd9518520ce0538ef2bb61b423ef3bfce3e056d6ddebc96a5b10 \\
Pure Prop Address: & TMTDNchhQ5726g1za89cNkp72gXjpPYs7Nm \\
Theory Prop Id: & 792d7d18b9ffdad302a08ed667c940da3d4f02f0bfbaf07fef81aa2961d74531 \\
Theory Prop Address: & TMVjMcbkMeWtsqfqTEQnrRhtUFG4TMoXw5s
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:dfjgoghg}
$\mname{Sing}$ is the opaque object of type ${{\iota}\unicdbdjdcd{\iota}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & bd01a809e97149be7e091bf7cbb44e0c2084c018911c24e159f585455d8e6bd0 \\
Pure Object Address: & TMRoFJh3XPuDqcMDh3fauvfQL55yG4ZW8xi \\
Theory Object Id: & b7dfc1c317fc5a717f457d8782ced05f886230b550688a8ad8b1a60364455741 \\
Theory Object Address: & TMYwdTEJpbYhdjjsshw7LP6uC2s7dSrhjMJ
\end{tabular}
\end{center}

\end{definition}
{\bf{Notation.}} We write $\{x\}$ for $\mname{Sing}~x$.

\begin{verbatim}
SingI
\end{verbatim}
\begin{theorem}\label{thm:dfjgoghgje} ${\unicdcdadad x : {\iota} .  {{x} \in {\{{x}\}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 6591bd63306a8b20a34c3c62753b21a3972cf8174ef23e9454980a5b6b82618d \\
Pure Prop Address: & TMWZhsiyoAnszzrXM7jCkxtmgh4ETFtiEfk \\
Theory Prop Id: & 2f93be9a22d244304c3bc2f3253e0b4a512c5f66bb0f005cb881e61f6eb26071 \\
Theory Prop Address: & TMbi5x8pysc7XDzhg16jDTJ4KrkuJzZS7BK
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
SingE
\end{verbatim}
\begin{theorem}\label{thm:dfjgoghgfe} ${\unicdcdadad x y : {\iota} .  {{{y} \in {\{{x}\}}}\unicdbdjdcd{{y}={x}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 9341fe885f477660bd3dfc0b46ef487b4623351d45911bddb267d44cdf6d0821 \\
Pure Prop Address: & TMNoMEGQFgAVj7maHozhYTCSXBfUaNXtuAN \\
Theory Prop Id: & 3b0dd829f31946c18010e2f35a58c321cf20e3464f3c10d63efcab64a4f018fb \\
Theory Prop Address: & TMGwutpkdmmtAbHgjLsWPgK3gW6vqLx2s43
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:cgjgogfhogjgpgog}
$\mname{binunion}$ is the opaque object of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 5e1ac4ac93257583d0e9e17d6d048ff7c0d6ccc1a69875b2a505a2d4da305784 \\
Pure Object Address: & TMKadjsG1yH8Ra5dXxSA9jstbEvqFo88bxo \\
Theory Object Id: & e14989b9e54d0036d328f81b7c2ca9bf3b1c6d7d6dfd5cbc1d8421fd6cc0159e \\
Theory Object Address: & TMWh5oU44xPmpsrB4CwWV2e49m2HBPkrW2D
\end{tabular}
\end{center}

\end{definition}
{\bf{Notation.}} We use $\infkdmfpckd$ as a left associative infix operator  corresponding to applying term ${\mname{binunion}}$.
\begin{verbatim}
binunionI1
\end{verbatim}
\begin{theorem}\label{thm:cgjgogfhogjgpgogjebd} ${\unicdcdadad X Y z : {\iota} .  {{{z} \in {X}}\unicdbdjdcd{{z} \in {{X}\unicdcdcdbg{Y}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 753b6ef046ed0483fcc02f203ffb7e80213207fe9ca6b95995de9c4eaea00411 \\
Pure Prop Address: & TMRRF1KJnf4XF9rqDvQv3UaJJUWLeXK8ZP9 \\
Theory Prop Id: & e43c8db7c2b8d05d548b5a0c56a8d23f40736402d22a35cb8a212ee0ab4be72c \\
Theory Prop Address: & TMMufFv1jkCn3ZdkSG7Y7viPMpw7eZgnmeh
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
binunionI2
\end{verbatim}
\begin{theorem}\label{thm:cgjgogfhogjgpgogjecd} ${\unicdcdadad X Y z : {\iota} .  {{{z} \in {Y}}\unicdbdjdcd{{z} \in {{X}\unicdcdcdbg{Y}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & b8821c633c5f298b2822c44b4eecc8fdef6356f33c6b8bdd93a53e96d7729690 \\
Pure Prop Address: & TMY2zmhR5aQU4DsXTEmDmSgQYhYPh1Py1VW \\
Theory Prop Id: & 959535d02d0caf6be5dc6d781bb10a45795b705bd32a8de6d41ef5ccdca130ce \\
Theory Prop Address: & TMLpWxJ4RXSb2TWfpnMMgvDQbHM1A4XSH9X
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
binunionE
\end{verbatim}
\begin{theorem}\label{thm:cgjgogfhogjgpgogfe} ${\unicdcdadad X Y z : {\iota} .  {{{z} \in {{X}\unicdcdcdbg{Y}}}\unicdbdjdcd{{{z} \in {X}}\unicdcdcdid{{z} \in {Y}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 5a319544d131da120ce102ea37cee203a594453cf4350bac27592a462809271b \\
Pure Prop Address: & TMHtDhNz67RzwWxi6YMkqKVbqx8c9XaiDyX \\
Theory Prop Id: & 1ceeb045243b9d5012dc124e31a841805b4e6059c2e99973ef3d2663b5039471 \\
Theory Prop Address: & TMMe9w3Qz1uA5B6MSbrBAwnM2Ydf6fFAksa
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:dffgehbeegkgpgjgog}
We define $\mname{SetAdjoin}$ to be ${\uniddcgcg X y .  {{X}\unicdcdcdbg{\{{y}\}}}}$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 1f3a09356e470bff37ef2408148f440357b92f92f9a27c828b37d777eb41ddc6 \\
Pure Object Address: & TMXya8p7m5AB5g1dVJ1MSDKpnXtcu2N87Mz \\
Theory Object Id: & 5bdda84d481c907ad5ac9225d0210c23eca52ec933bd26ac51fc7debfa5cd394 \\
Theory Object Address: & TMLYeA5y1CUhy319tM7uM8NUTufJJyM6eya
\end{tabular}
\end{center}

\end{definition}

{\bf{Notation.}} We now write $\{x_1,\ldots,x_n\}$ in general with the following conventions. If $n=0$, the notation means $\mname{Empty}$.
If $n=1$, the notation means $\mname{Sing}~x_1$.
If $n=2$, the notation means $\mname{UPair}~x_1~x_2$.
If $n>2$, then $\mname{SetAdjoin}$ is used to reduce to the case with one fewer elements.

\begin{verbatim}
Power_0_Sing_0
\end{verbatim}
\begin{theorem}\label{thm:afpghhfgchpfadpfdfjgoghgpfad} ${{{\mname{Power}}~{\mname{Empty}}}={\{{\mname{Empty}}\}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 6526a1550f9c7084aa6631fc5bd8b4d8d339fd0ce60e7d548edc293a22206f43 \\
Pure Prop Address: & TMFtrGrnuqpdT6zKi1x2QYqakvTT82UnEGx \\
Theory Prop Id: & a39fd0f7312cd15f6f2e488850e84694dd268ddebb9a0a84a4dec2e6cce4b2e2 \\
Theory Prop Address: & TMZJjQSh37Giw23bdQW2e8z3PhLqdGbYhbC
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Repl_UPair
\end{verbatim}
\begin{theorem}\label{thm:cffgahmgpfffafbgjgch} $${\unicdcdadad F : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad x y : {\iota} .  {{\{{{F}~{z}}|z \in {\{{x},{y}\}}\}}={\{{{F}~{x}},{{F}~{y}}\}}}}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & cacbdd41cb5a9699e9d7e46d5d2d536a174a15a2dad0e76a3885d739f3bf9618 \\
Pure Prop Address: & TMavxam5T7BVKzszyZpmyDGWmzwq22rrVr1 \\
Theory Prop Id: & 412745a32a74658e5f4747ff82265690389455bc948a7dc4ae5ff1cc468be3bd \\
Theory Prop Address: & TMSeQz641QN3jhU5ykuM6QagGpUJisdc52E
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Repl_Sing
\end{verbatim}
\begin{theorem}\label{thm:cffgahmgpfdfjgoghg} ${\unicdcdadad F : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad x : {\iota} .  {{\{{{F}~{z}}|z \in {\{{x}\}}\}}={\{{{F}~{x}}\}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 1b6f04154ad08fd4e5ac8a4a7e0666ebb6990dd65162ddc49c4c2aec615a9338 \\
Pure Prop Address: & TMXmXBaEMHiXuMsDum7NZFR84rqzoKxHCpU \\
Theory Prop Id: & bd9e64fedf4189ba490aa0c11b9fbd79890c422133c09d3193c333247af88b1b \\
Theory Prop Address: & TMV9HYczMJjbDeoJuBm27QfyM9yXxF6FN3Y
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Repl_restr
\end{verbatim}
\begin{theorem}\label{thm:cffgahmgpfchfgdhehch} ${\unicdcdadad X : {\iota} .  {\unicdcdadad F G : {{\iota}\unicdbdjdcd{\iota}} .  {{({\unicdcdadad x : {\iota} .  {{{x} \in {X}}\unicdbdjdcd{{{F}~{x}}={{G}~{x}}}}})}\unicdbdjdcd{{\{{{F}~{x}}|x \in {X}\}}={\{{{G}~{x}}|x \in {X}\}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 81eb906670f9d334d181dc7e4b9de214b26ca6dcc378c218bba5f27088c69e41 \\
Pure Prop Address: & TMNrQK5e5dPgQCprQNuNJ3RRcsb98VaqbXM \\
Theory Prop Id: & 7818462d4aac5c1290215c65d85d4a4cae2160757b04afdf041748738daa94de \\
Theory Prop Address: & TMHUULG8EX1BGFc9jYacJPvM5JWuzmqSJoh
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:ggbgngfhogjgpgog}
$\mname{famunion}$ is the opaque object of type ${{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{\iota}})}\unicdbdjdcd{\iota}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & b3e3bf86a58af5d468d398d3acad61ccc50261f43c856a68f8594967a06ec07a \\
Pure Object Address: & TMWQ76Uj1RnGeogmDxhYaxbaaPGB1LBoCiP \\
Theory Object Id: & 241349d21f55f878b9cd5590cf66f9dc362c98552772a88eccdedc7910500fd0 \\
Theory Object Address: & TMaTpVSSy7hrg8WXTVmsiohBmjmfrDfMMJG
\end{tabular}
\end{center}

\end{definition}

{\bf{Notation.}} We use $\bindmfpcpf_{x\in -} . -$ as a binder notation corresponding to a term constructed using ${\mname{famunion}}$.
\begin{verbatim}
famunionI
\end{verbatim}
\begin{theorem}\label{thm:ggbgngfhogjgpgogje} ${\unicdcdadad X : {\iota} .  {\unicdcdadad F : {({{\iota}\unicdbdjdcd{\iota}})} .  {\unicdcdadad x y : {\iota} .  {{{x} \in {X}}\unicdbdjdcd{{{y} \in {{F}~{x}}}\unicdbdjdcd{{y} \in {\unicdcddedd _{x \in {X}}{{F}~{x}}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0c23d0ec3aeca92359022d4236f139bbce8322597bc7aa615dfd5957df202628 \\
Pure Prop Address: & TMc9t7j1HpKhoSwH9rdLbnytztKsuCGA1n3 \\
Theory Prop Id: & e4f490a807c7166931ad2baca93cfaa01c42669f58e0e3fa9d5a4e910da403f1 \\
Theory Prop Address: & TMSPh7dPrn6WaLbJUMvCgyCRAXKpqw7tSxW
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
famunionE
\end{verbatim}
\begin{theorem}\label{thm:ggbgngfhogjgpgogfe} ${\unicdcdadad X : {\iota} .  {\unicdcdadad F : {({{\iota}\unicdbdjdcd{\iota}})} .  {\unicdcdadad y : {\iota} .  {{{y} \in {({\unicdcddedd _{x \in {X}}{{F}~{x}}})}}\unicdbdjdcd{\unicdcdaddd x \in {X} .  {{y} \in {{F}~{x}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 48683a19e0b9cac431e35763caf26ab25d3b68d0eec6fb8193bb111ac8d2a57a \\
Pure Prop Address: & TMS1BrnhPG5Rb3BqURjxG5UF4FXEg1CWJ6h \\
Theory Prop Id: & ede6e5d506bad2c8dd1acc9526f74416f2e8ed084472c376ae92dd12e47b1b36 \\
Theory Prop Address: & TMN9kEqZptjbB8TVx3pwjNpZJsSZxFeje71
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
famunionE_impred
\end{verbatim}
\begin{theorem}\label{thm:ggbgngfhogjgpgogfepfjgngahchfgeg} $${\unicdcdadad X : {\iota} .  {\unicdcdadad F : {({{\iota}\unicdbdjdcd{\iota}})} .  {\unicdcdadad y : {\iota} .  {{{y} \in {({\unicdcddedd _{x \in {X}}{{F}~{x}}})}}\unicdbdjdcd{\unicdcdadad p : {o} .  {{({\unicdcdadad x .  {{{x} \in {X}}\unicdbdjdcd{{{y} \in {{F}~{x}}}\unicdbdjdcd{p}}}})}\unicdbdjdcd{p}}}}}}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & ab22661d1f7c130e5684c80d6642dea2ccbe8caea270129cb32e218a75dc3b14 \\
Pure Prop Address: & TMM2k1dfrqcpKhy5sotaNPvjvVMC2zbAF94 \\
Theory Prop Id: & 562023a05cb52f7958f9f74add2503404a86b5d121085bea792c6ae40d578143 \\
Theory Prop Address: & TMbvpfPvzznj6iG7UVhksbQDUQpsJeGR69p
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
UnionEq_famunionId
\end{verbatim}
\begin{theorem}\label{thm:ffogjgpgogfebhpfggbgngfhogjgpgogjeeg} ${\unicdcdadad X : {\iota} .  {{{\mname{Union}}~{X}}={\unicdcddedd _{x \in {X}}{x}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & c0407ac29149de6b96007edfd11708f9cad613bf44851fb9a688ec0b72823abc \\
Pure Prop Address: & TMJq16zmpETvRMnCrNiWd4hPxiCF9wLQGvM \\
Theory Prop Id: & 5b5383939b1feed9224b810975652ed8da9eef8545e5df1b9311c75e151ca976 \\
Theory Prop Address: & TMazYyBoEesPvNn5L5cyG4oKnoYJWf1MTXS
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
ReplEq_famunion_Sing
\end{verbatim}
\begin{theorem}\label{thm:cffgahmgfebhpfggbgngfhogjgpgogpfdfjgoghg} ${\unicdcdadad X : {\iota} .  {\unicdcdadad F : {({{\iota}\unicdbdjdcd{\iota}})} .  {{\{{{F}~{x}}|x \in {X}\}}={\unicdcddedd _{x \in {X}}{\{{{F}~{x}}\}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & dfa22e97a0f977492075ad87b7ec5f1e874e8cc726cad73016122eff2e495382 \\
Pure Prop Address: & TMcpQ6xMXyb8neoFWcHWRhPuHkeDjU7r5Sc \\
Theory Prop Id: & 9829d1ccabddee314bee7238491144e99da007ceb90bcc3b1aade28e6bc30824 \\
Theory Prop Address: & TMbPFYZ4Eaf5LC8DmM7MPALZ4kWFxfV1npd
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Power_Sing
\end{verbatim}
\begin{theorem}\label{thm:afpghhfgchpfdfjgoghg} ${\unicdcdadad x : {\iota} .  {{{\mname{Power}}~{\{{x}\}}}={\{{\mname{Empty}},{\{{x}\}}\}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f735ed6a9bad818e002e12cc5ef0819b362cbc929180991433e3e3237282e883 \\
Pure Prop Address: & TMYYws5iekM1u7qxpPo65kGRFcdPoaPVCa9 \\
Theory Prop Id: & e5fb8fe5f5f2baf36fccd9d1f35398ed4a86da3345f90b8e9d2336d609a38a7b \\
Theory Prop Address: & TMYxTSeb1gFn8ZUnNyFfjYHJv1cLqspoYGo
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Power_Sing_0
\end{verbatim}
\begin{theorem}\label{thm:afpghhfgchpfdfjgoghgpfad} ${{{\mname{Power}}~{\{{\mname{Empty}}\}}}={\{{\mname{Empty}},{\{{\mname{Empty}}\}}\}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 24373cc848ed23a872ca0879dfdbcf7a451233726845c72b4cfccef56ea08e80 \\
Pure Prop Address: & TMVoMhEC9xC2sTc7tiuSozHc8YaTWHcTdNa \\
Theory Prop Id: & 173fc92aca3f0c56bd3327162bd62d8aa42795423e3bd3a7692afa1bcbead4cc \\
Theory Prop Address: & TMTeCtmtdQ9KwHpHJU1W4m7ytbUgCGJRUV5
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:dffgah}
$\mname{Sep}$ is the opaque object of type ${{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{o}})}\unicdbdjdcd{\iota}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & f336a4ec8d55185095e45a638507748bac5384e04e0c48d008e4f6a9653e9c44 \\
Pure Object Address: & TMUtfXxDDLj9Tk47vMVXxn7X4YsuGxPH9iG \\
Theory Object Id: & 7008ec0ee19d11cc67c5f11635c82852ccb27360b8bd8431676b0c7e03219428 \\
Theory Object Address: & TMU5xEoVJ4JK7LsxiB8DMm5ouqBu3Rgy3CL
\end{tabular}
\end{center}

\end{definition}

{\bf{Notation.}} We write $\{x\in A|varphi\}$ for $\mathsf{Sep}~A~(\lambda x.\varphi)$.

\begin{verbatim}
SepI
\end{verbatim}
\begin{theorem}\label{thm:dffgahje} ${\unicdcdadad X : {\iota} .  {\unicdcdadad P : {({{\iota}\unicdbdjdcd{o}})} .  {\unicdcdadad x : {\iota} .  {{{x} \in {X}}\unicdbdjdcd{{{P}~{x}}\unicdbdjdcd{{x} \in {\{x \in {X}|{{P}~{x}}\}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & ea56bb93dea4f3624b90c68591a17a4b0e370a444cd3e405fd7fcdb52632635b \\
Pure Prop Address: & TMR97AbUhdgTucfxJ7ujRoLGzK6qJ2E1jyn \\
Theory Prop Id: & 147a6ae90a60bb6d7a3135bb216628e19a94a3f9a5fb6e915e96bbbf26d60ba0 \\
Theory Prop Address: & TMUrJfQgr3jYT2UBYmVX9Mv2z2Jgr6upg8L
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
SepE
\end{verbatim}
\begin{theorem}\label{thm:dffgahfe} ${\unicdcdadad X : {\iota} .  {\unicdcdadad P : {({{\iota}\unicdbdjdcd{o}})} .  {\unicdcdadad x : {\iota} .  {{{x} \in {\{x \in {X}|{{P}~{x}}\}}}\unicdbdjdcd{{{x} \in {X}}\unicdcdcdhd{{P}~{x}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 102830994311842627e3ed866fe29eb1f07e8f9431d5cb028658a623df943412 \\
Pure Prop Address: & TMGr4JhwYm65vLL1JdgtV7Z4udWfVUCyR7C \\
Theory Prop Id: & 00899a751488a4862ed01d1ae8f2ff0dbfbfe3fe46a1349c813bec079a6f9ede \\
Theory Prop Address: & TMSaSd5PfDFDpCcrVNF6RUq6GkDHu9ks3pQ
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
SepE1
\end{verbatim}
\begin{theorem}\label{thm:dffgahfebd} ${\unicdcdadad X : {\iota} .  {\unicdcdadad P : {({{\iota}\unicdbdjdcd{o}})} .  {\unicdcdadad x : {\iota} .  {{{x} \in {\{x \in {X}|{{P}~{x}}\}}}\unicdbdjdcd{{x} \in {X}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d83445946f710ccd1847efc45d29fcc99bebd491806d37ec544f5350bcfa0f86 \\
Pure Prop Address: & TMWSj1Q1gssEN1FRYzrkAPVjkpNyJhfDv8F \\
Theory Prop Id: & 6399b0a98035d8a70e8306896b0f872730b3288dcdbb66b851b1f84cc75089c8 \\
Theory Prop Address: & TMSjwkTcc2asZAUTrPPnJyXprfdL48BnKdS
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
SepE2
\end{verbatim}
\begin{theorem}\label{thm:dffgahfecd} ${\unicdcdadad X : {\iota} .  {\unicdcdadad P : {({{\iota}\unicdbdjdcd{o}})} .  {\unicdcdadad x : {\iota} .  {{{x} \in {\{x \in {X}|{{P}~{x}}\}}}\unicdbdjdcd{{P}~{x}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & aa61ca17580417f6d32cdf9fba918e207307848ff899382c5acbd1e2027eebd5 \\
Pure Prop Address: & TMV6AB23w8THH3JMfPMPg1fJahEHtfBWk9A \\
Theory Prop Id: & 104227af0e258de974a06dacd30d9996af2cc290588f50a9c669aaf9868024f6 \\
Theory Prop Address: & TMUZTejdmRUG8mdTCdynTZZpHdZx8LNmpbi
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Sep_Subq
\end{verbatim}
\begin{theorem}\label{thm:dffgahpfdffhcgbh} ${\unicdcdadad X : {\iota} .  {\unicdcdadad P : {{\iota}\unicdbdjdcd{o}} .  {{\{x \in {X}|{{P}~{x}}\}} \subseteq {X}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 97d0809464d57d8f031c3968a64d1d7a35cc9bf2076517a32bfada2a891489f0 \\
Pure Prop Address: & TMKXby5zNJ4KVAvdU1gcKmDEYMkBvsYGdtv \\
Theory Prop Id: & c17d45b17052435d24c1e2d23e7e0c0589d735640358f24c5893103ac9cd487f \\
Theory Prop Address: & TMYQD6DWoPBDiMim118Sqg7B5nz4JVyqYui
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Sep_In_Power
\end{verbatim}
\begin{theorem}\label{thm:dffgahpfjeogpfafpghhfgch} ${\unicdcdadad X : {\iota} .  {\unicdcdadad P : {{\iota}\unicdbdjdcd{o}} .  {{\{x \in {X}|{{P}~{x}}\}} \in {{\mname{Power}}~{X}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 612c94a6047cff99b0373d060e43552169d05dddccd4ea06be3c8d6a86650764 \\
Pure Prop Address: & TMHfdLZNWAmDjm1ZXXcZtP8QxYVC7ugYRTA \\
Theory Prop Id: & fba53ed8ea5e05c876d2ead08cbb41c2104737958be70e5c48d509f88ed420a6 \\
Theory Prop Address: & TMd59svET4t7PBsSUNEFGENePU74pbhVRyk
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:cffgahmgdffgah}
$\mname{ReplSep}$ is the opaque object of type ${{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{o}})}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{\iota}})}\unicdbdjdcd{\iota}}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & ec807b205da3293041239ff9552e2912636525180ddecb3a2b285b91b53f70d8 \\
Pure Object Address: & TMLdtkt2SAyu6uRx3VwN4EmguAaBBbX15ky \\
Theory Object Id: & 9bdb562173d8d14c707097187f2b9ec994d4d550da69fd27247ea7a1734dc0ea \\
Theory Object Address: & TMRDkBndFptKLHv3ZdFcEM1zsnPucRbrZsD
\end{tabular}
\end{center}

\end{definition}

{\bf{Notation.}} We write $\{s | x\in A, \varphi\}$ for $\mathsf{ReplSep}~A~(\lambda x.\varphi)~(\lambda x.s)$.

\begin{verbatim}
ReplSepI
\end{verbatim}
\begin{theorem}\label{thm:cffgahmgdffgahje} ${\unicdcdadad X : {\iota} .  {\unicdcdadad P : {{\iota}\unicdbdjdcd{o}} .  {\unicdcdadad F : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad x : {\iota} .  {{{x} \in {X}}\unicdbdjdcd{{{P}~{x}}\unicdbdjdcd{{{F}~{x}} \in {\{{{F}~{x}}|x \in {X}, {{P}~{x}}\}}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 35b8ecafee8ec7ce07622bb50b3833b0aab40abc8e7a7253fef934747ce888e9 \\
Pure Prop Address: & TMWGYkRQTsDoJuJbmJZ1z6DVf1M5n7LNCgC \\
Theory Prop Id: & aa7b2b992fe9f4cd5864693019fc63fcdd7e92856cb452371ce4409e421bf1e7 \\
Theory Prop Address: & TMGFrvHwbGaUn5voQsk3ha4eAC8RLvBtTSB
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
ReplSepE
\end{verbatim}
\begin{theorem}\label{thm:cffgahmgdffgahfe}
$${\unicdcdadad X : {\iota} .  {\unicdcdadad P : {{\iota}\unicdbdjdcd{o}} .  {\unicdcdadad F : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad y : {\iota} .  {{{y} \in {\{{{F}~{x}}|x \in {X}, {{P}~{x}}\}}}\unicdbdjdcd{\unicdcdaddd x : {\iota} .  {{{{x} \in {X}}\unicdcdcdhd{{P}~{x}}}\unicdcdcdhd{{y}={{F}~{x}}}}}}}}}}.$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 415ff1723537afd685cb0fed04bae8d9d3e3c9fc8dd81f94e3e5ef00af2fcd62 \\
Pure Prop Address: & TMErPUtuvpjwR2ReNB9nGcmnK8AYV664v6C \\
Theory Prop Id: & b1bc76c44d5f7b7b23a5be6966a678cb5d36886ab4685b00d3d5157e8daf69e3 \\
Theory Prop Address: & TMQMpL9gjiXL2MUteH6hiemmLJG4AhbLTXr
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
ReplSepE_impred
\end{verbatim}
\begin{theorem}\label{thm:cffgahmgdffgahfepfjgngahchfgeg}
$${\unicdcdadad X : {\iota} .  {\unicdcdadad P : {{\iota}\unicdbdjdcd{o}} .  {\unicdcdadad F : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad y : {\iota} .  {{{y} \in {\{{{F}~{x}}|x \in {X}, {{P}~{x}}\}}}\unicdbdjdcd{\unicdcdadad p : {o} .  {{({\unicdcdadad x \in {X} .  {{{P}~{x}}\unicdbdjdcd{{{y}={{F}~{x}}}\unicdbdjdcd{p}}}})}\unicdbdjdcd{p}}}}}}}}.$$
The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 5d26e1469193d5bd2136b195439a688359b4bf58fb7a17905abb3c0cf02e93af \\
Pure Prop Address: & TMMk3dLDDxdwMUP7GQkv6ep261PQbXFJKi5 \\
Theory Prop Id: & 063cead7e54785ba03db6bfc07a0999226785a5ad4252309bcbbf4d94eb92422 \\
Theory Prop Address: & TMM2umBqoRLF5bftij5PkXw6MCfbhi2G26n
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:cffgahmgdffgahcd}
$\mname{ReplSep2}$ is the opaque object of type ${{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{\iota}})}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}})}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}})}\unicdbdjdcd{\iota}}}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & da098a2dd3a59275101fdd49b6d2258642997171eac15c6b60570c638743e785 \\
Pure Object Address: & TMNVwxznYhNZZoYoQL3ESJeSeewae4Z5ubB \\
Theory Object Id: & bd46a4454a608867c1da526c8a8d052f33ebc39c49a21d7e84f4d329218203b0 \\
Theory Object Address: & TMdeKFiZBi4BgUrRypBtmVFrLRWnZ8EbVUP
\end{tabular}
\end{center}

\end{definition}
\begin{verbatim}
ReplSep2I
\end{verbatim}
\begin{theorem}\label{thm:cffgahmgdffgahcdje}
$${\unicdcdadad A .  {\unicdcdadad B : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad P : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  {\unicdcdadad F : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}} .  {\unicdcdadad x \in {A} .  {\unicdcdadad y \in {{B}~{x}} .  {{{{P}~{x}}~{y}}\unicdbdjdcd{{{{F}~{x}}~{y}} \in {{{{{\mname{ReplSep2}}~{A}}~{B}}~{P}}~{F}}}}}}}}}}.$$
The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & c012d962b28e32216b7c116bb9b93b568f22cdbd01c2ad49eb0973e193d89ca5 \\
Pure Prop Address: & TMbDYFXkGgf7ZjkUpxAt2c8KfCPQnzBVHXo \\
Theory Prop Id: & d75c053450bb002a32e5862bcdf41f63858ceb9bca07b0b78edc448c3cd382e5 \\
Theory Prop Address: & TMTZAhgLueBybAHKpFbownqVFw34ydwJv3A
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
ReplSep2E_impred
\end{verbatim}
\begin{theorem}\label{thm:cffgahmgdffgahcdfepfjgngahchfgeg} 
$$
\begin{array}{c}
\unicdcdadad A .  \unicdcdadad B : {{\iota}\unicdbdjdcd{\iota}} .  \unicdcdadad P : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  \unicdcdadad F : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}} .\\  {\unicdcdadad r \in {{{{{\mname{ReplSep2}}~{A}}~{B}}~{P}}~{F}} .  {\unicdcdadad p : {o} .  {{({\unicdcdadad x \in {A} .  {\unicdcdadad y \in {{B}~{x}} .  {{{{P}~{x}}~{y}}\unicdbdjdcd{{{r}={{{F}~{x}}~{y}}}\unicdbdjdcd{p}}}}})}\unicdbdjdcd{p}}}}.
\end{array}
$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 9cf007f5a509413458fb2202520eeadc0e1282d8f5e08ea4e998973e0c49f6eb \\
Pure Prop Address: & TMH6JGjNiuhPqpFuX9oizzHFk5Le2zk5WAH \\
Theory Prop Id: & fc01e896457b69f97929e28b9ca1348b7bec5c0f73942fd10cd6424efd4ff8da \\
Theory Prop Address: & TMP5H56SXZ4FHy2J2NYCGC9QGApNByq6Fuv
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
ReplSep2E
\end{verbatim}
\begin{theorem}\label{thm:cffgahmgdffgahcdfe}
$$
\begin{array}{c}
\unicdcdadad A .  \unicdcdadad B : {{\iota}\unicdbdjdcd{\iota}} .  \unicdcdadad P : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  \unicdcdadad F : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}} .  \unicdcdadad r \in {{{{{\mname{ReplSep2}}~{A}}~{B}}~{P}}~{F}} . \\ {\unicdcdaddd x \in {A} .  {\unicdcdaddd y \in {{B}~{x}} .  {{{{P}~{x}}~{y}}\unicdcdcdhd{{r}={{{F}~{x}}~{y}}}}}}.
\end{array}$$
The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 7c43a59f9be76561c287a01d1503cef13020f9d5467c7fe07a42e5ca37944da3 \\
Pure Prop Address: & TMWPJMkxvgzqUKqtFU66YkSgt15bbJMX2GN \\
Theory Prop Id: & fb571ab298cdb2355f09c7b4be2d8e161ca5df97f2f94f5907375ecfd6c02700 \\
Theory Prop Address: & TMR6JYS9aq1RbPLrzpqs7eQpgMEUJFbekS2
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
binunion_asso
\end{verbatim}
\begin{theorem}\label{thm:cgjgogfhogjgpgogpfbgdhdhpg} ${\unicdcdadad X Y Z : {\iota} .  {{{X}\unicdcdcdbg{({{Y}\unicdcdcdbg{Z}})}}={{({{X}\unicdcdcdbg{Y}})}\unicdcdcdbg{Z}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & e0f701721ae7f584ad335901c46f861f37994ae2c421659e2fc7d24d52c4ad58 \\
Pure Prop Address: & TMSkYkrEs3aZ5sGQH7NK9w6LMvc7ihPrtiY \\
Theory Prop Id: & 61dfbad9a60ca916e2a74941dde462165a35addadb67dd1aa0e14bf13e972036 \\
Theory Prop Address: & TMay4ygEWLRWTtSwLgj2avwuNTtFqy4VPaD
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
binunion_com
\end{verbatim}
\begin{theorem}\label{thm:cgjgogfhogjgpgogpfdgpgng} ${\unicdcdadad X Y : {\iota} .  {{{X}\unicdcdcdbg{Y}}={{Y}\unicdcdcdbg{X}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & e20f4f80912d4279be9396097afd9e80c497a2f339edd6413343e5d23c789f0e \\
Pure Prop Address: & TMaLPUJawPt39v249vAR1DqP1n84oA3fd8g \\
Theory Prop Id: & bed33ed76997bd9546985ac652f8933bf140216a164aa11462375a79b95e7a08 \\
Theory Prop Address: & TMY4TyspYtVRBA6PfYNL89qxpZvncatAvsk
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
binunion_idl
\end{verbatim}
\begin{theorem}\label{thm:cgjgogfhogjgpgogpfjgegmg} ${\unicdcdadad X : {\iota} .  {{{\mname{Empty}}\unicdcdcdbg{X}}={X}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 8dc61661d4d5e1f88a3162d142c0a3e25f64eacc329dfd0068a1dc72be818a05 \\
Pure Prop Address: & TMHvo75eYy3DzHQyXDhy7nSXmaRpD1QL8Xv \\
Theory Prop Id: & 52cd24837ea762ce63b82815496f8b7cf911a666c277332e8ecf1679702408c2 \\
Theory Prop Address: & TMM6roc6rAT3Nk8tdS3jEzf3rjCYtEtKppo
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
binunion_idr
\end{verbatim}
\begin{theorem}\label{thm:cgjgogfhogjgpgogpfjgegch} ${\unicdcdadad X : {\iota} .  {{{X}\unicdcdcdbg{\mname{Empty}}}={X}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 67e82fb8d1d026e5488f27f866055b8ad7b6ae3107546e436d50455676cb7db6 \\
Pure Prop Address: & TMYUCbeWsYbEVYGjC69S1voGpXmnhiyPS1j \\
Theory Prop Id: & d5a0059cf51bb85c8614882cfb5aa46e5986047c17f59943f59e9afdca587577 \\
Theory Prop Address: & TMK8JAPKwtcTnWyvdtnBF1r93mW75pcUzMM
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
binunion_idem
\end{verbatim}
\begin{theorem}\label{thm:cgjgogfhogjgpgogpfjgegfgng} ${\unicdcdadad X : {\iota} .  {{{X}\unicdcdcdbg{X}}={X}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 810a82013ba606cd5918b3f6b58976e1a987615eaad568a3e32930a3239a3e37 \\
Pure Prop Address: & TMbQmiBEMSBKRMaesDwRUx5iHKc86Jpvahe \\
Theory Prop Id: & 10e6968d996355460bf1486862c7a957c7b64f3eaa21e7c5530de09d0acc76bd \\
Theory Prop Address: & TMRyZSEzQ6SeCXSBXN2HWBcfU7GgBsUCzp7
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
binunion_Subq_1
\end{verbatim}
\begin{theorem}\label{thm:cgjgogfhogjgpgogpfdffhcgbhpfbd} ${\unicdcdadad X Y : {\iota} .  {{X} \subseteq {{X}\unicdcdcdbg{Y}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & b2c65821a8c09a0b77af768d4af071f6f52e54e3ab9f874132e22d9b780fec03 \\
Pure Prop Address: & TMNMiyzoBmmTgby8dHSUT9GNJXBRATKB1Je \\
Theory Prop Id: & a9b3a8f498f868b3e5f0ad0bf8f135aeabf5748b92ad79003393964533a788f6 \\
Theory Prop Address: & TMKuARFTAuYGC1dr9qRt4msXcsg294CE5fx
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
binunion_Subq_2
\end{verbatim}
\begin{theorem}\label{thm:cgjgogfhogjgpgogpfdffhcgbhpfcd} ${\unicdcdadad X Y : {\iota} .  {{Y} \subseteq {{X}\unicdcdcdbg{Y}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 3cf2292964400c071542529f75f809fb1cccc1b48658e084626f9f60981211a2 \\
Pure Prop Address: & TMWp6qtFQ6sNjLamnX9ZFCwWRY29tAeEj4n \\
Theory Prop Id: & 1507ce49772284307aa14b5f6312cbe2050013469059484c4e6af749d27296c7 \\
Theory Prop Address: & TMHECM3VikFfrZ52FBVEeJcMZtdHizHKgfk
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
binunion_Subq_min
\end{verbatim}
\begin{theorem}\label{thm:cgjgogfhogjgpgogpfdffhcgbhpfngjgog} ${\unicdcdadad X Y Z : {\iota} .  {{{X} \subseteq {Z}}\unicdbdjdcd{{{Y} \subseteq {Z}}\unicdbdjdcd{{{X}\unicdcdcdbg{Y}} \subseteq {Z}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & cc32a5be9e847d0d6b3321ae657ec25e33e4efa0fa1a8b187388477416c1b8a3 \\
Pure Prop Address: & TMZ3UZw7snyBWjGXoD2PLSgQ7Z2tViLeZHE \\
Theory Prop Id: & d64da44c02293ec947fdce4b6a1334307011456947961dce8950499be075b837 \\
Theory Prop Address: & TMEmr475JNDN72vef9HbrMFEnw3HeFp8ckR
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Subq_binunion_eq
\end{verbatim}
\begin{theorem}\label{thm:dffhcgbhpfcgjgogfhogjgpgogpffgbh} ${\unicdcdadad X Y .  {{({{X} \subseteq {Y}})}={({{{X}\unicdcdcdbg{Y}}={Y}})}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f8ee53d9e4447bc52c14da3fcc90d5e8615f20617571fe5255ea2f6eb381e06d \\
Pure Prop Address: & TMbuiip99HVRqBDM9hnt3UzPZe6NvLXEw43 \\
Theory Prop Id: & c2d39365f127c2c7b045442887fe24ea64a512918a28eaa5c725c8592f45e775 \\
Theory Prop Address: & TMZAQ7e8J964d8E63qrdsixRgixW7twAP2T
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
binunion_nIn_I
\end{verbatim}
\begin{theorem}\label{thm:cgjgogfhogjgpgogpfogjeogpfje} ${\unicdcdadad X Y z : {\iota} .  {{{z}\unicdcdadjd{X}}\unicdbdjdcd{{{z}\unicdcdadjd{Y}}\unicdbdjdcd{{z}\unicdcdadjd{{X}\unicdcdcdbg{Y}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a815887d2483bf0106a08715fcac061cae3e6bcbb8e465a668937ec74c34a252 \\
Pure Prop Address: & TMHmep2oeAYUaJwZC3hiCXb2vG3pYtH1QiF \\
Theory Prop Id: & b26c78a45180d7dd20f8b0147d272da614cde185efd40b05c72c389284a5bdfd \\
Theory Prop Address: & TMNdwhoFsncxh4zt41JCJjMiky1UTdLveND
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
binunion_nIn_E
\end{verbatim}
\begin{theorem}\label{thm:cgjgogfhogjgpgogpfogjeogpffe} ${\unicdcdadad X Y z : {\iota} .  {{{z}\unicdcdadjd{{X}\unicdcdcdbg{Y}}}\unicdbdjdcd{{{z}\unicdcdadjd{X}}\unicdcdcdhd{{z}\unicdcdadjd{Y}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & eb90dbeba507f6184d9a4519639032fd25e13e8a5665b55e204384457add4651 \\
Pure Prop Address: & TMLKugoiqVxQHU6VmQg13s94YEdBHkpk3c6 \\
Theory Prop Id: & 64c8be6bcd58b6ff3005c6e68cea0923081c0c08b375ed3440f58e2ae4590507 \\
Theory Prop Address: & TMMzSapwNEj6zYnr4sqrPXz964RVJfZhXvJ
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:cgjgogjgogehfgchdhfgdgeh}
$\mname{binintersect}$ is the opaque object of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & b2abd2e5215c0170efe42d2fa0fb8a62cdafe2c8fbd0d37ca14e3497e54ba729 \\
Pure Object Address: & TMLEtM84AAELgYDKCd7u4BvMP8XhNj6rBEU \\
Theory Object Id: & 2c68d89742466253865fe4ac454f660dc5ef3aabe295adca6101b1cfe29a9b4b \\
Theory Object Address: & TMTxtnFNepi91FFerdTCcnaeQ6ZJWf8pc76
\end{tabular}
\end{center}

\end{definition}
{\bf{Notation.}} We use $\infkdpcmfkd$ as a left associative infix operator  corresponding to applying term ${\mname{binintersect}}$.
\begin{verbatim}
binintersectI
\end{verbatim}
\begin{theorem}\label{thm:cgjgogjgogehfgchdhfgdgehje} ${\unicdcdadad X Y z .  {{{z} \in {X}}\unicdbdjdcd{{{z} \in {Y}}\unicdbdjdcd{{z} \in {{X}\unicdcdcdjd{Y}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & fd656d06038bf1e8213bf796c99d2730d0934ac5207ea1a324a38e8ffb7f1d72 \\
Pure Prop Address: & TMavDaUgQY4Yc7jvGaUAZLBxvza2KYE7CTa \\
Theory Prop Id: & 9081a09947c1d3d1991f93fd8066a329cc8dd137d5232ac2ec7d204ac6f93e3c \\
Theory Prop Address: & TMW6j5eRPzucAp43ZDsETbD83EUAMzqu3gS
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
binintersectE
\end{verbatim}
\begin{theorem}\label{thm:cgjgogjgogehfgchdhfgdgehfe} ${\unicdcdadad X Y z .  {{{z} \in {{X}\unicdcdcdjd{Y}}}\unicdbdjdcd{{{z} \in {X}}\unicdcdcdhd{{z} \in {Y}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 463b5a7d659e015ae77f37224a2da56f16082db6bae0d607624285937805d0ac \\
Pure Prop Address: & TMGgPwxMGdV2DoStuTEK7hiAAwBA496E6VG \\
Theory Prop Id: & ca06365460a4a4310d69039b45771ed26e9f64b8553c1685d7d26b38bc88fce3 \\
Theory Prop Address: & TMT3UicyLqut6GdZ4E3a5HpLsx7pQRGYv4o
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
binintersectE1
\end{verbatim}
\begin{theorem}\label{thm:cgjgogjgogehfgchdhfgdgehfebd} ${\unicdcdadad X Y z .  {{{z} \in {{X}\unicdcdcdjd{Y}}}\unicdbdjdcd{{z} \in {X}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & b12123fa4efe378e34ca200da469f86ccfc917210d536de59d52c5e9de77116c \\
Pure Prop Address: & TMVXNYZCzRuA7LZtTrfmGXLqpJKtWXchcg3 \\
Theory Prop Id: & 51005ef0a8ef018c9807d92cb93099aee35ab19d9b57fee1f06b6d001123d66e \\
Theory Prop Address: & TMGso6ks75EXfsrAgvoTysUxjJQVJBRAjXQ
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
binintersectE2
\end{verbatim}
\begin{theorem}\label{thm:cgjgogjgogehfgchdhfgdgehfecd} ${\unicdcdadad X Y z .  {{{z} \in {{X}\unicdcdcdjd{Y}}}\unicdbdjdcd{{z} \in {Y}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 39656fd10aea14619f5a39d872360e27a8a2adbf407ac9f383cc565db9601f30 \\
Pure Prop Address: & TMFtaVMiexDH341MBZktuvoMPVCTRcMZ5E6 \\
Theory Prop Id: & 599de44995ff57c083eb2f45a7abd687d47df353ae136fb3a5621a3444c2edaf \\
Theory Prop Address: & TMckjJj9KRQHyQMWWeL4Y7CKxNta6jpAGYB
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
binintersect_Subq_1
\end{verbatim}
\begin{theorem}\label{thm:cgjgogjgogehfgchdhfgdgehpfdffhcgbhpfbd} ${\unicdcdadad X Y : {\iota} .  {{{X}\unicdcdcdjd{Y}} \subseteq {X}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f296ad2186681350539ee33fda247d0b2db3407ef4c9b9878863d410f9f6c174 \\
Pure Prop Address: & TMHYoEPaHzR6jsg5oRyMdnfEQqNRzrVv5fj \\
Theory Prop Id: & 303833566de1cc91ab34cfc55ff0aa1141fcb51e6ffe3026695258fa36b408ef \\
Theory Prop Address: & TMbU54waGS53UwVgzDZ1rm2yMPzD36vBhkj
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
binintersect_Subq_2
\end{verbatim}
\begin{theorem}\label{thm:cgjgogjgogehfgchdhfgdgehpfdffhcgbhpfcd} ${\unicdcdadad X Y : {\iota} .  {{{X}\unicdcdcdjd{Y}} \subseteq {Y}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & fcd5f54826312c964c01eee203b1512d720124e0ee6cda87c6500675af973a10 \\
Pure Prop Address: & TMdHZ7X2QicJLMked82RYwwjaLTcFLaALcQ \\
Theory Prop Id: & 8b9fd275589ddd59b577f6592484143e175ec81d47f79fecbc691c373af53bf6 \\
Theory Prop Address: & TMdhk1ZqZYfFHLHXb5kzMk3FTGGmYXyd6pv
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
binintersect_Subq_eq_1
\end{verbatim}
\begin{theorem}\label{thm:cgjgogjgogehfgchdhfgdgehpfdffhcgbhpffgbhpfbd} ${\unicdcdadad X Y .  {{{X} \subseteq {Y}}\unicdbdjdcd{{{X}\unicdcdcdjd{Y}}={X}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 277eecb6dd017782dd48738677bd8a5982157e4c5cd5cc05918e2124c974cd07 \\
Pure Prop Address: & TMGURzfSeKMD3UYDfmxJ2DFVhggDoZwZnUy \\
Theory Prop Id: & ec1cc3fd8120069fd440f892bb823f090399876a574880710582ba7186a73de5 \\
Theory Prop Address: & TMcUHjKDeFZpkMnMczJ2SUAQuA1B6GVgFMp
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
binintersect_Subq_max
\end{verbatim}
\begin{theorem}\label{thm:cgjgogjgogehfgchdhfgdgehpfdffhcgbhpfngbgih} ${\unicdcdadad X Y Z : {\iota} .  {{{Z} \subseteq {X}}\unicdbdjdcd{{{Z} \subseteq {Y}}\unicdbdjdcd{{Z} \subseteq {{X}\unicdcdcdjd{Y}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 95624ddfbe331265c4ca2f86b896a19a583eb8540109d5bf381eca2fd9c5a2ce \\
Pure Prop Address: & TMZEyDaHk9qJtwS7tYcTVD3TPZbywzpMvLN \\
Theory Prop Id: & 64636bafad5e1f11c7c5b8d776a60352971b7c848370b9d8c312eba0ba7c8a7d \\
Theory Prop Address: & TMYQdf7jp47hrnGmxiraKcX3aZTPo8rVu7B
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
binintersect_asso
\end{verbatim}
\begin{theorem}\label{thm:cgjgogjgogehfgchdhfgdgehpfbgdhdhpg} ${\unicdcdadad X Y Z : {\iota} .  {{{X}\unicdcdcdjd{({{Y}\unicdcdcdjd{Z}})}}={{({{X}\unicdcdcdjd{Y}})}\unicdcdcdjd{Z}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 888f8c948c07fff1208257cfdcb30e80aba97a0ea19895a0ddf3f2a7ccae2cdb \\
Pure Prop Address: & TMSNBUzV3aQxYYeZPY2TT8DCJH4y5uZtPS8 \\
Theory Prop Id: & e32fe808b50d4a7d26feb7c47fba0677ea7248260462759537117a8ded2fb5dc \\
Theory Prop Address: & TMYMBJhEnU2xzWURsT3VUeTKQ6932cZ99sf
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
binintersect_com
\end{verbatim}
\begin{theorem}\label{thm:cgjgogjgogehfgchdhfgdgehpfdgpgng} ${\unicdcdadad X Y : {\iota} .  {{{X}\unicdcdcdjd{Y}}={{Y}\unicdcdcdjd{X}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 1a2c6f83dfc7eef1f0f5d8a6ef71433168e521d79874af4f4612a7cae5c5b035 \\
Pure Prop Address: & TMb2URdQekPfF7sFmwNvzkDv5BMnydvoeSe \\
Theory Prop Id: & ea8a1cf7428c5c48bad97c047bde68748dd123f1e3e2886bb9723b9685f19f52 \\
Theory Prop Address: & TMPHGC6FLeDyJUBBy5raiX5Q2fa4jN5brmt
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
binintersect_annil
\end{verbatim}
\begin{theorem}\label{thm:cgjgogjgogehfgchdhfgdgehpfbgogogjgmg} ${\unicdcdadad X : {\iota} .  {{{\mname{Empty}}\unicdcdcdjd{X}}={\mname{Empty}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 19837ac3a4cc72e88c8423496b51c2617beb1ae51cfbefea7f1962c0b5f50a16 \\
Pure Prop Address: & TMHFgk1LgJ2LLMW8CoCeuxb6mvWZeaznuN8 \\
Theory Prop Id: & 66dfcafe7e8daa11a68daa9116d60646fe5aa8d58830a016d31ad2426013468c \\
Theory Prop Address: & TMUGqogYhT1MpqtsHd9QtihJT2pr5trMXwD
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
binintersect_annir
\end{verbatim}
\begin{theorem}\label{thm:cgjgogjgogehfgchdhfgdgehpfbgogogjgch} ${\unicdcdadad X : {\iota} .  {{{X}\unicdcdcdjd{\mname{Empty}}}={\mname{Empty}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0e7e2f4e6df513f1e6b5ccaea6a1621ebbca518c2b68b695a894a4ce698c4e0c \\
Pure Prop Address: & TMS8kC9HsHPYsso9Ze468n6eVHK6b88et1P \\
Theory Prop Id: & 347af54bba6e5ad1b72402cecf209ec4580f847c599c14715314311d43e1dcef \\
Theory Prop Address: & TMKWuV4D5gCFenDioXWGtrYFYLc52e3UzGG
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
binintersect_idem
\end{verbatim}
\begin{theorem}\label{thm:cgjgogjgogehfgchdhfgdgehpfjgegfgng} ${\unicdcdadad X : {\iota} .  {{{X}\unicdcdcdjd{X}}={X}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & dbddbcb4a8c0a37d70f0630df520746c472b6a1a846e6011ecc825783815db34 \\
Pure Prop Address: & TMHBW8eKU6ryBGgk4HWYuA3dnXogpEKcixW \\
Theory Prop Id: & d2a963ba345439222b37255ea718d0d0044869fef2d1dbf88d33f1c74f8181af \\
Theory Prop Address: & TMVpfMftXnY2WNrX82PsUg6Ffz8dhHZCCbY
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
binintersect_binunion_distr
\end{verbatim}
\begin{theorem}\label{thm:cgjgogjgogehfgchdhfgdgehpfcgjgogfhogjgpgogpfegjgdhehch} ${\unicdcdadad X Y Z : {\iota} .  {{{X}\unicdcdcdjd{({{Y}\unicdcdcdbg{Z}})}}={{{X}\unicdcdcdjd{Y}}\unicdcdcdbg{{X}\unicdcdcdjd{Z}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 36e5834dc2dad9ecc45b407b7436248dd124ef4599aa9404e9c6e2d285fdf8ce \\
Pure Prop Address: & TMJTm4UUo6gbzs6LVeQouXfnfj1XXyMHF1A \\
Theory Prop Id: & 8127d38d4909f520e4a84c6845262a06189700ca1e234d7cbdaf3d2ce716f3ca \\
Theory Prop Address: & TMbjiZjgzVpkQ3KA7NniPjhJJdwASKPh6M6
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
binunion_binintersect_distr
\end{verbatim}
\begin{theorem}\label{thm:cgjgogfhogjgpgogpfcgjgogjgogehfgchdhfgdgehpfegjgdhehch} ${\unicdcdadad X Y Z : {\iota} .  {{{X}\unicdcdcdbg{{Y}\unicdcdcdjd{Z}}}={{({{X}\unicdcdcdbg{Y}})}\unicdcdcdjd{({{X}\unicdcdcdbg{Z}})}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a9a58a72e353790019b05940c85c859102eea0d847382f289d58e8bd468aacc5 \\
Pure Prop Address: & TMUsf49mgzPX91G3rqfz1ovatYjDfYdvK98 \\
Theory Prop Id: & 4a9b047f4f17cdf61b7b7dd40930b1c044fa82525a4c6116a7e11a025b94040f \\
Theory Prop Address: & TMSNTa34aJse1X5BoYYckuaeBfJRNGqKuDG
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Subq_binintersection_eq
\end{verbatim}
\begin{theorem}\label{thm:dffhcgbhpfcgjgogjgogehfgchdhfgdgehjgpgogpffgbh} ${\unicdcdadad X Y : {\iota} .  {{({{X} \subseteq {Y}})}={({{{X}\unicdcdcdjd{Y}}={X}})}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 86d529c3fd349b6b3715efdec80a7ca160419af4d312f017c9b6429831a8b6fa \\
Pure Prop Address: & TMS6VwxbSL2tMcsJ33Gzb3sYguz8uL14aJW \\
Theory Prop Id: & 33cf2fc02a709c5c13da3cccb6bb79ee7947a9d4791092613388daca4cfe3096 \\
Theory Prop Address: & TMM8Sp6PDTpeVhKhLLCUpaWCnnBiqynotsR
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
binintersect_nIn_I1
\end{verbatim}
\begin{theorem}\label{thm:cgjgogjgogehfgchdhfgdgehpfogjeogpfjebd} ${\unicdcdadad X Y z : {\iota} .  {{{z}\unicdcdadjd{X}}\unicdbdjdcd{{z}\unicdcdadjd{{X}\unicdcdcdjd{Y}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 073b4038a060c4b1bde2ede64117c357d3bdce362ac825ec6a720138f563c8c5 \\
Pure Prop Address: & TMVoJYkpJgivDmuJexxTuap5J3uDDg1wMek \\
Theory Prop Id: & 9c3d131fc1d769080781e93eb8ec589b7a2c2d6c60bcbc11c1c14a15a604d93a \\
Theory Prop Address: & TMQojPTSE5pppDmrTox3ZJojc7GqQ5pR8nk
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
binintersect_nIn_I2
\end{verbatim}
\begin{theorem}\label{thm:cgjgogjgogehfgchdhfgdgehpfogjeogpfjecd} ${\unicdcdadad X Y z : {\iota} .  {{{z}\unicdcdadjd{Y}}\unicdbdjdcd{{z}\unicdcdadjd{{X}\unicdcdcdjd{Y}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 4cd97a3920660cc1baab84a02cde2f0752cc800bdbf6948734149b840f916d31 \\
Pure Prop Address: & TMHeuLBfC3AwL6jnzuUSDhrdaQmCoHoj5D3 \\
Theory Prop Id: & 095f40265118c2d28d3547f12e68d5c28ea77112d6ccc6b086c324fc60b2794e \\
Theory Prop Address: & TMMM6TarDYx9DpZCUpsD2z8vW1PAAJQ5vPa
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
binintersect_nIn_E
\end{verbatim}
\begin{theorem}\label{thm:cgjgogjgogehfgchdhfgdgehpfogjeogpffe} ${\unicdcdadad X Y z : {\iota} .  {{{z}\unicdcdadjd{{X}\unicdcdcdjd{Y}}}\unicdbdjdcd{{{z}\unicdcdadjd{X}}\unicdcdcdid{{z}\unicdcdadjd{Y}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f6260f7735d4122a10a80856c4f9049d1519687f57b7b19edb745ee2cf5cfd3e \\
Pure Prop Address: & TMdweHzbtRnrtxQVKunco97o2a12LP8roAQ \\
Theory Prop Id: & 84390c4eb6fdb43452a191bfde74ee0a790cd0285b2a874167fa19e4f893bf40 \\
Theory Prop Address: & TML22Gpy4Bf79Bv1gy1Ndk2iWQUPF7ZTQMZ
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:dhfgehngjgogfhdh}
$\mname{setminus}$ is the opaque object of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & c68e5a1f5f57bc5b6e12b423f8c24b51b48bcc32149a86fc2c30a969a15d8881 \\
Pure Object Address: & TMHxJ13rHG66sG7Z5d8qoQ2Wf71i3cMXRPW \\
Theory Object Id: & 913da1489106a5031ed6923d7aac74c19bb471c7cb6d0b317001452fc6f29b30 \\
Theory Object Address: & TMNfftowRQHpY83NVqg5iVfi5uncZiEp6pF
\end{tabular}
\end{center}

\end{definition}
{\bf{Notation.}} We use $\infkdmfkd$ as an infix operator  corresponding to applying term ${\mname{setminus}}$.
\begin{verbatim}
setminusI
\end{verbatim}
\begin{theorem}\label{thm:dhfgehngjgogfhdhje} ${\unicdcdadad X Y z .  {{({{z} \in {X}})}\unicdbdjdcd{{({{z}\unicdcdadjd{Y}})}\unicdbdjdcd{{z} \in {{X}\unicdcdbdgd{Y}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0feeb8d8a9b7ef65218a930ce4e11ecfc7dbb1545c5ef07add1f4b81afb9c3e5 \\
Pure Prop Address: & TMQPezxvx5iDwGozY2n44p1QSmzLW9c33gh \\
Theory Prop Id: & 80db6afb2b95204c3816c5c17e3193ee6ef8bd580a5c82b1d40de15b0dd67e5c \\
Theory Prop Address: & TMdgvunw2TsmUp4GCmh9xtJANKkfVaELTtY
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
setminusE
\end{verbatim}
\begin{theorem}\label{thm:dhfgehngjgogfhdhfe} ${\unicdcdadad X Y z .  {{({{z} \in {{X}\unicdcdbdgd{Y}}})}\unicdbdjdcd{{{z} \in {X}}\unicdcdcdhd{{z}\unicdcdadjd{Y}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 6774f4f653e1e92356f11506e8157d8abe7dbb9be9e6bcb14db1f0bceab51ef3 \\
Pure Prop Address: & TMXy1QEyBGVDaiEg8aD2Cam9qThxoomLi6f \\
Theory Prop Id: & 71763af047667a6ca6327c62400dccb91551bc8f9f136c9e479e28698216380b \\
Theory Prop Address: & TMdogwAC88ANifD7adTtE8r86D6W3bUPM9S
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
setminusE1
\end{verbatim}
\begin{theorem}\label{thm:dhfgehngjgogfhdhfebd} ${\unicdcdadad X Y z .  {{({{z} \in {{X}\unicdcdbdgd{Y}}})}\unicdbdjdcd{{z} \in {X}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 064bd5d663dc259ca997e99bb2bd4b8152814550c0aa05c43ce0df3746079700 \\
Pure Prop Address: & TMTjEjKNmtdB3PuULs3bKw7WREdMMYnLNNi \\
Theory Prop Id: & d74bafc908140cfff43333693f1863756a00f38b654f98d03ff010b973d027f6 \\
Theory Prop Address: & TMMW2tdJZPbYz3RFp8VEL3uz9UEjkov951Y
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
setminusE2
\end{verbatim}
\begin{theorem}\label{thm:dhfgehngjgogfhdhfecd} ${\unicdcdadad X Y z .  {{({{z} \in {{X}\unicdcdbdgd{Y}}})}\unicdbdjdcd{{z}\unicdcdadjd{Y}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 3e696906861b398caf75e058badb44e8df22002a1dbcebbd1e432ae75ebf73e8 \\
Pure Prop Address: & TMbw77MdhQRu71U2YgwKpdioxpTzvqPeTph \\
Theory Prop Id: & 36b2737dca3d3ac20725828013e922045b7f000d58c5bd39fbdbde5ba29e8f17 \\
Theory Prop Address: & TMK2S85jwBL3f1YkbqgioAc3U9L13yLZ4dq
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
setminus_Subq
\end{verbatim}
\begin{theorem}\label{thm:dhfgehngjgogfhdhpfdffhcgbh} ${\unicdcdadad X Y : {\iota} .  {{{X}\unicdcdbdgd{Y}} \subseteq {X}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 5a497a676d0c43a84c28067a8d230220dfff42d4ecda3069868bd45d6864a3a1 \\
Pure Prop Address: & TMZpkAydiSX6PF3eKuUhdGAjSwYNgM8nANN \\
Theory Prop Id: & 66f982019f8b0f9fb9cede258e617e735d7ee6afe6be70204a016fa60645b2ad \\
Theory Prop Address: & TMXKBY1x4AJNkQvcmzLSA5oKynMfanH8j8g
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
setminus_Subq_contra
\end{verbatim}
\begin{theorem}\label{thm:dhfgehngjgogfhdhpfdffhcgbhpfdgpgogehchbg} ${\unicdcdadad X Y Z : {\iota} .  {{{Z} \subseteq {Y}}\unicdbdjdcd{{{X}\unicdcdbdgd{Y}} \subseteq {{X}\unicdcdbdgd{Z}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & b1f440be52ba3f0081ae25bcbcaeb0ae2996726d1652a9b43221ba081ebb4046 \\
Pure Prop Address: & TML7YKpcn2xkVnB8jzzhMFivx3UtkkeTwEf \\
Theory Prop Id: & 9a06b276a8a3609d482bb051c783d938e2b4332e33f0c788b5b1eaa70620ea52 \\
Theory Prop Address: & TMYGQFvSYDuhgZUsfQwKDf3uo8fipNdRzPL
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
setminus_nIn_I1
\end{verbatim}
\begin{theorem}\label{thm:dhfgehngjgogfhdhpfogjeogpfjebd} ${\unicdcdadad X Y z .  {{{z}\unicdcdadjd{X}}\unicdbdjdcd{{z}\unicdcdadjd{{X}\unicdcdbdgd{Y}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a34d147d253b8631f71a8ad885d6b07b51174f6adb06f33ff18f2e17cc3a05d8 \\
Pure Prop Address: & TMP4Br6DGx2zPHwukCi4NHAb1J6UCTGEUTH \\
Theory Prop Id: & 0cf01b8566a440309bf989695975a3eb8c7b5b2b72839f4c5258a27e06a47268 \\
Theory Prop Address: & TMKc4mWQxd5nPWm3Twn6HUoZZ3TpTLTY6kk
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
setminus_nIn_I2
\end{verbatim}
\begin{theorem}\label{thm:dhfgehngjgogfhdhpfogjeogpfjecd} ${\unicdcdadad X Y z .  {{{z} \in {Y}}\unicdbdjdcd{{z}\unicdcdadjd{{X}\unicdcdbdgd{Y}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & bcb7ba48c815e20d7bee194dfed0cc862dd0e3d301f8c9b1d0280812f816ad6c \\
Pure Prop Address: & TMYK5VS87wrMj21qU9jtK2xRsBEsBv9CAaa \\
Theory Prop Id: & 358a53764f4ed435a531d19ce7ac02af9dfb2c98400d9d931a04c2593b2bee95 \\
Theory Prop Address: & TMRc5nmsKibAuSoPbYJ7nMiCh26fBzFmE26
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
setminus_nIn_E
\end{verbatim}
\begin{theorem}\label{thm:dhfgehngjgogfhdhpfogjeogpffe} ${\unicdcdadad X Y z .  {{{z}\unicdcdadjd{{X}\unicdcdbdgd{Y}}}\unicdbdjdcd{{{z}\unicdcdadjd{X}}\unicdcdcdid{{z} \in {Y}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 9bc7c60b2c9e62f8b2a9af59f911de6c5d68761f4a2fe77a94c69a7d3eaf26e2 \\
Pure Prop Address: & TMW5CoiZXunGqAiTQBjRhmUmvjXoJz3mude \\
Theory Prop Id: & 56f952bfe0bd75d292717ecaa4b14fda05ca0cf14fadaaa475598d568bff0ad2 \\
Theory Prop Address: & TMLi6vhY79EBfSSmntPk9snhH4VNXepc9wJ
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
setminus_selfannih
\end{verbatim}
\begin{theorem}\label{thm:dhfgehngjgogfhdhpfdhfgmgggbgogogjgig} ${\unicdcdadad X : {\iota} .  {{({{X}\unicdcdbdgd{X}})}={\mname{Empty}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d3b191afa78022d380048239a2968a37051b62e5c02fa9ac36ee4db31e1083aa \\
Pure Prop Address: & TManQQz76f8CsK8ZetcsbHQhCjjZe659QGn \\
Theory Prop Id: & 478fe86072ac5772bd0bc55b172cc272698845d92efc4458128557ac479044a8 \\
Theory Prop Address: & TMd6YxJcNSPF58sbPVXKMa7uGjNh2yUe8vf
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
setminus_binintersect
\end{verbatim}
\begin{theorem}\label{thm:dhfgehngjgogfhdhpfcgjgogjgogehfgchdhfgdgeh} ${\unicdcdadad X Y Z : {\iota} .  {{{X}\unicdcdbdgd{{Y}\unicdcdcdjd{Z}}}={{({{X}\unicdcdbdgd{Y}})}\unicdcdcdbg{({{X}\unicdcdbdgd{Z}})}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 2625c6089792c3161e4afb2ac98c688356a04763067fa6803e414d5dcedf8d4f \\
Pure Prop Address: & TMdyYr2Jj41ATEHaGEpR1dQgkGsyZP4FuYL \\
Theory Prop Id: & f764127a273ebffdd46d2090e345b6124d00e4e10a76d5047d199152fb751f21 \\
Theory Prop Address: & TMUUoPBVNSzcS2ijLW9PqkQhqPjPTs1Z7MA
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
setminus_binunion
\end{verbatim}
\begin{theorem}\label{thm:dhfgehngjgogfhdhpfcgjgogfhogjgpgog} ${\unicdcdadad X Y Z : {\iota} .  {{{X}\unicdcdbdgd{{Y}\unicdcdcdbg{Z}}}={{({{X}\unicdcdbdgd{Y}})}\unicdcdbdgd{Z}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0b9317714989035a7cbcbdd8eba497db661ca19eccedc9faeb0ae391b2c8987d \\
Pure Prop Address: & TMFwTVRbH9sP3ic4Jj5K77JHuuDaHidkTTo \\
Theory Prop Id: & 651326888d51f7ae0c489bc08dde18dffd32270d616f68516db81047548f94b9 \\
Theory Prop Address: & TMT4EsAWT7qGdwNHgiPcC19uNg3gnsu5RfF
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
binintersect_setminus
\end{verbatim}
\begin{theorem}\label{thm:cgjgogjgogehfgchdhfgdgehpfdhfgehngjgogfhdh} ${\unicdcdadad X Y Z : {\iota} .  {{{({{X}\unicdcdcdjd{Y}})}\unicdcdbdgd{Z}}={{X}\unicdcdcdjd{({{Y}\unicdcdbdgd{Z}})}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d1bd304c20aac47c64bd3668e5ee0c534b4dbff3de4e7a34ab27ea65f5a5e53e \\
Pure Prop Address: & TMYXNZDQUqfnGsDS2NpMohAoZPUMeuh4Puw \\
Theory Prop Id: & f50067170c57c9d167d2bbce86fb7bba1d5f359a694a3e8d87c42ea80fc8f4a9 \\
Theory Prop Address: & TMXQGHghJkaMcQb53tZ6WfydPdKPLw4Fbx3
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
binunion_setminus
\end{verbatim}
\begin{theorem}\label{thm:cgjgogfhogjgpgogpfdhfgehngjgogfhdh} ${\unicdcdadad X Y Z : {\iota} .  {{{{X}\unicdcdcdbg{Y}}\unicdcdbdgd{Z}}={{({{X}\unicdcdbdgd{Z}})}\unicdcdcdbg{({{Y}\unicdcdbdgd{Z}})}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 99c8981445a26f2a8f3c67db827e6580c563359a4f20df37e41dca73f6393a97 \\
Pure Prop Address: & TMbfg9u25oTvirxRNPHRobxdagcb2y9Y1Ez \\
Theory Prop Id: & 1c1cfdea82cec4035b3de28d39481169301aa46b0d0912a7f83e9228797f5a48 \\
Theory Prop Address: & TMQW2SjLqSWSKT8J2EQPCpxjys4GYkHvDX2
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
setminus_setminus
\end{verbatim}
\begin{theorem}\label{thm:dhfgehngjgogfhdhpfdhfgehngjgogfhdh} ${\unicdcdadad X Y Z : {\iota} .  {{{X}\unicdcdbdgd{({{Y}\unicdcdbdgd{Z}})}}={{({{X}\unicdcdbdgd{Y}})}\unicdcdcdbg{({{X}\unicdcdcdjd{Z}})}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 60e720f6c807ccdae50a934ea56981944603f9d6f18983c678c322715f66a587 \\
Pure Prop Address: & TMLXRcQtVsZ2gokZw2jjxkAgJhArzeWbwhF \\
Theory Prop Id: & cab095f0a1f43e4dc50e5489f05911c74f5fd42b4a8dced8ecea3a53e69f1d71 \\
Theory Prop Address: & TMEiQhFR4FhRQESPDAccJrCE98eg1tzdAEE
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
setminus_annil
\end{verbatim}
\begin{theorem}\label{thm:dhfgehngjgogfhdhpfbgogogjgmg} ${\unicdcdadad X : {\iota} .  {{{\mname{Empty}}\unicdcdbdgd{X}}={\mname{Empty}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & fd99d2feff8bf081dd1e98ac3ced977726230ad5af0c70364ed17032b322e958 \\
Pure Prop Address: & TMPjszawGe4kxyHBsc9D4AVrRBAh4nHf7YB \\
Theory Prop Id: & 3d2f5b9dfe25bba40fc9e8e784f45fff9a4a929712ef764617c8b137da6f2cdb \\
Theory Prop Address: & TMPrnLS8t41sPUjW6B8bNjh2dhMBwTbU9S8
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
setminus_idr
\end{verbatim}
\begin{theorem}\label{thm:dhfgehngjgogfhdhpfjgegch} ${\unicdcdadad X : {\iota} .  {{{X}\unicdcdbdgd{\mname{Empty}}}={X}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 20e1086759c8557ab7f7e06736e90912f8684d26fb4e569f3e23fc4960e2a173 \\
Pure Prop Address: & TMQi4nBawCq2rp7HipQymKHj8UhkFm1gCeM \\
Theory Prop Id: & ebb8ec6864341bd40d215d011ec32f77f22a7bfdb6d5d8332a0487fa1efbbaf9 \\
Theory Prop Address: & TMYkPV9ze3vB5CvjACMPmYU1b8ea1z2jSPg
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
In_irref
\end{verbatim}
\begin{theorem}\label{thm:jeogpfjgchchfggg} ${\unicdcdadad x .  {{x}\unicdcdadjd{x}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 12629a025dcc8a596e030daeffbf6322b3d51631eeebf85bcca0a44b6a7964cd \\
Pure Prop Address: & TMKwkB6s3TXZJG8hL6bLbEGFMysQgpweKpz \\
Theory Prop Id: & 7bfd46e967631be2a9098717487f5ae8f88e2867117fd98cce921a47bed1bdbf \\
Theory Prop Address: & TMZagTqZqCeDpgAoeuYZejsuagxzALpQvWL
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
In_no2cycle
\end{verbatim}
\begin{theorem}\label{thm:jeogpfogpgcddgjhdgmgfg} ${\unicdcdadad x y .  {{{x} \in {y}}\unicdbdjdcd{{{y} \in {x}}\unicdbdjdcd{\mname{False}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 6d0cb3f4b527344ea21bf482f99b38b72d358ba458097b2ed205e1de6bd2c82f \\
Pure Prop Address: & TMcBgknu3MmmLrKct3NGTcziaJv71unmDbY \\
Theory Prop Id: & 344f3082291501cfe856ef475802aea283ae4928899f0eba4e2c3a6556451b82 \\
Theory Prop Address: & TMNd1Mv58X5hcYFChdQ93tpgtHdhyahABAg
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
In_no3cycle
\end{verbatim}
\begin{theorem}\label{thm:jeogpfogpgdddgjhdgmgfg} ${\unicdcdadad x y z .  {{{x} \in {y}}\unicdbdjdcd{{{y} \in {z}}\unicdbdjdcd{{{z} \in {x}}\unicdbdjdcd{\mname{False}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 660f202c6752b9347ac4d5b7b55e28507e6fdf71c23bf56ce2eae287f04ec6f3 \\
Pure Prop Address: & TMQcimvCarrH1MmuAYoNABafQguio3NLZeY \\
Theory Prop Id: & 90080b22e6d3c8f5944bbe4d048a7d9fdffe58eac2e3d918ff8ad0d16d572a8e \\
Theory Prop Address: & TMZPDFZYJchoNx1RFvKeMUbtyTaSeQj9LrH
\end{tabular}
\end{center}

\end{theorem}

