\chapter{Some Basic Results}

\begin{theorem}\label{thm:gebgmgdhfgfe} ${{\mname{False}}\unicdbdjdcd{\unicdcdadad p : {o} .  {p}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0dcfe33e27797b7b436d2f4d048a94573a53d6753db4a3cc25933a3dd6f89015 \\
Pure Prop Address: & TMKsmG8CTue9Uq3xFgtUwj8xZhW6Vsv7LaE \\
Theory Prop Id: & f9a230def2f4412d999116d577818e7c13149b3ffd6ec8c0f216fb2570056eab \\
Theory Prop Address: & TMJrbzrCp7MPJvNNanPW79aqzPDUV4gcM4o
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:efchfhfgje} ${\mname{True}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f81b3934a73154a8595135f10d1564b0719278d3976cc83da7fda60151d770da \\
Pure Prop Address: & TMXh1PeTNoRdeQMkipsnTZ1NBoLMCSQGszg \\
Theory Prop Id: & eb5cbf9e00c1dc6fbac87f0e7dd91901a69a5afc430de9f265def7009d06523d \\
Theory Prop Address: & TMdaMQ9TGYHTUYWtAiezq6j2m9Lh8nTGaJX
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogpgehje} ${\unicdcdadad A : {o} .  {{({{A}\unicdbdjdcd{\mname{False}}})}\unicdbdjdcd{\preoh{{A}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 67ebfbb7241f6a92dbb75a0571d5396f165877e75a006c85956aeff1c756032a \\
Pure Prop Address: & TMMfBXPbPGW7MmkNMsTQVtkyifxwbPw9VeV \\
Theory Prop Id: & 12f948374053b3cf6da14578610534d466feec847f6e53f73e2bb362ee644abb \\
Theory Prop Address: & TMUAmMSt4Wx5Red5pwuUbb3SEBepWAW1UwN
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogpgehfe} ${\unicdcdadad A : {o} .  {{\preoh{{A}}}\unicdbdjdcd{{A}\unicdbdjdcd{\mname{False}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 23bb78c7c174d96fa3a932c82b14d7e88bfb71751aaaf84541df8ff1a4ceaf2e \\
Pure Prop Address: & TMVPdAHpYAjBMsM3in5F2sssApoxWNtPMfR \\
Theory Prop Id: & 856e325af2a33a3529471e559a4573ad6338bfc260d1c5073519e9b223161c81 \\
Theory Prop Address: & TMe11m2tYgGjWUJtGEX5X1tvrSDZWn8w2j1
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:bgogegje} ${\unicdcdadad A B : {o} .  {{A}\unicdbdjdcd{{B}\unicdbdjdcd{{A}\unicdcdcdhd{B}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 3c4f59ac38ec13161d275eff419ecea194e7a962d51e721d2c93249a9130e97c \\
Pure Prop Address: & TMdtgzJ3v8tqbJfC6ZLrrzp79xerKpJKvkB \\
Theory Prop Id: & 3bf1985f2198e37de5686038da57a16773e504ab6257e9686d49bfa2edd1762f \\
Theory Prop Address: & TMFJPpp7jnkJTJUfrH6ULPhVR9zhYrkB16u
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:bgogegfeme} ${\unicdcdadad A B : {o} .  {{{A}\unicdcdcdhd{B}}\unicdbdjdcd{A}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & c2f006baa588b23089bf32c5f1ecbbf59d67cec883a690fc7a3dfd4f92b52e28 \\
Pure Prop Address: & TMNrPqMjXhvQDz1y7fMcUrWvqz8EvpMAuGq \\
Theory Prop Id: & 718be46f06f0025b5dbef8d8ac0138d307c9b79d1e220278818af7e7137afaf1 \\
Theory Prop Address: & TMP2MCwM6msNpa6CvfXzjby7fxBAXQCafdT
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:bgogegfecf} ${\unicdcdadad A B : {o} .  {{{A}\unicdcdcdhd{B}}\unicdbdjdcd{B}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f66b82a6432b84ea5d3544eec5c9459bd603e2c74b7dc20fdb37c6c0278a30d2 \\
Pure Prop Address: & TML2fqTH52b5jHHUqj4UWsE6pCJqVKiMDrP \\
Theory Prop Id: & 5caea9b570346a0a4827977bc317350a63bfb51530b8489373b29970868e822a \\
Theory Prop Address: & TMRHXWMGqfM8cUBGJnz16hksWXqTpSxL6AN
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchjeme} ${\unicdcdadad A B : {o} .  {{A}\unicdbdjdcd{{A}\unicdcdcdid{B}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 55be8c084d3d69aaadcdfedd53b12314b3f00b7aa0fe62bba95d8e20a6913eef \\
Pure Prop Address: & TMcR7JViW1Pt5HqJG1ZrAu2LnZ6BoYWBfiw \\
Theory Prop Id: & 38267393635d01946334424cfe8e37c8739b8cefeb185f7310c8efc17536d3b6 \\
Theory Prop Address: & TMWwPCgtJ9GA5byYB2oN3wyknGgpGw6sABs
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchjecf} ${\unicdcdadad A B : {o} .  {{B}\unicdbdjdcd{{A}\unicdcdcdid{B}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 3c63fc5739c09fc9b12fb6d378e9de249f610fbbf2df1cce28f85000280f7bfb \\
Pure Prop Address: & TMTfYZuPbL4xJdZTnLMEYGVXQTCZrDeAcef \\
Theory Prop Id: & 8d8e400885f8d52e5c13e42b0127916d2d04fa1a6277be7ce7b01afd1b7e90bc \\
Theory Prop Address: & TMShT5hWbYuTfR7XBLwEnzy4XoJLhwhTWfs
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchfe} ${\unicdcdadad A B C : {o} .  {{({{A}\unicdbdjdcd{C}})}\unicdbdjdcd{{({{B}\unicdbdjdcd{C}})}\unicdbdjdcd{{{A}\unicdcdcdid{B}}\unicdbdjdcd{C}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 5af08e7b4b57e0dbdc28c2fff18dfe38e04e61787986420a7b92d8802bd7ebef \\
Pure Prop Address: & TMRxb9x7hsQcQdArwJPp9wuFPEjCqtSpjvD \\
Theory Prop Id: & 27f42ce3892a9e7634f07197c79efa6d1892500cb92de0ba160f103333bae4e5 \\
Theory Prop Address: & TMXA3QBiXM4MyCoYLxr1N5ZWgF5hLhEUP3r
\end{tabular}
\end{center}

\end{theorem}
\section{PropN}\label{afchpgahoe}Let $ P1 P2 P3 : {o}$ be given.
\begin{theorem}\label{thm:bgogegddje} ${{P1}\unicdbdjdcd{{P2}\unicdbdjdcd{{P3}\unicdbdjdcd{{{P1}\unicdcdcdhd{P2}}\unicdcdcdhd{P3}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 23ac9ca708caa1dd38b9d722781b028bb2d1c60d27249f613f0f58a46f811df6 \\
Pure Prop Address: & TMTCLZz943DGXmGagi5cxC1VhkU7Xh7gmxj \\
Theory Prop Id: & cb999bf5d18c324be0801b18f227a943efbdaa196adbe869b96f43be18f1790d \\
Theory Prop Address: & TMHU8VN1xhmJmu7CW62fpKC6YQYCHXWhdNt
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:bgogegddfe} ${{{{P1}\unicdcdcdhd{P2}}\unicdcdcdhd{P3}}\unicdbdjdcd{({\unicdcdadad p : {o} .  {{({{P1}\unicdbdjdcd{{P2}\unicdbdjdcd{{P3}\unicdbdjdcd{p}}}})}\unicdbdjdcd{p}}})}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 445f7614b5a460ac2ee2c65f60676f43814b16323277b97c9e03b7e2d5ef1bca \\
Pure Prop Address: & TMHw71AzVXN296b5iiE9yrMayr1gPK6Dmgn \\
Theory Prop Id: & 50fabe4d504ce92226b4ca92d7a1ab747f919e6c3d6c87a33765f260310d73ef \\
Theory Prop Address: & TMRpTuB7NQrKHNzC82mBhAzGZdBLPpwn8YZ
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchddjebd} ${{P1}\unicdbdjdcd{{{P1}\unicdcdcdid{P2}}\unicdcdcdid{P3}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & e44f34f452d8efd0440da0051ba3966fc604cdf0f1a7d5a43a24ebca3f6477e6 \\
Pure Prop Address: & TMY8tfGHE5SpXjBtYW9GnGTRRRYZjTkVC1h \\
Theory Prop Id: & ef9071fe3a6dd6111bf8b4b88913d688c289a81f6af948df2b99c0f80d2ac6c1 \\
Theory Prop Address: & TMKCha5JJm2rxV2CyYeXrokWFDR2ryrF4rE
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchddjecd} ${{P2}\unicdbdjdcd{{{P1}\unicdcdcdid{P2}}\unicdcdcdid{P3}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 8df6e153401808c8d1877008f68f33f35f4bb6901c96d857f1e0f13e1519cce6 \\
Pure Prop Address: & TMcANDxLDCL4xKQuqhsiQV2MPpGnTrcX2tb \\
Theory Prop Id: & 827a91555bc9a5f9fbc87e42c706559e78927705587b35109c356ece2a13307d \\
Theory Prop Address: & TMJjiRdEq1FHszQpepkDPdNLaNYqcVQvb3g
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchddjedd} ${{P3}\unicdbdjdcd{{{P1}\unicdcdcdid{P2}}\unicdcdcdid{P3}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 017a00202c1447a85eee3f717fabbb57b1194539474715a7958654c3eeff6dba \\
Pure Prop Address: & TMMKVc34VAUfiURqFmHXpwwfDmcdTEMi8p9 \\
Theory Prop Id: & 3b7f5abd745db6a80ff6dd817b2bc916034448d1d8cca1a8e2958f0b3257c71c \\
Theory Prop Address: & TMc5vyzo3ArE8GAUf3UUvpSQdgk1mgJAYae
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchddfe} ${{{{P1}\unicdcdcdid{P2}}\unicdcdcdid{P3}}\unicdbdjdcd{({\unicdcdadad p : {o} .  {{({{P1}\unicdbdjdcd{p}})}\unicdbdjdcd{{({{P2}\unicdbdjdcd{p}})}\unicdbdjdcd{{({{P3}\unicdbdjdcd{p}})}\unicdbdjdcd{p}}}}})}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 5d069d8e90aea128ccbc62404954d9fa5e38854f6dea8d51e13e68ff413e0ab1 \\
Pure Prop Address: & TML79YQmK3xkoSvhsjHcVf5xiAdsKJpEJBe \\
Theory Prop Id: & 2120c9770c0268721584c931577292b619113ab7eeb88e02ffbf738291ce46f1 \\
Theory Prop Address: & TMTxTUaNh3Y288kongaMx7qkfusZvuByRau
\end{tabular}
\end{center}

\end{theorem}
Let $ P4 : {o}$ be given.
\begin{theorem}\label{thm:bgogegedje} ${{P1}\unicdbdjdcd{{P2}\unicdbdjdcd{{P3}\unicdbdjdcd{{P4}\unicdbdjdcd{{{{P1}\unicdcdcdhd{P2}}\unicdcdcdhd{P3}}\unicdcdcdhd{P4}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & ed32cbf9688b8877bdd20c59f473bb9c69432ffd24de548cfc4c59616dd11c5a \\
Pure Prop Address: & TMdAoQLQ3RM117hTZoE6J4XtvGzkLFHKGQm \\
Theory Prop Id: & 906aaf2cf039cec16718707b69fda8d19357ca96611472679c8c38ac5552d505 \\
Theory Prop Address: & TMXRatgrgSzbMm1bvkukK5JVrsGh2z8rQ6u
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:bgogegedfe} ${{{{{P1}\unicdcdcdhd{P2}}\unicdcdcdhd{P3}}\unicdcdcdhd{P4}}\unicdbdjdcd{({\unicdcdadad p : {o} .  {{({{P1}\unicdbdjdcd{{P2}\unicdbdjdcd{{P3}\unicdbdjdcd{{P4}\unicdbdjdcd{p}}}}})}\unicdbdjdcd{p}}})}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 7f6e6c52947184716f0a59a54ee2c3fd4562ee529d8e109ad2527c908611d3be \\
Pure Prop Address: & TMTwtsu5L9Ezi887h92X1qCCtTSgg6Z5Fxr \\
Theory Prop Id: & b41cb764baa71ac5c454b1c9bff373c0bc8ceac5c10a56f18ba2e4a30db98bd1 \\
Theory Prop Address: & TMT4yM4NV4sxuvWZUkXew6X7hJ9zigrwUfZ
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchedjebd} ${{P1}\unicdbdjdcd{{{{P1}\unicdcdcdid{P2}}\unicdcdcdid{P3}}\unicdcdcdid{P4}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d61309b1a6dfcdb5b57f074782c88d8e6004fb5bd8c217f4ef2e88a3376de181 \\
Pure Prop Address: & TMNvs8HY31Qn4Ju5WNUWKVjbaoTkg7MDXDG \\
Theory Prop Id: & d10b2eb23a5fa505396dff509fa1c442d6870e72d887a41bf455239abe6dff54 \\
Theory Prop Address: & TMaTMcRZ9E1Rb4Nuq4C1Ho7bwKAyCZhJbn1
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchedjecd} ${{P2}\unicdbdjdcd{{{{P1}\unicdcdcdid{P2}}\unicdcdcdid{P3}}\unicdcdcdid{P4}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 17c763a32537244fd99d77c2973672e33ccdcb0195284690a5b20a50d917f1bc \\
Pure Prop Address: & TMMFmRtJXqQaL2pJyCq2NXmUoQo6iEcBUeF \\
Theory Prop Id: & f9e4cf5b7be5972585b09b77e8fe2de549ffcd217050934f83ca2a0269d7c22e \\
Theory Prop Address: & TMXYRWPJ6eBJ2veji2CB4sPXSweJfbMW9NC
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchedjedd} ${{P3}\unicdbdjdcd{{{{P1}\unicdcdcdid{P2}}\unicdcdcdid{P3}}\unicdcdcdid{P4}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 7500b33566aaf93de84ea48148bfb3bb21b30ec225170d993339f8bb0cbbaaf1 \\
Pure Prop Address: & TMZiwfSWdAkAZ7WSEnmx8EfCq26LV9zrvDT \\
Theory Prop Id: & 1a5881c849fb86fd77a8a4f11ef6783644b06e8c3f74fb02af0c13b7a816c3a7 \\
Theory Prop Address: & TMHnh1oKCafRDqpe4JxXfg2qfSkei64vT35
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchedjeed} ${{P4}\unicdbdjdcd{{{{P1}\unicdcdcdid{P2}}\unicdcdcdid{P3}}\unicdcdcdid{P4}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 7a20061f67b705b52da52d1619188bf47b727e3bf41cab7aab5e3b9c6c9e1e9f \\
Pure Prop Address: & TMVBHMZoCoxkQBLGMKjpPfCyWzaL2nkaZx4 \\
Theory Prop Id: & 1ecd5bc77d1ec7549783816ee07b8441f43a51ff5ab63ec30ca559c442813060 \\
Theory Prop Address: & TMFhHjtCoxKWhG8QRGUQ92dvizsEVBwWvYQ
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchedfe} $${{{{{P1}\unicdcdcdid{P2}}\unicdcdcdid{P3}}\unicdcdcdid{P4}}\unicdbdjdcd{({\unicdcdadad p : {o} .  {{({{P1}\unicdbdjdcd{p}})}\unicdbdjdcd{{({{P2}\unicdbdjdcd{p}})}\unicdbdjdcd{{({{P3}\unicdbdjdcd{p}})}\unicdbdjdcd{{({{P4}\unicdbdjdcd{p}})}\unicdbdjdcd{p}}}}}})}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d05b31b0be8cd483fa07a3f0f19264b60e47f6c21659902935462906bdf6b76d \\
Pure Prop Address: & TMQwRKYH5ei57PtG8MGuyMNQBKe8cuszmF4 \\
Theory Prop Id: & 1fdc2a30b796702db155c2eb5a9c6e71c48a99beca4fc05f20102b22e9cdce47 \\
Theory Prop Address: & TMWhPKKnyM7dRKMXmnAxawenezrpwrV9cgz
\end{tabular}
\end{center}

\end{theorem}
Let $ P5 : {o}$ be given.
\begin{theorem}\label{thm:bgogegfdje} ${{P1}\unicdbdjdcd{{P2}\unicdbdjdcd{{P3}\unicdbdjdcd{{P4}\unicdbdjdcd{{P5}\unicdbdjdcd{{{{{P1}\unicdcdcdhd{P2}}\unicdcdcdhd{P3}}\unicdcdcdhd{P4}}\unicdcdcdhd{P5}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 041ced6dc277faece2d470de6befa0e97006998af0c9cb1989fc9901b3ec866f \\
Pure Prop Address: & TMVd1Ghg1sxR7zcgk4GPNy72pYJ9AQdBzd6 \\
Theory Prop Id: & 11fc478665305a3b2e27aa913e8dcb933d84e00ee923c3e503f0ed51d4ed7d8f \\
Theory Prop Address: & TMFEndoHPA1ez9Y8dc2y2YAf6QxYxCFg4BB
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:bgogegfdfe} $${{{{{{P1}\unicdcdcdhd{P2}}\unicdcdcdhd{P3}}\unicdcdcdhd{P4}}\unicdcdcdhd{P5}}\unicdbdjdcd{({\unicdcdadad p : {o} .  {{({{P1}\unicdbdjdcd{{P2}\unicdbdjdcd{{P3}\unicdbdjdcd{{P4}\unicdbdjdcd{{P5}\unicdbdjdcd{p}}}}}})}\unicdbdjdcd{p}}})}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & b9e36eb0772059378de6e2bae57aec129036e5378cd37e203e1791e7b44f92cf \\
Pure Prop Address: & TMJBWvgmbPvfKX7ymNvDkg1M46iQe7Ny1z7 \\
Theory Prop Id: & a02e0e4e7793f2f93af907335f12098d37abc74e46d2eeb4465324ba9d8046db \\
Theory Prop Address: & TMMmsE2QkKEBNxNaoo9zCfmr5o7QBZgTPGQ
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchfdjebd} ${{P1}\unicdbdjdcd{{{{{P1}\unicdcdcdid{P2}}\unicdcdcdid{P3}}\unicdcdcdid{P4}}\unicdcdcdid{P5}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 39ea457dead1717f0a108c7304916bfd9cab247cf4cf2d3b67f5065814a8e0b4 \\
Pure Prop Address: & TMUs12JtV2vEaiiahyRUXpuovbU11fq7zLB \\
Theory Prop Id: & 4e8f4064dae12df31e7df3da1e5c8535b89046a7b5319d8f2305e5de1b24f829 \\
Theory Prop Address: & TMTPcpiEwfkrghjEEposf5yS1v869ke7Rrj
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchfdjecd} ${{P2}\unicdbdjdcd{{{{{P1}\unicdcdcdid{P2}}\unicdcdcdid{P3}}\unicdcdcdid{P4}}\unicdcdcdid{P5}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 8494de963a2912613d2bfb1d747fc055d6eb362d422be1896eee6d866c358af9 \\
Pure Prop Address: & TMFZtXVUhAJgMrzbc8SGQr8PvkqfircW7cL \\
Theory Prop Id: & 32035af2da626c1acd3d71cbf3197f52b67159384f068ebb3b5f4c50a08ce3db \\
Theory Prop Address: & TMR8LzrcpDPkw2uf7T8WHukPntFRQWVakmR
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchfdjedd} ${{P3}\unicdbdjdcd{{{{{P1}\unicdcdcdid{P2}}\unicdcdcdid{P3}}\unicdcdcdid{P4}}\unicdcdcdid{P5}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 09182b1c056c3e6ec773e5fb3c476f7e026643a15998bb79deb35e131fc516a4 \\
Pure Prop Address: & TMV1nEkVMZR4hjji67oiYpLCFwcPavF6bSp \\
Theory Prop Id: & 4aca859beb67b87c07448642e2f80b02e346c431898060774f6806896b8bc060 \\
Theory Prop Address: & TMVdimQJwC5PcNHpaQeD8vVev4mkSnqKUDh
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchfdjeed} ${{P4}\unicdbdjdcd{{{{{P1}\unicdcdcdid{P2}}\unicdcdcdid{P3}}\unicdcdcdid{P4}}\unicdcdcdid{P5}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 51cd1ca65c14f555453c13f820eac600735e6825f73e4e668138659cb752ce82 \\
Pure Prop Address: & TMRxkMs8kLmmDi8zdv7a2mgmiiwm8gtbeQC \\
Theory Prop Id: & 8e109e9f1c205c91c5b79a556c11e2b2fb94d2d77c537f904faaf5e7cdf2fce4 \\
Theory Prop Address: & TMTZe6z6z3GDdCznmKAm5d5ZAas3rSPduhh
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchfdjefd} ${{P5}\unicdbdjdcd{{{{{P1}\unicdcdcdid{P2}}\unicdcdcdid{P3}}\unicdcdcdid{P4}}\unicdcdcdid{P5}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 1d6362c9b2c69a1b4b1360eef0b6f9f9763f1089e1bbde2904b3db2c6544b5b9 \\
Pure Prop Address: & TMHM6WDtzUk5yH5hFkLWwTSXzie4fHKJkeR \\
Theory Prop Id: & 5947729b14c31f7f5dfb495f3dc278156afc20b954ecaa24e6839650aef497bf \\
Theory Prop Address: & TMWqVbPVCB7MunfAfT8ReFmNyoB4QbkEzA2
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchfdfe} $${{{{{{P1}\unicdcdcdid{P2}}\unicdcdcdid{P3}}\unicdcdcdid{P4}}\unicdcdcdid{P5}}\unicdbdjdcd{({\unicdcdadad p : {o} .  {{({{P1}\unicdbdjdcd{p}})}\unicdbdjdcd{{({{P2}\unicdbdjdcd{p}})}\unicdbdjdcd{{({{P3}\unicdbdjdcd{p}})}\unicdbdjdcd{{({{P4}\unicdbdjdcd{p}})}\unicdbdjdcd{{({{P5}\unicdbdjdcd{p}})}\unicdbdjdcd{p}}}}}}})}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & b956eb2b7204f5a6e780e90bc1bd534e682ab77b2ad4cb7c5d03d8acacfc9a2e \\
Pure Prop Address: & TMURL8fhzF9KpcCx1BootRK4CFuzooNhaUw \\
Theory Prop Id: & 780a9f1fdc60b8ddc55d630d2b78a74557585751e69471682b41605c6a27eef9 \\
Theory Prop Address: & TMVMNDhbZznQnqiXkLo51F83SmRwT6czcWC
\end{tabular}
\end{center}

\end{theorem}
Let $ P6 : {o}$ be given.
\begin{theorem}\label{thm:bgogeggdje} ${{P1}\unicdbdjdcd{{P2}\unicdbdjdcd{{P3}\unicdbdjdcd{{P4}\unicdbdjdcd{{P5}\unicdbdjdcd{{P6}\unicdbdjdcd{{{{{{P1}\unicdcdcdhd{P2}}\unicdcdcdhd{P3}}\unicdcdcdhd{P4}}\unicdcdcdhd{P5}}\unicdcdcdhd{P6}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 9817c7a535d81bed18efaa95b110653ebba78a7ad991eaca8054c41020b664da \\
Pure Prop Address: & TMM8hfvyGGBPHT3XKYSQ5WjPZBdQu8CHFmh \\
Theory Prop Id: & a5dc2935b019c23338edba6ccdea3a654b6a51efe6170f8887e55dc4e5d6e4ff \\
Theory Prop Address: & TMNPT8qknaGSp8UzvMyiNy5UD7HRGHNMvZ9
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:bgogeggdfe}
$${{{{{{{P1}\unicdcdcdhd{P2}}\unicdcdcdhd{P3}}\unicdcdcdhd{P4}}\unicdcdcdhd{P5}}\unicdcdcdhd{P6}}\unicdbdjdcd{({\unicdcdadad p : {o} .  {{({{P1}\unicdbdjdcd{{P2}\unicdbdjdcd{{P3}\unicdbdjdcd{{P4}\unicdbdjdcd{{P5}\unicdbdjdcd{{P6}\unicdbdjdcd{p}}}}}}})}\unicdbdjdcd{p}}})}}.$$
The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 3668da80c73d5b9a85e7b685ab4ed93a92bdbb2a7cacf0c764a2353bffd98bd5 \\
Pure Prop Address: & TMQ5JF8b5hxhEB7utWT6iBHdgtNte14WFKZ \\
Theory Prop Id: & 1c4fc650221a6c544c529f279d39c9effe360f4bbb342bf30ac2ef1bb0cae7bd \\
Theory Prop Address: & TMXE3S7PKbVYmocgEe4jSS2d628TPGWZpTj
\end{tabular}
\end{center}

\end{theorem}
Let $ P7 : {o}$ be given.
\begin{theorem}\label{thm:bgogeghdje} ${{P1}\unicdbdjdcd{{P2}\unicdbdjdcd{{P3}\unicdbdjdcd{{P4}\unicdbdjdcd{{P5}\unicdbdjdcd{{P6}\unicdbdjdcd{{P7}\unicdbdjdcd{{{{{{{P1}\unicdcdcdhd{P2}}\unicdcdcdhd{P3}}\unicdcdcdhd{P4}}\unicdcdcdhd{P5}}\unicdcdcdhd{P6}}\unicdcdcdhd{P7}}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 6a4d8ce6f0dd012e01148d6cfcd0336a7bdfd1f6e0a108700387aa6534f21e3a \\
Pure Prop Address: & TMcFEeC2wp56VXpGCwrrXAy9KX7iPCggM9d \\
Theory Prop Id: & c89388f0b732abd74a2fb4d6fef23202a20e588058361e4617d162de86cd6b7d \\
Theory Prop Address: & TMFwsYdcsUc2UYbNFsd4RzP6m2K8FrCgFrq
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:bgogeghdfe} $${{{{{{{{P1}\unicdcdcdhd{P2}}\unicdcdcdhd{P3}}\unicdcdcdhd{P4}}\unicdcdcdhd{P5}}\unicdcdcdhd{P6}}\unicdcdcdhd{P7}}\unicdbdjdcd{({\unicdcdadad p : {o} .  {{({{P1}\unicdbdjdcd{{P2}\unicdbdjdcd{{P3}\unicdbdjdcd{{P4}\unicdbdjdcd{{P5}\unicdbdjdcd{{P6}\unicdbdjdcd{{P7}\unicdbdjdcd{p}}}}}}}})}\unicdbdjdcd{p}}})}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 2ea6ee206fc0e0bac89e94ecdeb5cc8218a37b0e2ad93881ee4b947fe261aca5 \\
Pure Prop Address: & TMarbzMgS52Zmt6DZPQwD7NrgfFnGmniZBg \\
Theory Prop Id: & 02714a2b656b0d600f52d924edb42df9d13fd49d79bacc042df6ff567767a5a5 \\
Theory Prop Address: & TMJ3TDaD9hfZwexV6a4jq3FXE9KhjambBpi
\end{tabular}
\end{center}

\end{theorem}
\section{Further Results} % PropN
\begin{theorem}\label{thm:jgggggje} ${\unicdcdadad A B : {o} .  {{({{A}\unicdbdjdcd{B}})}\unicdbdjdcd{{({{B}\unicdbdjdcd{A}})}\unicdbdjdcd{({{A}\unicdbdjded{B}})}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 7516b9382e323d500a2b396c81bf98c3859ca15e7e7b359310c7cea2aeed5c8a \\
Pure Prop Address: & TMMjuJFnsPng1UMvQzKS18LFFsgWsi9d8xU \\
Theory Prop Id: & 4d966a5f5da0679b05fd8ce1619ac4165c9654be7a87ee2cceaaec3ceac10633 \\
Theory Prop Address: & TMddTKwGeWwMHruZq1JPdHyJmpeTrFg89Xi
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jgggggfeme} ${\unicdcdadad A B : {o} .  {{({{A}\unicdbdjded{B}})}\unicdbdjdcd{{A}\unicdbdjdcd{B}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0e94c69dbdcf6a1baca24d804ad190121b2de563e5642fa8c452be1c6595979b \\
Pure Prop Address: & TMPAKwBu2btn7LfWCbudNDBAqu86wzbzmEY \\
Theory Prop Id: & 9a07f60730cc4e5044b6b2af10fd8467b0bedf6f66364ca33c0818495467c2ed \\
Theory Prop Address: & TMTL1Jyg3GdY9swgWWQPXN6ceqVnBuFt1Dn
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jgggggfecf} ${\unicdcdadad A B : {o} .  {{({{A}\unicdbdjded{B}})}\unicdbdjdcd{{B}\unicdbdjdcd{A}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 54702aec0e7fabe49df0fa4b3a00910bf49c4c03c646ddc286485e7af2899fe8 \\
Pure Prop Address: & TMLxQTofs8NSTdPqLWVf9T5mVck9C5B8m8s \\
Theory Prop Id: & f5dfc0631a7727945b67f112d323c8a1558a724a0d6b5c261d4a11649d925f64 \\
Theory Prop Address: & TMGZN34A8TcN1Z21rxqNAMYJRjG67dAotvb
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jgggggpfchfggg} ${\unicdcdadad A : {o} .  {{A}\unicdbdjded{A}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 01338dd4902fcd80dd89af75713f451fe1b1e4804229f05955b962fe6def6250 \\
Pure Prop Address: & TMSKz5gXPFakcgFRBJ5RJYfDQC2q8ocrFi1 \\
Theory Prop Id: & 7b71b52f0f8ece18ad34af695ce60729d9853085b816941378947b88e44cbf0a \\
Theory Prop Address: & TML3Gcc3WbCE559uqmKxvpDahXs8iDJjURL
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfjgpfdhjhng} ${\unicdcdadad x y .  {{{x}\unicdcdgdad{y}}\unicdbdjdcd{{y}\unicdcdgdad{x}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 5c0ec9ea191d0f6e263cc182b469ec839768d633284966a6a6a2058c1778ed0f \\
Pure Prop Address: & TMXXdxoTHLJ7BfG4hU2CwgemEXjQ8FmtQ1C \\
Theory Prop Id: & 1a98981725a2236f37b1c465a0e41336ebef451702e4d9da44b1fab316a2e844 \\
Theory Prop Address: & TMdSA41VnJVw63YmxPtgsvson8sPkVFMoKc
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:ogjeog}
We define $\mname{nIn}$ to be ${\uniddcgcg x X .  {\preoh{{{{\mname{In}}~{x}}~{X}}}}}$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 36808cca33f2b3819497d3a1f10fcc77486a0cddbcb304e44cbf2d818e181c3e \\
Pure Object Address: & TMSqgddy21cUnLoRkMPcBAxXhAmCfaQeLQj \\
Theory Object Id: & 253451c995b7e8af5baae1333a990b55d0dea9af34d44b09b418d3f09fe72de4 \\
Theory Object Address: & TMReNhKc6t82pWW6stKo9YNy1BuLWXDCyeC
\end{tabular}
\end{center}

\end{definition}
{\bf{Notation.}} We use $\infpckdfg$ as an infix operator  corresponding to applying term ${\mname{nIn}}$.
\begin{theorem}\label{thm:feahdhpfjgpffgih} ${\unicdcdadad P : {{\iota}\unicdbdjdcd{o}} .  {{({\unicdcdaddd x .  {{P}~{x}}})}\unicdbdjdcd{{P}~{({{\mname{Eps\_i}}~{P}})}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & be36f0573e3745e47e74354bb117860bd387b3f6c26ba3a752a7388e6b66d647 \\
Pure Prop Address: & TMFoJytvVebF2Sg18ua9AU1WgCbeqEijvbZ \\
Theory Prop Id: & 6a28328c813ae82b72e327564626a89c19306d9b1f89653ada2b22e954e90881 \\
Theory Prop Address: & TMXYa9wuYkRrAmfCgqhH6hY5uK5GFw8gzHB
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ahchfgegpffgiheh} ${\unicdcdadad P Q : {{\iota}\unicdbdjdcd{o}} .  {{({\unicdcdadad x .  {{{P}~{x}}\unicdbdjded{{Q}~{x}}}})}\unicdbdjdcd{{P}={Q}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & e9e64b253f257e12e8cc34a6936324678cd05c9763263d2d12e48da4bd7198e7 \\
Pure Prop Address: & TMYnqc7V192uGaHR6Z4JQYWcpukZNrMq6cy \\
Theory Prop Id: & d4b2d3f3eabb3ff09d4d1a4e7e1663d78c31373aac18adcfbef2e2c081bb44fa \\
Theory Prop Address: & TMFdQW2ooCy3wDncDrzFGtMSsTwAzHRg5kG
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ahchpgahpffgihehpfcd} ${\unicdcdadad p q : {o} .  {{({{p}\unicdbdjdcd{q}})}\unicdbdjdcd{{({{q}\unicdbdjdcd{p}})}\unicdbdjdcd{{p}={q}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a9ede2c9e3cf1d70dfbf9f57d775f61afa29105059e99ada89c0de099e2c1a26 \\
Pure Prop Address: & TMNH7NvYuoPP9nYGA3ZMWdycLUsdiXP5REb \\
Theory Prop Id: & a56fc7bc69f2eed7db4340adfe025ace2f0f83cdfc470f09b018498a097775ab \\
Theory Prop Address: & TMYdTtZfAJ1wEsDSWCBMpXk181wbLRKQ2tT
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ahchfgegpffgihehpfcd} ${\unicdcdadad P Q : {{\iota}\unicdbdjdcd{o}} .  {{{P} \subseteq {Q}}\unicdbdjdcd{{{Q} \subseteq {P}}\unicdbdjdcd{{P}={Q}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & c558ffab38d9b7b5cc1866022b11c5f544a9b798f1745926e15f3391ff6cc87d \\
Pure Prop Address: & TML1d3NrCUcMsEZrsdaVLuyf7VGJq9zKYD8 \\
Theory Prop Id: & c5df8491488c0d5344f2a38c75caa07e6cfe3d5e89feb23ebc08798a9fdccfd4 \\
Theory Prop Address: & TMW8biyFW9jcdzzGjDz5sXDkojWntfdbQ1t
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:dffhcgbhpfchfggg} ${\unicdcdadad X : {\iota} .  {{X} \subseteq {X}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 4c53952cc6ecb22968534a4d43adab78af1f0b047ed070da10ea521d270d1f2a \\
Pure Prop Address: & TMWfjRz3PusvtrSBv2umMamuPFQ3vpfqq5R \\
Theory Prop Id: & 2efbacece8d60c274641e6775400fab460246bacd8ac2d18f883d059a7ac8358 \\
Theory Prop Address: & TMLkYwQzhxE5mhkLWGyedCPNtZ5dCRp8qmB
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:dffhcgbhpfehchbg} ${\unicdcdadad X Y Z : {\iota} .  {{{X} \subseteq {Y}}\unicdbdjdcd{{{Y} \subseteq {Z}}\unicdbdjdcd{{X} \subseteq {Z}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 79accb4060735cc396e0e3ea36014c3e94c87d8e52a22ed4c18d55d6af348d9e \\
Pure Prop Address: & TMXhwEo6mEGCoaDosK1LZDEK8xXZr8kji3H \\
Theory Prop Id: & fed662887c1b855fd3ff74e7894edbaebabacb12dcae138964b49804bddac9a6 \\
Theory Prop Address: & TMaozUoYZxHxHHTvoggGVukYwGVgw9VLyP8
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:dffhcgbhpfdgpgogehchbg} ${\unicdcdadad X Y z : {\iota} .  {{{X} \subseteq {Y}}\unicdbdjdcd{{{z}\unicdcdadjd{Y}}\unicdbdjdcd{{z}\unicdcdadjd{X}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d15e87bdbc1fd0a307b0f0b273414e5fca8c31ec8256241a668bcab8d25dc157 \\
Pure Prop Address: & TMZtpMMhjtkFakD25QWYgBYDJcz4naaYj5w \\
Theory Prop Id: & bd5a2f337d80e9eca8abab55ca08c824896fb8274ddacef26a0d1e1bf8b8f0a3 \\
Theory Prop Address: & TMFK5BFNrPEtMNeyxT8Acey4o4GybQWYQ8i
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fengahehjhfe} ${\unicdcdadad x : {\iota} .  {{x}\unicdcdadjd{\mname{Empty}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 93a77a0c78f3c49660c44dd07c723ad23e5e55e64c0dcd527a22c0278b829b8e \\
Pure Prop Address: & TMaSWKbJHDuPvqXN5ddrdRfghAejYyXef7K \\
Theory Prop Id: & 8349abf2aeba6cf6d62d407fc6062a629c409a81df869ba5e46a2adde87b67a5 \\
Theory Prop Address: & TMUoYxyibdoLdU1WGAmWKr2UQqgAiyrf8sb
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:dffhcgbhpffengahehjh} ${\unicdcdadad X : {\iota} .  {{\mname{Empty}} \subseteq {X}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a517cdaf3478a733b128a31cce59618dd840c79c17df99f29410ff3e9ba455e4 \\
Pure Prop Address: & TMWWMiBhRYozNqky8uYhTyxKxDXXVBjHmqH \\
Theory Prop Id: & 2faec377f13468a82bbfcb310b43ad7a193b5d26e72c513a4b6fbb139dd1f852 \\
Theory Prop Address: & TMJxeX1k56XRyrVDH9k6F9DZp2n6xFpPAck
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fengahehjhpfdffhcgbhpffgbh} ${\unicdcdadad X : {\iota} .  {{{X} \subseteq {\mname{Empty}}}\unicdbdjdcd{{X}={\mname{Empty}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 2dd95966ce09dd2345607d594b51d1640857501d96dea096bacb21e292697f31 \\
Pure Prop Address: & TMbzyCseCE8NavdH4tvfvqjNSXHHLkNaTk4 \\
Theory Prop Id: & 988691971197671404c5f64923b3e6f170a71f5f8f48e44c06089873913e08c9 \\
Theory Prop Address: & TMQENPUZ2wP5s7vyaLEtBCdaJErFFSUpJSV
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fengahehjhpffgbh} ${\unicdcdadad X : {\iota} .  {{({\unicdcdadad x .  {{x}\unicdcdadjd{X}}})}\unicdbdjdcd{{X}={\mname{Empty}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 3de0fdba2afc8aa47ba046f6d57a7edaabc38eebe8925bdc1b3803ca0a447373 \\
Pure Prop Address: & TMM1agcdRVrGxbz8kV5AmjKvcKDfDHWAxHb \\
Theory Prop Id: & 8b915bb396e264c2d82d33dc8dfd93f4374585f0ab37c01fc964b73f4e28b7a3 \\
Theory Prop Address: & TMcosVQ8txADpELPSRpWSvATFdw3vWrW8H2
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ffogjgpgogje} ${\unicdcdadad X x Y : {\iota} .  {{{x} \in {Y}}\unicdbdjdcd{{{Y} \in {X}}\unicdbdjdcd{{x} \in {{\mname{Union}}~{X}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 51b5499aea657de4516b761629ee7a8bf5292810ac70c13d0745541a55023b02 \\
Pure Prop Address: & TMQCYZzADyCKcXXBekJX5crLwK9MZzh7paV \\
Theory Prop Id: & bade054056415b264e8e0ad162a917d91a5399de193fc12ede490c8bf786acf3 \\
Theory Prop Address: & TMHDQ27UKqnJLKFeQDx27tH4XqzefSAZp1w
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ffogjgpgogfe} ${\unicdcdadad X x : {\iota} .  {{{x} \in {{\mname{Union}}~{X}}}\unicdbdjdcd{\unicdcdaddd Y : {\iota} .  {{{x} \in {Y}}\unicdcdcdhd{{Y} \in {X}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & db4bc1188573af6ee726c91f30668d0d047de9916b17056407fb50b728e30efe \\
Pure Prop Address: & TMF2PbBRuwVtGUAm2dBcakxEFts1b3gfeHi \\
Theory Prop Id: & ab781b05690ff7302616c39024e38d17990dfb88f8dc15950b3d5f47ab0a4324 \\
Theory Prop Address: & TMPGvCnxEDNcLzGEpegCEggB87LUw7GvgQ9
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ffogjgpgogfepfjgngahchfgeg} ${\unicdcdadad X x : {\iota} .  {{{x} \in {{\mname{Union}}~{X}}}\unicdbdjdcd{\unicdcdadad p : {o} .  {{({\unicdcdadad Y : {\iota} .  {{{x} \in {Y}}\unicdbdjdcd{{{Y} \in {X}}\unicdbdjdcd{p}}}})}\unicdbdjdcd{p}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 8efd578687dc029da349c22ca087953113491e4794018f04c73b2c7ae5084bf0 \\
Pure Prop Address: & TMH5ng38evRBjZnMvcn9FJLMLXbDC1Bz9aY \\
Theory Prop Id: & d621b2d16dc72ef52c1fe29162e3508201e053e42f163701b3713472780e9a5e \\
Theory Prop Address: & TMHeeXhX7g1GDga7C7LQdPcR4t9R2vstffp
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ffogjgpgogpffengahehjh} ${{{\mname{Union}}~{\mname{Empty}}}={\mname{Empty}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 2c511ebf784d1ac4263638dde61f03ebe06b666994224125d685445a9af596e3 \\
Pure Prop Address: & TMLm3kKCuXxhm2w4H3avGFTRVMtJZ4TZQPW \\
Theory Prop Id: & 72b1c4f60fbbe561816842cf8d137a012a23b49ea41913fed5ee67e33bbf6c52 \\
Theory Prop Address: & TMMwTUayoXbEd6iFoK2PNm3DAtTEe5cdhtf
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:afpghhfgchje} ${\unicdcdadad X Y : {\iota} .  {{{Y} \subseteq {X}}\unicdbdjdcd{{Y} \in {{\mname{Power}}~{X}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 7143d71ecf102401ab2636034e61d377bec399d276d42b9e418431501853f4c6 \\
Pure Prop Address: & TMYd9dR9ghFpJALxMSh1bifCcoHmd6XFuvA \\
Theory Prop Id: & 3c48d3c62b94e7a41c69deefa90b2e8c771cbc0aa279fcba058fefb98579331d \\
Theory Prop Address: & TMXdAMd1HZUyw6mE1ZFaV71nZ63jBYMLiUj
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:afpghhfgchfe} ${\unicdcdadad X Y : {\iota} .  {{{Y} \in {{\mname{Power}}~{X}}}\unicdbdjdcd{{Y} \subseteq {X}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 149030a919d6402241e63172077fe438016089bfde0e7da4cbc536dc04901bb1 \\
Pure Prop Address: & TMWSJ1X7N37P2Pemk8UyDMfYjkY3zie7nYZ \\
Theory Prop Id: & 6470703fa38f09b9dbdffe7bcefe88a4d4c94d929d7e93c64556a9f00ad14694 \\
Theory Prop Address: & TMTYtQq2xbReLwQoZqj15EvuksZjaG3A9fA
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:afpghhfgchpfdffhcgbh} ${\unicdcdadad X Y : {\iota} .  {{{X} \subseteq {Y}}\unicdbdjdcd{{{\mname{Power}}~{X}} \subseteq {{\mname{Power}}~{Y}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 6d8f173a14a5bbfef48f6ce86bee8512556a0deed405c0bd072d5141d2299af9 \\
Pure Prop Address: & TMUvnczMnpH9X3CybY6TzCw5SCHqkt7ir7u \\
Theory Prop Id: & 9dd5f3b3f3808a5118155ae75d2e1c08c28ea7ba30690f84aae27623efd601dd \\
Theory Prop Address: & TMLB1eXPkLwvDDtkFvqtauiz4FckV2UwQPk
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fengahehjhpfjeogpfafpghhfgch} ${\unicdcdadad X : {\iota} .  {{\mname{Empty}} \in {{\mname{Power}}~{X}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d2656b52d4bf2bab93fe5255f13b797a5512a056ca12c4fb73ccdc10829f6f17 \\
Pure Prop Address: & TMaK4ZHB63mPURsGQ3iXFc6dERVy8jXzgG5 \\
Theory Prop Id: & 487855dcfff4149b1efb5bd9ea0572b18fe9005d660d86fcfc5ff90110ba6df9 \\
Theory Prop Address: & TMa8XHamyspUjhkeiNgAYuj8aecCrFsHqjg
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:dffgmgggpfjeogpfafpghhfgch} ${\unicdcdadad X : {\iota} .  {{X} \in {{\mname{Power}}~{X}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f81ef2a25f07c69ddd40acce90e3caf25609ce25f8183e2509b613cb0092508e \\
Pure Prop Address: & TMQycQfNrWABmzjhJNUDx6UCqmAXeAy1qsv \\
Theory Prop Id: & 8336ff563585b5335f5d748d44c68d6e04e2e671537cfd5537a4b37acde6a25a \\
Theory Prop Address: & TMKY4E4GGAWwCfDftsZmANC17noKbnuCrbo
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ffogjgpgogpfafpghhfgchpfdffhcgbh} ${\unicdcdadad X : {\iota} .  {{{\mname{Union}}~{({{\mname{Power}}~{X}})}} \subseteq {X}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 7f4d2bc5abb24988ada92aecad1eeb9b7e0902f2bf91f6062f31024af17a8bed \\
Pure Prop Address: & TMTgvEtxJEiGcbTTuKLumZaRiNe3WkRbVBG \\
Theory Prop Id: & 1b4311aee3fe38a1eb6d381638c72194c02e1025b68cb8fd7f24d84b4aa8ff10 \\
Theory Prop Address: & TMQdwUwhhyCEESAhoqgTeHBAY85kLo5KAYP
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ihng} ${\unicdcdadad P : {o} .  {{P}\unicdcdcdid{\preoh{{P}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 62e4c3fec424181797ab4ef1d385902e9cdc35c7558a8f861b90f48a494c0e0e \\
Pure Prop Address: & TMKtBvuSXX3aDsty6aeAaXbywwMJa4KhJpC \\
Theory Prop Id: & 7b6737622a32781568aa9679a7eb1928791917e8dbf1a5fea21e2f0cbccee791 \\
Theory Prop Address: & TMMPzhDBTSXgihVRhAwaiREjdQ5Jeotv34y
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:egogfghg} ${\unicdcdadad P : {o} .  {{\preoh{{\preoh{{P}}}}}\unicdbdjdcd{P}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 852f346d61a871c2db340ac4fd7de308d10ae313849575cd39cfac1469b8995e \\
Pure Prop Address: & TMHNYQKxvrS4ZDs2FctrNBCPfYUgZB6RFrx \\
Theory Prop Id: & b7cc631d047502f5a0c47618dc8c76a4947e2224be400faf040b7ef95f7994da \\
Theory Prop Address: & TMRYv1F8fFeWtceTAuu9zbNET7tH5xtFHQn
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jgngahpfogpgehpfpgch} ${\unicdcdadad p q : {o} .  {{({{p}\unicdbdjdcd{q}})}\unicdbdjdcd{{\preoh{{p}}}\unicdcdcdid{q}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a8655639be6ebff69772dc3e37a7cf1414005132611dfae586f7e43fa02f82f9 \\
Pure Prop Address: & TMcvyPAhaTi7kXdf8YYSBsEH4XcVThUkX9L \\
Theory Prop Id: & 30c98c972cfd8712dbdce74f465991aad8aa72159a4511fc01e975a23d063a5c \\
Theory Prop Address: & TMH4ymv2c9JczjQGEQqzDcP9xj2yX1JHHfx
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogpgehpfbgogegpfpgchpfegfgngpgchhgbgog} ${\unicdcdadad p q : {o} .  {{\preoh{{({{p}\unicdcdcdhd{q}})}}}\unicdbdjdcd{{\preoh{{p}}}\unicdcdcdid{\preoh{{q}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 29877a368f94842edeff462e056244efa22376525930141a2d2926e5f3d0ef3b \\
Pure Prop Address: & TMQfs5TGwUrjea616pdTxbLXGNvhBxY4UzL \\
Theory Prop Id: & 63ddfe069e38d4763ee4f112c78b39e12a120ccaa496fd47e6a4646fc9391093 \\
Theory Prop Address: & TMaCC7RwYa5bssu9qewCUzTz5xikj6JohLz
\end{tabular}
\end{center}

\end{theorem}

\section{Exactly 1 of 2}
\begin{definition}\label{def:fgihbgdgehmgjhbdpgggcd}
$\mname{exactly1of2}$ is the opaque object of type ${{o}\unicdbdjdcd{{o}\unicdbdjdcd{o}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 163602f90de012a7426ee39176523ca58bc964ccde619b652cb448bd678f7e21 \\
Pure Object Address: & TMS9Bz8WFNT8hbFokWDmzwFmNr2ZD7CfP2e \\
Theory Object Id: & a0b94402d8edc93e77f0dd488bd6709a5ab850b3f07e42bedc0d1e40163aec06 \\
Theory Object Address: & TMEqbBVsvC394VsHqRdcJB6GggoMgLnuS6A
\end{tabular}
\end{center}

\end{definition}
\begin{theorem}\label{thm:fgihbgdgehmgjhbdpgggcdpfjebd} ${\unicdcdadad A B : {o} .  {{A}\unicdbdjdcd{{\preoh{{B}}}\unicdbdjdcd{{{\mname{exactly1of2}}~{A}}~{B}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 8e1e4515e8d2e1265d837e207a0eaa000d82c55e2fa708c4ebd9ad229b5a5d38 \\
Pure Prop Address: & TMQnjH6acMFmZdz797stCauUdrSebKX7Mev \\
Theory Prop Id: & 4f94fafdd5f7f8d4dc0f3e1b7277b17a0c7c19add3a6af231254dcedab30fe39 \\
Theory Prop Address: & TMJL9YXWiTdUUzhvi5WWHy9wvvoebH1tQzv
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihbgdgehmgjhbdpgggcdpfjecd} ${\unicdcdadad A B : {o} .  {{\preoh{{A}}}\unicdbdjdcd{{B}\unicdbdjdcd{{{\mname{exactly1of2}}~{A}}~{B}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & c9fd90a0917801b2b7fae79f83bdc259f931342830e8158acece4f3c1a283659 \\
Pure Prop Address: & TMMAKooscST9mjX4iuDPzg3FY58bpufyfVU \\
Theory Prop Id: & 6c1ad919f0b4255c719d573f707feb239d05426a99ece78b2f738ef43e3e1a51 \\
Theory Prop Address: & TML5oMK64kBLn2JLS7ATshVeqCgaCsuNK6e
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihbgdgehmgjhbdpgggcdpfjgngahjebd} ${\unicdcdadad A B : {o} .  {{({{A}\unicdbdjdcd{\preoh{{B}}}})}\unicdbdjdcd{{({{\preoh{{A}}}\unicdbdjdcd{B}})}\unicdbdjdcd{{{\mname{exactly1of2}}~{A}}~{B}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 51838fa63f26d38944c5e35f2413ef312130a04668affc103545649e6845b841 \\
Pure Prop Address: & TMRhwQ9VVpjkPMMkpzHArgyLqFJ2sLxakNb \\
Theory Prop Id: & 517be2b6e298510b19ae2a4576b522c9cc8fe9bf89dfa1630bc8b79219852955 \\
Theory Prop Address: & TMcoNtefvy7eJpxYPtwBmyQuGKfMJ9PMpkn
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihbgdgehmgjhbdpgggcdpfjgngahjecd} ${\unicdcdadad A B : {o} .  {{({{B}\unicdbdjdcd{\preoh{{A}}}})}\unicdbdjdcd{{({{\preoh{{B}}}\unicdbdjdcd{A}})}\unicdbdjdcd{{{\mname{exactly1of2}}~{A}}~{B}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f32aab556c283c02cca82ae1401040f6003bf6a1ac60788c12ad6329d832a293 \\
Pure Prop Address: & TMSY4dBSVErbAWxEf4c743PqBZ9EABV3BJY \\
Theory Prop Id: & 811f013a6ac0abc6e0c8f752b4c6fbd661919f540a84f0f8b6fc99dd0d22aa07 \\
Theory Prop Address: & TMGJHhrbg2Ea8nrQBjPv3SdM2aoAj4dxq8y
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihbgdgehmgjhbdpgggcdpffe} ${\unicdcdadad A B : {o} .  {{{{\mname{exactly1of2}}~{A}}~{B}}\unicdbdjdcd{\unicdcdadad p : {o} .  {{({{A}\unicdbdjdcd{{\preoh{{B}}}\unicdbdjdcd{p}}})}\unicdbdjdcd{{({{\preoh{{A}}}\unicdbdjdcd{{B}\unicdbdjdcd{p}}})}\unicdbdjdcd{p}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 29b901ba4db12851de74e31368539f6d1cc25bbc1c301edaa62335d7e6c17545 \\
Pure Prop Address: & TMRCeD4ey2b4rXZn7HkMnX7YburjvMK1Eyg \\
Theory Prop Id: & c674348923fa7045ff80c55a4bb504730f6f8ee0dcdf90e8c71d35291ea85112 \\
Theory Prop Address: & TMJHeaLcDFsg71BZKr8vRobyqEDxdcim8fW
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihbgdgehmgjhbdpgggcdpfpgch} ${\unicdcdadad A B : {o} .  {{{{\mname{exactly1of2}}~{A}}~{B}}\unicdbdjdcd{{A}\unicdcdcdid{B}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 18af7395e3694a283ae114ccec2d06247033786f17700e124d0fd73c83572675 \\
Pure Prop Address: & TMLi8xLyPBxTfc12noiHmSmqavSb4tpNQeQ \\
Theory Prop Id: & e092f672ff0d584cbaf46120347c86b03fbcec240a9d5100380e8240373fd2be \\
Theory Prop Address: & TMXLeWxQ5A2VGtDdKgtMuBn5HCa3VzxF1pb
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihbgdgehmgjhbdpgggcdpfjgngahogbdcd} ${\unicdcdadad A B : {o} .  {{{{\mname{exactly1of2}}~{A}}~{B}}\unicdbdjdcd{{A}\unicdbdjdcd{\preoh{{B}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d3009840b3d85b74b9e0a9620f4308a8e1436d22cdd2a69e83dd3c46c1487323 \\
Pure Prop Address: & TMWzgfM5wbPGyJhNsxsijwiYzmX4TthmdKH \\
Theory Prop Id: & ffdec3681a2e06d83ddcbdc151520cfe5b3b623d2db529d7a849209f1d6fe7cc \\
Theory Prop Address: & TMG66wx9tzCkMhQc9NRiUxq74peErmdEviC
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihbgdgehmgjhbdpgggcdpfjgngahogcdbd} ${\unicdcdadad A B : {o} .  {{{{\mname{exactly1of2}}~{A}}~{B}}\unicdbdjdcd{{B}\unicdbdjdcd{\preoh{{A}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 29929fd4030494b67c9eeeaa7dc35578573efb328bcafaf20f5efb6ad854e87b \\
Pure Prop Address: & TMJz2j2BW2BvWFzAm664pFqbVtvTqWXzGq7 \\
Theory Prop Id: & 7499d10110c69f4c2d84763d224e28a23a5525fa48cfc823789b09051b07db66 \\
Theory Prop Address: & TMPjFxrRCRMeS8z17aDuupoUhLQX4Kodx6A
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihbgdgehmgjhbdpgggcdpfogjgngahbdcd} ${\unicdcdadad A B : {o} .  {{{{\mname{exactly1of2}}~{A}}~{B}}\unicdbdjdcd{{\preoh{{A}}}\unicdbdjdcd{B}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0fb71ab4a166db8b8a5493187a1623cb2573bdafdb80c215e1df61d68b8fa34b \\
Pure Prop Address: & TMYo2ThWofRLhEMmrLih7wWsVmnmor928bi \\
Theory Prop Id: & d000b6d72c072278302ade061ba0e7a3735507b341fa9f3cb4b8ea13a683c623 \\
Theory Prop Address: & TMdXoSSvPrdQxAK2M2kCdSMvu74LozCHPWp
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihbgdgehmgjhbdpgggcdpfogjgngahcdbd} ${\unicdcdadad A B : {o} .  {{{{\mname{exactly1of2}}~{A}}~{B}}\unicdbdjdcd{{\preoh{{B}}}\unicdbdjdcd{A}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0ef7cfe1ed1435414acfd763fb0f561715bba0ebfee6abe5163770fb6289d861 \\
Pure Prop Address: & TMdxUZ8ab8VgywY6cY6h1Q7GH65rTvgRbZM \\
Theory Prop Id: & bced87455f1dbd71dca4499cef836fc13af9c4cd9d900b0e299d0289a36ec08d \\
Theory Prop Address: & TMXMKQXQCPoboD5XPkTZaaJc8c6rPbjnF7n
\end{tabular}
\end{center}

\end{theorem}
\section{Exactly 1 of 3}
\begin{definition}\label{def:fgihbgdgehmgjhbdpgggdd}
$\mname{exactly1of3}$ is the opaque object of type ${{o}\unicdbdjdcd{{o}\unicdbdjdcd{{o}\unicdbdjdcd{o}}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & aa4bcd059b9a4c99635877362627f7d5998ee755c58679934cc62913f8ef06e0 \\
Pure Object Address: & TMKyEfBd2FYAx6zajz2sxvYYYXLUo86oiwP \\
Theory Object Id: & c2eb06c534871c653d9f25994d6e8a39d134bed3c7ab7fe19a4f2ecc1eaa1c9c \\
Theory Object Address: & TMVfRiAA5KRi6JvZP4W3VJUw9mtsQVKMdhf
\end{tabular}
\end{center}

\end{definition}
\begin{theorem}\label{thm:fgihbgdgehmgjhbdpgggddpfjebd} ${\unicdcdadad A B C : {o} .  {{A}\unicdbdjdcd{{\preoh{{B}}}\unicdbdjdcd{{\preoh{{C}}}\unicdbdjdcd{{{{\mname{exactly1of3}}~{A}}~{B}}~{C}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 1310b63ae562af7333aee9625e0aa6979394ff104503c204c828d7b627b814d9 \\
Pure Prop Address: & TMcMEtNxcD358TggS5kHahcWnA74uxTqbqr \\
Theory Prop Id: & b7468ae93994040f6662cbfbfdfebbcd1b25bb59711010960cc711c9538dfac3 \\
Theory Prop Address: & TMYCtwze3JZKavf143XCtrbzsmDzM8qK318
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihbgdgehmgjhbdpgggddpfjecd} ${\unicdcdadad A B C : {o} .  {{\preoh{{A}}}\unicdbdjdcd{{B}\unicdbdjdcd{{\preoh{{C}}}\unicdbdjdcd{{{{\mname{exactly1of3}}~{A}}~{B}}~{C}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 00b5b6f76b51f729be0782aed25cf933b24c8784fde8d05bdc69f9b47b28a170 \\
Pure Prop Address: & TMbGNDSr1GGAFnxH4SmSg37nzwWa3ctnxUP \\
Theory Prop Id: & 9660f910a33194ba73b4fbc257bf1c9c423ef83597391b5889dfe8f6a38be5cb \\
Theory Prop Address: & TMXqa8cMXntrgJc53wodmauXTvXn3M1bkAY
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihbgdgehmgjhbdpgggddpfjedd} ${\unicdcdadad A B C : {o} .  {{\preoh{{A}}}\unicdbdjdcd{{\preoh{{B}}}\unicdbdjdcd{{C}\unicdbdjdcd{{{{\mname{exactly1of3}}~{A}}~{B}}~{C}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & fb6319ee090e002b279304bb4d2ec36b0740f58ea070dd36a44eed28f3b20035 \\
Pure Prop Address: & TMUH4ZTnmgc4sLH4v3sQNX3n4SQUyCZmnRE \\
Theory Prop Id: & 98b137b027f483863b18f8083c21acbebd5fb61bcf6f96cf6dbd18c4e987f7fe \\
Theory Prop Address: & TMR4EdHrWcDi4aPaboYPdGxLPTj5h4zc5Jb
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihbgdgehmgjhbdpgggddpfjgngahjebd} $${\unicdcdadad A B C : {o} .  {{({{A}\unicdbdjdcd{\preoh{{B}}}})}\unicdbdjdcd{{({{A}\unicdbdjdcd{\preoh{{C}}}})}\unicdbdjdcd{{({{B}\unicdbdjdcd{\preoh{{C}}}})}\unicdbdjdcd{{({{\preoh{{A}}}\unicdbdjdcd{{B}\unicdcdcdid{C}}})}\unicdbdjdcd{{{{\mname{exactly1of3}}~{A}}~{B}}~{C}}}}}}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & ad228087f6c62536f8e84aa14c71244af2a1324cab874e74e539fce731299438 \\
Pure Prop Address: & TMTheuMKMYKhVdkDXgyaffeAMHxELJkUktD \\
Theory Prop Id: & 83079842b76616f048df954d49c762e5ac75af2a19adeb1da721b43ed57eb0bf \\
Theory Prop Address: & TMREFPJ1oU8sqtHxNQZq9p3RdA4ch42V8qu
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihbgdgehmgjhbdpgggddpfjgngahjecd} $${\unicdcdadad A B C : {o} .  {{({{B}\unicdbdjdcd{\preoh{{A}}}})}\unicdbdjdcd{{({{B}\unicdbdjdcd{\preoh{{C}}}})}\unicdbdjdcd{{({{A}\unicdbdjdcd{\preoh{{C}}}})}\unicdbdjdcd{{({{\preoh{{B}}}\unicdbdjdcd{{A}\unicdcdcdid{C}}})}\unicdbdjdcd{{{{\mname{exactly1of3}}~{A}}~{B}}~{C}}}}}}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 92d78d63c2f16429dfa172220b50c32bf70c813aefa4c1fbfc82982a1db5b261 \\
Pure Prop Address: & TMPq35SCVMNKL4cFiGZvRwpmRBR7XyHk3FM \\
Theory Prop Id: & e9f574b7e9b23c6e5e976545161fe61fed9af69c6425e8992913d0188d809d95 \\
Theory Prop Address: & TMFXVhkyu6LNHsoHcGv18AE41FHiuVDFocM
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihbgdgehmgjhbdpgggddpfjgngahjedd} $${\unicdcdadad A B C : {o} .  {{({{C}\unicdbdjdcd{\preoh{{A}}}})}\unicdbdjdcd{{({{C}\unicdbdjdcd{\preoh{{B}}}})}\unicdbdjdcd{{({{A}\unicdbdjdcd{\preoh{{B}}}})}\unicdbdjdcd{{({{\preoh{{A}}}\unicdbdjdcd{B}})}\unicdbdjdcd{{{{\mname{exactly1of3}}~{A}}~{B}}~{C}}}}}}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 80acac2dac94c4ea11d970424ef6748ca187d4a2d65bb70dd89cbb140688d23c \\
Pure Prop Address: & TMXWj2i7Ck9NwC1rdBpeVZCnufshBHrocD1 \\
Theory Prop Id: & 78f24ba81b345b2c6ab858eba1eb4f9a5b836a0669931ce7c85b99e2a517410e \\
Theory Prop Address: & TMPZhiykV6QMjsj1rdDoZ3FEXBoTtzSGsW1
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihbgdgehmgjhbdpgggddpffe}
$$
\begin{array}{c}
\unicdcdadad A B C : {o} .  {{{{\mname{exactly1of3}}~{A}}~{B}}~{C}}\unicdbdjdcd\\
{\unicdcdadad p : {o} .  {{({{A}\unicdbdjdcd{{\preoh{{B}}}\unicdbdjdcd{{\preoh{{C}}}\unicdbdjdcd{p}}}})}\unicdbdjdcd{{({{\preoh{{A}}}\unicdbdjdcd{{B}\unicdbdjdcd{{\preoh{{C}}}\unicdbdjdcd{p}}}})}\unicdbdjdcd{{({{\preoh{{A}}}\unicdbdjdcd{{\preoh{{B}}}\unicdbdjdcd{{C}\unicdbdjdcd{p}}}})}\unicdbdjdcd{p}}}}}.
\end{array}
$$
The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 9abcef9e10449a86443719e4eccde7cc0122aea0cdd87559e72070b5056c68a3 \\
Pure Prop Address: & TMSs9kYqUVNU4be4UnVpebwjefQ88pwnfPh \\
Theory Prop Id: & f4999a084ffdbda508b13e281a016002d1099fdaf2727b624c9a352ff505061e \\
Theory Prop Address: & TMRGu2Bkor4inX6t54rtKgCqaA85yMnm4Fn
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihbgdgehmgjhbdpgggddpfpgch} ${\unicdcdadad A B C : {o} .  {{{{{\mname{exactly1of3}}~{A}}~{B}}~{C}}\unicdbdjdcd{{{A}\unicdcdcdid{B}}\unicdcdcdid{C}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & b9e1330f726a56d262ecb418f9a9f2892f85275d460094e7c8f3b8a38518f227 \\
Pure Prop Address: & TMLoZZfbmUJwXoBoU6BXeji1WYei2vbwgjy \\
Theory Prop Id: & 46638186a29363d865020e0cf0a5e9f76ca956ed7c669bee7f98f4d7fd242530 \\
Theory Prop Address: & TMLUgggjEPAVsx7wBkaGiLQy8AdUeXJZWjM
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihbgdgehmgjhbdpgggddpfjgngahogbdcd} ${\unicdcdadad A B C : {o} .  {{{{{\mname{exactly1of3}}~{A}}~{B}}~{C}}\unicdbdjdcd{{A}\unicdbdjdcd{\preoh{{B}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & aa5009ff9a11492e840f32443e73a771ca267d22293893156f1d4deb4aaab2be \\
Pure Prop Address: & TMYv5ButtzZjAKGh8ZS12xVuGTD6YJQcH2b \\
Theory Prop Id: & ddde3fa5accd00c57075aa8e16e5ddd6096787e97651a7d00fe4c06313bd25e5 \\
Theory Prop Address: & TMEsRotLbeZwM4Vb8CEFrHUrjwZobtVbQmC
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihbgdgehmgjhbdpgggddpfjgngahogbddd} ${\unicdcdadad A B C : {o} .  {{{{{\mname{exactly1of3}}~{A}}~{B}}~{C}}\unicdbdjdcd{{A}\unicdbdjdcd{\preoh{{C}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 610826600590b2f8df19bcab4fe7ab0aaf66cf995d6f68f1d9ef9fd3139ef3b3 \\
Pure Prop Address: & TMadDers8VBnavfoVVcRpPTxDYWgEMaqYaA \\
Theory Prop Id: & 829d4d5e39a13c5555db82570159451aaf7dedfe2b643ebc2c21720e8128ade4 \\
Theory Prop Address: & TMKWE5kXYcypJ3VwhHAfwnUZ524Pbhidn2h
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihbgdgehmgjhbdpgggddpfjgngahogcdbd} ${\unicdcdadad A B C : {o} .  {{{{{\mname{exactly1of3}}~{A}}~{B}}~{C}}\unicdbdjdcd{{B}\unicdbdjdcd{\preoh{{A}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 1d346d501d1ba647921c3025a1335977b63c27a8a61bd46533fcfc6ba14b2d81 \\
Pure Prop Address: & TMMzqWU52BqgHAJK8WaH7Z9CCq7JwxqJcP4 \\
Theory Prop Id: & 397117cbef66df36202b151aefd2ddef44318f936aabf85d3a81c5b6185a89a7 \\
Theory Prop Address: & TMRitWJaC1PAk8gRhTEJE7Eoz2VanS86r9f
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihbgdgehmgjhbdpgggddpfjgngahogcddd} ${\unicdcdadad A B C : {o} .  {{{{{\mname{exactly1of3}}~{A}}~{B}}~{C}}\unicdbdjdcd{{B}\unicdbdjdcd{\preoh{{C}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & e61d04bf5bbf41805809956d45bdde949bb6e8b00f4defdce071649f26b9bd42 \\
Pure Prop Address: & TMXB6Z3uL2sQmzDCqC3abT4uqUmke5iLtk6 \\
Theory Prop Id: & a5f7c26af5306214a6ff6a38a92231f9ad04f3095b211b4147ed6e6fa1272d23 \\
Theory Prop Address: & TMSaFCqhniFsaMDK85YeQmyVxVZbpNzbFHt
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihbgdgehmgjhbdpgggddpfjgngahogddbd} ${\unicdcdadad A B C : {o} .  {{{{{\mname{exactly1of3}}~{A}}~{B}}~{C}}\unicdbdjdcd{{C}\unicdbdjdcd{\preoh{{A}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & fca5376e31e8f8fc2e5c6f166569ff186415ff18941d23f3f6f029f569148dd7 \\
Pure Prop Address: & TMFM62rQpPoQyXj5ji7YpQmUU3nG3SpUV6h \\
Theory Prop Id: & 35250014509cb9f52a6cd6ac464fff7cd4df30035a9ea5b3c48aaedd2b42946b \\
Theory Prop Address: & TMTbHqaT1XHTxp9kCkBgrphFzfDCg9TtuTi
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihbgdgehmgjhbdpgggddpfjgngahogddcd} ${\unicdcdadad A B C : {o} .  {{{{{\mname{exactly1of3}}~{A}}~{B}}~{C}}\unicdbdjdcd{{C}\unicdbdjdcd{\preoh{{B}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & b27fbaab4bdf4912ad94528a90059e4fe9b1aa06f9c87ceed32c02a2c49b5dc5 \\
Pure Prop Address: & TMN18VWDLkauUPx1tHnX2hvXJFtMx1JohBA \\
Theory Prop Id: & fd95f6b42e5f234c90b8218b2e2ebe7858c531af928f420deb984c1f39e731d6 \\
Theory Prop Address: & TMY9goAmFbnGXqWRMRHhrFiULnAUs9A1FYY
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihbgdgehmgjhbdpgggddpfogjgngahbd} ${\unicdcdadad A B C : {o} .  {{{{{\mname{exactly1of3}}~{A}}~{B}}~{C}}\unicdbdjdcd{{\preoh{{A}}}\unicdbdjdcd{{B}\unicdcdcdid{C}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 6f09b4a396feb709ceb93d0a17d24519b1d958895abedbaba2715b65b7e7584e \\
Pure Prop Address: & TMJM8ao3vrQPrWM5rgtqDZ9GARGusrQ5wm3 \\
Theory Prop Id: & 21dd5ba0fc3af8a67d61c902bc798489c825a4490a81e54581755b00b24c8b73 \\
Theory Prop Address: & TMQ1J7pdfn7NmxfAzvuJMKcSZ7sdKVx5yff
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihbgdgehmgjhbdpgggddpfogjgngahcd} ${\unicdcdadad A B C : {o} .  {{{{{\mname{exactly1of3}}~{A}}~{B}}~{C}}\unicdbdjdcd{{\preoh{{B}}}\unicdbdjdcd{{A}\unicdcdcdid{C}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f93f16a2acab0e2c70aaa6ba0f16c5f8fae767769ebf1191ccb689aae347f908 \\
Pure Prop Address: & TMan3tfnxxCb6QyS1xebfjHrUsCXBfkbrta \\
Theory Prop Id: & 0a20f6a1f5ec9ea9dc84d10e81affaaeca954a6fb32ae14805896ac1d06bfb30 \\
Theory Prop Address: & TMTyG7NfHu1i8TzsieyTpERQxhdGXmw7o4P
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgihbgdgehmgjhbdpgggddpfogjgngahdd} ${\unicdcdadad A B C : {o} .  {{{{{\mname{exactly1of3}}~{A}}~{B}}~{C}}\unicdbdjdcd{{\preoh{{C}}}\unicdbdjdcd{{A}\unicdcdcdid{B}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 6e599c436e1c33f48b986f575992a80e57b99534e289fc843916f91e1d1a347d \\
Pure Prop Address: & TMbF9MFUNWCLgbMpnwTvAAwrKRm9QfXyEba \\
Theory Prop Id: & d19918a97b442e1a1f214592d4b8db4cdda02c3fe87acf67f5a1951ba2cab40a \\
Theory Prop Address: & TMaKsz23V9zHBq8Nc44i1QWCrQiM7XnB9N3
\end{tabular}
\end{center}

\section{More Basic Results}

\end{theorem}
\begin{theorem}\label{thm:cffgahmgje} ${\unicdcdadad A : {\iota} .  {\unicdcdadad F : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad x : {\iota} .  {{{x} \in {A}}\unicdbdjdcd{{{F}~{x}} \in {\{{{F}~{x}}|x \in {A}\}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & b146c5f4439d8676c0dccf44c83e811ebb81f9038983f510c8607ddc1eb34420 \\
Pure Prop Address: & TMP2e3huiS7VJFLqC2ppXhrjDJ2bUGLJV5e \\
Theory Prop Id: & f84982ee3b076ecba0e4ff60abdc2f37c622ad1afac9429103f323e4cdfe3e19 \\
Theory Prop Address: & TMHGmtrvwBUQsPubrpbb6tLvjthQVG8iwCD
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:cffgahmgfe} ${\unicdcdadad A : {\iota} .  {\unicdcdadad F : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad y : {\iota} .  {{{y} \in {\{{{F}~{x}}|x \in {A}\}}}\unicdbdjdcd{\unicdcdaddd x \in {A} .  {{y}={{F}~{x}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 311cdfe6686cf4d3ef41da3e91d25bb9180eb27a0f3a38739e52ece413817da1 \\
Pure Prop Address: & TMU6c8sDinZc5CK9bdAsnrw7LPnQPhim3R3 \\
Theory Prop Id: & d07e78df51e6c40a1fb15182455062bac21a7cd73536d47d7e4aeba8426d8f70 \\
Theory Prop Address: & TMdxK4ZQijyUW6813F1x5brcPHDKGCWdQpm
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:cffgahmgfepfjgngahchfgeg} ${\unicdcdadad A : {\iota} .  {\unicdcdadad F : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad y : {\iota} .  {{{y} \in {\{{{F}~{x}}|x \in {A}\}}}\unicdbdjdcd{\unicdcdadad p : {o} .  {{({\unicdcdadad x : {\iota} .  {{{x} \in {A}}\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: & 31e90a1cfe1339b3fdd723ef9c177dda85e4f3f565d6cd3cfb4f371ac4c304f8 \\
Pure Prop Address: & TMFAa4xtcBS2jBu91NQ7stWLB3d3RE3qzYR \\
Theory Prop Id: & 34fefdfa28cb805cd6e029487d3c32cc301dc5cfe9635fa1b9dded4506aca32e \\
Theory Prop Address: & TMJVpXF9QNoP2mDr6CyNe7oNaDmpm2R1zMb
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:cffgahmgpffengahehjh} ${\unicdcdadad F : {{\iota}\unicdbdjdcd{\iota}} .  {{\{{{F}~{x}}|x \in {\mname{Empty}}\}}={\mname{Empty}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 2af2ac513652a1800583c65d812613479314c35762cfa051dd456a4370470c27 \\
Pure Prop Address: & TMNTKJzUTMuevhemTED7aYZL43yxKSfLyaw \\
Theory Prop Id: & 0835bc06e82fa4c2e4d9eb7e519d643457109db965d61841af4879944ee45344 \\
Theory Prop Address: & TMdRuwDbtmFquZoGEj4pWkc2saYwQmcLziT
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:cffgahmgfebhpffgihehpfdhfhcg} ${\unicdcdadad X .  {\unicdcdadad F G : {{\iota}\unicdbdjdcd{\iota}} .  {{({\unicdcdadad x \in {X} .  {{{F}~{x}}={{G}~{x}}}})}\unicdbdjdcd{{\{{{F}~{x}}|x \in {X}\}} \subseteq {\{{{G}~{x}}|x \in {X}\}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & eb4c1d386f80c2ee581f2c1069f67f723e405c7993ee30a79f8bbd10d84d9ca3 \\
Pure Prop Address: & TMcq6sFfV1su5tjWvGTgkj2EP4oNFAVRcup \\
Theory Prop Id: & 56aad0710a7b30d465d2dbe0bd8d3c290b9f836ccb5a6fa4519911a80b05626a \\
Theory Prop Address: & TMZZYGkpW7fMLbAob3MNpFsZFKRvPdWXvXH
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:cffgahmgfebhpffgiheh} ${\unicdcdadad X .  {\unicdcdadad F G : {{\iota}\unicdbdjdcd{\iota}} .  {{({\unicdcdadad x \in {X} .  {{{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}

\section{If-then-else on Sets}

\begin{definition}\label{def:jeggpfjg}
$\mname{If\_i}$ is the opaque object of type ${{o}\unicdbdjdcd{{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & b8ff52f838d0ff97beb955ee0b26fad79602e1529f8a2854bda0ecd4193a8a3c \\
Pure Object Address: & TMFXposu1uQxEse8ZSjwvaRFgnCw5z9YTK6 \\
Theory Object Id: & 76c4c0ead9836400beb62a9590f920012eeb5b529d51bc098f0a4540dd3492bf \\
Theory Object Address: & TMTZcwmiXZdp3zV8ehxEX8eEg2jwH6B4gXM
\end{tabular}
\end{center}

\end{definition}
{\bf{Notation.}} We write $\mif{p}{x}{y}$ for $\mname{If\_i}~p~x~y$.

\begin{theorem}\label{thm:jeggpfjgpfdgpgchchfgdgeh} ${\unicdcdadad p : {o} .  {\unicdcdadad x y : {\iota} .  {{{p}\unicdcdcdhd{{({\mif{{p}}{{x}}{{y}}})}={x}}}\unicdcdcdid{{\preoh{{p}}}\unicdcdcdhd{{({\mif{{p}}{{x}}{{y}}})}={y}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 2a17ae8615c55763933cbf62cfdea60aab440ec5370b1a166e5a90b2dbbdaa33 \\
Pure Prop Address: & TMYAPcTTzBuQuezPwJWXPnQTtHjtuAmrh3a \\
Theory Prop Id: & b5c26bc5c00a1fae5b9eb6e6e2dddacab303e5c17f31736c985646e26d160188 \\
Theory Prop Address: & TMSSvVBAsGTpqvzGHpFj5YS4oCq5oKaLmoJ
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeggpfjgpfad} ${\unicdcdadad p : {o} .  {\unicdcdadad x y : {\iota} .  {{\preoh{{p}}}\unicdbdjdcd{{({\mif{{p}}{{x}}{{y}}})}={y}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & fde1a8047aea787315fd3c48c3bf4b8dcf677b9f13975abdc0cf25a46bd38dbe \\
Pure Prop Address: & TMS3vZha9dDF2eKGvMvTFmh9tT8CjUJYmHN \\
Theory Prop Id: & a9abd320bb96a93c0bfd6f8cd02d5a4b36f1c06bc80d8a0d61d8f7f21e978b60 \\
Theory Prop Address: & TMXimAMUQhCm2DKHwaiTu61r3YFoxo2t7aF
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeggpfjgpfbd} ${\unicdcdadad p : {o} .  {\unicdcdadad x y : {\iota} .  {{p}\unicdbdjdcd{{({\mif{{p}}{{x}}{{y}}})}={x}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & b1aa3ff40ccd3b5e52ea574b197c5921dcbf1d479f4fc972636f9a536dc4c6c7 \\
Pure Prop Address: & TMG6G29dgsYC3Bvq1bUdKCsiS18QXwMmERv \\
Theory Prop Id: & a93c2c61afa1f7d589c4078389126876aa054a9fb356be52dbf9a1ee994afe29 \\
Theory Prop Address: & TMLX1L6KQv9yGQm2cqdp146LHmN8xmhBiSp
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeggpfjgpfpgch} ${\unicdcdadad p : {o} .  {\unicdcdadad x y : {\iota} .  {{{({\mif{{p}}{{x}}{{y}}})}={x}}\unicdcdcdid{{({\mif{{p}}{{x}}{{y}}})}={y}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 3e14398be827f1c6e32094ea4dc2734502882cbca27eddafe5dce31ef4356336 \\
Pure Prop Address: & TMVLUMbzPPFhysrpDbLFxMCLeFJ1VVL1jZC \\
Theory Prop Id: & 4de742c8e4700f7927be7ee9ab705ba6fd76b46b20d1ba83576b15b076f51a7e \\
Theory Prop Address: & TMRFxe5VNckUFijgfvt4yKBVqJJFGDGD9Un
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeggpfjgpffgehbg} ${\unicdcdadad p : {o} .  {\unicdcdadad x : {\iota} .  {{({\mif{{p}}{{x}}{{x}}})}={x}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & c790ef8c8cbc1d8b8baccef44b4431f462ec3f875068c16063b3f8e4f9606c96 \\
Pure Prop Address: & TMEsYnnoa7TBfEDReC6dhETQtLYNdEGfVEm \\
Theory Prop Id: & e413bd92fbd8dffea8c40f40fa4c82bd8732a0d4a82572f9264e5767a06a8ade \\
Theory Prop Address: & TMTiR3dSMwWpEh2ReAKGGJZjp5K2AjJ4xrH
\end{tabular}
\end{center}

\end{theorem}


