\documentclass{article}
\newtheorem{axiom}{Axiom}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{proposition}{Proposition}
\newtheorem{definition}{Definition}
\newtheorem{example}{Example}
\newtheorem{conjecture}{Conjecture}
\newcommand\unicdcdgdad{\not=}
\newcommand\unicdcdcdbg{\cup}
\newcommand\unicdcdbdgd{\setminus}
\newcommand\unicdcdcdjd{\cap}
\newcommand\unicdcdadad{\forall}
\newcommand\unicdbdjdcd{\Rightarrow}
\newcommand\unicdcdadjd{\notin}
\newcommand\unicdbdjded{\Leftrightarrow}
\newcommand\unicdcdcdid{\lor}
\newcommand\unicdcdcdhd{\land}
\newcommand\uniddcgcg{\lambda}
\newcommand\unicdcdaddd{\exists}
\newcommand\unicdcdidid{\not\subseteq}
\newcommand\preoh[1]{\lnot #1}
\newcommand\mname[1]{{\mathsf{#1}}}
\begin{document}
\title{thm\_2Ering\_2Ering\_\_literal\_\_11 (TMPBLUQRPJp8myZWdHq4xD6AvdSVQ4dgA5n)}
\maketitle
Let $ c\_2Ebool\_2EARB : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
{{\unicdcdadad} A\_27a .  {{{nonempty}~{A\_27a}}{\unicdbdjdcd}{{{c\_2Ebool\_2EARB}~{A\_27a}} \in {A\_27a}}}}\label{hyp:ngfgngpfdgpfcdfecgpgpgmgpfcdfebecfce}
\end{equation}
\begin{definition}\label{def:dgpfcdfengjgogpfcdfepfddee}
We define $\mname{c\_2Emin\_2E\_3D}$ to be ${{\uniddcgcg} A .  {{\uniddcgcg} x \in {A} .  {{\uniddcgcg} y \in {A} .  {{inj\_\_o}~{({{x}={y}})}}}}}$ of type ${{\iota}{\unicdbdjdcd}{\iota}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfedgpgngcgjgogpfcdfele}
We define $\mname{c\_2Ecombin\_2EK}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {{\uniddcgcg} A\_27b : {\iota} .  {({{\uniddcgcg} V0x \in {A\_27a} .  {({{\uniddcgcg} V1y \in {A\_27b} .  {V0x}})}})}}}$.
\end{definition}
Let $ ty\_2Ering\_2Ering : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
{{\unicdcdadad} A0 .  {{{nonempty}~{A0}}{\unicdbdjdcd}{{nonempty}~{({{ty\_2Ering\_2Ering}~{A0}})}}}}\label{hyp:ogfgpfehjhpfcdfechjgoghgpfcdfechjgoghg}
\end{equation}
Let $ c\_2Ering\_2Ering\_\_R0\_\_fupd : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Ering\_2Ering\_\_R0\_\_fupd~A\_27a \in \\
(((ty\_2Ering\_2Ering~A\_27a)^{{({{ty\_2Ering\_2Ering}~{A\_27a}})}})^{{({{A\_27a}^{{A\_27a}}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfechjgoghgpfcdfechjgoghgpfpfcfadpfpfggfhaheg}
\end{equation}
Let $ c\_2Ering\_2Ering\_\_RN\_\_fupd : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Ering\_2Ering\_\_RN\_\_fupd~A\_27a \in \\
(((ty\_2Ering\_2Ering~A\_27a)^{{({{ty\_2Ering\_2Ering}~{A\_27a}})}})^{{({{({{A\_27a}^{{A\_27a}}})}^{{({{A\_27a}^{{A\_27a}}})}}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfechjgoghgpfcdfechjgoghgpfpfcfoepfpfggfhaheg}
\end{equation}
Let $ c\_2Ering\_2Ering\_\_RM\_\_fupd : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Ering\_2Ering\_\_RM\_\_fupd~A\_27a \in \\
(((ty\_2Ering\_2Ering~A\_27a)^{{({{ty\_2Ering\_2Ering}~{A\_27a}})}})^{{({{({{({{A\_27a}^{{A\_27a}}})}^{{A\_27a}}})}^{{({{({{A\_27a}^{{A\_27a}}})}^{{A\_27a}}})}}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfechjgoghgpfcdfechjgoghgpfpfcfnepfpfggfhaheg}
\end{equation}
Let $ c\_2Ering\_2Ering\_\_RP\_\_fupd : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Ering\_2Ering\_\_RP\_\_fupd~A\_27a \in \\
(((ty\_2Ering\_2Ering~A\_27a)^{{({{ty\_2Ering\_2Ering}~{A\_27a}})}})^{{({{({{({{A\_27a}^{{A\_27a}}})}^{{A\_27a}}})}^{{({{({{A\_27a}^{{A\_27a}}})}^{{A\_27a}}})}}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfechjgoghgpfcdfechjgoghgpfpfcfafpfpfggfhaheg}
\end{equation}
Let $ c\_2Ering\_2Ering\_\_R1\_\_fupd : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Ering\_2Ering\_\_R1\_\_fupd~A\_27a \in \\
(((ty\_2Ering\_2Ering~A\_27a)^{{({{ty\_2Ering\_2Ering}~{A\_27a}})}})^{{({{A\_27a}^{{A\_27a}}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfechjgoghgpfcdfechjgoghgpfpfcfbdpfpfggfhaheg}
\end{equation}
Let $ c\_2Ering\_2Ering\_\_RN : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Ering\_2Ering\_\_RN~A\_27a \in ((A\_27a^{{A\_27a}})^{{({{ty\_2Ering\_2Ering}~{A\_27a}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfechjgoghgpfcdfechjgoghgpfpfcfoe}
\end{equation}
Let $ c\_2Ering\_2Ering\_\_RM : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Ering\_2Ering\_\_RM~A\_27a \in (((\\
A\_27a^{{A\_27a}})^{{A\_27a}})^{{({{ty\_2Ering\_2Ering}~{A\_27a}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfechjgoghgpfcdfechjgoghgpfpfcfne}
\end{equation}
Let $ c\_2Ering\_2Ering\_\_RP : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Ering\_2Ering\_\_RP~A\_27a \in (((\\
A\_27a^{{A\_27a}})^{{A\_27a}})^{{({{ty\_2Ering\_2Ering}~{A\_27a}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfechjgoghgpfcdfechjgoghgpfpfcfaf}
\end{equation}
Let $ c\_2Ering\_2Ering\_\_R1 : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Ering\_2Ering\_\_R1~A\_27a \in (A\_27a^{{({{ty\_2Ering\_2Ering}~{A\_27a}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfechjgoghgpfcdfechjgoghgpfpfcfbd}
\end{equation}
Let $ c\_2Ering\_2Ering\_\_R0 : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Ering\_2Ering\_\_R0~A\_27a \in (A\_27a^{{({{ty\_2Ering\_2Ering}~{A\_27a}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfechjgoghgpfcdfechjgoghgpfpfcfad}
\end{equation}
\begin{definition}\label{def:dgpfcdfengjgogpfcdfepfddeepfddeepfddfe}
We define $\mname{c\_2Emin\_2E\_3D\_3D\_3E}$ to be ${{\uniddcgcg} P \in {2} .  {{\uniddcgcg} Q \in {2} .  {{inj\_\_o}~{({{{p}~{P}}{\unicdbdjdcd}{{p}~{Q}}})}}}}$ of type ${\iota}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfecgpgpgmgpfcdfeef}
We define $\mname{c\_2Ebool\_2ET}$ to be ${({{{ap}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_3D}}~{({{2}^{{2}}})}})}}~{({{\uniddcgcg} V0x \in {2} .  {V0x}})}})}}~{({{\uniddcgcg} V1x \in {2} .  {V1x}})}})}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfecgpgpgmgpfcdfepfcdbd}
We define $\mname{c\_2Ebool\_2E\_21}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {({{\uniddcgcg} V0P \in {({{2}^{{A\_27a}}})} .  {({{{ap}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_3D}}~{({{2}^{{A\_27a}}})}})}}~{V0P}})}}~{({{\uniddcgcg} V1x \in {A\_27a} .  {\mname{c\_2Ebool\_2ET}}})}})}})}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfecgpgpgmgpfcdfepfcdgepffdde}
We define $\mname{c\_2Ebool\_2E\_2F\_5C}$ to be ${({{\uniddcgcg} V0t1 \in {2} .  {({{\uniddcgcg} V1t2 \in {2} .  {({{{ap}~{({{\mname{c\_2Ebool\_2E\_21}}~{2}})}}~{({{\uniddcgcg} V2t \in {2} .  {({{{ap}~{({{{ap}~{\mname{c\_2Emin\_2E\_3D\_3D\_3E}}}~{({{{ap}~{({{{ap}~{\mname{c\_2Emin\_2E\_3D\_3D\_3E}}}~{V0t1}})}}~{({{{ap}~{({{{ap}~{\mname{c\_2Emin\_2E\_3D\_3D\_3E}}}~{V1t2}})}}~{V2t}})}})}})}}~{V2t}})}})}})}})}})}$.
\end{definition}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}{\unicdcdadad} A\_27b .  nonempty~A\_27b{\unicdbdjdcd}(\\
{\unicdcdadad} V0x \in A\_27a .  ({\unicdcdadad} V1y \in A\_27b .  ((ap~(ap~(\mname{c\_2Ecombin\_2EK}~\\
A\_27a~A\_27b)~V0x)~V1y)=V0x)))\end{array}
\label{hyp:ehigngpfcdfedgpgngcgjgogpfcdfelepfpfefiene}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}(({\unicdcdadad} V0r \in (ty\_2Ering\_2Ering~\\
A\_27a) .  ({\unicdcdadad} V1f \in (A\_27a^{{A\_27a}}) .  ((ap~(c\_2Ering\_2Ering\_\_R0~\\
A\_27a)~(ap~(ap~(c\_2Ering\_2Ering\_\_R1\_\_fupd~A\_27a)~V1f)~V0r))=(\\
ap~(c\_2Ering\_2Ering\_\_R0~A\_27a)~V0r)))){\unicdcdcdhd}(({\unicdcdadad} V2r \in (ty\_2Ering\_2Ering~\\
A\_27a) .  ({\unicdcdadad} V3f \in (((A\_27a^{{A\_27a}})^{{A\_27a}})^{{({{({{A\_27a}^{{A\_27a}}})}^{{A\_27a}}})}}) .  \\
((ap~(c\_2Ering\_2Ering\_\_R0~A\_27a)~(ap~(ap~(c\_2Ering\_2Ering\_\_RP\_\_fupd~\\
A\_27a)~V3f)~V2r))=(ap~(c\_2Ering\_2Ering\_\_R0~A\_27a)~V2r)))){\unicdcdcdhd}((\\
{\unicdcdadad} V4r \in (ty\_2Ering\_2Ering~A\_27a) .  ({\unicdcdadad} V5f \in (((A\_27a^{{A\_27a}})^{{A\_27a}})^{{({{({{A\_27a}^{{A\_27a}}})}^{{A\_27a}}})}}) .  \\
((ap~(c\_2Ering\_2Ering\_\_R0~A\_27a)~(ap~(ap~(c\_2Ering\_2Ering\_\_RM\_\_fupd~\\
A\_27a)~V5f)~V4r))=(ap~(c\_2Ering\_2Ering\_\_R0~A\_27a)~V4r)))){\unicdcdcdhd}((\\
{\unicdcdadad} V6r \in (ty\_2Ering\_2Ering~A\_27a) .  ({\unicdcdadad} V7f \in ((A\_27a^{{A\_27a}})^{{({{A\_27a}^{{A\_27a}}})}}) .  \\
((ap~(c\_2Ering\_2Ering\_\_R0~A\_27a)~(ap~(ap~(c\_2Ering\_2Ering\_\_RN\_\_fupd~\\
A\_27a)~V7f)~V6r))=(ap~(c\_2Ering\_2Ering\_\_R0~A\_27a)~V6r)))){\unicdcdcdhd}((\\
{\unicdcdadad} V8r \in (ty\_2Ering\_2Ering~A\_27a) .  ({\unicdcdadad} V9f \in (A\_27a^{{A\_27a}}) .  \\
((ap~(c\_2Ering\_2Ering\_\_R1~A\_27a)~(ap~(ap~(c\_2Ering\_2Ering\_\_R0\_\_fupd~\\
A\_27a)~V9f)~V8r))=(ap~(c\_2Ering\_2Ering\_\_R1~A\_27a)~V8r)))){\unicdcdcdhd}((\\
{\unicdcdadad} V10r \in (ty\_2Ering\_2Ering~A\_27a) .  ({\unicdcdadad} V11f \in (((A\_27a^{{A\_27a}})^{{A\_27a}})^{{({{({{A\_27a}^{{A\_27a}}})}^{{A\_27a}}})}}) .  \\
((ap~(c\_2Ering\_2Ering\_\_R1~A\_27a)~(ap~(ap~(c\_2Ering\_2Ering\_\_RP\_\_fupd~\\
A\_27a)~V11f)~V10r))=(ap~(c\_2Ering\_2Ering\_\_R1~A\_27a)~V10r)))){\unicdcdcdhd}\\
(({\unicdcdadad} V12r \in (ty\_2Ering\_2Ering~A\_27a) .  ({\unicdcdadad} V13f \in (((A\_27a^{{A\_27a}})^{{A\_27a}})^{{({{({{A\_27a}^{{A\_27a}}})}^{{A\_27a}}})}}) .  \\
((ap~(c\_2Ering\_2Ering\_\_R1~A\_27a)~(ap~(ap~(c\_2Ering\_2Ering\_\_RM\_\_fupd~\\
A\_27a)~V13f)~V12r))=(ap~(c\_2Ering\_2Ering\_\_R1~A\_27a)~V12r)))){\unicdcdcdhd}\\
(({\unicdcdadad} V14r \in (ty\_2Ering\_2Ering~A\_27a) .  ({\unicdcdadad} V15f \in ((A\_27a^{{A\_27a}})^{{({{A\_27a}^{{A\_27a}}})}}) .  \\
((ap~(c\_2Ering\_2Ering\_\_R1~A\_27a)~(ap~(ap~(c\_2Ering\_2Ering\_\_RN\_\_fupd~\\
A\_27a)~V15f)~V14r))=(ap~(c\_2Ering\_2Ering\_\_R1~A\_27a)~V14r)))){\unicdcdcdhd}\\
(({\unicdcdadad} V16r \in (ty\_2Ering\_2Ering~A\_27a) .  ({\unicdcdadad} V17f \in (A\_27a^{{A\_27a}}) .  \\
((ap~(c\_2Ering\_2Ering\_\_RP~A\_27a)~(ap~(ap~(c\_2Ering\_2Ering\_\_R0\_\_fupd~\\
A\_27a)~V17f)~V16r))=(ap~(c\_2Ering\_2Ering\_\_RP~A\_27a)~V16r)))){\unicdcdcdhd}\\
(({\unicdcdadad} V18r \in (ty\_2Ering\_2Ering~A\_27a) .  ({\unicdcdadad} V19f \in (A\_27a^{{A\_27a}}) .  \\
((ap~(c\_2Ering\_2Ering\_\_RP~A\_27a)~(ap~(ap~(c\_2Ering\_2Ering\_\_R1\_\_fupd~\\
A\_27a)~V19f)~V18r))=(ap~(c\_2Ering\_2Ering\_\_RP~A\_27a)~V18r)))){\unicdcdcdhd}\\
(({\unicdcdadad} V20r \in (ty\_2Ering\_2Ering~A\_27a) .  ({\unicdcdadad} V21f \in (((A\_27a^{{A\_27a}})^{{A\_27a}})^{{({{({{A\_27a}^{{A\_27a}}})}^{{A\_27a}}})}}) .  \\
((ap~(c\_2Ering\_2Ering\_\_RP~A\_27a)~(ap~(ap~(c\_2Ering\_2Ering\_\_RM\_\_fupd~\\
A\_27a)~V21f)~V20r))=(ap~(c\_2Ering\_2Ering\_\_RP~A\_27a)~V20r)))){\unicdcdcdhd}\\
(({\unicdcdadad} V22r \in (ty\_2Ering\_2Ering~A\_27a) .  ({\unicdcdadad} V23f \in ((A\_27a^{{A\_27a}})^{{({{A\_27a}^{{A\_27a}}})}}) .  \\
((ap~(c\_2Ering\_2Ering\_\_RP~A\_27a)~(ap~(ap~(c\_2Ering\_2Ering\_\_RN\_\_fupd~\\
A\_27a)~V23f)~V22r))=(ap~(c\_2Ering\_2Ering\_\_RP~A\_27a)~V22r)))){\unicdcdcdhd}\\
(({\unicdcdadad} V24r \in (ty\_2Ering\_2Ering~A\_27a) .  ({\unicdcdadad} V25f \in (A\_27a^{{A\_27a}}) .  \\
((ap~(c\_2Ering\_2Ering\_\_RM~A\_27a)~(ap~(ap~(c\_2Ering\_2Ering\_\_R0\_\_fupd~\\
A\_27a)~V25f)~V24r))=(ap~(c\_2Ering\_2Ering\_\_RM~A\_27a)~V24r)))){\unicdcdcdhd}\\
(({\unicdcdadad} V26r \in (ty\_2Ering\_2Ering~A\_27a) .  ({\unicdcdadad} V27f \in (A\_27a^{{A\_27a}}) .  \\
((ap~(c\_2Ering\_2Ering\_\_RM~A\_27a)~(ap~(ap~(c\_2Ering\_2Ering\_\_R1\_\_fupd~\\
A\_27a)~V27f)~V26r))=(ap~(c\_2Ering\_2Ering\_\_RM~A\_27a)~V26r)))){\unicdcdcdhd}\\
(({\unicdcdadad} V28r \in (ty\_2Ering\_2Ering~A\_27a) .  ({\unicdcdadad} V29f \in (((A\_27a^{{A\_27a}})^{{A\_27a}})^{{({{({{A\_27a}^{{A\_27a}}})}^{{A\_27a}}})}}) .  \\
((ap~(c\_2Ering\_2Ering\_\_RM~A\_27a)~(ap~(ap~(c\_2Ering\_2Ering\_\_RP\_\_fupd~\\
A\_27a)~V29f)~V28r))=(ap~(c\_2Ering\_2Ering\_\_RM~A\_27a)~V28r)))){\unicdcdcdhd}\\
(({\unicdcdadad} V30r \in (ty\_2Ering\_2Ering~A\_27a) .  ({\unicdcdadad} V31f \in ((A\_27a^{{A\_27a}})^{{({{A\_27a}^{{A\_27a}}})}}) .  \\
((ap~(c\_2Ering\_2Ering\_\_RM~A\_27a)~(ap~(ap~(c\_2Ering\_2Ering\_\_RN\_\_fupd~\\
A\_27a)~V31f)~V30r))=(ap~(c\_2Ering\_2Ering\_\_RM~A\_27a)~V30r)))){\unicdcdcdhd}\\
(({\unicdcdadad} V32r \in (ty\_2Ering\_2Ering~A\_27a) .  ({\unicdcdadad} V33f \in (A\_27a^{{A\_27a}}) .  \\
((ap~(c\_2Ering\_2Ering\_\_RN~A\_27a)~(ap~(ap~(c\_2Ering\_2Ering\_\_R0\_\_fupd~\\
A\_27a)~V33f)~V32r))=(ap~(c\_2Ering\_2Ering\_\_RN~A\_27a)~V32r)))){\unicdcdcdhd}\\
(({\unicdcdadad} V34r \in (ty\_2Ering\_2Ering~A\_27a) .  ({\unicdcdadad} V35f \in (A\_27a^{{A\_27a}}) .  \\
((ap~(c\_2Ering\_2Ering\_\_RN~A\_27a)~(ap~(ap~(c\_2Ering\_2Ering\_\_R1\_\_fupd~\\
A\_27a)~V35f)~V34r))=(ap~(c\_2Ering\_2Ering\_\_RN~A\_27a)~V34r)))){\unicdcdcdhd}\\
(({\unicdcdadad} V36r \in (ty\_2Ering\_2Ering~A\_27a) .  ({\unicdcdadad} V37f \in (((A\_27a^{{A\_27a}})^{{A\_27a}})^{{({{({{A\_27a}^{{A\_27a}}})}^{{A\_27a}}})}}) .  \\
((ap~(c\_2Ering\_2Ering\_\_RN~A\_27a)~(ap~(ap~(c\_2Ering\_2Ering\_\_RP\_\_fupd~\\
A\_27a)~V37f)~V36r))=(ap~(c\_2Ering\_2Ering\_\_RN~A\_27a)~V36r)))){\unicdcdcdhd}\\
(({\unicdcdadad} V38r \in (ty\_2Ering\_2Ering~A\_27a) .  ({\unicdcdadad} V39f \in (((A\_27a^{{A\_27a}})^{{A\_27a}})^{{({{({{A\_27a}^{{A\_27a}}})}^{{A\_27a}}})}}) .  \\
((ap~(c\_2Ering\_2Ering\_\_RN~A\_27a)~(ap~(ap~(c\_2Ering\_2Ering\_\_RM\_\_fupd~\\
A\_27a)~V39f)~V38r))=(ap~(c\_2Ering\_2Ering\_\_RN~A\_27a)~V38r)))){\unicdcdcdhd}\\
(({\unicdcdadad} V40r \in (ty\_2Ering\_2Ering~A\_27a) .  ({\unicdcdadad} V41f \in (A\_27a^{{A\_27a}}) .  \\
((ap~(c\_2Ering\_2Ering\_\_R0~A\_27a)~(ap~(ap~(c\_2Ering\_2Ering\_\_R0\_\_fupd~\\
A\_27a)~V41f)~V40r))=(ap~V41f~(ap~(c\_2Ering\_2Ering\_\_R0~A\_27a)~V40r))))){\unicdcdcdhd}\\
(({\unicdcdadad} V42r \in (ty\_2Ering\_2Ering~A\_27a) .  ({\unicdcdadad} V43f \in (A\_27a^{{A\_27a}}) .  \\
((ap~(c\_2Ering\_2Ering\_\_R1~A\_27a)~(ap~(ap~(c\_2Ering\_2Ering\_\_R1\_\_fupd~\\
A\_27a)~V43f)~V42r))=(ap~V43f~(ap~(c\_2Ering\_2Ering\_\_R1~A\_27a)~V42r))))){\unicdcdcdhd}\\
(({\unicdcdadad} V44r \in (ty\_2Ering\_2Ering~A\_27a) .  ({\unicdcdadad} V45f \in (((A\_27a^{{A\_27a}})^{{A\_27a}})^{{({{({{A\_27a}^{{A\_27a}}})}^{{A\_27a}}})}}) .  \\
((ap~(c\_2Ering\_2Ering\_\_RP~A\_27a)~(ap~(ap~(c\_2Ering\_2Ering\_\_RP\_\_fupd~\\
A\_27a)~V45f)~V44r))=(ap~V45f~(ap~(c\_2Ering\_2Ering\_\_RP~A\_27a)~V44r))))){\unicdcdcdhd}\\
(({\unicdcdadad} V46r \in (ty\_2Ering\_2Ering~A\_27a) .  ({\unicdcdadad} V47f \in (((A\_27a^{{A\_27a}})^{{A\_27a}})^{{({{({{A\_27a}^{{A\_27a}}})}^{{A\_27a}}})}}) .  \\
((ap~(c\_2Ering\_2Ering\_\_RM~A\_27a)~(ap~(ap~(c\_2Ering\_2Ering\_\_RM\_\_fupd~\\
A\_27a)~V47f)~V46r))=(ap~V47f~(ap~(c\_2Ering\_2Ering\_\_RM~A\_27a)~V46r))))){\unicdcdcdhd}\\
({\unicdcdadad} V48r \in (ty\_2Ering\_2Ering~A\_27a) .  ({\unicdcdadad} V49f \in ((A\_27a^{{A\_27a}})^{{({{A\_27a}^{{A\_27a}}})}}) .  \\
((ap~(c\_2Ering\_2Ering\_\_RN~A\_27a)~(ap~(ap~(c\_2Ering\_2Ering\_\_RN\_\_fupd~\\
A\_27a)~V49f)~V48r))=(ap~V49f~(ap~(c\_2Ering\_2Ering\_\_RN~A\_27a)~V48r)))))))))))))))))))))))))))))\end{array}
\label{hyp:ehigngpfcdfechjgoghgpfcdfechjgoghgpfpfbgdgdgggfhahegdh}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}({\unicdcdadad} V0r1 \in (ty\_2Ering\_2Ering~\\
A\_27a) .  ({\unicdcdadad} V1r2 \in (ty\_2Ering\_2Ering~A\_27a) .  ((V0r1=V1r2){\unicdbdjded}\\
(((ap~(c\_2Ering\_2Ering\_\_R0~A\_27a)~V0r1)=(ap~(c\_2Ering\_2Ering\_\_R0~\\
A\_27a)~V1r2)){\unicdcdcdhd}(((ap~(c\_2Ering\_2Ering\_\_R1~A\_27a)~V0r1)=(ap~(c\_2Ering\_2Ering\_\_R1~\\
A\_27a)~V1r2)){\unicdcdcdhd}(((ap~(c\_2Ering\_2Ering\_\_RP~A\_27a)~V0r1)=(ap~(c\_2Ering\_2Ering\_\_RP~\\
A\_27a)~V1r2)){\unicdcdcdhd}(((ap~(c\_2Ering\_2Ering\_\_RM~A\_27a)~V0r1)=(ap~(c\_2Ering\_2Ering\_\_RM~\\
A\_27a)~V1r2)){\unicdcdcdhd}((ap~(c\_2Ering\_2Ering\_\_RN~A\_27a)~V0r1)=(ap~(c\_2Ering\_2Ering\_\_RN~\\
A\_27a)~V1r2)))))))))\end{array}
\label{hyp:ehigngpfcdfechjgoghgpfcdfechjgoghgpfpfdgpgngahpgogfgogehpfpffgbhfhbgmgjgehjh}
\end{equation}
\begin{theorem}\label{thm:ehigngpfcdfechjgoghgpfcdfechjgoghgpfpfmgjgehfgchbgmgpfpfbdbd}
$$\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}({\unicdcdadad} V0a01 \in A\_27a .  ({\unicdcdadad} V1a1 \in \\
A\_27a .  ({\unicdcdadad} V2f11 \in ((A\_27a^{{A\_27a}})^{{A\_27a}}) .  ({\unicdcdadad} V3f01 \in (\\
(A\_27a^{{A\_27a}})^{{A\_27a}}) .  ({\unicdcdadad} V4f1 \in (A\_27a^{{A\_27a}}) .  ({\unicdcdadad} V5a02 \in \\
A\_27a .  ({\unicdcdadad} V6a2 \in A\_27a .  ({\unicdcdadad} V7f12 \in ((A\_27a^{{A\_27a}})^{{A\_27a}}) .  \\
({\unicdcdadad} V8f02 \in ((A\_27a^{{A\_27a}})^{{A\_27a}}) .  ({\unicdcdadad} V9f2 \in (A\_27a^{{A\_27a}}) .  \\
(((ap~(ap~(c\_2Ering\_2Ering\_\_R0\_\_fupd~A\_27a)~(ap~(\mname{c\_2Ecombin\_2EK}~\\
A\_27a~A\_27a)~V0a01))~(ap~(ap~(c\_2Ering\_2Ering\_\_R1\_\_fupd~A\_27a)~\\
(ap~(\mname{c\_2Ecombin\_2EK}~A\_27a~A\_27a)~V1a1))~(ap~(ap~(c\_2Ering\_2Ering\_\_RP\_\_fupd~\\
A\_27a)~(ap~(\mname{c\_2Ecombin\_2EK}~((A\_27a^{{A\_27a}})^{{A\_27a}})~((A\_27a^{{A\_27a}})^{{A\_27a}}))~\\
V2f11))~(ap~(ap~(c\_2Ering\_2Ering\_\_RM\_\_fupd~A\_27a)~(ap~(\mname{c\_2Ecombin\_2EK}~\\
((A\_27a^{{A\_27a}})^{{A\_27a}})~((A\_27a^{{A\_27a}})^{{A\_27a}}))~V3f01))~(ap~(ap~(c\_2Ering\_2Ering\_\_RN\_\_fupd~\\
A\_27a)~(ap~(\mname{c\_2Ecombin\_2EK}~(A\_27a^{{A\_27a}})~(A\_27a^{{A\_27a}}))~V4f1))~\\
(c\_2Ebool\_2EARB~(ty\_2Ering\_2Ering~A\_27a)))))))=(ap~(ap~(c\_2Ering\_2Ering\_\_R0\_\_fupd~\\
A\_27a)~(ap~(\mname{c\_2Ecombin\_2EK}~A\_27a~A\_27a)~V5a02))~(ap~(ap~(c\_2Ering\_2Ering\_\_R1\_\_fupd~\\
A\_27a)~(ap~(\mname{c\_2Ecombin\_2EK}~A\_27a~A\_27a)~V6a2))~(ap~(ap~(c\_2Ering\_2Ering\_\_RP\_\_fupd~\\
A\_27a)~(ap~(\mname{c\_2Ecombin\_2EK}~((A\_27a^{{A\_27a}})^{{A\_27a}})~((A\_27a^{{A\_27a}})^{{A\_27a}}))~\\
V7f12))~(ap~(ap~(c\_2Ering\_2Ering\_\_RM\_\_fupd~A\_27a)~(ap~(\mname{c\_2Ecombin\_2EK}~\\
((A\_27a^{{A\_27a}})^{{A\_27a}})~((A\_27a^{{A\_27a}})^{{A\_27a}}))~V8f02))~(ap~(ap~(c\_2Ering\_2Ering\_\_RN\_\_fupd~\\
A\_27a)~(ap~(\mname{c\_2Ecombin\_2EK}~(A\_27a^{{A\_27a}})~(A\_27a^{{A\_27a}}))~V9f2))~\\
(c\_2Ebool\_2EARB~(ty\_2Ering\_2Ering~A\_27a)))))))){\unicdbdjded}((V0a01=V5a02){\unicdcdcdhd}\\
((V1a1=V6a2){\unicdcdcdhd}((V2f11=V7f12){\unicdcdcdhd}((V3f01=V8f02){\unicdcdcdhd}(V4f1=V9f2))))))))))))))))\end{array}$$
\end{theorem}
\end{document}
