\chapter{More Logical Properties}
\begin{theorem}\label{thm:fgbhpfjgngahpfpgch} ${{({\uniddcgcg x y : {o} .  {({{x}\unicdbdjdcd{y}})}})}={({\uniddcgcg x y : {o} .  {({{\preoh{{x}}}\unicdcdcdid{y}})}})}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 06c3093aa740f38323ae4d7f0dbad8d508f40a0ca90fa41e9f01516651c3e3c1 \\
Pure Prop Address: & TMFQ6hVxLyhKxQEQs23Xv9LC6mgW4iwwgrX \\
Theory Prop Id: & 4c9dc0935ef80cbfc0fc55cf8abb066203b42c66e60c4bb6af8b939a9f3dba5a \\
Theory Prop Address: & TMRjkjWby7U8Aw7kefWq3i3PMiD7ahDD43F
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ggbgngfhogjgpgogpffengahehjh} ${\unicdcdadad F : {{\iota}\unicdbdjdcd{\iota}} .  {{({\unicdcddedd _{x \in {0}}{{F}~{x}}})}={0}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & fc1bdd286f0d898d898c29f18fbe095090efb65893028ab68d5f98d8caa05ce9 \\
Pure Prop Address: & TMZjHxMN3FYwok47JsaP7dDQjKXS6jyzcQx \\
Theory Prop Id: & 22bd10cff6495d6e03e6e76619e1426110cc714a9d78d666213a9e4d3b7897b2 \\
Theory Prop Address: & TMTAVVZK8aANakE2V9u1NoVueYVDuUeiPWu
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fengahehjhpfpgchpffgih} ${\unicdcdadad X : {\iota} .  {{{X}={\mname{Empty}}}\unicdcdcdid{\unicdcdaddd x : {\iota} .  {{x} \in {X}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & ea40ae60ad1226481a72c72991900ab1d75eaab2f2603b30f4021ec9bfa53243 \\
Pure Prop Address: & TMN7F3M7BEyv9u1wysCYB4eCnjR17p8fFPJ \\
Theory Prop Id: & 16587d445d1c65fd759cdc12b7fec9089c4b514284913be85bb2bfbaa6fe4f57 \\
Theory Prop Address: & TMGoeYYeEjatMCpA5EmBZSLRbtsqeYFpDcB
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogjeogpfadpfad} ${{0}\unicdcdadjd{0}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 09a099717c75645aead366c3b2036df70c9289907d2755e106f75199e5674813 \\
Pure Prop Address: & TMMk6er7mxLyAi5T6t3WpKRXJCMS7xBHwqu \\
Theory Prop Id: & 865a398e739b1785dc276dbe8cd4ed7fb4f1d8782c59e0b8e3b09c70fd4034c3 \\
Theory Prop Address: & TMSwDSAjn1RkA5QxqBbEUmy3yKyr57g6mWj
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogjeogpfbdpfad} ${{1}\unicdcdadjd{0}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & b197676023d2efaa19e70e356beb7444d5240c7348ab140126a015307c650d50 \\
Pure Prop Address: & TMavi1ZRdgBBbDLvwBQchihXtPKTjnNdhsk \\
Theory Prop Id: & 2fd3e19cdd9862468dc112216fa972acca941b4de769d35cc59d7ec1577cf0e0 \\
Theory Prop Address: & TMdqjwWDUF4ntu7oqJ4gg8mEYbpw158A4BJ
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogjeogpfcdpfad} ${{2}\unicdcdadjd{0}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 135dfc520ebfeb7876e0ee1477daff54f352c678350712bc7747990b981da558 \\
Pure Prop Address: & TMXsBVAtddQ17BGoDpSMPvxAsXgE6R4Qm3B \\
Theory Prop Id: & 556f07538b44668c0a147b4fc3e95e1df80a4f96ee895c6106b88cb0beddabcf \\
Theory Prop Address: & TMZ7o2p95PaehpRzBsCsB83NrmH4JcRBHJN
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogjeogpfbdpfbd} ${{1}\unicdcdadjd{1}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & e668f88d6e9498b6de122df37d7c3f2dc02798e0ebb033a625b6e3b40d880a0d \\
Pure Prop Address: & TMLzAqBPo85Hx5GYyr7xuu18NVjreNUyRSj \\
Theory Prop Id: & 7774094463b5d0735559a4bab3714251e4442b5e3727856df52e3ae54b23c64e \\
Theory Prop Address: & TMUrdNWeTXSbGVqA84DoNZn9BGLr6upydqx
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogjeogpfcdpfcd} ${{2}\unicdcdadjd{2}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 31c298db536bab1cc362a2d791118533b2cff78953407ece1ed3125867a3beb4 \\
Pure Prop Address: & TMXFjntzEU8n1QS25SjFvEdpbj6sq7qbV7d \\
Theory Prop Id: & 94398399c4d60eec85399c9cc75054c87b16f94488166ce079063afe25b9d45a \\
Theory Prop Address: & TML9u9hUZHGL9ztWF6S5eMPgi1WMRevw1sY
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:dffhcgbhpfadpfad} ${{0} \subseteq {0}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & e9749df5528d6c773cdda6fe3121311c07ae4197f8e3b399882f384c8541d735 \\
Pure Prop Address: & TMLX5CPCFVK66pFehnmXXgUmMn3P7noB8s2 \\
Theory Prop Id: & 6e655c00e783ba0a41d0029eaa2f71c798229b93c15f02483aafd5566f0a81f7 \\
Theory Prop Address: & TMLxnx5doMjojfharrvSwqG5tst7XcCPdHE
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:dffhcgbhpfadpfbd} ${{0} \subseteq {1}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & cad7c1cae1ff938a082e5d73d82de4e76f9337136b94ed225e559e21d73e498a \\
Pure Prop Address: & TMbAbdRq1jz52CySGPWWJzvEMuCMw9PQWf2 \\
Theory Prop Id: & f75cd0a8e8a447c357f931be8b2e1f23b89f6b92f2086dc3ff43276f2e88d35d \\
Theory Prop Address: & TMH3GTPuv5BQPyQShNEpPrnhYzZUwtmu5ib
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:dffhcgbhpfadpfcd} ${{0} \subseteq {2}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 4147baf022e55cf2dd6aacf5e6a00ad38638a106bc08411c05387011d04bb7e3 \\
Pure Prop Address: & TMT9Kq6Qfozmik7TG8YKt8eBb884fWgrGUV \\
Theory Prop Id: & e55065b32674ffef3065ed52eb5884c80c49f9fade95b3f25de91a675649b8fe \\
Theory Prop Address: & TMNVFjtQ2Uu5aRqUQUGEuZaFCmJzys2dTcX
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogdffhcgbhpfbdpfad} ${{1}\unicdcdidid{0}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & cd48c3a937c072b881fc81c095acf2d3d19992c467934cbf8c623a3e0b31c7b8 \\
Pure Prop Address: & TMMWurweEZoERkEgMW94uw2qJFHhYfSdhr1 \\
Theory Prop Id: & f57d867ae9fd7ef331bb12d8bbc87507a39c321aa63dccd26566dd794deb29aa \\
Theory Prop Address: & TMJfLY5kzU7711oJKtQgwAjc5L8YVWwNjDY
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:dffhcgbhpfbdpfbd} ${{1} \subseteq {1}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 6810b4ba8d863b656650594ed3d6b824b91deebd03aaa139e90a032fdc3f761e \\
Pure Prop Address: & TMVoM4uwCGDUnRZZHZKXUcXzt6mXEkzgVcY \\
Theory Prop Id: & 786cb1e61bb2545b3c1fa96512a920199016566e4b90be78896f3912039ebdd6 \\
Theory Prop Address: & TMcdzMHtEBTXABdHGrdDC4Ly4fpUtxsqxBG
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:dffhcgbhpfbdpfcd} ${{1} \subseteq {2}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 83e0b593f193b7c5aaa42ebec3fe80fdfec8811d24ad5d1ca621e5e328669b5f \\
Pure Prop Address: & TMKdW2ZiFjAjtmtoqqe1oUa34818gAT8iNr \\
Theory Prop Id: & eb94537ff458732f1b6a217159a18b54524b675d0382a95296b651d3ba8f33c9 \\
Theory Prop Address: & TMYt6f8BQGRNnMa17NCKpryL5i39M9NdrbM
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogdffhcgbhpfcdpfad} ${{2}\unicdcdidid{0}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 5810f58237fa5ea1a72b1b1a19c59174248b204a444cd813a87d5c24b492efed \\
Pure Prop Address: & TMapUXLAzmMk7EFCn8wdLE9wngohhRx64bJ \\
Theory Prop Id: & 3a7512da2ec785465bad179179151f9a8406012ca9652a22c5ee00b1c1e8d549 \\
Theory Prop Address: & TMc22TospZpLCRqLYeAzy9Aw2a8eBegKoHu
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogdffhcgbhpfcdpfbd} ${{2}\unicdcdidid{1}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 63bae94df530a1ce94daf68c68462bbef84a4139da4811189d52312898d4d441 \\
Pure Prop Address: & TMSu6yS8YSy2wRfQSYGzR3kr6TiHARnPaqe \\
Theory Prop Id: & 0a8588177b5ee4d07cdd286638afa3c070f40cd1a82c6cc63bee5d057c8b5211 \\
Theory Prop Address: & TMdVb69DrHqVTcNAtqfbK4id4jxAiXFYfQd
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:dffhcgbhpfcdpfcd} ${{2} \subseteq {2}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 7b90ad5115eabb6dc9245caeb7cbed2927cbb691b26ae5dcecad88d6115f09fa \\
Pure Prop Address: & TMPuu9Nr9pfr2rJDgk5gScNW6sYP8p19FRM \\
Theory Prop Id: & 0a1db4164bb30172507271531b8defd31e8ab3f2d787c5b272ee3bebeb2966f3 \\
Theory Prop Address: & TMUA9eA6KznSVoDTCQaVPvd6cuC6M5SRgKy
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfadpfhd} ${{0} \in {7}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a41b2c54f4d65391d6b32fb603ebffcff201103f2878a4a55f687b12bbe8b91a \\
Pure Prop Address: & TMdFjNSCWXW8Vpvt73BWqM4Zj86eN5S2KNu \\
Theory Prop Id: & 4cb36dedf7517e301f2945346202891f39d34107c01ef2e3b86d9e51b259df54 \\
Theory Prop Address: & TMUvTmAX6RDWKPVpacNDGZQ9p9sYmuoibQG
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfbdpfhd} ${{1} \in {7}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & aa5cdecdaec91fe3a6884b0f09c06631327c30886010ae16f21daddf6ba9c94d \\
Pure Prop Address: & TMJSrd3NEP4iMdJBKZ7F1cS2TZynGhaxyQZ \\
Theory Prop Id: & 392ce8e7c3bb5ff3aa4fa822b0258c7f80e76dedcd760af5717a6e916fa61cae \\
Theory Prop Address: & TMTHHZrGZFsevPcmaS6RDEwByfki1EHr2Fo
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfcdpfhd} ${{2} \in {7}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & b26cf008f7aa0e7ffcb65a467f1e4f72dd8227f1089ee19c2b649ac8f1118454 \\
Pure Prop Address: & TMZoShAAJg9Vr9iuc4kJeMjUubQz3hbFXXd \\
Theory Prop Id: & b47fba676b401c0467d0573bc3d555b8474735646a191dadb139c79d11b2e544 \\
Theory Prop Address: & TMUSma8kwGkSuHzU6fZivqqsFZseHSZ6rHq
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfddpfhd} ${{3} \in {7}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & e6779a7f3f395ebcac3bd6e88ecd8088dc9671cd31a2b7cd8763b2d1967a07e0 \\
Pure Prop Address: & TMZirYDzJAMpfJGxrd52NTyUfVEWH2SZGzA \\
Theory Prop Id: & 38ad3433d50b88a23443fb181777702afa2fd1d0aef7d62ea69949525c1e36c0 \\
Theory Prop Address: & TMPbKx6jYxRGDnKufFfM4TW7RyjNLYW4g4p
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfedpfhd} ${{4} \in {7}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 2d470f9c2b92bd61f616a640439618f469a0d784cb0b08a1a90625b00c1d5ba6 \\
Pure Prop Address: & TMFfR8LTg8YNKJkWgWwamN1Lgup4j48Whny \\
Theory Prop Id: & 07ae6986b58c8e30c6133f6e2016bfeae67ec868d1227fa18a921392adfd8d2a \\
Theory Prop Address: & TMPy9kPwbcVRmzis4rmmQajdnJnWBPWoMWA
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpffdpfhd} ${{5} \in {7}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 685d80ba7d066c28aa1d043f7db6d4b5114f616d882a3bfaf71cd542a148e4ba \\
Pure Prop Address: & TMMku2XXJ9wEw7xtWmoDtdpUqHzpip5x126 \\
Theory Prop Id: & 81137f00c9dd3d97ce30878bfcd5a44b55d559d1dd83f2f941053dd60b37883f \\
Theory Prop Address: & TMZb8pTSFybxEM3VZWF9cs1v9kTeYLx2Mn3
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfgdpfhd} ${{6} \in {7}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & cb4ca2976fd69ef1a079994c73071be6b55cea8db7238fccc9916cc3dd669ed7 \\
Pure Prop Address: & TMMcWExWsKZNzZxK6mn8N5UozNgsLWG22jv \\
Theory Prop Id: & fe9b561a0b2c561827d50aaf6b01fbc0a1fe14ef472c16cc21b1738fdf7693ce \\
Theory Prop Address: & TMa39PQbzrwe6rPaWAdYhM6GqbCbvwB5GFE
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfadpfid} ${{0} \in {8}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0f58323098cf1c7b76cfc3eeea9678f53a42cf23af1f553934572eb5b3fedb4b \\
Pure Prop Address: & TMbVc3Gz8q2ncEs1dxxpVYDJt5maYv7XRYR \\
Theory Prop Id: & 7797f1bcb9aa6b1d1d07565f754d8639d16574c1a6b38967e7432403cfbda877 \\
Theory Prop Address: & TMQfdecCs6mDoNMAna5TMVPYcgtewWsADLX
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfbdpfid} ${{1} \in {8}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & fbef0f51f12e7c2ae21b16ba602e7f68892a1dac9c238bf6b4c1f2bed4eb34d0 \\
Pure Prop Address: & TMXRwsKNE9viw546hC36BY9U9SuJziTMUDB \\
Theory Prop Id: & 0d7bd5f8b87d778142f6aef2fce3ecfd64b37623004ce8979fac7bb6dc71ecc1 \\
Theory Prop Address: & TMXL6Tdr6bmwMFVqYqUkidhjWc9dqLm4zuV
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfcdpfid} ${{2} \in {8}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a07c8ddbe590e66a92f9257de8f0fd799ef1483c2b0db58b970ebd947d68ede1 \\
Pure Prop Address: & TMLXEF3MDk7aJtSHea6Ts5kyRqVvzMTLVMx \\
Theory Prop Id: & a625dbe848c33627c83019ef18fb78feb77869dc01561231f770a2c4534e4fb6 \\
Theory Prop Address: & TMbknbBMXvxmm4ESoH75pgyt1UuzokTDX8U
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfddpfid} ${{3} \in {8}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 7ecdad34b9fda66b48c56dc6bf6ef24f1dd82edaf5b10a676dcb5b1c71d69d4d \\
Pure Prop Address: & TMKDDRJXEjpy9C7xEE4XcgqVTYixinVGGZq \\
Theory Prop Id: & 9b36a6f466e575fb7e2a48f68b7361e970bb6edc56671aeea80a5bed424770b2 \\
Theory Prop Address: & TMN2SjRR2yH8LkDiZpxREFxmhDWA1tRrd8y
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfedpfid} ${{4} \in {8}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 61791c2e5bf306497941d536e18c90c32dc8db7afd6c98cd73d9bbbf773d2493 \\
Pure Prop Address: & TMKmzqKEHSZcjMZkbLYvTdKBAypDeC2vkWw \\
Theory Prop Id: & 219ccf028539e884cc6ed244a4235bffac83e454680efdcbe9746634113b96b9 \\
Theory Prop Address: & TMapcHhFiw8K5Eyguh2XbYVss7iatNsa3XA
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpffdpfid} ${{5} \in {8}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d79eb5b8bab2d0ecce7a5262efe191d5cfa47f1546b64fca19ed3bbb64807bca \\
Pure Prop Address: & TMHdg4GnYxDRPSidyUUEWzVnoASUqBVUVB4 \\
Theory Prop Id: & 5625eb82bb63b6fa37d0b870f9d8240cc59102ee45b5c516d25f9c467415b0d9 \\
Theory Prop Address: & TMZyKWFWemTmDJxiJkpygV8twB2Rtp15Roo
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfgdpfid} ${{6} \in {8}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & bb5a775918672f1f9754e58316f4d97366beae541ee45c784b2caa7cf74b3d95 \\
Pure Prop Address: & TMNL3L2gEnenuX7Xv2E3UpeGxkaNNyZdubb \\
Theory Prop Id: & 3c5f2d23bf893b5c57c706c4203ef7618979c66711b505a3e143cd52883986c1 \\
Theory Prop Address: & TMGi4xjiJrNb1ynt5cGWncJKwUJnCmsHNBs
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfhdpfid} ${{7} \in {8}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 126eeac20dfdb85457404f82039e474f2a8eb9e482703a36265ea720baec0a3c \\
Pure Prop Address: & TMEjueeewmbW3RUuC5wTG9v3ube5BAnUEGQ \\
Theory Prop Id: & cc5985ce2772e22df62ec877dd1108f076a8d4ad53bb1b7aa440ceb21c281908 \\
Theory Prop Address: & TMGFU5u8dWSnsHseshspGDHDJEYkpW2VFo7
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfadpfjd} ${{0} \in {9}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f12d8e4addf556e8ac897b31bd7774ba5f016a114488aa7da47a4982ecf730e0 \\
Pure Prop Address: & TMXfAUPidgroRBVsfRFdmxVG3LXaAGCDfc3 \\
Theory Prop Id: & 5cb21ec1e1dd5e4c549e48ad0c126c468ccd82b46d5eea40b232ccf7c035b032 \\
Theory Prop Address: & TMPTV8Q2AeyehU2pLq7PNkwxbmhsacvmwyR
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfbdpfjd} ${{1} \in {9}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 5922261855dc9c35d7a19be6bbe7337de066e405197aa8c3f331b75cb8f166d2 \\
Pure Prop Address: & TMFXiJ1JnXuvAUNxeQTQDnCcXESe6geABqf \\
Theory Prop Id: & 0d30f02a5d23823a40baed594ac7548d8af020600e5b2a30d8d190892e99ac7f \\
Theory Prop Address: & TMLQmTKRPrhZ6kBwPoMiaYrb5eJ5CspjmFe
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfcdpfjd} ${{2} \in {9}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 024448eff2c81d63335a32519066934b16f60b301c909ac62e1aa2496f034b12 \\
Pure Prop Address: & TMSxqdqe4vyyMqhgByQKNDjzpe7hLiYJShy \\
Theory Prop Id: & 330a457d080fe85bbe9e6674a86a4ae3f9e863e5ef5d34f3d5fbd1229256ac61 \\
Theory Prop Address: & TMGa1rMZX1W4ZGdPLqcVb6bsiTpmjbxmANL
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfddpfjd} ${{3} \in {9}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & afa2b48908b69981c7ad81b71c4bb9e93fb53c3c337307ba4e9d394be14b4eae \\
Pure Prop Address: & TMa3VWUSB3PNWdYhRYTBKk4sraF2pPhodut \\
Theory Prop Id: & 6e40119249c9eff81c846d321343f9181f0fbbae5206bde40c6383b8c0ec20bc \\
Theory Prop Address: & TMP2oP3jaVQRn8x97tPUZDxRbcZQLEPeJ9x
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfedpfjd} ${{4} \in {9}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & fdadb4647802a0e507d7b6593df90699056f72e47e5888a3135537fb646a3dbc \\
Pure Prop Address: & TMSFuF88nVp1p3DHdC3pEkjfaYLf6goH5vi \\
Theory Prop Id: & caa1f8ed95c772063de3aa6a8b2cbfb5e9d219c3229bb9c5ce31f5eca2f9de0b \\
Theory Prop Address: & TMbbYX4XLfjzv5dH8d76TFx5HmsrMRJ4tm3
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpffdpfjd} ${{5} \in {9}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 318ef9258894a50147815073ae5c4f15b2e60e8d262fe4baa2fd4ac0643491bc \\
Pure Prop Address: & TMQXwEo9W8vVJvGC5AHtnroNxcEsfWyG8Kd \\
Theory Prop Id: & f8aae6c774ede7b089d55ed0f0b30d8fa10e7089bcc1eb1db56f40c182c816c0 \\
Theory Prop Address: & TMWDNdKoeVzUChM4ATtv7DwzjNjWouiN5u7
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfgdpfjd} ${{6} \in {9}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & dc3ff488e971d760fe164604c2ee2de729dd5be38a0bc74d93cedb851d661ab9 \\
Pure Prop Address: & TMTGMooeB9YBX55ezejbgrg6SxmcrHwz22C \\
Theory Prop Id: & 0c8dd335320b67f918a737c3818ade882eb57d2cecbad2d32baa17a47518ed1d \\
Theory Prop Address: & TMXsYFAkpquNtmfFQAYjQstpLXT7uYETZbU
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfhdpfjd} ${{7} \in {9}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 95d3ebc9e30fe58f8ee1d32b8b051ab32276f7f30609b2fdcd7cec1cf2c66cda \\
Pure Prop Address: & TMHUzLX2Z8CF8zE5QGfoumbM8j4vavy7ff5 \\
Theory Prop Id: & 02d55222d7d63900ce597b6f79802629c35164ffc62e82ce1b5c9351ae90842b \\
Theory Prop Address: & TMZYe552F7mK6w5rhKoUE4iCEyFHkzTaJsC
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeogpfidpfjd} ${{8} \in {9}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & aa9c6bc99164b52c64952a5e4c3f8ab0450b9a32b7a19a40e692e6458352bbdc \\
Pure Prop Address: & TMMVC6pC2fVWYrSnkueRZ7f3obgNuwZK5aW \\
Theory Prop Id: & 981f43991092c5fd5e23973a29612ea078b2458ee398f5f4e27b1c669761e9ca \\
Theory Prop Address: & TMdurdeoZjzzmm64ypv6qGYNuFSjkTQnJtF
\end{tabular}
\end{center}

\end{theorem}
\section{NatRec}\label{oebgehcffgdg}Let $ z : {\iota}$ be given.
Let $ f : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ be given.
Let $F : {{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{\iota}})}\unicdbdjdcd{\iota}}}$ be ${\uniddcgcg n g .  {\mif{{{{\mname{Union}}~{n}} \in {n}}}{{{{f}~{({{\mname{Union}}~{n}})}}~{({{g}~{({{\mname{Union}}~{n}})}})}}}{{z}}}}$.
\begin{definition}\label{def:ogbgehpfahchjgngchfgdg}
We define $\mname{nat\_primrec}$ to be ${{\mname{In\_rec\_i}}~{F}}$ of type ${{\iota}\unicdbdjdcd{\iota}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 3be1c5f3e403e02caebeaf6a2b30d019be74b996581a62908316c01702a459df \\
Pure Object Address: & TMMruBGibDS8rkGTgYt2TbCgEshTqpc8T9L \\
Theory Object Id: & 1a64d5d130b189ae403562ffd2a8a2fa63feaf78ed6abca2742cea1af4e1547a \\
Theory Object Address: & TMLxfukbsKf284nSh5ByiFX1hp1cggVTAUF
\end{tabular}
\end{center}

\end{definition}
\begin{theorem}\label{thm:ogbgehpfahchjgngchfgdgpfch} ${\unicdcdadad X : {\iota} .  {\unicdcdadad g h : {{\iota}\unicdbdjdcd{\iota}} .  {{({\unicdcdadad x \in {X} .  {{{g}~{x}}={{h}~{x}}}})}\unicdbdjdcd{{{{F}~{X}}~{g}}={{{F}~{X}}~{h}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & c955cd8ed0958d2ed269c30204a3cdf992cbaa25660ad46a00085023b9a73746 \\
Pure Prop Address: & TMV6dvzCjCU8eRTowJftzbC63sPXHppC6uR \\
Theory Prop Id: & 9ba88707241ec8607e5cec9c0325d12d528f63b0670344631f540a848092b465 \\
Theory Prop Address: & TMFCUCvpQLtDtMF2PaNT39UWn3VGzEMY9Cz
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogbgehpfahchjgngchfgdgpfad} ${{{\mname{nat\_primrec}}~{0}}={z}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 416eafbf1b348bac1c33766729696046e8de834bf29675a0bcbf8e9e2f4a2dc9 \\
Pure Prop Address: & TMVRM6N2YRqKYHAeVikSGWqmkhKWLLqo61v \\
Theory Prop Id: & be11a277d9d20c3312b9592199a4932dcad62cb9aee7679da0a117c5016e5477 \\
Theory Prop Address: & TMZ6oFEPsAfDfMvyeTRLHoi489W3WuPogFb
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogbgehpfahchjgngchfgdgpfdf} ${\unicdcdadad n : {\iota} .  {{{\mname{nat\_p}}~{n}}\unicdbdjdcd{{{\mname{nat\_primrec}}~{({{\mname{ordsucc}}~{n}})}}={{{f}~{n}}~{({{\mname{nat\_primrec}}~{n}})}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 79718550912e5445000ec2075df6854a99c68fbe7dc1bea4ca955eb813ce143d \\
Pure Prop Address: & TMQkJomVG82rUFW7nbsE295nn7dZqExNfUV \\
Theory Prop Id: & fe4c88c37a0678c8dd8db722e13c22b2d116aee8f889a70007d0ce07747f3f05 \\
Theory Prop Address: & TMXGF76gsDqDFEkGMFYsmNF4aDipvSuu3Xj
\end{tabular}
\end{center}

\end{theorem}
\section{NatArith}\label{oebgehbechjgehig}\begin{definition}\label{def:bgegegpfogbgeh}
We define $\mname{add\_nat}$ to be ${\uniddcgcg n m : {\iota} .  {{{{\mname{nat\_primrec}}~{n}}~{({\uniddcgcg \_ r .  {{\mname{ordsucc}}~{r}}})}}~{m}}}$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & afa8ae66d018824f39cfa44fb10fe583334a7b9375ac09f92d622a4833578d1a \\
Pure Object Address: & TMQX4KdWNNKEeAgNGf2XNUoYDVDzvGnc31d \\
Theory Object Id: & 29768b585374d1e88373f200fac530e11d07d4aec939607f546fda4fae32538d \\
Theory Object Address: & TMQ7riv5frn6wUQus29DXdY5DVorPU5wZwh
\end{tabular}
\end{center}

\end{definition}
{\bf{Notation.}} We use $\inflc$ as a right associative infix operator  corresponding to applying term ${\mname{add\_nat}}$.
\begin{theorem}\label{thm:bgegegpfogbgehpfadcf} ${\unicdcdadad n : {\iota} .  {{{n}+{0}}={n}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 402bcbdce23d41df6234b683ebd9d480b649637a52dbe21deab650c8ceded543 \\
Pure Prop Address: & TMYQQZGZaNiuYCPSimRia2Xfn2Q6QWbtqhS \\
Theory Prop Id: & 23277f785fd4b6fdf8ebe586a27b9fd4a47086eec22dc99b0d691329fba31a4b \\
Theory Prop Address: & TMXQW56dPBW8mAHqGUEmsjLRYKBrxAAonqY
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:bgegegpfogbgehpfdfcf} ${\unicdcdadad n m : {\iota} .  {{{\mname{nat\_p}}~{m}}\unicdbdjdcd{{{n}+{{\mname{ordsucc}}~{m}}}={{\mname{ordsucc}}~{({{n}+{m}})}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a53523a8fbb46795673b15c005b9c1c1d054e111ec64c524c3fa3b20ef02e932 \\
Pure Prop Address: & TMTGvLHefupPU9uKtSQRk1QWQzFMwgJrrZU \\
Theory Prop Id: & e61e18415fcbe09a2e909f97e3a2d3fe2abd965f61f8aab6a960f324295f0c82 \\
Theory Prop Address: & TMZUDpxQFwyy7YPJopzHZxFeJpa5xzNgnSM
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:bgegegpfogbgehpfah} ${\unicdcdadad n : {\iota} .  {{{\mname{nat\_p}}~{n}}\unicdbdjdcd{\unicdcdadad m : {\iota} .  {{{\mname{nat\_p}}~{m}}\unicdbdjdcd{{\mname{nat\_p}}~{({{n}+{m}})}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a68eaa385d85714b752c87f2a2eee1c568587a1fffda0e97906a41c26003cf88 \\
Pure Prop Address: & TMc24JjrtUUsp2EU37UmE4mu7iJ7DKkmhBJ \\
Theory Prop Id: & 4c1d5d018a9f1d2b9453690cae8404fa9eb620f367b5eea25a0cb86d97cbe223 \\
Theory Prop Address: & TMFY44nBuvZeLpSeXoD777seJQ3FwNH5bHN
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:bgegegpfogbgehpfbgdhdhpg} ${\unicdcdadad n : {\iota} .  {{{\mname{nat\_p}}~{n}}\unicdbdjdcd{\unicdcdadad m : {\iota} .  {{{\mname{nat\_p}}~{m}}\unicdbdjdcd{\unicdcdadad k : {\iota} .  {{{\mname{nat\_p}}~{k}}\unicdbdjdcd{{{({{n}+{m}})}+{k}}={{n}+{({{m}+{k}})}}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & c81c09e2824f3ae69080689a9918f8a8786896c891f60deb4ed02d6f67f3cb62 \\
Pure Prop Address: & TMKhPKqB8txYNiBHfmLH1ruc7muR6qocZmM \\
Theory Prop Id: & eec29406f31cd07c1e41a8cfa7dd645a14748dd76d405c653593376354c1801c \\
Theory Prop Address: & TMJ8UyHV8GUb8Vws1rSbV1qG6FtayeCkDeZ
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:bgegegpfogbgehpfadme} ${\unicdcdadad m : {\iota} .  {{{\mname{nat\_p}}~{m}}\unicdbdjdcd{{{0}+{m}}={m}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 8ceeb9658771d534867c4e7fb857c194b87b3c269b78a59e437c53340f7a0786 \\
Pure Prop Address: & TMLoqyDa4T219PBE9qaSVziSgcNXAuyYZSy \\
Theory Prop Id: & 84fbe4456a772afa70e2e251ea34167365bee559c7a5aeb17e73e850db6f7c53 \\
Theory Prop Address: & TMYQwEtyoLvmW7jPiZze4QVGPj5DZuaTf5Q
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:bgegegpfogbgehpfdfme} ${\unicdcdadad n : {\iota} .  {{{\mname{nat\_p}}~{n}}\unicdbdjdcd{\unicdcdadad m : {\iota} .  {{{\mname{nat\_p}}~{m}}\unicdbdjdcd{{{{\mname{ordsucc}}~{n}}+{m}}={{\mname{ordsucc}}~{({{n}+{m}})}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 9c442aaec4cf7410aad415dc7f4e04405898410e390d79880d0375c76066e5fa \\
Pure Prop Address: & TMaAYzqo6wqjw8Cyowaj3GfJxJxvbhxYDju \\
Theory Prop Id: & e6efb75f65615ef88f5bde274557d9a8df5606c47b340bdff64b75fde270e0f5 \\
Theory Prop Address: & TMHs3GjtfJJMSExofB5jjekwQXt9vQ9JVEp
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:bgegegpfogbgehpfdgpgng} ${\unicdcdadad n : {\iota} .  {{{\mname{nat\_p}}~{n}}\unicdbdjdcd{\unicdcdadad m : {\iota} .  {{{\mname{nat\_p}}~{m}}\unicdbdjdcd{{{n}+{m}}={{m}+{n}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 40e9527c8d2ba8c9684c597d041b44dd398a84708d4958ed949bd806aa07a045 \\
Pure Prop Address: & TMUKhdGt15R67GHJenCm4tPyhkXRshPnejp \\
Theory Prop Id: & 4ab1793481bb6270a606171fd587949f75d9e5d9f76c6cabe92d879d2029efbb \\
Theory Prop Address: & TMTvQoshXSimoWoX7FGXYgBcckAvFxKAzcM
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:ngfhmgpfogbgeh}
We define $\mname{mul\_nat}$ to be ${\uniddcgcg n m : {\iota} .  {{{{\mname{nat\_primrec}}~{0}}~{({\uniddcgcg \_ r .  {{n}+{r}}})}}~{m}}}$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 35a1ef539d3e67ef8257da2bd992638cf1225c34d637bc7d8b45cf51e0445d80 \\
Pure Object Address: & TMQ9VRpXGSTRvGimsfh4aDJ7zMynq4DQkpu \\
Theory Object Id: & 80ccc668a68b08f05dbefe4777f8a2954ee878fde2459ea00e9c3f844abba676 \\
Theory Object Address: & TMSPdCUvrmtPueTXMGGcZnyt6hALJ9ctyFj
\end{tabular}
\end{center}

\end{definition}
{\bf{Notation.}} We use $\infkc$ as a right associative infix operator  corresponding to applying term ${\mname{mul\_nat}}$.
\begin{theorem}\label{thm:ngfhmgpfogbgehpfadcf} ${\unicdcdadad n : {\iota} .  {{{n}*{0}}={0}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & b2f56c05dc69c0b009e6ef48273e48c299236dba09369d6470f062d8d4b9f4e0 \\
Pure Prop Address: & TMb9Vpd2YbcAwzGuAijMPac1ZZd1JTyv4Xi \\
Theory Prop Id: & 1e5b2cd8b1404db3fe789241877d2db676126a3ee22aef833bce50e59717f3b5 \\
Theory Prop Address: & TMYKPBEGEsiA6kAm2D5gNMaaoQznS2XzHfH
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ngfhmgpfogbgehpfdfcf} ${\unicdcdadad n m : {\iota} .  {{{\mname{nat\_p}}~{m}}\unicdbdjdcd{{{n}*{{\mname{ordsucc}}~{m}}}={{n}+{{n}*{m}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 37df54fff3ede09b5f27087075ed84f0c3c205aeb237fe98e376929562343633 \\
Pure Prop Address: & TMGeZ3mYtjU3qrjXWbppcFZ1rqeDWrfiSqC \\
Theory Prop Id: & 6dd6fc3c946630902a37292306a5d4628d0df49b90a16a0b4bde060e327d01ba \\
Theory Prop Address: & TMWCj8uVzNKMcnEEoUyEKaLXqDFHWBQkrus
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ngfhmgpfogbgehpfah} ${\unicdcdadad n : {\iota} .  {{{\mname{nat\_p}}~{n}}\unicdbdjdcd{\unicdcdadad m : {\iota} .  {{{\mname{nat\_p}}~{m}}\unicdbdjdcd{{\mname{nat\_p}}~{({{n}*{m}})}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d63438e3958a2dc77d897cf86bd67bfea42d951dc7cc262804802907e9d2702b \\
Pure Prop Address: & TMG1LZCLEQXdxeijnJMFK24mEb2ZENAEMJe \\
Theory Prop Id: & e910cb7dbed9f807bb2b492fd880072b0fa60ff97bf29504de618c1bb02b9b7b \\
Theory Prop Address: & TMHuRaAVff8dq9SXtxuPNkua68MeuTc6xgX
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ngfhmgpfogbgehpfadme} ${\unicdcdadad m : {\iota} .  {{{\mname{nat\_p}}~{m}}\unicdbdjdcd{{{0}*{m}}={0}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & db8a357ff4bbc85955dad0c6561e2f2e46517b67140c8b29f3410a166806d8c9 \\
Pure Prop Address: & TMat1oD79SXX8wbvMUfsE7vpuGWs6TV2tvt \\
Theory Prop Id: & 6a2dd6eb8d82e1ebdc8d29656a314ba5f0823446cfd1b7e3e023a868e5c576a8 \\
Theory Prop Address: & TMKees76uQpkLU55adTSh33A5D4a1pWMJ6o
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ngfhmgpfogbgehpfdfme} ${\unicdcdadad n : {\iota} .  {{{\mname{nat\_p}}~{n}}\unicdbdjdcd{\unicdcdadad m : {\iota} .  {{{\mname{nat\_p}}~{m}}\unicdbdjdcd{{{{\mname{ordsucc}}~{n}}*{m}}={{{n}*{m}}+{m}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 5cf7ece86a139e3814ee6c6c7d1036b5efd2cb2a7569655a5785267e6b0744c7 \\
Pure Prop Address: & TMPvhe9Rvam418EBDU6GUny2MjoZwaH5XpP \\
Theory Prop Id: & 24e4ebc5814e4a359b7a34331c431f191c16ea51e3acd3df89dfc39cbb4f5310 \\
Theory Prop Address: & TMK29Vjye4s7vokoPSyBUEGUMF7out1xEKo
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ngfhmgpfogbgehpfdgpgng} ${\unicdcdadad n : {\iota} .  {{{\mname{nat\_p}}~{n}}\unicdbdjdcd{\unicdcdadad m : {\iota} .  {{{\mname{nat\_p}}~{m}}\unicdbdjdcd{{{n}*{m}}={{m}*{n}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 4525ef58273c984cb807830a9315b6c92ea0e51493bee52c9fdb11b2c032debb \\
Pure Prop Address: & TMR99zvsWSdWrZH1xvD1ZPyyRe2sN3tw9DJ \\
Theory Prop Id: & 5d6ce40bd822f0043fa5e91314acb4c38d4657e00036f8292d1c646d61867911 \\
Theory Prop Address: & TMK6YYFmjjLN7XjWZngbXtSHGuvLhCNW5sK
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ngfhmgpfbgegegpfogbgehpfegjgdhehchme} ${\unicdcdadad n : {\iota} .  {{{\mname{nat\_p}}~{n}}\unicdbdjdcd{\unicdcdadad m : {\iota} .  {{{\mname{nat\_p}}~{m}}\unicdbdjdcd{\unicdcdadad k : {\iota} .  {{{\mname{nat\_p}}~{k}}\unicdbdjdcd{{{n}*{({{m}+{k}})}}={{{n}*{m}}+{{n}*{k}}}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 7758f10f23cd5bde5f62e6e19176c07070d03250e7ee2f5445ddd169a94ac9cc \\
Pure Prop Address: & TMEg6jVocmXvkpGecshFe76iHzxRPb9JEDU \\
Theory Prop Id: & d57b0261b87e3402ab865d1448a120cf5a64d7df32d00662a23546d0192c5f7f \\
Theory Prop Address: & TMRv9ASbnJeJHuEAVEnAXZtBdyUqKHy7Num
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ngfhmgpfbgegegpfogbgehpfegjgdhehchcf} ${\unicdcdadad n : {\iota} .  {{{\mname{nat\_p}}~{n}}\unicdbdjdcd{\unicdcdadad m : {\iota} .  {{{\mname{nat\_p}}~{m}}\unicdbdjdcd{\unicdcdadad k : {\iota} .  {{{\mname{nat\_p}}~{k}}\unicdbdjdcd{{{({{n}+{m}})}*{k}}={{{n}*{k}}+{{m}*{k}}}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & c2db2e2dc62062cd1a587ac9ba967b9afcf30e142bf9bd6067b24d6b2f537912 \\
Pure Prop Address: & TManfhaHUANQVLqQTLdBVmdTonLkBBLbBAf \\
Theory Prop Id: & a456bc1368534ecb0130b6b056bce984b8cae31fe686bfe5fa19371ee7bc295d \\
Theory Prop Address: & TMTE1UAeY9QMbiDArVw7LV9YCaXoyHNsWTu
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ngfhmgpfogbgehpfbgdhdhpg} ${\unicdcdadad n : {\iota} .  {{{\mname{nat\_p}}~{n}}\unicdbdjdcd{\unicdcdadad m : {\iota} .  {{{\mname{nat\_p}}~{m}}\unicdbdjdcd{\unicdcdadad k : {\iota} .  {{{\mname{nat\_p}}~{k}}\unicdbdjdcd{{{({{n}*{m}})}*{k}}={{n}*{({{m}*{k}})}}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 564886c3dec6ac8d225ffa511e508fd66f08a374ef9f3441d381346c5fd9da75 \\
Pure Prop Address: & TMTj2mzQJp3MhibenRc1qV4e9VBJHGB5LmM \\
Theory Prop Id: & 229d2cf885153a28edbff336b15f01f9a69ebb36151922686ca00a59c571593d \\
Theory Prop Address: & TMRAaHnsfviFEtPvtoFHTUV4fNfwKjkAV61
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:bgegegpfogbgehpfbdpfbdpfcd} ${{{1}+{1}}={2}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 174b87c6660c5b9369cec9ae0bb6fbfa629fb619d7c5b2abc06dbe96f057f730 \\
Pure Prop Address: & TMaJcaiD1zqTNzV6GxQBzYBvpnhKKCh8BgZ \\
Theory Prop Id: & 77f23f1fdaa42b143fa225c79a56a1ea865e80541dbf361ba18f855e404b3575 \\
Theory Prop Address: & TMWAt7x6EE1xxXg5JkjkfpLoXMkjM4S7GM9
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:egjgghjgegfgdhpfogbgeh}
We define $\mname{divides\_nat}$ to be ${\uniddcgcg m n .  {{{{m} \in {\mname{omega}}}\unicdcdcdhd{{n} \in {\mname{omega}}}}\unicdcdcdhd{\unicdcdaddd k \in {\mname{omega}} .  {{{m}*{k}}={n}}}}}$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 1b17d5d9c9e2b97e6f95ec4a022074e74b8cde3e5a8d49b62225063d44e67f4f \\
Pure Object Address: & TMFX8yTrN53rRgSLEZohcsRA6EaD3CSANo1 \\
Theory Object Id: & 355928b746d784c55c7688d88105ecefae6bd0215b4f742280a8381aabba7f6f \\
Theory Object Address: & TMc53M2iKqdhRPHnQpz3E7ib2G4x4BAu8NK
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:ahchjgngfgpfogbgeh}
We define $\mname{prime\_nat}$ to be ${\uniddcgcg n .  {{{{n} \in {\mname{omega}}}\unicdcdcdhd{{1} \in {n}}}\unicdcdcdhd{\unicdcdadad k \in {\mname{omega}} .  {{{{\mname{divides\_nat}}~{k}}~{n}}\unicdbdjdcd{{{k}={1}}\unicdcdcdid{{k}={n}}}}}}}$ of type ${{\iota}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 729ee87b361f57aed9acd8e4cdffcb3b80c01378d2410a0dabcf2c08b759e074 \\
Pure Object Address: & TMdvXdQkmLZGboSGJXGXRKmLGB5pqxCZpoJ \\
Theory Object Id: & a54ca44017bc4b34632c41638b465b39b14dd8cd1733ed77712e0d245baffed5 \\
Theory Object Address: & TMPsbUQYdAiibkkLrzYgRtSGEqJ5zvim61J
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:dgpgahchjgngfgpfogbgeh}
We define $\mname{coprime\_nat}$ to be ${\uniddcgcg a b .  {{{{a} \in {\mname{omega}}}\unicdcdcdhd{{b} \in {\mname{omega}}}}\unicdcdcdhd{\unicdcdadad x \in {{\mname{omega}}\unicdcdbdgd{1}} .  {{{{\mname{divides\_nat}}~{x}}~{a}}\unicdbdjdcd{{{{\mname{divides\_nat}}~{x}}~{b}}\unicdbdjdcd{{x}={1}}}}}}}$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 73e637446290a3810d64d64adc8380f0b3951e89a2162b4055f67b396b230371 \\
Pure Object Address: & TMFmmCt86ZmVJJyYkyLgqnb1fJ56frE48w6 \\
Theory Object Id: & 5e7a659c94f73f93fcc4101b5280fa38c54cf4b3836afc4acb20cdafe1a91f6c \\
Theory Object Address: & TMHvTwzJu9htnnfJFGzTSVgNXc69bPtJJRj
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:fgbhfhjgghpfogbgehpfngpgeg}
We define $\mname{equiv\_nat\_mod}$ to be ${\uniddcgcg m k n .  {{{{{m} \in {\mname{omega}}}\unicdcdcdhd{{k} \in {\mname{omega}}}}\unicdcdcdhd{{n} \in {\mname{omega}}}}\unicdcdcdhd{({{({\unicdcdaddd q \in {\mname{omega}} .  {{{m}+{{q}*{n}}}={k}}})}\unicdcdcdid{({\unicdcdaddd q \in {\mname{omega}} .  {{{k}+{{q}*{n}}}={m}}})}})}}}$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 23f216cd4975d7a2b1380d30e7b48227ee30bb436b18413678721f3abebc9c6a \\
Pure Object Address: & TMbQxhb4L79WyCM6RdiNH8CwjnACqvJCArJ \\
Theory Object Id: & b3e6279627f6e69ce3e9cae910a6faa1ed2221482dbf9b8cbfff595f2802cb5b \\
Theory Object Address: & TMTkKJpV4fxDM1kVGWKTUL74oaK3t8akX8c
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:fgihahpfogbgeh}
We define $\mname{exp\_nat}$ to be ${\uniddcgcg n m : {\iota} .  {{{{\mname{nat\_primrec}}~{1}}~{({\uniddcgcg \_ r .  {{n}*{r}}})}}~{m}}}$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 37c5310c8da5c9f9db9152285b742d487f1a5b1bd7c73a4207d40bcd4f4d13fb \\
Pure Object Address: & TMQbaN33eGzJDYuzCJatBYA9orZ4FEpcRPM \\
Theory Object Id: & 8e35a198b6dbafe8b2e95eb0500523f42f6367ca1c5bcf349ca278f24a3a07d7 \\
Theory Object Address: & TMEwKZ5cpkx2mJ4qE8BkCSWkbVNAA7Wvn6U
\end{tabular}
\end{center}

\end{definition}
{\bf{Notation.}} We use $\infof$ as a right associative infix operator  corresponding to applying term ${\mname{exp\_nat}}$.
\begin{definition}\label{def:fgghfgogpfogbgeh}
We define $\mname{even\_nat}$ to be ${\uniddcgcg n .  {{{n} \in {\mname{omega}}}\unicdcdcdhd{\unicdcdaddd m \in {\mname{omega}} .  {{n}={{2}*{m}}}}}}$ of type ${{\iota}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 1725096a59f3309a3f55cd24aaa2e28224213db0f2d4e34a9d3e5f9741529a68 \\
Pure Object Address: & TMJGQEurbTgjiciPtBTutT9u7rTkMUN4MWJ \\
Theory Object Id: & c28a39bb677f0bc8b9d085f62ff72d310153afc73e004a5ac360c1cd5397836a \\
Theory Object Address: & TMWJQjHTr9nF6QRD4b8ffhEed2Z8ZMsa6nB
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:pgegegpfogbgeh}
We define $\mname{odd\_nat}$ to be ${\uniddcgcg n .  {{{n} \in {\mname{omega}}}\unicdcdcdhd{\unicdcdadad m \in {\mname{omega}} .  {{n}\unicdcdgdad{{2}*{m}}}}}}$ of type ${{\iota}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 8358baafa9517c0278f00333f8801296b6383390ea4814caaadcff0dec35238d \\
Pure Object Address: & TMGKNXPQbMNiuCqZnwUEjEUha8fcnFt3Jk2 \\
Theory Object Id: & e16741f9a0da9b00388d2994378dc8d14febef4c577e38c02cea2b3600c7b124 \\
Theory Object Address: & TMPkkurDzwQcwtKKmG9c9urhgvFf7SduuxD
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:ogbgehpfggbgdgehpgchjgbgmg}
We define $\mname{nat\_factorial}$ to be ${\uniddcgcg n .  {{{{\mname{nat\_primrec}}~{1}}~{({\uniddcgcg k r .  {{{\mname{ordsucc}}~{k}}*{r}}})}}~{n}}}$ of type ${{\iota}\unicdbdjdcd{\iota}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & ff333a6e581c2606ed46db99bd40bdd3a1bab9a80526a0741eba5bddd37e1bba \\
Pure Object Address: & TMZjHdCL77axNr9RebheBmYNoJLbcGbbnfG \\
Theory Object Id: & 43798425ce2e239eb427ae260e9a7b313bf8bd7df1dab1d082f026f6c879692c \\
Theory Object Address: & TMYeeBw9Gn9bU5FejUUExj87nTNnbgW5gbX
\end{tabular}
\end{center}

\end{definition}
