include('Axioms/set_relation+2.ax').
fof(ne_ty_2Elist_2Elist,axiom,( ! [A0] : ( ne(A0) => ne(ty_2Elist_2Elist(A0)) ) )).
fof(mem_c_2Elist_2EALL__DISTINCT,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2EALL__DISTINCT(A_27a),arr(ty_2Elist_2Elist(A_27a),bool)) ) )).
fof(mem_c_2Elist_2EAPPEND,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2EAPPEND(A_27a),arr(ty_2Elist_2Elist(A_27a),arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a)))) ) )).
fof(mem_c_2Elist_2ECONS,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2ECONS(A_27a),arr(A_27a,arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a)))) ) )).
fof(mem_c_2Elist_2EDROP,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2EDROP(A_27a),arr(ty_2Enum_2Enum,arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a)))) ) )).
fof(mem_c_2Elist_2EEL,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2EEL(A_27a),arr(ty_2Enum_2Enum,arr(ty_2Elist_2Elist(A_27a),A_27a))) ) )).
fof(mem_c_2Elist_2EEVERY,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2EEVERY(A_27a),arr(arr(A_27a,bool),arr(ty_2Elist_2Elist(A_27a),bool))) ) )).
fof(mem_c_2Elist_2EEVERYi,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2EEVERYi(A_27a),arr(arr(ty_2Enum_2Enum,arr(A_27a,bool)),arr(ty_2Elist_2Elist(A_27a),bool))) ) )).
fof(mem_c_2Elist_2EEXISTS,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2EEXISTS(A_27a),arr(arr(A_27a,bool),arr(ty_2Elist_2Elist(A_27a),bool))) ) )).
fof(mem_c_2Elist_2EFILTER,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2EFILTER(A_27a),arr(arr(A_27a,bool),arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a)))) ) )).
fof(mem_c_2Elist_2EFIND,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2EFIND(A_27a),arr(arr(A_27a,bool),arr(ty_2Elist_2Elist(A_27a),ty_2Eoption_2Eoption(A_27a)))) ) )).
fof(mem_c_2Elist_2EFLAT,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2EFLAT(A_27a),arr(ty_2Elist_2Elist(ty_2Elist_2Elist(A_27a)),ty_2Elist_2Elist(A_27a))) ) )).
fof(mem_c_2Elist_2EFOLDL,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Elist_2EFOLDL(A_27a,A_27b),arr(arr(A_27b,arr(A_27a,A_27b)),arr(A_27b,arr(ty_2Elist_2Elist(A_27a),A_27b)))) ) ) )).
fof(mem_c_2Elist_2EFOLDL2,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [A_27c] : ( ne(A_27c) => mem(c_2Elist_2EFOLDL2(A_27a,A_27b,A_27c),arr(arr(A_27a,arr(A_27b,arr(A_27c,A_27a))),arr(A_27a,arr(ty_2Elist_2Elist(A_27b),arr(ty_2Elist_2Elist(A_27c),A_27a))))) ) ) ) )).
fof(mem_c_2Elist_2EFOLDR,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Elist_2EFOLDR(A_27a,A_27b),arr(arr(A_27a,arr(A_27b,A_27b)),arr(A_27b,arr(ty_2Elist_2Elist(A_27a),A_27b)))) ) ) )).
fof(mem_c_2Elist_2EFRONT,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2EFRONT(A_27a),arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a))) ) )).
fof(mem_c_2Elist_2EGENLIST,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2EGENLIST(A_27a),arr(arr(ty_2Enum_2Enum,A_27a),arr(ty_2Enum_2Enum,ty_2Elist_2Elist(A_27a)))) ) )).
fof(mem_c_2Elist_2EGENLIST__AUX,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2EGENLIST__AUX(A_27a),arr(arr(ty_2Enum_2Enum,A_27a),arr(ty_2Enum_2Enum,arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a))))) ) )).
fof(mem_c_2Elist_2EHD,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2EHD(A_27a),arr(ty_2Elist_2Elist(A_27a),A_27a)) ) )).
fof(mem_c_2Elist_2EINDEX__FIND,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2EINDEX__FIND(A_27a),arr(ty_2Enum_2Enum,arr(arr(A_27a,bool),arr(ty_2Elist_2Elist(A_27a),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Enum_2Enum,A_27a)))))) ) )).
fof(mem_c_2Elist_2EINDEX__OF,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2EINDEX__OF(A_27a),arr(A_27a,arr(ty_2Elist_2Elist(A_27a),ty_2Eoption_2Eoption(ty_2Enum_2Enum)))) ) )).
fof(mem_c_2Elist_2ELAST,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2ELAST(A_27a),arr(ty_2Elist_2Elist(A_27a),A_27a)) ) )).
fof(mem_c_2Elist_2ELEN,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2ELEN(A_27a),arr(ty_2Elist_2Elist(A_27a),arr(ty_2Enum_2Enum,ty_2Enum_2Enum))) ) )).
fof(mem_c_2Elist_2ELENGTH,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2ELENGTH(A_27a),arr(ty_2Elist_2Elist(A_27a),ty_2Enum_2Enum)) ) )).
fof(mem_c_2Elist_2ELIST__APPLY,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Elist_2ELIST__APPLY(A_27a,A_27b),arr(ty_2Elist_2Elist(arr(A_27b,A_27a)),arr(ty_2Elist_2Elist(A_27b),ty_2Elist_2Elist(A_27a)))) ) ) )).
fof(mem_c_2Elist_2ELIST__BIND,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Elist_2ELIST__BIND(A_27a,A_27b),arr(ty_2Elist_2Elist(A_27b),arr(arr(A_27b,ty_2Elist_2Elist(A_27a)),ty_2Elist_2Elist(A_27a)))) ) ) )).
fof(mem_c_2Elist_2ELIST__GUARD,axiom,( mem(c_2Elist_2ELIST__GUARD,arr(bool,ty_2Elist_2Elist(ty_2Eone_2Eone))) )).
fof(mem_c_2Elist_2ELIST__IGNORE__BIND,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Elist_2ELIST__IGNORE__BIND(A_27a,A_27b),arr(ty_2Elist_2Elist(A_27b),arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a)))) ) ) )).
fof(mem_c_2Elist_2ELIST__LIFT2,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [A_27c] : ( ne(A_27c) => mem(c_2Elist_2ELIST__LIFT2(A_27a,A_27b,A_27c),arr(arr(A_27b,arr(A_27c,A_27a)),arr(ty_2Elist_2Elist(A_27b),arr(ty_2Elist_2Elist(A_27c),ty_2Elist_2Elist(A_27a))))) ) ) ) )).
fof(mem_c_2Elist_2ELIST__REL,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Elist_2ELIST__REL(A_27a,A_27b),arr(arr(A_27a,arr(A_27b,bool)),arr(ty_2Elist_2Elist(A_27a),arr(ty_2Elist_2Elist(A_27b),bool)))) ) ) )).
fof(mem_c_2Elist_2ELIST__TO__SET,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2ELIST__TO__SET(A_27a),arr(ty_2Elist_2Elist(A_27a),arr(A_27a,bool))) ) )).
fof(mem_c_2Elist_2ELLEX,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2ELLEX(A_27a),arr(arr(A_27a,arr(A_27a,bool)),arr(ty_2Elist_2Elist(A_27a),arr(ty_2Elist_2Elist(A_27a),bool)))) ) )).
fof(mem_c_2Elist_2ELRC,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2ELRC(A_27a),arr(arr(A_27a,arr(A_27a,bool)),arr(ty_2Elist_2Elist(A_27a),arr(A_27a,arr(A_27a,bool))))) ) )).
fof(mem_c_2Elist_2ELUPDATE,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2ELUPDATE(A_27a),arr(A_27a,arr(ty_2Enum_2Enum,arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a))))) ) )).
fof(mem_c_2Elist_2EMAP,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Elist_2EMAP(A_27a,A_27b),arr(arr(A_27a,A_27b),arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27b)))) ) ) )).
fof(mem_c_2Elist_2EMAP2,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [A_27c] : ( ne(A_27c) => mem(c_2Elist_2EMAP2(A_27a,A_27b,A_27c),arr(arr(A_27b,arr(A_27c,A_27a)),arr(ty_2Elist_2Elist(A_27b),arr(ty_2Elist_2Elist(A_27c),ty_2Elist_2Elist(A_27a))))) ) ) ) )).
fof(mem_c_2Elist_2ENIL,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2ENIL(A_27a),ty_2Elist_2Elist(A_27a)) ) )).
fof(mem_c_2Elist_2ENULL,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2ENULL(A_27a),arr(ty_2Elist_2Elist(A_27a),bool)) ) )).
fof(mem_c_2Elist_2EOPT__MMAP,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Elist_2EOPT__MMAP(A_27a,A_27b),arr(arr(A_27b,ty_2Eoption_2Eoption(A_27a)),arr(ty_2Elist_2Elist(A_27b),ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a))))) ) ) )).
fof(mem_c_2Elist_2EPAD__LEFT,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2EPAD__LEFT(A_27a),arr(A_27a,arr(ty_2Enum_2Enum,arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a))))) ) )).
fof(mem_c_2Elist_2EPAD__RIGHT,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2EPAD__RIGHT(A_27a),arr(A_27a,arr(ty_2Enum_2Enum,arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a))))) ) )).
fof(mem_c_2Elist_2EREV,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2EREV(A_27a),arr(ty_2Elist_2Elist(A_27a),arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a)))) ) )).
fof(mem_c_2Elist_2EREVERSE,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2EREVERSE(A_27a),arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a))) ) )).
fof(mem_c_2Elist_2ESET__TO__LIST,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2ESET__TO__LIST(A_27a),arr(arr(A_27a,bool),ty_2Elist_2Elist(A_27a))) ) )).
fof(mem_c_2Elist_2ESHORTLEX,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2ESHORTLEX(A_27a),arr(arr(A_27a,arr(A_27a,bool)),arr(ty_2Elist_2Elist(A_27a),arr(ty_2Elist_2Elist(A_27a),bool)))) ) )).
fof(mem_c_2Elist_2ESNOC,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2ESNOC(A_27a),arr(A_27a,arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a)))) ) )).
fof(mem_c_2Elist_2ESUM,axiom,( mem(c_2Elist_2ESUM,arr(ty_2Elist_2Elist(ty_2Enum_2Enum),ty_2Enum_2Enum)) )).
fof(mem_c_2Elist_2ESUM__ACC,axiom,( mem(c_2Elist_2ESUM__ACC,arr(ty_2Elist_2Elist(ty_2Enum_2Enum),arr(ty_2Enum_2Enum,ty_2Enum_2Enum))) )).
fof(mem_c_2Elist_2ETAKE,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2ETAKE(A_27a),arr(ty_2Enum_2Enum,arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a)))) ) )).
fof(mem_c_2Elist_2ETL,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2ETL(A_27a),arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a))) ) )).
fof(mem_c_2Elist_2EUNIQUE,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2EUNIQUE(A_27a),arr(A_27a,arr(ty_2Elist_2Elist(A_27a),bool))) ) )).
fof(mem_c_2Elist_2EUNZIP,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Elist_2EUNZIP(A_27a,A_27b),arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)),ty_2Epair_2Eprod(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27b)))) ) ) )).
fof(mem_c_2Elist_2EZIP,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Elist_2EZIP(A_27a,A_27b),arr(ty_2Epair_2Eprod(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27b)),ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b)))) ) ) )).
fof(mem_c_2Elist_2EdropWhile,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2EdropWhile(A_27a),arr(arr(A_27a,bool),arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a)))) ) )).
fof(mem_c_2Elist_2EisPREFIX,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2EisPREFIX(A_27a),arr(ty_2Elist_2Elist(A_27a),arr(ty_2Elist_2Elist(A_27a),bool))) ) )).
fof(mem_c_2Elist_2Elist__CASE,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Elist_2Elist__CASE(A_27a,A_27b),arr(ty_2Elist_2Elist(A_27a),arr(A_27b,arr(arr(A_27a,arr(ty_2Elist_2Elist(A_27a),A_27b)),A_27b)))) ) ) )).
fof(mem_c_2Elist_2Elist__size,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2Elist__size(A_27a),arr(arr(A_27a,ty_2Enum_2Enum),arr(ty_2Elist_2Elist(A_27a),ty_2Enum_2Enum))) ) )).
fof(mem_c_2Elist_2Enub,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2Enub(A_27a),arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a))) ) )).
fof(mem_c_2Elist_2EoEL,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2EoEL(A_27a),arr(ty_2Enum_2Enum,arr(ty_2Elist_2Elist(A_27a),ty_2Eoption_2Eoption(A_27a)))) ) )).
fof(mem_c_2Elist_2EoHD,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Elist_2EoHD(A_27a),arr(ty_2Elist_2Elist(A_27a),ty_2Eoption_2Eoption(A_27a))) ) )).
fof(mem_c_2Elist_2EsplitAtPki,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Elist_2EsplitAtPki(A_27a,A_27b),arr(arr(ty_2Enum_2Enum,arr(A_27b,bool)),arr(arr(ty_2Elist_2Elist(A_27b),arr(ty_2Elist_2Elist(A_27b),A_27a)),arr(ty_2Elist_2Elist(A_27b),A_27a)))) ) ) )).
fof(ax_thm_2Elist_2Elist__TY__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ? [V0rep] : ( mem(V0rep,arr(ty_2Elist_2Elist(A_27a),ty_2Eind__type_2Erecspace(A_27a))) & p(ap(ap(c_2Ebool_2ETYPE__DEFINITION(ty_2Eind__type_2Erecspace(A_27a),ty_2Elist_2Elist(A_27a)),f386(A_27a)),V0rep)) ) ) )).
fof(ax_thm_2Elist_2Elist__case__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ( ( ! [V0v] : ( mem(V0v,A_27b) => ! [V1f] : ( mem(V1f,arr(A_27a,arr(ty_2Elist_2Elist(A_27a),A_27b))) => ( ap(ap(ap(c_2Elist_2Elist__CASE(A_27a,A_27b),c_2Elist_2ENIL(A_27a)),V0v),V1f) = V0v ) ) ) ) & ! [V2a0] : ( mem(V2a0,A_27a) => ! [V3a1] : ( mem(V3a1,ty_2Elist_2Elist(A_27a)) => ! [V4v] : ( mem(V4v,A_27b) => ! [V5f] : ( mem(V5f,arr(A_27a,arr(ty_2Elist_2Elist(A_27a),A_27b))) => ( ap(ap(ap(c_2Elist_2Elist__CASE(A_27a,A_27b),ap(ap(c_2Elist_2ECONS(A_27a),V2a0),V3a1)),V4v),V5f) = ap(ap(V5f,V2a0),V3a1) ) ) ) ) ) ) ) ) )).
fof(ax_thm_2Elist_2Elist__size__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0f] : ( mem(V0f,arr(A_27a,ty_2Enum_2Enum)) => ( ap(ap(c_2Elist_2Elist__size(A_27a),V0f),c_2Elist_2ENIL(A_27a)) = c_2Enum_2E0 ) ) ) & ! [V1f] : ( mem(V1f,arr(A_27a,ty_2Enum_2Enum)) => ! [V2a0] : ( mem(V2a0,A_27a) => ! [V3a1] : ( mem(V3a1,ty_2Elist_2Elist(A_27a)) => ( ap(ap(c_2Elist_2Elist__size(A_27a),V1f),ap(ap(c_2Elist_2ECONS(A_27a),V2a0),V3a1)) = ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),ap(ap(c_2Earithmetic_2E_2B,ap(V1f,V2a0)),ap(ap(c_2Elist_2Elist__size(A_27a),V1f),V3a1))) ) ) ) ) ) ) )).
fof(conj_thm_2Elist_2Edatatype__list,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0list] : ( mem(V0list,arr(ty_2Elist_2Elist(A_27a),arr(arr(A_27a,arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a))),bool))) => p(ap(c_2Ebool_2EDATATYPE(bool),ap(ap(V0list,c_2Elist_2ENIL(A_27a)),c_2Elist_2ECONS(A_27a)))) )))).
fof(conj_thm_2Elist_2Elist__11,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a0] : ( mem(V0a0,A_27a) => ! [V1a1] : ( mem(V1a1,ty_2Elist_2Elist(A_27a)) => ! [V2a0_27] : ( mem(V2a0_27,A_27a) => ! [V3a1_27] : ( mem(V3a1_27,ty_2Elist_2Elist(A_27a)) => ( ( ap(ap(c_2Elist_2ECONS(A_27a),V0a0),V1a1) = ap(ap(c_2Elist_2ECONS(A_27a),V2a0_27),V3a1_27) ) <=> ( ( V0a0 = V2a0_27 ) & ( V1a1 = V3a1_27 ) ) ) ) ) ) )))).
fof(conj_thm_2Elist_2Elist__distinct,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a1] : ( mem(V0a1,ty_2Elist_2Elist(A_27a)) => ! [V1a0] : ( mem(V1a0,A_27a) => ( ~~ ( c_2Elist_2ENIL(A_27a) = ap(ap(c_2Elist_2ECONS(A_27a),V1a0),V0a1) ) ) ) )))).
fof(conj_thm_2Elist_2Elist__Axiom,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f0] : ( mem(V0f0,A_27b) => ! [V1f1] : ( mem(V1f1,arr(A_27a,arr(ty_2Elist_2Elist(A_27a),arr(A_27b,A_27b)))) => ? [V2fn] : ( mem(V2fn,arr(ty_2Elist_2Elist(A_27a),A_27b)) & ( ( ap(V2fn,c_2Elist_2ENIL(A_27a)) = V0f0 ) & ! [V3a0] : ( mem(V3a0,A_27a) => ! [V4a1] : ( mem(V4a1,ty_2Elist_2Elist(A_27a)) => ( ap(V2fn,ap(ap(c_2Elist_2ECONS(A_27a),V3a0),V4a1)) = ap(ap(ap(V1f1,V3a0),V4a1),ap(V2fn,V4a1)) ) ) ) ) ) ) ))))).
fof(conj_thm_2Elist_2Elist__case__cong,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0v_27] : ( mem(V0v_27,A_27b) => ! [V1f_27] : ( mem(V1f_27,arr(A_27a,arr(ty_2Elist_2Elist(A_27a),A_27b))) => ! [V2M] : ( mem(V2M,ty_2Elist_2Elist(A_27a)) => ! [V3M_27] : ( mem(V3M_27,ty_2Elist_2Elist(A_27a)) => ! [V4v] : ( mem(V4v,A_27b) => ! [V5f] : ( mem(V5f,arr(A_27a,arr(ty_2Elist_2Elist(A_27a),A_27b))) => ( ( ( V2M = V3M_27 ) & ( ( ( V3M_27 = c_2Elist_2ENIL(A_27a) ) => ( V4v = V0v_27 ) ) & ! [V6a0] : ( mem(V6a0,A_27a) => ! [V7a1] : ( mem(V7a1,ty_2Elist_2Elist(A_27a)) => ( ( V3M_27 = ap(ap(c_2Elist_2ECONS(A_27a),V6a0),V7a1) ) => ( ap(ap(V5f,V6a0),V7a1) = ap(ap(V1f_27,V6a0),V7a1) ) ) ) ) ) ) => ( ap(ap(ap(c_2Elist_2Elist__CASE(A_27a,A_27b),V2M),V4v),V5f) = ap(ap(ap(c_2Elist_2Elist__CASE(A_27a,A_27b),V3M_27),V0v_27),V1f_27) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Elist_2Elist__case__eq,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0x] : ( mem(V0x,ty_2Elist_2Elist(A_27a)) => ! [V1v] : ( mem(V1v,A_27b) => ! [V2f] : ( mem(V2f,arr(A_27a,arr(ty_2Elist_2Elist(A_27a),A_27b))) => ! [V3v_27] : ( mem(V3v_27,A_27b) => ( ( ap(ap(ap(c_2Elist_2Elist__CASE(A_27a,A_27b),V0x),V1v),V2f) = V3v_27 ) <=> ( ( ( V0x = c_2Elist_2ENIL(A_27a) ) & ( V1v = V3v_27 ) ) | ? [V4a] : ( mem(V4a,A_27a) & ? [V5l] : ( mem(V5l,ty_2Elist_2Elist(A_27a)) & ( ( V0x = ap(ap(c_2Elist_2ECONS(A_27a),V4a),V5l) ) & ( ap(ap(V2f,V4a),V5l) = V3v_27 ) ) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Elist_2Elist__Axiom__old,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0x] : ( mem(V0x,A_27b) => ! [V1f] : ( mem(V1f,arr(A_27b,arr(A_27a,arr(ty_2Elist_2Elist(A_27a),A_27b)))) => p(ap(c_2Ebool_2E_3F_21(arr(ty_2Elist_2Elist(A_27a),A_27b)),f389(A_27b,A_27a,V0x,V1f))) ) ))))).
fof(ax_thm_2Elist_2ENULL__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( p(ap(c_2Elist_2ENULL(A_27a),c_2Elist_2ENIL(A_27a))) <=> $true ) & ! [V0h] : ( mem(V0h,A_27a) => ! [V1t] : ( mem(V1t,ty_2Elist_2Elist(A_27a)) => ( p(ap(c_2Elist_2ENULL(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V0h),V1t))) <=> $false ) ) ) ) ) )).
fof(ax_thm_2Elist_2EHD,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0h] : ( mem(V0h,A_27a) => ! [V1t] : ( mem(V1t,ty_2Elist_2Elist(A_27a)) => ( ap(c_2Elist_2EHD(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V0h),V1t)) = V0h ) ) ) ) )).
fof(ax_thm_2Elist_2ETL__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ap(c_2Elist_2ETL(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_2Elist_2ETL(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V0h),V1t)) = V1t ) ) ) ) ) )).
fof(conj_thm_2Elist_2ETL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0h] : ( mem(V0h,A_27a) => ! [V1t] : ( mem(V1t,ty_2Elist_2Elist(A_27a)) => ( ap(c_2Elist_2ETL(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V0h),V1t)) = V1t ) ) )))).
fof(ax_thm_2Elist_2ESUM,axiom, ( ( ap(c_2Elist_2ESUM,c_2Elist_2ENIL(ty_2Enum_2Enum)) = c_2Enum_2E0 ) & ! [V0h] : ( mem(V0h,ty_2Enum_2Enum) => ! [V1t] : ( mem(V1t,ty_2Elist_2Elist(ty_2Enum_2Enum)) => ( ap(c_2Elist_2ESUM,ap(ap(c_2Elist_2ECONS(ty_2Enum_2Enum),V0h),V1t)) = ap(ap(c_2Earithmetic_2E_2B,V0h),ap(c_2Elist_2ESUM,V1t)) ) ) ) )).
fof(ax_thm_2Elist_2EAPPEND,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ap(ap(c_2Elist_2EAPPEND(A_27a),c_2Elist_2ENIL(A_27a)),V0l) = V0l ) ) ) & ! [V1l1] : ( mem(V1l1,ty_2Elist_2Elist(A_27a)) => ! [V2l2] : ( mem(V2l2,ty_2Elist_2Elist(A_27a)) => ! [V3h] : ( mem(V3h,A_27a) => ( ap(ap(c_2Elist_2EAPPEND(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V3h),V1l1)),V2l2) = ap(ap(c_2Elist_2ECONS(A_27a),V3h),ap(ap(c_2Elist_2EAPPEND(A_27a),V1l1),V2l2)) ) ) ) ) ) ) )).
fof(ax_thm_2Elist_2EFLAT,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ap(c_2Elist_2EFLAT(A_27a),c_2Elist_2ENIL(ty_2Elist_2Elist(A_27a))) = c_2Elist_2ENIL(A_27a) ) & ! [V0h] : ( mem(V0h,ty_2Elist_2Elist(A_27a)) => ! [V1t] : ( mem(V1t,ty_2Elist_2Elist(ty_2Elist_2Elist(A_27a))) => ( ap(c_2Elist_2EFLAT(A_27a),ap(ap(c_2Elist_2ECONS(ty_2Elist_2Elist(A_27a)),V0h),V1t)) = ap(ap(c_2Elist_2EAPPEND(A_27a),V0h),ap(c_2Elist_2EFLAT(A_27a),V1t)) ) ) ) ) ) )).
fof(ax_thm_2Elist_2ELENGTH,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ap(c_2Elist_2ELENGTH(A_27a),c_2Elist_2ENIL(A_27a)) = c_2Enum_2E0 ) & ! [V0h] : ( mem(V0h,A_27a) => ! [V1t] : ( mem(V1t,ty_2Elist_2Elist(A_27a)) => ( ap(c_2Elist_2ELENGTH(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V0h),V1t)) = ap(c_2Enum_2ESUC,ap(c_2Elist_2ELENGTH(A_27a),V1t)) ) ) ) ) ) )).
fof(ax_thm_2Elist_2EMAP,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ( ( ! [V0f] : ( mem(V0f,arr(A_27a,A_27b)) => ( ap(ap(c_2Elist_2EMAP(A_27a,A_27b),V0f),c_2Elist_2ENIL(A_27a)) = c_2Elist_2ENIL(A_27b) ) ) ) & ! [V1f] : ( mem(V1f,arr(A_27a,A_27b)) => ! [V2h] : ( mem(V2h,A_27a) => ! [V3t] : ( mem(V3t,ty_2Elist_2Elist(A_27a)) => ( ap(ap(c_2Elist_2EMAP(A_27a,A_27b),V1f),ap(ap(c_2Elist_2ECONS(A_27a),V2h),V3t)) = ap(ap(c_2Elist_2ECONS(A_27b),ap(V1f,V2h)),ap(ap(c_2Elist_2EMAP(A_27a,A_27b),V1f),V3t)) ) ) ) ) ) ) ) )).
fof(ax_thm_2Elist_2ELIST__TO__SET__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0x] : ( mem(V0x,A_27a) => ( p(ap(ap(c_2Elist_2ELIST__TO__SET(A_27a),c_2Elist_2ENIL(A_27a)),V0x)) <=> $false ) ) ) & ! [V1h] : ( mem(V1h,A_27a) => ! [V2t] : ( mem(V2t,ty_2Elist_2Elist(A_27a)) => ! [V3x] : ( mem(V3x,A_27a) => ( p(ap(ap(c_2Elist_2ELIST__TO__SET(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V1h),V2t)),V3x)) <=> ( ( V3x = V1h ) | p(ap(ap(c_2Elist_2ELIST__TO__SET(A_27a),V2t),V3x)) ) ) ) ) ) ) ) )).
fof(conj_thm_2Elist_2ELIST__TO__SET,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0h] : ( mem(V0h,A_27b) => ! [V1t] : ( mem(V1t,ty_2Elist_2Elist(A_27b)) => ( ( ap(c_2Elist_2ELIST__TO__SET(A_27a),c_2Elist_2ENIL(A_27a)) = c_2Epred__set_2EEMPTY(A_27a) ) & ( ap(c_2Elist_2ELIST__TO__SET(A_27b),ap(ap(c_2Elist_2ECONS(A_27b),V0h),V1t)) = ap(ap(c_2Epred__set_2EINSERT(A_27b),V0h),ap(c_2Elist_2ELIST__TO__SET(A_27b),V1t)) ) ) ) ))))).
fof(ax_thm_2Elist_2EFILTER,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ( ap(ap(c_2Elist_2EFILTER(A_27a),V0P),c_2Elist_2ENIL(A_27a)) = c_2Elist_2ENIL(A_27a) ) ) ) & ! [V1P] : ( mem(V1P,arr(A_27a,bool)) => ! [V2h] : ( mem(V2h,A_27a) => ! [V3t] : ( mem(V3t,ty_2Elist_2Elist(A_27a)) => ( ap(ap(c_2Elist_2EFILTER(A_27a),V1P),ap(ap(c_2Elist_2ECONS(A_27a),V2h),V3t)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Elist_2Elist(A_27a)),ap(V1P,V2h)),ap(ap(c_2Elist_2ECONS(A_27a),V2h),ap(ap(c_2Elist_2EFILTER(A_27a),V1P),V3t))),ap(ap(c_2Elist_2EFILTER(A_27a),V1P),V3t)) ) ) ) ) ) ) )).
fof(ax_thm_2Elist_2EFOLDR,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_2Elist_2EFOLDR(A_27a,A_27b),V0f),V1e),c_2Elist_2ENIL(A_27a)) = V1e ) ) ) ) & ! [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_2Elist_2EFOLDR(A_27a,A_27b),V2f),V3e),ap(ap(c_2Elist_2ECONS(A_27a),V4x),V5l)) = ap(ap(V2f,V4x),ap(ap(ap(c_2Elist_2EFOLDR(A_27a,A_27b),V2f),V3e),V5l)) ) ) ) ) ) ) ) ) )).
fof(ax_thm_2Elist_2EFOLDL,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_2Elist_2EFOLDL(A_27a,A_27b),V0f),V1e),c_2Elist_2ENIL(A_27a)) = V1e ) ) ) ) & ! [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_2Elist_2EFOLDL(A_27a,A_27b),V2f),V3e),ap(ap(c_2Elist_2ECONS(A_27a),V4x),V5l)) = ap(ap(ap(c_2Elist_2EFOLDL(A_27a,A_27b),V2f),ap(ap(V2f,V3e),V4x)),V5l) ) ) ) ) ) ) ) ) )).
fof(ax_thm_2Elist_2EEVERY__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ( p(ap(ap(c_2Elist_2EEVERY(A_27a),V0P),c_2Elist_2ENIL(A_27a))) <=> $true ) ) ) & ! [V1P] : ( mem(V1P,arr(A_27a,bool)) => ! [V2h] : ( mem(V2h,A_27a) => ! [V3t] : ( mem(V3t,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Elist_2EEVERY(A_27a),V1P),ap(ap(c_2Elist_2ECONS(A_27a),V2h),V3t))) <=> ( p(ap(V1P,V2h)) & p(ap(ap(c_2Elist_2EEVERY(A_27a),V1P),V3t)) ) ) ) ) ) ) ) )).
fof(ax_thm_2Elist_2EEXISTS__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ( p(ap(ap(c_2Elist_2EEXISTS(A_27a),V0P),c_2Elist_2ENIL(A_27a))) <=> $false ) ) ) & ! [V1P] : ( mem(V1P,arr(A_27a,bool)) => ! [V2h] : ( mem(V2h,A_27a) => ! [V3t] : ( mem(V3t,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Elist_2EEXISTS(A_27a),V1P),ap(ap(c_2Elist_2ECONS(A_27a),V2h),V3t))) <=> ( p(ap(V1P,V2h)) | p(ap(ap(c_2Elist_2EEXISTS(A_27a),V1P),V3t)) ) ) ) ) ) ) ) )).
fof(ax_thm_2Elist_2EEL,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ap(ap(c_2Elist_2EEL(A_27a),c_2Enum_2E0),V0l) = ap(c_2Elist_2EHD(A_27a),V0l) ) ) ) & ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( ap(ap(c_2Elist_2EEL(A_27a),ap(c_2Enum_2ESUC,V2n)),V1l) = ap(ap(c_2Elist_2EEL(A_27a),V2n),ap(c_2Elist_2ETL(A_27a),V1l)) ) ) ) ) ) )).
fof(conj_thm_2Elist_2EMAP2__ind,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0P] : ( mem(V0P,arr(arr(A_27b,arr(A_27c,A_27a)),arr(ty_2Elist_2Elist(A_27b),arr(ty_2Elist_2Elist(A_27c),bool)))) => ( ( ( ! [V1f] : ( mem(V1f,arr(A_27b,arr(A_27c,A_27a))) => ! [V2h1] : ( mem(V2h1,A_27b) => ! [V3t1] : ( mem(V3t1,ty_2Elist_2Elist(A_27b)) => ! [V4h2] : ( mem(V4h2,A_27c) => ! [V5t2] : ( mem(V5t2,ty_2Elist_2Elist(A_27c)) => ( p(ap(ap(ap(V0P,V1f),V3t1),V5t2)) => p(ap(ap(ap(V0P,V1f),ap(ap(c_2Elist_2ECONS(A_27b),V2h1),V3t1)),ap(ap(c_2Elist_2ECONS(A_27c),V4h2),V5t2))) ) ) ) ) ) ) ) & ( ( ! [V6f] : ( mem(V6f,arr(A_27b,arr(A_27c,A_27a))) => ! [V7y] : ( mem(V7y,ty_2Elist_2Elist(A_27c)) => p(ap(ap(ap(V0P,V6f),c_2Elist_2ENIL(A_27b)),V7y)) ) ) ) & ! [V8f] : ( mem(V8f,arr(A_27b,arr(A_27c,A_27a))) => ! [V9v4] : ( mem(V9v4,A_27b) => ! [V10v5] : ( mem(V10v5,ty_2Elist_2Elist(A_27b)) => p(ap(ap(ap(V0P,V8f),ap(ap(c_2Elist_2ECONS(A_27b),V9v4),V10v5)),c_2Elist_2ENIL(A_27c))) ) ) ) ) ) => ! [V11v] : ( mem(V11v,arr(A_27b,arr(A_27c,A_27a))) => ! [V12v1] : ( mem(V12v1,ty_2Elist_2Elist(A_27b)) => ! [V13v2] : ( mem(V13v2,ty_2Elist_2Elist(A_27c)) => p(ap(ap(ap(V0P,V11v),V12v1),V13v2)) ) ) ) ) )))))).
fof(conj_thm_2Elist_2EMAP2__DEF,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ( ( ! [V0t2] : ( mem(V0t2,ty_2Elist_2Elist(A_27c)) => ! [V1t1] : ( mem(V1t1,ty_2Elist_2Elist(A_27b)) => ! [V2h2] : ( mem(V2h2,A_27c) => ! [V3h1] : ( mem(V3h1,A_27b) => ! [V4f] : ( mem(V4f,arr(A_27b,arr(A_27c,A_27a))) => ( ap(ap(ap(c_2Elist_2EMAP2(A_27a,A_27b,A_27c),V4f),ap(ap(c_2Elist_2ECONS(A_27b),V3h1),V1t1)),ap(ap(c_2Elist_2ECONS(A_27c),V2h2),V0t2)) = ap(ap(c_2Elist_2ECONS(A_27a),ap(ap(V4f,V3h1),V2h2)),ap(ap(ap(c_2Elist_2EMAP2(A_27a,A_27b,A_27c),V4f),V1t1),V0t2)) ) ) ) ) ) ) ) & ( ( ! [V5y] : ( mem(V5y,ty_2Elist_2Elist(A_27c)) => ! [V6f] : ( mem(V6f,arr(A_27b,arr(A_27c,A_27a))) => ( ap(ap(ap(c_2Elist_2EMAP2(A_27a,A_27b,A_27c),V6f),c_2Elist_2ENIL(A_27b)),V5y) = c_2Elist_2ENIL(A_27a) ) ) ) ) & ! [V7v5] : ( mem(V7v5,ty_2Elist_2Elist(A_27b)) => ! [V8v4] : ( mem(V8v4,A_27b) => ! [V9f] : ( mem(V9f,arr(A_27b,arr(A_27c,A_27a))) => ( ap(ap(ap(c_2Elist_2EMAP2(A_27a,A_27b,A_27c),V9f),ap(ap(c_2Elist_2ECONS(A_27b),V8v4),V7v5)),c_2Elist_2ENIL(A_27c)) = c_2Elist_2ENIL(A_27a) ) ) ) ) ) )))))).
fof(conj_thm_2Elist_2EMAP2,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) =>  ! [A_27d]: ( ne(A_27d) =>  ! [A_27e]: ( ne(A_27e) =>  ! [A_27f]: ( ne(A_27f) => ( ( ! [V0f] : ( mem(V0f,arr(A_27a,arr(A_27b,A_27c))) => ( ap(ap(ap(c_2Elist_2EMAP2(A_27c,A_27a,A_27b),V0f),c_2Elist_2ENIL(A_27a)),c_2Elist_2ENIL(A_27b)) = c_2Elist_2ENIL(A_27c) ) ) ) & ! [V1f] : ( mem(V1f,arr(A_27d,arr(A_27e,A_27f))) => ! [V2h1] : ( mem(V2h1,A_27d) => ! [V3t1] : ( mem(V3t1,ty_2Elist_2Elist(A_27d)) => ! [V4h2] : ( mem(V4h2,A_27e) => ! [V5t2] : ( mem(V5t2,ty_2Elist_2Elist(A_27e)) => ( ap(ap(ap(c_2Elist_2EMAP2(A_27f,A_27d,A_27e),V1f),ap(ap(c_2Elist_2ECONS(A_27d),V2h1),V3t1)),ap(ap(c_2Elist_2ECONS(A_27e),V4h2),V5t2)) = ap(ap(c_2Elist_2ECONS(A_27f),ap(ap(V1f,V2h1),V4h2)),ap(ap(ap(c_2Elist_2EMAP2(A_27f,A_27d,A_27e),V1f),V3t1),V5t2)) ) ) ) ) ) ) ))))))))).
fof(conj_thm_2Elist_2EMAP2__NIL,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0f] : ( mem(V0f,arr(A_27b,arr(A_27c,A_27a))) => ! [V1x] : ( mem(V1x,ty_2Elist_2Elist(A_27b)) => ( ap(ap(ap(c_2Elist_2EMAP2(A_27a,A_27b,A_27c),V0f),V1x),c_2Elist_2ENIL(A_27c)) = c_2Elist_2ENIL(A_27a) ) ) )))))).
fof(conj_thm_2Elist_2ELENGTH__MAP2,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_27c))) => ! [V1xs] : ( mem(V1xs,ty_2Elist_2Elist(A_27a)) => ! [V2ys] : ( mem(V2ys,ty_2Elist_2Elist(A_27b)) => ( ap(c_2Elist_2ELENGTH(A_27c),ap(ap(ap(c_2Elist_2EMAP2(A_27c,A_27a,A_27b),V0f),V1xs),V2ys)) = ap(ap(c_2Earithmetic_2EMIN,ap(c_2Elist_2ELENGTH(A_27a),V1xs)),ap(c_2Elist_2ELENGTH(A_27b),V2ys)) ) ) ) )))))).
fof(conj_thm_2Elist_2EEL__MAP2,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_27c))) => ! [V1ts] : ( mem(V1ts,ty_2Elist_2Elist(A_27a)) => ! [V2tt] : ( mem(V2tt,ty_2Elist_2Elist(A_27b)) => ! [V3n] : ( mem(V3n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V3n),ap(ap(c_2Earithmetic_2EMIN,ap(c_2Elist_2ELENGTH(A_27a),V1ts)),ap(c_2Elist_2ELENGTH(A_27b),V2tt)))) => ( ap(ap(c_2Elist_2EEL(A_27c),V3n),ap(ap(ap(c_2Elist_2EMAP2(A_27c,A_27a,A_27b),V0f),V1ts),V2tt)) = ap(ap(V0f,ap(ap(c_2Elist_2EEL(A_27a),V3n),V1ts)),ap(ap(c_2Elist_2EEL(A_27b),V3n),V2tt)) ) ) ) ) ) )))))).
fof(ax_thm_2Elist_2EINDEX__FIND__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0i] : ( mem(V0i,ty_2Enum_2Enum) => ! [V1P] : ( mem(V1P,arr(A_27a,bool)) => ( ap(ap(ap(c_2Elist_2EINDEX__FIND(A_27a),V0i),V1P),c_2Elist_2ENIL(A_27a)) = c_2Eoption_2ENONE(ty_2Epair_2Eprod(ty_2Enum_2Enum,A_27a)) ) ) ) ) & ! [V2i] : ( mem(V2i,ty_2Enum_2Enum) => ! [V3P] : ( mem(V3P,arr(A_27a,bool)) => ! [V4h] : ( mem(V4h,A_27a) => ! [V5t] : ( mem(V5t,ty_2Elist_2Elist(A_27a)) => ( ap(ap(ap(c_2Elist_2EINDEX__FIND(A_27a),V2i),V3P),ap(ap(c_2Elist_2ECONS(A_27a),V4h),V5t)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Enum_2Enum,A_27a))),ap(V3P,V4h)),ap(c_2Eoption_2ESOME(ty_2Epair_2Eprod(ty_2Enum_2Enum,A_27a)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),V2i),V4h))),ap(ap(ap(c_2Elist_2EINDEX__FIND(A_27a),ap(c_2Enum_2ESUC,V2i)),V3P),V5t)) ) ) ) ) ) ) ) )).
fof(ax_thm_2Elist_2EFIND__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ( ap(c_2Elist_2EFIND(A_27a),V0P) = ap(ap(c_2Ecombin_2Eo(ty_2Elist_2Elist(A_27a),ty_2Eoption_2Eoption(A_27a),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Enum_2Enum,A_27a))),ap(c_2Eoption_2EOPTION__MAP(ty_2Epair_2Eprod(ty_2Enum_2Enum,A_27a),A_27a),c_2Epair_2ESND(ty_2Enum_2Enum,A_27a))),ap(ap(c_2Elist_2EINDEX__FIND(A_27a),c_2Enum_2E0),V0P)) ) ) ) )).
fof(ax_thm_2Elist_2EINDEX__OF__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ( ap(c_2Elist_2EINDEX__OF(A_27a),V0x) = ap(ap(c_2Ecombin_2Eo(ty_2Elist_2Elist(A_27a),ty_2Eoption_2Eoption(ty_2Enum_2Enum),ty_2Eoption_2Eoption(ty_2Epair_2Eprod(ty_2Enum_2Enum,A_27a))),ap(c_2Eoption_2EOPTION__MAP(ty_2Epair_2Eprod(ty_2Enum_2Enum,A_27a),ty_2Enum_2Enum),c_2Epair_2EFST(ty_2Enum_2Enum,A_27a))),ap(ap(c_2Elist_2EINDEX__FIND(A_27a),c_2Enum_2E0),ap(c_2Emin_2E_3D(A_27a),V0x))) ) ) ) )).
fof(conj_thm_2Elist_2ENULL,lemma,( ! [A_27a]: ( ne(A_27a) => ( p(ap(c_2Elist_2ENULL(A_27a),c_2Elist_2ENIL(A_27a))) & ! [V0h] : ( mem(V0h,A_27a) => ! [V1t] : ( mem(V1t,ty_2Elist_2Elist(A_27a)) => ( ~~ p(ap(c_2Elist_2ENULL(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V0h),V1t))) ) ) ) )))).
fof(conj_thm_2Elist_2Elist__INDUCT0,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(ty_2Elist_2Elist(A_27a),bool)) => ( ( p(ap(V0P,c_2Elist_2ENIL(A_27a))) & ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ( p(ap(V0P,V1l)) => ! [V2a] : ( mem(V2a,A_27a) => p(ap(V0P,ap(ap(c_2Elist_2ECONS(A_27a),V2a),V1l))) ) ) ) ) => ! [V3l] : ( mem(V3l,ty_2Elist_2Elist(A_27a)) => p(ap(V0P,V3l)) ) ) )))).
fof(conj_thm_2Elist_2Elist__INDUCT,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(ty_2Elist_2Elist(A_27a),bool)) => ( ( p(ap(V0P,c_2Elist_2ENIL(A_27a))) & ! [V1t] : ( mem(V1t,ty_2Elist_2Elist(A_27a)) => ( p(ap(V0P,V1t)) => ! [V2h] : ( mem(V2h,A_27a) => p(ap(V0P,ap(ap(c_2Elist_2ECONS(A_27a),V2h),V1t))) ) ) ) ) => ! [V3l] : ( mem(V3l,ty_2Elist_2Elist(A_27a)) => p(ap(V0P,V3l)) ) ) )))).
fof(conj_thm_2Elist_2Elist__induction,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(ty_2Elist_2Elist(A_27a),bool)) => ( ( p(ap(V0P,c_2Elist_2ENIL(A_27a))) & ! [V1t] : ( mem(V1t,ty_2Elist_2Elist(A_27a)) => ( p(ap(V0P,V1t)) => ! [V2h] : ( mem(V2h,A_27a) => p(ap(V0P,ap(ap(c_2Elist_2ECONS(A_27a),V2h),V1t))) ) ) ) ) => ! [V3l] : ( mem(V3l,ty_2Elist_2Elist(A_27a)) => p(ap(V0P,V3l)) ) ) )))).
fof(conj_thm_2Elist_2Elist__CASES,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ( V0l = c_2Elist_2ENIL(A_27a) ) | ? [V1h] : ( mem(V1h,A_27a) & ? [V2t] : ( mem(V2t,ty_2Elist_2Elist(A_27a)) & ( V0l = ap(ap(c_2Elist_2ECONS(A_27a),V1h),V2t) ) ) ) ) )))).
fof(conj_thm_2Elist_2Elist__nchotomy,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ( V0l = c_2Elist_2ENIL(A_27a) ) | ? [V1h] : ( mem(V1h,A_27a) & ? [V2t] : ( mem(V2t,ty_2Elist_2Elist(A_27a)) & ( V0l = ap(ap(c_2Elist_2ECONS(A_27a),V1h),V2t) ) ) ) ) )))).
fof(conj_thm_2Elist_2Elist__case__compute,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0b] : ( mem(V0b,A_27b) => ! [V1f] : ( mem(V1f,arr(A_27a,arr(ty_2Elist_2Elist(A_27a),A_27b))) => ! [V2l] : ( mem(V2l,ty_2Elist_2Elist(A_27a)) => ( ap(ap(ap(c_2Elist_2Elist__CASE(A_27a,A_27b),V2l),V0b),V1f) = ap(ap(ap(c_2Ebool_2ECOND(A_27b),ap(c_2Elist_2ENULL(A_27a),V2l)),V0b),ap(ap(V1f,ap(c_2Elist_2EHD(A_27a),V2l)),ap(c_2Elist_2ETL(A_27a),V2l))) ) ) ) ))))).
fof(conj_thm_2Elist_2ECONS__11,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a0] : ( mem(V0a0,A_27a) => ! [V1a1] : ( mem(V1a1,ty_2Elist_2Elist(A_27a)) => ! [V2a0_27] : ( mem(V2a0_27,A_27a) => ! [V3a1_27] : ( mem(V3a1_27,ty_2Elist_2Elist(A_27a)) => ( ( ap(ap(c_2Elist_2ECONS(A_27a),V0a0),V1a1) = ap(ap(c_2Elist_2ECONS(A_27a),V2a0_27),V3a1_27) ) <=> ( ( V0a0 = V2a0_27 ) & ( V1a1 = V3a1_27 ) ) ) ) ) ) )))).
fof(conj_thm_2Elist_2ENOT__NIL__CONS,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a1] : ( mem(V0a1,ty_2Elist_2Elist(A_27a)) => ! [V1a0] : ( mem(V1a0,A_27a) => ( ~~ ( c_2Elist_2ENIL(A_27a) = ap(ap(c_2Elist_2ECONS(A_27a),V1a0),V0a1) ) ) ) )))).
fof(conj_thm_2Elist_2ENOT__CONS__NIL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a1] : ( mem(V0a1,ty_2Elist_2Elist(A_27a)) => ! [V1a0] : ( mem(V1a0,A_27a) => ( ~~ ( ap(ap(c_2Elist_2ECONS(A_27a),V1a0),V0a1) = c_2Elist_2ENIL(A_27a) ) ) ) )))).
fof(conj_thm_2Elist_2ELIST__NOT__EQ,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l1] : ( mem(V0l1,ty_2Elist_2Elist(A_27a)) => ! [V1l2] : ( mem(V1l2,ty_2Elist_2Elist(A_27a)) => ( ( ~~ ( V0l1 = V1l2 ) ) => ! [V2h1] : ( mem(V2h1,A_27a) => ! [V3h2] : ( mem(V3h2,A_27a) => ( ~~ ( ap(ap(c_2Elist_2ECONS(A_27a),V2h1),V0l1) = ap(ap(c_2Elist_2ECONS(A_27a),V3h2),V1l2) ) ) ) ) ) ) )))).
fof(conj_thm_2Elist_2ENOT__EQ__LIST,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0h1] : ( mem(V0h1,A_27a) => ! [V1h2] : ( mem(V1h2,A_27a) => ( ( ~~ ( V0h1 = V1h2 ) ) => ! [V2l1] : ( mem(V2l1,ty_2Elist_2Elist(A_27a)) => ! [V3l2] : ( mem(V3l2,ty_2Elist_2Elist(A_27a)) => ( ~~ ( ap(ap(c_2Elist_2ECONS(A_27a),V0h1),V2l1) = ap(ap(c_2Elist_2ECONS(A_27a),V1h2),V3l2) ) ) ) ) ) ) )))).
fof(conj_thm_2Elist_2EEQ__LIST,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0h1] : ( mem(V0h1,A_27a) => ! [V1h2] : ( mem(V1h2,A_27a) => ( ( V0h1 = V1h2 ) => ! [V2l1] : ( mem(V2l1,ty_2Elist_2Elist(A_27a)) => ! [V3l2] : ( mem(V3l2,ty_2Elist_2Elist(A_27a)) => ( ( V2l1 = V3l2 ) => ( ap(ap(c_2Elist_2ECONS(A_27a),V0h1),V2l1) = ap(ap(c_2Elist_2ECONS(A_27a),V1h2),V3l2) ) ) ) ) ) ) )))).
fof(conj_thm_2Elist_2ECONS,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ( ~~ p(ap(c_2Elist_2ENULL(A_27a),V0l)) ) => ( ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),V0l)),ap(c_2Elist_2ETL(A_27a),V0l)) = V0l ) ) )))).
fof(conj_thm_2Elist_2EAPPEND__NIL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ap(ap(c_2Elist_2EAPPEND(A_27a),V0l),c_2Elist_2ENIL(A_27a)) = V0l ) )))).
fof(conj_thm_2Elist_2EAPPEND__ASSOC,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l1] : ( mem(V0l1,ty_2Elist_2Elist(A_27a)) => ! [V1l2] : ( mem(V1l2,ty_2Elist_2Elist(A_27a)) => ! [V2l3] : ( mem(V2l3,ty_2Elist_2Elist(A_27a)) => ( ap(ap(c_2Elist_2EAPPEND(A_27a),V0l1),ap(ap(c_2Elist_2EAPPEND(A_27a),V1l2),V2l3)) = ap(ap(c_2Elist_2EAPPEND(A_27a),ap(ap(c_2Elist_2EAPPEND(A_27a),V0l1),V1l2)),V2l3) ) ) ) )))).
fof(conj_thm_2Elist_2ELENGTH__APPEND,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l1] : ( mem(V0l1,ty_2Elist_2Elist(A_27a)) => ! [V1l2] : ( mem(V1l2,ty_2Elist_2Elist(A_27a)) => ( ap(c_2Elist_2ELENGTH(A_27a),ap(ap(c_2Elist_2EAPPEND(A_27a),V0l1),V1l2)) = ap(ap(c_2Earithmetic_2E_2B,ap(c_2Elist_2ELENGTH(A_27a),V0l1)),ap(c_2Elist_2ELENGTH(A_27a),V1l2)) ) ) )))).
fof(conj_thm_2Elist_2EMAP__APPEND,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(A_27a,A_27b)) => ! [V1l1] : ( mem(V1l1,ty_2Elist_2Elist(A_27a)) => ! [V2l2] : ( mem(V2l2,ty_2Elist_2Elist(A_27a)) => ( ap(ap(c_2Elist_2EMAP(A_27a,A_27b),V0f),ap(ap(c_2Elist_2EAPPEND(A_27a),V1l1),V2l2)) = ap(ap(c_2Elist_2EAPPEND(A_27b),ap(ap(c_2Elist_2EMAP(A_27a,A_27b),V0f),V1l1)),ap(ap(c_2Elist_2EMAP(A_27a,A_27b),V0f),V2l2)) ) ) ) ))))).
fof(conj_thm_2Elist_2EMAP__ID,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ( ap(ap(c_2Elist_2EMAP(A_27a,A_27a),i(A_27a)),V0l) = V0l ) & ( ap(ap(c_2Elist_2EMAP(A_27a,A_27a),c_2Ecombin_2EI(A_27a)),V0l) = V0l ) ) )))).
fof(conj_thm_2Elist_2ELENGTH__MAP,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ! [V1f] : ( mem(V1f,arr(A_27a,A_27b)) => ( ap(c_2Elist_2ELENGTH(A_27b),ap(ap(c_2Elist_2EMAP(A_27a,A_27b),V1f),V0l)) = ap(c_2Elist_2ELENGTH(A_27a),V0l) ) ) ))))).
fof(conj_thm_2Elist_2EMAP__EQ__NIL,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ! [V1f] : ( mem(V1f,arr(A_27a,A_27b)) => ( ( ( ap(ap(c_2Elist_2EMAP(A_27a,A_27b),V1f),V0l) = c_2Elist_2ENIL(A_27b) ) <=> ( V0l = c_2Elist_2ENIL(A_27a) ) ) & ( ( c_2Elist_2ENIL(A_27b) = ap(ap(c_2Elist_2EMAP(A_27a,A_27b),V1f),V0l) ) <=> ( V0l = c_2Elist_2ENIL(A_27a) ) ) ) ) ))))).
fof(conj_thm_2Elist_2EMAP__EQ__CONS,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)) => ! [V2h] : ( mem(V2h,A_27b) => ! [V3t] : ( mem(V3t,ty_2Elist_2Elist(A_27b)) => ( ( ap(ap(c_2Elist_2EMAP(A_27a,A_27b),V0f),V1l) = ap(ap(c_2Elist_2ECONS(A_27b),V2h),V3t) ) <=> ? [V4x0] : ( mem(V4x0,A_27a) & ? [V5t0] : ( mem(V5t0,ty_2Elist_2Elist(A_27a)) & ( ( V1l = ap(ap(c_2Elist_2ECONS(A_27a),V4x0),V5t0) ) & ( ( V2h = ap(V0f,V4x0) ) & ( V3t = ap(ap(c_2Elist_2EMAP(A_27a,A_27b),V0f),V5t0) ) ) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Elist_2EMAP__EQ__SING,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)) => ! [V2x] : ( mem(V2x,A_27b) => ( ( ap(ap(c_2Elist_2EMAP(A_27a,A_27b),V0f),V1l) = ap(ap(c_2Elist_2ECONS(A_27b),V2x),c_2Elist_2ENIL(A_27b)) ) <=> ? [V3x0] : ( mem(V3x0,A_27a) & ( ( V1l = ap(ap(c_2Elist_2ECONS(A_27a),V3x0),c_2Elist_2ENIL(A_27a)) ) & ( V2x = ap(V0f,V3x0) ) ) ) ) ) ) ))))).
fof(conj_thm_2Elist_2EMAP__EQ__f,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f1] : ( mem(V0f1,arr(A_27a,A_27b)) => ! [V1f2] : ( mem(V1f2,arr(A_27a,A_27b)) => ! [V2l] : ( mem(V2l,ty_2Elist_2Elist(A_27a)) => ( ( ap(ap(c_2Elist_2EMAP(A_27a,A_27b),V0f1),V2l) = ap(ap(c_2Elist_2EMAP(A_27a,A_27b),V1f2),V2l) ) <=> ! [V3e] : ( mem(V3e,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V3e),ap(c_2Elist_2ELIST__TO__SET(A_27a),V2l))) => ( ap(V0f1,V3e) = ap(V1f2,V3e) ) ) ) ) ) ) ))))).
fof(conj_thm_2Elist_2EMAP__o,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0f] : ( mem(V0f,arr(A_27b,A_27c)) => ! [V1g] : ( mem(V1g,arr(A_27a,A_27b)) => ( ap(c_2Elist_2EMAP(A_27a,A_27c),ap(ap(c_2Ecombin_2Eo(A_27a,A_27c,A_27b),V0f),V1g)) = ap(ap(c_2Ecombin_2Eo(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27c),ty_2Elist_2Elist(A_27b)),ap(c_2Elist_2EMAP(A_27b,A_27c),V0f)),ap(c_2Elist_2EMAP(A_27a,A_27b),V1g)) ) ) )))))).
fof(conj_thm_2Elist_2EMAP__MAP__o,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0f] : ( mem(V0f,arr(A_27b,A_27c)) => ! [V1g] : ( mem(V1g,arr(A_27a,A_27b)) => ! [V2l] : ( mem(V2l,ty_2Elist_2Elist(A_27a)) => ( ap(ap(c_2Elist_2EMAP(A_27b,A_27c),V0f),ap(ap(c_2Elist_2EMAP(A_27a,A_27b),V1g),V2l)) = ap(ap(c_2Elist_2EMAP(A_27a,A_27c),ap(ap(c_2Ecombin_2Eo(A_27a,A_27c,A_27b),V0f),V1g)),V2l) ) ) ) )))))).
fof(conj_thm_2Elist_2EEL__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_2Eprim__rec_2E_3C,V0n),ap(c_2Elist_2ELENGTH(A_27a),V1l))) => ! [V2f] : ( mem(V2f,arr(A_27a,A_27b)) => ( ap(ap(c_2Elist_2EEL(A_27b),V0n),ap(ap(c_2Elist_2EMAP(A_27a,A_27b),V2f),V1l)) = ap(V2f,ap(ap(c_2Elist_2EEL(A_27a),V0n),V1l)) ) ) ) ) ))))).
fof(conj_thm_2Elist_2EEL__APPEND__EQN,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l1] : ( mem(V0l1,ty_2Elist_2Elist(A_27a)) => ! [V1l2] : ( mem(V1l2,ty_2Elist_2Elist(A_27a)) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( ap(ap(c_2Elist_2EEL(A_27a),V2n),ap(ap(c_2Elist_2EAPPEND(A_27a),V0l1),V1l2)) = ap(ap(ap(c_2Ebool_2ECOND(A_27a),ap(ap(c_2Eprim__rec_2E_3C,V2n),ap(c_2Elist_2ELENGTH(A_27a),V0l1))),ap(ap(c_2Elist_2EEL(A_27a),V2n),V0l1)),ap(ap(c_2Elist_2EEL(A_27a),ap(ap(c_2Earithmetic_2E_2D,V2n),ap(c_2Elist_2ELENGTH(A_27a),V0l1))),V1l2)) ) ) ) )))).
fof(conj_thm_2Elist_2EMAP__TL,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ! [V1f] : ( mem(V1f,arr(A_27a,A_27b)) => ( ( ~~ p(ap(c_2Elist_2ENULL(A_27a),V0l)) ) => ( ap(ap(c_2Elist_2EMAP(A_27a,A_27b),V1f),ap(c_2Elist_2ETL(A_27a),V0l)) = ap(c_2Elist_2ETL(A_27b),ap(ap(c_2Elist_2EMAP(A_27a,A_27b),V1f),V0l)) ) ) ) ))))).
fof(conj_thm_2Elist_2EEVERY__EL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ! [V1P] : ( mem(V1P,arr(A_27a,bool)) => ( p(ap(ap(c_2Elist_2EEVERY(A_27a),V1P),V0l)) <=> ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V2n),ap(c_2Elist_2ELENGTH(A_27a),V0l))) => p(ap(V1P,ap(ap(c_2Elist_2EEL(A_27a),V2n),V0l))) ) ) ) ) )))).
fof(conj_thm_2Elist_2EEVERY__CONJ,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_2EEVERY(A_27a),f390(A_27a,V0P,V1Q)),V2l)) <=> ( p(ap(ap(c_2Elist_2EEVERY(A_27a),V0P),V2l)) & p(ap(ap(c_2Elist_2EEVERY(A_27a),V1Q),V2l)) ) ) ) ) )))).
fof(conj_thm_2Elist_2EEVERY__MEM,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)) <=> ! [V2e] : ( mem(V2e,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V2e),ap(c_2Elist_2ELIST__TO__SET(A_27a),V1l))) => p(ap(V0P,V2e)) ) ) ) ) )))).
fof(conj_thm_2Elist_2EEVERY__MAP,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(A_27b,bool)) => ! [V1f] : ( mem(V1f,arr(A_27a,A_27b)) => ! [V2l] : ( mem(V2l,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Elist_2EEVERY(A_27b),V0P),ap(ap(c_2Elist_2EMAP(A_27a,A_27b),V1f),V2l))) <=> p(ap(ap(c_2Elist_2EEVERY(A_27a),f391(A_27a,A_27b,V1f,V0P)),V2l)) ) ) ) ))))).
fof(conj_thm_2Elist_2EEVERY__SIMP,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0c] : ( mem(V0c,bool) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Elist_2EEVERY(A_27a),k(A_27a,V0c)),V1l)) <=> ( ( V1l = c_2Elist_2ENIL(A_27a) ) | p(V0c) ) ) ) )))).
fof(conj_thm_2Elist_2EMONO__EVERY,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)) => ( ( ! [V3x] : ( mem(V3x,A_27a) => ( p(ap(V0P,V3x)) => p(ap(V1Q,V3x)) ) ) ) => ( p(ap(ap(c_2Elist_2EEVERY(A_27a),V0P),V2l)) => p(ap(ap(c_2Elist_2EEVERY(A_27a),V1Q),V2l)) ) ) ) ) )))).
fof(conj_thm_2Elist_2EEXISTS__MEM,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)) <=> ? [V2e] : ( mem(V2e,A_27a) & ( p(ap(ap(c_2Ebool_2EIN(A_27a),V2e),ap(c_2Elist_2ELIST__TO__SET(A_27a),V1l))) & p(ap(V0P,V2e)) ) ) ) ) )))).
fof(conj_thm_2Elist_2EEXISTS__MAP,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(A_27b,bool)) => ! [V1f] : ( mem(V1f,arr(A_27a,A_27b)) => ! [V2l] : ( mem(V2l,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Elist_2EEXISTS(A_27b),V0P),ap(ap(c_2Elist_2EMAP(A_27a,A_27b),V1f),V2l))) <=> p(ap(ap(c_2Elist_2EEXISTS(A_27a),f391(A_27a,A_27b,V1f,V0P)),V2l)) ) ) ) ))))).
fof(conj_thm_2Elist_2EEXISTS__SIMP,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0c] : ( mem(V0c,bool) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Elist_2EEXISTS(A_27a),k(A_27a,V0c)),V1l)) <=> ( ( ~~ ( V1l = c_2Elist_2ENIL(A_27a) ) ) & p(V0c) ) ) ) )))).
fof(conj_thm_2Elist_2EMONO__EXISTS,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)) => ( ( ! [V3x] : ( mem(V3x,A_27a) => ( p(ap(V0P,V3x)) => p(ap(V1Q,V3x)) ) ) ) => ( p(ap(ap(c_2Elist_2EEXISTS(A_27a),V0P),V2l)) => p(ap(ap(c_2Elist_2EEXISTS(A_27a),V1Q),V2l)) ) ) ) ) )))).
fof(conj_thm_2Elist_2EEVERY__NOT__EXISTS,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(c_2Elist_2EEXISTS(A_27a),f392(A_27a,V0P)),V1l)) ) ) ) )))).
fof(conj_thm_2Elist_2EEXISTS__NOT__EVERY,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(c_2Elist_2EEVERY(A_27a),f392(A_27a,V0P)),V1l)) ) ) ) )))).
fof(conj_thm_2Elist_2EMEM__APPEND,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0e] : ( mem(V0e,A_27a) => ! [V1l1] : ( mem(V1l1,ty_2Elist_2Elist(A_27a)) => ! [V2l2] : ( mem(V2l2,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V0e),ap(c_2Elist_2ELIST__TO__SET(A_27a),ap(ap(c_2Elist_2EAPPEND(A_27a),V1l1),V2l2)))) <=> ( p(ap(ap(c_2Ebool_2EIN(A_27a),V0e),ap(c_2Elist_2ELIST__TO__SET(A_27a),V1l1))) | p(ap(ap(c_2Ebool_2EIN(A_27a),V0e),ap(c_2Elist_2ELIST__TO__SET(A_27a),V2l2))) ) ) ) ) )))).
fof(conj_thm_2Elist_2EMEM__FILTER,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1L] : ( mem(V1L,ty_2Elist_2Elist(A_27a)) => ! [V2x] : ( mem(V2x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),ap(c_2Elist_2ELIST__TO__SET(A_27a),ap(ap(c_2Elist_2EFILTER(A_27a),V0P),V1L)))) <=> ( p(ap(V0P,V2x)) & p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),ap(c_2Elist_2ELIST__TO__SET(A_27a),V1L))) ) ) ) ) )))).
fof(conj_thm_2Elist_2EMEM__FLAT,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1L] : ( mem(V1L,ty_2Elist_2Elist(ty_2Elist_2Elist(A_27a))) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V0x),ap(c_2Elist_2ELIST__TO__SET(A_27a),ap(c_2Elist_2EFLAT(A_27a),V1L)))) <=> ? [V2l] : ( mem(V2l,ty_2Elist_2Elist(A_27a)) & ( p(ap(ap(c_2Ebool_2EIN(ty_2Elist_2Elist(A_27a)),V2l),ap(c_2Elist_2ELIST__TO__SET(ty_2Elist_2Elist(A_27a)),V1L))) & p(ap(ap(c_2Ebool_2EIN(A_27a),V0x),ap(c_2Elist_2ELIST__TO__SET(A_27a),V2l))) ) ) ) ) )))).
fof(conj_thm_2Elist_2EFLAT__APPEND,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l1] : ( mem(V0l1,ty_2Elist_2Elist(ty_2Elist_2Elist(A_27a))) => ! [V1l2] : ( mem(V1l2,ty_2Elist_2Elist(ty_2Elist_2Elist(A_27a))) => ( ap(c_2Elist_2EFLAT(A_27a),ap(ap(c_2Elist_2EAPPEND(ty_2Elist_2Elist(A_27a)),V0l1),V1l2)) = ap(ap(c_2Elist_2EAPPEND(A_27a),ap(c_2Elist_2EFLAT(A_27a),V0l1)),ap(c_2Elist_2EFLAT(A_27a),V1l2)) ) ) )))).
fof(conj_thm_2Elist_2EFLAT__compute,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0t] : ( mem(V0t,ty_2Elist_2Elist(ty_2Elist_2Elist(A_27b))) => ! [V1h] : ( mem(V1h,A_27c) => ! [V2t1] : ( mem(V2t1,ty_2Elist_2Elist(A_27c)) => ! [V3t2] : ( mem(V3t2,ty_2Elist_2Elist(ty_2Elist_2Elist(A_27c))) => ( ( ap(c_2Elist_2EFLAT(A_27a),c_2Elist_2ENIL(ty_2Elist_2Elist(A_27a))) = c_2Elist_2ENIL(A_27a) ) & ( ( ap(c_2Elist_2EFLAT(A_27b),ap(ap(c_2Elist_2ECONS(ty_2Elist_2Elist(A_27b)),c_2Elist_2ENIL(A_27b)),V0t)) = ap(c_2Elist_2EFLAT(A_27b),V0t) ) & ( ap(c_2Elist_2EFLAT(A_27c),ap(ap(c_2Elist_2ECONS(ty_2Elist_2Elist(A_27c)),ap(ap(c_2Elist_2ECONS(A_27c),V1h),V2t1)),V3t2)) = ap(ap(c_2Elist_2ECONS(A_27c),V1h),ap(c_2Elist_2EFLAT(A_27c),ap(ap(c_2Elist_2ECONS(ty_2Elist_2Elist(A_27c)),V2t1),V3t2))) ) ) ) ) ) ) )))))).
fof(conj_thm_2Elist_2EEVERY__APPEND,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1l1] : ( mem(V1l1,ty_2Elist_2Elist(A_27a)) => ! [V2l2] : ( mem(V2l2,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Elist_2EEVERY(A_27a),V0P),ap(ap(c_2Elist_2EAPPEND(A_27a),V1l1),V2l2))) <=> ( p(ap(ap(c_2Elist_2EEVERY(A_27a),V0P),V1l1)) & p(ap(ap(c_2Elist_2EEVERY(A_27a),V0P),V2l2)) ) ) ) ) )))).
fof(conj_thm_2Elist_2EEXISTS__APPEND,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1l1] : ( mem(V1l1,ty_2Elist_2Elist(A_27a)) => ! [V2l2] : ( mem(V2l2,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Elist_2EEXISTS(A_27a),V0P),ap(ap(c_2Elist_2EAPPEND(A_27a),V1l1),V2l2))) <=> ( p(ap(ap(c_2Elist_2EEXISTS(A_27a),V0P),V1l1)) | p(ap(ap(c_2Elist_2EEXISTS(A_27a),V0P),V2l2)) ) ) ) ) )))).
fof(conj_thm_2Elist_2ENOT__EVERY,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(c_2Elist_2EEXISTS(A_27a),ap(ap(c_2Ecombin_2Eo(A_27a,bool,bool),c_2Ebool_2E_7E),V0P)),V1l)) ) ) )))).
fof(conj_thm_2Elist_2ENOT__EXISTS,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(c_2Elist_2EEVERY(A_27a),ap(ap(c_2Ecombin_2Eo(A_27a,bool,bool),c_2Ebool_2E_7E),V0P)),V1l)) ) ) )))).
fof(conj_thm_2Elist_2EMEM__MAP,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ! [V1f] : ( mem(V1f,arr(A_27a,A_27b)) => ! [V2x] : ( mem(V2x,A_27b) => ( p(ap(ap(c_2Ebool_2EIN(A_27b),V2x),ap(c_2Elist_2ELIST__TO__SET(A_27b),ap(ap(c_2Elist_2EMAP(A_27a,A_27b),V1f),V0l)))) <=> ? [V3y] : ( mem(V3y,A_27a) & ( ( V2x = ap(V1f,V3y) ) & p(ap(ap(c_2Ebool_2EIN(A_27a),V3y),ap(c_2Elist_2ELIST__TO__SET(A_27a),V0l))) ) ) ) ) ) ))))).
fof(conj_thm_2Elist_2ELENGTH__NIL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ( ap(c_2Elist_2ELENGTH(A_27a),V0l) = c_2Enum_2E0 ) <=> ( V0l = c_2Elist_2ENIL(A_27a) ) ) )))).
fof(conj_thm_2Elist_2ELENGTH__NIL__SYM,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ( c_2Enum_2E0 = ap(c_2Elist_2ELENGTH(A_27a),V0l) ) <=> ( V0l = c_2Elist_2ENIL(A_27a) ) ) )))).
fof(conj_thm_2Elist_2ENULL__EQ,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ( p(ap(c_2Elist_2ENULL(A_27a),V0l)) <=> ( V0l = c_2Elist_2ENIL(A_27a) ) ) )))).
fof(conj_thm_2Elist_2ENULL__LENGTH,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ( p(ap(c_2Elist_2ENULL(A_27a),V0l)) <=> ( ap(c_2Elist_2ELENGTH(A_27a),V0l) = c_2Enum_2E0 ) ) )))).
fof(conj_thm_2Elist_2ELENGTH__CONS,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ( ap(c_2Elist_2ELENGTH(A_27a),V0l) = ap(c_2Enum_2ESUC,V1n) ) <=> ? [V2h] : ( mem(V2h,A_27a) & ? [V3l_27] : ( mem(V3l_27,ty_2Elist_2Elist(A_27a)) & ( ( ap(c_2Elist_2ELENGTH(A_27a),V3l_27) = V1n ) & ( V0l = ap(ap(c_2Elist_2ECONS(A_27a),V2h),V3l_27) ) ) ) ) ) ) )))).
fof(conj_thm_2Elist_2ELENGTH__EQ__CONS,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(ty_2Elist_2Elist(A_27a),bool)) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ( ! [V2l] : ( mem(V2l,ty_2Elist_2Elist(A_27a)) => ( ( ap(c_2Elist_2ELENGTH(A_27a),V2l) = ap(c_2Enum_2ESUC,V1n) ) => p(ap(V0P,V2l)) ) ) ) <=> ! [V3l] : ( mem(V3l,ty_2Elist_2Elist(A_27a)) => ( ( ap(c_2Elist_2ELENGTH(A_27a),V3l) = V1n ) => p(ap(f394(A_27a,V0P),V3l)) ) ) ) ) )))).
fof(conj_thm_2Elist_2ELENGTH__EQ__SUM,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ! [V1n1] : ( mem(V1n1,ty_2Enum_2Enum) => ! [V2n2] : ( mem(V2n2,ty_2Enum_2Enum) => ( ( ap(c_2Elist_2ELENGTH(A_27a),V0l) = ap(ap(c_2Earithmetic_2E_2B,V1n1),V2n2) ) <=> ? [V3l1] : ( mem(V3l1,ty_2Elist_2Elist(A_27a)) & ? [V4l2] : ( mem(V4l2,ty_2Elist_2Elist(A_27a)) & ( ( ap(c_2Elist_2ELENGTH(A_27a),V3l1) = V1n1 ) & ( ( ap(c_2Elist_2ELENGTH(A_27a),V4l2) = V2n2 ) & ( V0l = ap(ap(c_2Elist_2EAPPEND(A_27a),V3l1),V4l2) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Elist_2ELENGTH__EQ__NUM,lemma,( ! [A_27a]: ( ne(A_27a) => ( ( ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ( ap(c_2Elist_2ELENGTH(A_27a),V0l) = c_2Enum_2E0 ) <=> ( V0l = c_2Elist_2ENIL(A_27a) ) ) ) ) & ( ( ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( ( ap(c_2Elist_2ELENGTH(A_27a),V1l) = ap(c_2Enum_2ESUC,V2n) ) <=> ? [V3h] : ( mem(V3h,A_27a) & ? [V4l_27] : ( mem(V4l_27,ty_2Elist_2Elist(A_27a)) & ( ( ap(c_2Elist_2ELENGTH(A_27a),V4l_27) = V2n ) & ( V1l = ap(ap(c_2Elist_2ECONS(A_27a),V3h),V4l_27) ) ) ) ) ) ) ) ) & ! [V5l] : ( mem(V5l,ty_2Elist_2Elist(A_27a)) => ! [V6n1] : ( mem(V6n1,ty_2Enum_2Enum) => ! [V7n2] : ( mem(V7n2,ty_2Enum_2Enum) => ( ( ap(c_2Elist_2ELENGTH(A_27a),V5l) = ap(ap(c_2Earithmetic_2E_2B,V6n1),V7n2) ) <=> ? [V8l1] : ( mem(V8l1,ty_2Elist_2Elist(A_27a)) & ? [V9l2] : ( mem(V9l2,ty_2Elist_2Elist(A_27a)) & ( ( ap(c_2Elist_2ELENGTH(A_27a),V8l1) = V6n1 ) & ( ( ap(c_2Elist_2ELENGTH(A_27a),V9l2) = V7n2 ) & ( V5l = ap(ap(c_2Elist_2EAPPEND(A_27a),V8l1),V9l2) ) ) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Elist_2ELENGTH__EQ__NUM__compute,lemma,( ! [A_27a]: ( ne(A_27a) => ( ( ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ( ap(c_2Elist_2ELENGTH(A_27a),V0l) = c_2Enum_2E0 ) <=> ( V0l = c_2Elist_2ENIL(A_27a) ) ) ) ) & ( ( ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( ( ap(c_2Elist_2ELENGTH(A_27a),V1l) = ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V2n)) ) <=> ? [V3h] : ( mem(V3h,A_27a) & ? [V4l_27] : ( mem(V4l_27,ty_2Elist_2Elist(A_27a)) & ( ( ap(c_2Elist_2ELENGTH(A_27a),V4l_27) = ap(ap(c_2Earithmetic_2E_2D,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V2n))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) & ( V1l = ap(ap(c_2Elist_2ECONS(A_27a),V3h),V4l_27) ) ) ) ) ) ) ) ) & ( ( ! [V5l] : ( mem(V5l,ty_2Elist_2Elist(A_27a)) => ! [V6n] : ( mem(V6n,ty_2Enum_2Enum) => ( ( ap(c_2Elist_2ELENGTH(A_27a),V5l) = ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,V6n)) ) <=> ? [V7h] : ( mem(V7h,A_27a) & ? [V8l_27] : ( mem(V8l_27,ty_2Elist_2Elist(A_27a)) & ( ( ap(c_2Elist_2ELENGTH(A_27a),V8l_27) = ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V6n)) ) & ( V5l = ap(ap(c_2Elist_2ECONS(A_27a),V7h),V8l_27) ) ) ) ) ) ) ) ) & ! [V9l] : ( mem(V9l,ty_2Elist_2Elist(A_27a)) => ! [V10n1] : ( mem(V10n1,ty_2Enum_2Enum) => ! [V11n2] : ( mem(V11n2,ty_2Enum_2Enum) => ( ( ap(c_2Elist_2ELENGTH(A_27a),V9l) = ap(ap(c_2Earithmetic_2E_2B,V10n1),V11n2) ) <=> ? [V12l1] : ( mem(V12l1,ty_2Elist_2Elist(A_27a)) & ? [V13l2] : ( mem(V13l2,ty_2Elist_2Elist(A_27a)) & ( ( ap(c_2Elist_2ELENGTH(A_27a),V12l1) = V10n1 ) & ( ( ap(c_2Elist_2ELENGTH(A_27a),V13l2) = V11n2 ) & ( V9l = ap(ap(c_2Elist_2EAPPEND(A_27a),V12l1),V13l2) ) ) ) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Elist_2ELENGTH__EQ__NIL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(ty_2Elist_2Elist(A_27a),bool)) => ( ( ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ( ( ap(c_2Elist_2ELENGTH(A_27a),V1l) = c_2Enum_2E0 ) => p(ap(V0P,V1l)) ) ) ) <=> p(ap(V0P,c_2Elist_2ENIL(A_27a))) ) )))).
fof(conj_thm_2Elist_2ECONS__ACYCLIC,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ! [V1x] : ( mem(V1x,A_27a) => ( ( ~~ ( V0l = ap(ap(c_2Elist_2ECONS(A_27a),V1x),V0l) ) ) & ( ~~ ( ap(ap(c_2Elist_2ECONS(A_27a),V1x),V0l) = V0l ) ) ) ) )))).
fof(conj_thm_2Elist_2EAPPEND__eq__NIL,lemma,( ! [A_27a]: ( ne(A_27a) => ( ( ! [V0l1] : ( mem(V0l1,ty_2Elist_2Elist(A_27a)) => ! [V1l2] : ( mem(V1l2,ty_2Elist_2Elist(A_27a)) => ( ( c_2Elist_2ENIL(A_27a) = ap(ap(c_2Elist_2EAPPEND(A_27a),V0l1),V1l2) ) <=> ( ( V0l1 = c_2Elist_2ENIL(A_27a) ) & ( V1l2 = c_2Elist_2ENIL(A_27a) ) ) ) ) ) ) & ! [V2l1] : ( mem(V2l1,ty_2Elist_2Elist(A_27a)) => ! [V3l2] : ( mem(V3l2,ty_2Elist_2Elist(A_27a)) => ( ( ap(ap(c_2Elist_2EAPPEND(A_27a),V2l1),V3l2) = c_2Elist_2ENIL(A_27a) ) <=> ( ( V2l1 = c_2Elist_2ENIL(A_27a) ) & ( V3l2 = c_2Elist_2ENIL(A_27a) ) ) ) ) ) )))).
fof(conj_thm_2Elist_2EMAP__EQ__APPEND,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)) => ! [V2l1] : ( mem(V2l1,ty_2Elist_2Elist(A_27b)) => ! [V3l2] : ( mem(V3l2,ty_2Elist_2Elist(A_27b)) => ( ( ap(ap(c_2Elist_2EMAP(A_27a,A_27b),V0f),V1l) = ap(ap(c_2Elist_2EAPPEND(A_27b),V2l1),V3l2) ) <=> ? [V4l10] : ( mem(V4l10,ty_2Elist_2Elist(A_27a)) & ? [V5l20] : ( mem(V5l20,ty_2Elist_2Elist(A_27a)) & ( ( V1l = ap(ap(c_2Elist_2EAPPEND(A_27a),V4l10),V5l20) ) & ( ( V2l1 = ap(ap(c_2Elist_2EMAP(A_27a,A_27b),V0f),V4l10) ) & ( V3l2 = ap(ap(c_2Elist_2EMAP(A_27a,A_27b),V0f),V5l20) ) ) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Elist_2EAPPEND__EQ__SING,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l1] : ( mem(V0l1,ty_2Elist_2Elist(A_27a)) => ! [V1l2] : ( mem(V1l2,ty_2Elist_2Elist(A_27a)) => ! [V2e] : ( mem(V2e,A_27a) => ( ( ap(ap(c_2Elist_2EAPPEND(A_27a),V0l1),V1l2) = ap(ap(c_2Elist_2ECONS(A_27a),V2e),c_2Elist_2ENIL(A_27a)) ) <=> ( ( ( V0l1 = ap(ap(c_2Elist_2ECONS(A_27a),V2e),c_2Elist_2ENIL(A_27a)) ) & ( V1l2 = c_2Elist_2ENIL(A_27a) ) ) | ( ( V0l1 = c_2Elist_2ENIL(A_27a) ) & ( V1l2 = ap(ap(c_2Elist_2ECONS(A_27a),V2e),c_2Elist_2ENIL(A_27a)) ) ) ) ) ) ) )))).
fof(conj_thm_2Elist_2EAPPEND__11,lemma,( ! [A_27a]: ( ne(A_27a) => ( ( ! [V0l1] : ( mem(V0l1,ty_2Elist_2Elist(A_27a)) => ! [V1l2] : ( mem(V1l2,ty_2Elist_2Elist(A_27a)) => ! [V2l3] : ( mem(V2l3,ty_2Elist_2Elist(A_27a)) => ( ( ap(ap(c_2Elist_2EAPPEND(A_27a),V0l1),V1l2) = ap(ap(c_2Elist_2EAPPEND(A_27a),V0l1),V2l3) ) <=> ( V1l2 = V2l3 ) ) ) ) ) ) & ! [V3l1] : ( mem(V3l1,ty_2Elist_2Elist(A_27a)) => ! [V4l2] : ( mem(V4l2,ty_2Elist_2Elist(A_27a)) => ! [V5l3] : ( mem(V5l3,ty_2Elist_2Elist(A_27a)) => ( ( ap(ap(c_2Elist_2EAPPEND(A_27a),V4l2),V3l1) = ap(ap(c_2Elist_2EAPPEND(A_27a),V5l3),V3l1) ) <=> ( V4l2 = V5l3 ) ) ) ) ) )))).
fof(conj_thm_2Elist_2EAPPEND__LENGTH__EQ,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l1] : ( mem(V0l1,ty_2Elist_2Elist(A_27a)) => ! [V1l1_27] : ( mem(V1l1_27,ty_2Elist_2Elist(A_27a)) => ( ( ap(c_2Elist_2ELENGTH(A_27a),V0l1) = ap(c_2Elist_2ELENGTH(A_27a),V1l1_27) ) => ! [V2l2] : ( mem(V2l2,ty_2Elist_2Elist(A_27a)) => ! [V3l2_27] : ( mem(V3l2_27,ty_2Elist_2Elist(A_27a)) => ( ( ap(c_2Elist_2ELENGTH(A_27a),V2l2) = ap(c_2Elist_2ELENGTH(A_27a),V3l2_27) ) => ( ( ap(ap(c_2Elist_2EAPPEND(A_27a),V0l1),V2l2) = ap(ap(c_2Elist_2EAPPEND(A_27a),V1l1_27),V3l2_27) ) <=> ( ( V0l1 = V1l1_27 ) & ( V2l2 = V3l2_27 ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Elist_2EAPPEND__11__LENGTH,lemma,( ! [A_27a]: ( ne(A_27a) => ( ( ! [V0l1] : ( mem(V0l1,ty_2Elist_2Elist(A_27a)) => ! [V1l2] : ( mem(V1l2,ty_2Elist_2Elist(A_27a)) => ! [V2l1_27] : ( mem(V2l1_27,ty_2Elist_2Elist(A_27a)) => ! [V3l2_27] : ( mem(V3l2_27,ty_2Elist_2Elist(A_27a)) => ( ( ap(c_2Elist_2ELENGTH(A_27a),V0l1) = ap(c_2Elist_2ELENGTH(A_27a),V2l1_27) ) => ( ( ap(ap(c_2Elist_2EAPPEND(A_27a),V0l1),V1l2) = ap(ap(c_2Elist_2EAPPEND(A_27a),V2l1_27),V3l2_27) ) <=> ( ( V0l1 = V2l1_27 ) & ( V1l2 = V3l2_27 ) ) ) ) ) ) ) ) ) & ! [V4l1] : ( mem(V4l1,ty_2Elist_2Elist(A_27a)) => ! [V5l2] : ( mem(V5l2,ty_2Elist_2Elist(A_27a)) => ! [V6l1_27] : ( mem(V6l1_27,ty_2Elist_2Elist(A_27a)) => ! [V7l2_27] : ( mem(V7l2_27,ty_2Elist_2Elist(A_27a)) => ( ( ap(c_2Elist_2ELENGTH(A_27a),V5l2) = ap(c_2Elist_2ELENGTH(A_27a),V7l2_27) ) => ( ( ap(ap(c_2Elist_2EAPPEND(A_27a),V4l1),V5l2) = ap(ap(c_2Elist_2EAPPEND(A_27a),V6l1_27),V7l2_27) ) <=> ( ( V4l1 = V6l1_27 ) & ( V5l2 = V7l2_27 ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Elist_2EAPPEND__EQ__SELF,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) = V0l1 ) <=> ( V1l2 = c_2Elist_2ENIL(A_27a) ) ) ) ) ) & ( ( ! [V2l1] : ( mem(V2l1,ty_2Elist_2Elist(A_27a)) => ! [V3l2] : ( mem(V3l2,ty_2Elist_2Elist(A_27a)) => ( ( ap(ap(c_2Elist_2EAPPEND(A_27a),V2l1),V3l2) = V3l2 ) <=> ( V2l1 = c_2Elist_2ENIL(A_27a) ) ) ) ) ) & ( ( ! [V4l1] : ( mem(V4l1,ty_2Elist_2Elist(A_27a)) => ! [V5l2] : ( mem(V5l2,ty_2Elist_2Elist(A_27a)) => ( ( V4l1 = ap(ap(c_2Elist_2EAPPEND(A_27a),V4l1),V5l2) ) <=> ( V5l2 = c_2Elist_2ENIL(A_27a) ) ) ) ) ) & ! [V6l1] : ( mem(V6l1,ty_2Elist_2Elist(A_27a)) => ! [V7l2] : ( mem(V7l2,ty_2Elist_2Elist(A_27a)) => ( ( V7l2 = ap(ap(c_2Elist_2EAPPEND(A_27a),V6l1),V7l2) ) <=> ( V6l1 = c_2Elist_2ENIL(A_27a) ) ) ) ) ) ) )))).
fof(conj_thm_2Elist_2EMEM__SPLIT,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))) <=> ? [V2l1] : ( mem(V2l1,ty_2Elist_2Elist(A_27a)) & ? [V3l2] : ( mem(V3l2,ty_2Elist_2Elist(A_27a)) & ( V1l = ap(ap(c_2Elist_2EAPPEND(A_27a),V2l1),ap(ap(c_2Elist_2ECONS(A_27a),V0x),V3l2)) ) ) ) ) ) )))).
fof(conj_thm_2Elist_2ELIST__EQ__REWRITE,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l1] : ( mem(V0l1,ty_2Elist_2Elist(A_27a)) => ! [V1l2] : ( mem(V1l2,ty_2Elist_2Elist(A_27a)) => ( ( V0l1 = V1l2 ) <=> ( ( ap(c_2Elist_2ELENGTH(A_27a),V0l1) = ap(c_2Elist_2ELENGTH(A_27a),V1l2) ) & ! [V2x] : ( mem(V2x,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V2x),ap(c_2Elist_2ELENGTH(A_27a),V0l1))) => ( ap(ap(c_2Elist_2EEL(A_27a),V2x),V0l1) = ap(ap(c_2Elist_2EEL(A_27a),V2x),V1l2) ) ) ) ) ) ) )))).
fof(conj_thm_2Elist_2ELIST__EQ,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l1] : ( mem(V0l1,ty_2Elist_2Elist(A_27a)) => ! [V1l2] : ( mem(V1l2,ty_2Elist_2Elist(A_27a)) => ( ( ( ap(c_2Elist_2ELENGTH(A_27a),V0l1) = ap(c_2Elist_2ELENGTH(A_27a),V1l2) ) & ! [V2x] : ( mem(V2x,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V2x),ap(c_2Elist_2ELENGTH(A_27a),V0l1))) => ( ap(ap(c_2Elist_2EEL(A_27a),V2x),V0l1) = ap(ap(c_2Elist_2EEL(A_27a),V2x),V1l2) ) ) ) ) => ( V0l1 = V1l2 ) ) ) )))).
fof(conj_thm_2Elist_2EFOLDL__EQ__FOLDR,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0f] : ( mem(V0f,arr(A_27a,arr(A_27a,A_27a))) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ! [V2e] : ( mem(V2e,A_27a) => ( ( p(ap(c_2Ecombin_2EASSOC(A_27a),V0f)) & p(ap(c_2Ecombin_2ECOMM(A_27a,A_27a),V0f)) ) => ( ap(ap(ap(c_2Elist_2EFOLDL(A_27a,A_27a),V0f),V2e),V1l) = ap(ap(ap(c_2Elist_2EFOLDR(A_27a,A_27a),V0f),V2e),V1l) ) ) ) ) )))).
fof(conj_thm_2Elist_2EFOLDR__CONS,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(A_27a,A_27b)) => ! [V1ls] : ( mem(V1ls,ty_2Elist_2Elist(A_27a)) => ! [V2a] : ( mem(V2a,ty_2Elist_2Elist(A_27b)) => ( ap(ap(ap(c_2Elist_2EFOLDR(A_27a,ty_2Elist_2Elist(A_27b)),f396(A_27a,A_27b,V0f)),V2a),V1ls) = ap(ap(c_2Elist_2EAPPEND(A_27b),ap(ap(c_2Elist_2EMAP(A_27a,A_27b),V0f),V1ls)),V2a) ) ) ) ))))).
fof(conj_thm_2Elist_2ELENGTH__TL,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))) => ( ap(c_2Elist_2ELENGTH(A_27a),ap(c_2Elist_2ETL(A_27a),V0l)) = ap(ap(c_2Earithmetic_2E_2D,ap(c_2Elist_2ELENGTH(A_27a),V0l)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))) ) ) )))).
fof(conj_thm_2Elist_2EFILTER__EQ__NIL,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) = c_2Elist_2ENIL(A_27a) ) <=> p(ap(ap(c_2Elist_2EEVERY(A_27a),f392(A_27a,V0P)),V1l)) ) ) )))).
fof(conj_thm_2Elist_2EFILTER__NEQ__NIL,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) = c_2Elist_2ENIL(A_27a) ) ) <=> ? [V2x] : ( mem(V2x,A_27a) & ( p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),ap(c_2Elist_2ELIST__TO__SET(A_27a),V1l))) & p(ap(V0P,V2x)) ) ) ) ) )))).
fof(conj_thm_2Elist_2EFILTER__EQ__ID,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) = V1l ) <=> p(ap(ap(c_2Elist_2EEVERY(A_27a),V0P),V1l)) ) ) )))).
fof(conj_thm_2Elist_2EFILTER__NEQ__ID,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) = V1l ) ) <=> ? [V2x] : ( mem(V2x,A_27a) & ( p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),ap(c_2Elist_2ELIST__TO__SET(A_27a),V1l))) & ( ~~ p(ap(V0P,V2x)) ) ) ) ) ) )))).
fof(conj_thm_2Elist_2EFILTER__EQ__CONS,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ! [V2h] : ( mem(V2h,A_27a) => ! [V3lr] : ( mem(V3lr,ty_2Elist_2Elist(A_27a)) => ( ( ap(ap(c_2Elist_2EFILTER(A_27a),V0P),V1l) = ap(ap(c_2Elist_2ECONS(A_27a),V2h),V3lr) ) <=> ? [V4l1] : ( mem(V4l1,ty_2Elist_2Elist(A_27a)) & ? [V5l2] : ( mem(V5l2,ty_2Elist_2Elist(A_27a)) & ( ( V1l = ap(ap(c_2Elist_2EAPPEND(A_27a),ap(ap(c_2Elist_2EAPPEND(A_27a),V4l1),ap(ap(c_2Elist_2ECONS(A_27a),V2h),c_2Elist_2ENIL(A_27a)))),V5l2) ) & ( ( ap(ap(c_2Elist_2EFILTER(A_27a),V0P),V4l1) = c_2Elist_2ENIL(A_27a) ) & ( ( ap(ap(c_2Elist_2EFILTER(A_27a),V0P),V5l2) = V3lr ) & p(ap(V0P,V2h)) ) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Elist_2EFILTER__APPEND__DISTRIB,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1L] : ( mem(V1L,ty_2Elist_2Elist(A_27a)) => ! [V2M] : ( mem(V2M,ty_2Elist_2Elist(A_27a)) => ( ap(ap(c_2Elist_2EFILTER(A_27a),V0P),ap(ap(c_2Elist_2EAPPEND(A_27a),V1L),V2M)) = ap(ap(c_2Elist_2EAPPEND(A_27a),ap(ap(c_2Elist_2EFILTER(A_27a),V0P),V1L)),ap(ap(c_2Elist_2EFILTER(A_27a),V0P),V2M)) ) ) ) )))).
fof(conj_thm_2Elist_2EMEM,lemma,( ! [A_27a]: ( ne(A_27a) => ( ( ! [V0x] : ( mem(V0x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V0x),ap(c_2Elist_2ELIST__TO__SET(A_27a),c_2Elist_2ENIL(A_27a)))) <=> $false ) ) ) & ! [V1x] : ( mem(V1x,A_27a) => ! [V2h] : ( mem(V2h,A_27a) => ! [V3t] : ( mem(V3t,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V1x),ap(c_2Elist_2ELIST__TO__SET(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V2h),V3t)))) <=> ( ( V1x = V2h ) | p(ap(ap(c_2Ebool_2EIN(A_27a),V1x),ap(c_2Elist_2ELIST__TO__SET(A_27a),V3t))) ) ) ) ) ) )))).
fof(conj_thm_2Elist_2EFILTER__EQ__APPEND,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ! [V2l1] : ( mem(V2l1,ty_2Elist_2Elist(A_27a)) => ! [V3l2] : ( mem(V3l2,ty_2Elist_2Elist(A_27a)) => ( ( ap(ap(c_2Elist_2EFILTER(A_27a),V0P),V1l) = ap(ap(c_2Elist_2EAPPEND(A_27a),V2l1),V3l2) ) <=> ? [V4l3] : ( mem(V4l3,ty_2Elist_2Elist(A_27a)) & ? [V5l4] : ( mem(V5l4,ty_2Elist_2Elist(A_27a)) & ( ( V1l = ap(ap(c_2Elist_2EAPPEND(A_27a),V4l3),V5l4) ) & ( ( ap(ap(c_2Elist_2EFILTER(A_27a),V0P),V4l3) = V2l1 ) & ( ap(ap(c_2Elist_2EFILTER(A_27a),V0P),V5l4) = V3l2 ) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Elist_2EEVERY__FILTER,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)) => ( p(ap(ap(c_2Elist_2EEVERY(A_27a),V0P1),ap(ap(c_2Elist_2EFILTER(A_27a),V1P2),V2l))) <=> p(ap(ap(c_2Elist_2EEVERY(A_27a),f397(A_27a,V1P2,V0P1)),V2l)) ) ) ) )))).
fof(conj_thm_2Elist_2EEVERY__FILTER__IMP,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)) => ( p(ap(ap(c_2Elist_2EEVERY(A_27a),V0P1),V2l)) => p(ap(ap(c_2Elist_2EEVERY(A_27a),V0P1),ap(ap(c_2Elist_2EFILTER(A_27a),V1P2),V2l))) ) ) ) )))).
fof(conj_thm_2Elist_2EFILTER__COND__REWRITE,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),c_2Elist_2ENIL(A_27a)) = c_2Elist_2ENIL(A_27a) ) & ( ( ! [V2h] : ( mem(V2h,A_27a) => ( p(ap(V0P,V2h)) => ( ap(ap(c_2Elist_2EFILTER(A_27a),V0P),ap(ap(c_2Elist_2ECONS(A_27a),V2h),V1l)) = ap(ap(c_2Elist_2ECONS(A_27a),V2h),ap(ap(c_2Elist_2EFILTER(A_27a),V0P),V1l)) ) ) ) ) & ! [V3h] : ( mem(V3h,A_27a) => ( ( ~~ p(ap(V0P,V3h)) ) => ( ap(ap(c_2Elist_2EFILTER(A_27a),V0P),ap(ap(c_2Elist_2ECONS(A_27a),V3h),V1l)) = ap(ap(c_2Elist_2EFILTER(A_27a),V0P),V1l) ) ) ) ) ) ) )))).
fof(conj_thm_2Elist_2ENOT__NULL__MEM,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ( ~~ p(ap(c_2Elist_2ENULL(A_27a),V0l)) ) <=> ? [V1e] : ( mem(V1e,A_27a) & p(ap(ap(c_2Ebool_2EIN(A_27a),V1e),ap(c_2Elist_2ELIST__TO__SET(A_27a),V0l))) ) ) )))).
fof(conj_thm_2Elist_2EEL__compute,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => ( ap(ap(c_2Elist_2EEL(A_27a),V1n),V0l) = ap(ap(ap(c_2Ebool_2ECOND(A_27a),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),V1n),c_2Enum_2E0)),ap(c_2Elist_2EHD(A_27a),V0l)),ap(ap(c_2Elist_2EEL(A_27a),ap(c_2Eprim__rec_2EPRE,V1n)),ap(c_2Elist_2ETL(A_27a),V0l))) ) ) )))).
fof(conj_thm_2Elist_2EEL__simp,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ( ( ap(ap(c_2Elist_2EEL(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V0n))),V1l) = ap(ap(c_2Elist_2EEL(A_27a),ap(c_2Eprim__rec_2EPRE,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V0n)))),ap(c_2Elist_2ETL(A_27a),V1l)) ) & ( ap(ap(c_2Elist_2EEL(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,V0n))),V1l) = ap(ap(c_2Elist_2EEL(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V0n))),ap(c_2Elist_2ETL(A_27a),V1l)) ) ) ) )))).
fof(conj_thm_2Elist_2EEL__restricted,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1l] : ( mem(V1l,A_27b) => ! [V2ls] : ( mem(V2ls,ty_2Elist_2Elist(A_27b)) => ( ( ap(c_2Elist_2EEL(A_27a),c_2Enum_2E0) = c_2Elist_2EHD(A_27a) ) & ( ap(ap(c_2Elist_2EEL(A_27b),ap(c_2Enum_2ESUC,V0n)),ap(ap(c_2Elist_2ECONS(A_27b),V1l),V2ls)) = ap(ap(c_2Elist_2EEL(A_27b),V0n),V2ls) ) ) ) ) ))))).
fof(conj_thm_2Elist_2EEL__simp__restricted,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ! [V1l] : ( mem(V1l,A_27a) => ! [V2ls] : ( mem(V2ls,ty_2Elist_2Elist(A_27a)) => ( ( ap(ap(c_2Elist_2EEL(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V0n))),ap(ap(c_2Elist_2ECONS(A_27a),V1l),V2ls)) = ap(ap(c_2Elist_2EEL(A_27a),ap(c_2Eprim__rec_2EPRE,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V0n)))),V2ls) ) & ( ap(ap(c_2Elist_2EEL(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,V0n))),ap(ap(c_2Elist_2ECONS(A_27a),V1l),V2ls)) = ap(ap(c_2Elist_2EEL(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,V0n))),V2ls) ) ) ) ) )))).
fof(conj_thm_2Elist_2ESUM__eq__0,lemma,(! [V0ls] : ( mem(V0ls,ty_2Elist_2Elist(ty_2Enum_2Enum)) => ( ( ap(c_2Elist_2ESUM,V0ls) = c_2Enum_2E0 ) <=> ! [V1x] : ( mem(V1x,ty_2Enum_2Enum) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),V1x),ap(c_2Elist_2ELIST__TO__SET(ty_2Enum_2Enum),V0ls))) => ( V1x = c_2Enum_2E0 ) ) ) ) ))).
fof(conj_thm_2Elist_2ENULL__FILTER,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1ls] : ( mem(V1ls,ty_2Elist_2Elist(A_27a)) => ( p(ap(c_2Elist_2ENULL(A_27a),ap(ap(c_2Elist_2EFILTER(A_27a),V0P),V1ls))) <=> ! [V2x] : ( mem(V2x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),ap(c_2Elist_2ELIST__TO__SET(A_27a),V1ls))) => ( ~~ p(ap(V0P,V2x)) ) ) ) ) ) )))).
fof(conj_thm_2Elist_2EWF__LIST__PRED,lemma,( ! [A_27a]: ( ne(A_27a) => p(ap(c_2Erelation_2EWF(ty_2Elist_2Elist(A_27a)),f400(A_27a)))))).
fof(conj_thm_2Elist_2ELIST__REL__rules,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0R] : ( mem(V0R,arr(A_27a,arr(A_27b,bool))) => ( p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27b),V0R),c_2Elist_2ENIL(A_27a)),c_2Elist_2ENIL(A_27b))) & ! [V1h1] : ( mem(V1h1,A_27a) => ! [V2h2] : ( mem(V2h2,A_27b) => ! [V3t1] : ( mem(V3t1,ty_2Elist_2Elist(A_27a)) => ! [V4t2] : ( mem(V4t2,ty_2Elist_2Elist(A_27b)) => ( ( p(ap(ap(V0R,V1h1),V2h2)) & p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27b),V0R),V3t1),V4t2)) ) => p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27b),V0R),ap(ap(c_2Elist_2ECONS(A_27a),V1h1),V3t1)),ap(ap(c_2Elist_2ECONS(A_27b),V2h2),V4t2))) ) ) ) ) ) ) ))))).
fof(conj_thm_2Elist_2ELIST__REL__ind,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0R] : ( mem(V0R,arr(A_27a,arr(A_27b,bool))) => ! [V1LIST__REL_27] : ( mem(V1LIST__REL_27,arr(ty_2Elist_2Elist(A_27a),arr(ty_2Elist_2Elist(A_27b),bool))) => ( ( p(ap(ap(V1LIST__REL_27,c_2Elist_2ENIL(A_27a)),c_2Elist_2ENIL(A_27b))) & ! [V2h1] : ( mem(V2h1,A_27a) => ! [V3h2] : ( mem(V3h2,A_27b) => ! [V4t1] : ( mem(V4t1,ty_2Elist_2Elist(A_27a)) => ! [V5t2] : ( mem(V5t2,ty_2Elist_2Elist(A_27b)) => ( ( p(ap(ap(V0R,V2h1),V3h2)) & p(ap(ap(V1LIST__REL_27,V4t1),V5t2)) ) => p(ap(ap(V1LIST__REL_27,ap(ap(c_2Elist_2ECONS(A_27a),V2h1),V4t1)),ap(ap(c_2Elist_2ECONS(A_27b),V3h2),V5t2))) ) ) ) ) ) ) => ! [V6a0] : ( mem(V6a0,ty_2Elist_2Elist(A_27a)) => ! [V7a1] : ( mem(V7a1,ty_2Elist_2Elist(A_27b)) => ( p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27b),V0R),V6a0),V7a1)) => p(ap(ap(V1LIST__REL_27,V6a0),V7a1)) ) ) ) ) ) ))))).
fof(conj_thm_2Elist_2ELIST__REL__strongind,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0R] : ( mem(V0R,arr(A_27a,arr(A_27b,bool))) => ! [V1LIST__REL_27] : ( mem(V1LIST__REL_27,arr(ty_2Elist_2Elist(A_27a),arr(ty_2Elist_2Elist(A_27b),bool))) => ( ( p(ap(ap(V1LIST__REL_27,c_2Elist_2ENIL(A_27a)),c_2Elist_2ENIL(A_27b))) & ! [V2h1] : ( mem(V2h1,A_27a) => ! [V3h2] : ( mem(V3h2,A_27b) => ! [V4t1] : ( mem(V4t1,ty_2Elist_2Elist(A_27a)) => ! [V5t2] : ( mem(V5t2,ty_2Elist_2Elist(A_27b)) => ( ( p(ap(ap(V0R,V2h1),V3h2)) & ( p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27b),V0R),V4t1),V5t2)) & p(ap(ap(V1LIST__REL_27,V4t1),V5t2)) ) ) => p(ap(ap(V1LIST__REL_27,ap(ap(c_2Elist_2ECONS(A_27a),V2h1),V4t1)),ap(ap(c_2Elist_2ECONS(A_27b),V3h2),V5t2))) ) ) ) ) ) ) => ! [V6a0] : ( mem(V6a0,ty_2Elist_2Elist(A_27a)) => ! [V7a1] : ( mem(V7a1,ty_2Elist_2Elist(A_27b)) => ( p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27b),V0R),V6a0),V7a1)) => p(ap(ap(V1LIST__REL_27,V6a0),V7a1)) ) ) ) ) ) ))))).
fof(conj_thm_2Elist_2ELIST__REL__cases,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0R] : ( mem(V0R,arr(A_27a,arr(A_27b,bool))) => ! [V1a0] : ( mem(V1a0,ty_2Elist_2Elist(A_27a)) => ! [V2a1] : ( mem(V2a1,ty_2Elist_2Elist(A_27b)) => ( p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27b),V0R),V1a0),V2a1)) <=> ( ( ( V1a0 = c_2Elist_2ENIL(A_27a) ) & ( V2a1 = c_2Elist_2ENIL(A_27b) ) ) | ? [V3h1] : ( mem(V3h1,A_27a) & ? [V4h2] : ( mem(V4h2,A_27b) & ? [V5t1] : ( mem(V5t1,ty_2Elist_2Elist(A_27a)) & ? [V6t2] : ( mem(V6t2,ty_2Elist_2Elist(A_27b)) & ( ( V1a0 = ap(ap(c_2Elist_2ECONS(A_27a),V3h1),V5t1) ) & ( ( V2a1 = ap(ap(c_2Elist_2ECONS(A_27b),V4h2),V6t2) ) & ( p(ap(ap(V0R,V3h1),V4h2)) & p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27b),V0R),V5t1),V6t2)) ) ) ) ) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Elist_2ELIST__REL__EL__EQN,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0R] : ( mem(V0R,arr(A_27a,arr(A_27b,bool))) => ! [V1l1] : ( mem(V1l1,ty_2Elist_2Elist(A_27a)) => ! [V2l2] : ( mem(V2l2,ty_2Elist_2Elist(A_27b)) => ( p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27b),V0R),V1l1),V2l2)) <=> ( ( ap(c_2Elist_2ELENGTH(A_27a),V1l1) = ap(c_2Elist_2ELENGTH(A_27b),V2l2) ) & ! [V3n] : ( mem(V3n,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V3n),ap(c_2Elist_2ELENGTH(A_27a),V1l1))) => p(ap(ap(V0R,ap(ap(c_2Elist_2EEL(A_27a),V3n),V1l1)),ap(ap(c_2Elist_2EEL(A_27b),V3n),V2l2))) ) ) ) ) ) ) ))))).
fof(conj_thm_2Elist_2ELIST__REL__def,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0R] : ( mem(V0R,arr(A_27a,arr(A_27b,bool))) => ! [V1a] : ( mem(V1a,A_27a) => ! [V2as] : ( mem(V2as,ty_2Elist_2Elist(A_27a)) => ! [V3b] : ( mem(V3b,A_27b) => ! [V4bs] : ( mem(V4bs,ty_2Elist_2Elist(A_27b)) => ( ( p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27b),V0R),c_2Elist_2ENIL(A_27a)),c_2Elist_2ENIL(A_27b))) <=> $true ) & ( ( p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27b),V0R),ap(ap(c_2Elist_2ECONS(A_27a),V1a),V2as)),c_2Elist_2ENIL(A_27b))) <=> $false ) & ( ( p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27b),V0R),c_2Elist_2ENIL(A_27a)),ap(ap(c_2Elist_2ECONS(A_27b),V3b),V4bs))) <=> $false ) & ( p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27b),V0R),ap(ap(c_2Elist_2ECONS(A_27a),V1a),V2as)),ap(ap(c_2Elist_2ECONS(A_27b),V3b),V4bs))) <=> ( p(ap(ap(V0R,V1a),V3b)) & p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27b),V0R),V2as),V4bs)) ) ) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Elist_2ELIST__REL__mono,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0R1] : ( mem(V0R1,arr(A_27a,arr(A_27b,bool))) => ! [V1R2] : ( mem(V1R2,arr(A_27a,arr(A_27b,bool))) => ! [V2l1] : ( mem(V2l1,ty_2Elist_2Elist(A_27a)) => ! [V3l2] : ( mem(V3l2,ty_2Elist_2Elist(A_27b)) => ( ( ! [V4x] : ( mem(V4x,A_27a) => ! [V5y] : ( mem(V5y,A_27b) => ( p(ap(ap(V0R1,V4x),V5y)) => p(ap(ap(V1R2,V4x),V5y)) ) ) ) ) => ( p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27b),V0R1),V2l1),V3l2)) => p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27b),V1R2),V2l1),V3l2)) ) ) ) ) ) ))))).
fof(conj_thm_2Elist_2ELIST__REL__NIL,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0R] : ( mem(V0R,arr(A_27a,arr(A_27b,bool))) => ! [V1y] : ( mem(V1y,ty_2Elist_2Elist(A_27b)) => ! [V2x] : ( mem(V2x,ty_2Elist_2Elist(A_27a)) => ( ( p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27b),V0R),c_2Elist_2ENIL(A_27a)),V1y)) <=> ( V1y = c_2Elist_2ENIL(A_27b) ) ) & ( p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27b),V0R),V2x),c_2Elist_2ENIL(A_27b))) <=> ( V2x = c_2Elist_2ENIL(A_27a) ) ) ) ) ) ))))).
fof(conj_thm_2Elist_2ELIST__REL__CONS1,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0R] : ( mem(V0R,arr(A_27a,arr(A_27b,bool))) => ! [V1h] : ( mem(V1h,A_27a) => ! [V2t] : ( mem(V2t,ty_2Elist_2Elist(A_27a)) => ! [V3xs] : ( mem(V3xs,ty_2Elist_2Elist(A_27b)) => ( p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27b),V0R),ap(ap(c_2Elist_2ECONS(A_27a),V1h),V2t)),V3xs)) <=> ? [V4h_27] : ( mem(V4h_27,A_27b) & ? [V5t_27] : ( mem(V5t_27,ty_2Elist_2Elist(A_27b)) & ( ( V3xs = ap(ap(c_2Elist_2ECONS(A_27b),V4h_27),V5t_27) ) & ( p(ap(ap(V0R,V1h),V4h_27)) & p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27b),V0R),V2t),V5t_27)) ) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Elist_2ELIST__REL__CONS2,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0R] : ( mem(V0R,arr(A_27a,arr(A_27b,bool))) => ! [V1xs] : ( mem(V1xs,ty_2Elist_2Elist(A_27a)) => ! [V2h] : ( mem(V2h,A_27b) => ! [V3t] : ( mem(V3t,ty_2Elist_2Elist(A_27b)) => ( p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27b),V0R),V1xs),ap(ap(c_2Elist_2ECONS(A_27b),V2h),V3t))) <=> ? [V4h_27] : ( mem(V4h_27,A_27a) & ? [V5t_27] : ( mem(V5t_27,ty_2Elist_2Elist(A_27a)) & ( ( V1xs = ap(ap(c_2Elist_2ECONS(A_27a),V4h_27),V5t_27) ) & ( p(ap(ap(V0R,V4h_27),V2h)) & p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27b),V0R),V5t_27),V3t)) ) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Elist_2ELIST__REL__CONJ,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(A_27a,arr(A_27b,bool))) => ! [V1Q] : ( mem(V1Q,arr(A_27a,arr(A_27b,bool))) => ! [V2l1] : ( mem(V2l1,ty_2Elist_2Elist(A_27a)) => ! [V3l2] : ( mem(V3l2,ty_2Elist_2Elist(A_27b)) => ( p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27b),f402(A_27a,A_27b,V0P,V1Q)),V2l1),V3l2)) <=> ( p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27b),f404(A_27a,A_27b,V0P)),V2l1),V3l2)) & p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27b),f406(A_27a,A_27b,V1Q)),V2l1),V3l2)) ) ) ) ) ) ))))).
fof(conj_thm_2Elist_2ELIST__REL__MAP1,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0R] : ( mem(V0R,arr(A_27a,arr(A_27b,bool))) => ! [V1f] : ( mem(V1f,arr(A_27c,A_27a)) => ! [V2l1] : ( mem(V2l1,ty_2Elist_2Elist(A_27c)) => ! [V3l2] : ( mem(V3l2,ty_2Elist_2Elist(A_27b)) => ( p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27b),V0R),ap(ap(c_2Elist_2EMAP(A_27c,A_27a),V1f),V2l1)),V3l2)) <=> p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27c,A_27b),ap(ap(c_2Ecombin_2Eo(A_27c,arr(A_27b,bool),A_27a),V0R),V1f)),V2l1),V3l2)) ) ) ) ) )))))).
fof(conj_thm_2Elist_2ELIST__REL__MAP2,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0R] : ( mem(V0R,arr(A_27a,arr(A_27b,bool))) => ! [V1l1] : ( mem(V1l1,ty_2Elist_2Elist(A_27a)) => ! [V2f] : ( mem(V2f,arr(A_27c,A_27b)) => ! [V3l2] : ( mem(V3l2,ty_2Elist_2Elist(A_27c)) => ( p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27b),f408(A_27a,A_27b,V0R)),V1l1),ap(ap(c_2Elist_2EMAP(A_27c,A_27b),V2f),V3l2))) <=> p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27c),f410(A_27a,A_27b,A_27c,V0R,V2f)),V1l1),V3l2)) ) ) ) ) )))))).
fof(conj_thm_2Elist_2ELIST__REL__LENGTH,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0R] : ( mem(V0R,arr(A_27a,arr(A_27b,bool))) => ! [V1x] : ( mem(V1x,ty_2Elist_2Elist(A_27a)) => ! [V2y] : ( mem(V2y,ty_2Elist_2Elist(A_27b)) => ( p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27b),V0R),V1x),V2y)) => ( ap(c_2Elist_2ELENGTH(A_27a),V1x) = ap(c_2Elist_2ELENGTH(A_27b),V2y) ) ) ) ) ))))).
fof(conj_thm_2Elist_2ELIST__REL__SPLIT1,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(A_27a,arr(A_27b,bool))) => ! [V1xs2] : ( mem(V1xs2,ty_2Elist_2Elist(A_27a)) => ! [V2xs1] : ( mem(V2xs1,ty_2Elist_2Elist(A_27a)) => ! [V3zs] : ( mem(V3zs,ty_2Elist_2Elist(A_27b)) => ( p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27b),V0P),ap(ap(c_2Elist_2EAPPEND(A_27a),V2xs1),V1xs2)),V3zs)) <=> ? [V4ys1] : ( mem(V4ys1,ty_2Elist_2Elist(A_27b)) & ? [V5ys2] : ( mem(V5ys2,ty_2Elist_2Elist(A_27b)) & ( ( V3zs = ap(ap(c_2Elist_2EAPPEND(A_27b),V4ys1),V5ys2) ) & ( p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27b),V0P),V2xs1),V4ys1)) & p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27b),V0P),V1xs2),V5ys2)) ) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Elist_2ELIST__REL__SPLIT2,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(A_27b,arr(A_27a,bool))) => ! [V1xs2] : ( mem(V1xs2,ty_2Elist_2Elist(A_27a)) => ! [V2xs1] : ( mem(V2xs1,ty_2Elist_2Elist(A_27a)) => ! [V3zs] : ( mem(V3zs,ty_2Elist_2Elist(A_27b)) => ( p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27b,A_27a),V0P),V3zs),ap(ap(c_2Elist_2EAPPEND(A_27a),V2xs1),V1xs2))) <=> ? [V4ys1] : ( mem(V4ys1,ty_2Elist_2Elist(A_27b)) & ? [V5ys2] : ( mem(V5ys2,ty_2Elist_2Elist(A_27b)) & ( ( V3zs = ap(ap(c_2Elist_2EAPPEND(A_27b),V4ys1),V5ys2) ) & ( p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27b,A_27a),V0P),V4ys1),V2xs1)) & p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27b,A_27a),V0P),V5ys2),V1xs2)) ) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Elist_2Elist__size__cong,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0M] : ( mem(V0M,ty_2Elist_2Elist(A_27a)) => ! [V1N] : ( mem(V1N,ty_2Elist_2Elist(A_27a)) => ! [V2f] : ( mem(V2f,arr(A_27a,ty_2Enum_2Enum)) => ! [V3f_27] : ( mem(V3f_27,arr(A_27a,ty_2Enum_2Enum)) => ( ( ( V0M = V1N ) & ! [V4x] : ( mem(V4x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V4x),ap(c_2Elist_2ELIST__TO__SET(A_27a),V1N))) => ( ap(V2f,V4x) = ap(V3f_27,V4x) ) ) ) ) => ( ap(ap(c_2Elist_2Elist__size(A_27a),V2f),V0M) = ap(ap(c_2Elist_2Elist__size(A_27a),V3f_27),V1N) ) ) ) ) ) )))).
fof(conj_thm_2Elist_2EFOLDR__CONG,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ! [V1l_27] : ( mem(V1l_27,ty_2Elist_2Elist(A_27a)) => ! [V2b] : ( mem(V2b,A_27b) => ! [V3b_27] : ( mem(V3b_27,A_27b) => ! [V4f] : ( mem(V4f,arr(A_27a,arr(A_27b,A_27b))) => ! [V5f_27] : ( mem(V5f_27,arr(A_27a,arr(A_27b,A_27b))) => ( ( ( V0l = V1l_27 ) & ( ( V2b = V3b_27 ) & ! [V6x] : ( mem(V6x,A_27a) => ! [V7a] : ( mem(V7a,A_27b) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V6x),ap(c_2Elist_2ELIST__TO__SET(A_27a),V1l_27))) => ( ap(ap(V4f,V6x),V7a) = ap(ap(V5f_27,V6x),V7a) ) ) ) ) ) ) => ( ap(ap(ap(c_2Elist_2EFOLDR(A_27a,A_27b),V4f),V2b),V0l) = ap(ap(ap(c_2Elist_2EFOLDR(A_27a,A_27b),V5f_27),V3b_27),V1l_27) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Elist_2EFOLDL__CONG,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ! [V1l_27] : ( mem(V1l_27,ty_2Elist_2Elist(A_27a)) => ! [V2b] : ( mem(V2b,A_27b) => ! [V3b_27] : ( mem(V3b_27,A_27b) => ! [V4f] : ( mem(V4f,arr(A_27b,arr(A_27a,A_27b))) => ! [V5f_27] : ( mem(V5f_27,arr(A_27b,arr(A_27a,A_27b))) => ( ( ( V0l = V1l_27 ) & ( ( V2b = V3b_27 ) & ! [V6x] : ( mem(V6x,A_27a) => ! [V7a] : ( mem(V7a,A_27b) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V6x),ap(c_2Elist_2ELIST__TO__SET(A_27a),V1l_27))) => ( ap(ap(V4f,V7a),V6x) = ap(ap(V5f_27,V7a),V6x) ) ) ) ) ) ) => ( ap(ap(ap(c_2Elist_2EFOLDL(A_27a,A_27b),V4f),V2b),V0l) = ap(ap(ap(c_2Elist_2EFOLDL(A_27a,A_27b),V5f_27),V3b_27),V1l_27) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Elist_2EMAP__CONG,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0l1] : ( mem(V0l1,ty_2Elist_2Elist(A_27a)) => ! [V1l2] : ( mem(V1l2,ty_2Elist_2Elist(A_27a)) => ! [V2f] : ( mem(V2f,arr(A_27a,A_27b)) => ! [V3f_27] : ( mem(V3f_27,arr(A_27a,A_27b)) => ( ( ( V0l1 = V1l2 ) & ! [V4x] : ( mem(V4x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V4x),ap(c_2Elist_2ELIST__TO__SET(A_27a),V1l2))) => ( ap(V2f,V4x) = ap(V3f_27,V4x) ) ) ) ) => ( ap(ap(c_2Elist_2EMAP(A_27a,A_27b),V2f),V0l1) = ap(ap(c_2Elist_2EMAP(A_27a,A_27b),V3f_27),V1l2) ) ) ) ) ) ))))).
fof(conj_thm_2Elist_2EMAP2__CONG,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0l1] : ( mem(V0l1,ty_2Elist_2Elist(A_27a)) => ! [V1l1_27] : ( mem(V1l1_27,ty_2Elist_2Elist(A_27a)) => ! [V2l2] : ( mem(V2l2,ty_2Elist_2Elist(A_27b)) => ! [V3l2_27] : ( mem(V3l2_27,ty_2Elist_2Elist(A_27b)) => ! [V4f] : ( mem(V4f,arr(A_27a,arr(A_27b,A_27c))) => ! [V5f_27] : ( mem(V5f_27,arr(A_27a,arr(A_27b,A_27c))) => ( ( ( V0l1 = V1l1_27 ) & ( ( V2l2 = V3l2_27 ) & ! [V6x] : ( mem(V6x,A_27a) => ! [V7y] : ( mem(V7y,A_27b) => ( ( p(ap(ap(c_2Ebool_2EIN(A_27a),V6x),ap(c_2Elist_2ELIST__TO__SET(A_27a),V1l1_27))) & p(ap(ap(c_2Ebool_2EIN(A_27b),V7y),ap(c_2Elist_2ELIST__TO__SET(A_27b),V3l2_27))) ) => ( ap(ap(V4f,V6x),V7y) = ap(ap(V5f_27,V6x),V7y) ) ) ) ) ) ) => ( ap(ap(ap(c_2Elist_2EMAP2(A_27c,A_27a,A_27b),V4f),V0l1),V2l2) = ap(ap(ap(c_2Elist_2EMAP2(A_27c,A_27a,A_27b),V5f_27),V1l1_27),V3l2_27) ) ) ) ) ) ) ) )))))).
fof(conj_thm_2Elist_2EEXISTS__CONG,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l1] : ( mem(V0l1,ty_2Elist_2Elist(A_27a)) => ! [V1l2] : ( mem(V1l2,ty_2Elist_2Elist(A_27a)) => ! [V2P] : ( mem(V2P,arr(A_27a,bool)) => ! [V3P_27] : ( mem(V3P_27,arr(A_27a,bool)) => ( ( ( V0l1 = V1l2 ) & ! [V4x] : ( mem(V4x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V4x),ap(c_2Elist_2ELIST__TO__SET(A_27a),V1l2))) => ( p(ap(V2P,V4x)) <=> p(ap(V3P_27,V4x)) ) ) ) ) => ( p(ap(ap(c_2Elist_2EEXISTS(A_27a),V2P),V0l1)) <=> p(ap(ap(c_2Elist_2EEXISTS(A_27a),V3P_27),V1l2)) ) ) ) ) ) )))).
fof(conj_thm_2Elist_2EEVERY__CONG,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l1] : ( mem(V0l1,ty_2Elist_2Elist(A_27a)) => ! [V1l2] : ( mem(V1l2,ty_2Elist_2Elist(A_27a)) => ! [V2P] : ( mem(V2P,arr(A_27a,bool)) => ! [V3P_27] : ( mem(V3P_27,arr(A_27a,bool)) => ( ( ( V0l1 = V1l2 ) & ! [V4x] : ( mem(V4x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V4x),ap(c_2Elist_2ELIST__TO__SET(A_27a),V1l2))) => ( p(ap(V2P,V4x)) <=> p(ap(V3P_27,V4x)) ) ) ) ) => ( p(ap(ap(c_2Elist_2EEVERY(A_27a),V2P),V0l1)) <=> p(ap(ap(c_2Elist_2EEVERY(A_27a),V3P_27),V1l2)) ) ) ) ) ) )))).
fof(conj_thm_2Elist_2EEVERY__MONOTONIC,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1Q] : ( mem(V1Q,arr(A_27a,bool)) => ( ( ! [V2x] : ( mem(V2x,A_27a) => ( p(ap(V0P,V2x)) => p(ap(V1Q,V2x)) ) ) ) => ! [V3l] : ( mem(V3l,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Elist_2EEVERY(A_27a),V0P),V3l)) => p(ap(ap(c_2Elist_2EEVERY(A_27a),V1Q),V3l)) ) ) ) ) )))).
fof(ax_thm_2Elist_2EZIP__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ( ( ! [V0l2] : ( mem(V0l2,ty_2Elist_2Elist(A_27b)) => ( ap(c_2Elist_2EZIP(A_27a,A_27b),ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27b)),c_2Elist_2ENIL(A_27a)),V0l2)) = c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b)) ) ) ) & ( ( ! [V1l1] : ( mem(V1l1,ty_2Elist_2Elist(A_27a)) => ( ap(c_2Elist_2EZIP(A_27a,A_27b),ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27b)),V1l1),c_2Elist_2ENIL(A_27b))) = c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b)) ) ) ) & ! [V2x1] : ( mem(V2x1,A_27a) => ! [V3l1] : ( mem(V3l1,ty_2Elist_2Elist(A_27a)) => ! [V4x2] : ( mem(V4x2,A_27b) => ! [V5l2] : ( mem(V5l2,ty_2Elist_2Elist(A_27b)) => ( ap(c_2Elist_2EZIP(A_27a,A_27b),ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27b)),ap(ap(c_2Elist_2ECONS(A_27a),V2x1),V3l1)),ap(ap(c_2Elist_2ECONS(A_27b),V4x2),V5l2))) = ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V2x1),V4x2)),ap(c_2Elist_2EZIP(A_27a,A_27b),ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27b)),V3l1),V5l2))) ) ) ) ) ) ) ) ) ) )).
fof(conj_thm_2Elist_2EZIP,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) =>  ! [A_27d]: ( ne(A_27d) => ( ( ap(c_2Elist_2EZIP(A_27c,A_27d),ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(A_27c),ty_2Elist_2Elist(A_27d)),c_2Elist_2ENIL(A_27c)),c_2Elist_2ENIL(A_27d))) = c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27c,A_27d)) ) & ! [V0x1] : ( mem(V0x1,A_27a) => ! [V1l1] : ( mem(V1l1,ty_2Elist_2Elist(A_27a)) => ! [V2x2] : ( mem(V2x2,A_27b) => ! [V3l2] : ( mem(V3l2,ty_2Elist_2Elist(A_27b)) => ( ap(c_2Elist_2EZIP(A_27a,A_27b),ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27b)),ap(ap(c_2Elist_2ECONS(A_27a),V0x1),V1l1)),ap(ap(c_2Elist_2ECONS(A_27b),V2x2),V3l2))) = ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V0x1),V2x2)),ap(c_2Elist_2EZIP(A_27a,A_27b),ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27b)),V1l1),V3l2))) ) ) ) ) ) ))))))).
fof(ax_thm_2Elist_2EUNZIP,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ( ( ap(c_2Elist_2EUNZIP(A_27a,A_27b),c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b))) = ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27b)),c_2Elist_2ENIL(A_27a)),c_2Elist_2ENIL(A_27b)) ) & ! [V0x] : ( mem(V0x,ty_2Epair_2Eprod(A_27a,A_27b)) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ap(c_2Elist_2EUNZIP(A_27a,A_27b),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),V0x),V1l)) = ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27b)),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Epair_2EFST(A_27a,A_27b),V0x)),ap(c_2Epair_2EFST(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27b)),ap(c_2Elist_2EUNZIP(A_27a,A_27b),V1l)))),ap(ap(c_2Elist_2ECONS(A_27b),ap(c_2Epair_2ESND(A_27a,A_27b),V0x)),ap(c_2Epair_2ESND(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27b)),ap(c_2Elist_2EUNZIP(A_27a,A_27b),V1l)))) ) ) ) ) ) ) )).
fof(conj_thm_2Elist_2EUNZIP__THM,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1y] : ( mem(V1y,A_27b) => ! [V2t] : ( mem(V2t,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ( ap(c_2Elist_2EUNZIP(A_27a,A_27b),c_2Elist_2ENIL(ty_2Epair_2Eprod(A_27a,A_27b))) = ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27b)),c_2Elist_2ENIL(A_27a)),c_2Elist_2ENIL(A_27b)) ) & ( ap(c_2Elist_2EUNZIP(A_27a,A_27b),ap(ap(c_2Elist_2ECONS(ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V0x),V1y)),V2t)) = ap(ap(c_2Ebool_2ELET(ty_2Epair_2Eprod(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27b)),ty_2Epair_2Eprod(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27b))),ap(c_2Epair_2EUNCURRY(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27b),ty_2Epair_2Eprod(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27b))),f412(A_27a,A_27b,V0x,V1y))),ap(c_2Elist_2EUNZIP(A_27a,A_27b),V2t)) ) ) ) ) ))))).
fof(conj_thm_2Elist_2EUNZIP__MAP,lemma,( ! [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_2Elist_2EUNZIP(A_27a,A_27b),V0L) = ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27b)),ap(ap(c_2Elist_2EMAP(ty_2Epair_2Eprod(A_27a,A_27b),A_27a),c_2Epair_2EFST(A_27a,A_27b)),V0L)),ap(ap(c_2Elist_2EMAP(ty_2Epair_2Eprod(A_27a,A_27b),A_27b),c_2Epair_2ESND(A_27a,A_27b)),V0L)) ) ))))).
fof(conj_thm_2Elist_2ELENGTH__ZIP,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0l1] : ( mem(V0l1,ty_2Elist_2Elist(A_27a)) => ! [V1l2] : ( mem(V1l2,ty_2Elist_2Elist(A_27b)) => ( ( ap(c_2Elist_2ELENGTH(A_27a),V0l1) = ap(c_2Elist_2ELENGTH(A_27b),V1l2) ) => ( ( ap(c_2Elist_2ELENGTH(ty_2Epair_2Eprod(A_27a,A_27b)),ap(c_2Elist_2EZIP(A_27a,A_27b),ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27b)),V0l1),V1l2))) = ap(c_2Elist_2ELENGTH(A_27a),V0l1) ) & ( ap(c_2Elist_2ELENGTH(ty_2Epair_2Eprod(A_27a,A_27b)),ap(c_2Elist_2EZIP(A_27a,A_27b),ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27b)),V0l1),V1l2))) = ap(c_2Elist_2ELENGTH(A_27b),V1l2) ) ) ) ) ))))).
fof(conj_thm_2Elist_2ELENGTH__UNZIP,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0pl] : ( mem(V0pl,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ( ( ap(c_2Elist_2ELENGTH(A_27a),ap(c_2Epair_2EFST(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27b)),ap(c_2Elist_2EUNZIP(A_27a,A_27b),V0pl))) = ap(c_2Elist_2ELENGTH(ty_2Epair_2Eprod(A_27a,A_27b)),V0pl) ) & ( ap(c_2Elist_2ELENGTH(A_27b),ap(c_2Epair_2ESND(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27b)),ap(c_2Elist_2EUNZIP(A_27a,A_27b),V0pl))) = ap(c_2Elist_2ELENGTH(ty_2Epair_2Eprod(A_27a,A_27b)),V0pl) ) ) ))))).
fof(conj_thm_2Elist_2EZIP__UNZIP,lemma,( ! [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_2Elist_2EZIP(A_27a,A_27b),ap(c_2Elist_2EUNZIP(A_27a,A_27b),V0l)) = V0l ) ))))).
fof(conj_thm_2Elist_2EUNZIP__ZIP,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0l1] : ( mem(V0l1,ty_2Elist_2Elist(A_27a)) => ! [V1l2] : ( mem(V1l2,ty_2Elist_2Elist(A_27b)) => ( ( ap(c_2Elist_2ELENGTH(A_27a),V0l1) = ap(c_2Elist_2ELENGTH(A_27b),V1l2) ) => ( ap(c_2Elist_2EUNZIP(A_27a,A_27b),ap(c_2Elist_2EZIP(A_27a,A_27b),ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27b)),V0l1),V1l2))) = ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27b)),V0l1),V1l2) ) ) ) ))))).
fof(conj_thm_2Elist_2EZIP__MAP,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) =>  ! [A_27d]: ( ne(A_27d) => ! [V0l1] : ( mem(V0l1,ty_2Elist_2Elist(A_27a)) => ! [V1l2] : ( mem(V1l2,ty_2Elist_2Elist(A_27b)) => ! [V2f1] : ( mem(V2f1,arr(A_27a,A_27c)) => ! [V3f2] : ( mem(V3f2,arr(A_27b,A_27d)) => ( ( ap(c_2Elist_2ELENGTH(A_27a),V0l1) = ap(c_2Elist_2ELENGTH(A_27b),V1l2) ) => ( ( ap(c_2Elist_2EZIP(A_27c,A_27b),ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(A_27c),ty_2Elist_2Elist(A_27b)),ap(ap(c_2Elist_2EMAP(A_27a,A_27c),V2f1),V0l1)),V1l2)) = ap(ap(c_2Elist_2EMAP(ty_2Epair_2Eprod(A_27a,A_27b),ty_2Epair_2Eprod(A_27c,A_27b)),f413(A_27c,A_27a,A_27b,V2f1)),ap(c_2Elist_2EZIP(A_27a,A_27b),ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27b)),V0l1),V1l2))) ) & ( ap(c_2Elist_2EZIP(A_27a,A_27d),ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27d)),V0l1),ap(ap(c_2Elist_2EMAP(A_27b,A_27d),V3f2),V1l2))) = ap(ap(c_2Elist_2EMAP(ty_2Epair_2Eprod(A_27a,A_27b),ty_2Epair_2Eprod(A_27a,A_27d)),f414(A_27d,A_27a,A_27b,V3f2)),ap(c_2Elist_2EZIP(A_27a,A_27b),ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27b)),V0l1),V1l2))) ) ) ) ) ) ) ))))))).
fof(conj_thm_2Elist_2EMEM__ZIP,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0l1] : ( mem(V0l1,ty_2Elist_2Elist(A_27a)) => ! [V1l2] : ( mem(V1l2,ty_2Elist_2Elist(A_27b)) => ! [V2p] : ( mem(V2p,ty_2Epair_2Eprod(A_27a,A_27b)) => ( ( ap(c_2Elist_2ELENGTH(A_27a),V0l1) = ap(c_2Elist_2ELENGTH(A_27b),V1l2) ) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27b)),V2p),ap(c_2Elist_2ELIST__TO__SET(ty_2Epair_2Eprod(A_27a,A_27b)),ap(c_2Elist_2EZIP(A_27a,A_27b),ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27b)),V0l1),V1l2))))) <=> ? [V3n] : ( mem(V3n,ty_2Enum_2Enum) & ( p(ap(ap(c_2Eprim__rec_2E_3C,V3n),ap(c_2Elist_2ELENGTH(A_27a),V0l1))) & ( V2p = ap(ap(c_2Epair_2E_2C(A_27a,A_27b),ap(ap(c_2Elist_2EEL(A_27a),V3n),V0l1)),ap(ap(c_2Elist_2EEL(A_27b),V3n),V1l2)) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Elist_2EEL__ZIP,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0l1] : ( mem(V0l1,ty_2Elist_2Elist(A_27a)) => ! [V1l2] : ( mem(V1l2,ty_2Elist_2Elist(A_27b)) => ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => ( ( ( ap(c_2Elist_2ELENGTH(A_27a),V0l1) = ap(c_2Elist_2ELENGTH(A_27b),V1l2) ) & p(ap(ap(c_2Eprim__rec_2E_3C,V2n),ap(c_2Elist_2ELENGTH(A_27a),V0l1))) ) => ( ap(ap(c_2Elist_2EEL(ty_2Epair_2Eprod(A_27a,A_27b)),V2n),ap(c_2Elist_2EZIP(A_27a,A_27b),ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27b)),V0l1),V1l2))) = ap(ap(c_2Epair_2E_2C(A_27a,A_27b),ap(ap(c_2Elist_2EEL(A_27a),V2n),V0l1)),ap(ap(c_2Elist_2EEL(A_27b),V2n),V1l2)) ) ) ) ) ))))).
fof(conj_thm_2Elist_2EMAP2__ZIP,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0l1] : ( mem(V0l1,ty_2Elist_2Elist(A_27a)) => ! [V1l2] : ( mem(V1l2,ty_2Elist_2Elist(A_27b)) => ( ( ap(c_2Elist_2ELENGTH(A_27a),V0l1) = ap(c_2Elist_2ELENGTH(A_27b),V1l2) ) => ! [V2f] : ( mem(V2f,arr(A_27a,arr(A_27b,A_27c))) => ( ap(ap(ap(c_2Elist_2EMAP2(A_27c,A_27a,A_27b),V2f),V0l1),V1l2) = ap(ap(c_2Elist_2EMAP(ty_2Epair_2Eprod(A_27a,A_27b),A_27c),ap(c_2Epair_2EUNCURRY(A_27a,A_27b,A_27c),V2f)),ap(c_2Elist_2EZIP(A_27a,A_27b),ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27b)),V0l1),V1l2))) ) ) ) ) )))))).
fof(conj_thm_2Elist_2EMAP2__MAP,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0l1] : ( mem(V0l1,ty_2Elist_2Elist(A_27a)) => ! [V1l2] : ( mem(V1l2,ty_2Elist_2Elist(A_27b)) => ( ( ap(c_2Elist_2ELENGTH(A_27a),V0l1) = ap(c_2Elist_2ELENGTH(A_27b),V1l2) ) => ! [V2f] : ( mem(V2f,arr(A_27a,arr(A_27b,A_27c))) => ( ap(ap(ap(c_2Elist_2EMAP2(A_27c,A_27a,A_27b),V2f),V0l1),V1l2) = ap(ap(c_2Elist_2EMAP(ty_2Epair_2Eprod(A_27a,A_27b),A_27c),ap(c_2Epair_2EUNCURRY(A_27a,A_27b,A_27c),V2f)),ap(c_2Elist_2EZIP(A_27a,A_27b),ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27b)),V0l1),V1l2))) ) ) ) ) )))))).
fof(conj_thm_2Elist_2EMAP__ZIP,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) =>  ! [A_27d]: ( ne(A_27d) => ! [V0l1] : ( mem(V0l1,ty_2Elist_2Elist(A_27a)) => ! [V1l2] : ( mem(V1l2,ty_2Elist_2Elist(A_27b)) => ! [V2f] : ( mem(V2f,arr(A_27a,A_27c)) => ! [V3g] : ( mem(V3g,arr(A_27b,A_27d)) => ( ( ap(c_2Elist_2ELENGTH(A_27a),V0l1) = ap(c_2Elist_2ELENGTH(A_27b),V1l2) ) => ( ( ap(ap(c_2Elist_2EMAP(ty_2Epair_2Eprod(A_27a,A_27b),A_27a),c_2Epair_2EFST(A_27a,A_27b)),ap(c_2Elist_2EZIP(A_27a,A_27b),ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27b)),V0l1),V1l2))) = V0l1 ) & ( ( ap(ap(c_2Elist_2EMAP(ty_2Epair_2Eprod(A_27a,A_27b),A_27b),c_2Epair_2ESND(A_27a,A_27b)),ap(c_2Elist_2EZIP(A_27a,A_27b),ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27b)),V0l1),V1l2))) = V1l2 ) & ( ( ap(ap(c_2Elist_2EMAP(ty_2Epair_2Eprod(A_27a,A_27b),A_27c),ap(ap(c_2Ecombin_2Eo(ty_2Epair_2Eprod(A_27a,A_27b),A_27c,A_27a),V2f),c_2Epair_2EFST(A_27a,A_27b))),ap(c_2Elist_2EZIP(A_27a,A_27b),ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27b)),V0l1),V1l2))) = ap(ap(c_2Elist_2EMAP(A_27a,A_27c),V2f),V0l1) ) & ( ap(ap(c_2Elist_2EMAP(ty_2Epair_2Eprod(A_27a,A_27b),A_27d),ap(ap(c_2Ecombin_2Eo(ty_2Epair_2Eprod(A_27a,A_27b),A_27d,A_27b),V3g),c_2Epair_2ESND(A_27a,A_27b))),ap(c_2Elist_2EZIP(A_27a,A_27b),ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27b)),V0l1),V1l2))) = ap(ap(c_2Elist_2EMAP(A_27b,A_27d),V3g),V1l2) ) ) ) ) ) ) ) ) ))))))).
fof(conj_thm_2Elist_2EMEM__EL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ! [V1x] : ( mem(V1x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V1x),ap(c_2Elist_2ELIST__TO__SET(A_27a),V0l))) <=> ? [V2n] : ( mem(V2n,ty_2Enum_2Enum) & ( p(ap(ap(c_2Eprim__rec_2E_3C,V2n),ap(c_2Elist_2ELENGTH(A_27a),V0l))) & ( V1x = ap(ap(c_2Elist_2EEL(A_27a),V2n),V0l) ) ) ) ) ) )))).
fof(conj_thm_2Elist_2ESUM__MAP__PLUS__ZIP,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(ty_2Epair_2Eprod(A_27a,A_27b),ty_2Enum_2Enum)) => ! [V1g] : ( mem(V1g,arr(A_27a,ty_2Enum_2Enum)) => ! [V2h] : ( mem(V2h,arr(A_27b,ty_2Enum_2Enum)) => ! [V3ls1] : ( mem(V3ls1,ty_2Elist_2Elist(A_27a)) => ! [V4ls2] : ( mem(V4ls2,ty_2Elist_2Elist(A_27b)) => ( ( ( ap(c_2Elist_2ELENGTH(A_27a),V3ls1) = ap(c_2Elist_2ELENGTH(A_27b),V4ls2) ) & ! [V5x] : ( mem(V5x,A_27a) => ! [V6y] : ( mem(V6y,A_27b) => ( ap(V0f,ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V5x),V6y)) = ap(ap(c_2Earithmetic_2E_2B,ap(V1g,V5x)),ap(V2h,V6y)) ) ) ) ) => ( ap(c_2Elist_2ESUM,ap(ap(c_2Elist_2EMAP(ty_2Epair_2Eprod(A_27a,A_27b),ty_2Enum_2Enum),V0f),ap(c_2Elist_2EZIP(A_27a,A_27b),ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27b)),V3ls1),V4ls2)))) = ap(ap(c_2Earithmetic_2E_2B,ap(c_2Elist_2ESUM,ap(ap(c_2Elist_2EMAP(A_27a,ty_2Enum_2Enum),V1g),V3ls1))),ap(c_2Elist_2ESUM,ap(ap(c_2Elist_2EMAP(A_27b,ty_2Enum_2Enum),V2h),V4ls2))) ) ) ) ) ) ) ))))).
fof(conj_thm_2Elist_2ELIST__REL__EVERY__ZIP,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0R] : ( mem(V0R,arr(A_27a,arr(A_27b,bool))) => ! [V1l1] : ( mem(V1l1,ty_2Elist_2Elist(A_27a)) => ! [V2l2] : ( mem(V2l2,ty_2Elist_2Elist(A_27b)) => ( p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27b),V0R),V1l1),V2l2)) <=> ( ( ap(c_2Elist_2ELENGTH(A_27a),V1l1) = ap(c_2Elist_2ELENGTH(A_27b),V2l2) ) & p(ap(ap(c_2Elist_2EEVERY(ty_2Epair_2Eprod(A_27a,A_27b)),ap(c_2Epair_2EUNCURRY(A_27a,A_27b,bool),V0R)),ap(c_2Elist_2EZIP(A_27a,A_27b),ap(ap(c_2Epair_2E_2C(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27b)),V1l1),V2l2)))) ) ) ) ) ))))).
fof(ax_thm_2Elist_2EREVERSE__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ap(c_2Elist_2EREVERSE(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_2Elist_2EREVERSE(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V0h),V1t)) = ap(ap(c_2Elist_2EAPPEND(A_27a),ap(c_2Elist_2EREVERSE(A_27a),V1t)),ap(ap(c_2Elist_2ECONS(A_27a),V0h),c_2Elist_2ENIL(A_27a))) ) ) ) ) ) )).
fof(conj_thm_2Elist_2EREVERSE__APPEND,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l1] : ( mem(V0l1,ty_2Elist_2Elist(A_27a)) => ! [V1l2] : ( mem(V1l2,ty_2Elist_2Elist(A_27a)) => ( ap(c_2Elist_2EREVERSE(A_27a),ap(ap(c_2Elist_2EAPPEND(A_27a),V0l1),V1l2)) = ap(ap(c_2Elist_2EAPPEND(A_27a),ap(c_2Elist_2EREVERSE(A_27a),V1l2)),ap(c_2Elist_2EREVERSE(A_27a),V0l1)) ) ) )))).
fof(conj_thm_2Elist_2EREVERSE__REVERSE,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ap(c_2Elist_2EREVERSE(A_27a),ap(c_2Elist_2EREVERSE(A_27a),V0l)) = V0l ) )))).
fof(conj_thm_2Elist_2EREVERSE__11,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l1] : ( mem(V0l1,ty_2Elist_2Elist(A_27a)) => ! [V1l2] : ( mem(V1l2,ty_2Elist_2Elist(A_27a)) => ( ( ap(c_2Elist_2EREVERSE(A_27a),V0l1) = ap(c_2Elist_2EREVERSE(A_27a),V1l2) ) <=> ( V0l1 = V1l2 ) ) ) )))).
fof(conj_thm_2Elist_2EMEM__REVERSE,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ! [V1x] : ( mem(V1x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V1x),ap(c_2Elist_2ELIST__TO__SET(A_27a),ap(c_2Elist_2EREVERSE(A_27a),V0l)))) <=> p(ap(ap(c_2Ebool_2EIN(A_27a),V1x),ap(c_2Elist_2ELIST__TO__SET(A_27a),V0l))) ) ) )))).
fof(conj_thm_2Elist_2ELENGTH__REVERSE,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ap(c_2Elist_2ELENGTH(A_27a),ap(c_2Elist_2EREVERSE(A_27a),V0l)) = ap(c_2Elist_2ELENGTH(A_27a),V0l) ) )))).
fof(conj_thm_2Elist_2EREVERSE__EQ__NIL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ( ap(c_2Elist_2EREVERSE(A_27a),V0l) = c_2Elist_2ENIL(A_27a) ) <=> ( V0l = c_2Elist_2ENIL(A_27a) ) ) )))).
fof(conj_thm_2Elist_2EREVERSE__EQ__SING,conjecture,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ! [V1e] : ( mem(V1e,A_27a) => ( ( ap(c_2Elist_2EREVERSE(A_27a),V0l) = ap(ap(c_2Elist_2ECONS(A_27a),V1e),c_2Elist_2ENIL(A_27a)) ) <=> ( V0l = ap(ap(c_2Elist_2ECONS(A_27a),V1e),c_2Elist_2ENIL(A_27a)) ) ) ) )))).
