\chapter{Description and If-then-else}
\section{Descr\_ii}\label{eefgdhdgchpfjgjg}Let $ P : {{({{\iota}\unicdbdjdcd{\iota}})}\unicdbdjdcd{o}}$ be given.
\begin{definition}\label{def:eefgdhdgchpfjgjg}
$\mname{Descr\_ii}$ is the opaque object of type ${{\iota}\unicdbdjdcd{\iota}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 3bae39e9880bbf5d70538d82bbb05caf44c2c11484d80d06dee0589d6f75178c \\
Pure Object Address: & TMYQgJAnkDBZVfPWVEikmdFCVufuxzpsMuR \\
Theory Object Id: & 3a4ad2bbdc8560996c770f069c5b0861aa6f677de8c35f7e6825c37a062870ea \\
Theory Object Address: & TMPXygXB3Vatp7ehxXW1SzR7YDxpTfC383X
\end{tabular}
\end{center}

\end{definition}
Assume the following.
\begin{equation}
{\unicdcdaddd f : {{\iota}\unicdbdjdcd{\iota}} .  {{P}~{f}}}\label{hyp:affgih}
\end{equation}
Assume the following.
\begin{equation}
{\unicdcdadad f g : {{\iota}\unicdbdjdcd{\iota}} .  {{{P}~{f}}\unicdbdjdcd{{{P}~{g}}\unicdbdjdcd{{f}={g}}}}}\label{hyp:affhogjgbh}
\end{equation}
\begin{theorem}\label{thm:eefgdhdgchpfjgjgpfahchpgah} ${{P}~{\mname{Descr\_ii}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 45bfc0f7e5a41baec35381c982dec98e3138394009ea6479b4734e2b51ee3015 \\
Pure Prop Address: & TMRUGkPteutefnmzwHhFudjsxFRU5QyH8LU \\
Theory Prop Id: & e705d1e90646b5936b4d3f399b1ba2f451f5e0bfaa6d4ce06bde1703c2ac6afb \\
Theory Prop Address: & TMdRU9JrS4rFdHpHAP14V6T8N7yZhtAKeUt
\end{tabular}
\end{center}

\end{theorem}
\section{Descr\_iii}\label{eefgdhdgchpfjgjgjg}Let $ P : {{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}})}\unicdbdjdcd{o}}$ be given.
\begin{definition}\label{def:eefgdhdgchpfjgjgjg}
$\mname{Descr\_iii}$ is the opaque object of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & ca5fc17a582fdd4350456951ccbb37275637ba6c06694213083ed9434fe3d545 \\
Pure Object Address: & TMXQVeWJ4sPR355qf1XJWKLuqBobxgZ1f4j \\
Theory Object Id: & 877e40e99321711a3798c510f4a5784236e411ebab77a7914b276da43ccba50c \\
Theory Object Address: & TMUoa925kPFT8WA5VCxeG6JDVutAYyuK4A6
\end{tabular}
\end{center}

\end{definition}
Assume the following.
\begin{equation}
{\unicdcdaddd f : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}} .  {{P}~{f}}}\label{hyp:affgih}
\end{equation}
Assume the following.
\begin{equation}
{\unicdcdadad f g : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}} .  {{{P}~{f}}\unicdbdjdcd{{{P}~{g}}\unicdbdjdcd{{f}={g}}}}}\label{hyp:affhogjgbh}
\end{equation}
\begin{theorem}\label{thm:eefgdhdgchpfjgjgjgpfahchpgah} ${{P}~{\mname{Descr\_iii}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 261c3dac795dc9d12a850c45e12570f947cf3e73e7aac1d8b97f4fd8dfcaab74 \\
Pure Prop Address: & TMJbcddb8cyABNJEUp19YzaZ62uVYxZcxzw \\
Theory Prop Id: & 1604215f70483ff4639dd10934f543d9f25d48553a1e9dbbeae40186c6cf6c06 \\
Theory Prop Address: & TMLfZU6SKM2VC18naP9r39PVsCucjtdzWB9
\end{tabular}
\end{center}

\end{theorem}
\section{Descr\_iio}\label{eefgdhdgchpfjgjgpg}Let $ P : {{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}})}\unicdbdjdcd{o}}$ be given.
\begin{definition}\label{def:eefgdhdgchpfjgjgpg}
$\mname{Descr\_iio}$ is the opaque object of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & e8e5113bb5208434f24bf352985586094222b59a435d2d632e542c768fb9c029 \\
Pure Object Address: & TMc7TWyjFWcXBop91LuVowEJbeVve25nK5s \\
Theory Object Id: & 0423e66d8558444d27eb1068b080fe14267e388a7434254d29d1c826ce64ac94 \\
Theory Object Address: & TMJ6ajRQrfdbCkA3bH4AFazLF71vXbSokSz
\end{tabular}
\end{center}

\end{definition}
Assume the following.
\begin{equation}
{\unicdcdaddd f : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  {{P}~{f}}}\label{hyp:affgih}
\end{equation}
Assume the following.
\begin{equation}
{\unicdcdadad f g : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  {{{P}~{f}}\unicdbdjdcd{{{P}~{g}}\unicdbdjdcd{{f}={g}}}}}\label{hyp:affhogjgbh}
\end{equation}
\begin{theorem}\label{thm:eefgdhdgchpfjgjgpgpfahchpgah} ${{P}~{\mname{Descr\_iio}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 5dd3c7f22282c081da40fb112d8f2d8ffa44620b63f3136e2b179ca8f521ddc5 \\
Pure Prop Address: & TMVeGSPy1KHq36b4uHCMZWc5ghcexfzeT12 \\
Theory Prop Id: & 44dcac73e42284ed3d29fe0e058e46dcdf185b04829a0f7b5929c19617f0f40b \\
Theory Prop Address: & TMK1Bc1JaKqvjwRNdnxP1qds6eXGi9r8UaD
\end{tabular}
\end{center}

\end{theorem}

\section{Descr\_Vo1}\label{eefgdhdgchpfgfpgbd}

From now on we write $Vo~(n+1)$ to mean the type $Vo~n\to o$
where $Vo~0$ is $\iota$.

Let $ P : {{{Vo}~{1}}\unicdbdjdcd{o}}$ be given.
\begin{definition}\label{def:eefgdhdgchpfgfpgbd}
$\mname{Descr\_Vo1}$ is the opaque object of type ${{Vo}~{1}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 615c0ac7fca2b62596ed34285f29a77b39225d1deed75d43b7ae87c33ba37083 \\
Pure Object Address: & TMFQ3dBkT4GNkBxqPW23PKfo5eca5LbGLnM \\
Theory Object Id: & a4ecddac25cdabd614bf297524a2acb05724493b89ab7e7e636cf452a8887b01 \\
Theory Object Address: & TMS1y5bGeSZGkV7sivczRgNAQUcrNTaGYAX
\end{tabular}
\end{center}

\end{definition}
Assume the following.
\begin{equation}
{\unicdcdaddd f : {{Vo}~{1}} .  {{P}~{f}}}\label{hyp:affgih}
\end{equation}
Assume the following.
\begin{equation}
{\unicdcdadad f g : {{Vo}~{1}} .  {{{P}~{f}}\unicdbdjdcd{{{P}~{g}}\unicdbdjdcd{{f}={g}}}}}\label{hyp:affhogjgbh}
\end{equation}
\begin{theorem}\label{thm:eefgdhdgchpfgfpgbdpfahchpgah} ${{P}~{\mname{Descr\_Vo1}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f550ef6a927da855d9705aafeb7607fe3931aa8ec0f5f675da6011e035f22458 \\
Pure Prop Address: & TMMwzBC9pSvmYAJivGEMP4qt8Mt7WyJqduS \\
Theory Prop Id: & 2213e2f6bf896b176ce81e3f28c06d4eda10bd33020cb296513b4b938fcd9056 \\
Theory Prop Address: & TMLLpH2SQbA7WJA4grh8eUgfwMWFcLKc8kH
\end{tabular}
\end{center}

\end{theorem}
\section{Descr\_Vo2}\label{eefgdhdgchpfgfpgcd}Let $ P : {{{Vo}~{2}}\unicdbdjdcd{o}}$ be given.
\begin{definition}\label{def:eefgdhdgchpfgfpgcd}
$\mname{Descr\_Vo2}$ is the opaque object of type ${{Vo}~{2}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & a64b5b4306387d52672cb5cdbc1cb423709703e6c04fdd94fa6ffca008f7e1ab \\
Pure Object Address: & TMFZfGbPgS43AdHK51F7w5aNLJzHmKsdsJN \\
Theory Object Id: & 546d66811c244b38780425746c3230f23c0a0c78c5d74a314c6ec8eca20e5571 \\
Theory Object Address: & TMQQUC9cTGz9T8416CfsGFpzXHbvVhpxAu2
\end{tabular}
\end{center}

\end{definition}
Assume the following.
\begin{equation}
{\unicdcdaddd f : {{Vo}~{2}} .  {{P}~{f}}}\label{hyp:affgih}
\end{equation}
Assume the following.
\begin{equation}
{\unicdcdadad f g : {{Vo}~{2}} .  {{{P}~{f}}\unicdbdjdcd{{{P}~{g}}\unicdbdjdcd{{f}={g}}}}}\label{hyp:affhogjgbh}
\end{equation}
\begin{theorem}\label{thm:eefgdhdgchpfgfpgcdpfahchpgah} ${{P}~{\mname{Descr\_Vo2}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 95fc538f5d5098f54c64e376e95b1284227552f9e403c9a68ca16035b2a69c37 \\
Pure Prop Address: & TMLM1fK9jLGpTqnThj3QLyRf4RLDCjDXKzv \\
Theory Prop Id: & 763c84ad5f1253ac14ad30d1f2765feaf5cc0cdc449dab033ce038bcc35d452c \\
Theory Prop Address: & TMaBE8ZNQAt1zVAJ1G6cs2yjF99pYEBGHwz
\end{tabular}
\end{center}

\end{theorem}
\section{If\_ii}\label{jeggpfjgjg}Let $ p : {o}$ be given.
Let $ f g : {{\iota}\unicdbdjdcd{\iota}}$ be given.
\begin{definition}\label{def:jeggpfjgjg}
$\mname{If\_ii}$ is the opaque object of type ${{\iota}\unicdbdjdcd{\iota}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 17057f3db7be61b4e6bd237e7b37125096af29c45cb784bb9cc29b1d52333779 \\
Pure Object Address: & TMJ5CGNSX9XjHHwnu1BSQsVHCKzSFJcwu4b \\
Theory Object Id: & e290152395c5a355ecc6c5012e4cd4507f1895df9d71192a4e860e914c8db43e \\
Theory Object Address: & TMPHWP247Vz8BvmmXSfTeVHxvDsaU8cpPU8
\end{tabular}
\end{center}

\end{definition}
\begin{theorem}\label{thm:jeggpfjgjgpfbd} ${{p}\unicdbdjdcd{{\mname{If\_ii}}={f}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 31521ec60d1fb026a6fc18736822f20291fbb3d33597bb3efce99a03f03e11d9 \\
Pure Prop Address: & TMKosiG2dup6SxL5QSDUpucfR51n9gCyDgV \\
Theory Prop Id: & 342a1f3e82c1abf29e708798f7feb58587435d6e872e0fad569a7aa4aff40c55 \\
Theory Prop Address: & TMc5keGi4Y146iSqaxLiaYsAZYq1XuEVqNB
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeggpfjgjgpfad} ${{\preoh{{p}}}\unicdbdjdcd{{\mname{If\_ii}}={g}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 6acab05b8c4b66e4263e5b31aaa005d9f082668a8bbace0e6d83fd1b4f2a4e7c \\
Pure Prop Address: & TMNxHhMohQMfeSQ46TzksCAdPGGHded4fQn \\
Theory Prop Id: & 36418b196a3dc55851db392b475c08d495d7976847a1bfe1ffa0839c921a9904 \\
Theory Prop Address: & TMJAFTnXbqvZwsoNakQckwUkzUMcWByPVDq
\end{tabular}
\end{center}

\end{theorem}
\section{If\_iii}\label{jeggpfjgjgjg}Let $ p : {o}$ be given.
Let $ f g : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ be given.
\begin{definition}\label{def:jeggpfjgjgjg}
$\mname{If\_iii}$ is the opaque object of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 3314762dce5a2e94b7e9e468173b047dd4a9fac6ee2c5f553c6ea15e9c8b7542 \\
Pure Object Address: & TMafEMcrDN1G9aE3ciBtqxzAhjPGbGo9wGT \\
Theory Object Id: & dd7e2b57dd8bff886e536f76317306bce1d1c82c8d0c4990736c5435d5194472 \\
Theory Object Address: & TMXbifVhYnu2zzxcRpGBEz7yE8Zgdxct2bF
\end{tabular}
\end{center}

\end{definition}
\begin{theorem}\label{thm:jeggpfjgjgjgpfbd} ${{p}\unicdbdjdcd{{\mname{If\_iii}}={f}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 2d62ee998f0e93e8531c4fa56ae24814f441c745adbbf870b6533f8348e4105d \\
Pure Prop Address: & TMXoAktu9YHuqADS1FQhmqPQo88e8Wfe9Tc \\
Theory Prop Id: & 48bc10484ec823e29188216c5145c832ea01049091770c743d54872c69c3738d \\
Theory Prop Address: & TMP1NQtm8tugHGMUGtnKEr16wjn5P3HapKj
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeggpfjgjgjgpfad} ${{\preoh{{p}}}\unicdbdjdcd{{\mname{If\_iii}}={g}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 9b77d90fae20e665d930e198836d49c2f016c9359f15a9036520651d80559a50 \\
Pure Prop Address: & TMMxCCtSQ76TqwLa7cLQxLYRL1uvAhxf6G5 \\
Theory Prop Id: & d11201a0fa74b1965c04633e2fbf7c186e42c0fbf53635dd329a7bb860c6b930 \\
Theory Prop Address: & TMG9gLyxAgRsyCSfKKidGTT9tPyeptZY75x
\end{tabular}
\end{center}

\end{theorem}
\section{If\_Vo1}\label{jeggpfgfpgbd}Let $ p : {o}$ be given.
Let $ f g : {{Vo}~{1}}$ be given.
\begin{definition}\label{def:jeggpfgfpgbd}
$\mname{If\_Vo1}$ is the opaque object of type ${{Vo}~{1}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 2bb1d80de996e76ceb61fc1636c53ea4dc6f7ce534bd5caee16a3ba4c8794a58 \\
Pure Object Address: & TMJRubZpJkuKGf6tLSqj98TBUniTgSkcx2k \\
Theory Object Id: & c5705984e5c61b59990fd2a143acd737bb2dc7c7db647a62e398dac074967687 \\
Theory Object Address: & TMaRPXSn2Fjb29o31JvamGmuMJnp68JPVyZ
\end{tabular}
\end{center}

\end{definition}
\begin{theorem}\label{thm:jeggpfgfpgbdpfbd} ${{p}\unicdbdjdcd{{\mname{If\_Vo1}}={f}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & bb1012256bb9266025d71663756a5ebfd5e16baf8e93a915bfdd7fcb42d706f3 \\
Pure Prop Address: & TMXYuJm2QUHmNybRpkXiJxzCLG25czuz5LQ \\
Theory Prop Id: & 62b2b86d0737e9e18346982d5767e5ef03ab4118b70f45a9ff56d1c9e5216feb \\
Theory Prop Address: & TMFtdqVK8VYTrQ6cgnnamxbg6KeHhpZgPcd
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeggpfgfpgbdpfad} ${{\preoh{{p}}}\unicdbdjdcd{{\mname{If\_Vo1}}={g}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 59bda37f5c7398ead6c4b3243129fbad85f4f9f3636487f1c51cce4e0e6c8cfd \\
Pure Prop Address: & TMWqGQPgK8uAv1B3geaEm1MSYAnLtEgFcb9 \\
Theory Prop Id: & 78529c61edfcd02459bc4ec507c773553a628c9c32db5afd8b9669bdeb5624be \\
Theory Prop Address: & TMFdPp5SLYgJtZvzVSfP9YVDKe598dst2rw
\end{tabular}
\end{center}

\end{theorem}
\section{If\_iio}\label{jeggpfjgjgpg}Let $ p : {o}$ be given.
Let $ f g : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}}$ be given.
\begin{definition}\label{def:jeggpfjgjgpg}
$\mname{If\_iio}$ is the opaque object of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & bf2fb7b3431387bbd1ede0aa0b590233207130df523e71e36aaebd675479e880 \\
Pure Object Address: & TMSVGinFUSHBKXoj7UW42oxwqfA45nW9uYC \\
Theory Object Id: & f0254ba33a025d14997148eaf8b6489b75cbcd0e552813782f2fee4dac52a1ad \\
Theory Object Address: & TMVgQ7ZnQFc9zUqLQEygvRvocriNyw8Urgz
\end{tabular}
\end{center}

\end{definition}
\begin{theorem}\label{thm:jeggpfjgjgpgpfbd} ${{p}\unicdbdjdcd{{\mname{If\_iio}}={f}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 6e5b2f9d60ee2b95f684c6c89fac222c87c115edd65ea7faa36260e77030c34b \\
Pure Prop Address: & TMbdPHYFQQVTEPDFuKsr2RTPtLJWVQCkgmo \\
Theory Prop Id: & 5c40c9c2a99e6214c0a2e1d4e4d8ffe6b45d1a1be5958c0a0e817a962bcb2e40 \\
Theory Prop Address: & TMYBc7MrgDRDwERk16x3XtsYSbpzRT4JfeS
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeggpfjgjgpgpfad} ${{\preoh{{p}}}\unicdbdjdcd{{\mname{If\_iio}}={g}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 9eab66913f2b7839396a2642931e0c4f2b5b96d45aa947c433210d1358ad7ce9 \\
Pure Prop Address: & TMLjBZs3dbH9f9eUHYnJdu3t2Pqbht8aDBr \\
Theory Prop Id: & 09748b1d13dc8a2265025a9ce3f481495c8a7bccd4d956b5d4fc36dd28dfbd2b \\
Theory Prop Address: & TMbk4ju7Bfvef6aQhpURVB4h7ERGCJXtpm5
\end{tabular}
\end{center}

\end{theorem}
\section{If\_Vo2}\label{jeggpfgfpgcd}Let $ p : {o}$ be given.
Let $ f g : {{Vo}~{2}}$ be given.
\begin{definition}\label{def:jeggpfgfpgcd}
$\mname{If\_Vo2}$ is the opaque object of type ${{Vo}~{2}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 6cf28b2480e4fa77008de59ed21788efe58b7d6926c3a8b72ec889b0c27b2f2e \\
Pure Object Address: & TMH4op1eDosdCj4CskKLdVdQMoEMPyaKmKz \\
Theory Object Id: & f6760c1a5f26147ef91098a2d633b2f19a2f38b9c1c811244491274cf056b285 \\
Theory Object Address: & TMZuq1Mx5McSmUfVdPQ43iubWhx4f9CctV4
\end{tabular}
\end{center}

\end{definition}
\begin{theorem}\label{thm:jeggpfgfpgcdpfbd} ${{p}\unicdbdjdcd{{\mname{If\_Vo2}}={f}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0f655bcb4e8ea858e1e47b901188715bcb9443ff29ca227273b5eeab5ccce4fa \\
Pure Prop Address: & TMLf5qJmSHrs6Umik46niap6g6Puq8u38PZ \\
Theory Prop Id: & 530c03e594647527928784ed02365579d201bd63d29f76cf2679ec77f9c3a348 \\
Theory Prop Address: & TMYAJeyWgmE86YRTxka8iZ3VDvWDz4KFVak
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeggpfgfpgcdpfad} ${{\preoh{{p}}}\unicdbdjdcd{{\mname{If\_Vo2}}={g}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & ba20c1835570284aac2a734187c79818c51b3e6b4ef50125ec114563e95c56a3 \\
Pure Prop Address: & TMFhCsW5TbyvNPeCPg5q8UZQCNrh7ba7mc7 \\
Theory Prop Id: & 49a8cfcdec6a427975b6c3b9ac4c13c6b5dbfa0624fe913a360d44ecd3993241 \\
Theory Prop Address: & TMRyczcoeSo63tGt7RMgBM4C9d1EHxcvBZi
\end{tabular}
\end{center}

\end{theorem}
