\chapter{Misc}

\begin{verbatim}
f_eq_i
\end{verbatim}
\begin{theorem}\label{thm:ggpffgbhpfjg} ${\unicdcdadad f : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad x y .  {{{x}={y}}\unicdbdjdcd{{{f}~{x}}={{f}~{y}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & b0871b523a7b57f1eb5aaeab0fc7f0a48159bfb735912ea5ae95f631f41659b1 \\
Pure Prop Address: & TMPVNZYtUqHTp8RYLtZcxXu3DU3ivfR6rAr \\
Theory Prop Id: & 2a60fd880e3c5cee57da00ac972ed9116312115366d80d946af04bdedf52ba41 \\
Theory Prop Address: & TMcdcpfCVRxKR6sYN1s4kVKEHiMfK814Qv1
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
f_eq_i_i
\end{verbatim}
\begin{theorem}\label{thm:ggpffgbhpfjgpfjg} ${\unicdcdadad f : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}} .  {\unicdcdadad x y z w .  {{{x}={y}}\unicdbdjdcd{{{z}={w}}\unicdbdjdcd{{{{f}~{x}}~{z}}={{{f}~{y}}~{w}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 99d67d79970e96836845a0ba205f2ae8cf38fbbe7c66edb2e3dd47679e886175 \\
Pure Prop Address: & TMVyNZC57hm2JCbUEkm54EFRxyjV7uKHLYV \\
Theory Prop Id: & 47e5770eb29a6575bfe0da11c0c722b53eaa9c4f54a6338e54fda222161f1310 \\
Theory Prop Address: & TMJfWQ8qLkS2wi6eLaJhtLGmdrxxJvCx3w1
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
eq_i_tra
\end{verbatim}
\begin{theorem}\label{thm:fgbhpfjgpfehchbg} ${\unicdcdadad x y z .  {{{x}={y}}\unicdbdjdcd{{{y}={z}}\unicdbdjdcd{{x}={z}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 193bbfd16b1f36c82abc18861eb9920fd3ebdab3fa714704e5d9ee842a572cc0 \\
Pure Prop Address: & TMMRUBbS4C1QBM5KZBX4P26LywnZaH7iKjP \\
Theory Prop Id: & 7ecbc48d1e90e90e475c12e4250d6ed1b153fe65d79663458f1516c1b19ef29e \\
Theory Prop Address: & TMMtqtU6uJfRVq7S9aPMj7up363DpEmoc8j
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:ogdffhcgbh}
We define $\mname{nSubq}$ to be ${\uniddcgcg X Y .  {\preoh{{{{\mname{Subq}}~{X}}~{Y}}}}}$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & ea71e0a1be5437cf5b03cea5fe0e2b3f947897def4697ae7599a73137f27d0ee \\
Pure Object Address: & TMZtJ57VpuWkqSBd372tXDYbQV1ru9RQiP6 \\
Theory Object Id: & 1b32290aed0c0437eee0d631ba16b62c8142cad8d60330e8a2c72a430b7453ae \\
Theory Object Address: & TMUnveDfk5UPe9zq9bRZ9NGMx9j7NA22YVb
\end{tabular}
\end{center}

\end{definition}
{\bf{Notation.}} We use $\infpcdgnd$ as an infix operator  corresponding to applying term ${\mname{nSubq}}$.
\begin{verbatim}
Sing_inv
\end{verbatim}
\begin{theorem}\label{thm:dfjgoghgpfjgoggh} ${\unicdcdadad x Y .  {{{\{{x}\}}={Y}}\unicdbdjdcd{{{x} \in {Y}}\unicdcdcdhd{\unicdcdadad y \in {Y} .  {{y}={x}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 57ae4c95e879681858c5ff28d750d4d70e50b072a6d15b2feb91ea9fcef02da8 \\
Pure Prop Address: & TMGqotQdzdFCuZC8q4vqVRkFBMW4qjArQ3h \\
Theory Prop Id: & 199c6ccf6b8a2d5af1b102b165811324c6387df31287b0a86242c6611b629fed \\
Theory Prop Address: & TMMav2V1grSCKmckxQqmeTmvNxWh6DUx8uL
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
TransSet_In_ordsucc_Subq
\end{verbatim}
\begin{theorem}\label{thm:efchbgogdhdffgehpfjeogpfpgchegdhfhdgdgpfdffhcgbh} ${\unicdcdadad x y .  {{{\mname{TransSet}}~{y}}\unicdbdjdcd{{{x} \in {{\mname{ordsucc}}~{y}}}\unicdbdjdcd{{x} \subseteq {y}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f80c6ef5328d1aebbabe1261cb2a17127aad514383c2c09bbf3354725a9afe82 \\
Pure Prop Address: & TMPqbNun9yFToi13JVKcoYQrF59XATjGUYz \\
Theory Prop Id: & 34199340a5562195ace40af331c0a1da26d29faac3847d7b38f9e829ab506bd5 \\
Theory Prop Address: & TMH3pW2NLQvrgTnYbQVg1dcwdjLcHFcyHCU
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
inv_Repl_eq
\end{verbatim}
\begin{theorem}\label{thm:jgogghpfcffgahmgpffgbh} ${\unicdcdadad X .  {\unicdcdadad f g : {{\iota}\unicdbdjdcd{\iota}} .  {{({\unicdcdadad x \in {X} .  {{{f}~{({{g}~{x}})}}={x}}})}\unicdbdjdcd{{\{{{f}~{y}}|y \in {\{{{g}~{x}}|x \in {X}\}}\}}={X}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & de1759e07c1622dd0cf2ac0a92f57c8d0d379b3d4ee285440b6de212666d9eae \\
Pure Prop Address: & TMSStFLLm81AFEdPaJMUoYdRHkYa5ucHRD2 \\
Theory Prop Id: & 5a8fc2fd0b67b701a32a2d1b39179d4975ca830fffb1452d564b9af4e10a99b9 \\
Theory Prop Address: & TMTeQxUhBU7C2YeyWfVA7p37xMSPpxyofrK
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
invol_Repl_eq
\end{verbatim}
\begin{theorem}\label{thm:jgogghpgmgpfcffgahmgpffgbh} ${\unicdcdadad X .  {\unicdcdadad f : {{\iota}\unicdbdjdcd{\iota}} .  {{({\unicdcdadad x \in {X} .  {{{f}~{({{f}~{x}})}}={x}}})}\unicdbdjdcd{{\{{{f}~{y}}|y \in {\{{{f}~{x}}|x \in {X}\}}\}}={X}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 87b0604e91d11a8b4c06ac87cda6148fe5e60301aa91d79609febf82042a8ce3 \\
Pure Prop Address: & TMQznwJJoHjcdkGoE3rvi8W9R6zhQ68ZwCc \\
Theory Prop Id: & 393cc6aeb2c74236699aca97e243d3db17d6149941639ffde4f7d58dc26b2e6c \\
Theory Prop Address: & TMW5YcT8N18dkwdFihvpKYK9P8scfdxJAhs
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
Eps_i_set_R
\end{verbatim}
\begin{theorem}\label{thm:feahdhpfjgpfdhfgehpfcf}
$$
\begin{array}{c}
\unicdcdadad X : {\iota} .  \unicdcdadad P : {{\iota}\unicdbdjdcd{o}} .  \unicdcdadad x \in {X} .  {{P}~{x}}\unicdbdjdcd{{{\mname{Eps\_i}}~{({\uniddcgcg x .  {{{x} \in {X}}\unicdcdcdhd{{P}~{x}}}})}} \in {X}}\\
\unicdcdcdhd{{P}~{({{\mname{Eps\_i}}~{({\uniddcgcg x .  {{{x} \in {X}}\unicdcdcdhd{{P}~{x}}}})}})}}.
\end{array}
$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & b4f328ffb79aabb0df4389dfe10d26a1a90d7ed192a2b7e062aae20ce483c959 \\
Pure Prop Address: & TMFghbYQCmAiS83QkiJceQ1ocqagGS8fdof \\
Theory Prop Id: & a78d0d896dcf99f0838ebc9fbab4b2d7723c3dc6238c649009cf14a169e85421 \\
Theory Prop Address: & TMF6oMG8oYpvhQhrGCFXfDFrJYvD2UUnWF3
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
exandE_i
\end{verbatim}
\begin{theorem}\label{thm:fgihbgogegfepfjg} ${\unicdcdadad P Q : {{\iota}\unicdbdjdcd{o}} .  {{({\unicdcdaddd x .  {{{P}~{x}}\unicdcdcdhd{{Q}~{x}}}})}\unicdbdjdcd{\unicdcdadad r : {o} .  {{({\unicdcdadad x .  {{{P}~{x}}\unicdbdjdcd{{{Q}~{x}}\unicdbdjdcd{r}}}})}\unicdbdjdcd{r}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 083f822f238e73865a8e53f1b501a3274298103440996953b5dbe5b9f1c64a49 \\
Pure Prop Address: & TMcSPtKUzzFxn3xkTT3qXkbEzgxdcFKD64W \\
Theory Prop Id: & b1b26e0e1db0dccbd32126585f43f1f764c8cd693eeb9898836853ddea6300a1 \\
Theory Prop Address: & TMYHN9RveUaKq4szKucPeZQCRGkDxZMkhgC
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
exandE_ii
\end{verbatim}
\begin{theorem}\label{thm:fgihbgogegfepfjgjg}
$$\begin{array}{c}
\unicdcdadad P Q : {{({{\iota}\unicdbdjdcd{\iota}})}\unicdbdjdcd{o}} .  {({\unicdcdaddd x : {{\iota}\unicdbdjdcd{\iota}} .  {{{P}~{x}}\unicdcdcdhd{{Q}~{x}}}})}\\
\unicdbdjdcd{\unicdcdadad p : {o} .  {{({\unicdcdadad x : {{\iota}\unicdbdjdcd{\iota}} .  {{{P}~{x}}\unicdbdjdcd{{{Q}~{x}}\unicdbdjdcd{p}}}})}\unicdbdjdcd{p}}}.
\end{array}
$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & c3e995324746e718ab713bbf6a225f342b11f85e44af87041c25e67c26eea74b \\
Pure Prop Address: & TMRys3KSWGA2LC5vfb7h5HsWi6UReHYFA4A \\
Theory Prop Id: & ed9d65f783165c1844de5ef6e565738ab285fb760e976e5b2a4a0aaea6db676a \\
Theory Prop Address: & TMJjeW58a6DARdGUxoyLGC7KDSF7e5NyVkz
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
exandE_iii
\end{verbatim}
\begin{theorem}\label{thm:fgihbgogegfepfjgjgjg}
$$
\begin{array}{c}
\unicdcdadad P Q : {{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}})}\unicdbdjdcd{o}} .  {({\unicdcdaddd x : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}} .  {{{P}~{x}}\unicdcdcdhd{{Q}~{x}}}})}\\
\unicdbdjdcd{\unicdcdadad p : {o} .  {{({\unicdcdadad x : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}} .  {{{P}~{x}}\unicdbdjdcd{{{Q}~{x}}\unicdbdjdcd{p}}}})}\unicdbdjdcd{p}}}.
\end{array}
$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 028a8f7f6f33f8d9071fed86dccba76e2db66b07c2f6b7330daccd1792bb2382 \\
Pure Prop Address: & TMNuTg4eH32x4XhwU5Q9dAJWP8zDQ3b8ZXC \\
Theory Prop Id: & 80b3b0d1dac86077631ca90e19efac3b726c7697bfe6eeb63b5d74a056a3d3ee \\
Theory Prop Address: & TMKrUpgWDX1Lip64jWzHGPhKdYPQ9L4XevF
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
exandE_iiii
\end{verbatim}
\begin{theorem}\label{thm:fgihbgogegfepfjgjgjgjg}
$$
\begin{array}{c}
\unicdcdadad P Q : {{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}})}\unicdbdjdcd{o}} .  {({\unicdcdaddd x : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}} .  {{{P}~{x}}\unicdcdcdhd{{Q}~{x}}}})}\\
\unicdbdjdcd{\unicdcdadad p : {o} .  {{({\unicdcdadad x : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}} .  {{{P}~{x}}\unicdbdjdcd{{{Q}~{x}}\unicdbdjdcd{p}}}})}\unicdbdjdcd{p}}}.
\end{array}
$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 7807d4121dc1d8d66fac47e62c634706453ae9f2acfb88ce1adf46eedfce6b57 \\
Pure Prop Address: & TMPCN5CQwhpCx9SEJcLXFz7VTi2HpDCvNie \\
Theory Prop Id: & d1536a49224a1dfb03981a17133a78f7a7384d730d0fea9ee123ba6b7a9eee92 \\
Theory Prop Address: & TMNR9cr6cmoDmVuobFG1uP3pM5DqVkVGcfe
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
exandE_iio
\end{verbatim}
\begin{theorem}\label{thm:fgihbgogegfepfjgjgpg} $$
\begin{array}{c}
\unicdcdadad P Q : {{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}})}\unicdbdjdcd{o}} .  {({\unicdcdaddd x : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  {{{P}~{x}}\unicdcdcdhd{{Q}~{x}}}})}\\
\unicdbdjdcd{\unicdcdadad p : {o} .  {{({\unicdcdadad x : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  {{{P}~{x}}\unicdbdjdcd{{{Q}~{x}}\unicdbdjdcd{p}}}})}\unicdbdjdcd{p}}}.
\end{array}
$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 86782c60904be2e5e01ea093b9564a62c5d7b5c5248e75598e84cda4eaff6db1 \\
Pure Prop Address: & TMU81hY5npesCwKcB8HT2xq4ju8aURKMfbk \\
Theory Prop Id: & 9e40e24a95644e50b58d83354186c23bf455543eef7af35f3dcfdf02d9c6ef87 \\
Theory Prop Address: & TMZrs5GwEKYE1pY5Ctt2Fz9smjaQEZ5RQyx
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
exandE_iiio
\end{verbatim}
\begin{theorem}\label{thm:fgihbgogegfepfjgjgjgpg}
$$\begin{array}{c}
\unicdcdadad P Q : {{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}}})}\unicdbdjdcd{o}} .  {({\unicdcdaddd x : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}}} .  {{{P}~{x}}\unicdcdcdhd{{Q}~{x}}}})}\\
\unicdbdjdcd{\unicdcdadad p : {o} .  {{({\unicdcdadad x : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}}} .  {{{P}~{x}}\unicdbdjdcd{{{Q}~{x}}\unicdbdjdcd{p}}}})}\unicdbdjdcd{p}}}.
\end{array}
$$ The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & bd6e2d3ff943629d1de39214b2120452cec619ef78043f7c33b48dfd70ae31e3 \\
Pure Prop Address: & TMLJQJfu5Yt7gyzMd54gxCSHZYxdRbKTTPQ \\
Theory Prop Id: & ad03be44e266e20551e0c398f53a8d6eb2497ca6b16f6b686368373774c0e421 \\
Theory Prop Address: & TMQyqYULvp8WJD8eRf3khDrng9qgVuiu34m
\end{tabular}
\end{center}

\end{theorem}

