\chapter{Class Level Properties and Constructors}
\begin{definition}\label{def:cgjghgjgogehfgchdhfgdgeh}
We define $\mname{bigintersect}$ to be ${\uniddcgcg (D : {{({{\iota}\unicdbdjdcd{o}})}\unicdbdjdcd{o}})(x : {\iota}) . {\unicdcdadad P : {{\iota}\unicdbdjdcd{o}} .  {{{D}~{P}}\unicdbdjdcd{{P}~{x}}}}}$ 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}
\begin{definition}\label{def:chfgggmgfgihjgghfg}
We define $\mname{reflexive}$ to be ${\uniddcgcg R .  {\unicdcdadad x : {\iota} .  {{{R}~{x}}~{x}}}}$ of type ${{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}})}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 6a6dea288859e3f6bb58a32cace37ed96c35bdf6b0275b74982b243122972933 \\
Pure Object Address: & TMT7Ad5B4WrSQkBPTK8ixJeatPMtbGf5cdF \\
Theory Object Id: & a8e476299e8d33df6c6811c287e1b9fabc2185a0e461a2c739e7e02c9344377c \\
Theory Object Address: & TMUbRcXexrARoyLrg2fK8SYuYLT1wF4tnjt
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:jgchchfgggmgfgihjgghfg}
We define $\mname{irreflexive}$ to be ${\uniddcgcg R .  {\unicdcdadad x : {\iota} .  {\preoh{{{{R}~{x}}~{x}}}}}}$ of type ${{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}})}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & e2ea25bb1daaa6f56c9574c322ff417600093f1fea156f5efdcbe4a9b87e9dcf \\
Pure Object Address: & TMYbVtA5sMrdMd5HyhU7dkL61akED8Yzd4T \\
Theory Object Id: & e3b5275d1d8ea65a249223038cf102aa00ce1f82a9a8ca9a4bde7a257092a89e \\
Theory Object Address: & TMFSJ2T4un5uVsKW7djiQAvN1DAwTnNJUiC
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:dhjhngngfgehchjgdg}
We define $\mname{symmetric}$ to be ${\uniddcgcg R .  {\unicdcdadad x y : {\iota} .  {{{{R}~{x}}~{y}}\unicdbdjdcd{{{R}~{y}}~{x}}}}}$ of type ${{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}})}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 309408a91949b0fa15f2c3f34cdd5ff57cd98bb5f49b64e42eb97b4bf1ab623b \\
Pure Object Address: & TMGcxUiVbTw5fsQKQMYB8qsMsgLdrMBxa7j \\
Theory Object Id: & 120a5ebbb3c5e5ef6629806c0a1e8303ae93de2f42212d21a9ae33042777373c \\
Theory Object Address: & TMQbC5GACt2K5MgypgrbgKeZqE3KMVpjpim
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:bgogehjgdhjhngngfgehchjgdg}
We define $\mname{antisymmetric}$ to be ${\uniddcgcg R .  {\unicdcdadad x y : {\iota} .  {{{{R}~{x}}~{y}}\unicdbdjdcd{{{{R}~{y}}~{x}}\unicdbdjdcd{{x}={y}}}}}}$ of type ${{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}})}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 9a8a2beac3ecd759aebd5e91d3859dec6be35a41ec07f9aba583fb9c33b40fbe \\
Pure Object Address: & TMVbTEZn5mU4ZX9WkJ7WJ2yxJDVpXU5YAUm \\
Theory Object Id: & 82374c2974eaa40576881231e8c1e031292e0279528cee22769ae90c0d1ca574 \\
Theory Object Address: & TMNn7rfiqnuh8jbUTzq7HQitSyHk6xsoUfm
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:ehchbgogdhjgehjgghfg}
We define $\mname{transitive}$ to be ${\uniddcgcg R .  {\unicdcdadad x y z : {\iota} .  {{{{R}~{x}}~{y}}\unicdbdjdcd{{{{R}~{y}}~{z}}\unicdbdjdcd{{{R}~{x}}~{z}}}}}}$ of type ${{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}})}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & b145249bb4b36907159289e3a9066e31e94dfa5bb943fc63ff6d6ca9abab9e02 \\
Pure Object Address: & TMFM3TNU7g1EZuVHc24wspMS7Y75XqC8hvN \\
Theory Object Id: & d9f0d1487b5ca94d78a7fe0eb19e9c8bad4aad24dc543be4879ce610d5bd5c53 \\
Theory Object Address: & TMW5XFJc1g5eT257Q4ZaCqtxLhMtDWiqqty
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:fgbhchfgmgog}
We define $\mname{eqreln}$ to be ${\uniddcgcg R .  {{{{\mname{reflexive}}~{R}}\unicdcdcdhd{{\mname{symmetric}}~{R}}}\unicdcdcdhd{{\mname{transitive}}~{R}}}}$ of type ${{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}})}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 25d55803878b7ce4c199607568d5250ff00ee63629e243e2a1fd20966a3ee92c \\
Pure Object Address: & TMSuiPhKNmJUrhs9cRrAHLcqoskTttXj1fT \\
Theory Object Id: & c457d55160cd9e8319ea47367df7263cd5e391e71be5fe7a86c761faf2ab6f26 \\
Theory Object Address: & TMM8uEsESwkqXBF3DURiTCeRydaN9MdPa2n
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:ahfgch}
We define $\mname{per}$ to be ${\uniddcgcg R .  {{{\mname{symmetric}}~{R}}\unicdcdcdhd{{\mname{transitive}}~{R}}}}$ of type ${{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}})}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 5754c55c5ad43b5eaeb1fb67971026c82f41fd52267a380d6f2bb8487e4e959b \\
Pure Object Address: & TMJFMWPiZz3oFCEc6qbqK6ewA1Vd1h48BRr \\
Theory Object Id: & 2688d14197e49ace4c9134d31466ccf7c821723681dd3c0a8e19f30828b6e69b \\
Theory Object Address: & TMZ1qY6E5fsXqNMWYcwbbpUKqq24VbUFKZN
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:mgjgogfgbgch}
We define $\mname{linear}$ to be ${\uniddcgcg R .  {\unicdcdadad x y : {\iota} .  {{{{R}~{x}}~{y}}\unicdcdcdid{{{R}~{y}}~{x}}}}}$ of type ${{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}})}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 9db35ff1491b528184e71402ab4646334daef44c462a5c04ab2c952037a84f3f \\
Pure Object Address: & TMaYw74DvBqB1nULY5YzEwuZZL4wkaUyyxg \\
Theory Object Id: & 04b95b0ad1550900eb8cea4a13f9a204f7ee4ade8f078352bfea612b8b08bc4b \\
Theory Object Address: & TMYics8vs8zP2a85EMxEbQ7v2qa88dpRPxV
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:ehchjgdgigpgehpgngpgfhdhpfpgch}
We define $\mname{trichotomous\_or}$ to be ${\uniddcgcg R .  {\unicdcdadad x y : {\iota} .  {{{{{R}~{x}}~{y}}\unicdcdcdid{{x}={y}}}\unicdcdcdid{{{R}~{y}}~{x}}}}}$ of type ${{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}})}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & cc2c175bc9d6b3633a1f1084c35556110b83d269ebee07a3df3f71e3af4f8338 \\
Pure Object Address: & TMWfJY8TrCuqdBbXjXtyyPgdMaJFFhSYPxa \\
Theory Object Id: & 61a1215cd148d58b01ffff5d1f427041f8684c948585f39446780cb2f09332f5 \\
Theory Object Address: & TMShCrFwwqitm33uX4Zfg5LP3nxx3wiWms6
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:ahbgchehjgbgmgpgchegfgch}
We define $\mname{partialorder}$ to be ${\uniddcgcg R .  {{{{\mname{reflexive}}~{R}}\unicdcdcdhd{{\mname{antisymmetric}}~{R}}}\unicdcdcdhd{{\mname{transitive}}~{R}}}}$ of type ${{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}})}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 406b89b059127ed670c6985bd5f9a204a2d3bc3bdc624694c06119811f439421 \\
Pure Object Address: & TMW2bk6NEbDRdxmx9iWTp8eEaq5Bqs8wPgv \\
Theory Object Id: & c6fcf7ac241b0cf0da35ccb0b15e5793c002ba2e047a608000d69fd9887f713f \\
Theory Object Address: & TMbQ7jLDSWGqbR63ibKa1g9z7w1VxQwMmpi
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:ehpgehbgmgpgchegfgch}
We define $\mname{totalorder}$ to be ${\uniddcgcg R .  {{{\mname{partialorder}}~{R}}\unicdcdcdhd{{\mname{linear}}~{R}}}}$ of type ${{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}})}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 0e5ab00c10f017772d0d2cc2208e71a537fa4599590204be721685b72b5d213f \\
Pure Object Address: & TMKx8GCXERU42pBKUXaDWCBbgA3pQMRP8tN \\
Theory Object Id: & f82fe6af52f2eb7dba22be27f833973c1fc595caf2ed9e8d39761e844f892c7f \\
Theory Object Address: & TMdPhbDwqcJQrVhsNYionDKzTcsQAEnNsVD
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:dhehchjgdgehahbgchehjgbgmgpgchegfgch}
We define $\mname{strictpartialorder}$ to be ${\uniddcgcg R .  {{{\mname{irreflexive}}~{R}}\unicdcdcdhd{{\mname{transitive}}~{R}}}}$ of type ${{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}})}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & ee5d8d94a19e756967ad78f3921cd249bb4aefc510ede4b798f8aa02c5087dfa \\
Pure Object Address: & TMKCFjFsuHbvaNUnpivHQWRNoRicsnmAMxK \\
Theory Object Id: & c5200681a8c27017c79f5fdf3f12ab2bccac1fae4bdbf8e1fda11162db118256 \\
Theory Object Address: & TMUM3ZcpFdPNXn5zGKLbrqdF1jPboSGWNuB
\end{tabular}
\end{center}

\end{definition}
\begin{definition}\label{def:dhehchjgdgehehpgehbgmgpgchegfgch}
We define $\mname{stricttotalorder}$ to be ${\uniddcgcg R .  {{{\mname{strictpartialorder}}~{R}}\unicdcdcdhd{{\mname{trichotomous\_or}}~{R}}}}$ of type ${{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}})}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 42a3bcd22900658b0ec7c4bbc765649ccf2b1b5641760fc62cf8a6a6220cbc47 \\
Pure Object Address: & TMUQBjSjcsVDhSC7wkbaDUwYx5frU3mzZYL \\
Theory Object Id: & fc46b3ff515f15dc7d235be5f2ed71d758b31a1c27552cfb9c6a33f42d1a3a4f \\
Theory Object Address: & TMJjLnVKzQjT4WNmmFgDZ2Wjjd3Y3FEBCBr
\end{tabular}
\end{center}

\end{definition}
\begin{theorem}\label{thm:ahfgchpfdhjhng} ${\unicdcdadad R : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  {{{\mname{per}}~{R}}\unicdbdjdcd{{\mname{symmetric}}~{R}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 79f95ef7f3d535d6717f7ddc757df9b5e552d3ce9b4bdfb2e6a7fe0937c98439 \\
Pure Prop Address: & TMHJHazkkUfb6aCs84p71oZHrkAA9SrRF6B \\
Theory Prop Id: & 9c47256c1ffdf0d6543ef86bbda771b7500ac846168ef7cd276fefdf6ae54a1f \\
Theory Prop Address: & TMGvYGQrs8TGK53ZwpRhhXKcriX4siG4aWK
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ahfgchpfehchbg} ${\unicdcdadad R : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  {{{\mname{per}}~{R}}\unicdbdjdcd{{\mname{transitive}}~{R}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 607d155b87eb1945d8bd159974a5bd7062c2dea047295c027068baf6d81c8994 \\
Pure Prop Address: & TMPq6w6Ar2UhxZJQGGLkL7M9a8YzYHyjaEw \\
Theory Prop Id: & 8ce50de71d645606be80665db71c58b8813cd0d19d60d8b763ffc406b2efe6e4 \\
Theory Prop Address: & TMXqAeANVNhbDDSZf3ThqJh57d5d8akrVuU
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ahfgchpfdhehchbgbd} ${\unicdcdadad R : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  {{{\mname{per}}~{R}}\unicdbdjdcd{\unicdcdadad x y z : {\iota} .  {{{{R}~{y}}~{x}}\unicdbdjdcd{{{{R}~{y}}~{z}}\unicdbdjdcd{{{R}~{x}}~{z}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 25c6c513d28204a6d67aec12f103a90010140f5c065ee6e81a2a235388669203 \\
Pure Prop Address: & TMH8vH9JbJk1oRxfLTaWkXDsdp1tBajpRuU \\
Theory Prop Id: & 7450d4de2a0dc28afe52b779285309d8272e4ecc9d18b29694db6d0e88c2c70e \\
Theory Prop Address: & TMWwhnqMzeuBU4txn9M7KbX32G2MYUsYXWX
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ahfgchpfdhehchbgcd} ${\unicdcdadad R : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  {{{\mname{per}}~{R}}\unicdbdjdcd{\unicdcdadad x y z : {\iota} .  {{{{R}~{x}}~{y}}\unicdbdjdcd{{{{R}~{z}}~{y}}\unicdbdjdcd{{{R}~{x}}~{z}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 42041dce9407f5e451a83275d4ed3562d50e979b371ac9cfc9ce2bbf65ffb11b \\
Pure Prop Address: & TMczKpKZoBa6ULrfgZpdRBj5NNSBdUXVrmD \\
Theory Prop Id: & c1c6a191a79810f500d658f41a2be9542a0355f4071cdcddc0e1aca07f3db296 \\
Theory Prop Address: & TMYhQJwgjHAdPXsFBVaSDYV1rJZ3eh8ERrF
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ahfgchpfdhehchbgdd} ${\unicdcdadad R : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  {{{\mname{per}}~{R}}\unicdbdjdcd{\unicdcdadad x y z : {\iota} .  {{{{R}~{y}}~{x}}\unicdbdjdcd{{{{R}~{z}}~{y}}\unicdbdjdcd{{{R}~{x}}~{z}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d7b95260b2573ec1f7c5e60368e6752db7fa181ff7cfcb71c4f345b0bb109dd7 \\
Pure Prop Address: & TMGmGZb54Qqh3fp8xP84i6ikrSsAZHtQrK2 \\
Theory Prop Id: & 21217c9c11e8e6fc8b65cd0e9e3a540900e413d26333d881e5c72b28ed682b59 \\
Theory Prop Address: & TMR85C3Y3ZcsxRT7X96TVb5FfvijohyYrhB
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ahfgchpfchfgggbd} ${\unicdcdadad R : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  {{{\mname{per}}~{R}}\unicdbdjdcd{\unicdcdadad x y : {\iota} .  {{{{R}~{x}}~{y}}\unicdbdjdcd{{{R}~{x}}~{x}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & c9ce8823077b6bac6fe963cb5c95ed848be8455934bbdab468e7fd51a1b26027 \\
Pure Prop Address: & TMdPMQFgkvEnLZgXHL1Y1PTzuAK9GLNXFGi \\
Theory Prop Id: & 45e4c5e058614a4b8b7d87bd59727e65f215a29fc3061feeb56cde8a17916335 \\
Theory Prop Address: & TMTZp74GpF3FnWhQACszYMqVy96d8NVbFXr
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ahfgchpfchfgggcd} ${\unicdcdadad R : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  {{{\mname{per}}~{R}}\unicdbdjdcd{\unicdcdadad x y : {\iota} .  {{{{R}~{x}}~{y}}\unicdbdjdcd{{{R}~{y}}~{y}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & bbc879269d0205d16beaa6eee6fd30afbcdffa8cec1ac7f6b3b8d26e715d2345 \\
Pure Prop Address: & TMbvg6t3f8pBbTLcBciLrre2aCKoFw7zfno \\
Theory Prop Id: & 5755e01c047ecd7f625b9e98dc3a6c0651bc16c7c536503e8732f0ecc467f80d \\
Theory Prop Address: & TMLeJkqhNb5gsQPB2bsXFJnDEF5uSEmMFUv
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:ahbgchehjgbgmgpgchegfgchpfdhehchjgdgehahbgchehjgbgmgpgchegfgch} ${\unicdcdadad R : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  {{{\mname{partialorder}}~{R}}\unicdbdjdcd{{\mname{strictpartialorder}}~{({\uniddcgcg x y .  {{{{R}~{x}}~{y}}\unicdcdcdhd{{x}\unicdcdgdad{y}}}})}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 6d855f41855d31ad7129a125faa7f0b81aed14cfe4b95537164fbea0352b7169 \\
Pure Prop Address: & TMGDbQFv1xTKnLt1axDcGD9skkrk1NDjguy \\
Theory Prop Id: & f2be7026be53a9cc86a061447a9845aea99c3af1fd7b0e0a1be19f93eac40826 \\
Theory Prop Address: & TMW6QAQXciNiq23bCcarz6nxhYqvHh8imu8
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:chfgggmgdgmgpgdh}
We define $\mname{reflclos}$ to be ${\uniddcgcg R x y .  {{{{R}~{x}}~{y}}\unicdcdcdid{{x}={y}}}}$ of type ${{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}})}\unicdbdjdcd{({{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}})}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 71bff9a6ef1b13bbb1d24f9665cde6df41325f634491be19e3910bc2e308fa29 \\
Pure Object Address: & TMT2htU1EHitc1tMVfJYMWKQyBmwmD6rtWn \\
Theory Object Id: & 231a7bacb9df61407922150b01fd5a8408982ba28cc53a7b1116373732b564e5 \\
Theory Object Address: & TMUaCQBAHyUetsLgqr9moZkwAZ6DHmvevzv
\end{tabular}
\end{center}

\end{definition}
\begin{theorem}\label{thm:chfgggmgdgmgpgdhpfchfgggmg} ${\unicdcdadad R : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  {{\mname{reflexive}}~{({{\mname{reflclos}}~{R}})}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 04de27b34b8ee3720731f1aa3b07e08c79a5f5fe35b989e0e31c85df7d76188b \\
Pure Prop Address: & TMRXSNELTTP8r956vacXYEerEnidnHV3YDx \\
Theory Prop Id: & 073a437b4c2e1d6de20d186d3a62ccd4fbe468541fc10b5301ffbd1460aebad2 \\
Theory Prop Address: & TMcjRsdk3p8hhg3NaZJTez4aiFcKytNSMzj
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:chfgggmgdgmgpgdhpfngjgog} ${\unicdcdadad R S : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  {{{R} \subseteq {S}}\unicdbdjdcd{{{\mname{reflexive}}~{S}}\unicdbdjdcd{{{\mname{reflclos}}~{R}} \subseteq {S}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 3c9bfea39a96499adf86a25b70a01d86dda56919bef77987d48bd540eeb47105 \\
Pure Prop Address: & TMdFsDfTaJ75o8jviDeot8gUFggEbgrSQk9 \\
Theory Prop Id: & c6c85f19b2d660c314da672cf7ec92b47ac92205119f6d34f6f8d78bae7eb2aa \\
Theory Prop Address: & TMbsP4tFMHwzMtNmcrDFHkzc6XuNP7FvzeF
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:dhehchjgdgehahbgchehjgbgmgpgchegfgchpfahbgchehjgbgmgpgchegfgchpfchfgggmgdgmgpgdh} ${\unicdcdadad R : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  {{{\mname{strictpartialorder}}~{R}}\unicdbdjdcd{{\mname{partialorder}}~{({{\mname{reflclos}}~{R}})}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & aae20a4db679340a3b3489212833014ae04ff05454150367d01c07193f0b3f6e \\
Pure Prop Address: & TMRH8GAJvU7QCQVeMCvrdQxYzWTt23ioYvb \\
Theory Prop Id: & 8909d872000d95634b270e22a50ab08882a2efd39862ee4dc9372226770395f5 \\
Theory Prop Address: & TMMc6BxYynTzGhkvf3wwkqL4XNB328wz9Kc
\end{tabular}
\end{center}

\end{theorem}
\begin{theorem}\label{thm:dhehchjgdgehehpgehbgmgpgchegfgchpfehpgehbgmgpgchegfgchpfchfgggmgdgmgpgdh} ${\unicdcdadad R : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}} .  {{{\mname{stricttotalorder}}~{R}}\unicdbdjdcd{{\mname{totalorder}}~{({{\mname{reflclos}}~{R}})}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 76031124f76b48f04bc4f4bef1b143e3db985fab98172116e9eb3b62c7a65a54 \\
Pure Prop Address: & TMTpzN3QGmt1LjMzKNCWXA5CrTNPPXdsGom \\
Theory Prop Id: & 6057db1f3e57d31b555a933f5f17681a6a725f7108faaef6d41f2d8e944fd1ca \\
Theory Prop Address: & TMLi2krY1WNGGUsbxEr2fxHoJC6YZNrmfvS
\end{tabular}
\end{center}

\end{theorem}
