\begin{definition}\label{def:dgbgogpgogjgdgbgmgpffgmgeh}
$\mname{canonical\_elt}$ is the opaque object of type ${{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}})}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 24615c6078840ea77a483098ef7fecf7d2e10585bf1f31bd0c61fbaeced3ecb8 \\
Pure Object Address: & TMTxaocPHR7KaoAb7prHbkajsp6MUfshdsg \\
Theory Object Id: & a18d95a2ab34761092101861924b9134534850495d74fd75a2443135e945ea6f \\
Theory Object Address: & TMTEe99JMMf634KDuVmQ44i85VxLmTHvB9y
\end{tabular}
\end{center}

\end{definition}
\begin{theorem}\label{thm:dgbgogpgogjgdgbgmgpffgmgehpfchfgmg} ${\unicdcdadad R : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  {\unicdcdadad x : {\iota} .  {{{{R}~{x}}~{x}}\unicdbdjdcd{{{R}~{x}}~{({{{\mname{canonical\_elt}}~{R}}~{x}})}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 409f7f93609b8bbc78e9b27c91b8e8b15d16e673c0445c98fe5cbae6fe93e350 \\
Pure Prop Address: & TMQQtrdvb5MuDAgqNkxaL8Yxdiut4fDtB6a \\
Theory Prop Id: & a82ff2dd9b739269814be3b2b90d4dcd5d7e5f49fd6fa941daaf8f2fac8b7e4b \\
Theory Prop Address: & TMahFABoX7qUN4TKbs8SxWDdavcsNyazvny
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:dgbgogpgogjgdgbgmgpffgmgehpffgbh} ${\unicdcdadad R : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  {{{\mname{per}}~{R}}\unicdbdjdcd{\unicdcdadad x y : {\iota} .  {{{{R}~{x}}~{y}}\unicdbdjdcd{{{{\mname{canonical\_elt}}~{R}}~{x}}={{{\mname{canonical\_elt}}~{R}}~{y}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 77a0bb710d7f6fd22c2038b8e8a7aa53cb38b8625399eda5a768a92f86f94529 \\
Pure Prop Address: & TMNGDho8FciVfUN7CiWcH22sTikdZ3nEXxy \\
Theory Prop Id: & a3a6535b47fa636b2a37d0fd9d2cbc572ab41c638fc41180620163a965a862a9 \\
Theory Prop Address: & TMPA9JRmixkhj8Ft97qJcZE9RMXboWNNtQA
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:dgbgogpgogjgdgbgmgpffgmgehpfjgegfgng} ${\unicdcdadad R : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  {{{\mname{per}}~{R}}\unicdbdjdcd{\unicdcdadad x : {\iota} .  {{{{R}~{x}}~{x}}\unicdbdjdcd{{{{\mname{canonical\_elt}}~{R}}~{x}}={{{\mname{canonical\_elt}}~{R}}~{({{{\mname{canonical\_elt}}~{R}}~{x}})}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f360e8148073fe4e1c4b5a43fcb23f3a4230874ab3afbbbea65f8ac02b0385d5 \\
Pure Prop Address: & TMGnsgqbHzSxjuur9NxxHHErkCtdk6tipsC \\
Theory Prop Id: & 0881fbf40b7b603f1f612763b2238f0020aa675fdfbc4d16389c60ebcc4735ed \\
Theory Prop Address: & TMNx4jXjzYQJoqNMEri4pBsyV3LhSvqYYqt
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:bhfhpgehjgfgogeh}
$\mname{quotient}$ is the opaque object of type ${{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}})}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 185d8f16b44939deb8995cbb9be7d1b78b78d5fc4049043a3b6ccc9ec7b33b41 \\
Pure Object Address: & TMQgacYA6wSdteHEaGGZB5pfV8odVjnD3Ld \\
Theory Object Id: & eceb7632185ce5062420ae1f8b27cdcf062b7c243c6d9b7856e5e2a4e937e2af \\
Theory Object Address: & TMdVzy3y6H8DfNQEHsaYmphZTWHJpPCs1dv
\end{tabular}
\end{center}

\end{definition}
\begin{theorem}\label{thm:bhfhpgehjgfgogehpfahchpgahbd} ${\unicdcdadad R : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  {\unicdcdadad x : {\iota} .  {{{{\mname{quotient}}~{R}}~{x}}\unicdbdjdcd{{{R}~{x}}~{x}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & c9cf06df33dd5d9e1508e9c920dbee7c4fbe3ac5ca1796506c238279d7024d76 \\
Pure Prop Address: & TMEpRYaApsS9NBgYkPfxvKjtbKoMxckLJkg \\
Theory Prop Id: & 8eea9432bbf60de4e1871846f2697db36eb0c3579081190809f73c887aa8932c \\
Theory Prop Address: & TMHSpwoRWkRrT199Pr4Zw6NBfBmFt5FaZDd
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:bhfhpgehjgfgogehpfahchpgahcd} ${\unicdcdadad R : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  {{{\mname{per}}~{R}}\unicdbdjdcd{\unicdcdadad x y : {\iota} .  {{{{\mname{quotient}}~{R}}~{x}}\unicdbdjdcd{{{{\mname{quotient}}~{R}}~{y}}\unicdbdjdcd{{{{R}~{x}}~{y}}\unicdbdjdcd{{x}={y}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 54b14f4b32c6d1e65fbf61514c95ad09fa776454efdf44259705e3654a8de198 \\
Pure Prop Address: & TMWEzaUyoSBC2cv5ikpYBmh1Wxg9bwCWMaW \\
Theory Prop Id: & c5f241148436a9448eb8c5fe8b100b16191b8a22b99dbbc971e37dd9e6442a9c \\
Theory Prop Address: & TMSQAtmzR5PbKfWrMfYzL1xj4QFSrYQWPLq
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:dgbgogpgogjgdgbgmgpffgmgehpfegfggg}
$\mname{canonical\_elt\_def}$ is the opaque object of type ${{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}})}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{\iota}})}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & cd4f601256fbe0285d49ded42c4f554df32a64182e0242462437212fe90b44cd \\
Pure Object Address: & TMXTWshnbJ4phtQfmjt8rT3VUcaRS5EkRgM \\
Theory Object Id: & c6ce994fa2a7c7d9b9936df4d487c851d3b5a14f9d5b842e6d7950167473ab6e \\
Theory Object Address: & TMZLpA4pBtPQmtYCGc2fcZVLLXtrZbwNRz2
\end{tabular}
\end{center}

\end{definition}
\begin{theorem}\label{thm:dgbgogpgogjgdgbgmgpffgmgehpfegfgggpfchfgmg} ${\unicdcdadad R : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  {\unicdcdadad d : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad x : {\iota} .  {{{{R}~{x}}~{x}}\unicdbdjdcd{{{R}~{x}}~{({{{{\mname{canonical\_elt\_def}}~{R}}~{d}}~{x}})}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 427d7106df945e01d1e010f6b5f54619d5e305852962b29fd074411773f7a5fb \\
Pure Prop Address: & TMQseUYfkBpoXqbKv8vXzWb7zmRmZGRt6ho \\
Theory Prop Id: & ba911f1fb82909fa0343a89423fd8007a1eea7266f3a64d4f344fc4454b45e97 \\
Theory Prop Address: & TMSAmmXFWnmPQSVvG6xXns5c29knAy7NoJL
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:dgbgogpgogjgdgbgmgpffgmgehpfegfgggpffgbh} ${\unicdcdadad R : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  {{{\mname{per}}~{R}}\unicdbdjdcd{\unicdcdadad d : {{\iota}\unicdbdjdcd{\iota}} .  {{({\unicdcdadad x y : {\iota} .  {{{{R}~{x}}~{y}}\unicdbdjdcd{{{d}~{x}}={{d}~{y}}}}})}\unicdbdjdcd{\unicdcdadad x y : {\iota} .  {{{{R}~{x}}~{y}}\unicdbdjdcd{{{{{\mname{canonical\_elt\_def}}~{R}}~{d}}~{x}}={{{{\mname{canonical\_elt\_def}}~{R}}~{d}}~{y}}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 08b2b96ed66c9cf40b455864a9805316a228566ea2f3dee98727b4ddf6fdee29 \\
Pure Prop Address: & TMdbiHGV2yacZL1C6aVnpN4nqxmFxeFRfVh \\
Theory Prop Id: & 8b36f1b656a7909d9a962189ecd03e0e7de3681872a48796808275153f9b010f \\
Theory Prop Address: & TMQkuYZZz1p5gpefQX7a59yAUSxmoaUZ2B1
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:dgbgogpgogjgdgbgmgpffgmgehpfegfgggpfjgegfgng} ${\unicdcdadad R : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  {{{\mname{per}}~{R}}\unicdbdjdcd{\unicdcdadad d : {{\iota}\unicdbdjdcd{\iota}} .  {{({\unicdcdadad x y : {\iota} .  {{{{R}~{x}}~{y}}\unicdbdjdcd{{{d}~{x}}={{d}~{y}}}}})}\unicdbdjdcd{\unicdcdadad x : {\iota} .  {{{{R}~{x}}~{x}}\unicdbdjdcd{{{{{\mname{canonical\_elt\_def}}~{R}}~{d}}~{x}}={{{{\mname{canonical\_elt\_def}}~{R}}~{d}}~{({{{{\mname{canonical\_elt\_def}}~{R}}~{d}}~{x}})}}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 49efe82bbd3304683bf8464c2a34622dd4c9bffd857d2336f4501a2673d7d8f4 \\
Pure Prop Address: & TMFnpUHvtfsuux3kkiYp7792SjHSqdtGr2C \\
Theory Prop Id: & c305bfd1e77d91b812fe3dc8843e58279f1bb98be2cbbed8b4fedf7a73f5d6ef \\
Theory Prop Address: & TMKtsdWDnNkcBLMACntcRypwVFCS39wBpEg
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:bhfhpgehjgfgogehpfegfggg}
$\mname{quotient\_def}$ is the opaque object of type ${{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}})}\unicdbdjdcd{{({{\iota}\unicdbdjdcd{\iota}})}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 612d4b4fd0d22dd5985c10cf0fed7eda4e18dce70710ebd2cd5e91acf3995937 \\
Pure Object Address: & TMHzGWujGt1Siv1ANFttshwyzCe6VYRGi4K \\
Theory Object Id: & b18ffb4e6bef489f8b9eecd55fec81b0c0593f62e6a1386eb07f6c9250a2d493 \\
Theory Object Address: & TMQgkTfPUbwLT8jGwoRckaDnvCcP3Vd9PPz
\end{tabular}
\end{center}

\end{definition}
\begin{theorem}\label{thm:bhfhpgehjgfgogehpfegfgggpfahchpgahad} ${\unicdcdadad R : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  {{{\mname{per}}~{R}}\unicdbdjdcd{\unicdcdadad d : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad x : {\iota} .  {{{{R}~{x}}~{({{d}~{x}})}}\unicdbdjdcd{{{x}={{d}~{x}}}\unicdbdjdcd{{{{\mname{quotient\_def}}~{R}}~{d}}~{x}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & b6730b9da18d165aefaece5098a92db470398156beb51a1a0c1278d4e36152dc \\
Pure Prop Address: & TMVu99E7LXXZ91pqY2xzxjzevyHiyRuDk2L \\
Theory Prop Id: & 1e2c729d64e136e7b405ff57ee6ac780a1b626f5f145e0dc7b9f1d1c894c154b \\
Theory Prop Address: & TMUnYQqkYvFzvC8Rsud6AfF4JJ7DqXnWQxo
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:bhfhpgehjgfgogehpfegfgggpfahchpgahbd} ${\unicdcdadad R : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  {\unicdcdadad d : {{\iota}\unicdbdjdcd{\iota}} .  {\unicdcdadad x : {\iota} .  {{{{{\mname{quotient\_def}}~{R}}~{d}}~{x}}\unicdbdjdcd{{{R}~{x}}~{x}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 96ac55830548884573f3e141434b062bf9a4c5864092d3e70136808df96b01ad \\
Pure Prop Address: & TMXLZPFcYNs9m56G1QCx9QktiHeUscd41Rw \\
Theory Prop Id: & 0ba02cd229346ac664fd2fadc979d704d3e12575ce6ce56adbcbe00e2e55b9db \\
Theory Prop Address: & TMT4xAb2VRQxAVPG9ZG39hM8kN2w5vHWSNB
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:bhfhpgehjgfgogehpfegfgggpfahchpgahcd} ${\unicdcdadad R : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  {{{\mname{per}}~{R}}\unicdbdjdcd{\unicdcdadad d : {{\iota}\unicdbdjdcd{\iota}} .  {{({\unicdcdadad x y : {\iota} .  {{{{R}~{x}}~{y}}\unicdbdjdcd{{{d}~{x}}={{d}~{y}}}}})}\unicdbdjdcd{\unicdcdadad x y : {\iota} .  {{{{{\mname{quotient\_def}}~{R}}~{d}}~{x}}\unicdbdjdcd{{{{{\mname{quotient\_def}}~{R}}~{d}}~{y}}\unicdbdjdcd{{{{R}~{x}}~{y}}\unicdbdjdcd{{x}={y}}}}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & fd0707aa86d2b360392ba2fdfe2a63261a390d4e8aa5535320c6e57d0b01996e \\
Pure Prop Address: & TMU2h1hwqUi1KnjLzjZCzhLM9nK9DZmiDRP \\
Theory Prop Id: & 0dc38ca2997b0761433b4fc94c031c565be7652963fd19f4257dd60e41928762 \\
Theory Prop Address: & TMNeKehn9tffwmMaonuDau88ErbSbo4Wzam
\end{tabular}
\end{center}

\end{theorem}
