\chapter{If-then-else, Description and Recursion again}
\section{If\_Vo3}\label{jeggpfgfpgdd}Let $ p : {o}$ be given.
Let $ f g : {{Vo}~{3}}$ be given.
\begin{definition}\label{def:jeggpfgfpgdd}
$\mname{If\_Vo3}$ is the opaque object of type ${{Vo}~{3}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 73dd2d0fb9a3283dfd7b1d719404da0bf605e7b4c7b714a2b4e2cb1a38d98c6f \\
Pure Object Address: & TMcasq19pTUcLufiu26HYpBfxPmeYk6E8mT \\
Theory Object Id: & 333c92c590bdda1d300a193515c5804607be8cb804a38180a59610b36281676f \\
Theory Object Address: & TMKVqTVDwSwbDy1BLiFYKZbD6QhkcDSVJhc
\end{tabular}
\end{center}

\end{definition}
\begin{theorem}\label{thm:jeggpfgfpgddpfbd} ${{p}\unicdbdjdcd{{\mname{If\_Vo3}}={f}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 9cf80c77cf895a06b2027489d75da25a65f13d09dbb89106276596f1621e9190 \\
Pure Prop Address: & TMJ2NGWhftpmGTYwAy7YTG5gSV15BG4yDC4 \\
Theory Prop Id: & da37c739b9dd4956b241bec65be35f2c5b0640a3526959d750cfa4bcd78d0621 \\
Theory Prop Address: & TMNrJsMGCaKdKHP7L2e4Nm4EZXFs2uCAAw3
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeggpfgfpgddpfad} ${{\preoh{{p}}}\unicdbdjdcd{{\mname{If\_Vo3}}={g}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 26938a02bd0536ce534ff744512cc88eb86cd2ee1226183b145cae855a142032 \\
Pure Prop Address: & TMUNMynXzuArTTrK7p5jFXqihZJb43NBe7x \\
Theory Prop Id: & df49a9a1ae039c4a570658bf925b0179e4b0a63bbabd6021b74d66c7c709f80f \\
Theory Prop Address: & TMb4qEYPVKmSarAqVUz7NwbCdaKVAkyNYPm
\end{tabular}
\end{center}

\end{theorem}
\section{Descr\_Vo3}\label{eefgdhdgchpfgfpgdd}Let $ P : {{{Vo}~{3}}\unicdbdjdcd{o}}$ be given.
\begin{definition}\label{def:eefgdhdgchpfgfpgdd}
$\mname{Descr\_Vo3}$ is the opaque object of type ${{Vo}~{3}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & f25ee4a03f8810e3e5a11b184db6c8f282acaa7ef4bfd93c4b2de131431b977c \\
Pure Object Address: & TMQ2iYFqmoYhwP7TbZqwfTHcnxkgx715jsM \\
Theory Object Id: & d479f5126402f52d9a58899c5731677dad9533674526ab2b066def43094eec28 \\
Theory Object Address: & TMSADgxCz6JBunRMJpa7zmWr51aLHrZXZwg
\end{tabular}
\end{center}

\end{definition}
Assume the following.
\begin{equation}
{\unicdcdaddd f : {{Vo}~{3}} .  {{P}~{f}}}\label{hyp:affgih}
\end{equation}
Assume the following.
\begin{equation}
{\unicdcdadad f g : {{Vo}~{3}} .  {{{P}~{f}}\unicdbdjdcd{{{P}~{g}}\unicdbdjdcd{{f}={g}}}}}\label{hyp:affhogjgbh}
\end{equation}
\begin{theorem}\label{thm:eefgdhdgchpfgfpgddpfahchpgah} ${{P}~{\mname{Descr\_Vo3}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 20174ae5a109b906a46115d971515a729f9249f4f20fa5da310e2c4cdeab6249 \\
Pure Prop Address: & TMLwRSBien4w3CzFgCJ48yAfqXd7PCssRGE \\
Theory Prop Id: & 23c590cb67150ebe43754899c3f2b5d5f0927084676267173928ecff860e70b5 \\
Theory Prop Address: & TMWShaCPNhN2XvW2e4gefY2XgoDY4dWexFY
\end{tabular}
\end{center}

\end{theorem}
\section{EpsilonRec\_Vo3}\label{feahdhjgmgpgogcffgdgpfgfpgdd}Let $ F : {{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{{Vo}~{3}}})}\unicdbdjdcd{{Vo}~{3}}}}$ be given.
\begin{definition}\label{def:jeogpfchfgdgpfgfpgdd}
$\mname{In\_rec\_Vo3}$ is the opaque object of type ${{\iota}\unicdbdjdcd{{Vo}~{3}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 80f7da89cc801b8279f42f9e1ed519f72d50d76e88aba5efdb67c4ae1e59aee0 \\
Pure Object Address: & TMTrS1bWLxXMW5qTfHXLxP8rqsqDfcSj5it \\
Theory Object Id: & d1066f5fb07b44eb37af262f1b8cbfa415ea64116ce40aa20ad290bbdbba780e \\
Theory Object Address: & TMdJy3eq8ZYfdDZguQUCdxZ6rfJuYZZntCT
\end{tabular}
\end{center}

\end{definition}
Assume the following.
\begin{equation}
{\unicdcdadad X : {\iota} .  {\unicdcdadad g h : {{\iota}\unicdbdjdcd{{Vo}~{3}}} .  {{({\unicdcdadad x \in {X} .  {{{g}~{x}}={{h}~{x}}}})}\unicdbdjdcd{{{{F}~{X}}~{g}}={{{F}~{X}}~{h}}}}}}\label{hyp:gech}
\end{equation}
\begin{theorem}\label{thm:jeogpfchfgdgpfgfpgddpffgbh} ${\unicdcdadad X : {\iota} .  {{{\mname{In\_rec\_Vo3}}~{X}}={{{F}~{X}}~{\mname{In\_rec\_Vo3}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 2306eb8b31f5ee276553420c5e1f5c8c0651e1258c44c87a9c42e96bd3e79503 \\
Pure Prop Address: & TMaEn9SrA4LtLzZLVV3UpDHnxpFiFAqzKBz \\
Theory Prop Id: & 4d2789ab957df70c09911021b3cc17f5578b5a09007513d609947d6805b3ca93 \\
Theory Prop Address: & TMaSVdip28DZxPPo4ByXDcTwLWpi4sfc89Q
\end{tabular}
\end{center}

\end{theorem}
\section{If\_Vo4}\label{jeggpfgfpged}Let $ p : {o}$ be given.
Let $ f g : {{Vo}~{4}}$ be given.
\begin{definition}\label{def:jeggpfgfpged}
$\mname{If\_Vo4}$ is the opaque object of type ${{Vo}~{4}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 1a8f92ceed76bef818d85515ce73c347dd0e2c0bcfd3fdfc1fcaf4ec26faed04 \\
Pure Object Address: & TMFG5MpDVE3nFZV3NJZdM6wd42HBKVgpUkN \\
Theory Object Id: & 6f23a6aeaffecd3215c88a1ad6970a5926ecd481bf402e6873321d936dc9a49b \\
Theory Object Address: & TMPj7rvJRkP19dsCJAFArEnBpzMnvjtktEW
\end{tabular}
\end{center}

\end{definition}
\begin{theorem}\label{thm:jeggpfgfpgedpfbd} ${{p}\unicdbdjdcd{{\mname{If\_Vo4}}={f}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 06ad5c864f232538e5dcbad7b8a51389f2b7630bb8f0576bcc523d1811805afa \\
Pure Prop Address: & TMLaXf8kJ7EdCg7P6GR8txEnTFCZNLrNGCx \\
Theory Prop Id: & 3d1a5d619766f7ca661d7cf070c1c9e481cb4a26a2603723df79b27fbc512fc5 \\
Theory Prop Address: & TMTdC39nPta5qDs73eUJZFWgNT3PKvCQPkp
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:jeggpfgfpgedpfad} ${{\preoh{{p}}}\unicdbdjdcd{{\mname{If\_Vo4}}={g}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & bab37df6d4aabf30ec549e549b8fff3336e2c7eebd629e65365508a0a69be04b \\
Pure Prop Address: & TMTttbgudyrZKJvKhjQTui2Nr8qLhE3y4SX \\
Theory Prop Id: & 24dc8a58d4de615eeb9b719733472bdc39bddf577984e0488dbf60ad72aa5b3e \\
Theory Prop Address: & TMdiwt98qwWvCbCfyBMTBrpGjo53TgoPrZM
\end{tabular}
\end{center}

\end{theorem}
\section{Descr\_Vo4}\label{eefgdhdgchpfgfpged}Let $ P : {{{Vo}~{4}}\unicdbdjdcd{o}}$ be given.
\begin{definition}\label{def:eefgdhdgchpfgfpged}
$\mname{Descr\_Vo4}$ is the opaque object of type ${{Vo}~{4}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 8b81abb8b64cec9ea874d5c4dd619a9733a734933a713ef54ed7e7273510b0c3 \\
Pure Object Address: & TMLVDACU3jLYPMh9iPh1uhucMrsTaATPeZN \\
Theory Object Id: & 85f7ca0492b5dac0db0a41ea793b13fcebe7b788606ad42263186b19feb60364 \\
Theory Object Address: & TMd1yKi67f99nixn38zFHJA2mC8ypLfDMrV
\end{tabular}
\end{center}

\end{definition}
Assume the following.
\begin{equation}
{\unicdcdaddd f : {{Vo}~{4}} .  {{P}~{f}}}\label{hyp:affgih}
\end{equation}
Assume the following.
\begin{equation}
{\unicdcdadad f g : {{Vo}~{4}} .  {{{P}~{f}}\unicdbdjdcd{{{P}~{g}}\unicdbdjdcd{{f}={g}}}}}\label{hyp:affhogjgbh}
\end{equation}
\begin{theorem}\label{thm:eefgdhdgchpfgfpgedpfahchpgah} ${{P}~{\mname{Descr\_Vo4}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a6473b3334fd689271114e94dd8501ed316b996fca678cfd212ee147617f3b63 \\
Pure Prop Address: & TMFnuCwCTVMsFiXKonkd3YBQ9HMaKew1LfE \\
Theory Prop Id: & 3e862cb55935309dafceacc6dca361c6a70271794a80e68a76ec04b8d5b78104 \\
Theory Prop Address: & TMXUspN6Sx6CYJpANQyhMG8CHovhesMrXwZ
\end{tabular}
\end{center}

\end{theorem}
\section{EpsilonRec\_Vo4}\label{feahdhjgmgpgogcffgdgpfgfpged}Let $ F : {{\iota}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{{Vo}~{4}}})}\unicdbdjdcd{{Vo}~{4}}}}$ be given.
\begin{definition}\label{def:jeogpfchfgdgpfgfpged}
$\mname{In\_rec\_Vo4}$ is the opaque object of type ${{\iota}\unicdbdjdcd{{Vo}~{4}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & d82c5791815ca8155da516354e8f8024d8b9d43a14ce62e2526e4563ff64e67f \\
Pure Object Address: & TMFrL2oqNRAHoTkwnxvXz88hCQoB8Uoidfq \\
Theory Object Id: & 1e5061b04de4514b3a4c4ea251fd26dd589083b04c1276fec71c858ef714657d \\
Theory Object Address: & TMc9WkccuALwugHXmUhucdGnwNEmZuusP9z
\end{tabular}
\end{center}

\end{definition}
Assume the following.
\begin{equation}
{\unicdcdadad X : {\iota} .  {\unicdcdadad g h : {{\iota}\unicdbdjdcd{{Vo}~{4}}} .  {{({\unicdcdadad x \in {X} .  {{{g}~{x}}={{h}~{x}}}})}\unicdbdjdcd{{{{F}~{X}}~{g}}={{{F}~{X}}~{h}}}}}}\label{hyp:gech}
\end{equation}
\begin{theorem}\label{thm:jeogpfchfgdgpfgfpgedpffgbh} ${\unicdcdadad X : {\iota} .  {{{\mname{In\_rec\_Vo4}}~{X}}={{{F}~{X}}~{\mname{In\_rec\_Vo4}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 222bdbe9dc303a7fe1b2a2e6e60547f51606b31268e865e7f48ccdfc78fab6dc \\
Pure Prop Address: & TMLZ4TCFwAU7GVexuLeFpen6YpZfwwTmUrz \\
Theory Prop Id: & ab3561ec7f79f59905a72739474d784abea229696e9c83807694ef845230da1b \\
Theory Prop Address: & TMTTyAbVG9aCnaLjwPoFSBiNHFM6ZrztqWx
\end{tabular}
\end{center}

\end{theorem}
