\chapter{Disjoint Unions}

\begin{definition}\label{def:jeogkgbd}
We define $\mname{Inj1}$ to be ${{\mname{In\_rec\_i}}~{({\uniddcgcg X f .  {{\{{0}\}}\unicdcdcdbg{\{{{f}~{x}}|x \in {X}\}}}})}}$ of type ${{\iota}\unicdbdjdcd{\iota}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 8f0026627bca968c807e91fff0fdc318bc60691e5ae497542f92c8e85be9fd7d \\
Pure Object Address: & TMHfHa5vujJQpf428B9wNXuDE5s6mwdPL2X \\
Theory Object Id: & 7736ca8991b680139f61982df3af1ac650f0f26acdc0d8f0eee357ccb025fa14 \\
Theory Object Address: & TMG73kjDALbhSPSDyKjUdTNFaHJFKmvRPR3
\end{tabular}
\end{center}

\end{definition}
\begin{verbatim}
Inj1_eq
\end{verbatim}
\begin{theorem}\label{thm:jeogkgbdpffgbh} ${\unicdcdadad X : {\iota} .  {{{\mname{Inj1}}~{X}}={{\{{0}\}}\unicdcdcdbg{\{{{\mname{Inj1}}~{x}}|x \in {X}\}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 73d189eaaf79f7e70a5868626e8599a06905bffe21fe665a8b1af2a7532ef363 \\
Pure Prop Address: & TMVWdgZGFsyibGkrWpy2DrjXjAj4ZHnCcnv \\
Theory Prop Id: & b804575f2f48fe85cc3e16f46d28aedf5c9e1bd2db40240cdc402976b31678dc \\
Theory Prop Address: & TMc2FdiN6hAsJo3duwEKeNeMQK18PyUEFsh
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Inj1I1
\end{verbatim}
\begin{theorem}\label{thm:jeogkgbdjebd} ${\unicdcdadad X : {\iota} .  {{0} \in {{\mname{Inj1}}~{X}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 3c2cc4eebcc7df71902a867c8e10780084c122974b276dfc2e42b3636fcb7f48 \\
Pure Prop Address: & TMUKupGQMJTgBLEF8gUr11TxXdBgWPczFDF \\
Theory Prop Id: & 4ccac3180e2819292f9b0007f9583007576538ef5094469c5b9112c6324d5ae5 \\
Theory Prop Address: & TMFoqv2T2HTXaw58WBHGfN3Yg1LLmHDXTZY
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Inj1I2
\end{verbatim}
\begin{theorem}\label{thm:jeogkgbdjecd} ${\unicdcdadad X x : {\iota} .  {{{x} \in {X}}\unicdbdjdcd{{{\mname{Inj1}}~{x}} \in {{\mname{Inj1}}~{X}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & b6f23b38b854e4764eb026a61fb5de29c88c81746a47fcf866ef0b179e8cceb7 \\
Pure Prop Address: & TMZjKduCZEmbUN9ZBjsaBnKgkfw7LN2UDHT \\
Theory Prop Id: & 086475da641652d7d705bb3a628b3be4360161ede19a126c9e4a25189e1af347 \\
Theory Prop Address: & TMcYPGZrNfjZ1uwVn5pPjvCKQnbnj8Fb9jY
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Inj1E
\end{verbatim}
\begin{theorem}\label{thm:jeogkgbdfe} ${\unicdcdadad X y : {\iota} .  {{{y} \in {{\mname{Inj1}}~{X}}}\unicdbdjdcd{{{y}={0}}\unicdcdcdid{\unicdcdaddd x \in {X} .  {{y}={{\mname{Inj1}}~{x}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d4177b1a2defe4e7a1dc9a2f0cdd24121f05df2353248c4fbce54a7813e386aa \\
Pure Prop Address: & TMRaNkUGFqMNGWjPSkyqhVQ1u7CuZYnE44m \\
Theory Prop Id: & 259217a7917e6f724d1d01957b59b045b53d464a75ffd225751fab998674d1eb \\
Theory Prop Address: & TMKgb5K1zBg9yUsASeSHAXS5dXzMAp6g4mC
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Inj1NE1
\end{verbatim}
\begin{theorem}\label{thm:jeogkgbdoefebd} ${\unicdcdadad x : {\iota} .  {{{\mname{Inj1}}~{x}}\unicdcdgdad{0}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 5e3197f060ee011e661df22a9f6fa83fd21ce6975b1e8fffe8bf822020036e6e \\
Pure Prop Address: & TMZWFtRyxiZnniPvM2zyYdwdjemD8ju9G9q \\
Theory Prop Id: & 09bd10c733e446cd49301e4db4b5b278f8d986e3543f97f02967ca0c21b264ad \\
Theory Prop Address: & TMSEKm63FLbyd37zrxFC3ESBmnwSacXbajE
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Inj1NE2
\end{verbatim}
\begin{theorem}\label{thm:jeogkgbdoefecd} ${\unicdcdadad x : {\iota} .  {{{\mname{Inj1}}~{x}}\unicdcdadjd{\{{0}\}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 9e94b180d7b2cb52448d59e85f15103666357701440f2f18d5af02589fcb09ff \\
Pure Prop Address: & TMaoFDrWfevDLaLmviNwM8qU5VfCbfQNyxm \\
Theory Prop Id: & 3c4dd0ee065b1e59cfafc01a250811bc2c5b00c5d2b523db2b6fb82b36158b54 \\
Theory Prop Address: & TMdfQzzFY8EHNJ3UScdjLaKoU7T5kaYk9Gg
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:jeogkgad}
We define $\mname{Inj0}$ to be ${\uniddcgcg X .  {\{{{\mname{Inj1}}~{x}}|x \in {X}\}}}$ of type ${{\iota}\unicdbdjdcd{\iota}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 8143218ffde429ff34b20ee5c938914c75e40d59cd52cc5db4114971d231ca73 \\
Pure Object Address: & TMNyr2ri5LN86eqRzW8u1M6rvw78xBZoUjT \\
Theory Object Id: & 7d54bea1f00d9595006e5596af5681c32a7d5291e967d47e9c1f618685b8067e \\
Theory Object Address: & TMM4pcVYzZz9VCeFoN6ah22KyBbZKKNTDAc
\end{tabular}
\end{center}

\end{definition}
\begin{verbatim}
Inj0I
\end{verbatim}
\begin{theorem}\label{thm:jeogkgadje} ${\unicdcdadad X x : {\iota} .  {{{x} \in {X}}\unicdbdjdcd{{{\mname{Inj1}}~{x}} \in {{\mname{Inj0}}~{X}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 7fc2e938ecb986314c840c9ebc715b8faa04b3a118675b2f97af4d5a6475aa9f \\
Pure Prop Address: & TMPfdYfdnemz7bK4pdryqUiJ88tNURoednk \\
Theory Prop Id: & 5653780aa993662d9f130c83c987c41047896e81076539a071e059bef75c3a85 \\
Theory Prop Address: & TMWQMDFSDmKyL2MMoQEMXjXRGQkvWtCHUuQ
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Inj0E
\end{verbatim}
\begin{theorem}\label{thm:jeogkgadfe} ${\unicdcdadad X y : {\iota} .  {{{y} \in {{\mname{Inj0}}~{X}}}\unicdbdjdcd{\unicdcdaddd x : {\iota} .  {{{x} \in {X}}\unicdcdcdhd{{y}={{\mname{Inj1}}~{x}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 41668460a96da96670eda3373b14c44145fecc8b7543d1eb48cc87d1a03b5873 \\
Pure Prop Address: & TMR3n3H2ExAyH57HwSFYymEuxUDc7FLsyoo \\
Theory Prop Id: & 855213768c213323d014713167da61d832ba2c1f0e4bac38154d846f4887467d \\
Theory Prop Address: & TMGnC4VJWDhLev8VPHUK3NMMFBEpWB7UKzh
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:ffogkg}
We define $\mname{Unj}$ to be ${{\mname{In\_rec\_i}}~{({\uniddcgcg X f .  {\{{{f}~{x}}|x \in {{X}\unicdcdbdgd{\{{0}\}}}\}}})}}$ of type ${{\iota}\unicdbdjdcd{\iota}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & f202c1f30355001f3665c854acb4fdae117f5ac555d2616236548c8309e59026 \\
Pure Object Address: & TMWjsgx6D3647vX6CZ7FACDq76sirVgNudL \\
Theory Object Id: & 2e16753b23b9f054a644cd2c352a33cf3885b3e69791a426da64d5a3ff83d6ee \\
Theory Object Address: & TMUQznLHs487u6czgXR1tuqBrKovEsSFuwB
\end{tabular}
\end{center}

\end{definition}
\begin{verbatim}
Unj_eq
\end{verbatim}
\begin{theorem}\label{thm:ffogkgpffgbh} ${\unicdcdadad X : {\iota} .  {{{\mname{Unj}}~{X}}={\{{{\mname{Unj}}~{x}}|x \in {{X}\unicdcdbdgd{\{{0}\}}}\}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 3b1aa65e273ab9e8836c2bc74542816dbc66db6da358e79281baa68c1eac4c51 \\
Pure Prop Address: & TMUzG5DSxEUo14WoVVEZHRUadq2y9fEMq9D \\
Theory Prop Id: & b4c8525077a8bd9a2f4b5fe9b1db873fe4209bd38a98f300f580351d5d18d7d3 \\
Theory Prop Address: & TMLCXNWg3jeqjg6spuSQMWMiiuoNrDLSqsX
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Unj_Inj1_eq
\end{verbatim}
\begin{theorem}\label{thm:ffogkgpfjeogkgbdpffgbh} ${\unicdcdadad X : {\iota} .  {{{\mname{Unj}}~{({{\mname{Inj1}}~{X}})}}={X}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & e2cdfc6f275aeef110524d267044d56c4438d2db1293e2867fb46d60760a0f45 \\
Pure Prop Address: & TMRKw89oG3aDYwZKbJ2YCSPZoxR6oQrXVAM \\
Theory Prop Id: & ae00e1714271d7aa2be5da6b28ba3d58bf1dcb1e86e45bd075db78fb8e268271 \\
Theory Prop Address: & TMMx1iggqKMgEC5fpswYPb7SMn6mXdV3Gd6
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Inj1_inj
\end{verbatim}
\begin{theorem}\label{thm:jeogkgbdpfjgogkg} ${\unicdcdadad X Y : {\iota} .  {{{{\mname{Inj1}}~{X}}={{\mname{Inj1}}~{Y}}}\unicdbdjdcd{{X}={Y}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & ce8b6635f1785f75c7b5b16d1f61111f3895e4072cc06a71b7f2548024ab9fcb \\
Pure Prop Address: & TMPRTGLAeftK68qCgSftNHQAt5ZoPyRmGsh \\
Theory Prop Id: & 3e918a17810ff35edf26ed66220d1d7a2ce50e44383669fb3e82f49186cdee06 \\
Theory Prop Address: & TMaXPPDHYrLmw3vrDF8cSrSzcALUJ1fr2vQ
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Unj_Inj0_eq
\end{verbatim}
\begin{theorem}\label{thm:ffogkgpfjeogkgadpffgbh} ${\unicdcdadad X : {\iota} .  {{{\mname{Unj}}~{({{\mname{Inj0}}~{X}})}}={X}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f3e39c79aeba9f53d5600670c3217bc096389fccc95b8a119918ee61bbd2ba1f \\
Pure Prop Address: & TMZUKGCMAbV3pSZqA94UEu6kCWXx8F95cVU \\
Theory Prop Id: & 3808ad5876773f87048df2f1763c5b4749fa9feb633aabecd3c5bc64e8bea8ba \\
Theory Prop Address: & TMWJtkfszm1k5JmP9LnmZB5GUL6tyPJE95H
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Inj0_inj
\end{verbatim}
\begin{theorem}\label{thm:jeogkgadpfjgogkg} ${\unicdcdadad X Y : {\iota} .  {{{{\mname{Inj0}}~{X}}={{\mname{Inj0}}~{Y}}}\unicdbdjdcd{{X}={Y}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 662f53ab21221e41310d9ac6c9389a4c91b5f8a8c92bc0e7c16500877a0ee8d3 \\
Pure Prop Address: & TMc3veqimj5NLmacT7fJhju75JwAWeR5tRC \\
Theory Prop Id: & 29f9450d88499de2d9169079cdcb356767832e57ed9a0111ca120c9eb731b8d1 \\
Theory Prop Address: & TMV8xsSpddijAdXaoJ58C6Ds3FGDXzmngXz
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Inj0_0
\end{verbatim}
\begin{theorem}\label{thm:jeogkgadpfad} ${{{\mname{Inj0}}~{0}}={0}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 171f471b1ee40b5e9e23d33ae47d474ea49798216a6286e99f7505fd596e0b1d \\
Pure Prop Address: & TML5YcJHULJ6j353CwJ1qM8742qPffm73wi \\
Theory Prop Id: & 57f5af3069e244db75ffa5bfd8014bb81b0c95ace6e267ef286f6f4f11003544 \\
Theory Prop Address: & TMbQhddJBnbci3edhLUCUA3LAWeGzxZF6vQ
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Inj0_Inj1_neq
\end{verbatim}
\begin{theorem}\label{thm:jeogkgadpfjeogkgbdpfogfgbh} ${\unicdcdadad X Y : {\iota} .  {{{\mname{Inj0}}~{X}}\unicdcdgdad{{\mname{Inj1}}~{Y}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 21bb03ac63365d37ed4ef00915506a97c5a5b79e468a1019f8db539f0520ead3 \\
Pure Prop Address: & TMNaUd4a4oqrV7GxRGw17zvy3w3U9tCHd4W \\
Theory Prop Id: & 2b14d886759a5ff3af07d29a955feeeebe2511955316846bdd6b6a0516947b7e \\
Theory Prop Address: & TMNgqTkR1PJCufRmpkGQmktjoL6ruuRLg22
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:dhfgehdhfhng}
We define $\mname{setsum}$ to be ${\uniddcgcg X Y .  {{\{{{\mname{Inj0}}~{x}}|x \in {X}\}}\unicdcdcdbg{\{{{\mname{Inj1}}~{y}}|y \in {Y}\}}}}$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & afe37e3e9df1ab0b3a1c5daa589ec6a68c18bf14b3d81364ac41e1812672537a \\
Pure Object Address: & TMLfysEtzMCWeSWegZfR794mvNom3FuyKrm \\
Theory Object Id: & 5b7e09a6e30fb5cf9e9ae6e183db0d299ed352490f06c4381c56c42c8e75cced \\
Theory Object Address: & TMctw4uoy129ZSr7Njfx1xj2Bd38ipPNaKu
\end{tabular}
\end{center}

\end{definition}
{\bf{Notation.}} We use $\infkdlckd$ as a left associative infix operator  corresponding to applying term ${\mname{setsum}}$.
\begin{verbatim}
Inj0_setsum
\end{verbatim}
\begin{theorem}\label{thm:jeogkgadpfdhfgehdhfhng} ${\unicdcdadad X Y x : {\iota} .  {{{x} \in {X}}\unicdbdjdcd{{{\mname{Inj0}}~{x}} \in {{X}\uniadadcdcg{Y}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 1c640838de3fb39c7e9ba79c5409e04f12c37645baf67043e9f7f4278de39039 \\
Pure Prop Address: & TMKTYzxjjWdrWetApF9Sj67Z6edBVD8EBTo \\
Theory Prop Id: & 246ac5b8e5010b12d563e2f045e2abdb51d794611ea8dd590bc0fe11e5a7ad33 \\
Theory Prop Address: & TMTNL3J3wEnAzxucGw8kUWBscSaUn4BLgiu
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Inj1_setsum
\end{verbatim}
\begin{theorem}\label{thm:jeogkgbdpfdhfgehdhfhng} ${\unicdcdadad X Y y : {\iota} .  {{{y} \in {Y}}\unicdbdjdcd{{{\mname{Inj1}}~{y}} \in {{X}\uniadadcdcg{Y}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d47a0f2a013d89032cb64812b92012dc27b1d5fcc204fbc9a9c86638237204e2 \\
Pure Prop Address: & TMVgD1dS7zmrgJcgocmjP99ka8Dpg62ZCtL \\
Theory Prop Id: & 2b4f9491906d1ef49131201b69a9b8bd7d2f1ebf95fe8d5c0244a559215334ac \\
Theory Prop Address: & TMVk4zcLngHpsDrazL9rzQjzJ6jxFvj2f6c
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
setsum_Inj_inv
\end{verbatim}
\begin{theorem}\label{thm:dhfgehdhfhngpfjeogkgpfjgoggh} ${\unicdcdadad X Y z : {\iota} .  {{{z} \in {{X}\uniadadcdcg{Y}}}\unicdbdjdcd{{({\unicdcdaddd x \in {X} .  {{z}={{\mname{Inj0}}~{x}}}})}\unicdcdcdid{({\unicdcdaddd y \in {Y} .  {{z}={{\mname{Inj1}}~{y}}}})}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 645a6ce0a1cd5ad2ce3ac83a7b4d74f5954bae61db680341db619c0b10612a16 \\
Pure Prop Address: & TMGJozk41a81Kp4SygTYFZeKcuHrdPrC32q \\
Theory Prop Id: & a36400c28b0f8902008e9de3432e7367f347381ef074614db8802940be43cbc6 \\
Theory Prop Address: & TMHiPKm9hQiccXFfb4skC57UHenaqznn87b
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Inj0_setsum_0L
\end{verbatim}
\begin{theorem}\label{thm:jeogkgadpfdhfgehdhfhngpfadme} ${\unicdcdadad X : {\iota} .  {{{0}\uniadadcdcg{X}}={{\mname{Inj0}}~{X}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0be1e755f689c575a9eda08885f30343eeee939fbebeab4f3fa42931ed3bf82f \\
Pure Prop Address: & TMK8zdDs3kr6c2kZDhfjxDumvkoP5SgQ9RW \\
Theory Prop Id: & 36fabd108b18f5565ca33eddd506b2b62395333c16b3399474bae3abea3b0ada \\
Theory Prop Address: & TMbUYG9UEmYDqfxYZUKHNBKT4Y75njU2mbq
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Inj1_setsum_1L
\end{verbatim}
\begin{theorem}\label{thm:jeogkgbdpfdhfgehdhfhngpfbdme} ${\unicdcdadad X : {\iota} .  {{{1}\uniadadcdcg{X}}={{\mname{Inj1}}~{X}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f8d72132080ef3e20ece3ff94da26f46176e6715a7f569d277aefa88c73c3774 \\
Pure Prop Address: & TMVZEiZNntaDr4daY1DmuXvonFq9uNTdmig \\
Theory Prop Id: & 45b1c8dba7f1e6bb6910722f4bbf2ac5cec44dc5e8ebd74f245640488f2aa566 \\
Theory Prop Address: & TMME8xmRrBtE5QcayY5Ek96RbNEE8zSo5C2
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
nat_setsum1_ordsucc
\end{verbatim}
\begin{theorem}\label{thm:ogbgehpfdhfgehdhfhngbdpfpgchegdhfhdgdg} ${\unicdcdadad n : {\iota} .  {{{\mname{nat\_p}}~{n}}\unicdbdjdcd{{{1}\uniadadcdcg{n}}={{\mname{ordsucc}}~{n}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 3be3cce904aadda436daf1b9679086129be4811093362608100e6f068bdd4039 \\
Pure Prop Address: & TMHYS9eCHQRks9avhfkoeHGSrbHGL8uaBv1 \\
Theory Prop Id: & 8fbdda58ab70c8d36db764f1f86d169ce58ba6cc946bd4cb21cc5936808f1183 \\
Theory Prop Address: & TMUdCytedFWrC4iKskiF2SDYbA8djETMgpn
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
setsum_0_0
\end{verbatim}
\begin{theorem}\label{thm:dhfgehdhfhngpfadpfad} ${{{0}\uniadadcdcg{0}}={0}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 5dcaebebb574103d0edf890d85e23a5fa97b59db661795af9daeb7aa65f336a4 \\
Pure Prop Address: & TMaVr4aCWi6koabmAQVJ2wQdpL7mC7foUu9 \\
Theory Prop Id: & 4f3651b8f623daa8b048a8735ce8791d53d3c1d1b0f2aa681c537176ab51a619 \\
Theory Prop Address: & TMHtDbLm7fFXE2PBw9a9TaKFqUT1oKq4DFj
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
setsum_1_0_1
\end{verbatim}
\begin{theorem}\label{thm:dhfgehdhfhngpfbdpfadpfbd} ${{{1}\uniadadcdcg{0}}={1}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & c2107f17a63765673ccaf223da15ffd6fe6fcb31499a0a5fc5415779192120e5 \\
Pure Prop Address: & TMXomoBYE3zuVe9e7kyBAEnPduKtPVYL79A \\
Theory Prop Id: & e8609a742bc15d0823294b218d9d7e9f9d926e9cb69df0e589c81a5f60f5366e \\
Theory Prop Address: & TMGKXxfahnZuNyLnFqGHv1d446PYGT5n9MX
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
setsum_1_1_2
\end{verbatim}
\begin{theorem}\label{thm:dhfgehdhfhngpfbdpfbdpfcd} ${{{1}\uniadadcdcg{1}}={2}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 9c89c04ece2b66ca83b8a9b210a7f94ab137834db0b093883a5ab955eb6ef743 \\
Pure Prop Address: & TMSMi29gtadSxAPeBb5CCz27pw11Gt1r5Md \\
Theory Prop Id: & ef3f41b81000348e190c1253edc936248dee43fc698ee536fa6d9f1c6e97c1aa \\
Theory Prop Address: & TMH43YDo7oYg8zrgf9FjkpTTpmMyXLKMTTt
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
setsum_mon
\end{verbatim}
\begin{theorem}\label{thm:dhfgehdhfhngpfngpgog} ${\unicdcdadad X Y W Z .  {{{X} \subseteq {W}}\unicdbdjdcd{{{Y} \subseteq {Z}}\unicdbdjdcd{{{X}\uniadadcdcg{Y}} \subseteq {{W}\uniadadcdcg{Z}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 6e30186eb9483aaffe4c265cfe38dc213a2cf9faf3f5aa66b43cdfe7c9a5d2ca \\
Pure Prop Address: & TMUfRBKC5kCVDQmt7f2Q83pWENdCggpCtEM \\
Theory Prop Id: & 838d561df06bc2aee2d92713cb2b2d1c726613db9da9186614c6563f51c2bf86 \\
Theory Prop Address: & TMW7Tpt1vt99hraFFFRzz5pjENcaXQ9VV51
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:dgpgngcgjgogfgpfggfhogdgdh}
  We define $\mname{combine\_funcs}$ to be
  $${\uniddcgcg X Y f g z .  {\mif{{{z}={{\mname{Inj0}}~{({{\mname{Unj}}~{z}})}}}}{{{f}~{({{\mname{Unj}}~{z}})}}}{{{g}~{({{\mname{Unj}}~{z}})}}}}}$$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{\iota}})}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{\iota}})}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}}}}$
  identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & ccac4354446ce449bb1c967fa332cdf48b070fc032d9733e4c1305fb864cb72a \\
Pure Object Address: & TMKSa978XJEMycuWYBhLHN2QGXRqqHaF4Bb \\
Theory Object Id: & aa7bb3bbd2ec8e8fd8ba27aa97a6fc35a6ab1e3003dbbf6136a6110f1823bb93 \\
Theory Object Address: & TMJtkvSshA8XZqXDCbMyvjzjiyzZfNwnBom
\end{tabular}
\end{center}

\end{definition}
\begin{verbatim}
combine_funcs_eq1
\end{verbatim}
\begin{theorem}\label{thm:dgpgngcgjgogfgpfggfhogdgdhpffgbhbd}
  $${\unicdcdadad X Y .  {\unicdcdadad f g : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad x .  {{{{{{{\mname{combine\_funcs}}~{X}}~{Y}}~{f}}~{g}}~{({{\mname{Inj0}}~{x}})}}={{f}~{x}}}}}}.$$
  The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 19f032786d18528530a8e52c17dfc6a4417805e17b1a6ee6ed1364c06b749913 \\
Pure Prop Address: & TMXtLgamyXaY4YgLpaWoWvf8a28MSYTmXZ7 \\
Theory Prop Id: & a0730ef167ec6039eaf3084667d145e2e26662596942c8973bd0711b71f18ad3 \\
Theory Prop Address: & TMa8SMHnUqoCuZw2Kk78KMtZVfqopa2somA
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
combine_funcs_eq2
\end{verbatim}
\begin{theorem}\label{thm:dgpgngcgjgogfgpfggfhogdgdhpffgbhcd}
  $${\unicdcdadad X Y .  {\unicdcdadad f g : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad y .  {{{{{{{\mname{combine\_funcs}}~{X}}~{Y}}~{f}}~{g}}~{({{\mname{Inj1}}~{y}})}}={{g}~{y}}}}}}.$$
  The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 709f34af1e90fda80a83b8965675935d92fb44648d48274e89b23dc20e8ebff5 \\
Pure Prop Address: & TMLVrnvc3Z1Pjpg39KChTrX1Jjknz3bF3ri \\
Theory Prop Id: & 3933870bb4bccaad7d50c4972cba92adb92a7d7ff41c00d8ef4c83b8c60fad83 \\
Theory Prop Address: & TMTpr4M3N39vULCLJKgNMnuiESzd162fkqo
\end{tabular}
\end{center}

\end{theorem}
