\chapter{Natural Numbers II}
\begin{theorem}\label{thm:afjghgfgpgogiepgmgfgpfogbgeh} ${\unicdcdadad n .  {{{\mname{nat\_p}}~{n}}\unicdbdjdcd{\unicdcdadad f : {{\iota}\unicdbdjdcd{\iota}} .  {{({\unicdcdadad i \in {{\mname{ordsucc}}~{n}} .  {{{f}~{i}} \in {n}}})}\unicdbdjdcd{\preoh{{({\unicdcdadad i j \in {{\mname{ordsucc}}~{n}} .  {{{{f}~{i}}={{f}~{j}}}\unicdbdjdcd{{i}={j}}}})}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d756b7f9b65b31513512c63b940fdfc4ecb49540116753f6c2d340626609ee82 \\
Pure Prop Address: & TMLBavCBsSBws7ahi4AVPeESXViLDv31Ak8 \\
Theory Prop Id: & 604a84ad91cecfb6b42f1126bfec73fd706444dd748ec6c15b12ce0bfb69053a \\
Theory Prop Address: & TMVN7QY12B9fLrGqiNtTGBesGf96NCkiHRC
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:afjghgfgpgogiepgmgfgpfogbgehpfcgjgkg} ${\unicdcdadad n .  {{{\mname{nat\_p}}~{n}}\unicdbdjdcd{\unicdcdadad f : {{\iota}\unicdbdjdcd{\iota}} .  {{({\unicdcdadad i \in {n} .  {{{f}~{i}} \in {n}}})}\unicdbdjdcd{{({\unicdcdadad i j \in {n} .  {{{{f}~{i}}={{f}~{j}}}\unicdbdjdcd{{i}={j}}}})}\unicdbdjdcd{{{{\mname{bij}}~{n}}~{n}}~{f}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & cd3b8dc5389196c2477610f742fb1ee7dba1dcdf01fea50de9a063945a56cffb \\
Pure Prop Address: & TMV5QRAwtRsRGashmQVHiReREqRjLYeRTHc \\
Theory Prop Id: & 44a08f5c7754241cf51e71665e77acf0e4b00fd74a503742d7594661c4883eac \\
Theory Prop Address: & TMQn8ujQbMM2W4yRjHGhzmzMYVZfwKNdhFW
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:dgbgdhfgdhpfhd} ${\unicdcdadad i \in {7} .  {\unicdcdadad p : {{\iota}\unicdbdjdcd{o}} .  {{{p}~{0}}\unicdbdjdcd{{{p}~{1}}\unicdbdjdcd{{{p}~{2}}\unicdbdjdcd{{{p}~{3}}\unicdbdjdcd{{{p}~{4}}\unicdbdjdcd{{{p}~{5}}\unicdbdjdcd{{{p}~{6}}\unicdbdjdcd{{p}~{i}}}}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 9d65eaceb8856524e55245becb873ac99520db85c1aa6190004c31f201ae565a \\
Pure Prop Address: & TMMGJXuShsSGWBi3CaHZeVWjtSHGMJv1cqn \\
Theory Prop Id: & 0b70c477b139fb0134ba4733415ed1d40b67071992567e7df1d98b3fa3ef4f9b \\
Theory Prop Address: & TMXFRbLTTN6ihayKReZVwptm9miwKifcmVm
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:dgbgdhfgdhpfid} ${\unicdcdadad i \in {8} .  {\unicdcdadad p : {{\iota}\unicdbdjdcd{o}} .  {{{p}~{0}}\unicdbdjdcd{{{p}~{1}}\unicdbdjdcd{{{p}~{2}}\unicdbdjdcd{{{p}~{3}}\unicdbdjdcd{{{p}~{4}}\unicdbdjdcd{{{p}~{5}}\unicdbdjdcd{{{p}~{6}}\unicdbdjdcd{{{p}~{7}}\unicdbdjdcd{{p}~{i}}}}}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & fb834c80b903a21792ab31c32ca79011f1ed7fc1ee605431cab0377c113ce789 \\
Pure Prop Address: & TMJ9pan6QGbicHY78ZhcRV5sjSxUpJ9hjAe \\
Theory Prop Id: & 148753c82fc2d19e4d0ccfdd34fc8ac73852e40d98c8740e4bbf13f37f1469bc \\
Theory Prop Address: & TMaE8ED9F5UkowTrWVxJoWwkbViqo9kPjoK
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:dgbgdhfgdhpfjd} ${\unicdcdadad i \in {9} .  {\unicdcdadad p : {{\iota}\unicdbdjdcd{o}} .  {{{p}~{0}}\unicdbdjdcd{{{p}~{1}}\unicdbdjdcd{{{p}~{2}}\unicdbdjdcd{{{p}~{3}}\unicdbdjdcd{{{p}~{4}}\unicdbdjdcd{{{p}~{5}}\unicdbdjdcd{{{p}~{6}}\unicdbdjdcd{{{p}~{7}}\unicdbdjdcd{{{p}~{8}}\unicdbdjdcd{{p}~{i}}}}}}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0d0c6a6d27f3197a59eed06051dc8e722f3c73606b083f56fa41970d63f24e12 \\
Pure Prop Address: & TMKuRMEvwYcoSa8Gzg1hrtZoBaBSPH2xcsW \\
Theory Prop Id: & cc8c42c160b06cd70b0400e6d0cd711ceb06d2dd8fbbf1468400cdf70a509df5 \\
Theory Prop Address: & TMLp2MUsd6cFR8gFchdhfihDsX7oRanJWxR
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogjeogpfcdpfbd} ${{2}\unicdcdadjd{1}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d4d954c8170695a2939bec3c446c37edaeb27568ad48b1986c6ecaba24070132 \\
Pure Prop Address: & TMMJE7KaXfpvgsT5JWqzaMeStdMLFTu4s3R \\
Theory Prop Id: & 9f9cbd90053ad69e8dc078d6b9aafbd1e870ff598f884002a52555d6cf96db04 \\
Theory Prop Address: & TMSytpFZDKijwdEXRuEoRS26emWEHwyyJn9
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfgdpfad} ${{6}\unicdcdgdad{0}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d94311e2671c987b8b42941206d260e5fad22da17796f0e0af8fd9718168e741 \\
Pure Prop Address: & TMJPPVAEoouTBu7DFSenpbm1vf43asWn9A9 \\
Theory Prop Id: & f94806573dcb9fa2ec502b75f210c999a07ae981958bf4172d246de9cef66017 \\
Theory Prop Address: & TMUnexmnNzMTxwUotBtEVHCSB7LQYjDXGCA
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfgdpfbd} ${{6}\unicdcdgdad{1}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & c950efa1242fe81c8f031eb108e16f8792592823a5d93bd4f60a0f648062bc05 \\
Pure Prop Address: & TMG4GcsPH6pN4zKNadStY83A7KTwr1YmB43 \\
Theory Prop Id: & 799bdf447bc496543bc3e105fee018f133d24d15ca3c6eb8fa5bb71688379c06 \\
Theory Prop Address: & TMNpiWkUsYako2ZQqsmQ8aMpiCajvjtw6WY
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfgdpfcd} ${{6}\unicdcdgdad{2}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d5b69e228a453716ca00492b40a6fb313f2f582f72946915bc5cba6815ebd5b4 \\
Pure Prop Address: & TMady4g8qST1QcVR9VA5N56ED9kVDm8NbA8 \\
Theory Prop Id: & 2865cfc1f9a346744761d36b1b8ffe1def60d3f92967f64caf2bdd6621484595 \\
Theory Prop Address: & TMYMRVL2d8FLeABGAFvksAq5e8LTs37M9U5
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfgdpfdd} ${{6}\unicdcdgdad{3}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 03fcc4b85dfade6c906248f8f17bb4e90da92e6bc4bd7dae07dc87b1c793cafc \\
Pure Prop Address: & TMZhLzSJKhPJ6LW7S8RESbikoubnNwygd8E \\
Theory Prop Id: & 1ffa21cb3a06b988a3518b1986f09cebcda356923bb17b459190071df400c1fd \\
Theory Prop Address: & TMdSxgcJr8YTuZy9uTgG9ajdHdm6pAfiETZ
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfgdpfed} ${{6}\unicdcdgdad{4}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0ebd5de52c3bf03fa06ad9a52177c94376ac6d6d21e4f7eec2ae524c20eb865a \\
Pure Prop Address: & TMYRPQnnTxR6J8VzzoFmHbqoXkGa3GgD775 \\
Theory Prop Id: & b3e48dff2905f986f3b5caced5a64dcd7234bfbc66ef0306f80725cd1ece61c7 \\
Theory Prop Address: & TMbKF48GnbjUBGJE9sw73TPmMcB8d19vTHv
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfgdpffd} ${{6}\unicdcdgdad{5}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & e3c546719f53e598755a05b44ff1592522513e88eab553a3118e5486a81ed067 \\
Pure Prop Address: & TMYY56rp3pu1Md2tx7cYLemwdM1mR5gcmwn \\
Theory Prop Id: & f44366e0c31269b36c404d0c744fe0d1b9ff6021d8c4b58406adb81f5b1c2657 \\
Theory Prop Address: & TMdM2SjU46csQY7mCoKywbHX9m8H2pRDGvc
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfhdpfad} ${{7}\unicdcdgdad{0}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f1aca13486b782dc00a51c22a046ddf10b9e5b6024aa2d8487df4668d134ad21 \\
Pure Prop Address: & TMTpLW3ApNNyU9zRQ4a5vLvH6GvaG3hDZsw \\
Theory Prop Id: & 04777e1121acde4051c1076405353442ecc7c841d8f5b1e282a7bbc610a446dd \\
Theory Prop Address: & TMakKfA3Sv9UTsXeCRpShgJQ4dUnFkNenjx
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfhdpfbd} ${{7}\unicdcdgdad{1}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 7f68ac2aa17e9e283bde82aaa6848151f8aae61ca586307fee893ae0535713a5 \\
Pure Prop Address: & TMQ5xCGH582yDx55yDN51RKxK9oZ7i3pmXr \\
Theory Prop Id: & c517bd071cddfea2ce1c10f9a4334e27e7bb4cf04db904a41ccb36e001fe703d \\
Theory Prop Address: & TMMMZYiwPgt5qwiuqAdeUwY2qzRX4uwcTBy
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfhdpfcd} ${{7}\unicdcdgdad{2}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & e915b85aabc6ff55b599e8b765d9d05c01d9dda3408fd4fa0a9833c8f62024b5 \\
Pure Prop Address: & TMbBFKirdwXXTLhAyJKum1V8XdNj5BBozBE \\
Theory Prop Id: & 719b90b534d821a74d146a517ec28b80f23cdcc8ebf4522af7dfd48863cb4fa8 \\
Theory Prop Address: & TMFfMwPwBr11dsiDFnzdKdva5FgSwooFhKZ
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfhdpfdd} ${{7}\unicdcdgdad{3}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & bc468ab5a647c84bfe1cbf2177bddf3cd9dcbed388c41930e8429925a62165e5 \\
Pure Prop Address: & TMLWnYbD25mqPFYupL6Lc7hitrjdJcfniuS \\
Theory Prop Id: & 7c0147f7e0c5d264d821868156432da25efcb90102666d5c3d25e4e52d14e374 \\
Theory Prop Address: & TMLUE8BbNrawrU1x36jKypY1Hc7Dh9sTeBx
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfhdpfed} ${{7}\unicdcdgdad{4}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0241dc3875c580942490118be9d0c699ec0514fe9d772ea7a904789477d54238 \\
Pure Prop Address: & TMGN51cm5R9iSyp1WjfR5ejM1X6VgXfxqwX \\
Theory Prop Id: & b83dd2a8b6844c39918736d4bb65dae6cac7b407b3e1d7f856124a1b8c8b1bbb \\
Theory Prop Address: & TMczss8yk3mckgdGRz59sXdSgkJJAmtAG5j
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfhdpffd} ${{7}\unicdcdgdad{5}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0d6c1682fbca7a87f757e77ddd09c5bb907565625c9bb3bd4d4106f080d57fc6 \\
Pure Prop Address: & TMRiUm9T8u2HUSVqbxBbzUpwb8M5kpBY8y9 \\
Theory Prop Id: & 2c37cdd7efc305b90d6607a132b9b9dd842317e03383654b67242cd93c5a9abe \\
Theory Prop Address: & TMNyRaG3YG1Vk3iDDYuv3o2c1VCAw8DviHL
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfhdpfgd} ${{7}\unicdcdgdad{6}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0d1fd098069d41630b89611eb93f1f08bce1c36d9c813d078d3d146904cdd42f \\
Pure Prop Address: & TMdEyrS1cfBLmsvCe812P4oyjUa3LvHoT5m \\
Theory Prop Id: & 7b8e224d3ff812c0454afa567fe7c3949fb0d82d46543a26c9e7ca9d51dd332e \\
Theory Prop Address: & TMdRvdFMDC1LW6RXkFfr25AGkBNkYkv7Mt1
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfidpfad} ${{8}\unicdcdgdad{0}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & e3931d2d8a8848d0d9ee64433a011a9aa4a51737fbdb5b7ff75eda148be9a459 \\
Pure Prop Address: & TMMdAqero4SC35AeBiqqtuQEkyo6rgyk4ti \\
Theory Prop Id: & 30657128da01d2a236a2d6ddcc73e1f8049084468c98dd69a2605d082c526bb1 \\
Theory Prop Address: & TMSNjV8GGDiVXMRQBxvQkSYEkGBVdZjVjFm
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfidpfbd} ${{8}\unicdcdgdad{1}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 6a16eeb33a53075e488dca90100eb48cca90e3c02804aed2943df9da34c76b07 \\
Pure Prop Address: & TMU2yPgAvkUoBCYpDgKoFG8xJAzksaqUjrV \\
Theory Prop Id: & 3fab0e9aef535966602b629d8b325e7d4fcc22fddae36170ebb822bab8fe78f2 \\
Theory Prop Address: & TMPHMdwsKTGixUr9ovcL92TPpNn2DZ59xR3
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfidpfcd} ${{8}\unicdcdgdad{2}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 9f7e3d7052052f039493deaa72664346f98b44644d5ce8e1d6b29f702756dc87 \\
Pure Prop Address: & TMHiEy2g7ytqLkCShdFDkQrHwAxrHLJ4ewz \\
Theory Prop Id: & e34cd1607418d341f87f72d6c64acebcadb8c4c22064d081a9a312fa6ea07e26 \\
Theory Prop Address: & TMKa84jucjzdciZ6ZrGg7jbnwmESXpiuuyX
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfidpfdd} ${{8}\unicdcdgdad{3}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 338f0e75ea4c6be85d54aac86da1fd615b97b42931170925c246bdb4ead8b0c7 \\
Pure Prop Address: & TMXDqEySQWNgPDXaxytYNRxHDU8nnVJBQmE \\
Theory Prop Id: & c0304effdb21f61184bffd799d5816aa2c736176a0f60054faf868b3e0667412 \\
Theory Prop Address: & TMcMdW4UMw76zq4HEXEdz38xzdN3uEfNvfU
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfidpfed} ${{8}\unicdcdgdad{4}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d95ab6bf4885a62645e050411d3dc149b0c30553a1b11777fb9626b5056dd31a \\
Pure Prop Address: & TMZ1C39y5oktaYiujD5mMcSng5NPSLJeEQz \\
Theory Prop Id: & 626b967685fe040cf728abce59c8526d52b9320642a11332b64fb176654bcba1 \\
Theory Prop Address: & TMdUEjMQYbenfRooZ94bsLXZekKQw7AwjpY
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfidpffd} ${{8}\unicdcdgdad{5}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 3582f2a69391c993ecc9217f73540497ab0af13613233acff03d6d05999a68b9 \\
Pure Prop Address: & TMNQpkxEPyJb6YgZiPPBGZQ9GbC7g7hb3TA \\
Theory Prop Id: & f8515d4c2c16dac9f1318ebd500262d8f6382c1822da217b3713dd322b505844 \\
Theory Prop Address: & TMK22UzEck1xp8U1jNqX9wkEh8eNg2kiLgv
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfidpfgd} ${{8}\unicdcdgdad{6}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 15c47f6efea919c6469a2b32df126c3a593df8a81ab4ebc5df17a98087ebf8e6 \\
Pure Prop Address: & TMcBgaEvvTaTaTDaifgkFsjxZQsqU4WzYoY \\
Theory Prop Id: & f5b7bf37bd7435e07a0b28d0a188937c24f605630a543a4e882d91a080499e2a \\
Theory Prop Address: & TMM574yv9Ufaw1F3N1jvDPpcg9GNzrTpYD6
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfidpfhd} ${{8}\unicdcdgdad{7}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 8d3267526667c8bc389f97552b72f511aec9f5f758b6ffb5677e384888680a6f \\
Pure Prop Address: & TMSmpMULYdUBC4xMvaX48vBU8PW3G6mmegc \\
Theory Prop Id: & 4f0658fb5c5f798e5218782be81c0fc926d764645d937e30bf2af1ae4d64d8f2 \\
Theory Prop Address: & TMLSfV5KwoLtB3AyRu1AQrfTfXfUQMcVAmW
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfjdpfad} ${{9}\unicdcdgdad{0}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 7fad6a4021cfaad3cd966f9db7cbc322601a15b27f7bebd190db92d9227d7d9d \\
Pure Prop Address: & TMYqJFCaupzUjNDmU955uhVqnu4ij9Mkuyn \\
Theory Prop Id: & 6e3ac6edcc976b5d4163e1e746d46f422f0f0916bd84e45ef0045db9d55d4c19 \\
Theory Prop Address: & TMKrgJnjKmPUDz3Ei1FeB8qAqPZq38H7jTb
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfjdpfbd} ${{9}\unicdcdgdad{1}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d87ea84c9c5771eec45a1fd14ad9153c2ddcdc39dae8e258585d43f60d51fc0d \\
Pure Prop Address: & TMJggtzHrkHQuUoShHgUHjqXcPh3YDT7pN1 \\
Theory Prop Id: & 80c63319a6d1e1304573edb4dae25f062780f4a278368ab2d11ffeb00f49b7c6 \\
Theory Prop Address: & TMcbAZhdMU2jbnR5osTzLG3UcaHdNK1HoSu
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfjdpfcd} ${{9}\unicdcdgdad{2}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & e2f4a18541452ebc1ff6a767768646cff4511a43dacb70dc53eb524adbacf071 \\
Pure Prop Address: & TMW6fNB5sUi4nGQoEwhzSpZyo1Y1LXDN1Ax \\
Theory Prop Id: & 906ccd2680d9bcd663a9b598d0e0b69b8c88fbeaa778ec48beaa22ea36b6f5b6 \\
Theory Prop Address: & TMWS25pQtSvRUgzYu1ZiDeYaCbk35nSzVQb
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfjdpfdd} ${{9}\unicdcdgdad{3}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & c17c1de4ec497af0fe4297a258d7a7c3d135e22ec81c834e7c9a96add5cccf55 \\
Pure Prop Address: & TMcK89BgzJhDbNna2LzUzWNiyoYx6z5zftc \\
Theory Prop Id: & d46f51d9a1c08f9230e9eb18a81e934945d4012ad2dbe5e8e979e80e9c2d0a15 \\
Theory Prop Address: & TML3NJwKxkRE2ZwqumY1ptX5orP6hMULsaL
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfjdpfed} ${{9}\unicdcdgdad{4}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & b2be6a2b14079f391b61f0f2c994e6c1f83f55f33e48888f5714fe2885e624f7 \\
Pure Prop Address: & TMG2u9oAHq7WMiN9fonJks9eiAQRK26GM6C \\
Theory Prop Id: & b136fba6a8b8fe9273ffb6386834de99d159f7c0ebb273ae030c99bdb951d513 \\
Theory Prop Address: & TMUecGRuCAeSZwXfRoh3G38RVvj1529JShy
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfjdpffd} ${{9}\unicdcdgdad{5}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & b1aaed7edfc0b04b990d933a7c324285c4e528683b5444ae62b5f6a6a1fea631 \\
Pure Prop Address: & TMWqKkpLGp13Tno4pYWFNtmRzmAH8WgKrKw \\
Theory Prop Id: & 0ae3b202241c8b6489ff2afc286f400f7db9f53d731d7c5c96fbc5157b8f2546 \\
Theory Prop Address: & TMUn176msQ6tprqPwqSfnayaBTxnWVJfjxL
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfjdpfgd} ${{9}\unicdcdgdad{6}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & b0286fd9ca576d16fe9d5933787a03791678ce168ecfef6360c216512ecbe419 \\
Pure Prop Address: & TMYwbNuQhDPUxShjx7H2boyojGDg8rAw8MU \\
Theory Prop Id: & 19a02fe5d8602e59495deff9213cd8d10a5cc30204dadfbad1f34d1f0fad400f \\
Theory Prop Address: & TMbZ1StXWmE3GzbtLteGPhs8Bh7HEHWxABd
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfjdpfhd} ${{9}\unicdcdgdad{7}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & aa22ad31d3f91e04f56851635a9322d13c23e3854cf45c973dea5a3cd0990b88 \\
Pure Prop Address: & TMXRgW5zUyKotMqQa3YaGwUZ6vFLUNEzUV9 \\
Theory Prop Id: & ff267fe87e45aca713d50f6e46c11d032357b90dc7acb206e3eefd8d01d36e82 \\
Theory Prop Address: & TMRwAzgMNqVuBgS6WGFdfKaAwYzx2HWCZgu
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ogfgbhpfjdpfid} ${{9}\unicdcdgdad{8}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 552eeb72bea999741bbc3cfc4807d1e73d2669cb5a06966cd70231206647a992 \\
Pure Prop Address: & TMRjxiyZgHvxgNtxTc3rKqKfBHHQ3fpUnty \\
Theory Prop Id: & e47272afbed4b7d1b148ec0b93566130bd83c0c213facce0dfa529c59ee5d182 \\
Theory Prop Address: & TMXoTBB5rYLbYrboKc4G2FzdBcPPXa5C9uF
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:dffhcgbhpfbdpfdfjgoghgad} ${{1} \subseteq {\{{0}\}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & aeae9a39918acd52e99e4648ef2ce22082b14cdb7f056833b3c9b6c7b08071bb \\
Pure Prop Address: & TMd1acsG4T47vanN7AeZN9GBKVvieBkvmww \\
Theory Prop Id: & abab2d4437158699c98b6dc7b4a1d462e539047454145838ea1260d68fc49944 \\
Theory Prop Address: & TMbUJrpN4q3Hv8rt9wMEJobfB2VW2EKtT8g
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:dffhcgbhpfdfjgoghgadpfbd} ${{\{{0}\}} \subseteq {1}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & cd786497c06a79d7f8391817754ef67063326d18ddbf160ab5ed1c22c0a322eb \\
Pure Prop Address: & TMZDF4AA5AbafCq1V1cfLd6D4iDMcgeXjr5 \\
Theory Prop Id: & 1806bf9a09183656922b1ceb29490f6cc9898d3b353ad377a7e13edd309c7791 \\
Theory Prop Address: & TMHq3pPKYpd4KhjT9PUsaM9T7pKh9PDKCDK
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgbhpfbdpfdfjgoghgad} ${{1}={\{{0}\}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 5e59965f8dea2376b44a4645087aa7b0fb447c5e0b32fdfa0a419f8c6730821f \\
Pure Prop Address: & TMM87nnYFzft3WcRjLweo3mTQXoJfb1o2yT \\
Theory Prop Id: & 264f38ba2201bb27cd34ae54a896eda9cfb3191811b417511fd59a42a1aad583 \\
Theory Prop Address: & TMJZ4wN5mJDvtTGG8T4dkZwXYestYUa7nSE
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:dffhcgbhpfcdpfffafbgjgchadbd} ${{2} \subseteq {\{{0},{1}\}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d908841bebc314441f7259cb1ae1e06c95ce753fde5f00fc59b6dde11d4d93c1 \\
Pure Prop Address: & TMHVo8N2YAFhqLdCesUKneKkycAMCjufnxX \\
Theory Prop Id: & 94203e1d2b2c0faaa1b53b57d6e02377ba6909bbad4345113cca6c3b30ffc6c2 \\
Theory Prop Address: & TMdUkY7ub8vSPAiJMtCVLRMpJmEeZvULcKe
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:dffhcgbhpfffafbgjgchadbdpfcd} ${{\{{0},{1}\}} \subseteq {2}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a855482b832c8ea776aa01316555b8b83b59d1577d45ef4b5d123674420d0e01 \\
Pure Prop Address: & TMGfNJyPsWS2KxUk5KVgkcMQB4XboikFQcH \\
Theory Prop Id: & 0095605b59f5d2bbd6d2ac9dc6c80902a1f7530a558319eac4bd5e1225e3059a \\
Theory Prop Address: & TMYm6neMj3cdSovA76Sn3Rzr22vfiLnJrMu
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:fgbhpfcdpfffafbgjgchadbd} ${{2}={\{{0},{1}\}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & da80075027dc7a68c335dc91d0d1e2008733d49f594a4654f4808a72f790fe18 \\
Pure Prop Address: & TMTAkWeRWfntW6KcrRUzppdf93RSZBsj2kq \\
Theory Prop Id: & 7ae5a1ab159f51b92a97a85e8382349a9ddca06dc5c2f387f58ab6cada7ddc8d \\
Theory Prop Address: & TMd33UnmSrxCctoLEbFMBCqkF1i4pvM11uq
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchegjgogbgmgpfjgogeg} ${\unicdcdadad p : {{\iota}\unicdbdjdcd{o}} .  {{({\unicdcdadad alpha .  {{{\mname{ordinal}}~{\alpha}}\unicdbdjdcd{{({\unicdcdadad beta \in {\alpha} .  {{p}~{\beta}}})}\unicdbdjdcd{{p}~{\alpha}}}}})}\unicdbdjdcd{\unicdcdadad alpha .  {{{\mname{ordinal}}~{\alpha}}\unicdbdjdcd{{p}~{\alpha}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & bb557547876580348d1b27707e8329c129045f75384f6cfee3b6b3660d679f76 \\
Pure Prop Address: & TMMjF9N5BddMz7dZjRy3jb2edCyq6JxUnjh \\
Theory Prop Id: & 973cd8ebf285141bb206385be0589deb9b0d2b22f4291d4f8935767e2c8d72f7 \\
Theory Prop Address: & TMHyu4a19t1LKmHrnT3eDCrBexiXHK9SKmm
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:mgfgbgdhehpfpgchegjgogbgmgpffgih} ${\unicdcdadad p : {{\iota}\unicdbdjdcd{o}} .  {{({\unicdcdaddd alpha .  {{{\mname{ordinal}}~{\alpha}}\unicdcdcdhd{{p}~{\alpha}}}})}\unicdbdjdcd{\unicdcdaddd alpha .  {{{{\mname{ordinal}}~{\alpha}}\unicdcdcdhd{{p}~{\alpha}}}\unicdcdcdhd{\unicdcdadad beta \in {\alpha} .  {\preoh{{{p}~{\beta}}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & df6c7763ab1d598ac956e39f705674757a597eb43301218c4a0cf210679e8487 \\
Pure Prop Address: & TMR2LGsWB47Dd2V32aJMtRmhkcuHkb32B5c \\
Theory Prop Id: & ab6fe147dcaf15113c3482aa2b52e2418ef973d6f5f9ad0df1e81a91ac34fd0f \\
Theory Prop Address: & TMWujpqPswYN98tJhWJajsNjSmNit3C1wxB
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchegjgogbgmgpfehchjgdgigpgehpgngjhpfpgchpfjgngahchfgeg} ${\unicdcdadad alpha beta .  {{{\mname{ordinal}}~{\alpha}}\unicdbdjdcd{{{\mname{ordinal}}~{\beta}}\unicdbdjdcd{\unicdcdadad p : {o} .  {{({{{\alpha} \in {\beta}}\unicdbdjdcd{p}})}\unicdbdjdcd{{({{{\alpha}={\beta}}\unicdbdjdcd{p}})}\unicdbdjdcd{{({{{\beta} \in {\alpha}}\unicdbdjdcd{p}})}\unicdbdjdcd{p}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 7c0f0bd46025b48ff67a7143c3e4a076e5e080c3c720416d50d3fda07959571a \\
Pure Prop Address: & TMbyFsACnhcNuinkiWbTRsyq9Xw7dG3yxen \\
Theory Prop Id: & bb6d2d91d4ebfae062a8c9b008250ab6b380ac9e09ebf6e8ec9dfd01afcfc71b \\
Theory Prop Address: & TMX8gEh9epaBjfv8Rid5iBE5GnLWmimvYwE
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:pgchegjgogbgmgpfehchjgdgigpgehpgngjh} ${\unicdcdadad alpha beta : {\iota} .  {{{\mname{ordinal}}~{\alpha}}\unicdbdjdcd{{{\mname{ordinal}}~{\beta}}\unicdbdjdcd{{{{\mname{exactly1of3}}~{({{\alpha} \in {\beta}})}}~{({{\alpha}={\beta}})}}~{({{\beta} \in {\alpha}})}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 2230cfc37c714b9145baabb918487c4c4cb9582cb14de24bf562f395dbffef9e \\
Pure Prop Address: & TMUJTrRxNbofUZ7cPQahpGQK3QFoP7UEpr5 \\
Theory Prop Id: & 72667378ef8d960e362a49147b9f82d2da940398bc2f4f035524457ddae3b011 \\
Theory Prop Address: & TMadvrwG2zGWUTUNaw1gN8KJ6gPMX3d1LQJ
\end{tabular}
\end{center}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

\end{theorem}
