include('Axioms/quantHeuristics^2.ax').
thf(stp_c_ty_2Elist_2Elist_o,type,(tp__c_ty_2Elist_2Elist_o : $tType)).
thf(stp_inj_c_ty_2Elist_2Elist_o,type,(inj__c_ty_2Elist_2Elist_o : (tp__c_ty_2Elist_2Elist_o > $i))).
thf(stp_surj_c_ty_2Elist_2Elist_o,type,(surj__c_ty_2Elist_2Elist_o : ($i > tp__c_ty_2Elist_2Elist_o))).
thf(stp_inj_surj_c_ty_2Elist_2Elist_o,axiom,( ! [X:tp__c_ty_2Elist_2Elist_o] : ((surj__c_ty_2Elist_2Elist_o @ (inj__c_ty_2Elist_2Elist_o @ X)) = X))).
thf(stp_inj_mem_c_ty_2Elist_2Elist_o,axiom,( ! [X:tp__c_ty_2Elist_2Elist_o] : (mem @ (inj__c_ty_2Elist_2Elist_o @ X) @ (ty_2Elist_2Elist@bool)))).
thf(stp_iso_mem_c_ty_2Elist_2Elist_o,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Elist_2Elist@bool)) => (X = (inj__c_ty_2Elist_2Elist_o @ (surj__c_ty_2Elist_2Elist_o @ X)))))).
thf(tp_c_2Erich__list_2EAND__EL,type,(c_2Erich__list_2EAND__EL:$i)).
thf(mem_c_2Erich__list_2EAND__EL,axiom,(mem@c_2Erich__list_2EAND__EL@(arr@(ty_2Elist_2Elist@bool)@bool))).
thf(tp_c_2Erich__list_2EBUTLASTN,type,(c_2Erich__list_2EBUTLASTN:(del>$i))).
thf(mem_c_2Erich__list_2EBUTLASTN,axiom,( ! [A_27a:del] : (mem@(c_2Erich__list_2EBUTLASTN@A_27a)@(arr@ty_2Enum_2Enum@(arr@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a)))))).
thf(tp_c_2Erich__list_2ECOUNT__LIST,type,(c_2Erich__list_2ECOUNT__LIST:$i)).
thf(mem_c_2Erich__list_2ECOUNT__LIST,axiom,(mem@c_2Erich__list_2ECOUNT__LIST@(arr@ty_2Enum_2Enum@(ty_2Elist_2Elist@ty_2Enum_2Enum)))).
thf(tp_c_2Erich__list_2ECOUNT__LIST__AUX,type,(c_2Erich__list_2ECOUNT__LIST__AUX:$i)).
thf(mem_c_2Erich__list_2ECOUNT__LIST__AUX,axiom,(mem@c_2Erich__list_2ECOUNT__LIST__AUX@(arr@ty_2Enum_2Enum@(arr@(ty_2Elist_2Elist@ty_2Enum_2Enum)@(ty_2Elist_2Elist@ty_2Enum_2Enum))))).
thf(tp_c_2Erich__list_2EELL,type,(c_2Erich__list_2EELL:(del>$i))).
thf(mem_c_2Erich__list_2EELL,axiom,( ! [A_27a:del] : (mem@(c_2Erich__list_2EELL@A_27a)@(arr@ty_2Enum_2Enum@(arr@(ty_2Elist_2Elist@A_27a)@A_27a))))).
thf(tp_c_2Erich__list_2EIS__SUBLIST,type,(c_2Erich__list_2EIS__SUBLIST:(del>$i))).
thf(mem_c_2Erich__list_2EIS__SUBLIST,axiom,( ! [A_27a:del] : (mem@(c_2Erich__list_2EIS__SUBLIST@A_27a)@(arr@(ty_2Elist_2Elist@A_27a)@(arr@(ty_2Elist_2Elist@A_27a)@bool))))).
thf(tp_c_2Erich__list_2EIS__SUFFIX,type,(c_2Erich__list_2EIS__SUFFIX:(del>$i))).
thf(mem_c_2Erich__list_2EIS__SUFFIX,axiom,( ! [A_27a:del] : (mem@(c_2Erich__list_2EIS__SUFFIX@A_27a)@(arr@(ty_2Elist_2Elist@A_27a)@(arr@(ty_2Elist_2Elist@A_27a)@bool))))).
thf(tp_c_2Erich__list_2ELASTN,type,(c_2Erich__list_2ELASTN:(del>$i))).
thf(mem_c_2Erich__list_2ELASTN,axiom,( ! [A_27a:del] : (mem@(c_2Erich__list_2ELASTN@A_27a)@(arr@ty_2Enum_2Enum@(arr@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a)))))).
thf(tp_c_2Erich__list_2ELIST__ELEM__COUNT,type,(c_2Erich__list_2ELIST__ELEM__COUNT:(del>$i))).
thf(mem_c_2Erich__list_2ELIST__ELEM__COUNT,axiom,( ! [A_27a:del] : (mem@(c_2Erich__list_2ELIST__ELEM__COUNT@A_27a)@(arr@A_27a@(arr@(ty_2Elist_2Elist@A_27a)@ty_2Enum_2Enum))))).
thf(tp_c_2Erich__list_2EOR__EL,type,(c_2Erich__list_2EOR__EL:$i)).
thf(mem_c_2Erich__list_2EOR__EL,axiom,(mem@c_2Erich__list_2EOR__EL@(arr@(ty_2Elist_2Elist@bool)@bool))).
thf(tp_c_2Erich__list_2EPREFIX,type,(c_2Erich__list_2EPREFIX:(del>$i))).
thf(mem_c_2Erich__list_2EPREFIX,axiom,( ! [A_27a:del] : (mem@(c_2Erich__list_2EPREFIX@A_27a)@(arr@(arr@A_27a@bool)@(arr@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a)))))).
thf(tp_c_2Erich__list_2EREPLICATE,type,(c_2Erich__list_2EREPLICATE:(del>$i))).
thf(mem_c_2Erich__list_2EREPLICATE,axiom,( ! [A_27a:del] : (mem@(c_2Erich__list_2EREPLICATE@A_27a)@(arr@ty_2Enum_2Enum@(arr@A_27a@(ty_2Elist_2Elist@A_27a)))))).
thf(tp_c_2Erich__list_2ESCANL,type,(c_2Erich__list_2ESCANL:(del>(del>$i)))).
thf(mem_c_2Erich__list_2ESCANL,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Erich__list_2ESCANL@A_27a@A_27b)@(arr@(arr@A_27b@(arr@A_27a@A_27b))@(arr@A_27b@(arr@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27b)))))))).
thf(tp_c_2Erich__list_2ESCANR,type,(c_2Erich__list_2ESCANR:(del>(del>$i)))).
thf(mem_c_2Erich__list_2ESCANR,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Erich__list_2ESCANR@A_27a@A_27b)@(arr@(arr@A_27a@(arr@A_27b@A_27b))@(arr@A_27b@(arr@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27b)))))))).
thf(tp_c_2Erich__list_2ESEG,type,(c_2Erich__list_2ESEG:(del>$i))).
thf(mem_c_2Erich__list_2ESEG,axiom,( ! [A_27a:del] : (mem@(c_2Erich__list_2ESEG@A_27a)@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@(arr@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))))))).
thf(tp_c_2Erich__list_2ESPLITL,type,(c_2Erich__list_2ESPLITL:(del>$i))).
thf(mem_c_2Erich__list_2ESPLITL,axiom,( ! [A_27a:del] : (mem@(c_2Erich__list_2ESPLITL@A_27a)@(arr@(arr@A_27a@bool)@(arr@(ty_2Elist_2Elist@A_27a)@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))))))).
thf(tp_c_2Erich__list_2ESPLITP,type,(c_2Erich__list_2ESPLITP:(del>$i))).
thf(mem_c_2Erich__list_2ESPLITP,axiom,( ! [A_27a:del] : (mem@(c_2Erich__list_2ESPLITP@A_27a)@(arr@(arr@A_27a@bool)@(arr@(ty_2Elist_2Elist@A_27a)@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))))))).
thf(tp_c_2Erich__list_2ESPLITP__AUX,type,(c_2Erich__list_2ESPLITP__AUX:(del>$i))).
thf(mem_c_2Erich__list_2ESPLITP__AUX,axiom,( ! [A_27a:del] : (mem@(c_2Erich__list_2ESPLITP__AUX@A_27a)@(arr@(ty_2Elist_2Elist@A_27a)@(arr@(arr@A_27a@bool)@(arr@(ty_2Elist_2Elist@A_27a)@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a)))))))).
thf(tp_c_2Erich__list_2ESPLITR,type,(c_2Erich__list_2ESPLITR:(del>$i))).
thf(mem_c_2Erich__list_2ESPLITR,axiom,( ! [A_27a:del] : (mem@(c_2Erich__list_2ESPLITR@A_27a)@(arr@(arr@A_27a@bool)@(arr@(ty_2Elist_2Elist@A_27a)@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))))))).
thf(tp_c_2Erich__list_2ESUFFIX,type,(c_2Erich__list_2ESUFFIX:(del>$i))).
thf(mem_c_2Erich__list_2ESUFFIX,axiom,( ! [A_27a:del] : (mem@(c_2Erich__list_2ESUFFIX@A_27a)@(arr@(arr@A_27a@bool)@(arr@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a)))))).
thf(tp_c_2Erich__list_2ETL__T,type,(c_2Erich__list_2ETL__T:(del>$i))).
thf(mem_c_2Erich__list_2ETL__T,axiom,( ! [A_27a:del] : (mem@(c_2Erich__list_2ETL__T@A_27a)@(arr@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))))).
thf(tp_c_2Erich__list_2EUNZIP__FST,type,(c_2Erich__list_2EUNZIP__FST:(del>(del>$i)))).
thf(mem_c_2Erich__list_2EUNZIP__FST,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Erich__list_2EUNZIP__FST@A_27a@A_27b)@(arr@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@A_27a@A_27b))@(ty_2Elist_2Elist@A_27a)))))).
thf(tp_c_2Erich__list_2EUNZIP__SND,type,(c_2Erich__list_2EUNZIP__SND:(del>(del>$i)))).
thf(mem_c_2Erich__list_2EUNZIP__SND,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Erich__list_2EUNZIP__SND@A_27a@A_27b)@(arr@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@A_27b@A_27a))@(ty_2Elist_2Elist@A_27a)))))).
thf(tp_c_2Erich__list_2Ecommon__prefixes,type,(c_2Erich__list_2Ecommon__prefixes:(del>$i))).
thf(mem_c_2Erich__list_2Ecommon__prefixes,axiom,( ! [A_27a:del] : (mem@(c_2Erich__list_2Ecommon__prefixes@A_27a)@(arr@(arr@(ty_2Elist_2Elist@A_27a)@bool)@(arr@(ty_2Elist_2Elist@A_27a)@bool))))).
thf(tp_c_2Erich__list_2Elongest__prefix,type,(c_2Erich__list_2Elongest__prefix:(del>$i))).
thf(mem_c_2Erich__list_2Elongest__prefix,axiom,( ! [A_27a:del] : (mem@(c_2Erich__list_2Elongest__prefix@A_27a)@(arr@(arr@(ty_2Elist_2Elist@A_27a)@bool)@(ty_2Elist_2Elist@A_27a))))).
thf(ax_thm_2Erich__list_2EELL,axiom,( ! [A_27a:del]: (( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Erich__list_2EELL@A_27a)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@V0l) = (ap@(c_2Elist_2ELAST@A_27a)@V0l)))) & ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Erich__list_2EELL@A_27a)@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n)))@V2l) = (ap@(ap@(c_2Erich__list_2EELL@A_27a)@(inj__ty_2Enum_2Enum @ V1n))@(ap@(c_2Elist_2EFRONT@A_27a)@V2l))))))))).
thf(conj_thm_2Erich__list_2EELL__compute,lemma,( ! [A_27a:del]: (( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Erich__list_2EELL@A_27a)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@V0l) = (ap@(c_2Elist_2ELAST@A_27a)@V0l)))) & (( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Erich__list_2EELL@A_27a)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V1n))))@V2l) = (ap@(ap@(c_2Erich__list_2EELL@A_27a)@(ap@(ap@c_2Earithmetic_2E_2D@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V1n))))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@(c_2Elist_2EFRONT@A_27a)@V2l)))))) & ( ! [V3n:tp__ty_2Enum_2Enum] : ( ! [V4l:$i] : ((mem@V4l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Erich__list_2EELL@A_27a)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V3n))))@V4l) = (ap@(ap@(c_2Erich__list_2EELL@A_27a)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V3n))))@(ap@(c_2Elist_2EFRONT@A_27a)@V4l)))))))))).
thf(ax_thm_2Erich__list_2EREPLICATE,axiom,( ! [A_27a:del]: (( ! [V0x:$i] : ((mem@V0x@A_27a) => ((ap@(ap@(c_2Erich__list_2EREPLICATE@A_27a)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@V0x) = (c_2Elist_2ENIL@A_27a)))) & ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((ap@(ap@(c_2Erich__list_2EREPLICATE@A_27a)@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n)))@V2x) = (ap@(ap@(c_2Elist_2ECONS@A_27a)@V2x)@(ap@(ap@(c_2Erich__list_2EREPLICATE@A_27a)@(inj__ty_2Enum_2Enum @ V1n))@V2x))))))))).
thf(conj_thm_2Erich__list_2EREPLICATE__compute,lemma,( ! [A_27a:del]: (( ! [V0x:$i] : ((mem@V0x@A_27a) => ((ap@(ap@(c_2Erich__list_2EREPLICATE@A_27a)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@V0x) = (c_2Elist_2ENIL@A_27a)))) & (( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((ap@(ap@(c_2Erich__list_2EREPLICATE@A_27a)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V1n))))@V2x) = (ap@(ap@(c_2Elist_2ECONS@A_27a)@V2x)@(ap@(ap@(c_2Erich__list_2EREPLICATE@A_27a)@(ap@(ap@c_2Earithmetic_2E_2D@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V1n))))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@V2x)))))) & ( ! [V3n:tp__ty_2Enum_2Enum] : ( ! [V4x:$i] : ((mem@V4x@A_27a) => ((ap@(ap@(c_2Erich__list_2EREPLICATE@A_27a)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V3n))))@V4x) = (ap@(ap@(c_2Elist_2ECONS@A_27a)@V4x)@(ap@(ap@(c_2Erich__list_2EREPLICATE@A_27a)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V3n))))@V4x)))))))))).
thf(ax_thm_2Erich__list_2ESCANL,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0f:$i] : ((mem@V0f@(arr@A_27b@(arr@A_27a@A_27b))) => ( ! [V1e:$i] : ((mem@V1e@A_27b) => ((ap@(ap@(ap@(c_2Erich__list_2ESCANL@A_27a@A_27b)@V0f)@V1e)@(c_2Elist_2ENIL@A_27a)) = (ap@(ap@(c_2Elist_2ECONS@A_27b)@V1e)@(c_2Elist_2ENIL@A_27b))))))) & ( ! [V2f:$i] : ((mem@V2f@(arr@A_27b@(arr@A_27a@A_27b))) => ( ! [V3e:$i] : ((mem@V3e@A_27b) => ( ! [V4x:$i] : ((mem@V4x@A_27a) => ( ! [V5l:$i] : ((mem@V5l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(ap@(c_2Erich__list_2ESCANL@A_27a@A_27b)@V2f)@V3e)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V4x)@V5l)) = (ap@(ap@(c_2Elist_2ECONS@A_27b)@V3e)@(ap@(ap@(ap@(c_2Erich__list_2ESCANL@A_27a@A_27b)@V2f)@(ap@(ap@V2f@V3e)@V4x))@V5l))))))))))))))).
thf(ax_thm_2Erich__list_2ESCANR,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(arr@A_27b@A_27b))) => ( ! [V1e:$i] : ((mem@V1e@A_27b) => ((ap@(ap@(ap@(c_2Erich__list_2ESCANR@A_27a@A_27b)@V0f)@V1e)@(c_2Elist_2ENIL@A_27a)) = (ap@(ap@(c_2Elist_2ECONS@A_27b)@V1e)@(c_2Elist_2ENIL@A_27b))))))) & ( ! [V2f:$i] : ((mem@V2f@(arr@A_27a@(arr@A_27b@A_27b))) => ( ! [V3e:$i] : ((mem@V3e@A_27b) => ( ! [V4x:$i] : ((mem@V4x@A_27a) => ( ! [V5l:$i] : ((mem@V5l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(ap@(c_2Erich__list_2ESCANR@A_27a@A_27b)@V2f)@V3e)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V4x)@V5l)) = (ap@(ap@(c_2Elist_2ECONS@A_27b)@(ap@(ap@V2f@V4x)@(ap@(c_2Elist_2EHD@A_27b)@(ap@(ap@(ap@(c_2Erich__list_2ESCANR@A_27a@A_27b)@V2f)@V3e)@V5l))))@(ap@(ap@(ap@(c_2Erich__list_2ESCANR@A_27a@A_27b)@V2f)@V3e)@V5l))))))))))))))).
thf(ax_thm_2Erich__list_2ESPLITP,axiom,( ! [A_27a:del]: (( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ((ap@(ap@(c_2Erich__list_2ESPLITP@A_27a)@V0P)@(c_2Elist_2ENIL@A_27a)) = (ap@(ap@(c_2Epair_2E_2C@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))@(c_2Elist_2ENIL@A_27a))@(c_2Elist_2ENIL@A_27a))))) & ( ! [V1P:$i] : ((mem@V1P@(arr@A_27a@bool)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ( ! [V3l:$i] : ((mem@V3l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Erich__list_2ESPLITP@A_27a)@V1P)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V2x)@V3l)) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a)))@(ap@V1P@V2x))@(ap@(ap@(c_2Epair_2E_2C@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))@(c_2Elist_2ENIL@A_27a))@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V2x)@V3l)))@(ap@(ap@(c_2Epair_2E_2C@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V2x)@(ap@(c_2Epair_2EFST@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))@(ap@(ap@(c_2Erich__list_2ESPLITP@A_27a)@V1P)@V3l))))@(ap@(c_2Epair_2ESND@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))@(ap@(ap@(c_2Erich__list_2ESPLITP@A_27a)@V1P)@V3l)))))))))))))).
thf(ax_thm_2Erich__list_2ESPLITP__AUX__def,axiom,( ! [A_27a:del]: (( ! [V0acc:$i] : ((mem@V0acc@(ty_2Elist_2Elist@A_27a)) => ( ! [V1P:$i] : ((mem@V1P@(arr@A_27a@bool)) => ((ap@(ap@(ap@(c_2Erich__list_2ESPLITP__AUX@A_27a)@V0acc)@V1P)@(c_2Elist_2ENIL@A_27a)) = (ap@(ap@(c_2Epair_2E_2C@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))@V0acc)@(c_2Elist_2ENIL@A_27a))))))) & ( ! [V2acc:$i] : ((mem@V2acc@(ty_2Elist_2Elist@A_27a)) => ( ! [V3P:$i] : ((mem@V3P@(arr@A_27a@bool)) => ( ! [V4h:$i] : ((mem@V4h@A_27a) => ( ! [V5t:$i] : ((mem@V5t@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(ap@(c_2Erich__list_2ESPLITP__AUX@A_27a)@V2acc)@V3P)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V4h)@V5t)) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a)))@(ap@V3P@V4h))@(ap@(ap@(c_2Epair_2E_2C@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))@V2acc)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V4h)@V5t)))@(ap@(ap@(ap@(c_2Erich__list_2ESPLITP__AUX@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V2acc)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V4h)@(c_2Elist_2ENIL@A_27a))))@V3P)@V5t)))))))))))))).
thf(ax_thm_2Erich__list_2ESPLITL__def,axiom,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ((ap@(c_2Erich__list_2ESPLITL@A_27a)@V0P) = (ap@(c_2Erich__list_2ESPLITP@A_27a)@(ap@(ap@(c_2Ecombin_2Eo@A_27a@bool@bool)@c_2Ebool_2E_7E)@V0P))))))).
thf(ax_thm_2Erich__list_2ESPLITR__def,axiom,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Erich__list_2ESPLITR@A_27a)@V0P)@V1l) = (ap@(ap@(c_2Ebool_2ELET@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a)))@(ap@(c_2Epair_2EUNCURRY@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a)@(ty_2Epair_2Eprod@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a)))@(lam@(ty_2Elist_2Elist@A_27a)@(^ [V2a:$i] : (lam@(ty_2Elist_2Elist@A_27a)@(^ [V3b:$i] : (ap@(ap@(c_2Epair_2E_2C@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))@(ap@(c_2Elist_2EREVERSE@A_27a)@V3b))@(ap@(c_2Elist_2EREVERSE@A_27a)@V2a))))))))@(ap@(ap@(c_2Erich__list_2ESPLITP@A_27a)@(ap@(ap@(c_2Ecombin_2Eo@A_27a@bool@bool)@c_2Ebool_2E_7E)@V0P))@(ap@(c_2Elist_2EREVERSE@A_27a)@V1l)))))))))).
thf(ax_thm_2Erich__list_2EPREFIX__DEF,axiom,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Erich__list_2EPREFIX@A_27a)@V0P)@V1l) = (ap@(c_2Epair_2EFST@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))@(ap@(ap@(c_2Erich__list_2ESPLITP@A_27a)@(ap@(ap@(c_2Ecombin_2Eo@A_27a@bool@bool)@c_2Ebool_2E_7E)@V0P))@V1l))))))))).
thf(ax_thm_2Erich__list_2ESUFFIX__DEF,axiom,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Erich__list_2ESUFFIX@A_27a)@V0P)@V1l) = (ap@(ap@(ap@(c_2Elist_2EFOLDL@A_27a@(ty_2Elist_2Elist@A_27a))@(lam@(ty_2Elist_2Elist@A_27a)@(^ [V2l_27:$i] : (lam@A_27a@(^ [V3x:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Elist_2Elist@A_27a))@(ap@V0P@V3x))@(ap@(ap@(c_2Elist_2ESNOC@A_27a)@V3x)@V2l_27))@(c_2Elist_2ENIL@A_27a)))))))@(c_2Elist_2ENIL@A_27a))@V1l)))))))).
thf(ax_thm_2Erich__list_2EAND__EL__DEF,axiom,(c_2Erich__list_2EAND__EL = (ap@(c_2Elist_2EEVERY@bool)@(c_2Ecombin_2EI@bool)))).
thf(ax_thm_2Erich__list_2EOR__EL__DEF,axiom,(c_2Erich__list_2EOR__EL = (ap@(c_2Elist_2EEXISTS@bool)@(c_2Ecombin_2EI@bool)))).
thf(ax_thm_2Erich__list_2EUNZIP__FST__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@A_27a@A_27b))) => ((ap@(c_2Erich__list_2EUNZIP__FST@A_27a@A_27b)@V0l) = (ap@(c_2Epair_2EFST@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27b))@(ap@(c_2Elist_2EUNZIP@A_27a@A_27b)@V0l)))))))).
thf(ax_thm_2Erich__list_2EUNZIP__SND__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@A_27b@A_27a))) => ((ap@(c_2Erich__list_2EUNZIP__SND@A_27a@A_27b)@V0l) = (ap@(c_2Epair_2ESND@(ty_2Elist_2Elist@A_27b)@(ty_2Elist_2Elist@A_27a))@(ap@(c_2Elist_2EUNZIP@A_27b@A_27a)@V0l)))))))).
thf(ax_thm_2Erich__list_2ELIST__ELEM__COUNT__DEF,axiom,( ! [A_27a:del]: ( ! [V0e:$i] : ((mem@V0e@A_27a) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((surj__ty_2Enum_2Enum @ (ap@(ap@(c_2Erich__list_2ELIST__ELEM__COUNT@A_27a)@V0e)@V1l)) = (surj__ty_2Enum_2Enum @ (ap@(c_2Elist_2ELENGTH@A_27a)@(ap@(ap@(c_2Elist_2EFILTER@A_27a)@(lam@A_27a@(^ [V2x:$i] : (ap@(ap@(c_2Emin_2E_3D@A_27a)@V2x)@V0e))))@V1l)))))))))).
thf(ax_thm_2Erich__list_2ECOUNT__LIST__def,axiom,(((surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ (ap@c_2Erich__list_2ECOUNT__LIST@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) = (surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ (c_2Elist_2ENIL@ty_2Enum_2Enum))) & ( ! [V0n:tp__ty_2Enum_2Enum] : ((surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ (ap@c_2Erich__list_2ECOUNT__LIST@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V0n)))) = (surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ (ap@(ap@(c_2Elist_2ECONS@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@(ap@(c_2Elist_2EMAP@ty_2Enum_2Enum@ty_2Enum_2Enum)@c_2Enum_2ESUC)@(ap@c_2Erich__list_2ECOUNT__LIST@(inj__ty_2Enum_2Enum @ V0n))))))))).
thf(ax_thm_2Erich__list_2ECOUNT__LIST__AUX__def,axiom,(( ! [V0l:tp__c_ty_2Elist_2Elist_ty_2Enum_2Enum] : ((surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ (ap@(ap@c_2Erich__list_2ECOUNT__LIST__AUX@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ V0l))) = V0l)) & ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2l:tp__c_ty_2Elist_2Elist_ty_2Enum_2Enum] : ((surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ (ap@(ap@c_2Erich__list_2ECOUNT__LIST__AUX@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n)))@(inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ V2l))) = (surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ (ap@(ap@c_2Erich__list_2ECOUNT__LIST__AUX@(inj__ty_2Enum_2Enum @ V1n))@(ap@(ap@(c_2Elist_2ECONS@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V1n))@(inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ V2l))))))))).
thf(conj_thm_2Erich__list_2ECOUNT__LIST__AUX__def__compute,lemma,(( ! [V0l:tp__c_ty_2Elist_2Elist_ty_2Enum_2Enum] : ((surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ (ap@(ap@c_2Erich__list_2ECOUNT__LIST__AUX@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ V0l))) = V0l)) & (( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2l:tp__c_ty_2Elist_2Elist_ty_2Enum_2Enum] : ((surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ (ap@(ap@c_2Erich__list_2ECOUNT__LIST__AUX@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V1n))))@(inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ V2l))) = (surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ (ap@(ap@c_2Erich__list_2ECOUNT__LIST__AUX@(ap@(ap@c_2Earithmetic_2E_2D@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V1n))))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@(ap@(c_2Elist_2ECONS@ty_2Enum_2Enum)@(ap@(ap@c_2Earithmetic_2E_2D@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V1n))))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ V2l))))))) & ( ! [V3n:tp__ty_2Enum_2Enum] : ( ! [V4l:tp__c_ty_2Elist_2Elist_ty_2Enum_2Enum] : ((surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ (ap@(ap@c_2Erich__list_2ECOUNT__LIST__AUX@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V3n))))@(inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ V4l))) = (surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ (ap@(ap@c_2Erich__list_2ECOUNT__LIST__AUX@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V3n))))@(ap@(ap@(c_2Elist_2ECONS@ty_2Enum_2Enum)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V3n))))@(inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ V4l)))))))))).
thf(ax_thm_2Erich__list_2ETL__T__def,axiom,( ! [A_27a:del]: (((ap@(c_2Erich__list_2ETL__T@A_27a)@(c_2Elist_2ENIL@A_27a)) = (c_2Elist_2ENIL@A_27a)) & ( ! [V0h:$i] : ((mem@V0h@A_27a) => ( ! [V1t:$i] : ((mem@V1t@(ty_2Elist_2Elist@A_27a)) => ((ap@(c_2Erich__list_2ETL__T@A_27a)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V0h)@V1t)) = V1t)))))))).
thf(conj_thm_2Erich__list_2ETAKE,lemma,( ! [A_27a:del]: (( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Elist_2ETAKE@A_27a)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@V0l) = (c_2Elist_2ENIL@A_27a)))) & ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2x:$i] : ((mem@V2x@A_27a) => ( ! [V3l:$i] : ((mem@V3l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Elist_2ETAKE@A_27a)@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n)))@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V2x)@V3l)) = (ap@(ap@(c_2Elist_2ECONS@A_27a)@V2x)@(ap@(ap@(c_2Elist_2ETAKE@A_27a)@(inj__ty_2Enum_2Enum @ V1n))@V3l))))))))))).
thf(conj_thm_2Erich__list_2EDROP,lemma,( ! [A_27a:del]: (( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Elist_2EDROP@A_27a)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@V0l) = V0l))) & ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2x:$i] : ((mem@V2x@A_27a) => ( ! [V3l:$i] : ((mem@V3l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Elist_2EDROP@A_27a)@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n)))@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V2x)@V3l)) = (ap@(ap@(c_2Elist_2EDROP@A_27a)@(inj__ty_2Enum_2Enum @ V1n))@V3l)))))))))).
thf(conj_thm_2Erich__list_2EDROP__FUNPOW__TL,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Elist_2EDROP@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1l) = (ap@(ap@(ap@(c_2Earithmetic_2EFUNPOW@(ty_2Elist_2Elist@A_27a))@(c_2Erich__list_2ETL__T@A_27a))@(inj__ty_2Enum_2Enum @ V0n))@V1l))))))).
thf(conj_thm_2Erich__list_2ENOT__NULL__SNOC,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => (~~ (p@(ap@(c_2Elist_2ENULL@A_27a)@(ap@(ap@(c_2Elist_2ESNOC@A_27a)@V0x)@V1l)))))))))).
thf(ax_thm_2Erich__list_2ELASTN__def,axiom,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1xs:$i] : ((mem@V1xs@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Erich__list_2ELASTN@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1xs) = (ap@(c_2Elist_2EREVERSE@A_27a)@(ap@(ap@(c_2Elist_2ETAKE@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Elist_2EREVERSE@A_27a)@V1xs))))))))).
thf(conj_thm_2Erich__list_2ELASTN,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Erich__list_2ELASTN@A_27a)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@V0l) = (c_2Elist_2ENIL@A_27a)))) & ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2x:$i] : ((mem@V2x@A_27b) => ( ! [V3l:$i] : ((mem@V3l@(ty_2Elist_2Elist@A_27b)) => ((ap@(ap@(c_2Erich__list_2ELASTN@A_27b)@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n)))@(ap@(ap@(c_2Elist_2ESNOC@A_27b)@V2x)@V3l)) = (ap@(ap@(c_2Elist_2ESNOC@A_27b)@V2x)@(ap@(ap@(c_2Erich__list_2ELASTN@A_27b)@(inj__ty_2Enum_2Enum @ V1n))@V3l)))))))))))).
thf(ax_thm_2Erich__list_2EBUTLASTN__def,axiom,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1xs:$i] : ((mem@V1xs@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Erich__list_2EBUTLASTN@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1xs) = (ap@(c_2Elist_2EREVERSE@A_27a)@(ap@(ap@(c_2Elist_2EDROP@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Elist_2EREVERSE@A_27a)@V1xs))))))))).
thf(conj_thm_2Erich__list_2EBUTLASTN,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Erich__list_2EBUTLASTN@A_27a)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@V0l) = V0l))) & ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2x:$i] : ((mem@V2x@A_27b) => ( ! [V3l:$i] : ((mem@V3l@(ty_2Elist_2Elist@A_27b)) => ((ap@(ap@(c_2Erich__list_2EBUTLASTN@A_27b)@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n)))@(ap@(ap@(c_2Elist_2ESNOC@A_27b)@V2x)@V3l)) = (ap@(ap@(c_2Erich__list_2EBUTLASTN@A_27b)@(inj__ty_2Enum_2Enum @ V1n))@V3l))))))))))).
thf(ax_thm_2Erich__list_2EIS__SUBLIST,axiom,( ! [A_27a:del]: (( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Erich__list_2EIS__SUBLIST@A_27a)@V0l)@(c_2Elist_2ENIL@A_27a))) <=> $true))) & (( ! [V1x:$i] : ((mem@V1x@A_27a) => ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Erich__list_2EIS__SUBLIST@A_27a)@(c_2Elist_2ENIL@A_27a))@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V1x)@V2l))) <=> $false))))) & ( ! [V3x1:$i] : ((mem@V3x1@A_27a) => ( ! [V4l1:$i] : ((mem@V4l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V5x2:$i] : ((mem@V5x2@A_27a) => ( ! [V6l2:$i] : ((mem@V6l2@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Erich__list_2EIS__SUBLIST@A_27a)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V3x1)@V4l1))@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V5x2)@V6l2))) <=> (((V3x1 = V5x2) & (p@(ap@(ap@(c_2Elist_2EisPREFIX@A_27a)@V6l2)@V4l1))) | (p@(ap@(ap@(c_2Erich__list_2EIS__SUBLIST@A_27a)@V4l1)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V5x2)@V6l2))))))))))))))))).
thf(ax_thm_2Erich__list_2ESEG,axiom,( ! [A_27a:del]: (( ! [V0k:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(ap@(c_2Erich__list_2ESEG@A_27a)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V0k))@V1l) = (c_2Elist_2ENIL@A_27a))))) & (( ! [V2m:tp__ty_2Enum_2Enum] : ( ! [V3x:$i] : ((mem@V3x@A_27a) => ( ! [V4l:$i] : ((mem@V4l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(ap@(c_2Erich__list_2ESEG@A_27a)@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V2m)))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V3x)@V4l)) = (ap@(ap@(c_2Elist_2ECONS@A_27a)@V3x)@(ap@(ap@(ap@(c_2Erich__list_2ESEG@A_27a)@(inj__ty_2Enum_2Enum @ V2m))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@V4l)))))))) & ( ! [V5m:tp__ty_2Enum_2Enum] : ( ! [V6k:tp__ty_2Enum_2Enum] : ( ! [V7x:$i] : ((mem@V7x@A_27a) => ( ! [V8l:$i] : ((mem@V8l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(ap@(c_2Erich__list_2ESEG@A_27a)@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V5m)))@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V6k)))@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V7x)@V8l)) = (ap@(ap@(ap@(c_2Erich__list_2ESEG@A_27a)@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V5m)))@(inj__ty_2Enum_2Enum @ V6k))@V8l)))))))))))).
thf(ax_thm_2Erich__list_2EIS__SUFFIX,axiom,( ! [A_27a:del]: (( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Erich__list_2EIS__SUFFIX@A_27a)@V0l)@(c_2Elist_2ENIL@A_27a))) <=> $true))) & (( ! [V1x:$i] : ((mem@V1x@A_27a) => ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Erich__list_2EIS__SUFFIX@A_27a)@(c_2Elist_2ENIL@A_27a))@(ap@(ap@(c_2Elist_2ESNOC@A_27a)@V1x)@V2l))) <=> $false))))) & ( ! [V3x1:$i] : ((mem@V3x1@A_27a) => ( ! [V4l1:$i] : ((mem@V4l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V5x2:$i] : ((mem@V5x2@A_27a) => ( ! [V6l2:$i] : ((mem@V6l2@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Erich__list_2EIS__SUFFIX@A_27a)@(ap@(ap@(c_2Elist_2ESNOC@A_27a)@V3x1)@V4l1))@(ap@(ap@(c_2Elist_2ESNOC@A_27a)@V5x2)@V6l2))) <=> ((V3x1 = V5x2) & (p@(ap@(ap@(c_2Erich__list_2EIS__SUFFIX@A_27a)@V4l1)@V6l2)))))))))))))))).
thf(conj_thm_2Erich__list_2ELENGTH__NOT__NULL,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@(c_2Elist_2ELENGTH@A_27a)@V0l))) <=> (~~ (p@(ap@(c_2Elist_2ENULL@A_27a)@V0l)))))))).
thf(conj_thm_2Erich__list_2ENOT__NIL__SNOC,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => (~~ ((c_2Elist_2ENIL@A_27a) = (ap@(ap@(c_2Elist_2ESNOC@A_27a)@V0x)@V1l))))))))).
thf(conj_thm_2Erich__list_2ENOT__SNOC__NIL,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => (~~ ((ap@(ap@(c_2Elist_2ESNOC@A_27a)@V0x)@V1l) = (c_2Elist_2ENIL@A_27a))))))))).
thf(conj_thm_2Erich__list_2ESNOC__EQ__LENGTH__EQ,lemma,( ! [A_27a:del]: ( ! [V0x1:$i] : ((mem@V0x1@A_27a) => ( ! [V1l1:$i] : ((mem@V1l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V2x2:$i] : ((mem@V2x2@A_27a) => ( ! [V3l2:$i] : ((mem@V3l2@(ty_2Elist_2Elist@A_27a)) => (((ap@(ap@(c_2Elist_2ESNOC@A_27a)@V0x1)@V1l1) = (ap@(ap@(c_2Elist_2ESNOC@A_27a)@V2x2)@V3l2)) => ((surj__ty_2Enum_2Enum @ (ap@(c_2Elist_2ELENGTH@A_27a)@V1l1)) = (surj__ty_2Enum_2Enum @ (ap@(c_2Elist_2ELENGTH@A_27a)@V3l2)))))))))))))).
thf(conj_thm_2Erich__list_2ESNOC__REVERSE__CONS,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Elist_2ESNOC@A_27a)@V0x)@V1l) = (ap@(c_2Elist_2EREVERSE@A_27a)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V0x)@(ap@(c_2Elist_2EREVERSE@A_27a)@V1l)))))))))).
thf(conj_thm_2Erich__list_2EFOLDR__SNOC,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(arr@A_27b@A_27b))) => ( ! [V1e:$i] : ((mem@V1e@A_27b) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ( ! [V3l:$i] : ((mem@V3l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27a@A_27b)@V0f)@V1e)@(ap@(ap@(c_2Elist_2ESNOC@A_27a)@V2x)@V3l)) = (ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27a@A_27b)@V0f)@(ap@(ap@V0f@V2x)@V1e))@V3l))))))))))))).
thf(conj_thm_2Erich__list_2EFOLDR__FOLDL,lemma,( ! [A_27a:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V1e:$i] : ((mem@V1e@A_27a) => ((p@(ap@(ap@(c_2Ecombin_2EMONOID@A_27a)@V0f)@V1e)) => ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27a@A_27a)@V0f)@V1e)@V2l) = (ap@(ap@(ap@(c_2Elist_2EFOLDL@A_27a@A_27a)@V0f)@V1e)@V2l))))))))))).
thf(conj_thm_2Erich__list_2ELENGTH__FOLDR,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ((surj__ty_2Enum_2Enum @ (ap@(c_2Elist_2ELENGTH@A_27a)@V0l)) = (surj__ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27a@ty_2Enum_2Enum)@(lam@A_27a@(^ [V1x:$i] : (lam@ty_2Enum_2Enum@(^ [V2l_27:$i] : (ap@c_2Enum_2ESUC@V2l_27))))))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@V0l))))))).
thf(conj_thm_2Erich__list_2ELENGTH__FOLDL,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ((surj__ty_2Enum_2Enum @ (ap@(c_2Elist_2ELENGTH@A_27a)@V0l)) = (surj__ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Elist_2EFOLDL@A_27a@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V1l_27:$i] : (lam@A_27a@(^ [V2x:$i] : (ap@c_2Enum_2ESUC@V1l_27))))))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@V0l))))))).
thf(conj_thm_2Erich__list_2EMAP__FOLDR,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Elist_2EMAP@A_27a@A_27b)@V0f)@V1l) = (ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27a@(ty_2Elist_2Elist@A_27b))@(lam@A_27a@(^ [V2x:$i] : (lam@(ty_2Elist_2Elist@A_27b)@(^ [V3l_27:$i] : (ap@(ap@(c_2Elist_2ECONS@A_27b)@(ap@V0f@V2x))@V3l_27))))))@(c_2Elist_2ENIL@A_27b))@V1l))))))))).
thf(conj_thm_2Erich__list_2EMAP__FOLDL,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Elist_2EMAP@A_27a@A_27b)@V0f)@V1l) = (ap@(ap@(ap@(c_2Elist_2EFOLDL@A_27a@(ty_2Elist_2Elist@A_27b))@(lam@(ty_2Elist_2Elist@A_27b)@(^ [V2l_27:$i] : (lam@A_27a@(^ [V3x:$i] : (ap@(ap@(c_2Elist_2ESNOC@A_27b)@(ap@V0f@V3x))@V2l_27))))))@(c_2Elist_2ENIL@A_27b))@V1l))))))))).
thf(conj_thm_2Erich__list_2EFILTER__FOLDR,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Elist_2EFILTER@A_27a)@V0P)@V1l) = (ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27a@(ty_2Elist_2Elist@A_27a))@(lam@A_27a@(^ [V2x:$i] : (lam@(ty_2Elist_2Elist@A_27a)@(^ [V3l_27:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Elist_2Elist@A_27a))@(ap@V0P@V2x))@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V2x)@V3l_27))@V3l_27))))))@(c_2Elist_2ENIL@A_27a))@V1l)))))))).
thf(conj_thm_2Erich__list_2EFILTER__SNOC,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Elist_2EFILTER@A_27a)@V0P)@(ap@(ap@(c_2Elist_2ESNOC@A_27a)@V1x)@V2l)) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Elist_2Elist@A_27a))@(ap@V0P@V1x))@(ap@(ap@(c_2Elist_2ESNOC@A_27a)@V1x)@(ap@(ap@(c_2Elist_2EFILTER@A_27a)@V0P)@V2l)))@(ap@(ap@(c_2Elist_2EFILTER@A_27a)@V0P)@V2l))))))))))).
thf(conj_thm_2Erich__list_2EFILTER__FOLDL,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Elist_2EFILTER@A_27a)@V0P)@V1l) = (ap@(ap@(ap@(c_2Elist_2EFOLDL@A_27a@(ty_2Elist_2Elist@A_27a))@(lam@(ty_2Elist_2Elist@A_27a)@(^ [V2l_27:$i] : (lam@A_27a@(^ [V3x:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Elist_2Elist@A_27a))@(ap@V0P@V3x))@(ap@(ap@(c_2Elist_2ESNOC@A_27a)@V3x)@V2l_27))@V2l_27))))))@(c_2Elist_2ENIL@A_27a))@V1l)))))))).
thf(conj_thm_2Erich__list_2EFILTER__COMM,lemma,( ! [A_27a:del]: ( ! [V0f1:$i] : ((mem@V0f1@(arr@A_27a@bool)) => ( ! [V1f2:$i] : ((mem@V1f2@(arr@A_27a@bool)) => ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Elist_2EFILTER@A_27a)@V0f1)@(ap@(ap@(c_2Elist_2EFILTER@A_27a)@V1f2)@V2l)) = (ap@(ap@(c_2Elist_2EFILTER@A_27a)@V1f2)@(ap@(ap@(c_2Elist_2EFILTER@A_27a)@V0f1)@V2l))))))))))).
thf(conj_thm_2Erich__list_2EFILTER__IDEM,lemma,( ! [A_27a:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@bool)) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Elist_2EFILTER@A_27a)@V0f)@(ap@(ap@(c_2Elist_2EFILTER@A_27a)@V0f)@V1l)) = (ap@(ap@(c_2Elist_2EFILTER@A_27a)@V0f)@V1l)))))))).
thf(conj_thm_2Erich__list_2EFILTER__MAP,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f1:$i] : ((mem@V0f1@(arr@A_27a@bool)) => ( ! [V1f2:$i] : ((mem@V1f2@(arr@A_27b@A_27a)) => ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27b)) => ((ap@(ap@(c_2Elist_2EFILTER@A_27a)@V0f1)@(ap@(ap@(c_2Elist_2EMAP@A_27b@A_27a)@V1f2)@V2l)) = (ap@(ap@(c_2Elist_2EMAP@A_27b@A_27a)@V1f2)@(ap@(ap@(c_2Elist_2EFILTER@A_27b)@(ap@(ap@(c_2Ecombin_2Eo@A_27b@bool@A_27a)@V0f1)@V1f2))@V2l)))))))))))).
thf(conj_thm_2Erich__list_2ELENGTH__FILTER__LEQ,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(c_2Elist_2ELENGTH@A_27a)@(ap@(ap@(c_2Elist_2EFILTER@A_27a)@V0P)@V1l)))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))))))))).
thf(conj_thm_2Erich__list_2EFILTER__EQ,lemma,( ! [A_27a:del]: ( ! [V0P1:$i] : ((mem@V0P1@(arr@A_27a@bool)) => ( ! [V1P2:$i] : ((mem@V1P2@(arr@A_27a@bool)) => ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27a)) => (((ap@(ap@(c_2Elist_2EFILTER@A_27a)@V0P1)@V2l) = (ap@(ap@(c_2Elist_2EFILTER@A_27a)@V1P2)@V2l)) <=> ( ! [V3x:$i] : ((mem@V3x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@V2l))) => ((p@(ap@V0P1@V3x)) <=> (p@(ap@V1P2@V3x))))))))))))))).
thf(conj_thm_2Erich__list_2ELENGTH__SEG,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1k)))@(ap@(c_2Elist_2ELENGTH@A_27a)@V2l))) => ((surj__ty_2Enum_2Enum @ (ap@(c_2Elist_2ELENGTH@A_27a)@(ap@(ap@(ap@(c_2Erich__list_2ESEG@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1k))@V2l))) = V0n)))))))).
thf(conj_thm_2Erich__list_2EAPPEND__NIL,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V0l)@(c_2Elist_2ENIL@A_27a)) = V0l))) & ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27b)) => ((ap@(ap@(c_2Elist_2EAPPEND@A_27b)@(c_2Elist_2ENIL@A_27b))@V1l) = V1l))))))).
thf(conj_thm_2Erich__list_2EAPPEND__FOLDR,lemma,( ! [A_27a:del]: ( ! [V0l1:$i] : ((mem@V0l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l2:$i] : ((mem@V1l2@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V0l1)@V1l2) = (ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27a@(ty_2Elist_2Elist@A_27a))@(c_2Elist_2ECONS@A_27a))@V1l2)@V0l1)))))))).
thf(conj_thm_2Erich__list_2EAPPEND__FOLDL,lemma,( ! [A_27a:del]: ( ! [V0l1:$i] : ((mem@V0l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l2:$i] : ((mem@V1l2@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V0l1)@V1l2) = (ap@(ap@(ap@(c_2Elist_2EFOLDL@A_27a@(ty_2Elist_2Elist@A_27a))@(lam@(ty_2Elist_2Elist@A_27a)@(^ [V2l_27:$i] : (lam@A_27a@(^ [V3x:$i] : (ap@(ap@(c_2Elist_2ESNOC@A_27a)@V3x)@V2l_27))))))@V0l1)@V1l2)))))))).
thf(conj_thm_2Erich__list_2EFOLDR__APPEND,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(arr@A_27b@A_27b))) => ( ! [V1e:$i] : ((mem@V1e@A_27b) => ( ! [V2l1:$i] : ((mem@V2l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V3l2:$i] : ((mem@V3l2@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27a@A_27b)@V0f)@V1e)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V2l1)@V3l2)) = (ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27a@A_27b)@V0f)@(ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27a@A_27b)@V0f)@V1e)@V3l2))@V2l1))))))))))))).
thf(conj_thm_2Erich__list_2EFOLDL__APPEND,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(arr@A_27b@A_27a))) => ( ! [V1e:$i] : ((mem@V1e@A_27a) => ( ! [V2l1:$i] : ((mem@V2l1@(ty_2Elist_2Elist@A_27b)) => ( ! [V3l2:$i] : ((mem@V3l2@(ty_2Elist_2Elist@A_27b)) => ((ap@(ap@(ap@(c_2Elist_2EFOLDL@A_27b@A_27a)@V0f)@V1e)@(ap@(ap@(c_2Elist_2EAPPEND@A_27b)@V2l1)@V3l2)) = (ap@(ap@(ap@(c_2Elist_2EFOLDL@A_27b@A_27a)@V0f)@(ap@(ap@(ap@(c_2Elist_2EFOLDL@A_27b@A_27a)@V0f)@V1e)@V2l1))@V3l2))))))))))))).
thf(conj_thm_2Erich__list_2ECONS__APPEND,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Elist_2ECONS@A_27a)@V0x)@V1l) = (ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V0x)@(c_2Elist_2ENIL@A_27a)))@V1l)))))))).
thf(conj_thm_2Erich__list_2EASSOC__APPEND,lemma,( ! [A_27a:del]: (p@(ap@(c_2Ecombin_2EASSOC@(ty_2Elist_2Elist@A_27a))@(c_2Elist_2EAPPEND@A_27a))))).
thf(conj_thm_2Erich__list_2EMONOID__APPEND__NIL,lemma,( ! [A_27a:del]: (p@(ap@(ap@(c_2Ecombin_2EMONOID@(ty_2Elist_2Elist@A_27a))@(c_2Elist_2EAPPEND@A_27a))@(c_2Elist_2ENIL@A_27a))))).
thf(conj_thm_2Erich__list_2EFLAT__SNOC,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@(ty_2Elist_2Elist@A_27a))) => ((ap@(c_2Elist_2EFLAT@A_27a)@(ap@(ap@(c_2Elist_2ESNOC@(ty_2Elist_2Elist@A_27a))@V0x)@V1l)) = (ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(c_2Elist_2EFLAT@A_27a)@V1l))@V0x)))))))).
thf(conj_thm_2Erich__list_2EFLAT__FOLDR,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@(ty_2Elist_2Elist@A_27a))) => ((ap@(c_2Elist_2EFLAT@A_27a)@V0l) = (ap@(ap@(ap@(c_2Elist_2EFOLDR@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))@(c_2Elist_2EAPPEND@A_27a))@(c_2Elist_2ENIL@A_27a))@V0l)))))).
thf(conj_thm_2Erich__list_2EFLAT__FOLDL,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@(ty_2Elist_2Elist@A_27a))) => ((ap@(c_2Elist_2EFLAT@A_27a)@V0l) = (ap@(ap@(ap@(c_2Elist_2EFOLDL@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))@(c_2Elist_2EAPPEND@A_27a))@(c_2Elist_2ENIL@A_27a))@V0l)))))).
thf(conj_thm_2Erich__list_2ELENGTH__FLAT,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@(ty_2Elist_2Elist@A_27a))) => ((surj__ty_2Enum_2Enum @ (ap@(c_2Elist_2ELENGTH@A_27a)@(ap@(c_2Elist_2EFLAT@A_27a)@V0l))) = (surj__ty_2Enum_2Enum @ (ap@c_2Elist_2ESUM@(ap@(ap@(c_2Elist_2EMAP@(ty_2Elist_2Elist@A_27a)@ty_2Enum_2Enum)@(c_2Elist_2ELENGTH@A_27a))@V0l)))))))).
thf(conj_thm_2Erich__list_2EREVERSE__FOLDR,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ((ap@(c_2Elist_2EREVERSE@A_27a)@V0l) = (ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27a@(ty_2Elist_2Elist@A_27a))@(c_2Elist_2ESNOC@A_27a))@(c_2Elist_2ENIL@A_27a))@V0l)))))).
thf(conj_thm_2Erich__list_2EREVERSE__FOLDL,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ((ap@(c_2Elist_2EREVERSE@A_27a)@V0l) = (ap@(ap@(ap@(c_2Elist_2EFOLDL@A_27a@(ty_2Elist_2Elist@A_27a))@(lam@(ty_2Elist_2Elist@A_27a)@(^ [V1l_27:$i] : (lam@A_27a@(^ [V2x:$i] : (ap@(ap@(c_2Elist_2ECONS@A_27a)@V2x)@V1l_27))))))@(c_2Elist_2ENIL@A_27a))@V0l)))))).
thf(conj_thm_2Erich__list_2EALL__EL__MAP,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27b@A_27a)) => ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27b)) => ((p@(ap@(ap@(c_2Elist_2EEVERY@A_27a)@V0P)@(ap@(ap@(c_2Elist_2EMAP@A_27b@A_27a)@V1f)@V2l))) <=> (p@(ap@(ap@(c_2Elist_2EEVERY@A_27b)@(ap@(ap@(c_2Ecombin_2Eo@A_27b@bool@A_27a)@V0P)@V1f))@V2l)))))))))))).
thf(conj_thm_2Erich__list_2EMEM__EXISTS,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@V1l))) <=> (p@(ap@(ap@(c_2Elist_2EEXISTS@A_27a)@(ap@(c_2Emin_2E_3D@A_27a)@V0x))@V1l))))))))).
thf(conj_thm_2Erich__list_2ESUM__FOLDR,lemma,( ! [V0l:tp__c_ty_2Elist_2Elist_ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@c_2Elist_2ESUM@(inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ V0l))) = (surj__ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Elist_2EFOLDR@ty_2Enum_2Enum@ty_2Enum_2Enum)@c_2Earithmetic_2E_2B)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ V0l)))))).
thf(conj_thm_2Erich__list_2ESUM__FOLDL,lemma,( ! [V0l:tp__c_ty_2Elist_2Elist_ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@c_2Elist_2ESUM@(inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ V0l))) = (surj__ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Elist_2EFOLDL@ty_2Enum_2Enum@ty_2Enum_2Enum)@c_2Earithmetic_2E_2B)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ V0l)))))).
thf(conj_thm_2Erich__list_2EIS__PREFIX,lemma,( ! [A_27a:del]: (( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Elist_2EisPREFIX@A_27a)@(c_2Elist_2ENIL@A_27a))@V0l)) <=> $true))) & (( ! [V1x:$i] : ((mem@V1x@A_27a) => ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Elist_2EisPREFIX@A_27a)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V1x)@V2l))@(c_2Elist_2ENIL@A_27a))) <=> $false))))) & ( ! [V3x1:$i] : ((mem@V3x1@A_27a) => ( ! [V4l1:$i] : ((mem@V4l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V5x2:$i] : ((mem@V5x2@A_27a) => ( ! [V6l2:$i] : ((mem@V6l2@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Elist_2EisPREFIX@A_27a)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V5x2)@V6l2))@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V3x1)@V4l1))) <=> ((V3x1 = V5x2) & (p@(ap@(ap@(c_2Elist_2EisPREFIX@A_27a)@V6l2)@V4l1)))))))))))))))).
thf(conj_thm_2Erich__list_2EIS__PREFIX__APPEND,lemma,( ! [A_27a:del]: ( ! [V0l1:$i] : ((mem@V0l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l2:$i] : ((mem@V1l2@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Elist_2EisPREFIX@A_27a)@V1l2)@V0l1)) <=> (? [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27a)) & (V0l1 = (ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V1l2)@V2l))))))))))).
thf(conj_thm_2Erich__list_2EIS__SUFFIX__APPEND,lemma,( ! [A_27a:del]: ( ! [V0l1:$i] : ((mem@V0l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l2:$i] : ((mem@V1l2@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Erich__list_2EIS__SUFFIX@A_27a)@V0l1)@V1l2)) <=> (? [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27a)) & (V0l1 = (ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V2l)@V1l2))))))))))).
thf(conj_thm_2Erich__list_2EIS__SUBLIST__APPEND,lemma,( ! [A_27a:del]: ( ! [V0l1:$i] : ((mem@V0l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l2:$i] : ((mem@V1l2@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Erich__list_2EIS__SUBLIST@A_27a)@V0l1)@V1l2)) <=> (? [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27a)) & (? [V3l_27:$i] : ((mem@V3l_27@(ty_2Elist_2Elist@A_27a)) & (V0l1 = (ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V2l)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V1l2)@V3l_27)))))))))))))).
thf(conj_thm_2Erich__list_2EIS__PREFIX__IS__SUBLIST,lemma,( ! [A_27a:del]: ( ! [V0l1:$i] : ((mem@V0l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l2:$i] : ((mem@V1l2@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Elist_2EisPREFIX@A_27a)@V1l2)@V0l1)) => (p@(ap@(ap@(c_2Erich__list_2EIS__SUBLIST@A_27a)@V0l1)@V1l2))))))))).
thf(conj_thm_2Erich__list_2EIS__SUFFIX__IS__SUBLIST,lemma,( ! [A_27a:del]: ( ! [V0l1:$i] : ((mem@V0l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l2:$i] : ((mem@V1l2@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Erich__list_2EIS__SUFFIX@A_27a)@V0l1)@V1l2)) => (p@(ap@(ap@(c_2Erich__list_2EIS__SUBLIST@A_27a)@V0l1)@V1l2))))))))).
thf(conj_thm_2Erich__list_2EIS__PREFIX__REVERSE,lemma,( ! [A_27a:del]: ( ! [V0l1:$i] : ((mem@V0l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l2:$i] : ((mem@V1l2@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Elist_2EisPREFIX@A_27a)@(ap@(c_2Elist_2EREVERSE@A_27a)@V1l2))@(ap@(c_2Elist_2EREVERSE@A_27a)@V0l1))) <=> (p@(ap@(ap@(c_2Erich__list_2EIS__SUFFIX@A_27a)@V0l1)@V1l2))))))))).
thf(conj_thm_2Erich__list_2EIS__SUFFIX__REVERSE,lemma,( ! [A_27a:del]: ( ! [V0l2:$i] : ((mem@V0l2@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l1:$i] : ((mem@V1l1@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Erich__list_2EIS__SUFFIX@A_27a)@(ap@(c_2Elist_2EREVERSE@A_27a)@V1l1))@(ap@(c_2Elist_2EREVERSE@A_27a)@V0l2))) <=> (p@(ap@(ap@(c_2Elist_2EisPREFIX@A_27a)@V0l2)@V1l1))))))))).
thf(conj_thm_2Erich__list_2EIS__SUFFIX__CONS2__E,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(ty_2Elist_2Elist@A_27a)) => ( ! [V1h:$i] : ((mem@V1h@A_27a) => ( ! [V2t:$i] : ((mem@V2t@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Erich__list_2EIS__SUFFIX@A_27a)@V0s)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V1h)@V2t))) => (p@(ap@(ap@(c_2Erich__list_2EIS__SUFFIX@A_27a)@V0s)@V2t))))))))))).
thf(conj_thm_2Erich__list_2EIS__SUFFIX__REFL,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => (p@(ap@(ap@(c_2Erich__list_2EIS__SUFFIX@A_27a)@V0l)@V0l)))))).
thf(conj_thm_2Erich__list_2EIS__SUBLIST__REVERSE,lemma,( ! [A_27a:del]: ( ! [V0l1:$i] : ((mem@V0l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l2:$i] : ((mem@V1l2@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Erich__list_2EIS__SUBLIST@A_27a)@(ap@(c_2Elist_2EREVERSE@A_27a)@V0l1))@(ap@(c_2Elist_2EREVERSE@A_27a)@V1l2))) <=> (p@(ap@(ap@(c_2Erich__list_2EIS__SUBLIST@A_27a)@V0l1)@V1l2))))))))).
thf(conj_thm_2Erich__list_2EPREFIX__FOLDR,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Erich__list_2EPREFIX@A_27a)@V0P)@V1l) = (ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27a@(ty_2Elist_2Elist@A_27a))@(lam@A_27a@(^ [V2x:$i] : (lam@(ty_2Elist_2Elist@A_27a)@(^ [V3l_27:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Elist_2Elist@A_27a))@(ap@V0P@V2x))@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V2x)@V3l_27))@(c_2Elist_2ENIL@A_27a)))))))@(c_2Elist_2ENIL@A_27a))@V1l)))))))).
thf(conj_thm_2Erich__list_2EPREFIX,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ((ap@(ap@(c_2Erich__list_2EPREFIX@A_27a)@V0P)@(c_2Elist_2ENIL@A_27a)) = (c_2Elist_2ENIL@A_27a)))) & ( ! [V1P:$i] : ((mem@V1P@(arr@A_27b@bool)) => ( ! [V2x:$i] : ((mem@V2x@A_27b) => ( ! [V3l:$i] : ((mem@V3l@(ty_2Elist_2Elist@A_27b)) => ((ap@(ap@(c_2Erich__list_2EPREFIX@A_27b)@V1P)@(ap@(ap@(c_2Elist_2ECONS@A_27b)@V2x)@V3l)) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Elist_2Elist@A_27b))@(ap@V1P@V2x))@(ap@(ap@(c_2Elist_2ECONS@A_27b)@V2x)@(ap@(ap@(c_2Erich__list_2EPREFIX@A_27b)@V1P)@V3l)))@(c_2Elist_2ENIL@A_27b))))))))))))).
thf(conj_thm_2Erich__list_2EIS__PREFIX__PREFIX,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => (p@(ap@(ap@(c_2Elist_2EisPREFIX@A_27a)@(ap@(ap@(c_2Erich__list_2EPREFIX@A_27a)@V0P)@V1l))@V1l)))))))).
thf(conj_thm_2Erich__list_2ELENGTH__SCANL,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(arr@A_27b@A_27a))) => ( ! [V1e:$i] : ((mem@V1e@A_27a) => ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27b)) => ((surj__ty_2Enum_2Enum @ (ap@(c_2Elist_2ELENGTH@A_27a)@(ap@(ap@(ap@(c_2Erich__list_2ESCANL@A_27b@A_27a)@V0f)@V1e)@V2l))) = (surj__ty_2Enum_2Enum @ (ap@c_2Enum_2ESUC@(ap@(c_2Elist_2ELENGTH@A_27b)@V2l))))))))))))).
thf(conj_thm_2Erich__list_2ELENGTH__SCANR,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(arr@A_27b@A_27b))) => ( ! [V1e:$i] : ((mem@V1e@A_27b) => ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27a)) => ((surj__ty_2Enum_2Enum @ (ap@(c_2Elist_2ELENGTH@A_27b)@(ap@(ap@(ap@(c_2Erich__list_2ESCANR@A_27a@A_27b)@V0f)@V1e)@V2l))) = (surj__ty_2Enum_2Enum @ (ap@c_2Enum_2ESUC@(ap@(c_2Elist_2ELENGTH@A_27a)@V2l))))))))))))).
thf(conj_thm_2Erich__list_2ECOMM__MONOID__FOLDL,lemma,( ! [A_27a:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(arr@A_27a@A_27a))) => ((p@(ap@(c_2Ecombin_2ECOMM@A_27a@A_27a)@V0f)) => ( ! [V1e_27:$i] : ((mem@V1e_27@A_27a) => ((p@(ap@(ap@(c_2Ecombin_2EMONOID@A_27a)@V0f)@V1e_27)) => ( ! [V2e:$i] : ((mem@V2e@A_27a) => ( ! [V3l:$i] : ((mem@V3l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(ap@(c_2Elist_2EFOLDL@A_27a@A_27a)@V0f)@V2e)@V3l) = (ap@(ap@V0f@V2e)@(ap@(ap@(ap@(c_2Elist_2EFOLDL@A_27a@A_27a)@V0f)@V1e_27)@V3l))))))))))))))).
thf(conj_thm_2Erich__list_2ECOMM__MONOID__FOLDR,lemma,( ! [A_27a:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(arr@A_27a@A_27a))) => ((p@(ap@(c_2Ecombin_2ECOMM@A_27a@A_27a)@V0f)) => ( ! [V1e_27:$i] : ((mem@V1e_27@A_27a) => ((p@(ap@(ap@(c_2Ecombin_2EMONOID@A_27a)@V0f)@V1e_27)) => ( ! [V2e:$i] : ((mem@V2e@A_27a) => ( ! [V3l:$i] : ((mem@V3l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27a@A_27a)@V0f)@V2e)@V3l) = (ap@(ap@V0f@V2e)@(ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27a@A_27a)@V0f)@V1e_27)@V3l))))))))))))))).
thf(conj_thm_2Erich__list_2EFCOMM__FOLDR__APPEND,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0g:$i] : ((mem@V0g@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27b@(arr@A_27a@A_27a))) => ((p@(ap@(ap@(c_2Ecombin_2EFCOMM@A_27a@A_27a@A_27b)@V0g)@V1f)) => ( ! [V2e:$i] : ((mem@V2e@A_27a) => ((p@(ap@(ap@(c_2Ecombin_2ELEFT__ID@A_27a@A_27a)@V0g)@V2e)) => ( ! [V3l1:$i] : ((mem@V3l1@(ty_2Elist_2Elist@A_27b)) => ( ! [V4l2:$i] : ((mem@V4l2@(ty_2Elist_2Elist@A_27b)) => ((ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27b@A_27a)@V1f)@V2e)@(ap@(ap@(c_2Elist_2EAPPEND@A_27b)@V3l1)@V4l2)) = (ap@(ap@V0g@(ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27b@A_27a)@V1f)@V2e)@V3l1))@(ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27b@A_27a)@V1f)@V2e)@V4l2)))))))))))))))))).
thf(conj_thm_2Erich__list_2EFCOMM__FOLDL__APPEND,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(arr@A_27b@A_27a))) => ( ! [V1g:$i] : ((mem@V1g@(arr@A_27a@(arr@A_27a@A_27a))) => ((p@(ap@(ap@(c_2Ecombin_2EFCOMM@A_27a@A_27b@A_27a)@V0f)@V1g)) => ( ! [V2e:$i] : ((mem@V2e@A_27a) => ((p@(ap@(ap@(c_2Ecombin_2ERIGHT__ID@A_27a@A_27a)@V1g)@V2e)) => ( ! [V3l1:$i] : ((mem@V3l1@(ty_2Elist_2Elist@A_27b)) => ( ! [V4l2:$i] : ((mem@V4l2@(ty_2Elist_2Elist@A_27b)) => ((ap@(ap@(ap@(c_2Elist_2EFOLDL@A_27b@A_27a)@V0f)@V2e)@(ap@(ap@(c_2Elist_2EAPPEND@A_27b)@V3l1)@V4l2)) = (ap@(ap@V1g@(ap@(ap@(ap@(c_2Elist_2EFOLDL@A_27b@A_27a)@V0f)@V2e)@V3l1))@(ap@(ap@(ap@(c_2Elist_2EFOLDL@A_27b@A_27a)@V0f)@V2e)@V4l2)))))))))))))))))).
thf(conj_thm_2Erich__list_2EFOLDL__SINGLE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(arr@A_27b@A_27a))) => ( ! [V1e:$i] : ((mem@V1e@A_27a) => ( ! [V2x:$i] : ((mem@V2x@A_27b) => ((ap@(ap@(ap@(c_2Elist_2EFOLDL@A_27b@A_27a)@V0f)@V1e)@(ap@(ap@(c_2Elist_2ECONS@A_27b)@V2x)@(c_2Elist_2ENIL@A_27b))) = (ap@(ap@V0f@V1e)@V2x))))))))))).
thf(conj_thm_2Erich__list_2EFOLDR__SINGLE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(arr@A_27b@A_27b))) => ( ! [V1e:$i] : ((mem@V1e@A_27b) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27a@A_27b)@V0f)@V1e)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V2x)@(c_2Elist_2ENIL@A_27a))) = (ap@(ap@V0f@V2x)@V1e))))))))))).
thf(conj_thm_2Erich__list_2EFOLDR__CONS__NIL,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27a@(ty_2Elist_2Elist@A_27a))@(c_2Elist_2ECONS@A_27a))@(c_2Elist_2ENIL@A_27a))@V0l) = V0l))))).
thf(conj_thm_2Erich__list_2EFOLDL__SNOC__NIL,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(ap@(c_2Elist_2EFOLDL@A_27a@(ty_2Elist_2Elist@A_27a))@(lam@(ty_2Elist_2Elist@A_27a)@(^ [V1xs:$i] : (lam@A_27a@(^ [V2x:$i] : (ap@(ap@(c_2Elist_2ESNOC@A_27a)@V2x)@V1xs))))))@(c_2Elist_2ENIL@A_27a))@V0l) = V0l))))).
thf(conj_thm_2Erich__list_2EFOLDR__FOLDL__REVERSE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(arr@A_27b@A_27b))) => ( ! [V1e:$i] : ((mem@V1e@A_27b) => ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27a@A_27b)@V0f)@V1e)@V2l) = (ap@(ap@(ap@(c_2Elist_2EFOLDL@A_27a@A_27b)@(lam@A_27b@(^ [V3x:$i] : (lam@A_27a@(^ [V4y:$i] : (ap@(ap@V0f@V4y)@V3x))))))@V1e)@(ap@(c_2Elist_2EREVERSE@A_27a)@V2l)))))))))))).
thf(conj_thm_2Erich__list_2EFOLDL__FOLDR__REVERSE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(arr@A_27b@A_27a))) => ( ! [V1e:$i] : ((mem@V1e@A_27a) => ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27b)) => ((ap@(ap@(ap@(c_2Elist_2EFOLDL@A_27b@A_27a)@V0f)@V1e)@V2l) = (ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27b@A_27a)@(lam@A_27b@(^ [V3x:$i] : (lam@A_27a@(^ [V4y:$i] : (ap@(ap@V0f@V4y)@V3x))))))@V1e)@(ap@(c_2Elist_2EREVERSE@A_27b)@V2l)))))))))))).
thf(conj_thm_2Erich__list_2EFOLDR__REVERSE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(arr@A_27b@A_27b))) => ( ! [V1e:$i] : ((mem@V1e@A_27b) => ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27a@A_27b)@V0f)@V1e)@(ap@(c_2Elist_2EREVERSE@A_27a)@V2l)) = (ap@(ap@(ap@(c_2Elist_2EFOLDL@A_27a@A_27b)@(lam@A_27b@(^ [V3x:$i] : (lam@A_27a@(^ [V4y:$i] : (ap@(ap@V0f@V4y)@V3x))))))@V1e)@V2l))))))))))).
thf(conj_thm_2Erich__list_2EFOLDL__REVERSE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(arr@A_27b@A_27a))) => ( ! [V1e:$i] : ((mem@V1e@A_27a) => ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27b)) => ((ap@(ap@(ap@(c_2Elist_2EFOLDL@A_27b@A_27a)@V0f)@V1e)@(ap@(c_2Elist_2EREVERSE@A_27b)@V2l)) = (ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27b@A_27a)@(lam@A_27b@(^ [V3x:$i] : (lam@A_27a@(^ [V4y:$i] : (ap@(ap@V0f@V4y)@V3x))))))@V1e)@V2l))))))))))).
thf(conj_thm_2Erich__list_2EFOLDR__MAP,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(arr@A_27b@A_27b))) => ( ! [V1e:$i] : ((mem@V1e@A_27b) => ( ! [V2g:$i] : ((mem@V2g@(arr@A_27c@A_27a)) => ( ! [V3l:$i] : ((mem@V3l@(ty_2Elist_2Elist@A_27c)) => ((ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27a@A_27b)@V0f)@V1e)@(ap@(ap@(c_2Elist_2EMAP@A_27c@A_27a)@V2g)@V3l)) = (ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27c@A_27b)@(lam@A_27c@(^ [V4x:$i] : (lam@A_27b@(^ [V5y:$i] : (ap@(ap@V0f@(ap@V2g@V4x))@V5y))))))@V1e)@V3l)))))))))))))).
thf(conj_thm_2Erich__list_2EFOLDL__MAP,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(arr@A_27b@A_27a))) => ( ! [V1e:$i] : ((mem@V1e@A_27a) => ( ! [V2g:$i] : ((mem@V2g@(arr@A_27c@A_27b)) => ( ! [V3l:$i] : ((mem@V3l@(ty_2Elist_2Elist@A_27c)) => ((ap@(ap@(ap@(c_2Elist_2EFOLDL@A_27b@A_27a)@V0f)@V1e)@(ap@(ap@(c_2Elist_2EMAP@A_27c@A_27b)@V2g)@V3l)) = (ap@(ap@(ap@(c_2Elist_2EFOLDL@A_27c@A_27a)@(lam@A_27a@(^ [V4x:$i] : (lam@A_27c@(^ [V5y:$i] : (ap@(ap@V0f@V4x)@(ap@V2g@V5y)))))))@V1e)@V3l)))))))))))))).
thf(conj_thm_2Erich__list_2EEVERY__FOLDR,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Elist_2EEVERY@A_27a)@V0P)@V1l)) <=> (p@(ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27a@bool)@(lam@A_27a@(^ [V2x:$i] : (lam@bool@(^ [V3l_27:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0P@V2x))@V3l_27))))))@c_2Ebool_2ET)@V1l))))))))).
thf(conj_thm_2Erich__list_2EEVERY__FOLDL,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Elist_2EEVERY@A_27a)@V0P)@V1l)) <=> (p@(ap@(ap@(ap@(c_2Elist_2EFOLDL@A_27a@bool)@(lam@bool@(^ [V2l_27:$i] : (lam@A_27a@(^ [V3x:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@V2l_27)@(ap@V0P@V3x)))))))@c_2Ebool_2ET)@V1l))))))))).
thf(conj_thm_2Erich__list_2EEXISTS__FOLDR,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Elist_2EEXISTS@A_27a)@V0P)@V1l)) <=> (p@(ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27a@bool)@(lam@A_27a@(^ [V2x:$i] : (lam@bool@(^ [V3l_27:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0P@V2x))@V3l_27))))))@c_2Ebool_2EF)@V1l))))))))).
thf(conj_thm_2Erich__list_2EEXISTS__FOLDL,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Elist_2EEXISTS@A_27a)@V0P)@V1l)) <=> (p@(ap@(ap@(ap@(c_2Elist_2EFOLDL@A_27a@bool)@(lam@bool@(^ [V2l_27:$i] : (lam@A_27a@(^ [V3x:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@V2l_27)@(ap@V0P@V3x)))))))@c_2Ebool_2EF)@V1l))))))))).
thf(conj_thm_2Erich__list_2EEVERY__FOLDR__MAP,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Elist_2EEVERY@A_27a)@V0P)@V1l)) <=> (p@(ap@(ap@(ap@(c_2Elist_2EFOLDR@bool@bool)@c_2Ebool_2E_2F_5C)@c_2Ebool_2ET)@(ap@(ap@(c_2Elist_2EMAP@A_27a@bool)@V0P)@V1l)))))))))).
thf(conj_thm_2Erich__list_2EEVERY__FOLDL__MAP,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Elist_2EEVERY@A_27a)@V0P)@V1l)) <=> (p@(ap@(ap@(ap@(c_2Elist_2EFOLDL@bool@bool)@c_2Ebool_2E_2F_5C)@c_2Ebool_2ET)@(ap@(ap@(c_2Elist_2EMAP@A_27a@bool)@V0P)@V1l)))))))))).
thf(conj_thm_2Erich__list_2EEXISTS__FOLDR__MAP,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Elist_2EEXISTS@A_27a)@V0P)@V1l)) <=> (p@(ap@(ap@(ap@(c_2Elist_2EFOLDR@bool@bool)@c_2Ebool_2E_5C_2F)@c_2Ebool_2EF)@(ap@(ap@(c_2Elist_2EMAP@A_27a@bool)@V0P)@V1l)))))))))).
thf(conj_thm_2Erich__list_2EEXISTS__FOLDL__MAP,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Elist_2EEXISTS@A_27a)@V0P)@V1l)) <=> (p@(ap@(ap@(ap@(c_2Elist_2EFOLDL@bool@bool)@c_2Ebool_2E_5C_2F)@c_2Ebool_2EF)@(ap@(ap@(c_2Elist_2EMAP@A_27a@bool)@V0P)@V1l)))))))))).
thf(conj_thm_2Erich__list_2EFOLDR__FILTER,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(arr@A_27b@A_27b))) => ( ! [V1e:$i] : ((mem@V1e@A_27b) => ( ! [V2P:$i] : ((mem@V2P@(arr@A_27a@bool)) => ( ! [V3l:$i] : ((mem@V3l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27a@A_27b)@V0f)@V1e)@(ap@(ap@(c_2Elist_2EFILTER@A_27a)@V2P)@V3l)) = (ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27a@A_27b)@(lam@A_27a@(^ [V4x:$i] : (lam@A_27b@(^ [V5y:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@A_27b)@(ap@V2P@V4x))@(ap@(ap@V0f@V4x)@V5y))@V5y))))))@V1e)@V3l))))))))))))).
thf(conj_thm_2Erich__list_2EFOLDL__FILTER,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(arr@A_27b@A_27a))) => ( ! [V1e:$i] : ((mem@V1e@A_27a) => ( ! [V2P:$i] : ((mem@V2P@(arr@A_27b@bool)) => ( ! [V3l:$i] : ((mem@V3l@(ty_2Elist_2Elist@A_27b)) => ((ap@(ap@(ap@(c_2Elist_2EFOLDL@A_27b@A_27a)@V0f)@V1e)@(ap@(ap@(c_2Elist_2EFILTER@A_27b)@V2P)@V3l)) = (ap@(ap@(ap@(c_2Elist_2EFOLDL@A_27b@A_27a)@(lam@A_27a@(^ [V4x:$i] : (lam@A_27b@(^ [V5y:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@A_27a)@(ap@V2P@V5y))@(ap@(ap@V0f@V4x)@V5y))@V4x))))))@V1e)@V3l))))))))))))).
thf(conj_thm_2Erich__list_2EASSOC__FOLDR__FLAT,lemma,( ! [A_27a:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(arr@A_27a@A_27a))) => ((p@(ap@(c_2Ecombin_2EASSOC@A_27a)@V0f)) => ( ! [V1e:$i] : ((mem@V1e@A_27a) => ((p@(ap@(ap@(c_2Ecombin_2ELEFT__ID@A_27a@A_27a)@V0f)@V1e)) => ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@(ty_2Elist_2Elist@A_27a))) => ((ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27a@A_27a)@V0f)@V1e)@(ap@(c_2Elist_2EFLAT@A_27a)@V2l)) = (ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27a@A_27a)@V0f)@V1e)@(ap@(ap@(c_2Elist_2EMAP@(ty_2Elist_2Elist@A_27a)@A_27a)@(ap@(ap@(c_2Elist_2EFOLDR@A_27a@A_27a)@V0f)@V1e))@V2l))))))))))))).
thf(conj_thm_2Erich__list_2EASSOC__FOLDL__FLAT,lemma,( ! [A_27a:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(arr@A_27a@A_27a))) => ((p@(ap@(c_2Ecombin_2EASSOC@A_27a)@V0f)) => ( ! [V1e:$i] : ((mem@V1e@A_27a) => ((p@(ap@(ap@(c_2Ecombin_2ERIGHT__ID@A_27a@A_27a)@V0f)@V1e)) => ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@(ty_2Elist_2Elist@A_27a))) => ((ap@(ap@(ap@(c_2Elist_2EFOLDL@A_27a@A_27a)@V0f)@V1e)@(ap@(c_2Elist_2EFLAT@A_27a)@V2l)) = (ap@(ap@(ap@(c_2Elist_2EFOLDL@A_27a@A_27a)@V0f)@V1e)@(ap@(ap@(c_2Elist_2EMAP@(ty_2Elist_2Elist@A_27a)@A_27a)@(ap@(ap@(c_2Elist_2EFOLDL@A_27a@A_27a)@V0f)@V1e))@V2l))))))))))))).
thf(conj_thm_2Erich__list_2EMAP__FLAT,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@(ty_2Elist_2Elist@A_27a))) => ((ap@(ap@(c_2Elist_2EMAP@A_27a@A_27b)@V0f)@(ap@(c_2Elist_2EFLAT@A_27a)@V1l)) = (ap@(c_2Elist_2EFLAT@A_27b)@(ap@(ap@(c_2Elist_2EMAP@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27b))@(ap@(c_2Elist_2EMAP@A_27a@A_27b)@V0f))@V1l)))))))))).
thf(conj_thm_2Erich__list_2EFILTER__FLAT,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@(ty_2Elist_2Elist@A_27a))) => ((ap@(ap@(c_2Elist_2EFILTER@A_27a)@V0P)@(ap@(c_2Elist_2EFLAT@A_27a)@V1l)) = (ap@(c_2Elist_2EFLAT@A_27a)@(ap@(ap@(c_2Elist_2EMAP@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))@(ap@(c_2Elist_2EFILTER@A_27a)@V0P))@V1l))))))))).
thf(conj_thm_2Erich__list_2EEXISTS__DISJ,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1Q:$i] : ((mem@V1Q@(arr@A_27a@bool)) => ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Elist_2EEXISTS@A_27a)@(lam@A_27a@(^ [V3x:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@V0P@V3x))@(ap@V1Q@V3x)))))@V2l)) <=> ((p@(ap@(ap@(c_2Elist_2EEXISTS@A_27a)@V0P)@V2l)) | (p@(ap@(ap@(c_2Elist_2EEXISTS@A_27a)@V1Q)@V2l)))))))))))).
thf(conj_thm_2Erich__list_2EMEM__FOLDR,lemma,( ! [A_27a:del]: ( ! [V0y:$i] : ((mem@V0y@A_27a) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0y)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@V1l))) <=> (p@(ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27a@bool)@(lam@A_27a@(^ [V2x:$i] : (lam@bool@(^ [V3l_27:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@(c_2Emin_2E_3D@A_27a)@V0y)@V2x))@V3l_27))))))@c_2Ebool_2EF)@V1l))))))))).
thf(conj_thm_2Erich__list_2EMEM__FOLDL,lemma,( ! [A_27a:del]: ( ! [V0y:$i] : ((mem@V0y@A_27a) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0y)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@V1l))) <=> (p@(ap@(ap@(ap@(c_2Elist_2EFOLDL@A_27a@bool)@(lam@bool@(^ [V2l_27:$i] : (lam@A_27a@(^ [V3x:$i] : (ap@(ap@c_2Ebool_2E_5C_2F@V2l_27)@(ap@(ap@(c_2Emin_2E_3D@A_27a)@V0y)@V3x)))))))@c_2Ebool_2EF)@V1l))))))))).
thf(conj_thm_2Erich__list_2ENULL__FOLDR,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(c_2Elist_2ENULL@A_27a)@V0l)) <=> (p@(ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27a@bool)@(lam@A_27a@(^ [V1x:$i] : (lam@bool@(^ [V2l_27:$i] : c_2Ebool_2EF)))))@c_2Ebool_2ET)@V0l))))))).
thf(conj_thm_2Erich__list_2ENULL__FOLDL,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(c_2Elist_2ENULL@A_27a)@V0l)) <=> (p@(ap@(ap@(ap@(c_2Elist_2EFOLDL@A_27a@bool)@(lam@bool@(^ [V1x:$i] : (lam@A_27a@(^ [V2l_27:$i] : c_2Ebool_2EF)))))@c_2Ebool_2ET)@V0l))))))).
thf(conj_thm_2Erich__list_2EMAP__REVERSE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Elist_2EMAP@A_27a@A_27b)@V0f)@(ap@(c_2Elist_2EREVERSE@A_27a)@V1l)) = (ap@(c_2Elist_2EREVERSE@A_27b)@(ap@(ap@(c_2Elist_2EMAP@A_27a@A_27b)@V0f)@V1l)))))))))).
thf(conj_thm_2Erich__list_2ESEG__LENGTH__ID,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(ap@(c_2Erich__list_2ESEG@A_27a)@(ap@(c_2Elist_2ELENGTH@A_27a)@V0l))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@V0l) = V0l))))).
thf(conj_thm_2Erich__list_2ESEG__SUC__CONS,lemma,( ! [A_27a:del]: ( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27a)) => ( ! [V3x:$i] : ((mem@V3x@A_27a) => ((ap@(ap@(ap@(c_2Erich__list_2ESEG@A_27a)@(inj__ty_2Enum_2Enum @ V0m))@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n)))@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V3x)@V2l)) = (ap@(ap@(ap@(c_2Erich__list_2ESEG@A_27a)@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V1n))@V2l)))))))))).
thf(conj_thm_2Erich__list_2ESEG__0__SNOC,lemma,( ! [A_27a:del]: ( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0m))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))) => ((ap@(ap@(ap@(c_2Erich__list_2ESEG@A_27a)@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@(ap@(c_2Elist_2ESNOC@A_27a)@V2x)@V1l)) = (ap@(ap@(ap@(c_2Erich__list_2ESEG@A_27a)@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@V1l)))))))))).
thf(conj_thm_2Erich__list_2EBUTLASTN__SEG,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))) => ((ap@(ap@(c_2Erich__list_2EBUTLASTN@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1l) = (ap@(ap@(ap@(c_2Erich__list_2ESEG@A_27a)@(ap@(ap@c_2Earithmetic_2E_2D@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))@(inj__ty_2Enum_2Enum @ V0n)))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@V1l)))))))).
thf(conj_thm_2Erich__list_2ELASTN__CONS,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((ap@(ap@(c_2Erich__list_2ELASTN@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V2x)@V1l)) = (ap@(ap@(c_2Erich__list_2ELASTN@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1l)))))))))).
thf(conj_thm_2Erich__list_2ELENGTH__LASTN,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))) => ((surj__ty_2Enum_2Enum @ (ap@(c_2Elist_2ELENGTH@A_27a)@(ap@(ap@(c_2Erich__list_2ELASTN@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1l))) = V0n))))))).
thf(conj_thm_2Erich__list_2ELASTN__LENGTH__ID,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Erich__list_2ELASTN@A_27a)@(ap@(c_2Elist_2ELENGTH@A_27a)@V0l))@V0l) = V0l))))).
thf(conj_thm_2Erich__list_2ELASTN__LASTN,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2m:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V2m))@(ap@(c_2Elist_2ELENGTH@A_27a)@V0l))) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V1n))@(inj__ty_2Enum_2Enum @ V2m))) => ((ap@(ap@(c_2Erich__list_2ELASTN@A_27a)@(inj__ty_2Enum_2Enum @ V1n))@(ap@(ap@(c_2Erich__list_2ELASTN@A_27a)@(inj__ty_2Enum_2Enum @ V2m))@V0l)) = (ap@(ap@(c_2Erich__list_2ELASTN@A_27a)@(inj__ty_2Enum_2Enum @ V1n))@V0l)))))))))).
thf(conj_thm_2Erich__list_2ETAKE__SNOC,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((ap@(ap@(c_2Elist_2ETAKE@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(ap@(c_2Elist_2ESNOC@A_27a)@V2x)@V1l)) = (ap@(ap@(c_2Elist_2ETAKE@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1l)))))))))).
thf(conj_thm_2Erich__list_2EBUTLASTN__SUC__FRONT,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))) => ((ap@(ap@(c_2Erich__list_2EBUTLASTN@A_27a)@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V0n)))@V1l) = (ap@(ap@(c_2Erich__list_2EBUTLASTN@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Elist_2EFRONT@A_27a)@V1l))))))))).
thf(conj_thm_2Erich__list_2EBUTLASTN__FRONT,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))) => ((ap@(ap@(c_2Erich__list_2EBUTLASTN@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Elist_2EFRONT@A_27a)@V1l)) = (ap@(c_2Elist_2EFRONT@A_27a)@(ap@(ap@(c_2Erich__list_2EBUTLASTN@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1l))))))))).
thf(conj_thm_2Erich__list_2ELENGTH__BUTLASTN,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))) => ((surj__ty_2Enum_2Enum @ (ap@(c_2Elist_2ELENGTH@A_27a)@(ap@(ap@(c_2Erich__list_2EBUTLASTN@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1l))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2D@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))@(inj__ty_2Enum_2Enum @ V0n)))))))))).
thf(conj_thm_2Erich__list_2EBUTLASTN__BUTLASTN,lemma,( ! [A_27a:del]: ( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V1n))@(inj__ty_2Enum_2Enum @ V0m)))@(ap@(c_2Elist_2ELENGTH@A_27a)@V2l))) => ((ap@(ap@(c_2Erich__list_2EBUTLASTN@A_27a)@(inj__ty_2Enum_2Enum @ V1n))@(ap@(ap@(c_2Erich__list_2EBUTLASTN@A_27a)@(inj__ty_2Enum_2Enum @ V0m))@V2l)) = (ap@(ap@(c_2Erich__list_2EBUTLASTN@A_27a)@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V1n))@(inj__ty_2Enum_2Enum @ V0m)))@V2l))))))))).
thf(conj_thm_2Erich__list_2EAPPEND__BUTLASTN__LASTN,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))) => ((ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Erich__list_2EBUTLASTN@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1l))@(ap@(ap@(c_2Erich__list_2ELASTN@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1l)) = V1l))))))).
thf(conj_thm_2Erich__list_2EAPPEND__TAKE__LASTN,lemma,( ! [A_27a:del]: ( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27a)) => (((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V1n))) = (surj__ty_2Enum_2Enum @ (ap@(c_2Elist_2ELENGTH@A_27a)@V2l))) => ((ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Elist_2ETAKE@A_27a)@(inj__ty_2Enum_2Enum @ V1n))@V2l))@(ap@(ap@(c_2Erich__list_2ELASTN@A_27a)@(inj__ty_2Enum_2Enum @ V0m))@V2l)) = V2l)))))))).
thf(conj_thm_2Erich__list_2EBUTLASTN__APPEND2,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l1:$i] : ((mem@V1l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V2l2:$i] : ((mem@V2l2@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Elist_2ELENGTH@A_27a)@V2l2))) => ((ap@(ap@(c_2Erich__list_2EBUTLASTN@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V1l1)@V2l2)) = (ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V1l1)@(ap@(ap@(c_2Erich__list_2EBUTLASTN@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V2l2))))))))))).
thf(conj_thm_2Erich__list_2EBUTLASTN__LENGTH__APPEND,lemma,( ! [A_27a:del]: ( ! [V0l2:$i] : ((mem@V0l2@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l1:$i] : ((mem@V1l1@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Erich__list_2EBUTLASTN@A_27a)@(ap@(c_2Elist_2ELENGTH@A_27a)@V0l2))@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V1l1)@V0l2)) = V1l1))))))).
thf(conj_thm_2Erich__list_2ELASTN__LENGTH__APPEND,lemma,( ! [A_27a:del]: ( ! [V0l2:$i] : ((mem@V0l2@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l1:$i] : ((mem@V1l1@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Erich__list_2ELASTN@A_27a)@(ap@(c_2Elist_2ELENGTH@A_27a)@V0l2))@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V1l1)@V0l2)) = V0l2))))))).
thf(conj_thm_2Erich__list_2EBUTLASTN__CONS,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((ap@(ap@(c_2Erich__list_2EBUTLASTN@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V2x)@V1l)) = (ap@(ap@(c_2Elist_2ECONS@A_27a)@V2x)@(ap@(ap@(c_2Erich__list_2EBUTLASTN@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1l))))))))))).
thf(conj_thm_2Erich__list_2EBUTLASTN__LENGTH__CONS,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ((ap@(ap@(c_2Erich__list_2EBUTLASTN@A_27a)@(ap@(c_2Elist_2ELENGTH@A_27a)@V0l))@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V1x)@V0l)) = (ap@(ap@(c_2Elist_2ECONS@A_27a)@V1x)@(c_2Elist_2ENIL@A_27a))))))))).
thf(conj_thm_2Erich__list_2ELAST__LASTN__LAST,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))) => ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V0n))) => ((ap@(c_2Elist_2ELAST@A_27a)@(ap@(ap@(c_2Erich__list_2ELASTN@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1l)) = (ap@(c_2Elist_2ELAST@A_27a)@V1l))))))))).
thf(conj_thm_2Erich__list_2EBUTLASTN__LASTN__NIL,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))) => ((ap@(ap@(c_2Erich__list_2EBUTLASTN@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(ap@(c_2Erich__list_2ELASTN@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1l)) = (c_2Elist_2ENIL@A_27a)))))))).
thf(conj_thm_2Erich__list_2ELASTN__BUTLASTN,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m)))@(ap@(c_2Elist_2ELENGTH@A_27a)@V2l))) => ((ap@(ap@(c_2Erich__list_2ELASTN@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(ap@(c_2Erich__list_2EBUTLASTN@A_27a)@(inj__ty_2Enum_2Enum @ V1m))@V2l)) = (ap@(ap@(c_2Erich__list_2EBUTLASTN@A_27a)@(inj__ty_2Enum_2Enum @ V1m))@(ap@(ap@(c_2Erich__list_2ELASTN@A_27a)@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m)))@V2l)))))))))).
thf(conj_thm_2Erich__list_2EBUTLASTN__LASTN,lemma,( ! [A_27a:del]: ( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27a)) => (((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V1n))) & (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V1n))@(ap@(c_2Elist_2ELENGTH@A_27a)@V2l)))) => ((ap@(ap@(c_2Erich__list_2EBUTLASTN@A_27a)@(inj__ty_2Enum_2Enum @ V0m))@(ap@(ap@(c_2Erich__list_2ELASTN@A_27a)@(inj__ty_2Enum_2Enum @ V1n))@V2l)) = (ap@(ap@(c_2Erich__list_2ELASTN@A_27a)@(ap@(ap@c_2Earithmetic_2E_2D@(inj__ty_2Enum_2Enum @ V1n))@(inj__ty_2Enum_2Enum @ V0m)))@(ap@(ap@(c_2Erich__list_2EBUTLASTN@A_27a)@(inj__ty_2Enum_2Enum @ V0m))@V2l)))))))))).
thf(conj_thm_2Erich__list_2ELASTN__1,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ((~~ (V0l = (c_2Elist_2ENIL@A_27a))) => ((ap@(ap@(c_2Erich__list_2ELASTN@A_27a)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@V0l) = (ap@(ap@(c_2Elist_2ECONS@A_27a)@(ap@(c_2Elist_2ELAST@A_27a)@V0l))@(c_2Elist_2ENIL@A_27a)))))))).
thf(conj_thm_2Erich__list_2EBUTLASTN__1,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ((~~ (V0l = (c_2Elist_2ENIL@A_27a))) => ((ap@(ap@(c_2Erich__list_2EBUTLASTN@A_27a)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@V0l) = (ap@(c_2Elist_2EFRONT@A_27a)@V0l))))))).
thf(conj_thm_2Erich__list_2EBUTLASTN__APPEND1,lemma,( ! [A_27a:del]: ( ! [V0l2:$i] : ((mem@V0l2@(ty_2Elist_2Elist@A_27a)) => ( ! [V1n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(c_2Elist_2ELENGTH@A_27a)@V0l2))@(inj__ty_2Enum_2Enum @ V1n))) => ( ! [V2l1:$i] : ((mem@V2l1@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Erich__list_2EBUTLASTN@A_27a)@(inj__ty_2Enum_2Enum @ V1n))@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V2l1)@V0l2)) = (ap@(ap@(c_2Erich__list_2EBUTLASTN@A_27a)@(ap@(ap@c_2Earithmetic_2E_2D@(inj__ty_2Enum_2Enum @ V1n))@(ap@(c_2Elist_2ELENGTH@A_27a)@V0l2)))@V2l1)))))))))).
thf(conj_thm_2Erich__list_2ELASTN__APPEND2,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l2:$i] : ((mem@V1l2@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l2))) => ( ! [V2l1:$i] : ((mem@V2l1@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Erich__list_2ELASTN@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V2l1)@V1l2)) = (ap@(ap@(c_2Erich__list_2ELASTN@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1l2)))))))))).
thf(conj_thm_2Erich__list_2ELASTN__APPEND1,lemma,( ! [A_27a:del]: ( ! [V0l2:$i] : ((mem@V0l2@(ty_2Elist_2Elist@A_27a)) => ( ! [V1n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(c_2Elist_2ELENGTH@A_27a)@V0l2))@(inj__ty_2Enum_2Enum @ V1n))) => ( ! [V2l1:$i] : ((mem@V2l1@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Erich__list_2ELASTN@A_27a)@(inj__ty_2Enum_2Enum @ V1n))@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V2l1)@V0l2)) = (ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Erich__list_2ELASTN@A_27a)@(ap@(ap@c_2Earithmetic_2E_2D@(inj__ty_2Enum_2Enum @ V1n))@(ap@(c_2Elist_2ELENGTH@A_27a)@V0l2)))@V2l1))@V0l2)))))))))).
thf(conj_thm_2Erich__list_2ELASTN__MAP,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))) => ( ! [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27b)) => ((ap@(ap@(c_2Erich__list_2ELASTN@A_27b)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(ap@(c_2Elist_2EMAP@A_27a@A_27b)@V2f)@V1l)) = (ap@(ap@(c_2Elist_2EMAP@A_27a@A_27b)@V2f)@(ap@(ap@(c_2Erich__list_2ELASTN@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1l)))))))))))).
thf(conj_thm_2Erich__list_2EBUTLASTN__MAP,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))) => ( ! [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27b)) => ((ap@(ap@(c_2Erich__list_2EBUTLASTN@A_27b)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(ap@(c_2Elist_2EMAP@A_27a@A_27b)@V2f)@V1l)) = (ap@(ap@(c_2Elist_2EMAP@A_27a@A_27b)@V2f)@(ap@(ap@(c_2Erich__list_2EBUTLASTN@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1l)))))))))))).
thf(conj_thm_2Erich__list_2EEVERY__LASTN,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Elist_2EEVERY@A_27a)@V0P)@V1l)) => ( ! [V2m:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V2m))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))) => (p@(ap@(ap@(c_2Elist_2EEVERY@A_27a)@V0P)@(ap@(ap@(c_2Erich__list_2ELASTN@A_27a)@(inj__ty_2Enum_2Enum @ V2m))@V1l)))))))))))).
thf(conj_thm_2Erich__list_2EEVERY__BUTLASTN,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Elist_2EEVERY@A_27a)@V0P)@V1l)) => ( ! [V2m:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V2m))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))) => (p@(ap@(ap@(c_2Elist_2EEVERY@A_27a)@V0P)@(ap@(ap@(c_2Erich__list_2EBUTLASTN@A_27a)@(inj__ty_2Enum_2Enum @ V2m))@V1l)))))))))))).
thf(conj_thm_2Erich__list_2ETAKE__TAKE__T,lemma,( ! [A_27a:del]: ( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ( ! [V2n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V2n))@(inj__ty_2Enum_2Enum @ V0m))) => ((ap@(ap@(c_2Elist_2ETAKE@A_27a)@(inj__ty_2Enum_2Enum @ V2n))@(ap@(ap@(c_2Elist_2ETAKE@A_27a)@(inj__ty_2Enum_2Enum @ V0m))@V1l)) = (ap@(ap@(c_2Elist_2ETAKE@A_27a)@(inj__ty_2Enum_2Enum @ V2n))@V1l))))))))).
thf(conj_thm_2Erich__list_2ETAKE__TAKE,lemma,( ! [A_27a:del]: ( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0m))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))) => ( ! [V2n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V2n))@(inj__ty_2Enum_2Enum @ V0m))) => ((ap@(ap@(c_2Elist_2ETAKE@A_27a)@(inj__ty_2Enum_2Enum @ V2n))@(ap@(ap@(c_2Elist_2ETAKE@A_27a)@(inj__ty_2Enum_2Enum @ V0m))@V1l)) = (ap@(ap@(c_2Elist_2ETAKE@A_27a)@(inj__ty_2Enum_2Enum @ V2n))@V1l)))))))))).
thf(conj_thm_2Erich__list_2EDROP__LENGTH__NIL,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Elist_2EDROP@A_27a)@(ap@(c_2Elist_2ELENGTH@A_27a)@V0l))@V0l) = (c_2Elist_2ENIL@A_27a)))))).
thf(conj_thm_2Erich__list_2EBUTLASTN__LENGTH__NIL,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Erich__list_2EBUTLASTN@A_27a)@(ap@(c_2Elist_2ELENGTH@A_27a)@V0l))@V0l) = (c_2Elist_2ENIL@A_27a)))))).
thf(conj_thm_2Erich__list_2EDROP__APPEND,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l1:$i] : ((mem@V1l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V2l2:$i] : ((mem@V2l2@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Elist_2EDROP@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V1l1)@V2l2)) = (ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Elist_2EDROP@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1l1))@(ap@(ap@(c_2Elist_2EDROP@A_27a)@(ap@(ap@c_2Earithmetic_2E_2D@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l1)))@V2l2)))))))))).
thf(conj_thm_2Erich__list_2EDROP__APPEND1,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l1:$i] : ((mem@V1l1@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l1))) => ( ! [V2l2:$i] : ((mem@V2l2@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Elist_2EDROP@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V1l1)@V2l2)) = (ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Elist_2EDROP@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1l1))@V2l2)))))))))).
thf(conj_thm_2Erich__list_2EDROP__APPEND2,lemma,( ! [A_27a:del]: ( ! [V0l1:$i] : ((mem@V0l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(c_2Elist_2ELENGTH@A_27a)@V0l1))@(inj__ty_2Enum_2Enum @ V1n))) => ( ! [V2l2:$i] : ((mem@V2l2@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Elist_2EDROP@A_27a)@(inj__ty_2Enum_2Enum @ V1n))@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V0l1)@V2l2)) = (ap@(ap@(c_2Elist_2EDROP@A_27a)@(ap@(ap@c_2Earithmetic_2E_2D@(inj__ty_2Enum_2Enum @ V1n))@(ap@(c_2Elist_2ELENGTH@A_27a)@V0l1)))@V2l2)))))))))).
thf(conj_thm_2Erich__list_2EDROP__DROP__T,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Elist_2EDROP@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(ap@(c_2Elist_2EDROP@A_27a)@(inj__ty_2Enum_2Enum @ V1m))@V2l)) = (ap@(ap@(c_2Elist_2EDROP@A_27a)@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m)))@V2l)))))))).
thf(conj_thm_2Erich__list_2EDROP__DROP,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m)))@(ap@(c_2Elist_2ELENGTH@A_27a)@V2l))) => ((ap@(ap@(c_2Elist_2EDROP@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(ap@(c_2Elist_2EDROP@A_27a)@(inj__ty_2Enum_2Enum @ V1m))@V2l)) = (ap@(ap@(c_2Elist_2EDROP@A_27a)@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m)))@V2l))))))))).
thf(conj_thm_2Erich__list_2ELASTN__SEG,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))) => ((ap@(ap@(c_2Erich__list_2ELASTN@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1l) = (ap@(ap@(ap@(c_2Erich__list_2ESEG@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(ap@c_2Earithmetic_2E_2D@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))@(inj__ty_2Enum_2Enum @ V0n)))@V1l)))))))).
thf(conj_thm_2Erich__list_2ETAKE__SEG,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))) => ((ap@(ap@(c_2Elist_2ETAKE@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1l) = (ap@(ap@(ap@(c_2Erich__list_2ESEG@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@V1l)))))))).
thf(conj_thm_2Erich__list_2EDROP__SEG,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))) => ((ap@(ap@(c_2Elist_2EDROP@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1l) = (ap@(ap@(ap@(c_2Erich__list_2ESEG@A_27a)@(ap@(ap@c_2Earithmetic_2E_2D@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))@(inj__ty_2Enum_2Enum @ V0n)))@(inj__ty_2Enum_2Enum @ V0n))@V1l)))))))).
thf(conj_thm_2Erich__list_2EDROP__SNOC,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((ap@(ap@(c_2Elist_2EDROP@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(ap@(c_2Elist_2ESNOC@A_27a)@V2x)@V1l)) = (ap@(ap@(c_2Elist_2ESNOC@A_27a)@V2x)@(ap@(ap@(c_2Elist_2EDROP@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1l))))))))))).
thf(conj_thm_2Erich__list_2EAPPEND__BUTLASTN__DROP,lemma,( ! [A_27a:del]: ( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27a)) => (((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V1n))) = (surj__ty_2Enum_2Enum @ (ap@(c_2Elist_2ELENGTH@A_27a)@V2l))) => ((ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Erich__list_2EBUTLASTN@A_27a)@(inj__ty_2Enum_2Enum @ V0m))@V2l))@(ap@(ap@(c_2Elist_2EDROP@A_27a)@(inj__ty_2Enum_2Enum @ V1n))@V2l)) = V2l)))))))).
thf(conj_thm_2Erich__list_2ESEG__SEG,lemma,( ! [A_27a:del]: ( ! [V0n1:tp__ty_2Enum_2Enum] : ( ! [V1m1:tp__ty_2Enum_2Enum] : ( ! [V2n2:tp__ty_2Enum_2Enum] : ( ! [V3m2:tp__ty_2Enum_2Enum] : ( ! [V4l:$i] : ((mem@V4l@(ty_2Elist_2Elist@A_27a)) => (((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0n1))@(inj__ty_2Enum_2Enum @ V1m1)))@(ap@(c_2Elist_2ELENGTH@A_27a)@V4l))) & (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V2n2))@(inj__ty_2Enum_2Enum @ V3m2)))@(inj__ty_2Enum_2Enum @ V0n1)))) => ((ap@(ap@(ap@(c_2Erich__list_2ESEG@A_27a)@(inj__ty_2Enum_2Enum @ V2n2))@(inj__ty_2Enum_2Enum @ V3m2))@(ap@(ap@(ap@(c_2Erich__list_2ESEG@A_27a)@(inj__ty_2Enum_2Enum @ V0n1))@(inj__ty_2Enum_2Enum @ V1m1))@V4l)) = (ap@(ap@(ap@(c_2Erich__list_2ESEG@A_27a)@(inj__ty_2Enum_2Enum @ V2n2))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V1m1))@(inj__ty_2Enum_2Enum @ V3m2)))@V4l))))))))))).
thf(conj_thm_2Erich__list_2ESEG__APPEND1,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2l1:$i] : ((mem@V2l1@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m)))@(ap@(c_2Elist_2ELENGTH@A_27a)@V2l1))) => ( ! [V3l2:$i] : ((mem@V3l2@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(ap@(c_2Erich__list_2ESEG@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m))@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V2l1)@V3l2)) = (ap@(ap@(ap@(c_2Erich__list_2ESEG@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m))@V2l1))))))))))).
thf(conj_thm_2Erich__list_2ESEG__APPEND2,lemma,( ! [A_27a:del]: ( ! [V0l1:$i] : ((mem@V0l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : ( ! [V3l2:$i] : ((mem@V3l2@(ty_2Elist_2Elist@A_27a)) => (((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(c_2Elist_2ELENGTH@A_27a)@V0l1))@(inj__ty_2Enum_2Enum @ V1m))) & (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V2n))@(ap@(c_2Elist_2ELENGTH@A_27a)@V3l2)))) => ((ap@(ap@(ap@(c_2Erich__list_2ESEG@A_27a)@(inj__ty_2Enum_2Enum @ V2n))@(inj__ty_2Enum_2Enum @ V1m))@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V0l1)@V3l2)) = (ap@(ap@(ap@(c_2Erich__list_2ESEG@A_27a)@(inj__ty_2Enum_2Enum @ V2n))@(ap@(ap@c_2Earithmetic_2E_2D@(inj__ty_2Enum_2Enum @ V1m))@(ap@(c_2Elist_2ELENGTH@A_27a)@V0l1)))@V3l2))))))))))).
thf(conj_thm_2Erich__list_2ESEG__TAKE__DROP,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m)))@(ap@(c_2Elist_2ELENGTH@A_27a)@V2l))) => ((ap@(ap@(ap@(c_2Erich__list_2ESEG@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m))@V2l) = (ap@(ap@(c_2Elist_2ETAKE@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(ap@(c_2Elist_2EDROP@A_27a)@(inj__ty_2Enum_2Enum @ V1m))@V2l)))))))))).
thf(conj_thm_2Erich__list_2ESEG__APPEND,lemma,( ! [A_27a:del]: ( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1l1:$i] : ((mem@V1l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V2n:tp__ty_2Enum_2Enum] : ( ! [V3l2:$i] : ((mem@V3l2@(ty_2Elist_2Elist@A_27a)) => (((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0m))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l1))) & ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l1))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V2n))@(inj__ty_2Enum_2Enum @ V0m)))) & (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V2n))@(inj__ty_2Enum_2Enum @ V0m)))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l1))@(ap@(c_2Elist_2ELENGTH@A_27a)@V3l2)))))) => ((ap@(ap@(ap@(c_2Erich__list_2ESEG@A_27a)@(inj__ty_2Enum_2Enum @ V2n))@(inj__ty_2Enum_2Enum @ V0m))@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V1l1)@V3l2)) = (ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(ap@(c_2Erich__list_2ESEG@A_27a)@(ap@(ap@c_2Earithmetic_2E_2D@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l1))@(inj__ty_2Enum_2Enum @ V0m)))@(inj__ty_2Enum_2Enum @ V0m))@V1l1))@(ap@(ap@(ap@(c_2Erich__list_2ESEG@A_27a)@(ap@(ap@c_2Earithmetic_2E_2D@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V2n))@(inj__ty_2Enum_2Enum @ V0m)))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l1)))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@V3l2)))))))))))).
thf(conj_thm_2Erich__list_2ESEG__LENGTH__SNOC,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ((ap@(ap@(ap@(c_2Erich__list_2ESEG@A_27a)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(ap@(c_2Elist_2ELENGTH@A_27a)@V0l))@(ap@(ap@(c_2Elist_2ESNOC@A_27a)@V1x)@V0l)) = (ap@(ap@(c_2Elist_2ECONS@A_27a)@V1x)@(c_2Elist_2ENIL@A_27a))))))))).
thf(conj_thm_2Erich__list_2ESEG__SNOC,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m)))@(ap@(c_2Elist_2ELENGTH@A_27a)@V2l))) => ( ! [V3x:$i] : ((mem@V3x@A_27a) => ((ap@(ap@(ap@(c_2Erich__list_2ESEG@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m))@(ap@(ap@(c_2Elist_2ESNOC@A_27a)@V3x)@V2l)) = (ap@(ap@(ap@(c_2Erich__list_2ESEG@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m))@V2l))))))))))).
thf(conj_thm_2Erich__list_2EELL__SEG,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))) => ((ap@(ap@(c_2Erich__list_2EELL@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1l) = (ap@(c_2Elist_2EHD@A_27a)@(ap@(ap@(ap@(c_2Erich__list_2ESEG@A_27a)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(ap@c_2Eprim__rec_2EPRE@(ap@(ap@c_2Earithmetic_2E_2D@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))@(inj__ty_2Enum_2Enum @ V0n))))@V1l))))))))).
thf(conj_thm_2Erich__list_2ESNOC__FOLDR,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Elist_2ESNOC@A_27a)@V0x)@V1l) = (ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27a@(ty_2Elist_2Elist@A_27a))@(c_2Elist_2ECONS@A_27a))@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V0x)@(c_2Elist_2ENIL@A_27a)))@V1l)))))))).
thf(conj_thm_2Erich__list_2EMEM__FOLDR__MAP,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@V1l))) <=> (p@(ap@(ap@(ap@(c_2Elist_2EFOLDR@bool@bool)@c_2Ebool_2E_5C_2F)@c_2Ebool_2EF)@(ap@(ap@(c_2Elist_2EMAP@A_27a@bool)@(ap@(c_2Emin_2E_3D@A_27a)@V0x))@V1l)))))))))).
thf(conj_thm_2Erich__list_2EMEM__FOLDL__MAP,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@V1l))) <=> (p@(ap@(ap@(ap@(c_2Elist_2EFOLDL@bool@bool)@c_2Ebool_2E_5C_2F)@c_2Ebool_2EF)@(ap@(ap@(c_2Elist_2EMAP@A_27a@bool)@(ap@(c_2Emin_2E_3D@A_27a)@V0x))@V1l)))))))))).
thf(conj_thm_2Erich__list_2EFILTER__FILTER,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1Q:$i] : ((mem@V1Q@(arr@A_27a@bool)) => ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Elist_2EFILTER@A_27a)@V0P)@(ap@(ap@(c_2Elist_2EFILTER@A_27a)@V1Q)@V2l)) = (ap@(ap@(c_2Elist_2EFILTER@A_27a)@(lam@A_27a@(^ [V3x:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0P@V3x))@(ap@V1Q@V3x)))))@V2l)))))))))).
thf(conj_thm_2Erich__list_2EFCOMM__FOLDR__FLAT,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0g:$i] : ((mem@V0g@(arr@A_27a@(arr@A_27a@A_27a))) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27b@(arr@A_27a@A_27a))) => ((p@(ap@(ap@(c_2Ecombin_2EFCOMM@A_27a@A_27a@A_27b)@V0g)@V1f)) => ( ! [V2e:$i] : ((mem@V2e@A_27a) => ((p@(ap@(ap@(c_2Ecombin_2ELEFT__ID@A_27a@A_27a)@V0g)@V2e)) => ( ! [V3l:$i] : ((mem@V3l@(ty_2Elist_2Elist@(ty_2Elist_2Elist@A_27b))) => ((ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27b@A_27a)@V1f)@V2e)@(ap@(c_2Elist_2EFLAT@A_27b)@V3l)) = (ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27a@A_27a)@V0g)@V2e)@(ap@(ap@(c_2Elist_2EMAP@(ty_2Elist_2Elist@A_27b)@A_27a)@(ap@(ap@(c_2Elist_2EFOLDR@A_27b@A_27a)@V1f)@V2e))@V3l)))))))))))))))).
thf(conj_thm_2Erich__list_2EFCOMM__FOLDL__FLAT,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(arr@A_27b@A_27a))) => ( ! [V1g:$i] : ((mem@V1g@(arr@A_27a@(arr@A_27a@A_27a))) => ((p@(ap@(ap@(c_2Ecombin_2EFCOMM@A_27a@A_27b@A_27a)@V0f)@V1g)) => ( ! [V2e:$i] : ((mem@V2e@A_27a) => ((p@(ap@(ap@(c_2Ecombin_2ERIGHT__ID@A_27a@A_27a)@V1g)@V2e)) => ( ! [V3l:$i] : ((mem@V3l@(ty_2Elist_2Elist@(ty_2Elist_2Elist@A_27b))) => ((ap@(ap@(ap@(c_2Elist_2EFOLDL@A_27b@A_27a)@V0f)@V2e)@(ap@(c_2Elist_2EFLAT@A_27b)@V3l)) = (ap@(ap@(ap@(c_2Elist_2EFOLDL@A_27a@A_27a)@V1g)@V2e)@(ap@(ap@(c_2Elist_2EMAP@(ty_2Elist_2Elist@A_27b)@A_27a)@(ap@(ap@(c_2Elist_2EFOLDL@A_27b@A_27a)@V0f)@V2e))@V3l)))))))))))))))).
thf(conj_thm_2Erich__list_2EFOLDR__MAP__REVERSE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(arr@A_27a@A_27a))) => (( ! [V1a:$i] : ((mem@V1a@A_27a) => ( ! [V2b:$i] : ((mem@V2b@A_27a) => ( ! [V3c:$i] : ((mem@V3c@A_27a) => ((ap@(ap@V0f@V1a)@(ap@(ap@V0f@V2b)@V3c)) = (ap@(ap@V0f@V2b)@(ap@(ap@V0f@V1a)@V3c))))))))) => ( ! [V4e:$i] : ((mem@V4e@A_27a) => ( ! [V5g:$i] : ((mem@V5g@(arr@A_27b@A_27a)) => ( ! [V6l:$i] : ((mem@V6l@(ty_2Elist_2Elist@A_27b)) => ((ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27a@A_27a)@V0f)@V4e)@(ap@(ap@(c_2Elist_2EMAP@A_27b@A_27a)@V5g)@(ap@(c_2Elist_2EREVERSE@A_27b)@V6l))) = (ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27a@A_27a)@V0f)@V4e)@(ap@(ap@(c_2Elist_2EMAP@A_27b@A_27a)@V5g)@V6l))))))))))))))).
thf(conj_thm_2Erich__list_2EFOLDR__FILTER__REVERSE,lemma,( ! [A_27a:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(arr@A_27a@A_27a))) => (( ! [V1a:$i] : ((mem@V1a@A_27a) => ( ! [V2b:$i] : ((mem@V2b@A_27a) => ( ! [V3c:$i] : ((mem@V3c@A_27a) => ((ap@(ap@V0f@V1a)@(ap@(ap@V0f@V2b)@V3c)) = (ap@(ap@V0f@V2b)@(ap@(ap@V0f@V1a)@V3c))))))))) => ( ! [V4e:$i] : ((mem@V4e@A_27a) => ( ! [V5P:$i] : ((mem@V5P@(arr@A_27a@bool)) => ( ! [V6l:$i] : ((mem@V6l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27a@A_27a)@V0f)@V4e)@(ap@(ap@(c_2Elist_2EFILTER@A_27a)@V5P)@(ap@(c_2Elist_2EREVERSE@A_27a)@V6l))) = (ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27a@A_27a)@V0f)@V4e)@(ap@(ap@(c_2Elist_2EFILTER@A_27a)@V5P)@V6l)))))))))))))).
thf(conj_thm_2Erich__list_2ECOMM__ASSOC__FOLDR__REVERSE,lemma,( ! [A_27a:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(arr@A_27a@A_27a))) => ((p@(ap@(c_2Ecombin_2ECOMM@A_27a@A_27a)@V0f)) => ((p@(ap@(c_2Ecombin_2EASSOC@A_27a)@V0f)) => ( ! [V1e:$i] : ((mem@V1e@A_27a) => ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27a@A_27a)@V0f)@V1e)@(ap@(c_2Elist_2EREVERSE@A_27a)@V2l)) = (ap@(ap@(ap@(c_2Elist_2EFOLDR@A_27a@A_27a)@V0f)@V1e)@V2l)))))))))))).
thf(conj_thm_2Erich__list_2ECOMM__ASSOC__FOLDL__REVERSE,lemma,( ! [A_27a:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(arr@A_27a@A_27a))) => ((p@(ap@(c_2Ecombin_2ECOMM@A_27a@A_27a)@V0f)) => ((p@(ap@(c_2Ecombin_2EASSOC@A_27a)@V0f)) => ( ! [V1e:$i] : ((mem@V1e@A_27a) => ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(ap@(c_2Elist_2EFOLDL@A_27a@A_27a)@V0f)@V1e)@(ap@(c_2Elist_2EREVERSE@A_27a)@V2l)) = (ap@(ap@(ap@(c_2Elist_2EFOLDL@A_27a@A_27a)@V0f)@V1e)@V2l)))))))))))).
thf(conj_thm_2Erich__list_2EELL__LAST,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ((~~ (p@(ap@(c_2Elist_2ENULL@A_27a)@V0l))) => ((ap@(ap@(c_2Erich__list_2EELL@A_27a)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@V0l) = (ap@(c_2Elist_2ELAST@A_27a)@V0l))))))).
thf(conj_thm_2Erich__list_2EELL__0__SNOC,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ((ap@(ap@(c_2Erich__list_2EELL@A_27a)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@(ap@(c_2Elist_2ESNOC@A_27a)@V1x)@V0l)) = V1x))))))).
thf(conj_thm_2Erich__list_2EELL__SNOC,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V0n))) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Erich__list_2EELL@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(ap@(c_2Elist_2ESNOC@A_27a)@V1x)@V2l)) = (ap@(ap@(c_2Erich__list_2EELL@A_27a)@(ap@c_2Eprim__rec_2EPRE@(inj__ty_2Enum_2Enum @ V0n)))@V2l)))))))))).
thf(conj_thm_2Erich__list_2EELL__SUC__SNOC,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1x:$i] : ((mem@V1x@A_27a) => ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Erich__list_2EELL@A_27a)@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V0n)))@(ap@(ap@(c_2Elist_2ESNOC@A_27a)@V1x)@V2l)) = (ap@(ap@(c_2Erich__list_2EELL@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V2l))))))))).
thf(conj_thm_2Erich__list_2EELL__CONS,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((ap@(ap@(c_2Erich__list_2EELL@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V2x)@V1l)) = (ap@(ap@(c_2Erich__list_2EELL@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1l)))))))))).
thf(conj_thm_2Erich__list_2EELL__LENGTH__CONS,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ((ap@(ap@(c_2Erich__list_2EELL@A_27a)@(ap@(c_2Elist_2ELENGTH@A_27a)@V0l))@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V1x)@V0l)) = V1x))))))).
thf(conj_thm_2Erich__list_2EELL__LENGTH__SNOC,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ((ap@(ap@(c_2Erich__list_2EELL@A_27a)@(ap@(c_2Elist_2ELENGTH@A_27a)@V0l))@(ap@(ap@(c_2Elist_2ESNOC@A_27a)@V1x)@V0l)) = (ap@(ap@(ap@(c_2Ebool_2ECOND@A_27a)@(ap@(c_2Elist_2ENULL@A_27a)@V0l))@V1x)@(ap@(c_2Elist_2EHD@A_27a)@V0l))))))))).
thf(conj_thm_2Erich__list_2EELL__APPEND2,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l2:$i] : ((mem@V1l2@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l2))) => ( ! [V2l1:$i] : ((mem@V2l1@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Erich__list_2EELL@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V2l1)@V1l2)) = (ap@(ap@(c_2Erich__list_2EELL@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1l2)))))))))).
thf(conj_thm_2Erich__list_2EELL__APPEND1,lemma,( ! [A_27a:del]: ( ! [V0l2:$i] : ((mem@V0l2@(ty_2Elist_2Elist@A_27a)) => ( ! [V1n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(c_2Elist_2ELENGTH@A_27a)@V0l2))@(inj__ty_2Enum_2Enum @ V1n))) => ( ! [V2l1:$i] : ((mem@V2l1@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Erich__list_2EELL@A_27a)@(inj__ty_2Enum_2Enum @ V1n))@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V2l1)@V0l2)) = (ap@(ap@(c_2Erich__list_2EELL@A_27a)@(ap@(ap@c_2Earithmetic_2E_2D@(inj__ty_2Enum_2Enum @ V1n))@(ap@(c_2Elist_2ELENGTH@A_27a)@V0l2)))@V2l1)))))))))).
thf(conj_thm_2Erich__list_2EELL__PRE__LENGTH,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ((~~ (V0l = (c_2Elist_2ENIL@A_27a))) => ((ap@(ap@(c_2Erich__list_2EELL@A_27a)@(ap@c_2Eprim__rec_2EPRE@(ap@(c_2Elist_2ELENGTH@A_27a)@V0l)))@V0l) = (ap@(c_2Elist_2EHD@A_27a)@V0l))))))).
thf(conj_thm_2Erich__list_2EEL__PRE__LENGTH,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ((~~ (V0l = (c_2Elist_2ENIL@A_27a))) => ((ap@(ap@(c_2Elist_2EEL@A_27a)@(ap@c_2Eprim__rec_2EPRE@(ap@(c_2Elist_2ELENGTH@A_27a)@V0l)))@V0l) = (ap@(c_2Elist_2ELAST@A_27a)@V0l))))))).
thf(conj_thm_2Erich__list_2EEL__ELL,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))) => ((ap@(ap@(c_2Elist_2EEL@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1l) = (ap@(ap@(c_2Erich__list_2EELL@A_27a)@(ap@c_2Eprim__rec_2EPRE@(ap@(ap@c_2Earithmetic_2E_2D@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))@(inj__ty_2Enum_2Enum @ V0n))))@V1l)))))))).
thf(conj_thm_2Erich__list_2EEL__LENGTH__APPEND,lemma,( ! [A_27a:del]: ( ! [V0l2:$i] : ((mem@V0l2@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l1:$i] : ((mem@V1l1@(ty_2Elist_2Elist@A_27a)) => ((~~ (p@(ap@(c_2Elist_2ENULL@A_27a)@V0l2))) => ((ap@(ap@(c_2Elist_2EEL@A_27a)@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l1))@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V1l1)@V0l2)) = (ap@(c_2Elist_2EHD@A_27a)@V0l2))))))))).
thf(conj_thm_2Erich__list_2EELL__EL,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))) => ((ap@(ap@(c_2Erich__list_2EELL@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1l) = (ap@(ap@(c_2Elist_2EEL@A_27a)@(ap@c_2Eprim__rec_2EPRE@(ap@(ap@c_2Earithmetic_2E_2D@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))@(inj__ty_2Enum_2Enum @ V0n))))@V1l)))))))).
thf(conj_thm_2Erich__list_2EELL__MAP,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ( ! [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27b)) => ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))) => ((ap@(ap@(c_2Erich__list_2EELL@A_27b)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(ap@(c_2Elist_2EMAP@A_27a@A_27b)@V2f)@V1l)) = (ap@V2f@(ap@(ap@(c_2Erich__list_2EELL@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1l)))))))))))).
thf(conj_thm_2Erich__list_2ELENGTH__FRONT,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ((~~ (V0l = (c_2Elist_2ENIL@A_27a))) => ((surj__ty_2Enum_2Enum @ (ap@(c_2Elist_2ELENGTH@A_27a)@(ap@(c_2Elist_2EFRONT@A_27a)@V0l))) = (surj__ty_2Enum_2Enum @ (ap@c_2Eprim__rec_2EPRE@(ap@(c_2Elist_2ELENGTH@A_27a)@V0l))))))))).
thf(conj_thm_2Erich__list_2EDROP__LENGTH__APPEND,lemma,( ! [A_27a:del]: ( ! [V0l1:$i] : ((mem@V0l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l2:$i] : ((mem@V1l2@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Elist_2EDROP@A_27a)@(ap@(c_2Elist_2ELENGTH@A_27a)@V0l1))@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V0l1)@V1l2)) = V1l2))))))).
thf(conj_thm_2Erich__list_2ETAKE__APPEND,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l1:$i] : ((mem@V1l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V2l2:$i] : ((mem@V2l2@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Elist_2ETAKE@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V1l1)@V2l2)) = (ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Elist_2ETAKE@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1l1))@(ap@(ap@(c_2Elist_2ETAKE@A_27a)@(ap@(ap@c_2Earithmetic_2E_2D@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l1)))@V2l2)))))))))).
thf(conj_thm_2Erich__list_2ETAKE__APPEND1,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l1:$i] : ((mem@V1l1@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l1))) => ( ! [V2l2:$i] : ((mem@V2l2@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Elist_2ETAKE@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V1l1)@V2l2)) = (ap@(ap@(c_2Elist_2ETAKE@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1l1)))))))))).
thf(conj_thm_2Erich__list_2ETAKE__APPEND2,lemma,( ! [A_27a:del]: ( ! [V0l1:$i] : ((mem@V0l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(c_2Elist_2ELENGTH@A_27a)@V0l1))@(inj__ty_2Enum_2Enum @ V1n))) => ( ! [V2l2:$i] : ((mem@V2l2@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Elist_2ETAKE@A_27a)@(inj__ty_2Enum_2Enum @ V1n))@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V0l1)@V2l2)) = (ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V0l1)@(ap@(ap@(c_2Elist_2ETAKE@A_27a)@(ap@(ap@c_2Earithmetic_2E_2D@(inj__ty_2Enum_2Enum @ V1n))@(ap@(c_2Elist_2ELENGTH@A_27a)@V0l1)))@V2l2))))))))))).
thf(conj_thm_2Erich__list_2ETAKE__LENGTH__APPEND,lemma,( ! [A_27a:del]: ( ! [V0l1:$i] : ((mem@V0l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l2:$i] : ((mem@V1l2@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Elist_2ETAKE@A_27a)@(ap@(c_2Elist_2ELENGTH@A_27a)@V0l1))@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V0l1)@V1l2)) = V0l1))))))).
thf(conj_thm_2Erich__list_2EREVERSE__FLAT,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@(ty_2Elist_2Elist@A_27a))) => ((ap@(c_2Elist_2EREVERSE@A_27a)@(ap@(c_2Elist_2EFLAT@A_27a)@V0l)) = (ap@(c_2Elist_2EFLAT@A_27a)@(ap@(c_2Elist_2EREVERSE@(ty_2Elist_2Elist@A_27a))@(ap@(ap@(c_2Elist_2EMAP@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))@(c_2Elist_2EREVERSE@A_27a))@V0l)))))))).
thf(conj_thm_2Erich__list_2EMAP__FILTER,lemma,( ! [A_27a:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27a)) => ( ! [V1P:$i] : ((mem@V1P@(arr@A_27a@bool)) => ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27a)) => (( ! [V3x:$i] : ((mem@V3x@A_27a) => ((p@(ap@V1P@(ap@V0f@V3x))) <=> (p@(ap@V1P@V3x))))) => ((ap@(ap@(c_2Elist_2EMAP@A_27a@A_27a)@V0f)@(ap@(ap@(c_2Elist_2EFILTER@A_27a)@V1P)@V2l)) = (ap@(ap@(c_2Elist_2EFILTER@A_27a)@V1P)@(ap@(ap@(c_2Elist_2EMAP@A_27a@A_27a)@V0f)@V2l)))))))))))).
thf(conj_thm_2Erich__list_2EFLAT__REVERSE,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@(ty_2Elist_2Elist@A_27a))) => ((ap@(c_2Elist_2EFLAT@A_27a)@(ap@(c_2Elist_2EREVERSE@(ty_2Elist_2Elist@A_27a))@V0l)) = (ap@(c_2Elist_2EREVERSE@A_27a)@(ap@(c_2Elist_2EFLAT@A_27a)@(ap@(ap@(c_2Elist_2EMAP@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))@(c_2Elist_2EREVERSE@A_27a))@V0l)))))))).
thf(conj_thm_2Erich__list_2EFLAT__FLAT,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@(ty_2Elist_2Elist@(ty_2Elist_2Elist@A_27a)))) => ((ap@(c_2Elist_2EFLAT@A_27a)@(ap@(c_2Elist_2EFLAT@(ty_2Elist_2Elist@A_27a))@V0l)) = (ap@(c_2Elist_2EFLAT@A_27a)@(ap@(ap@(c_2Elist_2EMAP@(ty_2Elist_2Elist@(ty_2Elist_2Elist@A_27a))@(ty_2Elist_2Elist@A_27a))@(c_2Elist_2EFLAT@A_27a))@V0l))))))).
thf(conj_thm_2Erich__list_2EEVERY__REVERSE,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Elist_2EEVERY@A_27a)@V0P)@(ap@(c_2Elist_2EREVERSE@A_27a)@V1l))) <=> (p@(ap@(ap@(c_2Elist_2EEVERY@A_27a)@V0P)@V1l))))))))).
thf(conj_thm_2Erich__list_2EEXISTS__REVERSE,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Elist_2EEXISTS@A_27a)@V0P)@(ap@(c_2Elist_2EREVERSE@A_27a)@V1l))) <=> (p@(ap@(ap@(c_2Elist_2EEXISTS@A_27a)@V0P)@V1l))))))))).
thf(conj_thm_2Erich__list_2EEVERY__SEG,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Elist_2EEVERY@A_27a)@V0P)@V1l)) => ( ! [V2m:tp__ty_2Enum_2Enum] : ( ! [V3k:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V2m))@(inj__ty_2Enum_2Enum @ V3k)))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))) => (p@(ap@(ap@(c_2Elist_2EEVERY@A_27a)@V0P)@(ap@(ap@(ap@(c_2Erich__list_2ESEG@A_27a)@(inj__ty_2Enum_2Enum @ V2m))@(inj__ty_2Enum_2Enum @ V3k))@V1l))))))))))))).
thf(conj_thm_2Erich__list_2EEVERY__TAKE,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Elist_2EEVERY@A_27a)@V0P)@V1l)) => ( ! [V2m:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V2m))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))) => (p@(ap@(ap@(c_2Elist_2EEVERY@A_27a)@V0P)@(ap@(ap@(c_2Elist_2ETAKE@A_27a)@(inj__ty_2Enum_2Enum @ V2m))@V1l)))))))))))).
thf(conj_thm_2Erich__list_2EEVERY__DROP,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Elist_2EEVERY@A_27a)@V0P)@V1l)) => ( ! [V2m:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V2m))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))) => (p@(ap@(ap@(c_2Elist_2EEVERY@A_27a)@V0P)@(ap@(ap@(c_2Elist_2EDROP@A_27a)@(inj__ty_2Enum_2Enum @ V2m))@V1l)))))))))))).
thf(conj_thm_2Erich__list_2EEXISTS__SEG,lemma,( ! [A_27a:del]: ( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V1k)))@(ap@(c_2Elist_2ELENGTH@A_27a)@V2l))) => ( ! [V3P:$i] : ((mem@V3P@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Elist_2EEXISTS@A_27a)@V3P)@(ap@(ap@(ap@(c_2Erich__list_2ESEG@A_27a)@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V1k))@V2l))) => (p@(ap@(ap@(c_2Elist_2EEXISTS@A_27a)@V3P)@V2l)))))))))))).
thf(conj_thm_2Erich__list_2EEXISTS__TAKE__IMP,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2P:$i] : ((mem@V2P@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Elist_2EEXISTS@A_27a)@V2P)@(ap@(ap@(c_2Elist_2ETAKE@A_27a)@(inj__ty_2Enum_2Enum @ V1m))@V0l))) => (p@(ap@(ap@(c_2Elist_2EEXISTS@A_27a)@V2P)@V0l)))))))))).
thf(conj_thm_2Erich__list_2EEXISTS__DROP__IMP,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2P:$i] : ((mem@V2P@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Elist_2EEXISTS@A_27a)@V2P)@(ap@(ap@(c_2Elist_2EDROP@A_27a)@(inj__ty_2Enum_2Enum @ V1m))@V0l))) => (p@(ap@(ap@(c_2Elist_2EEXISTS@A_27a)@V2P)@V0l)))))))))).
thf(conj_thm_2Erich__list_2EEXISTS__TAKE,lemma,( ! [A_27a:del]: ( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0m))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))) => ( ! [V2P:$i] : ((mem@V2P@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Elist_2EEXISTS@A_27a)@V2P)@(ap@(ap@(c_2Elist_2ETAKE@A_27a)@(inj__ty_2Enum_2Enum @ V0m))@V1l))) => (p@(ap@(ap@(c_2Elist_2EEXISTS@A_27a)@V2P)@V1l))))))))))).
thf(conj_thm_2Erich__list_2EEXISTS__DROP,lemma,( ! [A_27a:del]: ( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0m))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))) => ( ! [V2P:$i] : ((mem@V2P@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Elist_2EEXISTS@A_27a)@V2P)@(ap@(ap@(c_2Elist_2EDROP@A_27a)@(inj__ty_2Enum_2Enum @ V0m))@V1l))) => (p@(ap@(ap@(c_2Elist_2EEXISTS@A_27a)@V2P)@V1l))))))))))).
thf(conj_thm_2Erich__list_2EEXISTS__LASTN,lemma,( ! [A_27a:del]: ( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0m))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))) => ( ! [V2P:$i] : ((mem@V2P@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Elist_2EEXISTS@A_27a)@V2P)@(ap@(ap@(c_2Erich__list_2ELASTN@A_27a)@(inj__ty_2Enum_2Enum @ V0m))@V1l))) => (p@(ap@(ap@(c_2Elist_2EEXISTS@A_27a)@V2P)@V1l))))))))))).
thf(conj_thm_2Erich__list_2EEXISTS__BUTLASTN,lemma,( ! [A_27a:del]: ( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0m))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))) => ( ! [V2P:$i] : ((mem@V2P@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Elist_2EEXISTS@A_27a)@V2P)@(ap@(ap@(c_2Erich__list_2EBUTLASTN@A_27a)@(inj__ty_2Enum_2Enum @ V0m))@V1l))) => (p@(ap@(ap@(c_2Elist_2EEXISTS@A_27a)@V2P)@V1l))))))))))).
thf(conj_thm_2Erich__list_2EMEM__SEG,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m)))@(ap@(c_2Elist_2ELENGTH@A_27a)@V2l))) => ( ! [V3x:$i] : ((mem@V3x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@(ap@(ap@(ap@(c_2Erich__list_2ESEG@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m))@V2l)))) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@V2l))))))))))))).
thf(conj_thm_2Erich__list_2EMEM__TAKE__IMP,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@(ap@(ap@(c_2Elist_2ETAKE@A_27a)@(inj__ty_2Enum_2Enum @ V1m))@V0l)))) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@V0l))))))))))).
thf(conj_thm_2Erich__list_2EMEM__DROP__IMP,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@(ap@(ap@(c_2Elist_2EDROP@A_27a)@(inj__ty_2Enum_2Enum @ V1m))@V0l)))) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@V0l))))))))))).
thf(conj_thm_2Erich__list_2EMEM__TAKE,lemma,( ! [A_27a:del]: ( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0m))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@(ap@(ap@(c_2Elist_2ETAKE@A_27a)@(inj__ty_2Enum_2Enum @ V0m))@V1l)))) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@V1l)))))))))))).
thf(conj_thm_2Erich__list_2EMEM__DROP,lemma,( ! [A_27a:del]: ( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0m))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@(ap@(ap@(c_2Elist_2EDROP@A_27a)@(inj__ty_2Enum_2Enum @ V0m))@V1l)))) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@V1l)))))))))))).
thf(conj_thm_2Erich__list_2EMEM__BUTLASTN,lemma,( ! [A_27a:del]: ( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0m))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@(ap@(ap@(c_2Erich__list_2EBUTLASTN@A_27a)@(inj__ty_2Enum_2Enum @ V0m))@V1l)))) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@V1l)))))))))))).
thf(conj_thm_2Erich__list_2EMEM__LASTN,lemma,( ! [A_27a:del]: ( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0m))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@(ap@(ap@(c_2Erich__list_2ELASTN@A_27a)@(inj__ty_2Enum_2Enum @ V0m))@V1l)))) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@V1l)))))))))))).
thf(conj_thm_2Erich__list_2EZIP__SNOC,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0l1:$i] : ((mem@V0l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l2:$i] : ((mem@V1l2@(ty_2Elist_2Elist@A_27b)) => (((surj__ty_2Enum_2Enum @ (ap@(c_2Elist_2ELENGTH@A_27a)@V0l1)) = (surj__ty_2Enum_2Enum @ (ap@(c_2Elist_2ELENGTH@A_27b)@V1l2))) => ( ! [V2x1:$i] : ((mem@V2x1@A_27a) => ( ! [V3x2:$i] : ((mem@V3x2@A_27b) => ((ap@(c_2Elist_2EZIP@A_27a@A_27b)@(ap@(ap@(c_2Epair_2E_2C@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27b))@(ap@(ap@(c_2Elist_2ESNOC@A_27a)@V2x1)@V0l1))@(ap@(ap@(c_2Elist_2ESNOC@A_27b)@V3x2)@V1l2))) = (ap@(ap@(c_2Elist_2ESNOC@(ty_2Epair_2Eprod@A_27a@A_27b))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V2x1)@V3x2))@(ap@(c_2Elist_2EZIP@A_27a@A_27b)@(ap@(ap@(c_2Epair_2E_2C@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27b))@V0l1)@V1l2)))))))))))))))).
thf(conj_thm_2Erich__list_2EUNZIP__SNOC,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : ((mem@V0x@(ty_2Epair_2Eprod@A_27a@A_27b)) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@A_27a@A_27b))) => ((ap@(c_2Elist_2EUNZIP@A_27a@A_27b)@(ap@(ap@(c_2Elist_2ESNOC@(ty_2Epair_2Eprod@A_27a@A_27b))@V0x)@V1l)) = (ap@(ap@(c_2Epair_2E_2C@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27b))@(ap@(ap@(c_2Elist_2ESNOC@A_27a)@(ap@(c_2Epair_2EFST@A_27a@A_27b)@V0x))@(ap@(c_2Epair_2EFST@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27b))@(ap@(c_2Elist_2EUNZIP@A_27a@A_27b)@V1l))))@(ap@(ap@(c_2Elist_2ESNOC@A_27b)@(ap@(c_2Epair_2ESND@A_27a@A_27b)@V0x))@(ap@(c_2Epair_2ESND@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27b))@(ap@(c_2Elist_2EUNZIP@A_27a@A_27b)@V1l)))))))))))).
thf(conj_thm_2Erich__list_2ELENGTH__UNZIP__FST,conjecture,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@A_27a@A_27b))) => ((surj__ty_2Enum_2Enum @ (ap@(c_2Elist_2ELENGTH@A_27a)@(ap@(c_2Erich__list_2EUNZIP__FST@A_27a@A_27b)@V0l))) = (surj__ty_2Enum_2Enum @ (ap@(c_2Elist_2ELENGTH@(ty_2Epair_2Eprod@A_27a@A_27b))@V0l)))))))).
