\chapter{More Logical Properties}
\begin{verbatim}
eq_imp_or
\end{verbatim}
\begin{theorem}\label{thm:fgbhpfjgngahpfpgch} ${{({\uniddcgcg x y : {o} .  {({{x}\unicdbdjdcd{y}})}})}={({\uniddcgcg x y : {o} .  {({{\preoh{{x}}}\unicdcdcdid{y}})}})}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 06c3093aa740f38323ae4d7f0dbad8d508f40a0ca90fa41e9f01516651c3e3c1 \\
Pure Prop Address: & TMFQ6hVxLyhKxQEQs23Xv9LC6mgW4iwwgrX \\
Theory Prop Id: & 4c9dc0935ef80cbfc0fc55cf8abb066203b42c66e60c4bb6af8b939a9f3dba5a \\
Theory Prop Address: & TMRjkjWby7U8Aw7kefWq3i3PMiD7ahDD43F
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
famunion_Empty
\end{verbatim}
\begin{theorem}\label{thm:ggbgngfhogjgpgogpffengahehjh} ${\unicdcdadad F : {{\iota}\unicdbdjdcd{\iota}} .  {{({\unicdcddedd _{x \in {0}}{{F}~{x}}})}={0}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & fc1bdd286f0d898d898c29f18fbe095090efb65893028ab68d5f98d8caa05ce9 \\
Pure Prop Address: & TMZjHxMN3FYwok47JsaP7dDQjKXS6jyzcQx \\
Theory Prop Id: & 22bd10cff6495d6e03e6e76619e1426110cc714a9d78d666213a9e4d3b7897b2 \\
Theory Prop Address: & TMTAVVZK8aANakE2V9u1NoVueYVDuUeiPWu
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Empty_or_ex
\end{verbatim}
\begin{theorem}\label{thm:fengahehjhpfpgchpffgih} ${\unicdcdadad X : {\iota} .  {{{X}={\mname{Empty}}}\unicdcdcdid{\unicdcdaddd x : {\iota} .  {{x} \in {X}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & ea40ae60ad1226481a72c72991900ab1d75eaab2f2603b30f4021ec9bfa53243 \\
Pure Prop Address: & TMN7F3M7BEyv9u1wysCYB4eCnjR17p8fFPJ \\
Theory Prop Id: & 16587d445d1c65fd759cdc12b7fec9089c4b514284913be85bb2bfbaa6fe4f57 \\
Theory Prop Address: & TMGoeYYeEjatMCpA5EmBZSLRbtsqeYFpDcB
\end{tabular}
\end{center}

\end{theorem}
