\chapter{Pairs, Sums, Functions and Products}
\section{pair\_setsum}\label{ahbgjgchpfdhfgehdhfhng}Let $pair$ be ${\mname{setsum}}$.
\begin{verbatim}
pair_0_0
\end{verbatim}
\begin{theorem}\label{thm:ahbgjgchpfadpfad} ${{{{pair}~{0}}~{0}}={0}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 5dcaebebb574103d0edf890d85e23a5fa97b59db661795af9daeb7aa65f336a4 \\
Pure Prop Address: & TMaVr4aCWi6koabmAQVJ2wQdpL7mC7foUu9 \\
Theory Prop Id: & 4f3651b8f623daa8b048a8735ce8791d53d3c1d1b0f2aa681c537176ab51a619 \\
Theory Prop Address: & TMHtDbLm7fFXE2PBw9a9TaKFqUT1oKq4DFj
\end{tabular}
\end{center}

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

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

\end{theorem}
\begin{verbatim}
nat_pair1_ordsucc
\end{verbatim}
\begin{theorem}\label{thm:ogbgehpfahbgjgchbdpfpgchegdhfhdgdg} ${\unicdcdadad n : {\iota} .  {{{\mname{nat\_p}}~{n}}\unicdbdjdcd{{{{pair}~{1}}~{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{definition}\label{def:ahchpgkgad}
We define $\mname{proj0}$ to be ${\uniddcgcg Z .  {\{{{\mname{Unj}}~{z}}|z \in {Z}, {\unicdcdaddd x : {\iota} .  {{{\mname{Inj0}}~{x}}={z}}}\}}}$ of type ${{\iota}\unicdbdjdcd{\iota}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 21a4888a1d196a26c9a88401c9f2b73d991cc569a069532cb5b119c4538a99d7 \\
Pure Object Address: & TMJAVsjow6vGiHhjkrvQ3hFGbgbvS9xcWyV \\
Theory Object Id: & 9c5e4e6be64531b8ea143c51d4eae82a384c81ad95f7a944e1c670a8a30da3b9 \\
Theory Object Address: & TMaHY5KSgmVdGVqgzTcQgf4sHUsLLKmvAny
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:ahchpgkgbd}
We define $\mname{proj1}$ to be ${\uniddcgcg Z .  {\{{{\mname{Unj}}~{z}}|z \in {Z}, {\unicdcdaddd y : {\iota} .  {{{\mname{Inj1}}~{y}}={z}}}\}}}$ of type ${{\iota}\unicdbdjdcd{\iota}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 7aba21bd28932bfdd0b1a640f09b1b836264d10ccbba50d568dea8389d2f8c9d \\
Pure Object Address: & TMaSYWTJtnhHMswCbUGaheomcukAYucQua4 \\
Theory Object Id: & 7fd81e3c066cdbca377abd70b13843fd894f77ad69e67cf26842b8bc147db710 \\
Theory Object Address: & TMPJv5Do7FeQVBbPTL9ZY9H9YGMGpRV652o
\end{tabular}
\end{center}

\end{definition}
\begin{verbatim}
Inj0_pair_0_eq
\end{verbatim}
\begin{theorem}\label{thm:jeogkgadpfahbgjgchpfadpffgbh} ${{\mname{Inj0}}={{pair}~{0}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0fe60101f9b90226a3183f7eee66d492a07dd05cb531e7baf46d3ab4302ca05f \\
Pure Prop Address: & TMVm4GBpHVCYV2pJB5HL2QNkHnuSGWZ9qAh \\
Theory Prop Id: & 490c2a25a7dca847f40f638f694a872a3f6f47d42aea7867c086f2c4cf3f6988 \\
Theory Prop Address: & TMNdMHTR5f8Y73jbhAeJgaesKTmGkru7yzB
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Inj1_pair_1_eq
\end{verbatim}
\begin{theorem}\label{thm:jeogkgbdpfahbgjgchpfbdpffgbh} ${{\mname{Inj1}}={{pair}~{1}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0bbde85d4f9a32c3b689bb6a75b3954d57abb296cbd0aa2745de678af1df9a59 \\
Pure Prop Address: & TMPgPyPUzWL2JW9oss4msqgSCZ6zCy2Ztc1 \\
Theory Prop Id: & 8272d79377fa78cbfc8589d848b8f5e3862c8d19e10dd47a58c6bea9d16d8447 \\
Theory Prop Address: & TMNjuSVZSzPL5H7zv2hTWCGkBLDksUvykJN
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
pairI0
\end{verbatim}
\begin{theorem}\label{thm:ahbgjgchjead}
  ${\unicdcdadad X Y x .  {{{x} \in {X}}\unicdbdjdcd{{{{pair}~{0}}~{x}} \in {{{pair}~{X}}~{Y}}}}}$.
  The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 21a4141f1e8cac366335c6139b8e6f6c143e493b4b78e1106e78e213967caf29 \\
Pure Prop Address: & TMPWuPuKr4fNYduR2p8k1ib9xWvBLuRs4wX \\
Theory Prop Id: & 34813b26053e164b7ed43057b6f8ee6ff0cd96d01f5b6401b42ceae658468e01 \\
Theory Prop Address: & TMNQzaX8ZiddhSn6QTSqc1McYEwNG1Fe8wT
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
pairI1
\end{verbatim}
\begin{theorem}\label{thm:ahbgjgchjebd} ${\unicdcdadad X Y y .  {{{y} \in {Y}}\unicdbdjdcd{{{{pair}~{1}}~{y}} \in {{{pair}~{X}}~{Y}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & bdaab525a50b9c2d070e4f67b9e4b3b931b06622695aa3c0f0b51683e1905bc7 \\
Pure Prop Address: & TMbhSedKYd5RyPq2mELrEkTMb7JkqLqrGWh \\
Theory Prop Id: & b5248b96fbd2dbc9c65f96e27bfae42798a39bc110034aa9dcc82afc9fe0056a \\
Theory Prop Address: & TMM3oDhF32usrf43sjdNDwEZbSftUuY8cjh
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
pairE
\end{verbatim}
\begin{theorem}\label{thm:ahbgjgchfe}
  $${\unicdcdadad X Y z .  {{{z} \in {{{pair}~{X}}~{Y}}}\unicdbdjdcd{{({\unicdcdaddd x \in {X} .  {{z}={{{pair}~{0}}~{x}}}})}\unicdcdcdid{({\unicdcdaddd y \in {Y} .  {{z}={{{pair}~{1}}~{y}}}})}}}}.$$
  The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & aac6108d214baf821b35d72218cb0b4f9e63fc00aecbbb7a4ce9bcbb8a21b941 \\
Pure Prop Address: & TMUqfs3rToFZZEUcGSfnRKkNmLL7jyk7GqJ \\
Theory Prop Id: & 0afdeb4f80887eb047d9b590fad88a119cbb419efa9edfb46ab666e1282c8fd4 \\
Theory Prop Address: & TMJLCz7nFpUma4iUHHjfnc85LCDmaCUqtN2
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
pairE0
\end{verbatim}
\begin{theorem}\label{thm:ahbgjgchfead} ${\unicdcdadad X Y x .  {{{{{pair}~{0}}~{x}} \in {{{pair}~{X}}~{Y}}}\unicdbdjdcd{{x} \in {X}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 042f308329163b02cbbc55bb0027f0352880a98c06f8ab271eadf3ec5e9f04e3 \\
Pure Prop Address: & TMJeqsKVgs3VYVeCG9rGS4ZNKAdR8nTs38m \\
Theory Prop Id: & f50b255d63e6dbed7324927c7b1afe6317eea22dbd269f2a5b27d6f6565c5445 \\
Theory Prop Address: & TMLQ2VeBqCmuyodmpqK5dmQM5s98wqPSfk2
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
pairE1
\end{verbatim}
\begin{theorem}\label{thm:ahbgjgchfebd} ${\unicdcdadad X Y y .  {{{{{pair}~{1}}~{y}} \in {{{pair}~{X}}~{Y}}}\unicdbdjdcd{{y} \in {Y}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 505cfcb3d7610169f4bfa8ba33596724c69138cb7d875cad9a309a91e2402eb6 \\
Pure Prop Address: & TMcH1uWQFgoCUsZbTGyxzwk17PtdC9cvCA6 \\
Theory Prop Id: & 30a181bf14bf2566fdcf937c9b42f3512a8a40f569e90dc2aef4aa7ae0db9e24 \\
Theory Prop Address: & TMQgeZWRp9TKUwYNKVDSo4jYfniQaLPJzRY
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
pairEq
\end{verbatim}
\begin{theorem}\label{thm:ahbgjgchfebh}
  $${\unicdcdadad X Y z .  {{{z} \in {{{pair}~{X}}~{Y}}}\unicdbdjded{{({\unicdcdaddd x \in {X} .  {{z}={{{pair}~{0}}~{x}}}})}\unicdcdcdid{({\unicdcdaddd y \in {Y} .  {{z}={{{pair}~{1}}~{y}}}})}}}}.$$
  The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 98d332f11ba6fc7f438c81b60a59777921748d69f214c8a1788cc4374ca7f53b \\
Pure Prop Address: & TMVrjFeVrNRrLEwuGQPfHQJgGH3nN34D2yd \\
Theory Prop Id: & 65c2d317407da943881beedf59fac794f29f668a2676e85d7c1d17f0f0f1c0ca \\
Theory Prop Address: & TMRyemtQaJ4VgBEH4b2NuAukq6NEzdWuaof
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
pairSubq
\end{verbatim}
\begin{theorem}\label{thm:ahbgjgchdffhcgbh} ${\unicdcdadad X Y W Z .  {{{X} \subseteq {W}}\unicdbdjdcd{{{Y} \subseteq {Z}}\unicdbdjdcd{{{{pair}~{X}}~{Y}} \subseteq {{{pair}~{W}}~{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{verbatim}
proj0I
\end{verbatim}
\begin{theorem}\label{thm:ahchpgkgadje} ${\unicdcdadad w u : {\iota} .  {{{{{pair}~{0}}~{u}} \in {w}}\unicdbdjdcd{{u} \in {{\mname{proj0}}~{w}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & be55b9a07966119a7062e99cbd0ce90614937b1321ad2f7982157399ef7cd51b \\
Pure Prop Address: & TMMvCe8JzDEJMj9cXvrha66rpRYMz5CKGJ1 \\
Theory Prop Id: & 840c8df1f99f4da23ec51cac3d8dc3d97931d9d67121464862c6504eec69245a \\
Theory Prop Address: & TMGtD6G4wVv2RV84KASZp4iaX1TDhDn2QMG
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
proj0E
\end{verbatim}
\begin{theorem}\label{thm:ahchpgkgadfe} ${\unicdcdadad w u : {\iota} .  {{{u} \in {{\mname{proj0}}~{w}}}\unicdbdjdcd{{{{pair}~{0}}~{u}} \in {w}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & b9afa9f543fc43d88abece7f6e50c4eb30c889faceb03f4deb53230d9fb540ba \\
Pure Prop Address: & TMQYzQmm1NFjQJzmtbAGu6ymzj9LF6Gx53A \\
Theory Prop Id: & 5b7f586d6ff9e7dda36e45b26ab54d9324d38494897913660be264154c751908 \\
Theory Prop Address: & TMKRt7H9e4QrANP7FuuuVFh5G963n269NGA
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
proj1I
\end{verbatim}
\begin{theorem}\label{thm:ahchpgkgbdje} ${\unicdcdadad w u : {\iota} .  {{{{{pair}~{1}}~{u}} \in {w}}\unicdbdjdcd{{u} \in {{\mname{proj1}}~{w}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & fbddb75c7d6c8d452a3849e8b97ab824ad9f6385bfaee6fab47eb8e903c72ff0 \\
Pure Prop Address: & TMMhHn9rASEBErsJ8RZqUMcdtgkQZHiTtjS \\
Theory Prop Id: & 595b3cca1eb4a87a06e1fac1e30ea2a8d161b87216b075cfab0ff0066f3025c6 \\
Theory Prop Address: & TMPGXMep9UXBiUhuNpo5MxyTNz4GnkUrTMz
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
proj1E
\end{verbatim}
\begin{theorem}\label{thm:ahchpgkgbdfe} ${\unicdcdadad w u : {\iota} .  {{{u} \in {{\mname{proj1}}~{w}}}\unicdbdjdcd{{{{pair}~{1}}~{u}} \in {w}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 06e32e59aafc4113d0d25461bbdd08d7d93a870dec775e19a9e48a763362b709 \\
Pure Prop Address: & TMTjqJpi2rtJW9qijp4JKmBpdTppjv1rP6f \\
Theory Prop Id: & c3c3e6c3e94f9e03aeb2b4f93e33744decc142ead482a1fa50a8767e7fc99638 \\
Theory Prop Address: & TMcN2J3tSopfuEz9NRL1jfvCCu5kxE2v2No
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
proj0_pair_eq
\end{verbatim}
\begin{theorem}\label{thm:ahchpgkgadpfahbgjgchpffgbh} ${\unicdcdadad X Y : {\iota} .  {{{\mname{proj0}}~{({{{pair}~{X}}~{Y}})}}={X}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d546f32a1c10eae38a9af6397e8d2af2759b1d0646a5f3d4868c51100c9e2395 \\
Pure Prop Address: & TMbPLyxLXKPkMnkdo72LQeKTjebPKPLSJmk \\
Theory Prop Id: & 0c12fbce603161ada7fcfdceb916aa8184711c821cd1e1b2326d5152dfe84499 \\
Theory Prop Address: & TMHWPP4mLNCpHEx7SiPwPaQi8HiEHdVrm9b
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
proj1_pair_eq
\end{verbatim}
\begin{theorem}\label{thm:ahchpgkgbdpfahbgjgchpffgbh} ${\unicdcdadad X Y : {\iota} .  {{{\mname{proj1}}~{({{{pair}~{X}}~{Y}})}}={Y}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 9f98a8d2797cf5bb49a476c118564c127ff5edcaea373b1ca114e096c594679f \\
Pure Prop Address: & TMLxPAuDd6Zdjkv16vcwxEZoxAdBz8adaQM \\
Theory Prop Id: & e0cb0f860b00c8c1dea60e21e3bab80b7213e7c2da3750ce479bd67ef1eee60d \\
Theory Prop Address: & TMM7LPbGJRfCrTrhXupSUxTM5PSBW4xxwqf
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
pair_inj
\end{verbatim}
\begin{theorem}\label{thm:ahbgjgchpfjgogkg} ${\unicdcdadad x y w z : {\iota} .  {{{{{pair}~{x}}~{y}}={{{pair}~{w}}~{z}}}\unicdbdjdcd{{{x}={w}}\unicdcdcdhd{{y}={z}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & c7ef9fe33c7c1572d541f409e082fd4867a3959389d1246ddb8c6e790550ad23 \\
Pure Prop Address: & TMEvDEchwftSTVQExszQAystHF4dFnXXiiV \\
Theory Prop Id: & 972ddf22ac0ad35ef54fbe2f14d3eb51f3932d2eb7c90de81cea04fd839a85b6 \\
Theory Prop Address: & TMTqqAmny9TT4MKV73TgCn5hxdYCZV3qB4j
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
pair_eta_Subq_proj
\end{verbatim}
\begin{theorem}\label{thm:ahbgjgchpffgehbgpfdffhcgbhpfahchpgkg} ${\unicdcdadad w .  {{{{pair}~{({{\mname{proj0}}~{w}})}}~{({{\mname{proj1}}~{w}})}} \subseteq {w}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a868f0131174256073ca2e69f0629c02909a5e8cddbddc8bf755c9d11a4fc8df \\
Pure Prop Address: & TMSF6AUrFFqfp7WqPsWnmZrPyBmHXMFBof5 \\
Theory Prop Id: & 9afd8b29c6f5307394a6a98ed81326ea8d0a1e58965e3886e0fcd87155aba943 \\
Theory Prop Address: & TMNSTW7wqZuPxSL1kuFRRghsCCu3eRTUUC1
\end{tabular}
\end{center}

\end{theorem}

\section{Dependent Sums}

\begin{definition}\label{def:dfjghgngbg}
We define $\mname{Sigma}$ to be ${\uniddcgcg X Y .  {\unicdcddedd _{x \in {X}}{\{{{{pair}~{x}}~{y}}|y \in {{Y}~{x}}\}}}}$ of type ${{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{\iota}})}\unicdbdjdcd{\iota}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 8acbb2b5de4ab265344d713b111d82b0048c8a4bf732a67ad35f1054a4eb4642 \\
Pure Object Address: & TMMDLyvQS3eoiP32KBXjSQyuvc4keN5yMmX \\
Theory Object Id: & d64bcbbefe13f9fc0035d2317f017d9ee3aeb3de90b836ed7cbe11d46f478799 \\
Theory Object Address: & TMS2X4GvB3DZiVdQjy5ZeDZQVVCDuJBZvgW
\end{tabular}
\end{center}

\end{definition}
{\bf{Notation.}} We use $\binddfjghgngbgpf x,\ldots,y  . $ as a binder notation corresponding to a term constructed using ${\mname{Sigma}}$.
\begin{verbatim}
pair_Sigma
\end{verbatim}
\begin{theorem}\label{thm:ahbgjgchpfdfjghgngbg} ${\unicdcdadad X : {\iota} .  {\unicdcdadad Y : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad x \in {X} .  {\unicdcdadad y \in {{Y}~{x}} .  {{{{pair}~{x}}~{y}} \in {\unicdcdbdbd x \in {X} .  {{Y}~{x}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0d8645a51ab956ff15d92813d2cab140e73529474636367747958b8e18bab905 \\
Pure Prop Address: & TML8ffdR3C51f2E9BMf7H2BS9S1rFurh827 \\
Theory Prop Id: & 1456cb5b576a7c97a2a8bc57c2896584b0d55dd30ca4212f1733b4c7ebe4f919 \\
Theory Prop Address: & TMaVj4zKhXkoLhyH11SzjuosBXYALhD49xN
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Sigma_eta_proj0_proj1
\end{verbatim}
\begin{theorem}\label{thm:dfjghgngbgpffgehbgpfahchpgkgadpfahchpgkgbd}
  $$
  \begin{array}{c}
    \unicdcdadad X : {\iota} .  \unicdcdadad Y : {{\iota}\unicdbdjdcd{\iota}} .  \unicdcdadad z \in {({\unicdcdbdbd x \in {X} .  {{Y}~{x}}})} .\\
                 {{{{{{pair}~{({{\mname{proj0}}~{z}})}}~{({{\mname{proj1}}~{z}})}}={z}}\unicdcdcdhd{{{\mname{proj0}}~{z}} \in {X}}}\unicdcdcdhd{{{\mname{proj1}}~{z}} \in {{Y}~{({{\mname{proj0}}~{z}})}}}}.
  \end{array}
  $$
  The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & afe96271dba741ef6022853ac10aa26abecb9b32d05c44f71e7c5089f782d778 \\
Pure Prop Address: & TMWpztGVWdAFQ1ovvNdLFx6cps617NMUj8f \\
Theory Prop Id: & 77ba8e9a2110bd246cbd0efc93c8437da7906392890ad5f4156a4e526a76a950 \\
Theory Prop Address: & TMY1GRBXj483wdHtvtfTD9uZNgUp8CAiaRD
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
proj_Sigma_eta
\end{verbatim}
\begin{theorem}\label{thm:ahchpgkgpfdfjghgngbgpffgehbg} $${\unicdcdadad X : {\iota} .  {\unicdcdadad Y : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad z \in {({\unicdcdbdbd x \in {X} .  {{Y}~{x}}})} .  {{{{pair}~{({{\mname{proj0}}~{z}})}}~{({{\mname{proj1}}~{z}})}}={z}}}}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 8b31cdfbbf34fe7c3b0423c153108eed30fc19b3ff82132f32fc21939416a2ef \\
Pure Prop Address: & TMJH9UNCBubGXwZc46iPvjZm3iBB1y6mfHu \\
Theory Prop Id: & f30f76cb2aef08be1838ea268e49d550fefb9694a95470f51dd35304cd46da86 \\
Theory Prop Address: & TMX4ChFaKVytLhSzjfKyAapz8j6LrbpcHM5
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
proj0_Sigma
\end{verbatim}
\begin{theorem}\label{thm:ahchpgkgadpfdfjghgngbg}
  $${\unicdcdadad X : {\iota} .  {\unicdcdadad Y : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad z : {\iota} .  {{{z} \in {({\unicdcdbdbd x \in {X} .  {{Y}~{x}}})}}\unicdbdjdcd{{{\mname{proj0}}~{z}} \in {X}}}}}}.$$
  The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & ae12a7b526c0a13cce84f529e93ced0f678ce1c9b63337256f2952f31af9eb47 \\
Pure Prop Address: & TMGDaF1fWHGqSd5NBBSVmU2WGERM8Yb3k9o \\
Theory Prop Id: & 50686996f47a43fc8b07a9886de2c8d44fb1f23e5ebe1c95ea71b5d7a06d274a \\
Theory Prop Address: & TMWkPywgVwGwhQpBQMdXhZTDgiXWekNhrCd
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
proj1_Sigma
\end{verbatim}
\begin{theorem}\label{thm:ahchpgkgbdpfdfjghgngbg}
  $${\unicdcdadad X : {\iota} .  {\unicdcdadad Y : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad z : {\iota} .  {{{z} \in {({\unicdcdbdbd x \in {X} .  {{Y}~{x}}})}}\unicdbdjdcd{{{\mname{proj1}}~{z}} \in {{Y}~{({{\mname{proj0}}~{z}})}}}}}}}.$$
  The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 553db6938c6f87c354d6c9209f682b09c73f8cbc2eb21ab6513fee7dd2092d35 \\
Pure Prop Address: & TMaYkGoHBN1iZiAYUVzJRZLn3EgRSQWrx1H \\
Theory Prop Id: & d79917b7b626dcc0902b44780a05f036fcf9f4445434650e2ea129fa0f955938 \\
Theory Prop Address: & TMFMACi6zbuVxKdSyevDC9cG2fhuphqdLvD
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
pair_Sigma_E0
\end{verbatim}
\begin{theorem}\label{thm:ahbgjgchpfdfjghgngbgpffead}
  $\unicdcdadad X : {\iota} .  \unicdcdadad Y : {{\iota}\unicdbdjdcd{\iota}} .  \unicdcdadad x y : {\iota} . {{{{pair}~{x}}~{y}} \in {({\unicdcdbdbd x \in {X} .  {{Y}~{x}}})}}\unicdbdjdcd{{x} \in {X}}$.
  The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & c4b4172cb06b68610331df0bff40a80e131c5fe7a0f37012432d5896d5e2c4a8 \\
Pure Prop Address: & TMa5xp6pY52DfG6pfd7VzRGhjHUWXTk87nR \\
Theory Prop Id: & 481fddcf7b10f918784064dcf83451596b1a8fec3423f6e7215608a7dccefb43 \\
Theory Prop Address: & TMRJQf5xNbV6uehrGdTPq6X4eyNfy3irJAQ
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
pair_Sigma_E1
\end{verbatim}
\begin{theorem}\label{thm:ahbgjgchpfdfjghgngbgpffebd} ${\unicdcdadad X : {\iota} .  {\unicdcdadad Y : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad x y : {\iota} .  {{{{{pair}~{x}}~{y}} \in {({\unicdcdbdbd x \in {X} .  {{Y}~{x}}})}}\unicdbdjdcd{{y} \in {{Y}~{x}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & c294a7d73a371c2ac828dbda009fa9e74a8b85adfe24c4731eb12086f8913b12 \\
Pure Prop Address: & TMMukS2p563YcLJwvCEj2kjfqr8z23JmFUE \\
Theory Prop Id: & 81d8b0d6136a1b697d4b5753d87fb42789104c2db7a89e6023100fcb32516c3f \\
Theory Prop Address: & TMWdjWXycEquBp15ycxwyeRHKb8YEFjrntf
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Sigma_E
\end{verbatim}
\begin{theorem}\label{thm:dfjghgngbgpffe}
  $${\unicdcdadad X : {\iota} .  {\unicdcdadad Y : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad z : {\iota} .  {{{z} \in {({\unicdcdbdbd x \in {X} .  {{Y}~{x}}})}}\unicdbdjdcd{\unicdcdaddd x \in {X} .  {\unicdcdaddd y \in {{Y}~{x}} .  {{z}={{{pair}~{x}}~{y}}}}}}}}}.$$
  The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 5b1bd2e14ea3dbf36ed03b2bca51d8d6329ffb7924a6198502c84e472877864e \\
Pure Prop Address: & TMKZhCQwWmLxNmtRGpKgTrmnpUbXzpUqcC6 \\
Theory Prop Id: & 8ecfabfede2e6f041d7ca7aa6d8ddc7d93e1d4a8f77164e302775838b170ef2f \\
Theory Prop Address: & TMHvzRUPwTDz6sNjr1Xu75jPe97kiKyiFRf
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Sigma_Eq
\end{verbatim}
\begin{theorem}\label{thm:dfjghgngbgpffebh} $${\unicdcdadad X : {\iota} .  {\unicdcdadad Y : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad z : {\iota} .  {{{z} \in {({\unicdcdbdbd x \in {X} .  {{Y}~{x}}})}}\unicdbdjded{\unicdcdaddd x \in {X} .  {\unicdcdaddd y \in {{Y}~{x}} .  {{z}={{{pair}~{x}}~{y}}}}}}}}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 49886b5979c9429dfa4b9590d2e5c308bccd95f87e7cc32f24dc682e35e497f8 \\
Pure Prop Address: & TMXKo25CKqXa5jWu42vnAgmVtNvhqv9e29Q \\
Theory Prop Id: & e7bf483e07224467cd16dcad77572201131ce4f5471414967c469948e6ef38dd \\
Theory Prop Address: & TMUV6V5qcBof6dwE3ebfhwBLiWuk2pD9W8w
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Sigma_mon
\end{verbatim}
\begin{theorem}\label{thm:dfjghgngbgpfngpgog} $${\unicdcdadad X Y : {\iota} .  {{{X} \subseteq {Y}}\unicdbdjdcd{\unicdcdadad Z W : {{\iota}\unicdbdjdcd{\iota}} .  {{({\unicdcdadad x \in {X} .  {{{Z}~{x}} \subseteq {{W}~{x}}}})}\unicdbdjdcd{{({\unicdcdbdbd x \in {X} .  {{Z}~{x}}})} \subseteq {\unicdcdbdbd y \in {Y} .  {{W}~{y}}}}}}}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 425a20091aa7362e407182389fe24965433da14fc0de3e08e13b5905910b2208 \\
Pure Prop Address: & TMYSaxNB5bpwjKeSA3Sf2F7RCAM2gnN5zrb \\
Theory Prop Id: & a8addf8ad27e68150e96f0d2dbd7dd38f2d552c5eb34a1bd96b1975a2139fa44 \\
Theory Prop Address: & TMS4jg3iXSAoEt25M7crKBhYaShmP982iYR
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Sigma_mon0
\end{verbatim}
\begin{theorem}\label{thm:dfjghgngbgpfngpgogad} $${\unicdcdadad X Y : {\iota} .  {{{X} \subseteq {Y}}\unicdbdjdcd{\unicdcdadad Z : {{\iota}\unicdbdjdcd{\iota}} .  {{({\unicdcdbdbd x \in {X} .  {{Z}~{x}}})} \subseteq {\unicdcdbdbd y \in {Y} .  {{Z}~{y}}}}}}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 9b3fbfc10d8cb198135b15ef9120823b40c83a7048721a2a8f5bd592dccd207e \\
Pure Prop Address: & TMHvdHmzNtjNYsphs5AwquVMExTDwRKzC6i \\
Theory Prop Id: & 0c39e5d90a03c8b53d1f91b86500a8426061994e891ba8d4f0abf6ed55874388 \\
Theory Prop Address: & TMG1irPWX7hSKZCJSoz5U9WvofwpYiLcPrD
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Sigma_mon1
\end{verbatim}
\begin{theorem}\label{thm:dfjghgngbgpfngpgogbd} $${\unicdcdadad X : {\iota} .  {\unicdcdadad Z W : {{\iota}\unicdbdjdcd{\iota}} .  {{({\unicdcdadad x .  {{{x} \in {X}}\unicdbdjdcd{{{Z}~{x}} \subseteq {{W}~{x}}}}})}\unicdbdjdcd{{({\unicdcdbdbd x \in {X} .  {{Z}~{x}}})} \subseteq {\unicdcdbdbd x \in {X} .  {{W}~{x}}}}}}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 8f6c670d9cf58964547a2c8f5ecb2655c51fed679a89fcbaf042a9a98576b22c \\
Pure Prop Address: & TMHxEXAifEfqBZatTVRBvvzdAKBzqA8xJC8 \\
Theory Prop Id: & 8a20d4273c3bd449f68d0446ea954be5016f26a33d1b32bc491ace72b24bfce8 \\
Theory Prop Address: & TMVezD2kkz73gqZqGBDvxeirmP7cryxcrP2
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Sigma_Power_1
\end{verbatim}
\begin{theorem}\label{thm:dfjghgngbgpfafpghhfgchpfbd} $${\unicdcdadad X : {\iota} .  {{{X} \in {{\mname{Power}}~{1}}}\unicdbdjdcd{\unicdcdadad Y : {{\iota}\unicdbdjdcd{\iota}} .  {{({\unicdcdadad x \in {X} .  {{{Y}~{x}} \in {{\mname{Power}}~{1}}}})}\unicdbdjdcd{{({\unicdcdbdbd x \in {X} .  {{Y}~{x}}})} \in {{\mname{Power}}~{1}}}}}}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 7a3ae673c65b20d28f4b80b127c87fe8effc6abadb514348178f01786f8f687a \\
Pure Prop Address: & TMTUPmfM2Mi7ztuVrQGCeVRgWXipKh9vVXb \\
Theory Prop Id: & 889ba9237de623f9140e05e0574c4f3e91b2c3c0df705ac3109723a3a09dda78 \\
Theory Prop Address: & TMZYULyhhi7GEPAnwEARVDsEJgpr2MpVTbG
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:dhfgehahchpgeg}
We define $\mname{setprod}$ to be ${\uniddcgcg X Y : {\iota} .  {\unicdcdbdbd x \in {X} .  {Y}}}$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & fc0b600a21afd76820f1fb74092d9aa81687f3b0199e9b493dafd3e283c6e8ca \\
Pure Object Address: & TMX5iqj6cvWjd5eoMqqTEF1367VHDQkj6Yq \\
Theory Object Id: & 107b6bb74ab2c1972d7258ba373ae94a01269f3d05e17f604d541e405e9ab93f \\
Theory Object Address: & TMFyVvPCFYsHfsACwhMzeFYF8jZqyyWje7X
\end{tabular}
\end{center}

\end{definition}
{\bf{Notation.}} We use $\infkdkckd$ as a left associative infix operator  corresponding to applying term ${\mname{setprod}}$.
\begin{verbatim}
pair_setprod
\end{verbatim}
\begin{theorem}\label{thm:ahbgjgchpfdhfgehahchpgeg} ${\unicdcdadad X Y : {\iota} .  {\unicdcdadad (x \in {X})(y \in {Y}) . {{{{pair}~{x}}~{y}} \in {{X}\unicdbgcdgg{Y}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f55ea3828e02273317f0b400d2105e5f6809d31a9ac1326fe0fea71657f5048d \\
Pure Prop Address: & TMP1cFf4SMJvCYXWGuPAbdAT3rrBv9oFfUd \\
Theory Prop Id: & 1dd4994dec4372a29bd9c00f15aa916beb53d6a66b15c1d25e72219e6a2d006c \\
Theory Prop Address: & TMJCXgkH2PkoAWeAmeW98Fvbhtn48QfWyEd
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
proj0_setprod
\end{verbatim}
\begin{theorem}\label{thm:ahchpgkgadpfdhfgehahchpgeg} ${\unicdcdadad X Y : {\iota} .  {\unicdcdadad z \in {{X}\unicdbgcdgg{Y}} .  {{{\mname{proj0}}~{z}} \in {X}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 510623d6d9fee58fe36195a65b68d9e88774298fd789c76bb947e43ba0e9ddd3 \\
Pure Prop Address: & TMbvsu8j8H6CMFRSSMgZzBoz1STTTdmJCQv \\
Theory Prop Id: & f7a519336a9ebe4633840fe128d350ab70461bc5396fe75659857496a4df6c8e \\
Theory Prop Address: & TMQGsuKAnuZCk7jn3UYPfyZCtmqNjDLEXm9
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
proj1_setprod
\end{verbatim}
\begin{theorem}\label{thm:ahchpgkgbdpfdhfgehahchpgeg} ${\unicdcdadad X Y : {\iota} .  {\unicdcdadad z \in {{X}\unicdbgcdgg{Y}} .  {{{\mname{proj1}}~{z}} \in {Y}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f6765c051b33e8891d8407887b98ac6204877cdb39b1c5336a548c49859ce225 \\
Pure Prop Address: & TMMHAkHerqWaT2pFe3dt7C1yXqqaPT3Lotj \\
Theory Prop Id: & afe85e979f6864648f01f74dec8776c350283f9b19d37ad3b00f2558dc5da050 \\
Theory Prop Address: & TMVQEexDvYgcxvr3ptPV72JSsdGheT6ge7G
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
pair_setprod_E0
\end{verbatim}
\begin{theorem}\label{thm:ahbgjgchpfdhfgehahchpgegpffead} ${\unicdcdadad X Y x y : {\iota} .  {{{{{pair}~{x}}~{y}} \in {{X}\unicdbgcdgg{Y}}}\unicdbdjdcd{{x} \in {X}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 107e92452bde569e548509981b8ad6b3760e221a2995bd8b8b11748c06428f6e \\
Pure Prop Address: & TMKaLir23aqUncRog77yHWNUteSZpVWVbf5 \\
Theory Prop Id: & 92b4c14b744c79aa7e9d294133d7983d9ba8f30c9cc011c9d079a5f451447047 \\
Theory Prop Address: & TMSWuEEd13oCxUA81Augy7MtxEyUeafaiQQ
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
pair_setprod_E1
\end{verbatim}
\begin{theorem}\label{thm:ahbgjgchpfdhfgehahchpgegpffebd} ${\unicdcdadad X Y x y : {\iota} .  {{{{{pair}~{x}}~{y}} \in {{X}\unicdbgcdgg{Y}}}\unicdbdjdcd{{y} \in {Y}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 50179b781626f48b09be181df9f551b18fbc72192d119884122eea0b4427b916 \\
Pure Prop Address: & TMTFx9j8XQY7mMx8nXnVLkS1ReCnJvoc5VR \\
Theory Prop Id: & 4e83a82fa29d4046c8ca4bd9154e06e2992eba3ed652c3aa954d141cccef49be \\
Theory Prop Address: & TMYMex5ZPQm8KKBnWBPkZD51i9QL5Ao4tHE
\end{tabular}
\end{center}

\end{theorem}
\section{Functions}
Let $lam : {{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{\iota}})}\unicdbdjdcd{\iota}}}$ be ${\mname{Sigma}}$.
We write $\lambda x\in X.t$ for ${lam}~X~(\lambda x.t)$.
Note that $\Sigma_{x\in X}.t$ and $\lambda x\in X.t$ are two notations
for the same term.

\begin{definition}\label{def:bgah}
We define $\mname{ap}$ to be ${\uniddcgcg f x .  {\{{{\mname{proj1}}~{z}}|z \in {f}, {\unicdcdaddd y : {\iota} .  {{z}={{{pair}~{x}}~{y}}}}\}}}$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & c7aaa670ef9b6f678b8cf10b13b2571e4dc1e6fde061d1f641a5fa6c30c09d46 \\
Pure Object Address: & TMRkKHvzv8Tta9AhRXsVE4k7dQ68XWymCoD \\
Theory Object Id: & a4d82c5a3643a7e174676c313ef995e0307b3b56f57e8ae761b7c6033bbc40db \\
Theory Object Address: & TMULGKR83zvLzsaT5wtaLqEme8A8TV9uVcG
\end{tabular}
\end{center}

\end{definition}
{\bf{Notation.}} When $x$ and $y$ are of type $\iota$, then $x y$ means ${\mname{ap}}~x~y$.

%{\bf{Notation.}} <span class='ltree'>&#x03bb; <i>x</i> &#x2208; <i>A</i> &#x21d2; <i>B</i></span> is notation for the set <span class='ltree'>\mname{Sigma} <i>A</i> (&#x03bb; <i>x</i> : set &#x21d2; <i>B</i>)</span>.
\begin{verbatim}
lamI
\end{verbatim}
\begin{theorem}\label{thm:mgbgngje} ${\unicdcdadad X : {\iota} .  {\unicdcdadad F : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad x \in {X} .  {\unicdcdadad y \in {{F}~{x}} .  {{{{pair}~{x}}~{y}} \in {\uniddcgcg x \in {X} .  {{F}~{x}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0d8645a51ab956ff15d92813d2cab140e73529474636367747958b8e18bab905 \\
Pure Prop Address: & TML8ffdR3C51f2E9BMf7H2BS9S1rFurh827 \\
Theory Prop Id: & 1456cb5b576a7c97a2a8bc57c2896584b0d55dd30ca4212f1733b4c7ebe4f919 \\
Theory Prop Address: & TMaVj4zKhXkoLhyH11SzjuosBXYALhD49xN
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
lamE
\end{verbatim}
\begin{theorem}\label{thm:mgbgngfe} $${\unicdcdadad X : {\iota} .  {\unicdcdadad F : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad z : {\iota} .  {{{z} \in {({\uniddcgcg x \in {X} .  {{F}~{x}}})}}\unicdbdjdcd{\unicdcdaddd x \in {X} .  {\unicdcdaddd y \in {{F}~{x}} .  {{z}={{{pair}~{x}}~{y}}}}}}}}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 5b1bd2e14ea3dbf36ed03b2bca51d8d6329ffb7924a6198502c84e472877864e \\
Pure Prop Address: & TMKZhCQwWmLxNmtRGpKgTrmnpUbXzpUqcC6 \\
Theory Prop Id: & 8ecfabfede2e6f041d7ca7aa6d8ddc7d93e1d4a8f77164e302775838b170ef2f \\
Theory Prop Address: & TMHvzRUPwTDz6sNjr1Xu75jPe97kiKyiFRf
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
lamEq
\end{verbatim}
\begin{theorem}\label{thm:mgbgngfebh} $${\unicdcdadad X : {\iota} .  {\unicdcdadad F : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad z .  {{{z} \in {({\uniddcgcg x \in {X} .  {{F}~{x}}})}}\unicdbdjded{\unicdcdaddd x \in {X} .  {\unicdcdaddd y \in {{F}~{x}} .  {{z}={{{pair}~{x}}~{y}}}}}}}}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 49886b5979c9429dfa4b9590d2e5c308bccd95f87e7cc32f24dc682e35e497f8 \\
Pure Prop Address: & TMXKo25CKqXa5jWu42vnAgmVtNvhqv9e29Q \\
Theory Prop Id: & e7bf483e07224467cd16dcad77572201131ce4f5471414967c469948e6ef38dd \\
Theory Prop Address: & TMUV6V5qcBof6dwE3ebfhwBLiWuk2pD9W8w
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
apI
\end{verbatim}
\begin{theorem}\label{thm:bgahje} ${\unicdcdadad f x y .  {{{{{pair}~{x}}~{y}} \in {f}}\unicdbdjdcd{{y} \in {{f}~{x}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 64667c3e12b9f3ae61ec356833747e367523a8c0ce6c2a9d93f4c38b0783bde5 \\
Pure Prop Address: & TMZLPpY9KNgV39N2yHL65R4C438SdAntCJF \\
Theory Prop Id: & 7708163781ef5b94401f65bdb2a5b080ff257a5930faf05dd1bbe0b4789e9537 \\
Theory Prop Address: & TMPak8MUV4CmmTFj6jaPQ3fYN19JukFbBVX
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
apE
\end{verbatim}
\begin{theorem}\label{thm:bgahfe} ${\unicdcdadad f x y .  {{{y} \in {{f}~{x}}}\unicdbdjdcd{{{{pair}~{x}}~{y}} \in {f}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 85693a617f5d7231598e57242e17d01ba19426804680415415d83c36ca14dcf3 \\
Pure Prop Address: & TMM471VfyY9L9ihJZoGVZy3MTJucpLkPz71 \\
Theory Prop Id: & c08565940adcaebbb0bd8ea7dca3ebc52f096c6a861e7e3eb1dfcc522c057448 \\
Theory Prop Address: & TMNq9VhD4hU2LQs2wbRmvWrApYxACcfdNyd
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
apEq
\end{verbatim}
\begin{theorem}\label{thm:bgahfebh} ${\unicdcdadad f x y .  {{{y} \in {{f}~{x}}}\unicdbdjded{{{{pair}~{x}}~{y}} \in {f}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 4c9d67e97abd0fc158c7647a05ca09ff2992ddd126c6b8d0b452e70e8cbcc406 \\
Pure Prop Address: & TMZQ7PrqUw2JPS363w3buW9bffJsBTNttxy \\
Theory Prop Id: & bd396ee22cc900202a9db5ef15b2b6dc151ca2285723ce93f3f245def051fbe2 \\
Theory Prop Address: & TMSiUYhpZzUqv5JfXdvkMd9Vyn2Xj1gRY8z
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
beta
\end{verbatim}
\begin{theorem}\label{thm:cgfgehbg} ${\unicdcdadad X : {\iota} .  {\unicdcdadad F : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad x : {\iota} .  {{{x} \in {X}}\unicdbdjdcd{{{({\uniddcgcg x \in {X} .  {{F}~{x}}})}~{x}}={{F}~{x}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 95991de564f22218049f5c01a2054c9f531e2a0e7f89348f4cd3cce56269ee6a \\
Pure Prop Address: & TMW5SkUgFpNvxZtwNs5tigJKy4uVF4aLEX4 \\
Theory Prop Id: & b5182dff18aa9200707f42f128e18ba010c3c5b0a3a598682cfd9fe3e36def5d \\
Theory Prop Address: & TMUK7trdHToYkqBA9FA7nyBfnGCJVnzMrdt
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
beta0
\end{verbatim}
\begin{theorem}\label{thm:cgfgehbgad} ${\unicdcdadad X : {\iota} .  {\unicdcdadad F : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad x : {\iota} .  {{{x}\unicdcdadjd{X}}\unicdbdjdcd{{{({\uniddcgcg x \in {X} .  {{F}~{x}}})}~{x}}={0}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 3bb4348d3945f138f08291a2d198487854d211b0b272222fe4f9e932e577522b \\
Pure Prop Address: & TMc9Mv7ukGPvjkLta2ci5R66AEtkDgNuCSM \\
Theory Prop Id: & 475c212b14b3b0ca0e09cf957e6ba095fef5db59bc5b0dcdbe6adbb59a281cce \\
Theory Prop Address: & TMFBwjzjE5yzpGy66RMUx1PdJ9mHVfc6dHb
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
proj0_ap_0
\end{verbatim}
\begin{theorem}\label{thm:ahchpgkgadpfbgahpfad} ${\unicdcdadad u .  {{{\mname{proj0}}~{u}}={{u}~{0}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 588f379b68a9458a540fcdf77dc5d2f4783c00f4cce95dc51c95471cc943eb03 \\
Pure Prop Address: & TMYCXMFZ4HzrBKRUDMYgmo4eHSvQVMQ7p31 \\
Theory Prop Id: & d4f3513ee04ff36d85b2db23be3080385b47ffa013ac715ce8658accd5d66b38 \\
Theory Prop Address: & TMSgBry8vyDWLoFEMZhop4n2xDSn5k839xF
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
proj1_ap_1
\end{verbatim}
\begin{theorem}\label{thm:ahchpgkgbdpfbgahpfbd} ${\unicdcdadad u .  {{{\mname{proj1}}~{u}}={{u}~{1}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d116b3ec53d3345a265357a353929b0e25b62670c0a9b2a3d51a8c73ef732f19 \\
Pure Prop Address: & TMNoHiTHocDKAmUg9hNSv1FxD2Amd3S3tUP \\
Theory Prop Id: & 2328b0e51e8e97743e5baf0897eb65244f631c1e1667f87ea13b28f83b8939b1 \\
Theory Prop Address: & TMRaYAR6WpaEp6hPTm43iVAHVqRrJwCb9di
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
pair_ap_0
\end{verbatim}
\begin{theorem}\label{thm:ahbgjgchpfbgahpfad} ${\unicdcdadad x y : {\iota} .  {{{({{{pair}~{x}}~{y}})}~{0}}={x}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & ac34b9cde0ee2208ea8e422cba572e3fb7982b46ebfdd714251b2dfcb897193e \\
Pure Prop Address: & TMVVcCiRogXNQekjrhetLEc1AwKsjAoaCUb \\
Theory Prop Id: & bb047796b50fbb719f3e14fe10b517fd118f2911a01dac2dc1972ece4948275e \\
Theory Prop Address: & TMPNWnANeRPomJ9tENqayKNjmwfidUynXLZ
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
pair_ap_1
\end{verbatim}
\begin{theorem}\label{thm:ahbgjgchpfbgahpfbd} ${\unicdcdadad x y : {\iota} .  {{{({{{pair}~{x}}~{y}})}~{1}}={y}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 2274fc6211c808c3b1604a439df9779ba0f1ddad055df119366dc394c2fb97f6 \\
Pure Prop Address: & TMSs4jYzqSwfDX666rdcAD6CeBDVaoMRoyc \\
Theory Prop Id: & cce3d21c0d689ca2584d628eb0fdd682ec793195238268afe769ce51f75bb164 \\
Theory Prop Address: & TMFmHmqub8mZKhdbCxJVhYYkdtHahTZ7UAh
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
pair_ap_n2
\end{verbatim}
\begin{theorem}\label{thm:ahbgjgchpfbgahpfogcd} ${\unicdcdadad x y i : {\iota} .  {{{i}\unicdcdadjd{2}}\unicdbdjdcd{{{({{{pair}~{x}}~{y}})}~{i}}={0}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & aa4c5b4688eb6b4f059f6d4ecc867417bf44703f3f25ae2c2a4bb84351e4918a \\
Pure Prop Address: & TMJvhJVjoT8tymCLYAEd8KMpMSd7c5dzvrs \\
Theory Prop Id: & 6a36da546596b4c9b0cab2739118ca96148377b2acb8a70b37d0a4aa0d404b22 \\
Theory Prop Address: & TMapLv3NXF9X9vWbexn1gRz4mSdux6SZs6w
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
ap0_Sigma
\end{verbatim}
\begin{theorem}\label{thm:bgahadpfdfjghgngbg} ${\unicdcdadad X : {\iota} .  {\unicdcdadad Y : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad z : {\iota} .  {{{z} \in {({\unicdcdbdbd x \in {X} .  {{Y}~{x}}})}}\unicdbdjdcd{{({{z}~{0}})} \in {X}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 861a795017a942802f4443c95b5a36332a33f167ce1441dfc6a24503f6268b3e \\
Pure Prop Address: & TMKRf5LGKqydnVhB8vpAzDvodiXpqNvrMxB \\
Theory Prop Id: & 1affcc338ae841e0e000cf9be970918006435331f595cedc951a44209748026c \\
Theory Prop Address: & TMUBP4wFdxgzoA73DJqdvnWDxq8D4ZPGmSV
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
ap1_Sigma
\end{verbatim}
\begin{theorem}\label{thm:bgahbdpfdfjghgngbg} $${\unicdcdadad X : {\iota} .  {\unicdcdadad Y : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad z : {\iota} .  {{{z} \in {({\unicdcdbdbd x \in {X} .  {{Y}~{x}}})}}\unicdbdjdcd{{({{z}~{1}})} \in {({{Y}~{({{z}~{0}})}})}}}}}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & ad3bfe036fa895ae325d64498611356bb49df8ebd34b91be258534581bb43fb7 \\
Pure Prop Address: & TMQ3NDTgxp9a1VuLPqoNmEGA5MjKwt6QJLH \\
Theory Prop Id: & 520af5f2f80e3d8411b1460e91384a058099174706d3029c6f03f1ab389a8f32 \\
Theory Prop Address: & TMKB8YXKTKjDb1T1UTPbMwrfxTLy3KBSoJv
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:ahbgjgchpfah}
We define $\mname{pair\_p}$ to be ${\uniddcgcg u : {\iota} .  {{{{pair}~{({{u}~{0}})}}~{({{u}~{1}})}}={u}}}$ of type ${{\iota}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & ade2bb455de320054265fc5dccac77731c4aa2464b054286194d634707d2e120 \\
Pure Object Address: & TMSvXNQFUtikJWHkJ8EmjpLPVE6eVHHPye3 \\
Theory Object Id: & 5c8a35346b94416c8921f9496e68b956c0e80aa2f5b966805dd30a7cc9bdb03e \\
Theory Object Address: & TMbuqZXCg75fnX39GezV6NmULFhCWCyVQLX
\end{tabular}
\end{center}

\end{definition}
\begin{verbatim}
pair_p_I
\end{verbatim}
\begin{theorem}\label{thm:ahbgjgchpfahpfje} ${\unicdcdadad x y .  {{\mname{pair\_p}}~{({{{pair}~{x}}~{y}})}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 06d9a28b2c025648a5c4c367e18ca07d131c2483cbec5ef5ed9b8c412a2959e3 \\
Pure Prop Address: & TMJoDcS8DRqyUSNGb82nnjwSRKn9hqLmFdN \\
Theory Prop Id: & 8f2fdee4c2a4b4668940264d97e6a4d34887ed1cb2b9462e5a68ea86f3267c92 \\
Theory Prop Address: & TMPcM8MemhXia2UuEVstbB2UDdYPEQwK1R1
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
pair_p_I2
\end{verbatim}
\begin{theorem}\label{thm:ahbgjgchpfahpfjecd} ${\unicdcdadad w .  {{({\unicdcdadad u \in {w} .  {{{\mname{pair\_p}}~{u}}\unicdcdcdhd{{{u}~{0}} \in {2}}}})}\unicdbdjdcd{{\mname{pair\_p}}~{w}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & e4b35e6cad38e54d2a79aadbe2af0245099589e5c7fade68162ef8871c460979 \\
Pure Prop Address: & TMJUphhHJCGQn6H3JsbDsYQ2vhJYQpGSSq6 \\
Theory Prop Id: & f66937108389bce047e36e45cd53689abfbd69e81d439e978b5d6f03a84804fd \\
Theory Prop Address: & TMUhxxoG6nPHQGfqpNzk4M5VX4pepkB3W7b
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
pair_p_In_ap
\end{verbatim}
\begin{theorem}\label{thm:ahbgjgchpfahpfjeogpfbgah} ${\unicdcdadad w f .  {{{\mname{pair\_p}}~{w}}\unicdbdjdcd{{{w} \in {f}}\unicdbdjdcd{{{w}~{1}} \in {{{\mname{ap}}~{f}}~{({{w}~{0}})}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & e93eb76f4ff4537fc952c7e2663dd348eba0a1eda133a280fa73a98aaed1afd7 \\
Pure Prop Address: & TMMpbcE9Nf47Qr4V5rA9WJeQ3beYck2RvoP \\
Theory Prop Id: & cda5c674d061ba7e438ebe2318a287bc128928b90a50c0bbd5f76eb976eda17a \\
Theory Prop Address: & TMVJ3KJ5wJShTfj2JebzJWxoqicyYhHmzhf
\end{tabular}
\end{center}

\end{theorem}

\section{Tuples as Functions on Naturals}\label{effhahmgfgdh0}

\begin{definition}\label{def:ehfhahmgfgpfah}
We define $\mname{tuple\_p}$ to be $${\uniddcgcg n u .  {\unicdcdadad z \in {u} .  {\unicdcdaddd i \in {n} .  {\unicdcdaddd x : {\iota} .  {{z}={{{pair}~{i}}~{x}}}}}}}$$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 83d48a514448966e1b5b259c5f356357f149bf0184a37feae52fc80d5e8083e5 \\
Pure Object Address: & TMPQRFB8kv9Mi3hJcbAVVFkKaCjpTiKn5DP \\
Theory Object Id: & 7b913e689b741f5e3d1a5c19e7580fd46ffd026760b86242807b35879571cbe3 \\
Theory Object Address: & TMSwuuEUBwMbLNhY2oHRChGyRGNSMgRmKA1
\end{tabular}
\end{center}

\end{definition}
\begin{verbatim}
pair_p_tuple2
\end{verbatim}
\begin{theorem}\label{thm:ahbgjgchpfahpfehfhahmgfgcd} ${{\mname{pair\_p}}={{\mname{tuple\_p}}~{2}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & edb4f2daac705fc5fde5fb625306e4ce3b70b5c324811dcfe9286a3352609130 \\
Pure Prop Address: & TMa7Ph4F792pWejWQxMqTYL67K6y3Atz3GB \\
Theory Prop Id: & 4ab8c71265b072dffa2255ec379c857d2480a9f4cc0b5722bf710c7b2e3aaa21 \\
Theory Prop Address: & TMPDLkLax6xryGqZWfjiAzsWiueQwkeoq77
\end{tabular}
\end{center}

\end{theorem}

{\bf{Notation.}} When $x_0,\ldots,x_{n-1}$ are of type $\iota$, we write $(x_0,\ldots,x_{n-1})$
for $\lambda i \in n.\mif{i=0}{x_0}{\cdots\mif{i=n-1}{x_{n-1}}{0}}$.

\begin{verbatim}
tuple_p_2_tuple
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfahpfcdpfehfhahmgfg} ${\unicdcdadad x y : {\iota} .  {{{\mname{tuple\_p}}~{2}}~{({x},{y})}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 982145ec24f8189cb7ff562fa9a82c89405822de093f290a7c78ff1b6560c79b \\
Pure Prop Address: & TMRXKTaQZ2mMDiGAZrvuMg3ozPJcAZAgWGP \\
Theory Prop Id: & f8f972a715455be65b85075f8f7f738798be5894513ebfc46853439a15150d79 \\
Theory Prop Address: & TMX5VxQzTL4dEJu18K3FBfoBgfDf59XiNpV
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_pair
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfahbgjgch} ${\unicdcdadad x y : {\iota} .  {{{{pair}~{x}}~{y}}={({x},{y})}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & c122f6c45d6ae2b29699ba19714006844818fe6aed0b78c730fa61d541f8f655 \\
Pure Prop Address: & TMNGGwosAVCCgzqRpMz6fsnenJVoBPWXYUc \\
Theory Prop Id: & 18198e977ce2f209097f879f8fb82081371242788607f8a3fa8da991d443ee60 \\
Theory Prop Address: & TMUTEozs7LjRCKnvt77suPHQfR7gNvzEi7v
\end{tabular}
\end{center}

\end{theorem}

\section{Dependent Products}

\begin{definition}\label{def:afjg}
We define $\mname{Pi}$ to be $${\uniddcgcg X Y .  {\{f \in {{\mname{Power}}~{({\unicdcdbdbd x \in {X} .  {{\mname{Union}}~{({{Y}~{x}})}}})}}|{\unicdcdadad x \in {X} .  {{{f}~{x}} \in {{Y}~{x}}}}\}}}$$ of type ${{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{\iota}})}\unicdbdjdcd{\iota}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 40f1c38f975e69e2ae664b3395551df5820b0ba6a93a228eba771fc2a4551293 \\
Pure Object Address: & TMMmsr8jojnNQnfEu32oXr8oHW6b2JucDYn \\
Theory Object Id: & a7b1b09cb152a467eba4c7154e043aede9f10dd364de00ce2145c5178d3ad12b \\
Theory Object Address: & TMb8zzbN5gj4sGhAcwYC7Re7qCi97Rtgo7h
\end{tabular}
\end{center}

\end{definition}
{\bf{Notation.}} We use $\bindafjgpf x,\ldots,y  . $ as a binder notation corresponding to a term constructed using ${\mname{Pi}}$.
\begin{verbatim}
PiI
\end{verbatim}
\begin{theorem}\label{thm:afjgje}
  $$
  \begin{array}{c}
    \unicdcdadad X : {\iota} .  \unicdcdadad Y : {{\iota}\unicdbdjdcd{\iota}} .  \unicdcdadad f : {\iota} .  {({\unicdcdadad u \in {f} .  {{{\mname{pair\_p}}~{u}}\unicdcdcdhd{{{u}~{0}} \in {X}}}})}\unicdbdjdcd\\
                 {{({\unicdcdadad x \in {X} .  {{{f}~{x}} \in {{Y}~{x}}}})}\unicdbdjdcd{{f} \in {\unicdcdadgg x \in {X} .  {{Y}~{x}}}}}.
  \end{array}
  $$
  The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 2b7ef42e911f5c9d245f0e1650bdf7a017dc07c61643b180beacd902afa937ac \\
Pure Prop Address: & TMHGz8t2EnwQDiuH6KDQpg8EnyxGgR8dS7e \\
Theory Prop Id: & 1f8f6f437998cacea340ec1ea9cc9798e39298aa0d85498c0c20643140f46942 \\
Theory Prop Address: & TMWx4ti6JwTdu8xygg15tK2YVvzLMBHLWpP
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
PiE
\end{verbatim}
\begin{theorem}\label{thm:afjgfe}
  $$
  \begin{array}{c}
    \unicdcdadad X : {\iota} .  \unicdcdadad Y : {{\iota}\unicdbdjdcd{\iota}} .  \unicdcdadad f : {\iota} .  {{f} \in {({\unicdcdadgg x \in {X} .  {{Y}~{x}}})}}\unicdbdjdcd\\
                 {{({\unicdcdadad u \in {f} .  {{{\mname{pair\_p}}~{u}}\unicdcdcdhd{{{u}~{0}} \in {X}}}})}\unicdcdcdhd{({\unicdcdadad x \in {X} .  {{{f}~{x}} \in {{Y}~{x}}}})}}.
  \end{array}
  $$
  The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & e900d056f38f163f77287b64052d5d9e602edf6c698bce849b83205e4fecd08a \\
Pure Prop Address: & TMQswaTQQ8v2NGGPZrcYHSjahdLxdVqq8Bc \\
Theory Prop Id: & c6a19abb37631cc1754b1e349cb516006e88cf3a4a1da2d0f9de9154571fabdc \\
Theory Prop Address: & TMNmPoYTgXJ1oQ5bHuJoN3MvGSuMrhGxKb8
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
PiEq
\end{verbatim}
\begin{theorem}\label{thm:afjgfebh}
  $$
  \begin{array}{c}
    \unicdcdadad X : {\iota} .  \unicdcdadad Y : {{\iota}\unicdbdjdcd{\iota}} .  \unicdcdadad f : {\iota} .  {{f} \in {{{\mname{Pi}}~{X}}~{Y}}}\unicdbdjded\\
                 {{({\unicdcdadad u \in {f} .  {{{\mname{pair\_p}}~{u}}\unicdcdcdhd{{{u}~{0}} \in {X}}}})}\unicdcdcdhd{({\unicdcdadad x \in {X} .  {{{f}~{x}} \in {{Y}~{x}}}})}}.
  \end{array}
  $$
  The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & aee68f00e9f9b4dfa4f93208b50b84f39e34d3143871795718db72cf160eceba \\
Pure Prop Address: & TMLoctKVTPvcs1L1sQJmpzmMB7ZGefxweHF \\
Theory Prop Id: & e80f95c3f8e7d257d04588c36cf7c2cbcef829f184e76311e443137e0d9bf708 \\
Theory Prop Address: & TMJq3SLpMrtKWAEFsc6WRLhigo1buRia2SA
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
lam_Pi
\end{verbatim}
\begin{theorem}\label{thm:mgbgngpfafjg}
  $$
  \begin{array}{c}
    \unicdcdadad X : {\iota} .  \unicdcdadad Y : {{\iota}\unicdbdjdcd{\iota}} .  \unicdcdadad F : {{\iota}\unicdbdjdcd{\iota}} .  {({\unicdcdadad x \in {X} .  {{{F}~{x}} \in {{Y}~{x}}}})}\unicdbdjdcd\\
                 {{({\uniddcgcg x \in {X} .  {{F}~{x}}})} \in {({\unicdcdadgg x \in {X} .  {{Y}~{x}}})}}.
  \end{array}
  $$
  The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & c0b88f5343d69ece7a5c1776f75f883b1ea441d9f54b23c0f2f9bfd3d63291ce \\
Pure Prop Address: & TMK1tiobRV7Rk8oLJDiqRt9emhAiARd65fd \\
Theory Prop Id: & 3733f8d8b8cfb744a472ecadfd3dd8ec6a02c94d9f4ba9cb8fe6fa05f899b65e \\
Theory Prop Address: & TMR7xMjyWg42N9C62nDT2fP29rt63NXuwrb
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
ap_Pi
\end{verbatim}
\begin{theorem}\label{thm:bgahpfafjg} $${\unicdcdadad X : {\iota} .  {\unicdcdadad Y : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad f : {\iota} .  {\unicdcdadad x : {\iota} .  {{{f} \in {({\unicdcdadgg x \in {X} .  {{Y}~{x}}})}}\unicdbdjdcd{{{x} \in {X}}\unicdbdjdcd{{{f}~{x}} \in {{Y}~{x}}}}}}}}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 7c36179a82d8644940659a1f02b440b62c39cf8ece8fc0d2538fccfd980eaa68 \\
Pure Prop Address: & TMXNoSqzT5Lu24RbFYcKt5N8JRNvmf1MDSm \\
Theory Prop Id: & cb962ef0bbe77996198527ec24108318b6142c9b6d3b1cacdc185efa044e94f6 \\
Theory Prop Address: & TMFXJjxwrkNdrbgK4hwdYsRNhanGr8DEELP
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Pi_ext_Subq
\end{verbatim}
\begin{theorem}\label{thm:afjgpffgihehpfdffhcgbh} $${\unicdcdadad X : {\iota} .  {\unicdcdadad Y : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad f g \in {({\unicdcdadgg x \in {X} .  {{Y}~{x}}})} .  {{({\unicdcdadad x \in {X} .  {{{f}~{x}} \subseteq {{g}~{x}}}})}\unicdbdjdcd{{f} \subseteq {g}}}}}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 895d76cfaedb48089543791c77f82e5ff8402576798d94cc12c928b42720b3c7 \\
Pure Prop Address: & TMK7g7rTpdWeWhZFQAosbFDbAB6K9oH1vVL \\
Theory Prop Id: & fcbe2211dda51b2c7c056b9eb958563051102a56a57c22caef81a1ef81d5955c \\
Theory Prop Address: & TMQb6BZWimWiUUD2TKu7WGhQkSQpf98JfKA
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Pi_ext
\end{verbatim}
\begin{theorem}\label{thm:afjgpffgiheh} $${\unicdcdadad X : {\iota} .  {\unicdcdadad Y : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad f g \in {({\unicdcdadgg x \in {X} .  {{Y}~{x}}})} .  {{({\unicdcdadad x \in {X} .  {{{f}~{x}}={{g}~{x}}}})}\unicdbdjdcd{{f}={g}}}}}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & afabf60d2f0c584af57bc85ddf915b13c2173fba3ae62a67a3862a472418d979 \\
Pure Prop Address: & TMZQyqEpgM1nAy5SpShxXSu4QC8bRbftnW5 \\
Theory Prop Id: & 08bc8829905fa1c9330919448051750a09ed9872e5fe47a6c8f242ef8905a6e1 \\
Theory Prop Address: & TMFnU1vnCxgdDuPv6P9CoEak4jkUTjULRYT
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Pi_eta
\end{verbatim}
\begin{theorem}\label{thm:afjgpffgehbg} $${\unicdcdadad X : {\iota} .  {\unicdcdadad Y : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad f : {\iota} .  {{{f} \in {({\unicdcdadgg x \in {X} .  {{Y}~{x}}})}}\unicdbdjdcd{{({\uniddcgcg x \in {X} .  {{f}~{x}}})}={f}}}}}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 9ca3eb4ba8300315de6cc6aa4bc0569bf6750d0a55b1e27929bafce0326878c2 \\
Pure Prop Address: & TMZ1A4m5suKjS6q8ujjemybzpezfVbf3Ja5 \\
Theory Prop Id: & 9bd10ac78e1b9dd36b301ed8e06904d4553c0bd53f28e2dd52662fee5e5fd680 \\
Theory Prop Address: & TMXWQh8ieRCGD99r9bmA7JmXyAU4rDWeass
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:dhfgehfgihah}
We define $\mname{setexp}$ to be ${\uniddcgcg X Y : {\iota} .  {\unicdcdadgg y \in {Y} .  {X}}}$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 1de7fcfb8d27df15536f5567084f73d70d2b8526ee5d05012e7c9722ec76a8a6 \\
Pure Object Address: & TMdMKJiLvRmU1utdH9i5YSFhSMeAkFKRH1a \\
Theory Object Id: & 021ae079aee80b7f24175c08d98ddd174bcabd841750953bdefaa681a83714e7 \\
Theory Object Address: & TMMDiZSCEZ1dDZ4PWaQHcXQkH4ocT26aDjJ
\end{tabular}
\end{center}

\end{definition}
{\bf{Notation.}}
We use superscripts as notation for applying the term ${\mname{setexp}}$.
\begin{verbatim}
pair_tuple_fun
\end{verbatim}
\begin{theorem}\label{thm:ahbgjgchpfehfhahmgfgpfggfhog} ${{pair}={({\uniddcgcg x y .  {({x},{y})}})}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & b02dfae335ec8db395520722941b8dc3a0d6514527797822554c3261ab3f1cb8 \\
Pure Prop Address: & TMQLyvPjAxztmV8UGpQ822nUAH8ziqxafSL \\
Theory Prop Id: & ed37d0c53ab39329962382f39457e2117aa8fbbe349e0cb167d2c2d76af2a96e \\
Theory Prop Address: & TMQyWvvFdsJND6mF8ATSUatvvo9p2RAUqY3
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
lamI2
\end{verbatim}
\begin{theorem}\label{thm:mgbgngjecd} ${\unicdcdadad X .  {\unicdcdadad F : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad x \in {X} .  {\unicdcdadad y \in {{F}~{x}} .  {{({x},{y})} \in {\uniddcgcg x \in {X} .  {{F}~{x}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d4a9d90bcc14a1607b933d2b6324f74a12e560f1ee23d66bbef65f0ab2300245 \\
Pure Prop Address: & TMTxDywb49ok9weqR5PA1YkH5HYVVQgfmLa \\
Theory Prop Id: & de381fee5dd742f3e056c75fdc7abdebc389a9d213f325ce23fff6b0562da398 \\
Theory Prop Address: & TMYB1uFbN7KQg4EMgzCmiEUJxJcauCrH6gi
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
lamE2
\end{verbatim}
\begin{theorem}\label{thm:mgbgngfecd} $${\unicdcdadad X .  {\unicdcdadad F : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad z : {\iota} .  {{{z} \in {({\uniddcgcg x \in {X} .  {{F}~{x}}})}}\unicdbdjdcd{\unicdcdaddd x \in {X} .  {\unicdcdaddd y \in {{F}~{x}} .  {{z}={({x},{y})}}}}}}}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 2907d7e677f8d705f7bf5bfe75cf312a139a28537d4ee131f50b8e62731177d7 \\
Pure Prop Address: & TMMNkCJJRFygiBFaXLzPkZ9eYzm8gs5REwb \\
Theory Prop Id: & c69df21f0c5d7582f84f032104dcbf0cdde6b5a1e91fbe54831893e9ab547722 \\
Theory Prop Address: & TMZ49ENvtTqA2Tv7yJYdvGtiYB5BtFdTeVV
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_2_inj
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfcdpfjgogkg} ${\unicdcdadad x y w z : {\iota} .  {{{({x},{y})}={({w},{z})}}\unicdbdjdcd{{{x}={w}}\unicdcdcdhd{{y}={z}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 5a5be1cedd8243deb6c455ce395e463e404fca87c52b0a3a277a9b3855cb78e9 \\
Pure Prop Address: & TMFbqwXKr8H1bgcdquem9YDZJMmsUJmHeKC \\
Theory Prop Id: & 8feaceee2c95bc779292a107468e26dcc3aeefca4f4cec066bd23102d06d83ad \\
Theory Prop Address: & TMNPCfqHk5t1KqeT14ns1V9EhdHeBU9wLyc
\end{tabular}
\end{center}

\end{theorem}

\section{Pairs as Tuples}\label{effhahmgfgdh}Let $ x0, x1 : {\iota}$ be given.
\begin{verbatim}
tuple_2_0_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfcdpfadpffgbh} ${{{({x0},{x1})}~{0}}={x0}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 42d4527df30bd5915ecca74999921e236618128fee94e9018ab8452c7d825590 \\
Pure Prop Address: & TMQ8nhtfV6W3JDU3mscgLR5QMXHfDZgZYK4 \\
Theory Prop Id: & ad903742c17c3fe99f8b82cdfafdc7c72f5443fcb7032eb137490fe2367b8749 \\
Theory Prop Address: & TMMmXMGjkWqC3h5qQxyBwLzymNx8CZr1RZA
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_2_1_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfcdpfbdpffgbh} ${{{({x0},{x1})}~{1}}={x1}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 596569b2cc94a7411cd00ed3dcc85f68340782a2dea77d8454b30f81c7eb6661 \\
Pure Prop Address: & TMJ9iszZSDm4Q8D744Pr5ok8cAppzRJapau \\
Theory Prop Id: & 2c0ad17788686eabbd5f29d00be65516a9112c392a4d4466c10b9df595bb100e \\
Theory Prop Address: & TMNHajqbPTVi7TYeCTT1YBrSfZg2Srt6YhV
\end{tabular}
\end{center}

\end{theorem}
\subsection{Abstracting with Two Variables} % Tuples
\begin{definition}\label{def:dffgahcd}
  We define $\mname{Sep2}$ to be
  $${\uniddcgcg X Y R .  {\{u \in {\unicdcdbdbd x \in {X} .  {{Y}~{x}}}|{{{R}~{({{u}~{0}})}}~{({{u}~{1}})}}\}}}$$ of type ${{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{\iota}})}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}})}\unicdbdjdcd{\iota}}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & b86d403403efb36530cd2adfbcacc86b2c6986a54e80eb4305bfdd0e0b457810 \\
Pure Object Address: & TMJBzUyWurQtsdPSJTbqaZih7trGyeYoC3m \\
Theory Object Id: & fc03e85944df87e6a24b2bdf2798d99cf3faa3ada8ae8ebef483367bb485a195 \\
Theory Object Address: & TMYXWf8P7ybU2LjpjrRcGd9ZaYEfsgynmzt
\end{tabular}
\end{center}

\end{definition}
\begin{verbatim}
Sep2I
\end{verbatim}
\begin{theorem}\label{thm:dffgahcdje}
  $$
  \begin{array}{c}
    \unicdcdadad X .  \unicdcdadad Y : {{\iota}\unicdbdjdcd{\iota}} .  \unicdcdadad R : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  \unicdcdadad x \in {X} .  \unicdcdadad y \in {{Y}~{x}} . \\
                 {{{R}~{x}}~{y}}\unicdbdjdcd{{({x},{y})} \in {{{{\mname{Sep2}}~{X}}~{Y}}~{R}}}.
  \end{array}
  $$
  The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f2dd7d7d0de46ec460fe30813842b2da107da11fbc9608d96eea869888811cca \\
Pure Prop Address: & TMZdgPdsrcEjsnAmQm7foGQpRLeMQ4R8i64 \\
Theory Prop Id: & 35493133c295677bdfd5c4e9ab9236a9a50b7d9c1c379734567bf32375fc9508 \\
Theory Prop Address: & TMYNAkcLqkkyU7u7qUwEAZxTvqQnKYD6FxK
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Sep2E
\end{verbatim}
\begin{theorem}\label{thm:dffgahcdfe}
  $$
  \begin{array}{c}
    \unicdcdadad X .  \unicdcdadad Y : {{\iota}\unicdbdjdcd{\iota}} .  \unicdcdadad R : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  \unicdcdadad u \in {{{{\mname{Sep2}}~{X}}~{Y}}~{R}} .\\
                 {\unicdcdaddd x \in {X} .  {\unicdcdaddd y \in {{Y}~{x}} .  {{{u}={({x},{y})}}\unicdcdcdhd{{{R}~{x}}~{y}}}}}.
  \end{array}
  $$
  The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & aca0dd1d7527fc7cb76890b26390b9351092342fe8f0f530c801862f12edf753 \\
Pure Prop Address: & TMMMFQtAKedKiQ38BC5pn49TBQDJSeKoTYo \\
Theory Prop Id: & f094fb5ccc800bcb94dec37b2867363bf66db0ad9e299e07454e901889561056 \\
Theory Prop Address: & TMYo6UtpLGR595GYoBTpBoawMbFG3BTJ6aH
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Sep2E'
\end{verbatim}
\begin{theorem}\label{thm:dffgahcdfehc}
  $$
  \begin{array}{c}
    \unicdcdadad X .  \unicdcdadad Y : {{\iota}\unicdbdjdcd{\iota}} .  \unicdcdadad R : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .\\  {\unicdcdadad x y .  {{{({x},{y})} \in {{{{\mname{Sep2}}~{X}}~{Y}}~{R}}}\unicdbdjdcd{{{{x} \in {X}}\unicdcdcdhd{{y} \in {{Y}~{x}}}}\unicdcdcdhd{{{R}~{x}}~{y}}}}}.
  \end{array}
  $$
  The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & c5ad5457a7903751d537c31ccfbac1f4b84637cc2029ba26617d81ccecc36758 \\
Pure Prop Address: & TMbEYwrs85BumegRS4Nue1VQK9pgGsjNjk6 \\
Theory Prop Id: & f89326bba190a5f12b5139594f24a9ffae64a5b1b99d9ad4ab4e87f02434d466 \\
Theory Prop Address: & TMEw2C6gFcC7Dv9bdaWQaJELJTrEwgTQ5p6
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Sep2E'1
\end{verbatim}
\begin{theorem}\label{thm:dffgahcdfehcbd} $${\unicdcdadad X .  {\unicdcdadad Y : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad R : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  {\unicdcdadad x y .  {{{({x},{y})} \in {{{{\mname{Sep2}}~{X}}~{Y}}~{R}}}\unicdbdjdcd{{x} \in {X}}}}}}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d38eaf92e4d64f247f4a780f3acacb7e2b72c2c3161acddce4ff56153a152346 \\
Pure Prop Address: & TMKEJf9zJKiTAqodB3HUgFWJktNYut6txng \\
Theory Prop Id: & 0df0e0988ad65ec90d05105e87f7530d402ff762879f9f56fd2cea42ba0e3868 \\
Theory Prop Address: & TMQamUmivkZALac37sX35Qy2VnbAqqLtDUR
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Sep2E'2
\end{verbatim}
\begin{theorem}\label{thm:dffgahcdfehccd} $${\unicdcdadad X .  {\unicdcdadad Y : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad R : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  {\unicdcdadad x y .  {{{({x},{y})} \in {{{{\mname{Sep2}}~{X}}~{Y}}~{R}}}\unicdbdjdcd{{y} \in {{Y}~{x}}}}}}}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & aa8d9b9df491ed7a1a582cbb2433626cfd9178aed409e00cfb68e55d7be32deb \\
Pure Prop Address: & TMTb1KVCtVPHStwUTCiwdLPEPhorfx9R1DH \\
Theory Prop Id: & b637cd9c32289ddb25bdd962484739bdb1e70ff50694648a27ce6bcbbd48aadf \\
Theory Prop Address: & TMRNNqqH7CLCLvFwcFthUaz6sHcYuKw3TTR
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Sep2E'3
\end{verbatim}
\begin{theorem}\label{thm:dffgahcdfehcdd} $${\unicdcdadad X .  {\unicdcdadad Y : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad R : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  {\unicdcdadad x y .  {{{({x},{y})} \in {{{{\mname{Sep2}}~{X}}~{Y}}~{R}}}\unicdbdjdcd{{{R}~{x}}~{y}}}}}}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 5bc2e18996dfa5f943f7598be61adad327423e248744c541671fbe4a34dbcdb9 \\
Pure Prop Address: & TMJnp3Ji7AtjsMbmW8cAVsi53FTqYVAGgdL \\
Theory Prop Id: & 379abcf237632ff104c4aa456b6ade54b471ea851766aabd28e15e516d1cbc2d \\
Theory Prop Address: & TMS5WEGW72CGY6U9AD8kjGtvBWaHnyN25En
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:dhfgehpfpgggpfahbgjgchdh}
We define $\mname{set\_of\_pairs}$ to be ${\uniddcgcg X .  {\unicdcdadad x \in {X} .  {\unicdcdaddd y z .  {{x}={({y},{z})}}}}}$ of type ${{\iota}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & f0b1c15b686d1aa6492d7e76874c7afc5cd026a88ebdb352e9d7f0867f39d916 \\
Pure Object Address: & TMUjSWaE3xf1N5QcPC5311QNAmCHwv9P5Wh \\
Theory Object Id: & fd6f81f636454aafecfc9ce1aff42ca28607f59856bf0029f61a1c9a3db299fd \\
Theory Object Address: & TMGXX5uaVkMUzQ1LmgBVrBHf1qxYoxXsvza
\end{tabular}
\end{center}

\end{definition}
\begin{verbatim}
set_of_pairs_ext
\end{verbatim}
\begin{theorem}\label{thm:dhfgehpfpgggpfahbgjgchdhpffgiheh}
  $$
  \begin{array}{c}
    \unicdcdadad X Y .  {{\mname{set\_of\_pairs}}~{X}}\unicdbdjdcd{{\mname{set\_of\_pairs}}~{Y}}\unicdbdjdcd\\
          {{({\unicdcdadad v w .  {{{({v},{w})} \in {X}}\unicdbdjded{{({v},{w})} \in {Y}}}})}\unicdbdjdcd{{X}={Y}}}.
  \end{array}
  $$
  The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a6a9b8a124fce5adc383130f08213682d41360dcd1f274f71b33e154a055cc62 \\
Pure Prop Address: & TMJxKznQHdHfEU5fnQZwkd5AQ1SGfmDPbwC \\
Theory Prop Id: & 4367f3d59340f9ed670f3765311f00f3089bb7fe2b92d37317898a53a96fbced \\
Theory Prop Address: & TMJd1FMb8pL4Bst6TsZEDp74LjsFRSbxwiC
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Sep2_set_of_pairs
\end{verbatim}
\begin{theorem}\label{thm:dffgahcdpfdhfgehpfpgggpfahbgjgchdh} ${\unicdcdadad X .  {\unicdcdadad Y : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad R : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  {{\mname{set\_of\_pairs}}~{({{{{\mname{Sep2}}~{X}}~{Y}}~{R}})}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a60553fc65df7d42bd360fe1cd8b1f9fc8ccc08be19e4177f1ba046a7532ceca \\
Pure Prop Address: & TMTsAuBK39fZ9F9TNnMkeSTj8FGHfLzf6dj \\
Theory Prop Id: & 405a7213163c862c29aeb2e09d4e10989b3c7e06b28850ebc7378a653fbe4fdc \\
Theory Prop Address: & TMH6hRBLodwvqfQVE5ky49zcXJLCo6tRMY5
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Sep2_ext
\end{verbatim}
\begin{theorem}\label{thm:dffgahcdpffgiheh}
  $$
  \begin{array}{c}
    \unicdcdadad X .  \unicdcdadad Y : {{\iota}\unicdbdjdcd{\iota}} .  \unicdcdadad R R' : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  {({\unicdcdadad x \in {X} .  {\unicdcdadad y \in {{Y}~{x}} .  {{{{R}~{x}}~{y}}\unicdbdjded{{{R'}~{x}}~{y}}}}})}\unicdbdjdcd\\
            {{{{{\mname{Sep2}}~{X}}~{Y}}~{R}}={{{{\mname{Sep2}}~{X}}~{Y}}~{R'}}}.
  \end{array}
  $$
  The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0d9958e6cc16ac9372dc8846011178fe201c3d9b19cdc001f26e2e162b34d938 \\
Pure Prop Address: & TMJACniaRX5HaiHuCE6bbMAHvHDcUhXZ2pH \\
Theory Prop Id: & 94f11b19e5200e39967696f4804cf43ac713a68f6e15ca6369756da68d2d967b \\
Theory Prop Address: & TMRjiAegumXRHuqWAazF89LwDqZTyyMSddG
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
lam_ext_sub
\end{verbatim}
\begin{theorem}\label{thm:mgbgngpffgihehpfdhfhcg} $${\unicdcdadad X .  {\unicdcdadad F G : {{\iota}\unicdbdjdcd{\iota}} .  {{({\unicdcdadad x \in {X} .  {{{F}~{x}}={{G}~{x}}}})}\unicdbdjdcd{{({\uniddcgcg x \in {X} .  {{F}~{x}}})} \subseteq {({\uniddcgcg x \in {X} .  {{G}~{x}}})}}}}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & b2e26f98453afefcb6f3f49b69c601bd95524ea1ad1932d9fcbd17ae8e3732d6 \\
Pure Prop Address: & TMTQkRNn8PD1f7MWUC1oifnJZfbsstmDxEp \\
Theory Prop Id: & 79c629a63ae9a61f24fd859e86bcc2c5d7619d2e635836bd41d82acd839a0640 \\
Theory Prop Address: & TMGxXnao732sc8NYXxP9KnXrb3jXwMstnZZ
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
lam_ext
\end{verbatim}
\begin{theorem}\label{thm:mgbgngpffgiheh} $${\unicdcdadad X .  {\unicdcdadad F G : {{\iota}\unicdbdjdcd{\iota}} .  {{({\unicdcdadad x \in {X} .  {{{F}~{x}}={{G}~{x}}}})}\unicdbdjdcd{{({\uniddcgcg x \in {X} .  {{F}~{x}}})}={({\uniddcgcg x \in {X} .  {{G}~{x}}})}}}}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 2a894ae4a36b338440c9116b7d1b5a156eee0387a8f218922dbee9a1525dd98f \\
Pure Prop Address: & TMczyezqH3mj8KqKko9PzTFrNnQbEq2hbYj \\
Theory Prop Id: & 15b7126fd92862295ccc8704bc2c31eecaf79f06db2c59eff164b6dc9e9b9d46 \\
Theory Prop Address: & TMVLMDciL8LE8HAPbirRFgBN1S6reWhpgHE
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
lam_eta
\end{verbatim}
\begin{theorem}\label{thm:mgbgngpffgehbg} ${\unicdcdadad X .  {\unicdcdadad F : {{\iota}\unicdbdjdcd{\iota}} .  {{({\uniddcgcg x \in {X} .  {{({\uniddcgcg x \in {X} .  {{F}~{x}}})}~{x}}})}={({\uniddcgcg x \in {X} .  {{F}~{x}}})}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 19cd9ab03cf4c749ed30f30ed2ed505f627543fbe9a6a2e5eb19aa3c7b0d1b1b \\
Pure Prop Address: & TMTTDo5Up8FsTSMC9bQsVxqiR8BLjPdvHGD \\
Theory Prop Id: & 9103bc442270a76ca14900757db09b5b74bccb4b76e1e17b7ef9f7dd674fc8f9 \\
Theory Prop Address: & TMMRnP58fZgQnvj38xKhFcWRj7vE5fPQZAr
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_2_eta
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfcdpffgehbg} ${\unicdcdadad x y .  {{({\uniddcgcg i \in {2} .  {{({x},{y})}~{i}}})}={({x},{y})}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 87a4aae7ea69d72da1affd33a6e6fdff7bb4f0d789de45c146aa1dfd53b9aeda \\
Pure Prop Address: & TMLTia4kgENRM1HdxJL6n2c4optHfFxVxdR \\
Theory Prop Id: & 29558e38c4342ce7594d397f1a575f3b2c5f24e1032c87cf9c8a8a79b6832c83 \\
Theory Prop Address: & TMGGubBp6qMsgQrvqroY5peGfyYATfj7oYx
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:mgbgngcd}
We define $\mname{lam2}$ to be ${\uniddcgcg X Y F .  {\uniddcgcg x \in {X} .  {\uniddcgcg y \in {{Y}~{x}} .  {{{F}~{x}}~{y}}}}}$ of type ${{\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: & f73bdcf4eeb9bdb2b6f83670b8a2e4309a4526044d548f7bfef687cb949027eb \\
Pure Object Address: & TMYPta1FoiMuP1GN6PBin1Xx2bXh9F4jZu5 \\
Theory Object Id: & 1af26ca6648a0a5f2f504ed4d407dacb2d1295021bfab70e16a756e32019be58 \\
Theory Object Address: & TMFfLmxP1LgSqtznbFPEPY5Ne2h6kro5fyD
\end{tabular}
\end{center}

\end{definition}
\begin{verbatim}
beta2
\end{verbatim}
\begin{theorem}\label{thm:cgfgehbgcd} $${\unicdcdadad X .  {\unicdcdadad Y : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad F : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}} .  {\unicdcdadad x \in {X} .  {\unicdcdadad y \in {{Y}~{x}} .  {{{{{{{\mname{lam2}}~{X}}~{Y}}~{F}}~{x}}~{y}}={{{F}~{x}}~{y}}}}}}}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 2de6dedd220a397af6370f72b7a1335bcfa1475e0d9eb3d9cc7ff55075b114b9 \\
Pure Prop Address: & TMagrn8mKPRRmZwMivWkUiffvhd5tm79Win \\
Theory Prop Id: & 4bb51dcd166eb4dab05760eec9ee7a9c07acd7688f394f84fc37ce9a362ea7f7 \\
Theory Prop Address: & TMGMZXJkR32EUzV9izhKBE2MEoS3MKPLbXm
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
lam2_ext
\end{verbatim}
\begin{theorem}\label{thm:mgbgngcdpffgiheh}
  $$
  \begin{array}{c}
    \unicdcdadad X .  \unicdcdadad Y : {{\iota}\unicdbdjdcd{\iota}} .  \unicdcdadad F G : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}} .  {({\unicdcdadad x \in {X} .  {\unicdcdadad y \in {{Y}~{x}} .  {{{{F}~{x}}~{y}}={{{G}~{x}}~{y}}}}})}\unicdbdjdcd\\
            {{{{{\mname{lam2}}~{X}}~{Y}}~{F}}={{{{\mname{lam2}}~{X}}~{Y}}~{G}}}.
  \end{array}
  $$
  The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 2fcf8329eb8970256dd334aa201b65fa25e730316c3d42fb8e24bbfb8baa1da6 \\
Pure Prop Address: & TMWA1B5WDTBTsPxXTq3a4ASUuADPsARiKwo \\
Theory Prop Id: & 36ee1989db22297f701d46985e3f5b8484beb0cc98783f705be675646c00e858 \\
Theory Prop Address: & TMQRLHS3cYoRzXTpwWXkAqwX3mPwkxYT46Y
\end{tabular}
\end{center}

\end{theorem}

\section{Encodings of Functions and Predicates as Sets}

\begin{definition}\label{def:fgogdgpgegfgpffh}
We define $\mname{encode\_u}$ to be ${lam}$ of type ${{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{\iota}})}\unicdbdjdcd{\iota}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 8acbb2b5de4ab265344d713b111d82b0048c8a4bf732a67ad35f1054a4eb4642 \\
Pure Object Address: & TMMDLyvQS3eoiP32KBXjSQyuvc4keN5yMmX \\
Theory Object Id: & d64bcbbefe13f9fc0035d2317f017d9ee3aeb3de90b836ed7cbe11d46f478799 \\
Theory Object Address: & TMS2X4GvB3DZiVdQjy5ZeDZQVVCDuJBZvgW
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:egfgdgpgegfgpffh}
We define $\mname{decode\_u}$ to be ${\mname{ap}}$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & c7aaa670ef9b6f678b8cf10b13b2571e4dc1e6fde061d1f641a5fa6c30c09d46 \\
Pure Object Address: & TMRkKHvzv8Tta9AhRXsVE4k7dQ68XWymCoD \\
Theory Object Id: & a4d82c5a3643a7e174676c313ef995e0307b3b56f57e8ae761b7c6033bbc40db \\
Theory Object Address: & TMULGKR83zvLzsaT5wtaLqEme8A8TV9uVcG
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:fgogdgpgegfgpfcg}
We define $\mname{encode\_b}$ to be ${\uniddcgcg X F .  {{{{\mname{lam2}}~{X}}~{({\uniddcgcg \_ .  {X}})}}~{F}}}$ of type ${{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}})}\unicdbdjdcd{\iota}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 4c89a6c736b15453d749c576f63559855d72931c3c7513c44e12ce14882d2fa7 \\
Pure Object Address: & TMEnk3YrwKupP9z6sTwXokwBz2J6VVGp5Zh \\
Theory Object Id: & 2857218138584f5287cfe4ade2be20096822070b538af7d77aac47d32304f2b6 \\
Theory Object Address: & TMEomjpi2NLe2mLYiaW5hqvmjvtSXDYVCri
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:egfgdgpgegfgpfcg}
We define $\mname{decode\_b}$ to be ${\uniddcgcg F x y .  {{{F}~{x}}~{y}}}$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 1024fb6c1c39aaae4a36f455b998b6ed0405d12e967bf5eae211141970ffa4fa \\
Pure Object Address: & TMLJXUAwxDCzt7HeMEhmMtFjPFH82BuahcJ \\
Theory Object Id: & 3b93ea7cf603f82962cfaa76e280e5218df781b7ff8b501b4dea38f2c76f0ce4 \\
Theory Object Address: & TMdai21pMbN5LhRjuzG8fbyq6jLXZp8xvQD
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:fgogdgpgegfgpfah}
We define $\mname{encode\_p}$ to be ${\uniddcgcg X P .  {{{\mname{Sep}}~{X}}~{P}}}$ of type ${{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{o}})}\unicdbdjdcd{\iota}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & f336a4ec8d55185095e45a638507748bac5384e04e0c48d008e4f6a9653e9c44 \\
Pure Object Address: & TMUtfXxDDLj9Tk47vMVXxn7X4YsuGxPH9iG \\
Theory Object Id: & 7008ec0ee19d11cc67c5f11635c82852ccb27360b8bd8431676b0c7e03219428 \\
Theory Object Address: & TMU5xEoVJ4JK7LsxiB8DMm5ouqBu3Rgy3CL
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:egfgdgpgegfgpfah}
We define $\mname{decode\_p}$ to be ${\uniddcgcg P x .  {{x} \in {P}}}$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 02231a320843b92b212e53844c7e20e84a5114f2609e0ccf1fe173603ec3af98 \\
Pure Object Address: & TMNmYnbPvxg781LaE377972CwGGRP6A4t2c \\
Theory Object Id: & e9507346effb55f2b66cdfb801523074014fb64eeccb8e226d8fdc9359337830 \\
Theory Object Address: & TMEnXjKVptqvfEYytFygN49BmBFhyNV8YJ8
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:fgogdgpgegfgpfch}
We define $\mname{encode\_r}$ to be ${\uniddcgcg X R .  {{{{\mname{Sep2}}~{X}}~{({\uniddcgcg \_ .  {X}})}}~{R}}}$ of type ${{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}})}\unicdbdjdcd{\iota}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 17bc9f7081d26ba5939127ec0eef23162cf5bbe34ceeb18f41b091639dd2d108 \\
Pure Object Address: & TMVAvkv75vEbx8iL4LYfx77aKBqGpyF2x3q \\
Theory Object Id: & e6e31b91e856a7c568a0d85625bf50833d9a6ba3696590b494c9be80206757f7 \\
Theory Object Address: & TMaAgBFCWYRYoi83L9vFaz2ee8AkoYAQ7dn
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:egfgdgpgegfgpfch}
We define $\mname{decode\_r}$ to be ${\uniddcgcg R x y .  {{({x},{y})} \in {R}}}$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & f2f91589fb6488dd2bad3cebb9f65a57b7d7f3818091dcc789edd28f5d0ef2af \\
Pure Object Address: & TMUxUtfWjzRHvsq1Hh2nzZmnFZn4W4k5yZ1 \\
Theory Object Id: & b93a65581af63e84497eb9a1ce7d86376ff948ca78630d50cb4fb879fe8b35a6 \\
Theory Object Address: & TMGH5mJWrbQCiFMwfcAubZ4xHfJdMSJxuWk
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:fgogdgpgegfgpfdg}
We define $\mname{encode\_c}$ to be $${\uniddcgcg X C .  {{{\mname{Sep}}~{({{\mname{Power}}~{X}})}}~{({\uniddcgcg U .  {({{C}~{({\uniddcgcg x .  {{x} \in {U}}})}})}})}}}$$ of type ${{\iota}\unicdbdjdcd{{({{({{\iota}\unicdbdjdcd{o}})}\unicdbdjdcd{o}})}\unicdbdjdcd{\iota}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 02824c8d211e3e78d6ae93d4f25c198a734a5de114367ff490b2821787a620fc \\
Pure Object Address: & TMPoUwriPcHMpXKUSPr2n5eeCVHPwVTvJjh \\
Theory Object Id: & abcb4f0b23ce219b19f08deedb28f9946fc52a200cd5ab9c101ffc24d294a926 \\
Theory Object Address: & TMdFVb6jHzinhqHU8R1E9GETd9GtqL67GFs
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:egfgdgpgegfgpfdg}
We define $\mname{decode\_c}$ to be $${\uniddcgcg C U .  {\unicdcdaddd V .  {{({\unicdcdadad x .  {{{U}~{x}}\unicdbdjded{{x} \in {V}}}})}\unicdcdcdhd{{V} \in {C}}}}}$$ of type ${{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{o}})}\unicdbdjdcd{o}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 47a1eff65bbadf7400d8f2532141a437990ed7a8581fea1db023c7edd06be32c \\
Pure Object Address: & TMGRAT91AwN8Jcefxc45YTgTK8w2jHVUmwH \\
Theory Object Id: & 3edd4a21f511f37d2fa9b701d6bceefc3ec4979b0aa937da2224b9712a600388 \\
Theory Object Address: & TMKMbEUcTZ35ASSvnJwrdeRpZrpSFw3akQn
\end{tabular}
\end{center}

\end{definition}
\begin{verbatim}
decode_encode_u
\end{verbatim}
\begin{theorem}\label{thm:egfgdgpgegfgpffgogdgpgegfgpffh}
  $${\unicdcdadad X .  {\unicdcdadad F : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad x \in {X} .  {{{{\mname{decode\_u}}~{({{{\mname{encode\_u}}~{X}}~{F}})}}~{x}}={{F}~{x}}}}}}.$$
  The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 95991de564f22218049f5c01a2054c9f531e2a0e7f89348f4cd3cce56269ee6a \\
Pure Prop Address: & TMW5SkUgFpNvxZtwNs5tigJKy4uVF4aLEX4 \\
Theory Prop Id: & b5182dff18aa9200707f42f128e18ba010c3c5b0a3a598682cfd9fe3e36def5d \\
Theory Prop Address: & TMUK7trdHToYkqBA9FA7nyBfnGCJVnzMrdt
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
encode_u_ext
\end{verbatim}
\begin{theorem}\label{thm:fgogdgpgegfgpffhpffgiheh} $${\unicdcdadad X .  {\unicdcdadad F F' : {{\iota}\unicdbdjdcd{\iota}} .  {{({\unicdcdadad x \in {X} .  {{{F}~{x}}={{F'}~{x}}}})}\unicdbdjdcd{{{{\mname{encode\_u}}~{X}}~{F}}={{{\mname{encode\_u}}~{X}}~{F'}}}}}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 2a894ae4a36b338440c9116b7d1b5a156eee0387a8f218922dbee9a1525dd98f \\
Pure Prop Address: & TMczyezqH3mj8KqKko9PzTFrNnQbEq2hbYj \\
Theory Prop Id: & 15b7126fd92862295ccc8704bc2c31eecaf79f06db2c59eff164b6dc9e9b9d46 \\
Theory Prop Address: & TMVLMDciL8LE8HAPbirRFgBN1S6reWhpgHE
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
decode_encode_b
\end{verbatim}
\begin{theorem}\label{thm:egfgdgpgegfgpffgogdgpgegfgpfcg} $${\unicdcdadad X .  {\unicdcdadad F : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}} .  {\unicdcdadad x y \in {X} .  {{{{{\mname{decode\_b}}~{({{{\mname{encode\_b}}~{X}}~{F}})}}~{x}}~{y}}={{{F}~{x}}~{y}}}}}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 3ee73039a869eb8092f936deea2d3411e72305d82a14a6e988c4a1bf8d16ca83 \\
Pure Prop Address: & TMMn46yDXgo1kjEyPcuewexTo1Z9Ay42Wje \\
Theory Prop Id: & 8d10ce96d1c3a115ca4a3c97096a0ef9b1241c7944342a034d52676ec1576ca9 \\
Theory Prop Address: & TMNxzXmNthWVuFuJrEbR2rZdFYrRPUUpZEg
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
encode_b_ext
\end{verbatim}
\begin{theorem}\label{thm:fgogdgpgegfgpfcgpffgiheh} $${\unicdcdadad X .  {\unicdcdadad F F' : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}} .  {{({\unicdcdadad x y \in {X} .  {{{{F}~{x}}~{y}}={{{F'}~{x}}~{y}}}})}\unicdbdjdcd{{{{\mname{encode\_b}}~{X}}~{F}}={{{\mname{encode\_b}}~{X}}~{F'}}}}}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 332cea87dd4a05957a0e32b3f6ad9a7a65f7c156b384ab1468dabd57ed690e07 \\
Pure Prop Address: & TMF4RHp7VrPNSphZfAnfvL4aSLfmrbynJJb \\
Theory Prop Id: & d010291fc325252d96b8617d5107ca33d0bd9906a978a831ac853d04850ba94b \\
Theory Prop Address: & TMMdZbVStJuaWiLad5uZeQNMN7wid9XW5qy
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
decode_encode_p
\end{verbatim}
\begin{theorem}\label{thm:egfgdgpgegfgpffgogdgpgegfgpfah} $${\unicdcdadad X .  {\unicdcdadad P : {{\iota}\unicdbdjdcd{o}} .  {\unicdcdadad x \in {X} .  {{({{{\mname{decode\_p}}~{({{{\mname{encode\_p}}~{X}}~{P}})}}~{x}})}={({{P}~{x}})}}}}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 76e0c4faba69952ec67742eeb94d927de40a5f192c9d6aecccd1035a84de0723 \\
Pure Prop Address: & TML6EPefmfw97vntVGgeVFz8HyFXfeVpHzC \\
Theory Prop Id: & d58325ff2359f69c9e2bd75a02be4ef6854835056c014507b6c92d4e2cf7ceb3 \\
Theory Prop Address: & TMcADFusuPHtjARgdAGwzLTRfoHmoLdpnbx
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
encode_p_ext
\end{verbatim}
\begin{theorem}\label{thm:fgogdgpgegfgpfahpffgiheh} $${\unicdcdadad X .  {\unicdcdadad P P' : {{\iota}\unicdbdjdcd{o}} .  {{({\unicdcdadad x \in {X} .  {{{P}~{x}}\unicdbdjded{{P'}~{x}}}})}\unicdbdjdcd{{{{\mname{encode\_p}}~{X}}~{P}}={{{\mname{encode\_p}}~{X}}~{P'}}}}}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 3b7abeffd741d27cffec5971d6a6a069502f5125137259639ec8c7fe9e08137e \\
Pure Prop Address: & TMJ9Y8Nubbgp1Z251WmGmhd5ZqmvRxaibVa \\
Theory Prop Id: & c103040e5a72e28e42a8b370fe0915a43c227b83d6405d91b72df648a194fbe7 \\
Theory Prop Address: & TMaHzJHmzSrfHeEaV6hRXwCRYPY5P2JHZy1
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
decode_encode_r
\end{verbatim}
\begin{theorem}\label{thm:egfgdgpgegfgpffgogdgpgegfgpfch} $${\unicdcdadad X .  {\unicdcdadad R : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  {\unicdcdadad x y \in {X} .  {{({{{{\mname{decode\_r}}~{({{{\mname{encode\_r}}~{X}}~{R}})}}~{x}}~{y}})}={({{{R}~{x}}~{y}})}}}}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 1014a9bcf05c5f44d84ef0e62da543b87727aca195ad8496cd18d175889c170e \\
Pure Prop Address: & TMGVNLSr6YarTJyvLJtRUNqkQhdbWL1MPdw \\
Theory Prop Id: & 08a8a48da6a92bd5fc4224fbd113b9d97621ed1e4dd0440c1782a73cdced5b82 \\
Theory Prop Address: & TMKQ1xev2H6uLTz75vjFPQTwWGXdKuTWAw4
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
encode_r_ext
\end{verbatim}
\begin{theorem}\label{thm:fgogdgpgegfgpfchpffgiheh} $${\unicdcdadad X .  {\unicdcdadad R R' : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  {{({\unicdcdadad x y \in {X} .  {{{{R}~{x}}~{y}}\unicdbdjded{{{R'}~{x}}~{y}}}})}\unicdbdjdcd{{{{\mname{encode\_r}}~{X}}~{R}}={{{\mname{encode\_r}}~{X}}~{R'}}}}}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 7e28f4c2e174003767040fb758e5a7abd8bf6f6859c428b0cba2d3531a22173d \\
Pure Prop Address: & TManVioQo3HkeWcxBTPLk7ZWsNqo8qG2Y11 \\
Theory Prop Id: & fa3b122d8b29e30bf435481e40c1cf6b59f126107a670fcc9198128c41d97b0c \\
Theory Prop Address: & TMEyPUz1f5trR77TrCy5T6ALTtFw5QB8hNw
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
decode_encode_c
\end{verbatim}
\begin{theorem}\label{thm:egfgdgpgegfgpffgogdgpgegfgpfdg}
  $$
  \begin{array}{c}
    \unicdcdadad X .  \unicdcdadad C : {{({{\iota}\unicdbdjdcd{o}})}\unicdbdjdcd{o}} .  \unicdcdadad U : {{\iota}\unicdbdjdcd{o}} .  {({\unicdcdadad x .  {{{U}~{x}}\unicdbdjdcd{{x} \in {X}}}})}\unicdbdjdcd\\
            {{({{{\mname{decode\_c}}~{({{{\mname{encode\_c}}~{X}}~{C}})}}~{U}})}={({{C}~{U}})}}.
  \end{array}
  $$
  The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 7a75630d7138237a35850129ec0899748c1ef7c52bef0bde27d23694b7dea800 \\
Pure Prop Address: & TMYedqhNDgqDPXcTzM355Rp53xYHrH9uyDf \\
Theory Prop Id: & 880bfbe387f844851c05145a1db503fb36936d2294f75af51c5ce2785d96bf21 \\
Theory Prop Address: & TMG3Jf332EdHAKZvGPSKqfyZgKCYjmL7sQ3
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
encode_c_ext
\end{verbatim}
\begin{theorem}\label{thm:fgogdgpgegfgpfdgpffgiheh}
  $$
  \begin{array}{c}
    \unicdcdadad X .  \unicdcdadad C C' : {{({{\iota}\unicdbdjdcd{o}})}\unicdbdjdcd{o}} .  {({\unicdcdadad U : {{\iota}\unicdbdjdcd{o}} .  {{({\unicdcdadad x .  {{{U}~{x}}\unicdbdjdcd{{x} \in {X}}}})}\unicdbdjdcd{({{{C}~{U}}\unicdbdjded{{C'}~{U}}})}}})}\unicdbdjdcd\\
          {{{{\mname{encode\_c}}~{X}}~{C}}={{{\mname{encode\_c}}~{X}}~{C'}}}.
  \end{array}
  $$
  The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & baacc5826835bdf9ff6b14cd7397faa14ac4deec11a936d577ef7808babe0837 \\
Pure Prop Address: & TMKwAfPDG9pG12Fvp5oGJz7NXs7naikE7x8 \\
Theory Prop Id: & 0c5483759fc520ad24416714aabea399eb7cb84016cdcbc605ffec9d6504a0b0 \\
Theory Prop Address: & TMTNaV2fXyXXwapDqmZgoh9Bwtevm9wRREw
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
setprod_mon
\end{verbatim}
\begin{theorem}\label{thm:dhfgehahchpgegpfngpgog} ${\unicdcdadad X Y : {\iota} .  {{{X} \subseteq {Y}}\unicdbdjdcd{\unicdcdadad Z W : {\iota} .  {{{Z} \subseteq {W}}\unicdbdjdcd{{{X}\unicdbgcdgg{Z}} \subseteq {{Y}\unicdbgcdgg{W}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 63d72a5736b6dad618fb3fe72b9bce7bd5535acd2498fd7efcd60df85fe65ef0 \\
Pure Prop Address: & TMa6kynUKR5kseqtucWFdECHsZBBaPS7mrj \\
Theory Prop Id: & a74bcaef7267fce98f2a364fb6c5734d406f80cb027560a59947536a21433041 \\
Theory Prop Address: & TMRkBMu4VTR26BPV4YUTQHzEAUt27bx9EXj
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
setprod_mon0
\end{verbatim}
\begin{theorem}\label{thm:dhfgehahchpgegpfngpgogad} ${\unicdcdadad X Y : {\iota} .  {{{X} \subseteq {Y}}\unicdbdjdcd{\unicdcdadad Z : {\iota} .  {{{X}\unicdbgcdgg{Z}} \subseteq {{Y}\unicdbgcdgg{Z}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 7bd32d8dd36d89ace87f57f3e3d5d041a6b193856d3cabf95317325c73b3df3f \\
Pure Prop Address: & TMP3EP5PaqbZ1cxhh8WmVQQLcsFCXTW7rCy \\
Theory Prop Id: & 455a4284ff6e2959b9e8a657510f722883ee919b1b17703dac1942a7edbdda0c \\
Theory Prop Address: & TMVWdnQ7qpSHvYcKK6yidsz39oPTDKBkq8r
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
setprod_mon1
\end{verbatim}
\begin{theorem}\label{thm:dhfgehahchpgegpfngpgogbd} ${\unicdcdadad X : {\iota} .  {\unicdcdadad Z W : {\iota} .  {{{Z} \subseteq {W}}\unicdbdjdcd{{{X}\unicdbgcdgg{Z}} \subseteq {{X}\unicdbgcdgg{W}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 6e2e07464345fa4f1a371f688df924851a665ecd94aaed51223be1ae886bc23e \\
Pure Prop Address: & TMSnywK9u9fk9Ed6jbYvBs1ZUC6LKFAgpKS \\
Theory Prop Id: & a90d34c038dd8dbab84e007a80008f440fca47232d9907f639d52500513f5a4f \\
Theory Prop Address: & TMPygssHhnaE9kaN6NAnhRiDZooV9D1npXA
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
pair_eta_Subq
\end{verbatim}
\begin{theorem}\label{thm:ahbgjgchpffgehbgpfdffhcgbh} ${\unicdcdadad w .  {{{{pair}~{({{w}~{0}})}}~{({{w}~{1}})}} \subseteq {w}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 4f3ebfd1a2003335ce7adcc7c9b187a22011f65ae156fa1445a702cf001c3927 \\
Pure Prop Address: & TMVusjsTB3ex7nLq2jbiMtM6jhKF3AJBbiD \\
Theory Prop Id: & 74e00933da8b7173ceedb24a78d36aedd8271dc642ef0da29ab7608538b9bcb4 \\
Theory Prop Address: & TMFvqxkSHYjcmeNXXjANHaP3wFYajKhHUMA
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Sigma_eta
\end{verbatim}
\begin{theorem}\label{thm:dfjghgngbgpffgehbg} ${\unicdcdadad X : {\iota} .  {\unicdcdadad Y : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad z \in {({\unicdcdbdbd x \in {X} .  {{Y}~{x}}})} .  {{{{pair}~{({{z}~{0}})}}~{({{z}~{1}})}}={z}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 49ff5151b49302ac99558664cc438f0a4d40498c14aadb3e399282edcabda3fb \\
Pure Prop Address: & TMSCgjHPA66KEFpj15NkePtPi8MUx8TeT4Z \\
Theory Prop Id: & 8049133218c094e36a326d0302747b6faed7820279c4ca43b4aaaba59da8d86f \\
Theory Prop Address: & TMZAcyQRmA4RUYzXLLDvy9X9mq3N9qQySRD
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
ReplEq_setprod_ext
\end{verbatim}
\begin{theorem}\label{thm:cffgahmgfebhpfdhfgehahchpgegpffgiheh}
  $$
  \begin{array}{c}
    \unicdcdadad X Y .  \unicdcdadad F G : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}} .  {({\unicdcdadad x \in {X} .  {\unicdcdadad y \in {Y} .  {{{{F}~{x}}~{y}}={{{G}~{x}}~{y}}}}})}\unicdbdjdcd\\
          {{\{{{{F}~{({{w}~{0}})}}~{({{w}~{1}})}}|w \in {{X}\unicdbgcdgg{Y}}\}}={\{{{{G}~{({{w}~{0}})}}~{({{w}~{1}})}}|w \in {{X}\unicdbgcdgg{Y}}\}}}.
  \end{array}
  $$
  The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & c486ab09b581a313204dc303b15e3611e31121022211233d7418fa02f6cc7299 \\
Pure Prop Address: & TMWwkDTMCqBE34kbrXdyyAhqVm2sbfTQjce \\
Theory Prop Id: & f689a07de22b0aec4db3cba58ed366ef7f1c7bf74bbf6b2e727fd32a368b68eb \\
Theory Prop Address: & TMTDNNDk6TRtimfgiJDfHre2Zghrr4cfc5k
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_p_3_tuple
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfahpfddpfehfhahmgfg} ${\unicdcdadad x y z : {\iota} .  {{{\mname{tuple\_p}}~{3}}~{({x},{y},{z})}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & cf993987b43146748735706a7857f006cbd148697f781826b45bb9c65766a0d4 \\
Pure Prop Address: & TMF2RMvq3PMYzBY3dD3WXb7CLziCt6USMZD \\
Theory Prop Id: & 77393568486dac4f6831171dad84d01e9b6df6e1d91b218fcdd823e87841c937 \\
Theory Prop Address: & TMR9fqGfQKrPPzAcNDvk14YN5xCHfLnGWnB
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_p_4_tuple
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfahpfedpfehfhahmgfg} ${\unicdcdadad x y z w : {\iota} .  {{{\mname{tuple\_p}}~{4}}~{({x},{y},{z},{w})}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 5cb9dd366dfb4bd3932546b2b6ce146f154c0ab4a373c38ab6422bfba5679085 \\
Pure Prop Address: & TMdpGdQnb2pjcxbUxX2XUCUMgbpPFfAHvzv \\
Theory Prop Id: & 58c3b26de9e903a7f82ccf8e0237aeba24a5fc22ffdc521a5446cbca1243b942 \\
Theory Prop Address: & TMMXKVHZmRa3TWvKaoU4TWL4zLf8ocjRiox
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Pi_Power_1
\end{verbatim}
\begin{theorem}\label{thm:afjgpfafpghhfgchpfbd} $${\unicdcdadad X : {\iota} .  {\unicdcdadad Y : {{\iota}\unicdbdjdcd{\iota}} .  {{({\unicdcdadad x \in {X} .  {{{Y}~{x}} \in {{\mname{Power}}~{1}}}})}\unicdbdjdcd{{({\unicdcdadgg x \in {X} .  {{Y}~{x}}})} \in {{\mname{Power}}~{1}}}}}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 749337506bbff9c2bed1261a0faa5ea2bf92d0442dacccd5c665ddabd12a5e41 \\
Pure Prop Address: & TMSQqTJzh57zKzeJmXEtHFgtRKNkkoRZ5Yg \\
Theory Prop Id: & 53185f562ff7551b58214aa425c4679c294ce17583608a17fded6fd0251b725e \\
Theory Prop Address: & TMQ6JF9rZDAhvvypZvKH3NTaGvdGWRexq52
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Pi_0_dom_mon
\end{verbatim}
\begin{theorem}\label{thm:afjgpfadpfegpgngpfngpgog}
  $$
  \begin{array}{c}
    \unicdcdadad X Y : {\iota} .  \unicdcdadad A : {{\iota}\unicdbdjdcd{\iota}} .  {{X} \subseteq {Y}}\unicdbdjdcd\\
                 {{({\unicdcdadad y \in {Y} .  {{{y}\unicdcdadjd{X}}\unicdbdjdcd{{0} \in {{A}~{y}}}}})}\unicdbdjdcd{{({\unicdcdadgg x \in {X} .  {{A}~{x}}})} \subseteq {\unicdcdadgg y \in {Y} .  {{A}~{y}}}}}.
  \end{array}
  $$
  The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & afd68d2c59d656bb239ccbebabc9bd0a0bd90439f78158e146e8fc748463f7d5 \\
Pure Prop Address: & TMbgKzF8UHU8QuRUAoJPZtfPZpKdMV6fH4X \\
Theory Prop Id: & 8b265dd368d5ae9935219b30f9ab92687d8f287fc776d2c4ff902bdf59efc063 \\
Theory Prop Address: & TMbVdN1MHHnjdbTQaqcsa3c43EUJLPRyXxf
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Pi_cod_mon
\end{verbatim}
\begin{theorem}\label{thm:afjgpfdgpgegpfngpgog} $${\unicdcdadad X : {\iota} .  {\unicdcdadad A B : {{\iota}\unicdbdjdcd{\iota}} .  {{({\unicdcdadad x \in {X} .  {{{A}~{x}} \subseteq {{B}~{x}}}})}\unicdbdjdcd{{({\unicdcdadgg x \in {X} .  {{A}~{x}}})} \subseteq {\unicdcdadgg x \in {X} .  {{B}~{x}}}}}}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 3f6023959e78603c118adb6a4ff1b02d56955380be26e0747fae716b2cd95d97 \\
Pure Prop Address: & TMaeWxiHTomfFysYznzJfEDq1N349zj13nT \\
Theory Prop Id: & c65ee3b2fffcc8ba8c7c4d2fef3d6aee20f82c17cf3c09dc7a7e72f8a251d98a \\
Theory Prop Address: & TMZud88tiwxGZkbhtpgTUFSV8FPmskRGQHU
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Pi_0_mon
\end{verbatim}
\begin{theorem}\label{thm:afjgpfadpfngpgog}
  $$
  \begin{array}{c}
    \unicdcdadad X Y : {\iota} .  \unicdcdadad A B : {{\iota}\unicdbdjdcd{\iota}} .  {({\unicdcdadad x \in {X} .  {{{A}~{x}} \subseteq {{B}~{x}}}})}\unicdbdjdcd{{X} \subseteq {Y}}\unicdbdjdcd\\
                 {{({\unicdcdadad y \in {Y} .  {{{y}\unicdcdadjd{X}}\unicdbdjdcd{{0} \in {{B}~{y}}}}})}\unicdbdjdcd{{({\unicdcdadgg x \in {X} .  {{A}~{x}}})} \subseteq {\unicdcdadgg y \in {Y} .  {{B}~{y}}}}}.
  \end{array}
  $$
  The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 74a4777899bd48bce73a6950d5c843aa0ef4895865b762f7d6e9504173de2d2a \\
Pure Prop Address: & TMQsGPc8N3Ubv5n8RJVHF7c8JKNSvH4P3Mv \\
Theory Prop Id: & d876ad3e474910e13beae3e36658e1cba27e007339b5c367e122cea96ba5a530 \\
Theory Prop Address: & TMJpkgSLqGH7HNbMBRcohiUdmHzCQFD3orZ
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
setexp_2_eq
\end{verbatim}
\begin{theorem}\label{thm:dhfgehfgihahpfcdpffgbh} ${\unicdcdadad X : {\iota} .  {{{X}\unicdbgcdgg{X}}={{X}^{{2}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & ffa8ca03579eb26597d40ec371bf1e68b77c9e00e70e22aa75cb005b599928fa \\
Pure Prop Address: & TMQo8m7mTFS5ULGe5RFn9ewAV6USEFmXGEe \\
Theory Prop Id: & 97b6d296a52705b137946c7684a42f90e6dcdc16ccd27fcc6f843903334d6124 \\
Theory Prop Address: & TMU8ZQ356N7f1ur9PqrcyhFvUrEU8Uw3pCd
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
setexp_0_dom_mon
\end{verbatim}
\begin{theorem}\label{thm:dhfgehfgihahpfadpfegpgngpfngpgog} ${\unicdcdadad A : {\iota} .  {{{0} \in {A}}\unicdbdjdcd{\unicdcdadad X Y : {\iota} .  {{{X} \subseteq {Y}}\unicdbdjdcd{{{A}^{{X}}} \subseteq {{A}^{{Y}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & c82a77bea63c3045dd2d0390019427d36b3850e817a7c7d81c9d44dd83da9951 \\
Pure Prop Address: & TMQY2MPGRLH7DstKxCBvTt7ycuHKzG3Egta \\
Theory Prop Id: & 320220221d2ff027b0b203b874e4695ae660ced55ac0790f282597f5e9613e9f \\
Theory Prop Address: & TMdJC2UYVneWjpMTvmnbkFG2QrY6sZa7dzC
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
setexp_0_mon
\end{verbatim}
\begin{theorem}\label{thm:dhfgehfgihahpfadpfngpgog} ${\unicdcdadad X Y A B : {\iota} .  {{{0} \in {B}}\unicdbdjdcd{{{A} \subseteq {B}}\unicdbdjdcd{{{X} \subseteq {Y}}\unicdbdjdcd{{{A}^{{X}}} \subseteq {{B}^{{Y}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 9626c863679499ee9efb3a97f6d2c94d448186ea2212527485c1494342277958 \\
Pure Prop Address: & TMSVKPxofDcRCRvbvF6CiPxy7w1U9GV3abU \\
Theory Prop Id: & 90c509fbef3ca7822c8b20ec7e5a62fd62a043b9500aaa739b5118a3c994d408 \\
Theory Prop Address: & TMG4aTTfVaxVUnsqSgBoVVNATLoR7h38zjG
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
nat_in_setexp_mon
\end{verbatim}
\begin{theorem}\label{thm:ogbgehpfjgogpfdhfgehfgihahpfngpgog} ${\unicdcdadad A : {\iota} .  {{{0} \in {A}}\unicdbdjdcd{\unicdcdadad n .  {{{\mname{nat\_p}}~{n}}\unicdbdjdcd{\unicdcdadad m \in {n} .  {{{A}^{{m}}} \subseteq {{A}^{{n}}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d4aff1269d336f4267535d4b630549f976211672cd2893c8f0d5f93ccc2a2c01 \\
Pure Prop Address: & TMHmDB4dHXevKqyYjk66EaYCALxGuURyksG \\
Theory Prop Id: & 325485fa49bc41efd250c31eb18bded07de4228f53ab976ea68b483631dc46be \\
Theory Prop Address: & TMX7YsW1eVF8qPSQpQudbRa9xp2Q6wGVEfD
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tupleI0
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgjead} ${\unicdcdadad X Y x .  {{{x} \in {X}}\unicdbdjdcd{{({0},{x})} \in {({X},{Y})}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a5d9e60bb578510eba8f8727ca81d4ad6c6ea416e3b1dec75e56736f2c7fbf28 \\
Pure Prop Address: & TMbWA1F32KHzES5haJKo6Ltd6Myvmdja6kj \\
Theory Prop Id: & 7bad4e2f646b78cc8e4ab2dde15f4dad2279a633db69af2d130325d2df660497 \\
Theory Prop Address: & TMYRiZH6QeEcQSbTsa8ff35vULKtFPjDWGZ
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tupleI1
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgjebd} ${\unicdcdadad X Y y .  {{{y} \in {Y}}\unicdbdjdcd{{({1},{y})} \in {({X},{Y})}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 5c347a6088d371c6a7be279b519d891f8b247a1dc86c7f1a5e4e91182d2cd741 \\
Pure Prop Address: & TMR457F4pvZZp7RcTd3TbZY6m59BdcrF2rh \\
Theory Prop Id: & 5e3cb317730d8131182f7c240578e9b710c06861aa264924c853babd66ad53f1 \\
Theory Prop Address: & TMQKbRaumSCTKfCNkFDrzfYb7gjLPbdz9bg
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tupleE
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgfe} $${\unicdcdadad X Y z .  {{{z} \in {({X},{Y})}}\unicdbdjdcd{{({\unicdcdaddd x \in {X} .  {{z}={({0},{x})}}})}\unicdcdcdid{({\unicdcdaddd y \in {Y} .  {{z}={({1},{y})}}})}}}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 8b6d364ac254012dfb266e48ccd8017c4df7092dc82d2f6356aa98f2c113f819 \\
Pure Prop Address: & TMaevMuU9VPUjmzk93asQnRSf6s5giQjEGz \\
Theory Prop Id: & 226332642373ce44237e3431b4e96d902d54149ae33bde4bedb64b30fb8d0fa2 \\
Theory Prop Address: & TMdn86EVVTVBkyXsXj9Vmq1oLxSWWr4xxfb
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_2_Sigma
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfcdpfdfjghgngbg} ${\unicdcdadad X : {\iota} .  {\unicdcdadad Y : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad x \in {X} .  {\unicdcdadad y \in {{Y}~{x}} .  {{({x},{y})} \in {\unicdcdbdbd x \in {X} .  {{Y}~{x}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d4a9d90bcc14a1607b933d2b6324f74a12e560f1ee23d66bbef65f0ab2300245 \\
Pure Prop Address: & TMTxDywb49ok9weqR5PA1YkH5HYVVQgfmLa \\
Theory Prop Id: & de381fee5dd742f3e056c75fdc7abdebc389a9d213f325ce23fff6b0562da398 \\
Theory Prop Address: & TMYB1uFbN7KQg4EMgzCmiEUJxJcauCrH6gi
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_2_setprod
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfcdpfdhfgehahchpgeg} ${\unicdcdadad X : {\iota} .  {\unicdcdadad Y : {\iota} .  {\unicdcdadad x \in {X} .  {\unicdcdadad y \in {Y} .  {{({x},{y})} \in {{X}\unicdbgcdgg{Y}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & e907b80c4db444253db900e46741dbeb4c373f9357cc51990287b6b4bc4e0111 \\
Pure Prop Address: & TMU5XWQo6K7rWoGntpngjoB7dZXxPoSYoxC \\
Theory Prop Id: & 1f9d7fcc7017d00b96708fc1b8cd4c299aede7855c9c051ad9ed1f17edf0696a \\
Theory Prop Address: & TMQby1erMukDCSudbBu6DXLdSmpJnUwy4bN
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_Sigma_eta
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfdfjghgngbgpffgehbg} ${\unicdcdadad X : {\iota} .  {\unicdcdadad Y : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad z \in {({\unicdcdbdbd x \in {X} .  {{Y}~{x}}})} .  {{({{z}~{0}},{{z}~{1}})}={z}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 7cc266621e49b9c431179e0045a15c6c2bd49d0bb6d49aefbb923becb4f3b9ee \\
Pure Prop Address: & TMSgpyjZ757izmXroHBFU7jiFn39AxWAcPa \\
Theory Prop Id: & d965e01dd42fa888cdd06e063200196d2578c975d5c706f981c47060524c38ec \\
Theory Prop Address: & TMXQjnReFQQDxxkiWBRLot9EZBBJmxctC5k
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
apI2
\end{verbatim}
\begin{theorem}\label{thm:bgahjecd} ${\unicdcdadad f x y .  {{{({x},{y})} \in {f}}\unicdbdjdcd{{y} \in {{f}~{x}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 334f53713d549322405aec659458426a25e4aa7e1dcba4fbfad411bfe0628835 \\
Pure Prop Address: & TMcAcmb8L7yHFzTFqsQ3a4kWhFMbRKovMNC \\
Theory Prop Id: & 6f716abb65c7606ae6b5749d37dda052e685a4d4f7519d400bedcc1fcee23320 \\
Theory Prop Address: & TMTjJZzRce6va39d2z3pncuj6jrfGtJ3eoy
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
apE2
\end{verbatim}
\begin{theorem}\label{thm:bgahfecd} ${\unicdcdadad f x y .  {{{y} \in {{f}~{x}}}\unicdbdjdcd{{({x},{y})} \in {f}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 2a2c24116214dee00936cfdd3231d8a70a4ff6d3efda38a95a724e0e4cd155a1 \\
Pure Prop Address: & TMWSE1naRk6JPjqHbwkoVtBu4k9tumZgTyX \\
Theory Prop Id: & 57702acf505aa564187ee95d1b240f6ea6befe178029989924da2df6cea2a42f \\
Theory Prop Address: & TMGiJF872peSuqfKRH9jn9RcqbjuUAS8qbD
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
ap_const_0
\end{verbatim}
\begin{theorem}\label{thm:bgahpfdgpgogdhehpfad} ${\unicdcdadad x .  {{{0}~{x}}={0}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a4ea444af8365c1c911ed81357b063cf1823fcc07b1e9fa2848a6e26d14a5f23 \\
Pure Prop Address: & TMZQjyRKodf7sfVuPrUmzZLt88BXcuEKsxk \\
Theory Prop Id: & f66b937fdac9351c50455abd7b2f8c4008f271f243b5a551b8020099b6ea59d9 \\
Theory Prop Address: & TMYDg1Trrx3692oVX9Md1Ss8h7pKgzipsXy
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_2_in_A_2
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfcdpfjgogpfbepfcd} ${\unicdcdadad x y A .  {{{x} \in {A}}\unicdbdjdcd{{{y} \in {A}}\unicdbdjdcd{{({x},{y})} \in {{A}^{{2}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 1fa999eab25ebfb7f69caf608dacd0faa4724522bf176de884702e54c99b0dfc \\
Pure Prop Address: & TMTdPZ59TT37q3Gv7R8XAXdt6EShALVC2bx \\
Theory Prop Id: & 234a4a6a1e3d22203eab3e75c58b409a92981de21f60b36b7bacdbe94c2f695e \\
Theory Prop Address: & TMEgxar8usGXDWMn2dQrfqcaTBMsQmobYQL
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_2_bij_2
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfcdpfcgjgkgpfcd} ${\unicdcdadad x y .  {{{x} \in {2}}\unicdbdjdcd{{{y} \in {2}}\unicdbdjdcd{{{x}\unicdcdgdad{y}}\unicdbdjdcd{{{{\mname{bij}}~{2}}~{2}}~{({\uniddcgcg i .  {{({x},{y})}~{i}}})}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 1458e4c76e00e5e5ab03f1e51a59e8b2db6f5aedb0ec7b7437f01c606e57f61c \\
Pure Prop Address: & TML944PLcXEhMqhaj1bSJ66jCqyeP9nidJV \\
Theory Prop Id: & 5fae0dbc2404ab825ce386605b9b51bc9aeac0b473aaf79cb2ca0d2802ca5c3d \\
Theory Prop Address: & TMTfcLL44Zqzsq91secQcUt9S5DKUtpL89s
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_3_eta
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfddpffgehbg} ${\unicdcdadad x y z .  {{({\uniddcgcg i \in {3} .  {{({x},{y},{z})}~{i}}})}={({x},{y},{z})}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 557b0ee79b2a52e8ce18d61ad94a7f15864471688ec9c794f1d5f24c9783005c \\
Pure Prop Address: & TMXagwe8TteWaGYj5KgUBttDC1wW28KphHN \\
Theory Prop Id: & b1962f9a855cfebb9323ea0e424ab44c88fc28f2f25e542d11602c8562b09544 \\
Theory Prop Address: & TMNJCyieXsgj2hu8gCm37y28P14rCCpCUyg
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_4_eta
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfedpffgehbg} ${\unicdcdadad x y z w .  {{({\uniddcgcg i \in {4} .  {{({x},{y},{z},{w})}~{i}}})}={({x},{y},{z},{w})}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 774296b519bf68aacdfe0445662dcdccfc6c74dcc7d3898d0507c5079d63d8f8 \\
Pure Prop Address: & TMQxXPgmA8bowKXArUpmiz87siaeSw2Q5MW \\
Theory Prop Id: & e04fd23dfc3d7c5f1a127aba4c6547e3b393dfb6545e480f9953e26ca3c3fc0d \\
Theory Prop Address: & TMYx47haX7KQ8PtiUHHnWXRWY2AfpDb5mNZ
\end{tabular}
\end{center}

\end{theorem}
\subsection{Tuples with More Than 2 Components}\label{effhahmgfgdh2}Let $ x0, x1, x2 : {\iota}$ be given.
\begin{verbatim}
tuple_3_0_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfddpfadpffgbh} ${{{({x0},{x1},{x2})}~{0}}={x0}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 2299dd127ed9d00d183b81051f52579a3638dd91f46ef778aa50c442abc6b092 \\
Pure Prop Address: & TMFhwi4ZC3VWuBy42eEzHkLCbNwo3Ev8HEf \\
Theory Prop Id: & 0a4f57728c3c5c761b448d44960ca6a828c0a440fd63d1aa6d9c2e57c0243787 \\
Theory Prop Address: & TMW5V1hAcqqC4skHEBzYR3ZiJGL8pvjwYWK
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_3_1_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfddpfbdpffgbh} ${{{({x0},{x1},{x2})}~{1}}={x1}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 414e8bd1880695006637be5415198e0c43b53e9609ce62bb325610bdc38977f9 \\
Pure Prop Address: & TMX5TRv8W5gSMK3DnrehU1GjFmEMuBgMie9 \\
Theory Prop Id: & 14ea6626db4405895dcefd0542273be1017929dc5a35662b5fc7930a86d2bb05 \\
Theory Prop Address: & TMNBfanXBAVa8NNCyyTX1KCDoX1oZugTZeK
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_3_2_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfddpfcdpffgbh} ${{{({x0},{x1},{x2})}~{2}}={x2}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 6b6b08fb7649ca4a49e5f256d73d38901cade1dbab78712081d4c92f5f63a44f \\
Pure Prop Address: & TMUzP7TDpQtCwif8aAwohSj3JNWVX6TEdjc \\
Theory Prop Id: & f69c06f91e4e8a435b4ac8fb4653343c5430c0f76186ed2c6b5a8285be49dd75 \\
Theory Prop Address: & TMQ7XSB36vKMD44joDM3WQNXQ5hqU7Zeu4r
\end{tabular}
\end{center}

\end{theorem}
Let $ x3 : {\iota}$ be given.
\begin{verbatim}
tuple_4_0_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfedpfadpffgbh} ${{{({x0},{x1},{x2},{x3})}~{0}}={x0}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a6e3de0ca7e59eaaf3122d630187610de4188d6b0275524d8b75d2bc27abda32 \\
Pure Prop Address: & TMF5etreB3YRde69S2FeY8M1oVAWjjxQ6v5 \\
Theory Prop Id: & fe5627737874494b543777e809941dce8d7e9a8013c7963f2809078137e82277 \\
Theory Prop Address: & TMYGbLVThnvCWxfpjrsDHdPixQYq8AwiQAz
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_4_1_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfedpfbdpffgbh} ${{{({x0},{x1},{x2},{x3})}~{1}}={x1}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 733dff0a1d011b3d6a42f3265c3727b7801c71ce1aae4ed97fa0c7086d2a3fc6 \\
Pure Prop Address: & TMSYE1DSLMRdPHth8BZAHKadTikLP9Hp1dN \\
Theory Prop Id: & bf73bc8d27290ee55ba023d0c035f7daaf4cf11c12a380d059c86f22816eb234 \\
Theory Prop Address: & TMX1ctd3QUcXQ7ntu5MvE9xqwY9fi3maxEg
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_4_2_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfedpfcdpffgbh} ${{{({x0},{x1},{x2},{x3})}~{2}}={x2}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & ed4aa73355586a09081629dab3b75a5dec8a417c17ed0d84b8443443fb2785a4 \\
Pure Prop Address: & TMExys3qMfkBQ43ojYUvQ8d1LY1vZw1enfP \\
Theory Prop Id: & 7d4422df851f3d7c9b2b10bc33820c35b9f3567e7a28a65da668a14c240d5d55 \\
Theory Prop Address: & TMNiHJsEoF9pvnK73fnpVv3rnvdPVJKtB7P
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_4_3_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfedpfddpffgbh} ${{{({x0},{x1},{x2},{x3})}~{3}}={x3}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 6a238391dd9d73ec2a175b97bcd4c846967958d9fb539afaec96724c51bf7e9f \\
Pure Prop Address: & TMTCp2qqDTin3jc37q6q6PLfMoJcCzaq48h \\
Theory Prop Id: & 1a82d64dd6e2e5694e2d044a818489902c8025fada8fb5f3561aa926882f5af2 \\
Theory Prop Address: & TMHfo157hjhQzHLRL8e3AAL7NmnK4YXNyFv
\end{tabular}
\end{center}

\end{theorem}
Let $ x4 : {\iota}$ be given.
\begin{verbatim}
tuple_5_0_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpffdpfadpffgbh} ${{{({x0},{x1},{x2},{x3},{x4})}~{0}}={x0}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f808b62bbfe0261c431302a1f9d628c853f68d912aa2f152472c2dfa90557d18 \\
Pure Prop Address: & TMGre8WKqnRD2NJPkoaA7jbLWUipgYm5jog \\
Theory Prop Id: & 2eb5ddc5a16b3a7d9a1280b24d3e509bd011ce52296873af2d6879fb547774ea \\
Theory Prop Address: & TMe1KWBCo857cwBq4Uy3dWDEAzMuSo7LxQm
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_5_1_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpffdpfbdpffgbh} ${{{({x0},{x1},{x2},{x3},{x4})}~{1}}={x1}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 5714821964a45eae8276b9e96c0d7f3dc70c4a421256104663fe4622cb6dda9d \\
Pure Prop Address: & TMQcHzma6cxkMaJgGHj1SX9kiVwhL66i5aW \\
Theory Prop Id: & 49b93f2b2cb80b89ed8e5dba6af36b0110694d89f4106c7b23eb3abdee76c4f2 \\
Theory Prop Address: & TMachUcuahLvMtFu7FZn7cYP4oDkK8ciBkE
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_5_2_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpffdpfcdpffgbh} ${{{({x0},{x1},{x2},{x3},{x4})}~{2}}={x2}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & cfa53ec600e79400f6f667fa9b058c813cc71e4bebcbef4760d5e26acfb75b75 \\
Pure Prop Address: & TMFYhqnKU46a4x3LZyhSt4RajqBX6cEKbFx \\
Theory Prop Id: & 3bb23a1a7686e9d933ead58faf0abbc08a769032e8988fd111a8d08413d02d1f \\
Theory Prop Address: & TMWnPwZQBGvW4pee3GLW8LkfkhmmfRtVKmF
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_5_3_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpffdpfddpffgbh} ${{{({x0},{x1},{x2},{x3},{x4})}~{3}}={x3}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 1b1587958694c5a5e88c0848a23a4e473c235eefdc4ef28de59de0e840fdd536 \\
Pure Prop Address: & TMaXA4j4fzMqVPAEs32Lkx3LxUCXkwLbpMV \\
Theory Prop Id: & 527729cf29653b87109e805ea351973493674baa2ed19682f7fbb67c753e4707 \\
Theory Prop Address: & TMHJVjGa5dY6E8B16YUobHUQV7gxBZGTtkQ
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_5_4_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpffdpfedpffgbh} ${{{({x0},{x1},{x2},{x3},{x4})}~{4}}={x4}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 4b873a60b686c40372a054db2e8bc63d7af0fe67ef2f26f88f9a9279bb14648f \\
Pure Prop Address: & TMQuKuBaYQaVUjVyxJUQ247CUXS7YEvahrM \\
Theory Prop Id: & 39fb6373be9c1ed3946575a5f4f3666171d7e8bfe812b3f8d57f6a9a6c5dafec \\
Theory Prop Address: & TMG8m35MwfUjvACH7KLAnZSxxnizHeeC6py
\end{tabular}
\end{center}

\end{theorem}
Let $ x5 : {\iota}$ be given.
\begin{verbatim}
tuple_6_0_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfgdpfadpffgbh} ${{{({x0},{x1},{x2},{x3},{x4},{x5})}~{0}}={x0}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 09a916f7cab6d7d54eeebdf48131510af7e2286ceae22ad4b167cef732ec5024 \\
Pure Prop Address: & TMHkcrA1nz7EC1iKBwwwMHDsTRdph4WGCMe \\
Theory Prop Id: & 431823a5e23f06055a6b8d3de1cd5baaf82ffaca75dc198d13b368e15c356496 \\
Theory Prop Address: & TMZfq1XThKjcGE26mvQn13MnXXuNnXLjT91
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_6_1_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfgdpfbdpffgbh} ${{{({x0},{x1},{x2},{x3},{x4},{x5})}~{1}}={x1}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 29da6a2f4d3d0147e6f18d6c08aac5b7c54b66d6227fec45e9b37962c74efd62 \\
Pure Prop Address: & TMLK9MjtbDbJHdSXq3UFqNrBCpsMatyNCUJ \\
Theory Prop Id: & 649eac8b3e9c6e791fc56cac42ca9787ec30ec00c1f8ecc5b68831e978a459c8 \\
Theory Prop Address: & TMcCvMHVhFKscbxwpj6BsdrkD4ne1ELkvgn
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_6_2_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfgdpfcdpffgbh} ${{{({x0},{x1},{x2},{x3},{x4},{x5})}~{2}}={x2}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 8dde2d93ac41664c4b1687e280531801c7c9b7502d9ef12722abd166d16050e0 \\
Pure Prop Address: & TMaHcLc1izgmwaWPEBG57z2qAT17g26H4L7 \\
Theory Prop Id: & f750917ac06e451a6eecda8fca53336730cd931fdf493afb63413e3fe3aea0f9 \\
Theory Prop Address: & TMUHUCWa6x5Cs3iENyWQFdVm4DWTTXfjXKk
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_6_3_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfgdpfddpffgbh} ${{{({x0},{x1},{x2},{x3},{x4},{x5})}~{3}}={x3}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a5391e373cc4ee39be40eb3722e01b208d2935f48e4a422581e36b530e106751 \\
Pure Prop Address: & TMWnuyCP9Xhcj8WXFvvmExAgQv5q8FLMf87 \\
Theory Prop Id: & 9c6fc47f25c0dfa31aaf9660010b55a370cf936d297c0550428e6361c3846acb \\
Theory Prop Address: & TMR4FTBgD9zS7EN9XzWafwrqhmFsUjwH57g
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_6_4_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfgdpfedpffgbh} ${{{({x0},{x1},{x2},{x3},{x4},{x5})}~{4}}={x4}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 454d77053132c71f1d965c99fa38da3d894908d33f7b7e16eaf6821ccc7266f8 \\
Pure Prop Address: & TMS87PUFZMv9WtLqYWCHZds6nUvxfnbUYRh \\
Theory Prop Id: & 59ae63f950d447046bb6bae0eeeed28c4a7cf3348434b3fe2b85ed366aaccc5a \\
Theory Prop Address: & TMYgmDm3q8F4Mm3PxvLRJqjhm53p6v4SckS
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_6_5_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfgdpffdpffgbh} ${{{({x0},{x1},{x2},{x3},{x4},{x5})}~{5}}={x5}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & e53f7e86153a20747dc21bbf79ab7de024febeef898b88b7ca1b8a25f1dbe489 \\
Pure Prop Address: & TMdTTWmw4pKJNhk1pcAsNTBNcpR4rYNZdWx \\
Theory Prop Id: & 3948d3857fe77f9ea2e9fa5db183819280b873fc0ff58efec01627914174b604 \\
Theory Prop Address: & TMcBoE6Vfa7iKDQFescgG8sF1w6NkoWVsRP
\end{tabular}
\end{center}

\end{theorem}
Let $ x6 : {\iota}$ be given.
\begin{verbatim}
tuple_7_0_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfhdpfadpffgbh} ${{{({x0},{x1},{x2},{x3},{x4},{x5},{x6})}~{0}}={x0}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 2e6014a9fce0b27e920adaf5d4ce5cd70132df4f7186fe3ee541fbb88d55e5ff \\
Pure Prop Address: & TMSw7zxqpUofUXu1iw13sy9eGNZFkJ83G8m \\
Theory Prop Id: & 1dd20a0f28040bbf9f665874e170b2a7507504613edf15bfdaeccac483fe8d57 \\
Theory Prop Address: & TMFmBTCrMA6APNwYVkmVE5BR4uSANNxuCnr
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_7_1_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfhdpfbdpffgbh} ${{{({x0},{x1},{x2},{x3},{x4},{x5},{x6})}~{1}}={x1}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 50757afcd46384f164088eecd0890ea20e41d6faabc75520acbbcbc8caded1f9 \\
Pure Prop Address: & TMGz5g964HWbsbR8EdvqGJX38rYAsa8B6A4 \\
Theory Prop Id: & df1371c7546e44515aa1062d1787c0276481ea613ed0b0c96d52df80ee45960b \\
Theory Prop Address: & TMJrw6pMykGM46pQg8E3npd2RCSbU1sxJdZ
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_7_2_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfhdpfcdpffgbh} ${{{({x0},{x1},{x2},{x3},{x4},{x5},{x6})}~{2}}={x2}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 42d292c18db7c0a80c38bd4ad63c9931011a99c7f28f1d3f98fc7be5ba02f6fa \\
Pure Prop Address: & TMaDjeg9UWvnEZBxqcyDSjZqA9PdDXB6FdL \\
Theory Prop Id: & f1f4ec953eb39d38b739d1cb8eb86ec8cb64944b9e496c426a73c3e9e8247f1e \\
Theory Prop Address: & TMQmpwNMGPPbdwGTDnpPL4Bofnunn3sUWup
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_7_3_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfhdpfddpffgbh} ${{{({x0},{x1},{x2},{x3},{x4},{x5},{x6})}~{3}}={x3}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 9bf8cc6fcb3bbff2fb13bd77a32b81fc0c78e82ac38fba8ecf898116272a76c6 \\
Pure Prop Address: & TMUya4w7djLwbukHFDyKwD1eFvHneTmmPTn \\
Theory Prop Id: & 0ee6c00d403225b610cf3cbdcb67fe69f1b99a36ed115272a676b3ff5895ea20 \\
Theory Prop Address: & TMJdFNXdzogDAxgPCDUbrEfUH5qS2fodYvz
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_7_4_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfhdpfedpffgbh} ${{{({x0},{x1},{x2},{x3},{x4},{x5},{x6})}~{4}}={x4}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 8462f55255364b442133232a99948ac976e6a6fb1fcad9753fd37e423292b072 \\
Pure Prop Address: & TMbPipbzrrjCW5jfNhEUnUim1TDD5mFRKh2 \\
Theory Prop Id: & a1e2a4c78071f6df819ba47d9b0dfd266b20490f5cfd23e24c39c68d7733ab6c \\
Theory Prop Address: & TMSvveckTP4ZbhKhqsjNNf6HyqQpZtmtqeN
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_7_5_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfhdpffdpffgbh} ${{{({x0},{x1},{x2},{x3},{x4},{x5},{x6})}~{5}}={x5}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d72f29ba20ccd83f14385aee069bd57c87c90fff8d2a86cf9c56d81df57ccf7a \\
Pure Prop Address: & TMYnZE8WXPd7Lz6nNYaNwd53r9FLYVqbHot \\
Theory Prop Id: & b3bff055493211cb1eaee1162d67c798ed21ac3305b1e4f92aea7ef0a84f21a3 \\
Theory Prop Address: & TMGq56172uFcBvMUViudP5XBkrjMQZDLoWW
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_7_6_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfhdpfgdpffgbh} ${{{({x0},{x1},{x2},{x3},{x4},{x5},{x6})}~{6}}={x6}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 6a6e0703f1e5cdb6bb4cdfe2feaf16914b1e19e04acbf2ec6f83392a9ba32159 \\
Pure Prop Address: & TMRnWwZbYhS2xiXxEBDwKjrHtL82AeLyj3v \\
Theory Prop Id: & 3fd34b4049502dd532ee544c178b866077b61510f73540a979b4cb630631a075 \\
Theory Prop Address: & TMUYHfZMdobjQfNUAjkyHkmaeYViwqtCndh
\end{tabular}
\end{center}

\end{theorem}
Let $ x7 : {\iota}$ be given.
\begin{verbatim}
tuple_8_0_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfidpfadpffgbh} ${{{({x0},{x1},{x2},{x3},{x4},{x5},{x6},{x7})}~{0}}={x0}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 4d531e28345c633c2002654dcc743a093af9ee8b7f68ff77c4f7267261a19d71 \\
Pure Prop Address: & TMckKDatqdQwJzLKWCavwMR6tjSPWLVCMWD \\
Theory Prop Id: & 1b9fca46dbafdb59c9e774e473a1cbe61e9e6f78e7eaf15a1d24c3f6c61b8b52 \\
Theory Prop Address: & TMSNRtL24tamygfhPna4TbgXg6e1xm7U4SF
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_8_1_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfidpfbdpffgbh} ${{{({x0},{x1},{x2},{x3},{x4},{x5},{x6},{x7})}~{1}}={x1}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a89a9e6dadd13a5330864d0051afdedff37a8d6c55b3991826097d7fd9e2a431 \\
Pure Prop Address: & TMcfnBEJnMxoVVovoBVi4dwC2PvUfkqu3eZ \\
Theory Prop Id: & fafd80409a2da6a08db5bda00f3225829870d378adfb385c57fde0e89b0b986e \\
Theory Prop Address: & TMPoe6wCmvUNubyq1MbpHDtwHtVKon77Awk
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_8_2_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfidpfcdpffgbh} ${{{({x0},{x1},{x2},{x3},{x4},{x5},{x6},{x7})}~{2}}={x2}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 49e82c53acd392cd8e7fdd61b280cc3953c508ee664a1617ecdc5a378d0dbc31 \\
Pure Prop Address: & TMduvfU8rksxh1TRJ5nqEAuDZZfnJ7orBPX \\
Theory Prop Id: & c4f8325d16f1f37c6c1b8f3611beacf3e5027e0b4a964af75dd596b2fd3f3964 \\
Theory Prop Address: & TMYtGYjHksBMoXSBuCV2L7EZPAK41CBNa5B
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_8_3_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfidpfddpffgbh} ${{{({x0},{x1},{x2},{x3},{x4},{x5},{x6},{x7})}~{3}}={x3}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 165a4eea8749fd9e02498a1ebda5ee12fe020e0fd7c18820b62a240cee4313ed \\
Pure Prop Address: & TMVio5C24nLLNCMHHwF2Hj74cLzmmxeD1Vf \\
Theory Prop Id: & 813d2d46172e67e30343892ae6f61699148d68c69c7af2ea5359c272e75dc1f6 \\
Theory Prop Address: & TMYr323e2X9sRx49CLZrkYn4vV85NQRyoRT
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_8_4_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfidpfedpffgbh} ${{{({x0},{x1},{x2},{x3},{x4},{x5},{x6},{x7})}~{4}}={x4}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 4e1b495a5072ad1d3b879ed62eff2c100fb8f975c0ad2a6f54d301c81de26c44 \\
Pure Prop Address: & TMY5bJDeHJshTEqZj17jxPqa8JntKZiRsCe \\
Theory Prop Id: & 4437b79893da40005550d241d6c12c7063f25afb64d237b52b0242a035218898 \\
Theory Prop Address: & TMMVNvpvjzLdjgRF292vzfCgLN1tRcuXph8
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_8_5_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfidpffdpffgbh} ${{{({x0},{x1},{x2},{x3},{x4},{x5},{x6},{x7})}~{5}}={x5}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 563677657a81d01f8e8dd06ec4032e620ce92956af773ea886d10e8a18a0e37e \\
Pure Prop Address: & TMP7vfkqYAkgGnygvPp1DhbmEUEpX2vcTC7 \\
Theory Prop Id: & 5078953fb1b78cf7ee83f76004c34c338e15e1b22a251c44b4c22a7e75b3e49d \\
Theory Prop Address: & TMK3bws6NYHpsM12NM3kXJordSrkVZiwXdS
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_8_6_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfidpfgdpffgbh} ${{{({x0},{x1},{x2},{x3},{x4},{x5},{x6},{x7})}~{6}}={x6}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 8a30e81feba75452c73351f490aecb9e61529a2fb4beee2aea3f106abbec6783 \\
Pure Prop Address: & TMGVN5oXmWa1ZAx5JDJzTAxZNkAPUL18MWj \\
Theory Prop Id: & 2e35ad0124fc4b59017241f14ed8cadd718350ce99b31f1f8010bd4433d2fc10 \\
Theory Prop Address: & TMVH2QvTzDv8bXohG5W1at4o2xEqMR3wTiN
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_8_7_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfidpfhdpffgbh} ${{{({x0},{x1},{x2},{x3},{x4},{x5},{x6},{x7})}~{7}}={x7}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 57dbf4f7ff71f1e9c347c26193ffe394feb41601e047c06c67f8288012465ab2 \\
Pure Prop Address: & TMULadmzcV4DX8JBCi7ogRsVnsU97NMsnBA \\
Theory Prop Id: & 96777da9be70f7524c8eb35e7801fe9f0e20108d7bd0be0f5dc289bb821dc659 \\
Theory Prop Address: & TMcoMGrJAhGkKy8Louj6kpH3a7yNkTuMNYw
\end{tabular}
\end{center}

\end{theorem}
Let $ x8 : {\iota}$ be given.
\begin{verbatim}
tuple_9_0_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfjdpfadpffgbh} ${{{({x0},{x1},{x2},{x3},{x4},{x5},{x6},{x7},{x8})}~{0}}={x0}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 26d3d48c9c93b7ec957763149ffa832050df3100f14d665f9a1c7a61f59e9925 \\
Pure Prop Address: & TMJMTn7StT21vzeC8qwYcWigwJ4kq5aY9oo \\
Theory Prop Id: & 29c132099b2f6c53ca2f04ce3ca16cc8de2ea951e11fb4ac5dbd7fc184921f8c \\
Theory Prop Address: & TMXgk5r2Wc1ku9pdXFHc89zP32xZ8hwx4kt
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_9_1_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfjdpfbdpffgbh} ${{{({x0},{x1},{x2},{x3},{x4},{x5},{x6},{x7},{x8})}~{1}}={x1}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 3a3c1cb789c9f600657400101f3562fb437f82776a00c2a32c686549a63f8e42 \\
Pure Prop Address: & TMHkZbR5acwXro73RegaXWPvpdK2cEUGU44 \\
Theory Prop Id: & 6919b89ef581bce0dccbc7b8e0d02d831b4094ed9862095c50cb82f7fce1f138 \\
Theory Prop Address: & TMQE3e1rPeJMLKx8ndXckY8TL8GUjATgfDx
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_9_2_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfjdpfcdpffgbh} ${{{({x0},{x1},{x2},{x3},{x4},{x5},{x6},{x7},{x8})}~{2}}={x2}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 62a1ca05201c6214162f1b3abb7aac30f56939908278fa886379a9d4b8b82e80 \\
Pure Prop Address: & TMR3ZPXHQu2ywtSwNsvBLZjBq5B3bXZt1gr \\
Theory Prop Id: & cbc94460959b856131086866189279bf769c522b562c6627b9f28426cbd337d6 \\
Theory Prop Address: & TMcHUnvscx8DjAsJLn8qhtXg6wp1Uwae864
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_9_3_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfjdpfddpffgbh} ${{{({x0},{x1},{x2},{x3},{x4},{x5},{x6},{x7},{x8})}~{3}}={x3}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & ff32780d6432c453f8f483ee108e60697671b297f3692720ed857d111dfb71ff \\
Pure Prop Address: & TMM8Wc2najKFrxPLc9rLMDHAPijUVkEZqgE \\
Theory Prop Id: & 1c8999f1f6c222289e7f742f2e89913886228a37f06d003c45a34a2f39454710 \\
Theory Prop Address: & TMPrj3JT9vGnAt3EdTZh4hNCBJWF9jSUnCc
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_9_4_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfjdpfedpffgbh} ${{{({x0},{x1},{x2},{x3},{x4},{x5},{x6},{x7},{x8})}~{4}}={x4}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a6eff8bb384773eb50520928a17869c5a362f5a8aad62aefdbc76289e9a6d79f \\
Pure Prop Address: & TMVD2U7o4KhyJ5vRSXBuCtRYNqiDUPGGdvV \\
Theory Prop Id: & a8ebb556022b919699ce1585f44fe5382a8f90cbfb906757e003fee89ef48dc3 \\
Theory Prop Address: & TMYBL14qJDzq5tT7Kafcbuu2kZuud4Kxisj
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_9_5_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfjdpffdpffgbh} ${{{({x0},{x1},{x2},{x3},{x4},{x5},{x6},{x7},{x8})}~{5}}={x5}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & c78a9b1e8f5a59a13fac52e14833a96eaca2cfa10c50958e33b15229b119fe88 \\
Pure Prop Address: & TMZwGSJLxkX6PKAVCtFGmZZJrSr2BqfJGTX \\
Theory Prop Id: & d77f4e4c53456c2e683d10d9701b4877455bca6113ce67c8044a027158f9bda4 \\
Theory Prop Address: & TMYxcJb6i94M3w3oNmuZV5FueX4QnERLxfS
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_9_6_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfjdpfgdpffgbh} ${{{({x0},{x1},{x2},{x3},{x4},{x5},{x6},{x7},{x8})}~{6}}={x6}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 6e88afe0e1aee7023c9f258a6001f4b275581eec0fa26c41b702c8ca1ff82aac \\
Pure Prop Address: & TMWrYTvycmEwE7477Npqu6z4QaWkaJsxrK1 \\
Theory Prop Id: & 14cf05c1356df0137d6e6227fa3cf268b8268ba41d288eb04289088d348ca7fc \\
Theory Prop Address: & TMbPUqUn32XqEuCscjPeu2f4QjNwqVJq1Vv
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_9_7_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfjdpfhdpffgbh} ${{{({x0},{x1},{x2},{x3},{x4},{x5},{x6},{x7},{x8})}~{7}}={x7}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 810f4de4b017dc83221bcc8ff7116206998e3957bec3786295c9a0429ce531eb \\
Pure Prop Address: & TMdA5ixqphhBmefBSSzHsamLt8GAzvT9yfo \\
Theory Prop Id: & 6cad9319962321f56f773887d81f42aa4ad5b8eedcdcf7236252cca9d9f647ea \\
Theory Prop Address: & TMbt5vtmatV53yku7m11vPWF23UU2d79D6y
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_9_8_eq
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfjdpfidpffgbh} ${{{({x0},{x1},{x2},{x3},{x4},{x5},{x6},{x7},{x8})}~{8}}={x8}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 8486de1f45eebeac976e64b40817e81d801358e1aa3eb4db3f60660662253a51 \\
Pure Prop Address: & TMbcVQrFnbaUtBNZg7rEVeHjsbRYhwsse9z \\
Theory Prop Id: & 011a8763916b9f748447c0172bb5ffdb73d7eda2528b2a21e183952258975e18 \\
Theory Prop Address: & TMNGCEjuYZhPiHizVLu725KogvvA3BCGiiK
\end{tabular}
\end{center}

\end{theorem}
\section{Notation for Sums and Products} % pair_setsum
{\bf{Notation.}} We use $\binddfjghgngbgpf x,\ldots,y  . $ as a binder notation corresponding to a term constructed using ${\mname{Sigma}}$.
We use $\infkdkckd$ as a left associative infix operator  corresponding to applying term ${\mname{setprod}}$.
We use $\bindafjgpf x,\ldots,y  . $ as a binder notation corresponding to a term constructed using ${\mname{Pi}}$.
We use superscripts as notation for applying the term ${\mname{setexp}}$.

\begin{verbatim}
tuple_3_in_A_3
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfddpfjgogpfbepfdd} ${\unicdcdadad x y z A .  {{{x} \in {A}}\unicdbdjdcd{{{y} \in {A}}\unicdbdjdcd{{{z} \in {A}}\unicdbdjdcd{{({x},{y},{z})} \in {{A}^{{3}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & b6cd63778e5c307591e09f0dbe6709f3e2a0a25002362cc8bc25c497de01c8af \\
Pure Prop Address: & TMJv4GJ6yA6E4zrTys8Fvo4pAxneFHykrEo \\
Theory Prop Id: & 039f9b74048094fcf8f6a563d8ade3c5c8fae05574e684d2f7a1119e2bb00978 \\
Theory Prop Address: & TMcqM5egc3mW237ChXvW4EschnVxw2CaHsw
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_3_bij_3
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfddpfcgjgkgpfdd}
  $$
  \begin{array}{c}
    \unicdcdadad x y z .  {{x} \in {3}}\unicdbdjdcd{{y} \in {3}}\unicdbdjdcd{{z} \in {3}}\unicdbdjdcd{{x}\unicdcdgdad{y}}\unicdbdjdcd{{x}\unicdcdgdad{z}}\unicdbdjdcd{{y}\unicdcdgdad{z}}\unicdbdjdcd\\
                 {{{{\mname{bij}}~{3}}~{3}}~{({\uniddcgcg i .  {{({x},{y},{z})}~{i}}})}}.
  \end{array}
  $$
  The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 8fc73d4725ec781165c998d0b4398e6ba4fcf725b30d828af8a3419c83437f62 \\
Pure Prop Address: & TMHDdHVHUS4jN4k7phZYZXRAa2d6TcLAbNa \\
Theory Prop Id: & 921a459779265cfc541794e752d792d1a82c2eaf3b4d1acdafdd92cbf66dab3e \\
Theory Prop Address: & TMXTMvgV3GghUjq7QBj1XncxXwtTjahmJVW
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_4_in_A_4
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfedpfjgogpfbepfed} $${\unicdcdadad x y z w A .  {{{x} \in {A}}\unicdbdjdcd{{{y} \in {A}}\unicdbdjdcd{{{z} \in {A}}\unicdbdjdcd{{{w} \in {A}}\unicdbdjdcd{{({x},{y},{z},{w})} \in {{A}^{{4}}}}}}}}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 9dfa39b843ce4aacc1ee090d1483a1708c5dc6df066ae816e7a9ecee8013a642 \\
Pure Prop Address: & TMUtkQ3zWCfss9WPT6D8cb1egDHRfo1MVkn \\
Theory Prop Id: & c23e38f69ea81031bbd8a5d922a52882ec9ad56393a4fac4d35a44bfa890dd02 \\
Theory Prop Address: & TMPzwDRXgLuZdfX4s8JwnPpH2jBU25hsWEm
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
tuple_4_bij_4
\end{verbatim}
\begin{theorem}\label{thm:ehfhahmgfgpfedpfcgjgkgpfed}
  $$
  \begin{array}{c}
    \unicdcdadad x y z w .  {{x} \in {4}}\unicdbdjdcd{{y} \in {4}}\unicdbdjdcd{{z} \in {4}}\unicdbdjdcd{{w} \in {4}}\unicdbdjdcd\\
                 {{x}\unicdcdgdad{y}}\unicdbdjdcd{{x}\unicdcdgdad{z}}\unicdbdjdcd{{x}\unicdcdgdad{w}}\unicdbdjdcd{{y}\unicdcdgdad{z}}\unicdbdjdcd{{y}\unicdcdgdad{w}}\unicdbdjdcd{{z}\unicdcdgdad{w}}\unicdbdjdcd\\
                          {{{{\mname{bij}}~{4}}~{4}}~{({\uniddcgcg i .  {{({x},{y},{z},{w})}~{i}}})}}.
  \end{array}
  $$
  The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 8d7a7d5ba57f64b10810f6a1009fb528d3588de74399da873640c14afb5cf725 \\
Pure Prop Address: & TMXDjtm9zxy9LdmBcvD1u1oaVds6NRkYyfJ \\
Theory Prop Id: & d8db975b63b69912e055c4b2c24308cac5831ad7491c3f8bea7b38fe6767e7bc \\
Theory Prop Address: & TMdGBeJemPTJ6p1TyGocFh5ejMH1SY1thm4
\end{tabular}
\end{center}

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

\end{theorem}
\begin{verbatim}
iff_sym
\end{verbatim}
\begin{theorem}\label{thm:jgggggpfdhjhng} ${\unicdcdadad A B : {o} .  {{({{A}\unicdbdjded{B}})}\unicdbdjdcd{({{B}\unicdbdjded{A}})}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 00bac1cbdb77d159cd3e6b357772b77cfbf5fd08ad17791fd058a31c0475a3f6 \\
Pure Prop Address: & TMWtfJhtiuKuNHV2k6qcVXL3USFSvbCNETm \\
Theory Prop Id: & 11f51b14cc9177b5bc57ce79c943b2dcdfe3d83f93b1a6336d2174ba4e9df0b7 \\
Theory Prop Address: & TMEgLJHQtw8TKqiFHfyA8RQk6wHyjMKHyrr
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
iff_trans
\end{verbatim}
\begin{theorem}\label{thm:jgggggpfehchbgogdh} ${\unicdcdadad A B C : {o} .  {{({{A}\unicdbdjded{B}})}\unicdbdjdcd{{({{B}\unicdbdjded{C}})}\unicdbdjdcd{({{A}\unicdbdjded{C}})}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 363285ef27e2778afb838fe5fa3dd62807d7a90305f7def9e4fde9ad6aee1383 \\
Pure Prop Address: & TMZye8CSrfjLgw85BDLDes4EZvTCzY9U9wh \\
Theory Prop Id: & c3b8f10058ec7ec17c37e487120493fd766e40d5ebea182f66ee1a52c306ddac \\
Theory Prop Address: & TMGt6JXemXxv9o18nreYuNrNEaPaXkqRn3V
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
not_or_and_demorgan
\end{verbatim}
\begin{theorem}\label{thm:ogpgehpfpgchpfbgogegpfegfgngpgchhgbgog} ${\unicdcdadad A B : {o} .  {{\preoh{{({{A}\unicdcdcdid{B}})}}}\unicdbdjdcd{{\preoh{{A}}}\unicdcdcdhd{\preoh{{B}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 8733b0a9ab0e00cdbd3a98177e398aa4cdb186d6fc7dc3377ad202c7a9841879 \\
Pure Prop Address: & TMRcU714fZk34v4xKvog8EUFH1iBy9go9dP \\
Theory Prop Id: & 27db911b3442575d6174ef608b04eba2264a9ff43956cb9f48038590759a688b \\
Theory Prop Address: & TMVWiPV5LBpzWhx13DG3yh1p7aPM8pSt1F5
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
and_not_or_demorgan
\end{verbatim}
\begin{theorem}\label{thm:bgogegpfogpgehpfpgchpfegfgngpgchhgbgog} ${\unicdcdadad A B : {o} .  {{{\preoh{{A}}}\unicdcdcdhd{\preoh{{B}}}}\unicdbdjdcd{\preoh{{({{A}\unicdcdcdid{B}})}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d4efd56c095b9a01570df661ec52e9fc1d3acf99dbb90a82e8047f781b21c525 \\
Pure Prop Address: & TMKRSDh9GPJPyX9ZtDqiV2KvjiUnNipaWCc \\
Theory Prop Id: & 1b5ff58044cbc333c55074f5e5983bf4a0ac161bc254b95d032435918a88edba \\
Theory Prop Address: & TMZ7VzgbGyQBuJB8KTDGonc6PtcMRxd2VSQ
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
not_ex_all_demorgan_i
\end{verbatim}
\begin{theorem}\label{thm:ogpgehpffgihpfbgmgmgpfegfgngpgchhgbgogpfjg} ${\unicdcdadad P : {{\iota}\unicdbdjdcd{o}} .  {{({\preoh{{\unicdcdaddd x .  {{P}~{x}}}}})}\unicdbdjdcd{\unicdcdadad x .  {\preoh{{{P}~{x}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 73523ea5da5dea92107627d5a291d82f8297690e14be35d05c010105c296529b \\
Pure Prop Address: & TMMTCJ7GAVwzZ3Kw9d5Cbo8nEoqaWP6dBZs \\
Theory Prop Id: & 075ddf1e62156846e54afd9c4c7a78cb61fa7d76482304fb50d121bd59d57fd5 \\
Theory Prop Address: & TMNGgYHHcc31AsZAqJEYPmSY4HMBaLLKAHS
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
not_all_ex_demorgan_i
\end{verbatim}
\begin{theorem}\label{thm:ogpgehpfbgmgmgpffgihpfegfgngpgchhgbgogpfjg} ${\unicdcdadad P : {{\iota}\unicdbdjdcd{o}} .  {{\preoh{{({\unicdcdadad x .  {{P}~{x}}})}}}\unicdbdjdcd{\unicdcdaddd x .  {\preoh{{{P}~{x}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 9bfa06e2e338dc6635e2549a3e17611c80217077a8b944a0478de74cd035b7e7 \\
Pure Prop Address: & TMdvAZELU6wRxcmyDehPqHUGeECff7oXd9k \\
Theory Prop Id: & 4b147405ce7450475ec000fd6756e31ec6f80a467321e8614a031eb4efa82ae9 \\
Theory Prop Address: & TMReccPGDm1kZKJBaUcrWSWSEbaxPa45Qos
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
eq_or_nand
\end{verbatim}
\begin{theorem}\label{thm:fgbhpfpgchpfogbgogeg} ${{\mname{or}}={({\uniddcgcg x y : {o} .  {\preoh{{({{\preoh{{x}}}\unicdcdcdhd{\preoh{{y}}}})}}}})}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 24ac29991a11e5ff752e6de9a587fd6a214a662220d9d009904454a69ff0f25a \\
Pure Prop Address: & TMaWRCFfz4Q1tpK7DeCGe2qubLQxDVTPHUN \\
Theory Prop Id: & d212ef38daafdab7978d40905362a79d7c00ead847e06d6f47e2921708ce316e \\
Theory Prop Address: & TMd6MEzYCjYvnk16kTfPmz5gduojxUSzocf
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:feahdhcfpfjgpfjgpfbd}
$\mname{EpsR\_i\_i\_1}$ is the opaque object of type ${{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}})}\unicdbdjdcd{\iota}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 20c61c861cf1a0ec40aa6c975b43cd41a1479be2503a10765e97a8492374fbb0 \\
Pure Object Address: & TMdTiwgMp6N6HYyfybe9XUGgVm2baQ7rg6M \\
Theory Object Id: & aced991b30f594da8af7187f84a33d664ee2260df28fd11d86b6d8b6281bc768 \\
Theory Object Address: & TMUkEyWxAV2ZVYdDpQxADf9KP7MV4bVGB3m
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:feahdhcfpfjgpfjgpfcd}
$\mname{EpsR\_i\_i\_2}$ is the opaque object of type ${{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}})}\unicdbdjdcd{\iota}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & eced574473e7bc0629a71e0b88779fd6c752d24e0ef24f1e40d37c12fedf400a \\
Pure Object Address: & TMFeweZzkVerYMn5MZFuEXjq9udK79AoNif \\
Theory Object Id: & 9087d981ba2801ae343ebf3a94c2e492b130dcee92d602d81eb4fa743b836009 \\
Theory Object Address: & TMG4jTkPFvT4pZQYm7XyoTAQ2rCoJWUGyE8
\end{tabular}
\end{center}

\end{definition}
\begin{verbatim}
EpsR_i_i_12
\end{verbatim}
\begin{theorem}\label{thm:feahdhcfpfjgpfjgpfbdcd} $${\unicdcdadad R : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  {{({\unicdcdaddd x y .  {{{R}~{x}}~{y}}})}\unicdbdjdcd{{{R}~{({{\mname{EpsR\_i\_i\_1}}~{R}})}}~{({{\mname{EpsR\_i\_i\_2}}~{R}})}}}}.$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 95a215a34ac047e6487e5f941e77b1193b239ef381850705e74d3f067c0bd706 \\
Pure Prop Address: & TMHei6pp5iZeH81iwXzRtjmAKAWBcbScwk3 \\
Theory Prop Id: & 444c78c63c5fa77e04db6105dd5977e47fec752e9fdc8aa48314397572063a6d \\
Theory Prop Address: & TMM2ecoMZfXHpCELLyzJSaxKGa3nTPfMSpY
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:eefgdhdgchcfpfjgpfjgpgpfbd}
  $\mname{DescrR\_i\_io\_1}$ is the opaque object of type
  $${{({{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{o}})}\unicdbdjdcd{o}}})}\unicdbdjdcd{\iota}}$$
  identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 1d3fd4a14ef05bd43f5c147d7966cf05fd2fed808eea94f56380454b9a6044b2 \\
Pure Object Address: & TMYtxWX7Bmit31XQaJHqNRjz54fNehWemQx \\
Theory Object Id: & 82aeccfa6a8d109c25ec362683dff6b3c19f69eb033bc53476eebc1307c2f73a \\
Theory Object Address: & TMG2AhxUeoPURmtyqa7z6V67bTzk9kjG2Gb
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:eefgdhdgchcfpfjgpfjgpgpfcd}
  $\mname{DescrR\_i\_io\_2}$ is the opaque object of type
  $${{({{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{o}})}\unicdbdjdcd{o}}})}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}}$$
  identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 768eb2ad186988375e6055394e36e90c81323954b8a44eb08816fb7a84db2272 \\
Pure Object Address: & TMQ5YqiemA8Nk8YhMLn6FVrHVdoZLZYhFMU \\
Theory Object Id: & 3f82bc7f6e996e5dd88799a9921cab56f8d25ed0bcfad1f9f0e2b2a2968fcab4 \\
Theory Object Address: & TMSA1F1Xty3y6u3fgqcMyVysuyvX9HKs1vN
\end{tabular}
\end{center}

\end{definition}
\begin{verbatim}
DescrR_i_io_12
\end{verbatim}
\begin{theorem}\label{thm:eefgdhdgchcfpfjgpfjgpgpfbdcd}
  $$
  \begin{array}{c}
    \unicdcdadad R : {{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{o}})}\unicdbdjdcd{o}}} .\\
                 {({\unicdcdaddd x .  {{({\unicdcdaddd y : {{\iota}\unicdbdjdcd{o}} .  {{{R}~{x}}~{y}}})}\unicdcdcdhd{({\unicdcdadad y z : {{\iota}\unicdbdjdcd{o}} .  {{{{R}~{x}}~{y}}\unicdbdjdcd{{{{R}~{x}}~{z}}\unicdbdjdcd{{y}={z}}}}})}}})}\unicdbdjdcd\\
                 {{{R}~{({{\mname{DescrR\_i\_io\_1}}~{R}})}}~{({{\mname{DescrR\_i\_io\_2}}~{R}})}}.
  \end{array}
  $$
  The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a4fae2546427685ef36418f88478e6af3ac2e79bb359fbb0c2ffab0ae113217f \\
Pure Prop Address: & TMXTFXfZpFuoocq9aqaPeoZwN93KkV2Yp2R \\
Theory Prop Id: & da4f023fa8a6db67051918ac52618aa28cd3cd54056987f781a8085ae23273a1 \\
Theory Prop Address: & TMZVTm3MugdHj2HeAWLwWA24D1RpC1Kq1TU
\end{tabular}
\end{center}

\end{theorem}
