include('Axioms/quantHeuristics_2.ax').
tff(stp_c_ty_2Elist_2Elist_o,type,(tp__c_ty_2Elist_2Elist_o : $tType)).
tff(stp_inj_c_ty_2Elist_2Elist_o,type,(inj__c_ty_2Elist_2Elist_o : tp__c_ty_2Elist_2Elist_o > $i)).
tff(stp_surj_c_ty_2Elist_2Elist_o,type,(surj__c_ty_2Elist_2Elist_o : $i > tp__c_ty_2Elist_2Elist_o)).
tff(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))).
tff(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))))).
tff(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)))))).
tff(tp_c_2Erich__list_2EAND__EL,type,(c_2Erich__list_2EAND__EL:$i)).
tff(mem_c_2Erich__list_2EAND__EL,axiom,mem(c_2Erich__list_2EAND__EL,arr(ty_2Elist_2Elist(bool),bool))).
tff(stp_fo_c_2Erich__list_2EAND__EL,type,(fo__c_2Erich__list_2EAND__EL:(tp__c_ty_2Elist_2Elist_o) > tp__o)).
tff(stp_eq_fo_c_2Erich__list_2EAND__EL,axiom,( ! [X0:tp__c_ty_2Elist_2Elist_o] : (inj__o(fo__c_2Erich__list_2EAND__EL(X0)) = ap(c_2Erich__list_2EAND__EL,inj__c_ty_2Elist_2Elist_o(X0))))).
tff(tp_c_2Erich__list_2EBUTLASTN,type,(c_2Erich__list_2EBUTLASTN:del > $i)).
tff(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)))))).
tff(tp_c_2Erich__list_2ECOUNT__LIST,type,(c_2Erich__list_2ECOUNT__LIST:$i)).
tff(mem_c_2Erich__list_2ECOUNT__LIST,axiom,mem(c_2Erich__list_2ECOUNT__LIST,arr(ty_2Enum_2Enum,ty_2Elist_2Elist(ty_2Enum_2Enum)))).
tff(tp_c_2Erich__list_2ECOUNT__LIST__AUX,type,(c_2Erich__list_2ECOUNT__LIST__AUX:$i)).
tff(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))))).
tff(tp_c_2Erich__list_2EELL,type,(c_2Erich__list_2EELL:del > $i)).
tff(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))))).
tff(tp_c_2Erich__list_2EIS__SUBLIST,type,(c_2Erich__list_2EIS__SUBLIST:del > $i)).
tff(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))))).
tff(tp_c_2Erich__list_2EIS__SUFFIX,type,(c_2Erich__list_2EIS__SUFFIX:del > $i)).
tff(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))))).
tff(tp_c_2Erich__list_2ELASTN,type,(c_2Erich__list_2ELASTN:del > $i)).
tff(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)))))).
tff(tp_c_2Erich__list_2ELIST__ELEM__COUNT,type,(c_2Erich__list_2ELIST__ELEM__COUNT:del > $i)).
tff(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))))).
tff(tp_c_2Erich__list_2EOR__EL,type,(c_2Erich__list_2EOR__EL:$i)).
tff(mem_c_2Erich__list_2EOR__EL,axiom,mem(c_2Erich__list_2EOR__EL,arr(ty_2Elist_2Elist(bool),bool))).
tff(stp_fo_c_2Erich__list_2EOR__EL,type,(fo__c_2Erich__list_2EOR__EL:(tp__c_ty_2Elist_2Elist_o) > tp__o)).
tff(stp_eq_fo_c_2Erich__list_2EOR__EL,axiom,( ! [X0:tp__c_ty_2Elist_2Elist_o] : (inj__o(fo__c_2Erich__list_2EOR__EL(X0)) = ap(c_2Erich__list_2EOR__EL,inj__c_ty_2Elist_2Elist_o(X0))))).
tff(tp_c_2Erich__list_2EPREFIX,type,(c_2Erich__list_2EPREFIX:del > $i)).
tff(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)))))).
tff(tp_c_2Erich__list_2EREPLICATE,type,(c_2Erich__list_2EREPLICATE:del > $i)).
tff(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)))))).
tff(tp_c_2Erich__list_2ESCANL,type,(c_2Erich__list_2ESCANL:(del * del) > $i)).
tff(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)))))))).
tff(tp_c_2Erich__list_2ESCANR,type,(c_2Erich__list_2ESCANR:(del * del) > $i)).
tff(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)))))))).
tff(tp_c_2Erich__list_2ESEG,type,(c_2Erich__list_2ESEG:del > $i)).
tff(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))))))).
tff(tp_c_2Erich__list_2ESPLITL,type,(c_2Erich__list_2ESPLITL:del > $i)).
tff(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))))))).
tff(tp_c_2Erich__list_2ESPLITP,type,(c_2Erich__list_2ESPLITP:del > $i)).
tff(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))))))).
tff(tp_c_2Erich__list_2ESPLITP__AUX,type,(c_2Erich__list_2ESPLITP__AUX:del > $i)).
tff(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)))))))).
tff(tp_c_2Erich__list_2ESPLITR,type,(c_2Erich__list_2ESPLITR:del > $i)).
tff(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))))))).
tff(tp_c_2Erich__list_2ESUFFIX,type,(c_2Erich__list_2ESUFFIX:del > $i)).
tff(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)))))).
tff(tp_c_2Erich__list_2ETL__T,type,(c_2Erich__list_2ETL__T:del > $i)).
tff(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))))).
tff(tp_c_2Erich__list_2EUNZIP__FST,type,(c_2Erich__list_2EUNZIP__FST:(del * del) > $i)).
tff(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)))))).
tff(tp_c_2Erich__list_2EUNZIP__SND,type,(c_2Erich__list_2EUNZIP__SND:(del * del) > $i)).
tff(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)))))).
tff(tp_c_2Erich__list_2Ecommon__prefixes,type,(c_2Erich__list_2Ecommon__prefixes:del > $i)).
tff(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))))).
tff(tp_c_2Erich__list_2Elongest__prefix,type,(c_2Erich__list_2Elongest__prefix:del > $i)).
tff(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))))).
tff(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))))))))).
tff(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))))))))))).
tff(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))))))))).
tff(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))))))))))).
tff(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))))))))))))))).
tff(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))))))))))))))).
tff(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)))))))))))))).
tff(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)))))))))))))).
tff(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))))))).
tff(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))),f760(A_27a))),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)))))))))).
tff(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))))))))).
tff(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)),f762(A_27a,V0P)),c_2Elist_2ENIL(A_27a)),V1l)))))))).
tff(ax_thm_2Erich__list_2EAND__EL__DEF,axiom,(c_2Erich__list_2EAND__EL = ap(c_2Elist_2EEVERY(bool),c_2Ecombin_2EI(bool)))).
tff(ax_thm_2Erich__list_2EOR__EL__DEF,axiom,(c_2Erich__list_2EOR__EL = ap(c_2Elist_2EEXISTS(bool),c_2Ecombin_2EI(bool)))).
tff(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)))))))).
tff(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)))))))).
tff(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),f763(A_27a,V0e)),V1l)))))))))).
tff(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))))))))).
tff(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))))))))).
tff(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))))))))))).
tff(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)))))))).
tff(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)))))))))))).
tff(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))))))))))).
tff(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)))))))).
tff(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))))))))))).
tff(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))))))))).
tff(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))))))))))))).
tff(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))))))))).
tff(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)))))))))))).
tff(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))))))))))))))))).
tff(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)))))))))))).
tff(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)))))))))))))))).
tff(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))))))))).
tff(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)))))))))).
tff(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)))))))))).
tff(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))))))))))))))).
tff(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))))))))))).
tff(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)))))))))))))).
tff(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)))))))))))).
tff(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),k(A_27a,f764)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),V0l)))))))).
tff(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),f765),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),V0l)))))))).
tff(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)),f767(A_27a,A_27b,V0f)),c_2Elist_2ENIL(A_27b)),V1l)))))))))).
tff(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)),f769(A_27a,A_27b,V0f)),c_2Elist_2ENIL(A_27b)),V1l)))))))))).
tff(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)),f771(A_27a,V0P)),c_2Elist_2ENIL(A_27a)),V1l))))))))).
tff(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)))))))))))).
tff(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)),f773(A_27a,V0P)),c_2Elist_2ENIL(A_27a)),V1l))))))))).
tff(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)))))))))))).
tff(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))))))))).
tff(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))))))))))))).
tff(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)))))))))).
tff(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)))))))))))))))).
tff(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))))))))).
tff(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)))))))).
tff(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))))))))).
tff(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)),f775(A_27a)),V0l1),V1l2))))))))).
tff(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)))))))))))))).
tff(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)))))))))))))).
tff(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))))))))).
tff(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)))))).
tff(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)))))).
tff(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))))))))).
tff(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))))))).
tff(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))))))).
tff(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))))))))).
tff(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))))))).
tff(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)),f777(A_27a)),c_2Elist_2ENIL(A_27a)),V0l))))))).
tff(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))))))))))))).
tff(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)))))))))).
tff(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))))))).
tff(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))))))).
tff(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))))))))))))))))).
tff(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)))))))))))).
tff(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)))))))))))).
tff(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))))))))))))))).
tff(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)))))))))).
tff(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)))))))))).
tff(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)))))))))).
tff(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)))))))))).
tff(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)))))))))))).
tff(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))))))).
tff(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)))))))))).
tff(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)),f779(A_27a,V0P)),c_2Elist_2ENIL(A_27a)),V1l))))))))).
tff(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)))))))))))))).
tff(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))))))))).
tff(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)))))))))))))).
tff(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)))))))))))))).
tff(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)))))))))))))))).
tff(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)))))))))))))))).
tff(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))))))))))))))))))).
tff(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))))))))))))))))))).
tff(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)))))))))))).
tff(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)))))))))))).
tff(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)))))).
tff(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)),f781(A_27a)),c_2Elist_2ENIL(A_27a)),V0l) = V0l)))))).
tff(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),f783(A_27a,A_27b,V0f)),V1e),ap(c_2Elist_2EREVERSE(A_27a),V2l))))))))))))).
tff(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),f783(A_27a,A_27b,V0f)),V1e),ap(c_2Elist_2EREVERSE(A_27b),V2l))))))))))))).
tff(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),f783(A_27a,A_27b,V0f)),V1e),V2l)))))))))))).
tff(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),f783(A_27a,A_27b,V0f)),V1e),V2l)))))))))))).
tff(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),f785(A_27c,A_27a,A_27b,V0f,V2g)),V1e),V3l))))))))))))))).
tff(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),f787(A_27a,A_27b,A_27c,V0f,V2g)),V1e),V3l))))))))))))))).
tff(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),f789(A_27a,V0P)),inj__o(fo__c_2Ebool_2ET)),V1l)))))))))).
tff(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),f791(A_27a,V0P)),inj__o(fo__c_2Ebool_2ET)),V1l)))))))))).
tff(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),f793(A_27a,V0P)),inj__o(fo__c_2Ebool_2EF)),V1l)))))))))).
tff(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),f795(A_27a,V0P)),inj__o(fo__c_2Ebool_2EF)),V1l)))))))))).
tff(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),inj__o(fo__c_2Ebool_2ET)),ap(ap(c_2Elist_2EMAP(A_27a,bool),V0P),V1l))))))))))).
tff(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),inj__o(fo__c_2Ebool_2ET)),ap(ap(c_2Elist_2EMAP(A_27a,bool),V0P),V1l))))))))))).
tff(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),inj__o(fo__c_2Ebool_2EF)),ap(ap(c_2Elist_2EMAP(A_27a,bool),V0P),V1l))))))))))).
tff(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),inj__o(fo__c_2Ebool_2EF)),ap(ap(c_2Elist_2EMAP(A_27a,bool),V0P),V1l))))))))))).
tff(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),f797(A_27a,A_27b,V2P,V0f)),V1e),V3l)))))))))))))).
tff(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),f799(A_27b,A_27a,V2P,V0f)),V1e),V3l)))))))))))))).
tff(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)))))))))))))).
tff(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)))))))))))))).
tff(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))))))))))).
tff(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)))))))))).
tff(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),f800(A_27a,V0P,V1Q)),V2l)) <=> (p(ap(ap(c_2Elist_2EEXISTS(A_27a),V0P),V2l)) | p(ap(ap(c_2Elist_2EEXISTS(A_27a),V1Q),V2l))))))))))))).
tff(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),f802(A_27a,V0y)),inj__o(fo__c_2Ebool_2EF)),V1l)))))))))).
tff(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),f804(A_27a,V0y)),inj__o(fo__c_2Ebool_2EF)),V1l)))))))))).
tff(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),k(A_27a,k(bool,c_2Ebool_2EF))),inj__o(fo__c_2Ebool_2ET)),V0l)))))))).
tff(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),k(bool,k(A_27a,c_2Ebool_2EF))),inj__o(fo__c_2Ebool_2ET)),V0l)))))))).
tff(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))))))))))).
tff(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)))))).
tff(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))))))))))).
tff(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))))))))))).
tff(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))))))))).
tff(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))))))))))).
tff(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)))))))).
tff(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)))))).
tff(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))))))))))).
tff(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))))))))))).
tff(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)))))))))).
tff(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)))))))))).
tff(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))))))))))).
tff(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)))))))))).
tff(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)))))))).
tff(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))))))))).
tff(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)))))))))))).
tff(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)))))))).
tff(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)))))))).
tff(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)))))))))))).
tff(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)))))))))).
tff(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)))))))))).
tff(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))))))))).
tff(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))))))))))).
tff(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))))))))))).
tff(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))))))))).
tff(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)))))))).
tff(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))))))))))).
tff(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))))))))))).
tff(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))))))))))).
tff(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))))))))))))).
tff(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))))))))))))).
tff(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))))))))))))).
tff(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))))))))))))).
tff(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)))))))))).
tff(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))))))))))).
tff(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))))))).
tff(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))))))).
tff(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))))))))))).
tff(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))))))))))).
tff(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))))))))))).
tff(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))))))))).
tff(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)))))))))).
tff(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))))))))).
tff(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))))))))).
tff(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))))))))).
tff(conj_thm_2Erich__list_2EDROP__SNOC,conjecture,(( ! [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)))))))))))).
