\chapter{Natural Numbers III and Ordinals}
\begin{verbatim}
PigeonHole_nat
\end{verbatim}
\begin{theorem}\label{thm:afjghgfgpgogiepgmgfgpfogbgeh}
  $$
  \begin{array}{c}
    \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}}}})}}.
  \end{array}
  $$
  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{verbatim}
PigeonHole_nat_bij
\end{verbatim}
\begin{theorem}\label{thm:afjghgfgpgogiepgmgfgpfogbgehpfcgjgkg}
  $$
  \begin{array}{c}
    \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}}.
  \end{array}
  $$
  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{verbatim}
cases_7
\end{verbatim}
\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{verbatim}
cases_8
\end{verbatim}
\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{verbatim}
cases_9
\end{verbatim}
\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{verbatim}
nIn_2_1
\end{verbatim}
\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{verbatim}
neq_6_0
\end{verbatim}
\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{verbatim}
neq_6_1
\end{verbatim}
\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{verbatim}
neq_6_2
\end{verbatim}
\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{verbatim}
neq_6_3
\end{verbatim}
\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{verbatim}
neq_6_4
\end{verbatim}
\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{verbatim}
neq_6_5
\end{verbatim}
\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{verbatim}
neq_7_0
\end{verbatim}
\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{verbatim}
neq_7_1
\end{verbatim}
\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{verbatim}
neq_7_2
\end{verbatim}
\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{verbatim}
neq_7_3
\end{verbatim}
\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{verbatim}
neq_7_4
\end{verbatim}
\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{verbatim}
neq_7_5
\end{verbatim}
\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{verbatim}
neq_7_6
\end{verbatim}
\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{verbatim}
neq_8_0
\end{verbatim}
\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{verbatim}
neq_8_1
\end{verbatim}
\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{verbatim}
neq_8_2
\end{verbatim}
\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{verbatim}
neq_8_3
\end{verbatim}
\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{verbatim}
neq_8_4
\end{verbatim}
\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{verbatim}
neq_8_5
\end{verbatim}
\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{verbatim}
neq_8_6
\end{verbatim}
\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{verbatim}
neq_8_7
\end{verbatim}
\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{verbatim}
neq_9_0
\end{verbatim}
\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{verbatim}
neq_9_1
\end{verbatim}
\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{verbatim}
neq_9_2
\end{verbatim}
\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{verbatim}
neq_9_3
\end{verbatim}
\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{verbatim}
neq_9_4
\end{verbatim}
\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{verbatim}
neq_9_5
\end{verbatim}
\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{verbatim}
neq_9_6
\end{verbatim}
\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{verbatim}
neq_9_7
\end{verbatim}
\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{verbatim}
neq_9_8
\end{verbatim}
\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{verbatim}
Subq_1_Sing0
\end{verbatim}
\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{verbatim}
Subq_Sing0_1
\end{verbatim}
\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{verbatim}
eq_1_Sing0
\end{verbatim}
\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{verbatim}
Subq_2_UPair01
\end{verbatim}
\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{verbatim}
Subq_UPair01_2
\end{verbatim}
\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{verbatim}
eq_2_UPair01
\end{verbatim}
\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{verbatim}
ordinal_ind
\end{verbatim}
\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{verbatim}
least_ordinal_ex
\end{verbatim}
\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{verbatim}
ordinal_trichotomy_or_impred
\end{verbatim}
\begin{theorem}\label{thm:pgchegjgogbgmgpfehchjgdgigpgehpgngjhpfpgchpfjgngahchfgeg}
  $$
  \begin{array}{c}
    \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}}}}.
  \end{array}
  $$
  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{verbatim}
ordinal_trichotomy
\end{verbatim}
\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}
