\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\_2Eupdate\_2ELIST\_\_UPDATE\_\_THMS (TMbHRfVrBup94F6NUaYkWxa9Vs5FaVyLnsh)}
\maketitle
\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: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}
Let $ ty\_2Elist\_2Elist : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
{{\unicdcdadad} A0 .  {{{nonempty}~{A0}}{\unicdbdjdcd}{{nonempty}~{({{ty\_2Elist\_2Elist}~{A0}})}}}}\label{hyp:ogfgpfehjhpfcdfemgjgdhehpfcdfemgjgdheh}
\end{equation}
Let $ c\_2Elist\_2EAPPEND : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Elist\_2EAPPEND~A\_27a \in (((ty\_2Elist\_2Elist~\\
A\_27a)^{{({{ty\_2Elist\_2Elist}~{A\_27a}})}})^{{({{ty\_2Elist\_2Elist}~{A\_27a}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfemgjgdhehpfcdfebeafaffeoeee}
\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}
Let $ c\_2Elist\_2ESNOC : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Elist\_2ESNOC~A\_27a \in (((ty\_2Elist\_2Elist~\\
A\_27a)^{{({{ty\_2Elist\_2Elist}~{A\_27a}})}})^{{A\_27a}})\end{array}
\label{hyp:ngfgngpfdgpfcdfemgjgdhehpfcdfedfoepede}
\end{equation}
\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}
Let $ ty\_2Epair\_2Eprod : {{\iota}{\unicdbdjdcd}{{\iota}{\unicdbdjdcd}{\iota}}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A0 .  nonempty~A0{\unicdbdjdcd}{\unicdcdadad} A1 .  nonempty~A1{\unicdbdjdcd}nonempty~(ty\_2Epair\_2Eprod~\\
A0~A1)\end{array}
\label{hyp:ogfgpfehjhpfcdfeahbgjgchpfcdfeahchpgeg}
\end{equation}
Let $ c\_2Epair\_2EABS\_\_prod : {{\iota}{\unicdbdjdcd}{{\iota}{\unicdbdjdcd}{\iota}}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}{\unicdcdadad} A\_27b .  nonempty~A\_27b{\unicdbdjdcd}c\_2Epair\_2EABS\_\_prod~\\
A\_27a~A\_27b \in ((ty\_2Epair\_2Eprod~A\_27a~A\_27b)^{{({{({{2}^{{A\_27b}}})}^{{A\_27a}}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfeahbgjgchpfcdfebecedfpfpfahchpgeg}
\end{equation}
\begin{definition}\label{def:dgpfcdfeahbgjgchpfcdfepfcdde}
We define $\mname{c\_2Epair\_2E\_2C}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {{\uniddcgcg} A\_27b : {\iota} .  {{\uniddcgcg} V0x \in {A\_27a} .  {{\uniddcgcg} V1y \in {A\_27b} .  {({{{ap}~{({{{c\_2Epair\_2EABS\_\_prod}~{A\_27a}}~{A\_27b}})}}~{({{\uniddcgcg} V2a \in {A\_27a} .  {({{\uniddcgcg} V3b \in {A\_27b} .  {({{{ap}~{({{{ap}~{\mname{c\_2Ebool\_2E\_2F\_5C}}}~{({{{ap}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_3D}}~{A\_27a}})}}~{V2a}})}}~{V0x}})}})}}~{({{{ap}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_3D}}~{A\_27b}})}}~{V3b}})}}~{V1y}})}})}})}})}})}}}}}$.
\end{definition}
Let $ c\_2Epair\_2ESND : {{\iota}{\unicdbdjdcd}{{\iota}{\unicdbdjdcd}{\iota}}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}{\unicdcdadad} A\_27b .  nonempty~A\_27b{\unicdbdjdcd}c\_2Epair\_2ESND~\\
A\_27a~A\_27b \in (A\_27b^{{({{{ty\_2Epair\_2Eprod}~{A\_27a}}~{A\_27b}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfeahbgjgchpfcdfedfoeee}
\end{equation}
Let $ c\_2Epair\_2EFST : {{\iota}{\unicdbdjdcd}{{\iota}{\unicdbdjdcd}{\iota}}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}{\unicdcdadad} A\_27b .  nonempty~A\_27b{\unicdbdjdcd}c\_2Epair\_2EFST~\\
A\_27a~A\_27b \in (A\_27a^{{({{{ty\_2Epair\_2Eprod}~{A\_27a}}~{A\_27b}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfeahbgjgchpfcdfegedfef}
\end{equation}
\begin{definition}\label{def:dgpfcdfecgpgpgmgpfcdfege}
We define $\mname{c\_2Ebool\_2EF}$ to be ${({{{ap}~{({{\mname{c\_2Ebool\_2E\_21}}~{2}})}}~{({{\uniddcgcg} V0t \in {2} .  {V0t}})}})}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfengjgogpfcdfepfedad}
We define $\mname{c\_2Emin\_2E\_40}$ to be ${{\uniddcgcg} A .  {{\uniddcgcg} P \in {{2}^{{A}}} .  {{\mathbf{if}}~{({{\unicdcdaddd} x \in {A} .  {{p}~{({{{ap}~{P}}~{x}})}}})}~{\mathbf{then}}~{({{the}~{({{\uniddcgcg} x .  {{{x} \in {A}}{\unicdcdcdhd}{{p}~{({{{ap}~{P}}~{x}})}}}})}})}~{\mathbf{else}}~{({{the}~{({{\uniddcgcg} x .  {{x} \in {A}}})}})}}}}$ of type ${{\iota}{\unicdbdjdcd}{\iota}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfecgpgpgmgpfcdfedepeoeee}
We define $\mname{c\_2Ebool\_2ECOND}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {({{\uniddcgcg} V0t \in {2} .  {({{\uniddcgcg} V1t1 \in {A\_27a} .  {({{\uniddcgcg} V2t2 \in {A\_27a} .  {({{{ap}~{({{\mname{c\_2Emin\_2E\_40}}~{A\_27a}})}}~{({{\uniddcgcg} V3x \in {A\_27a} .  {({{{ap}~{({{{ap}~{\mname{c\_2Ebool\_2E\_2F\_5C}}}~{({{{ap}~{({{{ap}~{\mname{c\_2Emin\_2E\_3D\_3D\_3E}}}~{({{{ap}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_3D}}~{2}})}}~{V0t}})}}~{\mname{c\_2Ebool\_2ET}}})}})}}~{({{{ap}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_3D}}~{A\_27a}})}}~{V3x}})}}~{V1t1}})}})}})}}~{({{{ap}~{({{{ap}~{\mname{c\_2Emin\_2E\_3D\_3D\_3E}}}~{({{{ap}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_3D}}~{2}})}}~{V0t}})}}~{\mname{c\_2Ebool\_2EF}}})}})}}~{({{{ap}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_3D}}~{A\_27a}})}}~{V3x}})}}~{V2t2}})}})}})}})}})}})}})}})}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfedgpgngcgjgogpfcdfeffafeebeeffe}
We define $\mname{c\_2Ecombin\_2EUPDATE}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {{\uniddcgcg} A\_27b : {\iota} .  {{\uniddcgcg} V0a \in {A\_27a} .  {{\uniddcgcg} V1b \in {A\_27b} .  {({{\uniddcgcg} V2f \in {({{A\_27b}^{{A\_27a}}})} .  {({{\uniddcgcg} V3c \in {A\_27a} .  {({{{ap}~{({{{ap}~{({{{ap}~{({{\mname{c\_2Ebool\_2ECOND}}~{A\_27b}})}}~{({{{ap}~{({{{ap}~{({{\mname{c\_2Emin\_2E\_3D}}~{A\_27a}})}}~{V0a}})}}~{V3c}})}})}}~{V1b}})}}~{({{{ap}~{V2f}}~{V3c}})}})}})}})}}}}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfedgpgngcgjgogpfcdfepg}
We define $\mname{c\_2Ecombin\_2Eo}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {{\uniddcgcg} A\_27b : {\iota} .  {{\uniddcgcg} A\_27c : {\iota} .  {{\uniddcgcg} V0f \in {({{A\_27b}^{{A\_27c}}})} .  {{\uniddcgcg} V1g \in {({{A\_27c}^{{A\_27a}}})} .  {({{\uniddcgcg} V2x \in {A\_27a} .  {({{{ap}~{V0f}}~{({{{ap}~{V1g}}~{V2x}})}})}})}}}}}}$.
\end{definition}
Let $ c\_2Elist\_2ECONS : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Elist\_2ECONS~A\_27a \in (((ty\_2Elist\_2Elist~\\
A\_27a)^{{({{ty\_2Elist\_2Elist}~{A\_27a}})}})^{{A\_27a}})\end{array}
\label{hyp:ngfgngpfdgpfcdfemgjgdhehpfcdfedepeoedf}
\end{equation}
\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}
\begin{definition}\label{def:dgpfcdfedgpgngcgjgogpfcdfedf}
We define $\mname{c\_2Ecombin\_2ES}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {{\uniddcgcg} A\_27b : {\iota} .  {{\uniddcgcg} A\_27c : {\iota} .  {({{\uniddcgcg} V0f \in {({{({{A\_27c}^{{A\_27b}}})}^{{A\_27a}}})} .  {({{\uniddcgcg} V1g \in {({{A\_27b}^{{A\_27a}}})} .  {({{\uniddcgcg} V2x \in {A\_27a} .  {({{{ap}~{({{{ap}~{V0f}}~{V2x}})}}~{({{{ap}~{V1g}}~{V2x}})}})}})}})}})}}}}$.
\end{definition}
\begin{definition}\label{def:dgpfcdfedgpgngcgjgogpfcdfeje}
We define $\mname{c\_2Ecombin\_2EI}$ to be ${{\uniddcgcg} A\_27a : {\iota} .  {({{{ap}~{({{{ap}~{({{{{\mname{c\_2Ecombin\_2ES}}~{A\_27a}}~{({{A\_27a}^{{A\_27a}}})}}~{A\_27a}})}}~{({{{\mname{c\_2Ecombin\_2EK}}~{A\_27a}}~{({{A\_27a}^{{A\_27a}}})}})}})}}~{({{{\mname{c\_2Ecombin\_2EK}}~{A\_27a}}~{A\_27a}})}})}}$.
\end{definition}
Let $ c\_2Elist\_2ENIL : {{\iota}{\unicdbdjdcd}{\iota}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}c\_2Elist\_2ENIL~A\_27a \in (ty\_2Elist\_2Elist~\\
A\_27a)\end{array}
\label{hyp:ngfgngpfdgpfcdfemgjgdhehpfcdfeoejeme}
\end{equation}
Let $ c\_2Eupdate\_2ELIST\_\_UPDATE : {{\iota}{\unicdbdjdcd}{{\iota}{\unicdbdjdcd}{\iota}}}$ be given.
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}{\unicdcdadad} A\_27b .  nonempty~A\_27b{\unicdbdjdcd}c\_2Eupdate\_2ELIST\_\_UPDATE~\\
A\_27a~A\_27b \in (((A\_27b^{{A\_27a}})^{{({{A\_27b}^{{A\_27a}}})}})^{{({{ty\_2Elist\_2Elist}~{({{{ty\_2Epair\_2Eprod}~{A\_27a}}~{A\_27b}})}})}})\end{array}
\label{hyp:ngfgngpfdgpfcdfefhahegbgehfgpfcdfemejedfefpfpfffafeebeeffe}
\end{equation}
Assume the following.
\begin{equation}
{True}\label{hyp:ehigngpfcdfecgpgpgmgpfcdfeefcfffefie}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}({\unicdcdadad} V0x \in A\_27a .  ((V0x=V0x){\unicdbdjded}\\
True))\end{array}
\label{hyp:ehigngpfcdfecgpgpgmgpfcdfecffegemepfpfdemebeffdffe}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}({\unicdcdadad} V0x \in A\_27a .  ({\unicdcdadad} V1y \in \\
A\_27a .  ((V0x=V1y){\unicdbdjded}(V1y=V0x))))\end{array}
\label{hyp:ehigngpfcdfecgpgpgmgpfcdfefebfpfpfdfjfnepfpffebf}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}{\unicdcdadad} A\_27b .  nonempty~A\_27b{\unicdbdjdcd}{\unicdcdadad} A\_27c .  \\
nonempty~A\_27c{\unicdbdjdcd}({\unicdcdadad} V0f \in (A\_27b^{{A\_27a}}) .  ({\unicdcdadad} V1g \in (A\_27a^{{A\_27c}}) .  \\
({\unicdcdadad} V2x \in A\_27c .  ((ap~(ap~(ap~(\mname{c\_2Ecombin\_2Eo}~A\_27c~A\_27b~A\_27a)~\\
V0f)~V1g)~V2x)=(ap~V0f~(ap~V1g~V2x))))))\end{array}
\label{hyp:ehigngpfcdfedgpgngcgjgogpfcdfepgpfpfefiene}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}{\unicdcdadad} A\_27b .  nonempty~A\_27b{\unicdbdjdcd}{\unicdcdadad} A\_27c .  \\
nonempty~A\_27c{\unicdbdjdcd}{\unicdcdadad} A\_27d .  nonempty~A\_27d{\unicdbdjdcd}({\unicdcdadad} V0f \in (A\_27b^{{A\_27a}}) .  \\
({\unicdcdadad} V1g \in (A\_27a^{{A\_27c}}) .  ({\unicdcdadad} V2h \in (A\_27c^{{A\_27d}}) .  ((ap~(\\
ap~(\mname{c\_2Ecombin\_2Eo}~A\_27d~A\_27b~A\_27a)~V0f)~(ap~(ap~(\mname{c\_2Ecombin\_2Eo}~\\
A\_27d~A\_27a~A\_27c)~V1g)~V2h))=(ap~(ap~(\mname{c\_2Ecombin\_2Eo}~A\_27d~A\_27b~\\
A\_27c)~(ap~(ap~(\mname{c\_2Ecombin\_2Eo}~A\_27c~A\_27b~A\_27a)~V0f)~V1g))~V2h)))))\end{array}
\label{hyp:ehigngpfcdfedgpgngcgjgogpfcdfepgpfpfbedfdfpede}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}({\unicdcdadad} V0x \in A\_27a .  ((ap~(\mname{c\_2Ecombin\_2EI}~\\
A\_27a)~V0x)=V0x))\end{array}
\label{hyp:ehigngpfcdfedgpgngcgjgogpfcdfejepfpfefiene}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}{\unicdcdadad} A\_27b .  nonempty~A\_27b{\unicdbdjdcd}(\\
{\unicdcdadad} V0f \in (A\_27b^{{A\_27a}}) .  (((ap~(ap~(\mname{c\_2Ecombin\_2Eo}~A\_27a~A\_27b~\\
A\_27b)~(\mname{c\_2Ecombin\_2EI}~A\_27b))~V0f)=V0f){\unicdcdcdhd}((ap~(ap~(\mname{c\_2Ecombin\_2Eo}~\\
A\_27a~A\_27b~A\_27a)~V0f)~(\mname{c\_2Ecombin\_2EI}~A\_27a))=V0f)))\end{array}
\label{hyp:ehigngpfcdfedgpgngcgjgogpfcdfejepfpfpgpfpfjeee}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}(({\unicdcdadad} V0l \in (ty\_2Elist\_2Elist~\\
A\_27a) .  ((ap~(ap~(c\_2Elist\_2EAPPEND~A\_27a)~(c\_2Elist\_2ENIL~A\_27a))~\\
V0l)=V0l)){\unicdcdcdhd}({\unicdcdadad} V1l1 \in (ty\_2Elist\_2Elist~A\_27a) .  ({\unicdcdadad} V2l2 \in \\
(ty\_2Elist\_2Elist~A\_27a) .  ({\unicdcdadad} V3h \in A\_27a .  ((ap~(ap~(c\_2Elist\_2EAPPEND~\\
A\_27a)~(ap~(ap~(c\_2Elist\_2ECONS~A\_27a)~V3h)~V1l1))~V2l2)=(ap~(ap~\\
(c\_2Elist\_2ECONS~A\_27a)~V3h)~(ap~(ap~(c\_2Elist\_2EAPPEND~A\_27a)~\\
V1l1)~V2l2)))))))\end{array}
\label{hyp:ehigngpfcdfemgjgdhehpfcdfebeafaffeoeee}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}({\unicdcdadad} V0P \in (2^{{({{ty\_2Elist\_2Elist}~{A\_27a}})}}) .  \\
(((p~(ap~V0P~(c\_2Elist\_2ENIL~A\_27a))){\unicdcdcdhd}({\unicdcdadad} V1t \in (ty\_2Elist\_2Elist~\\
A\_27a) .  ((p~(ap~V0P~V1t)){\unicdbdjdcd}({\unicdcdadad} V2h \in A\_27a .  (p~(ap~V0P~(ap~(ap~(\\
c\_2Elist\_2ECONS~A\_27a)~V2h)~V1t))))))){\unicdbdjdcd}({\unicdcdadad} V3l \in (ty\_2Elist\_2Elist~\\
A\_27a) .  (p~(ap~V0P~V3l)))))\end{array}
\label{hyp:ehigngpfcdfemgjgdhehpfcdfemgjgdhehpfpfjgogegfhdgehjgpgog}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}(({\unicdcdadad} V0x \in A\_27a .  ((ap~(ap~(c\_2Elist\_2ESNOC~\\
A\_27a)~V0x)~(c\_2Elist\_2ENIL~A\_27a))=(ap~(ap~(c\_2Elist\_2ECONS~\\
A\_27a)~V0x)~(c\_2Elist\_2ENIL~A\_27a)))){\unicdcdcdhd}({\unicdcdadad} V1x \in A\_27a .  ({\unicdcdadad} V2x\_27 \in \\
A\_27a .  ({\unicdcdadad} V3l \in (ty\_2Elist\_2Elist~A\_27a) .  ((ap~(ap~(c\_2Elist\_2ESNOC~\\
A\_27a)~V1x)~(ap~(ap~(c\_2Elist\_2ECONS~A\_27a)~V2x\_27)~V3l))=(ap~(\\
ap~(c\_2Elist\_2ECONS~A\_27a)~V2x\_27)~(ap~(ap~(c\_2Elist\_2ESNOC~A\_27a)~\\
V1x)~V3l)))))))\end{array}
\label{hyp:ehigngpfcdfemgjgdhehpfcdfedfoepede}
\end{equation}
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~(c\_2Epair\_2EFST~A\_27a~\\
A\_27b)~(ap~(ap~(\mname{c\_2Epair\_2E\_2C}~A\_27a~A\_27b)~V0x)~V1y))=V0x)))\end{array}
\label{hyp:ehigngpfcdfeahbgjgchpfcdfegedfef}
\end{equation}
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~(c\_2Epair\_2ESND~A\_27a~\\
A\_27b)~(ap~(ap~(\mname{c\_2Epair\_2E\_2C}~A\_27a~A\_27b)~V0x)~V1y))=V1y)))\end{array}
\label{hyp:ehigngpfcdfeahbgjgchpfcdfedfoeee}
\end{equation}
Assume the following.
\begin{equation}
\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}{\unicdcdadad} A\_27b .  nonempty~A\_27b{\unicdbdjdcd}(\\
((ap~(c\_2Eupdate\_2ELIST\_\_UPDATE~A\_27a~A\_27b)~(c\_2Elist\_2ENIL~\\
(ty\_2Epair\_2Eprod~A\_27a~A\_27b)))=(\mname{c\_2Ecombin\_2EI}~(A\_27b^{{A\_27a}}))){\unicdcdcdhd}\\
({\unicdcdadad} V0h \in (ty\_2Epair\_2Eprod~A\_27a~A\_27b) .  ({\unicdcdadad} V1t \in (ty\_2Elist\_2Elist~\\
(ty\_2Epair\_2Eprod~A\_27a~A\_27b)) .  ((ap~(c\_2Eupdate\_2ELIST\_\_UPDATE~\\
A\_27a~A\_27b)~(ap~(ap~(c\_2Elist\_2ECONS~(ty\_2Epair\_2Eprod~A\_27a~\\
A\_27b))~V0h)~V1t))=(ap~(ap~(\mname{c\_2Ecombin\_2Eo}~(A\_27b^{{A\_27a}})~(A\_27b^{{A\_27a}})~\\
(A\_27b^{{A\_27a}}))~(ap~(ap~(\mname{c\_2Ecombin\_2EUPDATE}~A\_27a~A\_27b)~(ap~(c\_2Epair\_2EFST~\\
A\_27a~A\_27b)~V0h))~(ap~(c\_2Epair\_2ESND~A\_27a~A\_27b)~V0h)))~(ap~(\\
c\_2Eupdate\_2ELIST\_\_UPDATE~A\_27a~A\_27b)~V1t))))))\end{array}
\label{hyp:ehigngpfcdfefhahegbgehfgpfcdfemejedfefpfpfffafeebeeffepfpfegfggg}
\end{equation}
\begin{theorem}\label{thm:ehigngpfcdfefhahegbgehfgpfcdfemejedfefpfpfffafeebeeffepfpfefienedf}
$$\begin{array}{c}{\unicdcdadad} A\_27a .  nonempty~A\_27a{\unicdbdjdcd}{\unicdcdadad} A\_27b .  nonempty~A\_27b{\unicdbdjdcd}{\unicdcdadad} A\_27c .  \\
nonempty~A\_27c{\unicdbdjdcd}{\unicdcdadad} A\_27d .  nonempty~A\_27d{\unicdbdjdcd}{\unicdcdadad} A\_27e .  nonempty~\\
A\_27e{\unicdbdjdcd}{\unicdcdadad} A\_27f .  nonempty~A\_27f{\unicdbdjdcd}{\unicdcdadad} A\_27g .  nonempty~A\_27g{\unicdbdjdcd}\\
{\unicdcdadad} A\_27h .  nonempty~A\_27h{\unicdbdjdcd}((({\unicdcdadad} V0l1 \in A\_27a .  ({\unicdcdadad} V1l2 \in \\
A\_27a .  ({\unicdcdadad} V2r1 \in A\_27b .  ({\unicdcdadad} V3r2 \in A\_27b .  ((ap~(ap~(\mname{c\_2Ecombin\_2Eo}~\\
(A\_27b^{{A\_27a}})~(A\_27b^{{A\_27a}})~(A\_27b^{{A\_27a}}))~(ap~(ap~(\mname{c\_2Ecombin\_2EUPDATE}~\\
A\_27a~A\_27b)~V0l1)~V2r1))~(ap~(ap~(\mname{c\_2Ecombin\_2EUPDATE}~A\_27a~A\_27b)~\\
V1l2)~V3r2))=(ap~(c\_2Eupdate\_2ELIST\_\_UPDATE~A\_27a~A\_27b)~(ap~\\
(ap~(c\_2Elist\_2ECONS~(ty\_2Epair\_2Eprod~A\_27a~A\_27b))~(ap~(ap~(\\
\mname{c\_2Epair\_2E\_2C}~A\_27a~A\_27b)~V0l1)~V2r1))~(ap~(ap~(c\_2Elist\_2ECONS~\\
(ty\_2Epair\_2Eprod~A\_27a~A\_27b))~(ap~(ap~(\mname{c\_2Epair\_2E\_2C}~A\_27a~\\
A\_27b)~V1l2)~V3r2))~(c\_2Elist\_2ENIL~(ty\_2Epair\_2Eprod~A\_27a~A\_27b)))))))))){\unicdcdcdhd}\\
(({\unicdcdadad} V4l \in A\_27c .  ({\unicdcdadad} V5r \in A\_27d .  ({\unicdcdadad} V6t \in (ty\_2Elist\_2Elist~\\
(ty\_2Epair\_2Eprod~A\_27c~A\_27d)) .  ((ap~(ap~(\mname{c\_2Ecombin\_2Eo}~(A\_27d^{{A\_27c}})~\\
(A\_27d^{{A\_27c}})~(A\_27d^{{A\_27c}}))~(ap~(ap~(\mname{c\_2Ecombin\_2EUPDATE}~A\_27c~\\
A\_27d)~V4l)~V5r))~(ap~(c\_2Eupdate\_2ELIST\_\_UPDATE~A\_27c~A\_27d)~\\
V6t))=(ap~(c\_2Eupdate\_2ELIST\_\_UPDATE~A\_27c~A\_27d)~(ap~(ap~(c\_2Elist\_2ECONS~\\
(ty\_2Epair\_2Eprod~A\_27c~A\_27d))~(ap~(ap~(\mname{c\_2Epair\_2E\_2C}~A\_27c~\\
A\_27d)~V4l)~V5r))~V6t)))))){\unicdcdcdhd}(({\unicdcdadad} V7l1 \in A\_27e .  ({\unicdcdadad} V8l2 \in \\
A\_27e .  ({\unicdcdadad} V9r1 \in A\_27f .  ({\unicdcdadad} V10r2 \in A\_27f .  ({\unicdcdadad} V11f \in \\
(A\_27f^{{A\_27e}}) .  ((ap~(ap~(ap~(\mname{c\_2Ecombin\_2EUPDATE}~A\_27e~A\_27f)~V7l1)~\\
V9r1)~(ap~(ap~(ap~(\mname{c\_2Ecombin\_2EUPDATE}~A\_27e~A\_27f)~V8l2)~V10r2)~\\
V11f))=(ap~(ap~(c\_2Eupdate\_2ELIST\_\_UPDATE~A\_27e~A\_27f)~(ap~(ap~\\
(c\_2Elist\_2ECONS~(ty\_2Epair\_2Eprod~A\_27e~A\_27f))~(ap~(ap~(\mname{c\_2Epair\_2E\_2C}~\\
A\_27e~A\_27f)~V7l1)~V9r1))~(ap~(ap~(c\_2Elist\_2ECONS~(ty\_2Epair\_2Eprod~\\
A\_27e~A\_27f))~(ap~(ap~(\mname{c\_2Epair\_2E\_2C}~A\_27e~A\_27f)~V8l2)~V10r2))~\\
(c\_2Elist\_2ENIL~(ty\_2Epair\_2Eprod~A\_27e~A\_27f)))))~V11f))))))){\unicdcdcdhd}\\
({\unicdcdadad} V12l \in A\_27g .  ({\unicdcdadad} V13r \in A\_27h .  ({\unicdcdadad} V14t \in (ty\_2Elist\_2Elist~\\
(ty\_2Epair\_2Eprod~A\_27g~A\_27h)) .  ({\unicdcdadad} V15f \in (A\_27h^{{A\_27g}}) .  \\
((ap~(ap~(ap~(\mname{c\_2Ecombin\_2EUPDATE}~A\_27g~A\_27h)~V12l)~V13r)~(ap~(\\
ap~(c\_2Eupdate\_2ELIST\_\_UPDATE~A\_27g~A\_27h)~V14t)~V15f))=(ap~(\\
ap~(c\_2Eupdate\_2ELIST\_\_UPDATE~A\_27g~A\_27h)~(ap~(ap~(c\_2Elist\_2ECONS~\\
(ty\_2Epair\_2Eprod~A\_27g~A\_27h))~(ap~(ap~(\mname{c\_2Epair\_2E\_2C}~A\_27g~\\
A\_27h)~V12l)~V13r))~V14t))~V15f))))))))){\unicdcdcdhd}(({\unicdcdadad} V16l1 \in (ty\_2Elist\_2Elist~\\
(ty\_2Epair\_2Eprod~A\_27a~A\_27b)) .  ({\unicdcdadad} V17l2 \in (ty\_2Elist\_2Elist~\\
(ty\_2Epair\_2Eprod~A\_27a~A\_27b)) .  ((ap~(ap~(\mname{c\_2Ecombin\_2Eo}~(A\_27b^{{A\_27a}})~\\
(A\_27b^{{A\_27a}})~(A\_27b^{{A\_27a}}))~(ap~(c\_2Eupdate\_2ELIST\_\_UPDATE~A\_27a~\\
A\_27b)~V16l1))~(ap~(c\_2Eupdate\_2ELIST\_\_UPDATE~A\_27a~A\_27b)~V17l2))=\\
(ap~(c\_2Eupdate\_2ELIST\_\_UPDATE~A\_27a~A\_27b)~(ap~(ap~(c\_2Elist\_2EAPPEND~\\
(ty\_2Epair\_2Eprod~A\_27a~A\_27b))~V16l1)~V17l2))))){\unicdcdcdhd}(({\unicdcdadad} V18l1 \in \\
(ty\_2Elist\_2Elist~(ty\_2Epair\_2Eprod~A\_27c~A\_27d)) .  ({\unicdcdadad} V19l2 \in \\
A\_27c .  ({\unicdcdadad} V20r \in A\_27d .  ((ap~(ap~(\mname{c\_2Ecombin\_2Eo}~(A\_27d^{{A\_27c}})~\\
(A\_27d^{{A\_27c}})~(A\_27d^{{A\_27c}}))~(ap~(c\_2Eupdate\_2ELIST\_\_UPDATE~A\_27c~\\
A\_27d)~V18l1))~(ap~(ap~(\mname{c\_2Ecombin\_2EUPDATE}~A\_27c~A\_27d)~V19l2)~\\
V20r))=(ap~(c\_2Eupdate\_2ELIST\_\_UPDATE~A\_27c~A\_27d)~(ap~(ap~(c\_2Elist\_2ESNOC~\\
(ty\_2Epair\_2Eprod~A\_27c~A\_27d))~(ap~(ap~(\mname{c\_2Epair\_2E\_2C}~A\_27c~\\
A\_27d)~V19l2)~V20r))~V18l1)))))){\unicdcdcdhd}(({\unicdcdadad} V21l1 \in (ty\_2Elist\_2Elist~\\
(ty\_2Epair\_2Eprod~A\_27e~A\_27f)) .  ({\unicdcdadad} V22l2 \in (ty\_2Elist\_2Elist~\\
(ty\_2Epair\_2Eprod~A\_27e~A\_27f)) .  ({\unicdcdadad} V23f \in (A\_27f^{{A\_27e}}) .  \\
((ap~(ap~(c\_2Eupdate\_2ELIST\_\_UPDATE~A\_27e~A\_27f)~V21l1)~(ap~(ap~\\
(c\_2Eupdate\_2ELIST\_\_UPDATE~A\_27e~A\_27f)~V22l2)~V23f))=(ap~(ap~\\
(c\_2Eupdate\_2ELIST\_\_UPDATE~A\_27e~A\_27f)~(ap~(ap~(c\_2Elist\_2EAPPEND~\\
(ty\_2Epair\_2Eprod~A\_27e~A\_27f))~V21l1)~V22l2))~V23f))))){\unicdcdcdhd}({\unicdcdadad} V24l1 \in \\
(ty\_2Elist\_2Elist~(ty\_2Epair\_2Eprod~A\_27g~A\_27h)) .  ({\unicdcdadad} V25l2 \in \\
A\_27g .  ({\unicdcdadad} V26r \in A\_27h .  ({\unicdcdadad} V27f \in (A\_27h^{{A\_27g}}) .  ((ap~\\
(ap~(c\_2Eupdate\_2ELIST\_\_UPDATE~A\_27g~A\_27h)~V24l1)~(ap~(ap~(ap~\\
(\mname{c\_2Ecombin\_2EUPDATE}~A\_27g~A\_27h)~V25l2)~V26r)~V27f))=(ap~(ap~\\
(c\_2Eupdate\_2ELIST\_\_UPDATE~A\_27g~A\_27h)~(ap~(ap~(c\_2Elist\_2ESNOC~\\
(ty\_2Epair\_2Eprod~A\_27g~A\_27h))~(ap~(ap~(\mname{c\_2Epair\_2E\_2C}~A\_27g~\\
A\_27h)~V25l2)~V26r))~V24l1))~V27f))))))))))\end{array}$$
\end{theorem}
\end{document}
