include('Axioms/quantHeuristics+2.ax').
fof(mem_c_2Erich__list_2EAND__EL,axiom,( mem(c_2Erich__list_2EAND__EL,arr(ty_2Elist_2Elist(bool),bool)) )).
fof(mem_c_2Erich__list_2EBUTLASTN,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Erich__list_2EBUTLASTN(A_27a),arr(ty_2Enum_2Enum,arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a)))) ) )).
fof(mem_c_2Erich__list_2ECOUNT__LIST,axiom,( mem(c_2Erich__list_2ECOUNT__LIST,arr(ty_2Enum_2Enum,ty_2Elist_2Elist(ty_2Enum_2Enum))) )).
fof(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)))) )).
fof(mem_c_2Erich__list_2EELL,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Erich__list_2EELL(A_27a),arr(ty_2Enum_2Enum,arr(ty_2Elist_2Elist(A_27a),A_27a))) ) )).
fof(mem_c_2Erich__list_2EIS__SUBLIST,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Erich__list_2EIS__SUBLIST(A_27a),arr(ty_2Elist_2Elist(A_27a),arr(ty_2Elist_2Elist(A_27a),bool))) ) )).
fof(mem_c_2Erich__list_2EIS__SUFFIX,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Erich__list_2EIS__SUFFIX(A_27a),arr(ty_2Elist_2Elist(A_27a),arr(ty_2Elist_2Elist(A_27a),bool))) ) )).
fof(mem_c_2Erich__list_2ELASTN,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Erich__list_2ELASTN(A_27a),arr(ty_2Enum_2Enum,arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a)))) ) )).
fof(mem_c_2Erich__list_2ELIST__ELEM__COUNT,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Erich__list_2ELIST__ELEM__COUNT(A_27a),arr(A_27a,arr(ty_2Elist_2Elist(A_27a),ty_2Enum_2Enum))) ) )).
fof(mem_c_2Erich__list_2EOR__EL,axiom,( mem(c_2Erich__list_2EOR__EL,arr(ty_2Elist_2Elist(bool),bool)) )).
fof(mem_c_2Erich__list_2EPREFIX,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Erich__list_2EPREFIX(A_27a),arr(arr(A_27a,bool),arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a)))) ) )).
fof(mem_c_2Erich__list_2EREPLICATE,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Erich__list_2EREPLICATE(A_27a),arr(ty_2Enum_2Enum,arr(A_27a,ty_2Elist_2Elist(A_27a)))) ) )).
fof(mem_c_2Erich__list_2ESCANL,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => 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))))) ) ) )).
fof(mem_c_2Erich__list_2ESCANR,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => 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))))) ) ) )).
fof(mem_c_2Erich__list_2ESEG,axiom,( ! [A_27a] : ( ne(A_27a) => 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))))) ) )).
fof(mem_c_2Erich__list_2ESPLITL,axiom,( ! [A_27a] : ( ne(A_27a) => 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))))) ) )).
fof(mem_c_2Erich__list_2ESPLITP,axiom,( ! [A_27a] : ( ne(A_27a) => 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))))) ) )).
fof(mem_c_2Erich__list_2ESPLITP__AUX,axiom,( ! [A_27a] : ( ne(A_27a) => 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)))))) ) )).
fof(mem_c_2Erich__list_2ESPLITR,axiom,( ! [A_27a] : ( ne(A_27a) => 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))))) ) )).
fof(mem_c_2Erich__list_2ESUFFIX,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Erich__list_2ESUFFIX(A_27a),arr(arr(A_27a,bool),arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a)))) ) )).
fof(mem_c_2Erich__list_2ETL__T,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Erich__list_2ETL__T(A_27a),arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a))) ) )).
fof(mem_c_2Erich__list_2EUNZIP__FST,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => 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))) ) ) )).
fof(mem_c_2Erich__list_2EUNZIP__SND,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => 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))) ) ) )).
fof(mem_c_2Erich__list_2Ecommon__prefixes,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Erich__list_2Ecommon__prefixes(A_27a),arr(arr(ty_2Elist_2Elist(A_27a),bool),arr(ty_2Elist_2Elist(A_27a),bool))) ) )).
fof(mem_c_2Erich__list_2Elongest__prefix,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Erich__list_2Elongest__prefix(A_27a),arr(arr(ty_2Elist_2Elist(A_27a),bool),ty_2Elist_2Elist(A_27a))) ) )).
fof(ax_thm_2Erich__list_2EELL,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ap(ap(c_2Erich__list_2EELL(A_27a),c_2Enum_2E0),V0l) = ap(c_2Elist_2ELAST(A_27a),V0l) ) ) ) & ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2l] : ( mem(V2l,ty_2Elist_2Elist(A_27a)) => ( ap(ap(c_2Erich__list_2EELL(A_27a),ap(c_2Enum_2ESUC,V1n)),V2l) = ap(ap(c_2Erich__list_2EELL(A_27a),V1n),ap(c_2Elist_2EFRONT(A_27a),V2l)) ) ) ) ) ) )).
fof(conj_thm_2Erich__list_2EELL__compute,lemma,( ! [A_27a]: ( ne(A_27a) => ( ( ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ap(ap(c_2Erich__list_2EELL(A_27a),c_2Enum_2E0),V0l) = ap(c_2Elist_2ELAST(A_27a),V0l) ) ) ) & ( ( ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2l] : ( mem(V2l,ty_2Elist_2Elist(A_27a)) => ( ap(ap(c_2Erich__list_2EELL(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V1n))),V2l) = ap(ap(c_2Erich__list_2EELL(A_27a),ap(ap(c_2Earithmetic_2E_2D,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V1n))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),ap(c_2Elist_2EFRONT(A_27a),V2l)) ) ) ) ) & ! [V3n] : ( mem(V3n,ty_2Enum_2Enum) => ! [V4l] : ( mem(V4l,ty_2Elist_2Elist(A_27a)) => ( ap(ap(c_2Erich__list_2EELL(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,V3n))),V4l) = ap(ap(c_2Erich__list_2EELL(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V3n))),ap(c_2Elist_2EFRONT(A_27a),V4l)) ) ) ) ) )))).
fof(ax_thm_2Erich__list_2EREPLICATE,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0x] : ( mem(V0x,A_27a) => ( ap(ap(c_2Erich__list_2EREPLICATE(A_27a),c_2Enum_2E0),V0x) = c_2Elist_2ENIL(A_27a) ) ) ) & ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2x] : ( mem(V2x,A_27a) => ( ap(ap(c_2Erich__list_2EREPLICATE(A_27a),ap(c_2Enum_2ESUC,V1n)),V2x) = ap(ap(c_2Elist_2ECONS(A_27a),V2x),ap(ap(c_2Erich__list_2EREPLICATE(A_27a),V1n),V2x)) ) ) ) ) ) )).
fof(conj_thm_2Erich__list_2EREPLICATE__compute,lemma,( ! [A_27a]: ( ne(A_27a) => ( ( ! [V0x] : ( mem(V0x,A_27a) => ( ap(ap(c_2Erich__list_2EREPLICATE(A_27a),c_2Enum_2E0),V0x) = c_2Elist_2ENIL(A_27a) ) ) ) & ( ( ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2x] : ( mem(V2x,A_27a) => ( ap(ap(c_2Erich__list_2EREPLICATE(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,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,V1n))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),V2x)) ) ) ) ) & ! [V3n] : ( mem(V3n,ty_2Enum_2Enum) => ! [V4x] : ( mem(V4x,A_27a) => ( ap(ap(c_2Erich__list_2EREPLICATE(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,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,V3n))),V4x)) ) ) ) ) )))).
fof(ax_thm_2Erich__list_2ESCANL,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ( ( ! [V0f] : ( mem(V0f,arr(A_27b,arr(A_27a,A_27b))) => ! [V1e] : ( 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] : ( mem(V2f,arr(A_27b,arr(A_27a,A_27b))) => ! [V3e] : ( mem(V3e,A_27b) => ! [V4x] : ( mem(V4x,A_27a) => ! [V5l] : ( 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)) ) ) ) ) ) ) ) ) )).
fof(ax_thm_2Erich__list_2ESCANR,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ( ( ! [V0f] : ( mem(V0f,arr(A_27a,arr(A_27b,A_27b))) => ! [V1e] : ( 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] : ( mem(V2f,arr(A_27a,arr(A_27b,A_27b))) => ! [V3e] : ( mem(V3e,A_27b) => ! [V4x] : ( mem(V4x,A_27a) => ! [V5l] : ( 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)) ) ) ) ) ) ) ) ) )).
fof(ax_thm_2Erich__list_2ESPLITP,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0P] : ( 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] : ( mem(V1P,arr(A_27a,bool)) => ! [V2x] : ( mem(V2x,A_27a) => ! [V3l] : ( 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)))) ) ) ) ) ) ) )).
fof(ax_thm_2Erich__list_2ESPLITP__AUX__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0acc] : ( mem(V0acc,ty_2Elist_2Elist(A_27a)) => ! [V1P] : ( 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] : ( mem(V2acc,ty_2Elist_2Elist(A_27a)) => ! [V3P] : ( mem(V3P,arr(A_27a,bool)) => ! [V4h] : ( mem(V4h,A_27a) => ! [V5t] : ( 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)) ) ) ) ) ) ) ) )).
fof(ax_thm_2Erich__list_2ESPLITL__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0P] : ( 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)) ) ) ) )).
fof(ax_thm_2Erich__list_2ESPLITR__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1l] : ( 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))) ) ) ) ) )).
fof(ax_thm_2Erich__list_2EPREFIX__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1l] : ( 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)) ) ) ) ) )).
fof(ax_thm_2Erich__list_2ESUFFIX__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1l] : ( 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) ) ) ) ) )).
fof(ax_thm_2Erich__list_2EAND__EL__DEF,axiom, ( c_2Erich__list_2EAND__EL = ap(c_2Elist_2EEVERY(bool),c_2Ecombin_2EI(bool)) )).
fof(ax_thm_2Erich__list_2EOR__EL__DEF,axiom, ( c_2Erich__list_2EOR__EL = ap(c_2Elist_2EEXISTS(bool),c_2Ecombin_2EI(bool)) )).
fof(ax_thm_2Erich__list_2EUNZIP__FST__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0l] : ( 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)) ) ) ) ) )).
fof(ax_thm_2Erich__list_2EUNZIP__SND__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0l] : ( 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)) ) ) ) ) )).
fof(ax_thm_2Erich__list_2ELIST__ELEM__COUNT__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0e] : ( mem(V0e,A_27a) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ( ap(ap(c_2Erich__list_2ELIST__ELEM__COUNT(A_27a),V0e),V1l) = ap(c_2Elist_2ELENGTH(A_27a),ap(ap(c_2Elist_2EFILTER(A_27a),f763(A_27a,V0e)),V1l)) ) ) ) ) )).
fof(ax_thm_2Erich__list_2ECOUNT__LIST__def,axiom, ( ( ap(c_2Erich__list_2ECOUNT__LIST,c_2Enum_2E0) = c_2Elist_2ENIL(ty_2Enum_2Enum) ) & ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(c_2Erich__list_2ECOUNT__LIST,ap(c_2Enum_2ESUC,V0n)) = ap(ap(c_2Elist_2ECONS(ty_2Enum_2Enum),c_2Enum_2E0),ap(ap(c_2Elist_2EMAP(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Enum_2ESUC),ap(c_2Erich__list_2ECOUNT__LIST,V0n))) ) ) )).
fof(ax_thm_2Erich__list_2ECOUNT__LIST__AUX__def,axiom, ( ( ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(ty_2Enum_2Enum)) => ( ap(ap(c_2Erich__list_2ECOUNT__LIST__AUX,c_2Enum_2E0),V0l) = V0l ) ) ) & ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2l] : ( mem(V2l,ty_2Elist_2Elist(ty_2Enum_2Enum)) => ( ap(ap(c_2Erich__list_2ECOUNT__LIST__AUX,ap(c_2Enum_2ESUC,V1n)),V2l) = ap(ap(c_2Erich__list_2ECOUNT__LIST__AUX,V1n),ap(ap(c_2Elist_2ECONS(ty_2Enum_2Enum),V1n),V2l)) ) ) ) )).
fof(conj_thm_2Erich__list_2ECOUNT__LIST__AUX__def__compute,lemma,(( ( ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(ty_2Enum_2Enum)) => ( ap(ap(c_2Erich__list_2ECOUNT__LIST__AUX,c_2Enum_2E0),V0l) = V0l ) ) ) & ( ( ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2l] : ( mem(V2l,ty_2Elist_2Elist(ty_2Enum_2Enum)) => ( ap(ap(c_2Erich__list_2ECOUNT__LIST__AUX,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V1n))),V2l) = ap(ap(c_2Erich__list_2ECOUNT__LIST__AUX,ap(ap(c_2Earithmetic_2E_2D,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V1n))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,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,V1n))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO)))),V2l)) ) ) ) ) & ! [V3n] : ( mem(V3n,ty_2Enum_2Enum) => ! [V4l] : ( mem(V4l,ty_2Elist_2Elist(ty_2Enum_2Enum)) => ( ap(ap(c_2Erich__list_2ECOUNT__LIST__AUX,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,V3n))),V4l) = ap(ap(c_2Erich__list_2ECOUNT__LIST__AUX,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V3n))),ap(ap(c_2Elist_2ECONS(ty_2Enum_2Enum),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V3n))),V4l)) ) ) ) ) ))).
fof(ax_thm_2Erich__list_2ETL__T__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ap(c_2Erich__list_2ETL__T(A_27a),c_2Elist_2ENIL(A_27a)) = c_2Elist_2ENIL(A_27a) ) & ! [V0h] : ( mem(V0h,A_27a) => ! [V1t] : ( 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 ) ) ) ) ) )).
fof(conj_thm_2Erich__list_2ETAKE,lemma,( ! [A_27a]: ( ne(A_27a) => ( ( ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ap(ap(c_2Elist_2ETAKE(A_27a),c_2Enum_2E0),V0l) = c_2Elist_2ENIL(A_27a) ) ) ) & ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2x] : ( mem(V2x,A_27a) => ! [V3l] : ( mem(V3l,ty_2Elist_2Elist(A_27a)) => ( ap(ap(c_2Elist_2ETAKE(A_27a),ap(c_2Enum_2ESUC,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),V1n),V3l)) ) ) ) ) )))).
fof(conj_thm_2Erich__list_2EDROP,lemma,( ! [A_27a]: ( ne(A_27a) => ( ( ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ap(ap(c_2Elist_2EDROP(A_27a),c_2Enum_2E0),V0l) = V0l ) ) ) & ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2x] : ( mem(V2x,A_27a) => ! [V3l] : ( mem(V3l,ty_2Elist_2Elist(A_27a)) => ( ap(ap(c_2Elist_2EDROP(A_27a),ap(c_2Enum_2ESUC,V1n)),ap(ap(c_2Elist_2ECONS(A_27a),V2x),V3l)) = ap(ap(c_2Elist_2EDROP(A_27a),V1n),V3l) ) ) ) ) )))).
fof(conj_thm_2Erich__list_2EDROP__FUNPOW__TL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ( ap(ap(c_2Elist_2EDROP(A_27a),V0n),V1l) = ap(ap(ap(c_2Earithmetic_2EFUNPOW(ty_2Elist_2Elist(A_27a)),c_2Erich__list_2ETL__T(A_27a)),V0n),V1l) ) ) )))).
fof(conj_thm_2Erich__list_2ENOT__NULL__SNOC,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ( ~~ p(ap(c_2Elist_2ENULL(A_27a),ap(ap(c_2Elist_2ESNOC(A_27a),V0x),V1l))) ) ) )))).
fof(ax_thm_2Erich__list_2ELASTN__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1xs] : ( mem(V1xs,ty_2Elist_2Elist(A_27a)) => ( ap(ap(c_2Erich__list_2ELASTN(A_27a),V0n),V1xs) = ap(c_2Elist_2EREVERSE(A_27a),ap(ap(c_2Elist_2ETAKE(A_27a),V0n),ap(c_2Elist_2EREVERSE(A_27a),V1xs))) ) ) ) ) )).
fof(conj_thm_2Erich__list_2ELASTN,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( ( ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ap(ap(c_2Erich__list_2ELASTN(A_27a),c_2Enum_2E0),V0l) = c_2Elist_2ENIL(A_27a) ) ) ) & ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2x] : ( mem(V2x,A_27b) => ! [V3l] : ( mem(V3l,ty_2Elist_2Elist(A_27b)) => ( ap(ap(c_2Erich__list_2ELASTN(A_27b),ap(c_2Enum_2ESUC,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),V1n),V3l)) ) ) ) ) ))))).
fof(ax_thm_2Erich__list_2EBUTLASTN__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1xs] : ( mem(V1xs,ty_2Elist_2Elist(A_27a)) => ( ap(ap(c_2Erich__list_2EBUTLASTN(A_27a),V0n),V1xs) = ap(c_2Elist_2EREVERSE(A_27a),ap(ap(c_2Elist_2EDROP(A_27a),V0n),ap(c_2Elist_2EREVERSE(A_27a),V1xs))) ) ) ) ) )).
fof(conj_thm_2Erich__list_2EBUTLASTN,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( ( ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ap(ap(c_2Erich__list_2EBUTLASTN(A_27a),c_2Enum_2E0),V0l) = V0l ) ) ) & ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2x] : ( mem(V2x,A_27b) => ! [V3l] : ( mem(V3l,ty_2Elist_2Elist(A_27b)) => ( ap(ap(c_2Erich__list_2EBUTLASTN(A_27b),ap(c_2Enum_2ESUC,V1n)),ap(ap(c_2Elist_2ESNOC(A_27b),V2x),V3l)) = ap(ap(c_2Erich__list_2EBUTLASTN(A_27b),V1n),V3l) ) ) ) ) ))))).
fof(ax_thm_2Erich__list_2EIS__SUBLIST,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0l] : ( 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] : ( mem(V1x,A_27a) => ! [V2l] : ( 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] : ( mem(V3x1,A_27a) => ! [V4l1] : ( mem(V4l1,ty_2Elist_2Elist(A_27a)) => ! [V5x2] : ( mem(V5x2,A_27a) => ! [V6l2] : ( 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))) ) ) ) ) ) ) ) ) ) )).
fof(ax_thm_2Erich__list_2ESEG,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0k] : ( mem(V0k,ty_2Enum_2Enum) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ( ap(ap(ap(c_2Erich__list_2ESEG(A_27a),c_2Enum_2E0),V0k),V1l) = c_2Elist_2ENIL(A_27a) ) ) ) ) & ( ( ! [V2m] : ( mem(V2m,ty_2Enum_2Enum) => ! [V3x] : ( mem(V3x,A_27a) => ! [V4l] : ( mem(V4l,ty_2Elist_2Elist(A_27a)) => ( ap(ap(ap(c_2Erich__list_2ESEG(A_27a),ap(c_2Enum_2ESUC,V2m)),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),V2m),c_2Enum_2E0),V4l)) ) ) ) ) ) & ! [V5m] : ( mem(V5m,ty_2Enum_2Enum) => ! [V6k] : ( mem(V6k,ty_2Enum_2Enum) => ! [V7x] : ( mem(V7x,A_27a) => ! [V8l] : ( mem(V8l,ty_2Elist_2Elist(A_27a)) => ( ap(ap(ap(c_2Erich__list_2ESEG(A_27a),ap(c_2Enum_2ESUC,V5m)),ap(c_2Enum_2ESUC,V6k)),ap(ap(c_2Elist_2ECONS(A_27a),V7x),V8l)) = ap(ap(ap(c_2Erich__list_2ESEG(A_27a),ap(c_2Enum_2ESUC,V5m)),V6k),V8l) ) ) ) ) ) ) ) ) )).
fof(ax_thm_2Erich__list_2EIS__SUFFIX,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0l] : ( 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] : ( mem(V1x,A_27a) => ! [V2l] : ( 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] : ( mem(V3x1,A_27a) => ! [V4l1] : ( mem(V4l1,ty_2Elist_2Elist(A_27a)) => ! [V5x2] : ( mem(V5x2,A_27a) => ! [V6l2] : ( 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)) ) ) ) ) ) ) ) ) ) )).
fof(conj_thm_2Erich__list_2ELENGTH__NOT__NULL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),ap(c_2Elist_2ELENGTH(A_27a),V0l))) <=> ( ~~ p(ap(c_2Elist_2ENULL(A_27a),V0l)) ) ) )))).
fof(conj_thm_2Erich__list_2ENOT__NIL__SNOC,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ( ~~ ( c_2Elist_2ENIL(A_27a) = ap(ap(c_2Elist_2ESNOC(A_27a),V0x),V1l) ) ) ) )))).
fof(conj_thm_2Erich__list_2ENOT__SNOC__NIL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ( ~~ ( ap(ap(c_2Elist_2ESNOC(A_27a),V0x),V1l) = c_2Elist_2ENIL(A_27a) ) ) ) )))).
fof(conj_thm_2Erich__list_2ESNOC__EQ__LENGTH__EQ,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x1] : ( mem(V0x1,A_27a) => ! [V1l1] : ( mem(V1l1,ty_2Elist_2Elist(A_27a)) => ! [V2x2] : ( mem(V2x2,A_27a) => ! [V3l2] : ( 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) ) => ( ap(c_2Elist_2ELENGTH(A_27a),V1l1) = ap(c_2Elist_2ELENGTH(A_27a),V3l2) ) ) ) ) ) )))).
fof(conj_thm_2Erich__list_2ESNOC__REVERSE__CONS,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1l] : ( 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))) ) ) )))).
fof(conj_thm_2Erich__list_2EFOLDR__SNOC,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(A_27a,arr(A_27b,A_27b))) => ! [V1e] : ( mem(V1e,A_27b) => ! [V2x] : ( mem(V2x,A_27a) => ! [V3l] : ( 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) ) ) ) ) ))))).
fof(conj_thm_2Erich__list_2EFOLDR__FOLDL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0f] : ( mem(V0f,arr(A_27a,arr(A_27a,A_27a))) => ! [V1e] : ( mem(V1e,A_27a) => ( p(ap(ap(c_2Ecombin_2EMONOID(A_27a),V0f),V1e)) => ! [V2l] : ( 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) ) ) ) ) )))).
fof(conj_thm_2Erich__list_2ELENGTH__FOLDR,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ap(c_2Elist_2ELENGTH(A_27a),V0l) = ap(ap(ap(c_2Elist_2EFOLDR(A_27a,ty_2Enum_2Enum),k(A_27a,f764)),c_2Enum_2E0),V0l) ) )))).
fof(conj_thm_2Erich__list_2ELENGTH__FOLDL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ap(c_2Elist_2ELENGTH(A_27a),V0l) = ap(ap(ap(c_2Elist_2EFOLDL(A_27a,ty_2Enum_2Enum),f765),c_2Enum_2E0),V0l) ) )))).
fof(conj_thm_2Erich__list_2EMAP__FOLDR,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(A_27a,A_27b)) => ! [V1l] : ( 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) ) ) ))))).
fof(conj_thm_2Erich__list_2EMAP__FOLDL,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(A_27a,A_27b)) => ! [V1l] : ( 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) ) ) ))))).
fof(conj_thm_2Erich__list_2EFILTER__FOLDR,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1l] : ( 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) ) ) )))).
fof(conj_thm_2Erich__list_2EFILTER__SNOC,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1x] : ( mem(V1x,A_27a) => ! [V2l] : ( 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)) ) ) ) )))).
fof(conj_thm_2Erich__list_2EFILTER__FOLDL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1l] : ( 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) ) ) )))).
fof(conj_thm_2Erich__list_2EFILTER__COMM,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0f1] : ( mem(V0f1,arr(A_27a,bool)) => ! [V1f2] : ( mem(V1f2,arr(A_27a,bool)) => ! [V2l] : ( 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)) ) ) ) )))).
fof(conj_thm_2Erich__list_2EFILTER__IDEM,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0f] : ( mem(V0f,arr(A_27a,bool)) => ! [V1l] : ( 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) ) ) )))).
fof(conj_thm_2Erich__list_2EFILTER__MAP,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f1] : ( mem(V0f1,arr(A_27a,bool)) => ! [V1f2] : ( mem(V1f2,arr(A_27b,A_27a)) => ! [V2l] : ( 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)) ) ) ) ))))).
fof(conj_thm_2Erich__list_2ELENGTH__FILTER__LEQ,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1l] : ( 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))) ) )))).
fof(conj_thm_2Erich__list_2EFILTER__EQ,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P1] : ( mem(V0P1,arr(A_27a,bool)) => ! [V1P2] : ( mem(V1P2,arr(A_27a,bool)) => ! [V2l] : ( 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] : ( 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)) ) ) ) ) ) ) )))).
fof(conj_thm_2Erich__list_2ELENGTH__SEG,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1k] : ( mem(V1k,ty_2Enum_2Enum) => ! [V2l] : ( mem(V2l,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2B,V0n),V1k)),ap(c_2Elist_2ELENGTH(A_27a),V2l))) => ( ap(c_2Elist_2ELENGTH(A_27a),ap(ap(ap(c_2Erich__list_2ESEG(A_27a),V0n),V1k),V2l)) = V0n ) ) ) ) )))).
fof(conj_thm_2Erich__list_2EAPPEND__NIL,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( ( ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ap(ap(c_2Elist_2EAPPEND(A_27a),V0l),c_2Elist_2ENIL(A_27a)) = V0l ) ) ) & ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27b)) => ( ap(ap(c_2Elist_2EAPPEND(A_27b),c_2Elist_2ENIL(A_27b)),V1l) = V1l ) ) ))))).
fof(conj_thm_2Erich__list_2EAPPEND__FOLDR,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l1] : ( mem(V0l1,ty_2Elist_2Elist(A_27a)) => ! [V1l2] : ( 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) ) ) )))).
fof(conj_thm_2Erich__list_2EAPPEND__FOLDL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l1] : ( mem(V0l1,ty_2Elist_2Elist(A_27a)) => ! [V1l2] : ( 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) ) ) )))).
fof(conj_thm_2Erich__list_2EFOLDR__APPEND,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(A_27a,arr(A_27b,A_27b))) => ! [V1e] : ( mem(V1e,A_27b) => ! [V2l1] : ( mem(V2l1,ty_2Elist_2Elist(A_27a)) => ! [V3l2] : ( 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) ) ) ) ) ))))).
fof(conj_thm_2Erich__list_2EFOLDL__APPEND,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(A_27a,arr(A_27b,A_27a))) => ! [V1e] : ( mem(V1e,A_27a) => ! [V2l1] : ( mem(V2l1,ty_2Elist_2Elist(A_27b)) => ! [V3l2] : ( 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) ) ) ) ) ))))).
fof(conj_thm_2Erich__list_2ECONS__APPEND,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1l] : ( 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) ) ) )))).
fof(conj_thm_2Erich__list_2EASSOC__APPEND,lemma,( ! [A_27a]: ( ne(A_27a) => p(ap(c_2Ecombin_2EASSOC(ty_2Elist_2Elist(A_27a)),c_2Elist_2EAPPEND(A_27a)))))).
fof(conj_thm_2Erich__list_2EMONOID__APPEND__NIL,lemma,( ! [A_27a]: ( ne(A_27a) => p(ap(ap(c_2Ecombin_2EMONOID(ty_2Elist_2Elist(A_27a)),c_2Elist_2EAPPEND(A_27a)),c_2Elist_2ENIL(A_27a)))))).
fof(conj_thm_2Erich__list_2EFLAT__SNOC,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,ty_2Elist_2Elist(A_27a)) => ! [V1l] : ( 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) ) ) )))).
fof(conj_thm_2Erich__list_2EFLAT__FOLDR,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( 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) ) )))).
fof(conj_thm_2Erich__list_2EFLAT__FOLDL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( 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) ) )))).
fof(conj_thm_2Erich__list_2ELENGTH__FLAT,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(ty_2Elist_2Elist(A_27a))) => ( ap(c_2Elist_2ELENGTH(A_27a),ap(c_2Elist_2EFLAT(A_27a),V0l)) = ap(c_2Elist_2ESUM,ap(ap(c_2Elist_2EMAP(ty_2Elist_2Elist(A_27a),ty_2Enum_2Enum),c_2Elist_2ELENGTH(A_27a)),V0l)) ) )))).
fof(conj_thm_2Erich__list_2EREVERSE__FOLDR,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( 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) ) )))).
fof(conj_thm_2Erich__list_2EREVERSE__FOLDL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( 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) ) )))).
fof(conj_thm_2Erich__list_2EALL__EL__MAP,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1f] : ( mem(V1f,arr(A_27b,A_27a)) => ! [V2l] : ( 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)) ) ) ) ))))).
fof(conj_thm_2Erich__list_2EMEM__EXISTS,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1l] : ( 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)) ) ) )))).
fof(conj_thm_2Erich__list_2ESUM__FOLDR,lemma,(! [V0l] : ( mem(V0l,ty_2Elist_2Elist(ty_2Enum_2Enum)) => ( ap(c_2Elist_2ESUM,V0l) = ap(ap(ap(c_2Elist_2EFOLDR(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Earithmetic_2E_2B),c_2Enum_2E0),V0l) ) ))).
fof(conj_thm_2Erich__list_2ESUM__FOLDL,lemma,(! [V0l] : ( mem(V0l,ty_2Elist_2Elist(ty_2Enum_2Enum)) => ( ap(c_2Elist_2ESUM,V0l) = ap(ap(ap(c_2Elist_2EFOLDL(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Earithmetic_2E_2B),c_2Enum_2E0),V0l) ) ))).
fof(conj_thm_2Erich__list_2EIS__PREFIX,lemma,( ! [A_27a]: ( ne(A_27a) => ( ( ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Elist_2EisPREFIX(A_27a),c_2Elist_2ENIL(A_27a)),V0l)) <=> $true ) ) ) & ( ( ! [V1x] : ( mem(V1x,A_27a) => ! [V2l] : ( 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] : ( mem(V3x1,A_27a) => ! [V4l1] : ( mem(V4l1,ty_2Elist_2Elist(A_27a)) => ! [V5x2] : ( mem(V5x2,A_27a) => ! [V6l2] : ( 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)) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Erich__list_2EIS__PREFIX__APPEND,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l1] : ( mem(V0l1,ty_2Elist_2Elist(A_27a)) => ! [V1l2] : ( mem(V1l2,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Elist_2EisPREFIX(A_27a),V1l2),V0l1)) <=> ? [V2l] : ( mem(V2l,ty_2Elist_2Elist(A_27a)) & ( V0l1 = ap(ap(c_2Elist_2EAPPEND(A_27a),V1l2),V2l) ) ) ) ) )))).
fof(conj_thm_2Erich__list_2EIS__SUFFIX__APPEND,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l1] : ( mem(V0l1,ty_2Elist_2Elist(A_27a)) => ! [V1l2] : ( mem(V1l2,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Erich__list_2EIS__SUFFIX(A_27a),V0l1),V1l2)) <=> ? [V2l] : ( mem(V2l,ty_2Elist_2Elist(A_27a)) & ( V0l1 = ap(ap(c_2Elist_2EAPPEND(A_27a),V2l),V1l2) ) ) ) ) )))).
fof(conj_thm_2Erich__list_2EIS__SUBLIST__APPEND,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l1] : ( mem(V0l1,ty_2Elist_2Elist(A_27a)) => ! [V1l2] : ( mem(V1l2,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Erich__list_2EIS__SUBLIST(A_27a),V0l1),V1l2)) <=> ? [V2l] : ( mem(V2l,ty_2Elist_2Elist(A_27a)) & ? [V3l_27] : ( 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)) ) ) ) ) ) )))).
fof(conj_thm_2Erich__list_2EIS__PREFIX__IS__SUBLIST,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l1] : ( mem(V0l1,ty_2Elist_2Elist(A_27a)) => ! [V1l2] : ( 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)) ) ) )))).
fof(conj_thm_2Erich__list_2EIS__SUFFIX__IS__SUBLIST,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l1] : ( mem(V0l1,ty_2Elist_2Elist(A_27a)) => ! [V1l2] : ( 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)) ) ) )))).
fof(conj_thm_2Erich__list_2EIS__PREFIX__REVERSE,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l1] : ( mem(V0l1,ty_2Elist_2Elist(A_27a)) => ! [V1l2] : ( 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)) ) ) )))).
fof(conj_thm_2Erich__list_2EIS__SUFFIX__REVERSE,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l2] : ( mem(V0l2,ty_2Elist_2Elist(A_27a)) => ! [V1l1] : ( 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)) ) ) )))).
fof(conj_thm_2Erich__list_2EIS__SUFFIX__CONS2__E,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,ty_2Elist_2Elist(A_27a)) => ! [V1h] : ( mem(V1h,A_27a) => ! [V2t] : ( 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)) ) ) ) )))).
fof(conj_thm_2Erich__list_2EIS__SUFFIX__REFL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => p(ap(ap(c_2Erich__list_2EIS__SUFFIX(A_27a),V0l),V0l)) )))).
fof(conj_thm_2Erich__list_2EIS__SUBLIST__REVERSE,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l1] : ( mem(V0l1,ty_2Elist_2Elist(A_27a)) => ! [V1l2] : ( 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)) ) ) )))).
fof(conj_thm_2Erich__list_2EPREFIX__FOLDR,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1l] : ( 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) ) ) )))).
fof(conj_thm_2Erich__list_2EPREFIX,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( ( ! [V0P] : ( 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] : ( mem(V1P,arr(A_27b,bool)) => ! [V2x] : ( mem(V2x,A_27b) => ! [V3l] : ( 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)) ) ) ) ) ))))).
fof(conj_thm_2Erich__list_2EIS__PREFIX__PREFIX,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1l] : ( 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)) ) )))).
fof(conj_thm_2Erich__list_2ELENGTH__SCANL,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(A_27a,arr(A_27b,A_27a))) => ! [V1e] : ( mem(V1e,A_27a) => ! [V2l] : ( mem(V2l,ty_2Elist_2Elist(A_27b)) => ( ap(c_2Elist_2ELENGTH(A_27a),ap(ap(ap(c_2Erich__list_2ESCANL(A_27b,A_27a),V0f),V1e),V2l)) = ap(c_2Enum_2ESUC,ap(c_2Elist_2ELENGTH(A_27b),V2l)) ) ) ) ))))).
fof(conj_thm_2Erich__list_2ELENGTH__SCANR,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(A_27a,arr(A_27b,A_27b))) => ! [V1e] : ( mem(V1e,A_27b) => ! [V2l] : ( mem(V2l,ty_2Elist_2Elist(A_27a)) => ( ap(c_2Elist_2ELENGTH(A_27b),ap(ap(ap(c_2Erich__list_2ESCANR(A_27a,A_27b),V0f),V1e),V2l)) = ap(c_2Enum_2ESUC,ap(c_2Elist_2ELENGTH(A_27a),V2l)) ) ) ) ))))).
fof(conj_thm_2Erich__list_2ECOMM__MONOID__FOLDL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0f] : ( mem(V0f,arr(A_27a,arr(A_27a,A_27a))) => ( p(ap(c_2Ecombin_2ECOMM(A_27a,A_27a),V0f)) => ! [V1e_27] : ( mem(V1e_27,A_27a) => ( p(ap(ap(c_2Ecombin_2EMONOID(A_27a),V0f),V1e_27)) => ! [V2e] : ( mem(V2e,A_27a) => ! [V3l] : ( 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)) ) ) ) ) ) ) )))).
fof(conj_thm_2Erich__list_2ECOMM__MONOID__FOLDR,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0f] : ( mem(V0f,arr(A_27a,arr(A_27a,A_27a))) => ( p(ap(c_2Ecombin_2ECOMM(A_27a,A_27a),V0f)) => ! [V1e_27] : ( mem(V1e_27,A_27a) => ( p(ap(ap(c_2Ecombin_2EMONOID(A_27a),V0f),V1e_27)) => ! [V2e] : ( mem(V2e,A_27a) => ! [V3l] : ( 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)) ) ) ) ) ) ) )))).
fof(conj_thm_2Erich__list_2EFCOMM__FOLDR__APPEND,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0g] : ( mem(V0g,arr(A_27a,arr(A_27a,A_27a))) => ! [V1f] : ( 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] : ( mem(V2e,A_27a) => ( p(ap(ap(c_2Ecombin_2ELEFT__ID(A_27a,A_27a),V0g),V2e)) => ! [V3l1] : ( mem(V3l1,ty_2Elist_2Elist(A_27b)) => ! [V4l2] : ( 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)) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Erich__list_2EFCOMM__FOLDL__APPEND,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(A_27a,arr(A_27b,A_27a))) => ! [V1g] : ( 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] : ( mem(V2e,A_27a) => ( p(ap(ap(c_2Ecombin_2ERIGHT__ID(A_27a,A_27a),V1g),V2e)) => ! [V3l1] : ( mem(V3l1,ty_2Elist_2Elist(A_27b)) => ! [V4l2] : ( 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)) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Erich__list_2EFOLDL__SINGLE,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(A_27a,arr(A_27b,A_27a))) => ! [V1e] : ( mem(V1e,A_27a) => ! [V2x] : ( 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) ) ) ) ))))).
fof(conj_thm_2Erich__list_2EFOLDR__SINGLE,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(A_27a,arr(A_27b,A_27b))) => ! [V1e] : ( mem(V1e,A_27b) => ! [V2x] : ( 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) ) ) ) ))))).
fof(conj_thm_2Erich__list_2EFOLDR__CONS__NIL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( 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 ) )))).
fof(conj_thm_2Erich__list_2EFOLDL__SNOC__NIL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( 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 ) )))).
fof(conj_thm_2Erich__list_2EFOLDR__FOLDL__REVERSE,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(A_27a,arr(A_27b,A_27b))) => ! [V1e] : ( mem(V1e,A_27b) => ! [V2l] : ( 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)) ) ) ) ))))).
fof(conj_thm_2Erich__list_2EFOLDL__FOLDR__REVERSE,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(A_27a,arr(A_27b,A_27a))) => ! [V1e] : ( mem(V1e,A_27a) => ! [V2l] : ( 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)) ) ) ) ))))).
fof(conj_thm_2Erich__list_2EFOLDR__REVERSE,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(A_27a,arr(A_27b,A_27b))) => ! [V1e] : ( mem(V1e,A_27b) => ! [V2l] : ( 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) ) ) ) ))))).
fof(conj_thm_2Erich__list_2EFOLDL__REVERSE,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(A_27a,arr(A_27b,A_27a))) => ! [V1e] : ( mem(V1e,A_27a) => ! [V2l] : ( 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) ) ) ) ))))).
fof(conj_thm_2Erich__list_2EFOLDR__MAP,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0f] : ( mem(V0f,arr(A_27a,arr(A_27b,A_27b))) => ! [V1e] : ( mem(V1e,A_27b) => ! [V2g] : ( mem(V2g,arr(A_27c,A_27a)) => ! [V3l] : ( 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) ) ) ) ) )))))).
fof(conj_thm_2Erich__list_2EFOLDL__MAP,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0f] : ( mem(V0f,arr(A_27a,arr(A_27b,A_27a))) => ! [V1e] : ( mem(V1e,A_27a) => ! [V2g] : ( mem(V2g,arr(A_27c,A_27b)) => ! [V3l] : ( 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) ) ) ) ) )))))).
fof(conj_thm_2Erich__list_2EEVERY__FOLDR,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1l] : ( 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)),c_2Ebool_2ET),V1l)) ) ) )))).
fof(conj_thm_2Erich__list_2EEVERY__FOLDL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1l] : ( 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)),c_2Ebool_2ET),V1l)) ) ) )))).
fof(conj_thm_2Erich__list_2EEXISTS__FOLDR,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1l] : ( 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)),c_2Ebool_2EF),V1l)) ) ) )))).
fof(conj_thm_2Erich__list_2EEXISTS__FOLDL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1l] : ( 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)),c_2Ebool_2EF),V1l)) ) ) )))).
fof(conj_thm_2Erich__list_2EEVERY__FOLDR__MAP,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1l] : ( 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))) ) ) )))).
fof(conj_thm_2Erich__list_2EEVERY__FOLDL__MAP,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1l] : ( 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))) ) ) )))).
fof(conj_thm_2Erich__list_2EEXISTS__FOLDR__MAP,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1l] : ( 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))) ) ) )))).
fof(conj_thm_2Erich__list_2EEXISTS__FOLDL__MAP,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1l] : ( 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))) ) ) )))).
fof(conj_thm_2Erich__list_2EFOLDR__FILTER,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(A_27a,arr(A_27b,A_27b))) => ! [V1e] : ( mem(V1e,A_27b) => ! [V2P] : ( mem(V2P,arr(A_27a,bool)) => ! [V3l] : ( 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) ) ) ) ) ))))).
fof(conj_thm_2Erich__list_2EFOLDL__FILTER,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(A_27a,arr(A_27b,A_27a))) => ! [V1e] : ( mem(V1e,A_27a) => ! [V2P] : ( mem(V2P,arr(A_27b,bool)) => ! [V3l] : ( 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) ) ) ) ) ))))).
fof(conj_thm_2Erich__list_2EASSOC__FOLDR__FLAT,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0f] : ( mem(V0f,arr(A_27a,arr(A_27a,A_27a))) => ( p(ap(c_2Ecombin_2EASSOC(A_27a),V0f)) => ! [V1e] : ( mem(V1e,A_27a) => ( p(ap(ap(c_2Ecombin_2ELEFT__ID(A_27a,A_27a),V0f),V1e)) => ! [V2l] : ( 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)) ) ) ) ) ) )))).
fof(conj_thm_2Erich__list_2EASSOC__FOLDL__FLAT,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0f] : ( mem(V0f,arr(A_27a,arr(A_27a,A_27a))) => ( p(ap(c_2Ecombin_2EASSOC(A_27a),V0f)) => ! [V1e] : ( mem(V1e,A_27a) => ( p(ap(ap(c_2Ecombin_2ERIGHT__ID(A_27a,A_27a),V0f),V1e)) => ! [V2l] : ( 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)) ) ) ) ) ) )))).
fof(conj_thm_2Erich__list_2EMAP__FLAT,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(A_27a,A_27b)) => ! [V1l] : ( 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)) ) ) ))))).
fof(conj_thm_2Erich__list_2EFILTER__FLAT,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1l] : ( 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)) ) ) )))).
fof(conj_thm_2Erich__list_2EEXISTS__DISJ,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1Q] : ( mem(V1Q,arr(A_27a,bool)) => ! [V2l] : ( 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)) ) ) ) ) )))).
fof(conj_thm_2Erich__list_2EMEM__FOLDR,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0y] : ( mem(V0y,A_27a) => ! [V1l] : ( 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)),c_2Ebool_2EF),V1l)) ) ) )))).
fof(conj_thm_2Erich__list_2EMEM__FOLDL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0y] : ( mem(V0y,A_27a) => ! [V1l] : ( 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)),c_2Ebool_2EF),V1l)) ) ) )))).
fof(conj_thm_2Erich__list_2ENULL__FOLDR,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( 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))),c_2Ebool_2ET),V0l)) ) )))).
fof(conj_thm_2Erich__list_2ENULL__FOLDL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( 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))),c_2Ebool_2ET),V0l)) ) )))).
fof(conj_thm_2Erich__list_2EMAP__REVERSE,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(A_27a,A_27b)) => ! [V1l] : ( 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)) ) ) ))))).
fof(conj_thm_2Erich__list_2ESEG__LENGTH__ID,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ap(ap(ap(c_2Erich__list_2ESEG(A_27a),ap(c_2Elist_2ELENGTH(A_27a),V0l)),c_2Enum_2E0),V0l) = V0l ) )))).
fof(conj_thm_2Erich__list_2ESEG__SUC__CONS,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2l] : ( mem(V2l,ty_2Elist_2Elist(A_27a)) => ! [V3x] : ( mem(V3x,A_27a) => ( ap(ap(ap(c_2Erich__list_2ESEG(A_27a),V0m),ap(c_2Enum_2ESUC,V1n)),ap(ap(c_2Elist_2ECONS(A_27a),V3x),V2l)) = ap(ap(ap(c_2Erich__list_2ESEG(A_27a),V0m),V1n),V2l) ) ) ) ) )))).
fof(conj_thm_2Erich__list_2ESEG__0__SNOC,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ! [V2x] : ( mem(V2x,A_27a) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0m),ap(c_2Elist_2ELENGTH(A_27a),V1l))) => ( ap(ap(ap(c_2Erich__list_2ESEG(A_27a),V0m),c_2Enum_2E0),ap(ap(c_2Elist_2ESNOC(A_27a),V2x),V1l)) = ap(ap(ap(c_2Erich__list_2ESEG(A_27a),V0m),c_2Enum_2E0),V1l) ) ) ) ) )))).
fof(conj_thm_2Erich__list_2EBUTLASTN__SEG,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0n),ap(c_2Elist_2ELENGTH(A_27a),V1l))) => ( ap(ap(c_2Erich__list_2EBUTLASTN(A_27a),V0n),V1l) = ap(ap(ap(c_2Erich__list_2ESEG(A_27a),ap(ap(c_2Earithmetic_2E_2D,ap(c_2Elist_2ELENGTH(A_27a),V1l)),V0n)),c_2Enum_2E0),V1l) ) ) ) )))).
fof(conj_thm_2Erich__list_2ELASTN__CONS,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0n),ap(c_2Elist_2ELENGTH(A_27a),V1l))) => ! [V2x] : ( mem(V2x,A_27a) => ( ap(ap(c_2Erich__list_2ELASTN(A_27a),V0n),ap(ap(c_2Elist_2ECONS(A_27a),V2x),V1l)) = ap(ap(c_2Erich__list_2ELASTN(A_27a),V0n),V1l) ) ) ) ) )))).
fof(conj_thm_2Erich__list_2ELENGTH__LASTN,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0n),ap(c_2Elist_2ELENGTH(A_27a),V1l))) => ( ap(c_2Elist_2ELENGTH(A_27a),ap(ap(c_2Erich__list_2ELASTN(A_27a),V0n),V1l)) = V0n ) ) ) )))).
fof(conj_thm_2Erich__list_2ELASTN__LENGTH__ID,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ap(ap(c_2Erich__list_2ELASTN(A_27a),ap(c_2Elist_2ELENGTH(A_27a),V0l)),V0l) = V0l ) )))).
fof(conj_thm_2Erich__list_2ELASTN__LASTN,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2m] : ( mem(V2m,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V2m),ap(c_2Elist_2ELENGTH(A_27a),V0l))) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V1n),V2m)) => ( ap(ap(c_2Erich__list_2ELASTN(A_27a),V1n),ap(ap(c_2Erich__list_2ELASTN(A_27a),V2m),V0l)) = ap(ap(c_2Erich__list_2ELASTN(A_27a),V1n),V0l) ) ) ) ) ) )))).
fof(conj_thm_2Erich__list_2ETAKE__SNOC,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0n),ap(c_2Elist_2ELENGTH(A_27a),V1l))) => ! [V2x] : ( mem(V2x,A_27a) => ( ap(ap(c_2Elist_2ETAKE(A_27a),V0n),ap(ap(c_2Elist_2ESNOC(A_27a),V2x),V1l)) = ap(ap(c_2Elist_2ETAKE(A_27a),V0n),V1l) ) ) ) ) )))).
fof(conj_thm_2Erich__list_2EBUTLASTN__SUC__FRONT,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V0n),ap(c_2Elist_2ELENGTH(A_27a),V1l))) => ( ap(ap(c_2Erich__list_2EBUTLASTN(A_27a),ap(c_2Enum_2ESUC,V0n)),V1l) = ap(ap(c_2Erich__list_2EBUTLASTN(A_27a),V0n),ap(c_2Elist_2EFRONT(A_27a),V1l)) ) ) ) )))).
fof(conj_thm_2Erich__list_2EBUTLASTN__FRONT,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V0n),ap(c_2Elist_2ELENGTH(A_27a),V1l))) => ( ap(ap(c_2Erich__list_2EBUTLASTN(A_27a),V0n),ap(c_2Elist_2EFRONT(A_27a),V1l)) = ap(c_2Elist_2EFRONT(A_27a),ap(ap(c_2Erich__list_2EBUTLASTN(A_27a),V0n),V1l)) ) ) ) )))).
fof(conj_thm_2Erich__list_2ELENGTH__BUTLASTN,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0n),ap(c_2Elist_2ELENGTH(A_27a),V1l))) => ( ap(c_2Elist_2ELENGTH(A_27a),ap(ap(c_2Erich__list_2EBUTLASTN(A_27a),V0n),V1l)) = ap(ap(c_2Earithmetic_2E_2D,ap(c_2Elist_2ELENGTH(A_27a),V1l)),V0n) ) ) ) )))).
fof(conj_thm_2Erich__list_2EBUTLASTN__BUTLASTN,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2l] : ( mem(V2l,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2B,V1n),V0m)),ap(c_2Elist_2ELENGTH(A_27a),V2l))) => ( ap(ap(c_2Erich__list_2EBUTLASTN(A_27a),V1n),ap(ap(c_2Erich__list_2EBUTLASTN(A_27a),V0m),V2l)) = ap(ap(c_2Erich__list_2EBUTLASTN(A_27a),ap(ap(c_2Earithmetic_2E_2B,V1n),V0m)),V2l) ) ) ) ) )))).
fof(conj_thm_2Erich__list_2EAPPEND__BUTLASTN__LASTN,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0n),ap(c_2Elist_2ELENGTH(A_27a),V1l))) => ( ap(ap(c_2Elist_2EAPPEND(A_27a),ap(ap(c_2Erich__list_2EBUTLASTN(A_27a),V0n),V1l)),ap(ap(c_2Erich__list_2ELASTN(A_27a),V0n),V1l)) = V1l ) ) ) )))).
fof(conj_thm_2Erich__list_2EAPPEND__TAKE__LASTN,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2l] : ( mem(V2l,ty_2Elist_2Elist(A_27a)) => ( ( ap(ap(c_2Earithmetic_2E_2B,V0m),V1n) = ap(c_2Elist_2ELENGTH(A_27a),V2l) ) => ( ap(ap(c_2Elist_2EAPPEND(A_27a),ap(ap(c_2Elist_2ETAKE(A_27a),V1n),V2l)),ap(ap(c_2Erich__list_2ELASTN(A_27a),V0m),V2l)) = V2l ) ) ) ) )))).
fof(conj_thm_2Erich__list_2EBUTLASTN__APPEND2,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1l1] : ( mem(V1l1,ty_2Elist_2Elist(A_27a)) => ! [V2l2] : ( mem(V2l2,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0n),ap(c_2Elist_2ELENGTH(A_27a),V2l2))) => ( ap(ap(c_2Erich__list_2EBUTLASTN(A_27a),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),V0n),V2l2)) ) ) ) ) )))).
fof(conj_thm_2Erich__list_2EBUTLASTN__LENGTH__APPEND,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l2] : ( mem(V0l2,ty_2Elist_2Elist(A_27a)) => ! [V1l1] : ( 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 ) ) )))).
fof(conj_thm_2Erich__list_2ELASTN__LENGTH__APPEND,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l2] : ( mem(V0l2,ty_2Elist_2Elist(A_27a)) => ! [V1l1] : ( 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 ) ) )))).
fof(conj_thm_2Erich__list_2EBUTLASTN__CONS,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0n),ap(c_2Elist_2ELENGTH(A_27a),V1l))) => ! [V2x] : ( mem(V2x,A_27a) => ( ap(ap(c_2Erich__list_2EBUTLASTN(A_27a),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),V0n),V1l)) ) ) ) ) )))).
fof(conj_thm_2Erich__list_2EBUTLASTN__LENGTH__CONS,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ! [V1x] : ( 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)) ) ) )))).
fof(conj_thm_2Erich__list_2ELAST__LASTN__LAST,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0n),ap(c_2Elist_2ELENGTH(A_27a),V1l))) => ( p(ap(ap(c_2Eprim__rec_2E_3C,c_2Enum_2E0),V0n)) => ( ap(c_2Elist_2ELAST(A_27a),ap(ap(c_2Erich__list_2ELASTN(A_27a),V0n),V1l)) = ap(c_2Elist_2ELAST(A_27a),V1l) ) ) ) ) )))).
fof(conj_thm_2Erich__list_2EBUTLASTN__LASTN__NIL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0n),ap(c_2Elist_2ELENGTH(A_27a),V1l))) => ( ap(ap(c_2Erich__list_2EBUTLASTN(A_27a),V0n),ap(ap(c_2Erich__list_2ELASTN(A_27a),V0n),V1l)) = c_2Elist_2ENIL(A_27a) ) ) ) )))).
fof(conj_thm_2Erich__list_2ELASTN__BUTLASTN,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1m] : ( mem(V1m,ty_2Enum_2Enum) => ! [V2l] : ( mem(V2l,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2B,V0n),V1m)),ap(c_2Elist_2ELENGTH(A_27a),V2l))) => ( ap(ap(c_2Erich__list_2ELASTN(A_27a),V0n),ap(ap(c_2Erich__list_2EBUTLASTN(A_27a),V1m),V2l)) = ap(ap(c_2Erich__list_2EBUTLASTN(A_27a),V1m),ap(ap(c_2Erich__list_2ELASTN(A_27a),ap(ap(c_2Earithmetic_2E_2B,V0n),V1m)),V2l)) ) ) ) ) )))).
fof(conj_thm_2Erich__list_2EBUTLASTN__LASTN,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ! [V2l] : ( mem(V2l,ty_2Elist_2Elist(A_27a)) => ( ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0m),V1n)) & p(ap(ap(c_2Earithmetic_2E_3C_3D,V1n),ap(c_2Elist_2ELENGTH(A_27a),V2l))) ) => ( ap(ap(c_2Erich__list_2EBUTLASTN(A_27a),V0m),ap(ap(c_2Erich__list_2ELASTN(A_27a),V1n),V2l)) = ap(ap(c_2Erich__list_2ELASTN(A_27a),ap(ap(c_2Earithmetic_2E_2D,V1n),V0m)),ap(ap(c_2Erich__list_2EBUTLASTN(A_27a),V0m),V2l)) ) ) ) ) )))).
fof(conj_thm_2Erich__list_2ELASTN__1,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( 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,c_2Earithmetic_2EZERO))),V0l) = ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2ELAST(A_27a),V0l)),c_2Elist_2ENIL(A_27a)) ) ) )))).
fof(conj_thm_2Erich__list_2EBUTLASTN__1,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( 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,c_2Earithmetic_2EZERO))),V0l) = ap(c_2Elist_2EFRONT(A_27a),V0l) ) ) )))).
fof(conj_thm_2Erich__list_2EBUTLASTN__APPEND1,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l2] : ( mem(V0l2,ty_2Elist_2Elist(A_27a)) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Elist_2ELENGTH(A_27a),V0l2)),V1n)) => ! [V2l1] : ( mem(V2l1,ty_2Elist_2Elist(A_27a)) => ( ap(ap(c_2Erich__list_2EBUTLASTN(A_27a),V1n),ap(ap(c_2Elist_2EAPPEND(A_27a),V2l1),V0l2)) = ap(ap(c_2Erich__list_2EBUTLASTN(A_27a),ap(ap(c_2Earithmetic_2E_2D,V1n),ap(c_2Elist_2ELENGTH(A_27a),V0l2))),V2l1) ) ) ) ) )))).
fof(conj_thm_2Erich__list_2ELASTN__APPEND2,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1l2] : ( mem(V1l2,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0n),ap(c_2Elist_2ELENGTH(A_27a),V1l2))) => ! [V2l1] : ( mem(V2l1,ty_2Elist_2Elist(A_27a)) => ( ap(ap(c_2Erich__list_2ELASTN(A_27a),V0n),ap(ap(c_2Elist_2EAPPEND(A_27a),V2l1),V1l2)) = ap(ap(c_2Erich__list_2ELASTN(A_27a),V0n),V1l2) ) ) ) ) )))).
fof(conj_thm_2Erich__list_2ELASTN__APPEND1,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l2] : ( mem(V0l2,ty_2Elist_2Elist(A_27a)) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Elist_2ELENGTH(A_27a),V0l2)),V1n)) => ! [V2l1] : ( mem(V2l1,ty_2Elist_2Elist(A_27a)) => ( ap(ap(c_2Erich__list_2ELASTN(A_27a),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,V1n),ap(c_2Elist_2ELENGTH(A_27a),V0l2))),V2l1)),V0l2) ) ) ) ) )))).
fof(conj_thm_2Erich__list_2ELASTN__MAP,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0n),ap(c_2Elist_2ELENGTH(A_27a),V1l))) => ! [V2f] : ( mem(V2f,arr(A_27a,A_27b)) => ( ap(ap(c_2Erich__list_2ELASTN(A_27b),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),V0n),V1l)) ) ) ) ) ))))).
fof(conj_thm_2Erich__list_2EBUTLASTN__MAP,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0n),ap(c_2Elist_2ELENGTH(A_27a),V1l))) => ! [V2f] : ( mem(V2f,arr(A_27a,A_27b)) => ( ap(ap(c_2Erich__list_2EBUTLASTN(A_27b),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),V0n),V1l)) ) ) ) ) ))))).
fof(conj_thm_2Erich__list_2EEVERY__LASTN,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Elist_2EEVERY(A_27a),V0P),V1l)) => ! [V2m] : ( mem(V2m,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,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),V2m),V1l))) ) ) ) ) )))).
fof(conj_thm_2Erich__list_2EEVERY__BUTLASTN,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Elist_2EEVERY(A_27a),V0P),V1l)) => ! [V2m] : ( mem(V2m,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,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),V2m),V1l))) ) ) ) ) )))).
fof(conj_thm_2Erich__list_2ETAKE__TAKE__T,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V2n),V0m)) => ( ap(ap(c_2Elist_2ETAKE(A_27a),V2n),ap(ap(c_2Elist_2ETAKE(A_27a),V0m),V1l)) = ap(ap(c_2Elist_2ETAKE(A_27a),V2n),V1l) ) ) ) ) )))).
fof(conj_thm_2Erich__list_2ETAKE__TAKE,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0m] : ( mem(V0m,ty_2Enum_2Enum) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V0m),ap(c_2Elist_2ELENGTH(A_27a),V1l))) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Earithmetic_2E_3C_3D,V2n),V0m)) => ( ap(ap(c_2Elist_2ETAKE(A_27a),V2n),ap(ap(c_2Elist_2ETAKE(A_27a),V0m),V1l)) = ap(ap(c_2Elist_2ETAKE(A_27a),V2n),V1l) ) ) ) ) ) )))).
fof(conj_thm_2Erich__list_2EDROP__LENGTH__NIL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( 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) ) )))).
fof(conj_thm_2Erich__list_2EBUTLASTN__LENGTH__NIL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( 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) ) )))).
fof(conj_thm_2Erich__list_2EDROP__APPEND,conjecture,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1l1] : ( mem(V1l1,ty_2Elist_2Elist(A_27a)) => ! [V2l2] : ( mem(V2l2,ty_2Elist_2Elist(A_27a)) => ( ap(ap(c_2Elist_2EDROP(A_27a),V0n),ap(ap(c_2Elist_2EAPPEND(A_27a),V1l1),V2l2)) = ap(ap(c_2Elist_2EAPPEND(A_27a),ap(ap(c_2Elist_2EDROP(A_27a),V0n),V1l1)),ap(ap(c_2Elist_2EDROP(A_27a),ap(ap(c_2Earithmetic_2E_2D,V0n),ap(c_2Elist_2ELENGTH(A_27a),V1l1))),V2l2)) ) ) ) )))).
