include('Axioms/set_relation_2.ax').
tff(tp_ty_2Elist_2Elist,type,( ty_2Elist_2Elist: del > del )).
tff(tp_c_2Elist_2EALL__DISTINCT,type,(c_2Elist_2EALL__DISTINCT:del > $i)).
tff(mem_c_2Elist_2EALL__DISTINCT,axiom,( ! [A_27a:del] : mem(c_2Elist_2EALL__DISTINCT(A_27a),arr(ty_2Elist_2Elist(A_27a),bool)))).
tff(tp_c_2Elist_2EAPPEND,type,(c_2Elist_2EAPPEND:del > $i)).
tff(mem_c_2Elist_2EAPPEND,axiom,( ! [A_27a:del] : mem(c_2Elist_2EAPPEND(A_27a),arr(ty_2Elist_2Elist(A_27a),arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a)))))).
tff(tp_c_2Elist_2ECONS,type,(c_2Elist_2ECONS:del > $i)).
tff(mem_c_2Elist_2ECONS,axiom,( ! [A_27a:del] : mem(c_2Elist_2ECONS(A_27a),arr(A_27a,arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a)))))).
tff(tp_c_2Elist_2EDROP,type,(c_2Elist_2EDROP:del > $i)).
tff(mem_c_2Elist_2EDROP,axiom,( ! [A_27a:del] : mem(c_2Elist_2EDROP(A_27a),arr(ty_2Enum_2Enum,arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a)))))).
tff(tp_c_2Elist_2EEL,type,(c_2Elist_2EEL:del > $i)).
tff(mem_c_2Elist_2EEL,axiom,( ! [A_27a:del] : mem(c_2Elist_2EEL(A_27a),arr(ty_2Enum_2Enum,arr(ty_2Elist_2Elist(A_27a),A_27a))))).
tff(tp_c_2Elist_2EEVERY,type,(c_2Elist_2EEVERY:del > $i)).
tff(mem_c_2Elist_2EEVERY,axiom,( ! [A_27a:del] : mem(c_2Elist_2EEVERY(A_27a),arr(arr(A_27a,bool),arr(ty_2Elist_2Elist(A_27a),bool))))).
tff(tp_c_2Elist_2EEVERYi,type,(c_2Elist_2EEVERYi:del > $i)).
tff(mem_c_2Elist_2EEVERYi,axiom,( ! [A_27a:del] : mem(c_2Elist_2EEVERYi(A_27a),arr(arr(ty_2Enum_2Enum,arr(A_27a,bool)),arr(ty_2Elist_2Elist(A_27a),bool))))).
tff(tp_c_2Elist_2EEXISTS,type,(c_2Elist_2EEXISTS:del > $i)).
tff(mem_c_2Elist_2EEXISTS,axiom,( ! [A_27a:del] : mem(c_2Elist_2EEXISTS(A_27a),arr(arr(A_27a,bool),arr(ty_2Elist_2Elist(A_27a),bool))))).
tff(tp_c_2Elist_2EFILTER,type,(c_2Elist_2EFILTER:del > $i)).
tff(mem_c_2Elist_2EFILTER,axiom,( ! [A_27a:del] : mem(c_2Elist_2EFILTER(A_27a),arr(arr(A_27a,bool),arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a)))))).
tff(tp_c_2Elist_2EFIND,type,(c_2Elist_2EFIND:del > $i)).
tff(mem_c_2Elist_2EFIND,axiom,( ! [A_27a:del] : mem(c_2Elist_2EFIND(A_27a),arr(arr(A_27a,bool),arr(ty_2Elist_2Elist(A_27a),ty_2Eoption_2Eoption(A_27a)))))).
tff(tp_c_2Elist_2EFLAT,type,(c_2Elist_2EFLAT:del > $i)).
tff(mem_c_2Elist_2EFLAT,axiom,( ! [A_27a:del] : mem(c_2Elist_2EFLAT(A_27a),arr(ty_2Elist_2Elist(ty_2Elist_2Elist(A_27a)),ty_2Elist_2Elist(A_27a))))).
tff(tp_c_2Elist_2EFOLDL,type,(c_2Elist_2EFOLDL:(del * del) > $i)).
tff(mem_c_2Elist_2EFOLDL,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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))))))).
tff(tp_c_2Elist_2EFOLDL2,type,(c_2Elist_2EFOLDL2:(del * del * del) > $i)).
tff(mem_c_2Elist_2EFOLDL2,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27c:del] : 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))))))))).
tff(tp_c_2Elist_2EFOLDR,type,(c_2Elist_2EFOLDR:(del * del) > $i)).
tff(mem_c_2Elist_2EFOLDR,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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))))))).
tff(tp_c_2Elist_2EFRONT,type,(c_2Elist_2EFRONT:del > $i)).
tff(mem_c_2Elist_2EFRONT,axiom,( ! [A_27a:del] : mem(c_2Elist_2EFRONT(A_27a),arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a))))).
tff(tp_c_2Elist_2EGENLIST,type,(c_2Elist_2EGENLIST:del > $i)).
tff(mem_c_2Elist_2EGENLIST,axiom,( ! [A_27a:del] : mem(c_2Elist_2EGENLIST(A_27a),arr(arr(ty_2Enum_2Enum,A_27a),arr(ty_2Enum_2Enum,ty_2Elist_2Elist(A_27a)))))).
tff(tp_c_2Elist_2EGENLIST__AUX,type,(c_2Elist_2EGENLIST__AUX:del > $i)).
tff(mem_c_2Elist_2EGENLIST__AUX,axiom,( ! [A_27a:del] : 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))))))).
tff(tp_c_2Elist_2EHD,type,(c_2Elist_2EHD:del > $i)).
tff(mem_c_2Elist_2EHD,axiom,( ! [A_27a:del] : mem(c_2Elist_2EHD(A_27a),arr(ty_2Elist_2Elist(A_27a),A_27a)))).
tff(tp_c_2Elist_2EINDEX__FIND,type,(c_2Elist_2EINDEX__FIND:del > $i)).
tff(mem_c_2Elist_2EINDEX__FIND,axiom,( ! [A_27a:del] : 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)))))))).
tff(tp_c_2Elist_2EINDEX__OF,type,(c_2Elist_2EINDEX__OF:del > $i)).
tff(mem_c_2Elist_2EINDEX__OF,axiom,( ! [A_27a:del] : mem(c_2Elist_2EINDEX__OF(A_27a),arr(A_27a,arr(ty_2Elist_2Elist(A_27a),ty_2Eoption_2Eoption(ty_2Enum_2Enum)))))).
tff(tp_c_2Elist_2ELAST,type,(c_2Elist_2ELAST:del > $i)).
tff(mem_c_2Elist_2ELAST,axiom,( ! [A_27a:del] : mem(c_2Elist_2ELAST(A_27a),arr(ty_2Elist_2Elist(A_27a),A_27a)))).
tff(tp_c_2Elist_2ELEN,type,(c_2Elist_2ELEN:del > $i)).
tff(mem_c_2Elist_2ELEN,axiom,( ! [A_27a:del] : mem(c_2Elist_2ELEN(A_27a),arr(ty_2Elist_2Elist(A_27a),arr(ty_2Enum_2Enum,ty_2Enum_2Enum))))).
tff(tp_c_2Elist_2ELENGTH,type,(c_2Elist_2ELENGTH:del > $i)).
tff(mem_c_2Elist_2ELENGTH,axiom,( ! [A_27a:del] : mem(c_2Elist_2ELENGTH(A_27a),arr(ty_2Elist_2Elist(A_27a),ty_2Enum_2Enum)))).
tff(tp_c_2Elist_2ELIST__APPLY,type,(c_2Elist_2ELIST__APPLY:(del * del) > $i)).
tff(mem_c_2Elist_2ELIST__APPLY,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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))))))).
tff(tp_c_2Elist_2ELIST__BIND,type,(c_2Elist_2ELIST__BIND:(del * del) > $i)).
tff(mem_c_2Elist_2ELIST__BIND,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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))))))).
tff(stp_c_ty_2Elist_2Elist_ty_2Eone_2Eone,type,(tp__c_ty_2Elist_2Elist_ty_2Eone_2Eone : $tType)).
tff(stp_inj_c_ty_2Elist_2Elist_ty_2Eone_2Eone,type,(inj__c_ty_2Elist_2Elist_ty_2Eone_2Eone : tp__c_ty_2Elist_2Elist_ty_2Eone_2Eone > $i)).
tff(stp_surj_c_ty_2Elist_2Elist_ty_2Eone_2Eone,type,(surj__c_ty_2Elist_2Elist_ty_2Eone_2Eone : $i > tp__c_ty_2Elist_2Elist_ty_2Eone_2Eone)).
tff(stp_inj_surj_c_ty_2Elist_2Elist_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Elist_2Elist_ty_2Eone_2Eone] : (surj__c_ty_2Elist_2Elist_ty_2Eone_2Eone(inj__c_ty_2Elist_2Elist_ty_2Eone_2Eone(X)) = X))).
tff(stp_inj_mem_c_ty_2Elist_2Elist_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Elist_2Elist_ty_2Eone_2Eone] : (mem(inj__c_ty_2Elist_2Elist_ty_2Eone_2Eone(X),ty_2Elist_2Elist(ty_2Eone_2Eone))))).
tff(stp_iso_mem_c_ty_2Elist_2Elist_ty_2Eone_2Eone,axiom,( ! [X:$i] : (mem(X,ty_2Elist_2Elist(ty_2Eone_2Eone)) => (X = inj__c_ty_2Elist_2Elist_ty_2Eone_2Eone(surj__c_ty_2Elist_2Elist_ty_2Eone_2Eone(X)))))).
tff(tp_c_2Elist_2ELIST__GUARD,type,(c_2Elist_2ELIST__GUARD:$i)).
tff(mem_c_2Elist_2ELIST__GUARD,axiom,mem(c_2Elist_2ELIST__GUARD,arr(bool,ty_2Elist_2Elist(ty_2Eone_2Eone)))).
tff(tp_c_2Elist_2ELIST__IGNORE__BIND,type,(c_2Elist_2ELIST__IGNORE__BIND:(del * del) > $i)).
tff(mem_c_2Elist_2ELIST__IGNORE__BIND,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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))))))).
tff(tp_c_2Elist_2ELIST__LIFT2,type,(c_2Elist_2ELIST__LIFT2:(del * del * del) > $i)).
tff(mem_c_2Elist_2ELIST__LIFT2,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27c:del] : 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))))))))).
tff(tp_c_2Elist_2ELIST__REL,type,(c_2Elist_2ELIST__REL:(del * del) > $i)).
tff(mem_c_2Elist_2ELIST__REL,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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))))))).
tff(tp_c_2Elist_2ELIST__TO__SET,type,(c_2Elist_2ELIST__TO__SET:del > $i)).
tff(mem_c_2Elist_2ELIST__TO__SET,axiom,( ! [A_27a:del] : mem(c_2Elist_2ELIST__TO__SET(A_27a),arr(ty_2Elist_2Elist(A_27a),arr(A_27a,bool))))).
tff(tp_c_2Elist_2ELLEX,type,(c_2Elist_2ELLEX:del > $i)).
tff(mem_c_2Elist_2ELLEX,axiom,( ! [A_27a:del] : 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)))))).
tff(tp_c_2Elist_2ELRC,type,(c_2Elist_2ELRC:del > $i)).
tff(mem_c_2Elist_2ELRC,axiom,( ! [A_27a:del] : 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))))))).
tff(tp_c_2Elist_2ELUPDATE,type,(c_2Elist_2ELUPDATE:del > $i)).
tff(mem_c_2Elist_2ELUPDATE,axiom,( ! [A_27a:del] : mem(c_2Elist_2ELUPDATE(A_27a),arr(A_27a,arr(ty_2Enum_2Enum,arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a))))))).
tff(tp_c_2Elist_2EMAP,type,(c_2Elist_2EMAP:(del * del) > $i)).
tff(mem_c_2Elist_2EMAP,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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))))))).
tff(tp_c_2Elist_2EMAP2,type,(c_2Elist_2EMAP2:(del * del * del) > $i)).
tff(mem_c_2Elist_2EMAP2,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27c:del] : 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))))))))).
tff(tp_c_2Elist_2ENIL,type,(c_2Elist_2ENIL:del > $i)).
tff(mem_c_2Elist_2ENIL,axiom,( ! [A_27a:del] : mem(c_2Elist_2ENIL(A_27a),ty_2Elist_2Elist(A_27a)))).
tff(tp_c_2Elist_2ENULL,type,(c_2Elist_2ENULL:del > $i)).
tff(mem_c_2Elist_2ENULL,axiom,( ! [A_27a:del] : mem(c_2Elist_2ENULL(A_27a),arr(ty_2Elist_2Elist(A_27a),bool)))).
tff(tp_c_2Elist_2EOPT__MMAP,type,(c_2Elist_2EOPT__MMAP:(del * del) > $i)).
tff(mem_c_2Elist_2EOPT__MMAP,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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)))))))).
tff(tp_c_2Elist_2EPAD__LEFT,type,(c_2Elist_2EPAD__LEFT:del > $i)).
tff(mem_c_2Elist_2EPAD__LEFT,axiom,( ! [A_27a:del] : 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))))))).
tff(tp_c_2Elist_2EPAD__RIGHT,type,(c_2Elist_2EPAD__RIGHT:del > $i)).
tff(mem_c_2Elist_2EPAD__RIGHT,axiom,( ! [A_27a:del] : 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))))))).
tff(tp_c_2Elist_2EREV,type,(c_2Elist_2EREV:del > $i)).
tff(mem_c_2Elist_2EREV,axiom,( ! [A_27a:del] : mem(c_2Elist_2EREV(A_27a),arr(ty_2Elist_2Elist(A_27a),arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a)))))).
tff(tp_c_2Elist_2EREVERSE,type,(c_2Elist_2EREVERSE:del > $i)).
tff(mem_c_2Elist_2EREVERSE,axiom,( ! [A_27a:del] : mem(c_2Elist_2EREVERSE(A_27a),arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a))))).
tff(tp_c_2Elist_2ESET__TO__LIST,type,(c_2Elist_2ESET__TO__LIST:del > $i)).
tff(mem_c_2Elist_2ESET__TO__LIST,axiom,( ! [A_27a:del] : mem(c_2Elist_2ESET__TO__LIST(A_27a),arr(arr(A_27a,bool),ty_2Elist_2Elist(A_27a))))).
tff(tp_c_2Elist_2ESHORTLEX,type,(c_2Elist_2ESHORTLEX:del > $i)).
tff(mem_c_2Elist_2ESHORTLEX,axiom,( ! [A_27a:del] : 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)))))).
tff(tp_c_2Elist_2ESNOC,type,(c_2Elist_2ESNOC:del > $i)).
tff(mem_c_2Elist_2ESNOC,axiom,( ! [A_27a:del] : mem(c_2Elist_2ESNOC(A_27a),arr(A_27a,arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a)))))).
tff(stp_c_ty_2Elist_2Elist_ty_2Enum_2Enum,type,(tp__c_ty_2Elist_2Elist_ty_2Enum_2Enum : $tType)).
tff(stp_inj_c_ty_2Elist_2Elist_ty_2Enum_2Enum,type,(inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum : tp__c_ty_2Elist_2Elist_ty_2Enum_2Enum > $i)).
tff(stp_surj_c_ty_2Elist_2Elist_ty_2Enum_2Enum,type,(surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum : $i > tp__c_ty_2Elist_2Elist_ty_2Enum_2Enum)).
tff(stp_inj_surj_c_ty_2Elist_2Elist_ty_2Enum_2Enum,axiom,( ! [X:tp__c_ty_2Elist_2Elist_ty_2Enum_2Enum] : (surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum(inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum(X)) = X))).
tff(stp_inj_mem_c_ty_2Elist_2Elist_ty_2Enum_2Enum,axiom,( ! [X:tp__c_ty_2Elist_2Elist_ty_2Enum_2Enum] : (mem(inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum(X),ty_2Elist_2Elist(ty_2Enum_2Enum))))).
tff(stp_iso_mem_c_ty_2Elist_2Elist_ty_2Enum_2Enum,axiom,( ! [X:$i] : (mem(X,ty_2Elist_2Elist(ty_2Enum_2Enum)) => (X = inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum(surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum(X)))))).
tff(tp_c_2Elist_2ESUM,type,(c_2Elist_2ESUM:$i)).
tff(mem_c_2Elist_2ESUM,axiom,mem(c_2Elist_2ESUM,arr(ty_2Elist_2Elist(ty_2Enum_2Enum),ty_2Enum_2Enum))).
tff(stp_fo_c_2Elist_2ESUM,type,(fo__c_2Elist_2ESUM:(tp__c_ty_2Elist_2Elist_ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Elist_2ESUM,axiom,( ! [X0:tp__c_ty_2Elist_2Elist_ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Elist_2ESUM(X0)) = ap(c_2Elist_2ESUM,inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum(X0))))).
tff(tp_c_2Elist_2ESUM__ACC,type,(c_2Elist_2ESUM__ACC:$i)).
tff(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)))).
tff(stp_fo_c_2Elist_2ESUM__ACC,type,(fo__c_2Elist_2ESUM__ACC:(tp__c_ty_2Elist_2Elist_ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Elist_2ESUM__ACC,axiom,( ! [X0:tp__c_ty_2Elist_2Elist_ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Elist_2ESUM__ACC(X0,X1)) = ap(ap(c_2Elist_2ESUM__ACC,inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Elist_2ETAKE,type,(c_2Elist_2ETAKE:del > $i)).
tff(mem_c_2Elist_2ETAKE,axiom,( ! [A_27a:del] : mem(c_2Elist_2ETAKE(A_27a),arr(ty_2Enum_2Enum,arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a)))))).
tff(tp_c_2Elist_2ETL,type,(c_2Elist_2ETL:del > $i)).
tff(mem_c_2Elist_2ETL,axiom,( ! [A_27a:del] : mem(c_2Elist_2ETL(A_27a),arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a))))).
tff(tp_c_2Elist_2EUNIQUE,type,(c_2Elist_2EUNIQUE:del > $i)).
tff(mem_c_2Elist_2EUNIQUE,axiom,( ! [A_27a:del] : mem(c_2Elist_2EUNIQUE(A_27a),arr(A_27a,arr(ty_2Elist_2Elist(A_27a),bool))))).
tff(tp_c_2Elist_2EUNZIP,type,(c_2Elist_2EUNZIP:(del * del) > $i)).
tff(mem_c_2Elist_2EUNZIP,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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))))))).
tff(tp_c_2Elist_2EZIP,type,(c_2Elist_2EZIP:(del * del) > $i)).
tff(mem_c_2Elist_2EZIP,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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))))))).
tff(tp_c_2Elist_2EdropWhile,type,(c_2Elist_2EdropWhile:del > $i)).
tff(mem_c_2Elist_2EdropWhile,axiom,( ! [A_27a:del] : mem(c_2Elist_2EdropWhile(A_27a),arr(arr(A_27a,bool),arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a)))))).
tff(tp_c_2Elist_2EisPREFIX,type,(c_2Elist_2EisPREFIX:del > $i)).
tff(mem_c_2Elist_2EisPREFIX,axiom,( ! [A_27a:del] : mem(c_2Elist_2EisPREFIX(A_27a),arr(ty_2Elist_2Elist(A_27a),arr(ty_2Elist_2Elist(A_27a),bool))))).
tff(tp_c_2Elist_2Elist__CASE,type,(c_2Elist_2Elist__CASE:(del * del) > $i)).
tff(mem_c_2Elist_2Elist__CASE,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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))))))).
tff(tp_c_2Elist_2Elist__size,type,(c_2Elist_2Elist__size:del > $i)).
tff(mem_c_2Elist_2Elist__size,axiom,( ! [A_27a:del] : mem(c_2Elist_2Elist__size(A_27a),arr(arr(A_27a,ty_2Enum_2Enum),arr(ty_2Elist_2Elist(A_27a),ty_2Enum_2Enum))))).
tff(tp_c_2Elist_2Enub,type,(c_2Elist_2Enub:del > $i)).
tff(mem_c_2Elist_2Enub,axiom,( ! [A_27a:del] : mem(c_2Elist_2Enub(A_27a),arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a))))).
tff(tp_c_2Elist_2EoEL,type,(c_2Elist_2EoEL:del > $i)).
tff(mem_c_2Elist_2EoEL,axiom,( ! [A_27a:del] : mem(c_2Elist_2EoEL(A_27a),arr(ty_2Enum_2Enum,arr(ty_2Elist_2Elist(A_27a),ty_2Eoption_2Eoption(A_27a)))))).
tff(tp_c_2Elist_2EoHD,type,(c_2Elist_2EoHD:del > $i)).
tff(mem_c_2Elist_2EoHD,axiom,( ! [A_27a:del] : mem(c_2Elist_2EoHD(A_27a),arr(ty_2Elist_2Elist(A_27a),ty_2Eoption_2Eoption(A_27a))))).
tff(tp_c_2Elist_2EsplitAtPki,type,(c_2Elist_2EsplitAtPki:(del * del) > $i)).
tff(mem_c_2Elist_2EsplitAtPki,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : 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))))))).
tff(ax_thm_2Elist_2Elist__TY__DEF,axiom,( ! [A_27a:del]: (? [V0rep:$i] : (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)))))).
tff(ax_thm_2Elist_2Elist__case__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0v:$i] : (mem(V0v,A_27b) => ( ! [V1f:$i] : (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:$i] : (mem(V2a0,A_27a) => ( ! [V3a1:$i] : (mem(V3a1,ty_2Elist_2Elist(A_27a)) => ( ! [V4v:$i] : (mem(V4v,A_27b) => ( ! [V5f:$i] : (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)))))))))))))).
tff(ax_thm_2Elist_2Elist__size__def,axiom,( ! [A_27a:del]: (( ! [V0f:$i] : (mem(V0f,arr(A_27a,ty_2Enum_2Enum)) => (surj__ty_2Enum_2Enum(ap(ap(c_2Elist_2Elist__size(A_27a),V0f),c_2Elist_2ENIL(A_27a))) = fo__c_2Enum_2E0))) & ( ! [V1f:$i] : (mem(V1f,arr(A_27a,ty_2Enum_2Enum)) => ( ! [V2a0:$i] : (mem(V2a0,A_27a) => ( ! [V3a1:$i] : (mem(V3a1,ty_2Elist_2Elist(A_27a)) => (surj__ty_2Enum_2Enum(ap(ap(c_2Elist_2Elist__size(A_27a),V1f),ap(ap(c_2Elist_2ECONS(A_27a),V2a0),V3a1))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(c_2Earithmetic_2E_2B,ap(V1f,V2a0)),ap(ap(c_2Elist_2Elist__size(A_27a),V1f),V3a1)))))))))))))).
tff(conj_thm_2Elist_2Edatatype__list,lemma,(( ! [A_27a:del]: ( ! [V0list:$i] : (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))))))))).
tff(conj_thm_2Elist_2Elist__11,lemma,(( ! [A_27a:del]: ( ! [V0a0:$i] : (mem(V0a0,A_27a) => ( ! [V1a1:$i] : (mem(V1a1,ty_2Elist_2Elist(A_27a)) => ( ! [V2a0_27:$i] : (mem(V2a0_27,A_27a) => ( ! [V3a1_27:$i] : (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)))))))))))))).
tff(conj_thm_2Elist_2Elist__distinct,lemma,(( ! [A_27a:del]: ( ! [V0a1:$i] : (mem(V0a1,ty_2Elist_2Elist(A_27a)) => ( ! [V1a0:$i] : (mem(V1a0,A_27a) => (~~ (c_2Elist_2ENIL(A_27a) = ap(ap(c_2Elist_2ECONS(A_27a),V1a0),V0a1)))))))))).
tff(conj_thm_2Elist_2Elist__Axiom,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f0:$i] : (mem(V0f0,A_27b) => ( ! [V1f1:$i] : (mem(V1f1,arr(A_27a,arr(ty_2Elist_2Elist(A_27a),arr(A_27b,A_27b)))) => (? [V2fn:$i] : (mem(V2fn,arr(ty_2Elist_2Elist(A_27a),A_27b)) & ((ap(V2fn,c_2Elist_2ENIL(A_27a)) = V0f0) & ( ! [V3a0:$i] : (mem(V3a0,A_27a) => ( ! [V4a1:$i] : (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)))))))))))))))))).
tff(conj_thm_2Elist_2Elist__case__cong,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v_27:$i] : (mem(V0v_27,A_27b) => ( ! [V1f_27:$i] : (mem(V1f_27,arr(A_27a,arr(ty_2Elist_2Elist(A_27a),A_27b))) => ( ! [V2M:$i] : (mem(V2M,ty_2Elist_2Elist(A_27a)) => ( ! [V3M_27:$i] : (mem(V3M_27,ty_2Elist_2Elist(A_27a)) => ( ! [V4v:$i] : (mem(V4v,A_27b) => ( ! [V5f:$i] : (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:$i] : (mem(V6a0,A_27a) => ( ! [V7a1:$i] : (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))))))))))))))))))).
tff(conj_thm_2Elist_2Elist__case__eq,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : (mem(V0x,ty_2Elist_2Elist(A_27a)) => ( ! [V1v:$i] : (mem(V1v,A_27b) => ( ! [V2f:$i] : (mem(V2f,arr(A_27a,arr(ty_2Elist_2Elist(A_27a),A_27b))) => ( ! [V3v_27:$i] : (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:$i] : (mem(V4a,A_27a) & (? [V5l:$i] : (mem(V5l,ty_2Elist_2Elist(A_27a)) & ((V0x = ap(ap(c_2Elist_2ECONS(A_27a),V4a),V5l)) & (ap(ap(V2f,V4a),V5l) = V3v_27)))))))))))))))))))).
tff(conj_thm_2Elist_2Elist__Axiom__old,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : (mem(V0x,A_27b) => ( ! [V1f:$i] : (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))))))))))).
tff(ax_thm_2Elist_2ENULL__DEF,axiom,( ! [A_27a:del]: ((p(ap(c_2Elist_2ENULL(A_27a),c_2Elist_2ENIL(A_27a))) <=> $true) & ( ! [V0h:$i] : (mem(V0h,A_27a) => ( ! [V1t:$i] : (mem(V1t,ty_2Elist_2Elist(A_27a)) => (p(ap(c_2Elist_2ENULL(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V0h),V1t))) <=> $false)))))))).
tff(ax_thm_2Elist_2EHD,axiom,( ! [A_27a:del]: ( ! [V0h:$i] : (mem(V0h,A_27a) => ( ! [V1t:$i] : (mem(V1t,ty_2Elist_2Elist(A_27a)) => (ap(c_2Elist_2EHD(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V0h),V1t)) = V0h))))))).
tff(ax_thm_2Elist_2ETL__DEF,axiom,( ! [A_27a:del]: ((ap(c_2Elist_2ETL(A_27a),c_2Elist_2ENIL(A_27a)) = c_2Elist_2ENIL(A_27a)) & ( ! [V0h:$i] : (mem(V0h,A_27a) => ( ! [V1t:$i] : (mem(V1t,ty_2Elist_2Elist(A_27a)) => (ap(c_2Elist_2ETL(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V0h),V1t)) = V1t)))))))).
tff(conj_thm_2Elist_2ETL,lemma,(( ! [A_27a:del]: ( ! [V0h:$i] : (mem(V0h,A_27a) => ( ! [V1t:$i] : (mem(V1t,ty_2Elist_2Elist(A_27a)) => (ap(c_2Elist_2ETL(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V0h),V1t)) = V1t)))))))).
tff(ax_thm_2Elist_2ESUM,axiom,((surj__ty_2Enum_2Enum(ap(c_2Elist_2ESUM,c_2Elist_2ENIL(ty_2Enum_2Enum))) = fo__c_2Enum_2E0) & ( ! [V0h:tp__ty_2Enum_2Enum] : ( ! [V1t:tp__c_ty_2Elist_2Elist_ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Elist_2ESUM,ap(ap(c_2Elist_2ECONS(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V0h)),inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum(V1t)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0h)),ap(c_2Elist_2ESUM,inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum(V1t))))))))).
tff(ax_thm_2Elist_2EAPPEND,axiom,( ! [A_27a:del]: (( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => (ap(ap(c_2Elist_2EAPPEND(A_27a),c_2Elist_2ENIL(A_27a)),V0l) = V0l))) & ( ! [V1l1:$i] : (mem(V1l1,ty_2Elist_2Elist(A_27a)) => ( ! [V2l2:$i] : (mem(V2l2,ty_2Elist_2Elist(A_27a)) => ( ! [V3h:$i] : (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)))))))))))).
tff(ax_thm_2Elist_2EFLAT,axiom,( ! [A_27a:del]: ((ap(c_2Elist_2EFLAT(A_27a),c_2Elist_2ENIL(ty_2Elist_2Elist(A_27a))) = c_2Elist_2ENIL(A_27a)) & ( ! [V0h:$i] : (mem(V0h,ty_2Elist_2Elist(A_27a)) => ( ! [V1t:$i] : (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)))))))))).
tff(ax_thm_2Elist_2ELENGTH,axiom,( ! [A_27a:del]: ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),c_2Elist_2ENIL(A_27a))) = fo__c_2Enum_2E0) & ( ! [V0h:$i] : (mem(V0h,A_27a) => ( ! [V1t:$i] : (mem(V1t,ty_2Elist_2Elist(A_27a)) => (surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V0h),V1t))) = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(c_2Elist_2ELENGTH(A_27a),V1t))))))))))).
tff(ax_thm_2Elist_2EMAP,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0f:$i] : (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:$i] : (mem(V1f,arr(A_27a,A_27b)) => ( ! [V2h:$i] : (mem(V2h,A_27a) => ( ! [V3t:$i] : (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))))))))))))).
tff(ax_thm_2Elist_2ELIST__TO__SET__DEF,axiom,( ! [A_27a:del]: (( ! [V0x:$i] : (mem(V0x,A_27a) => (p(ap(ap(c_2Elist_2ELIST__TO__SET(A_27a),c_2Elist_2ENIL(A_27a)),V0x)) <=> $false))) & ( ! [V1h:$i] : (mem(V1h,A_27a) => ( ! [V2t:$i] : (mem(V2t,ty_2Elist_2Elist(A_27a)) => ( ! [V3x:$i] : (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))))))))))))).
tff(conj_thm_2Elist_2ELIST__TO__SET,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0h:$i] : (mem(V0h,A_27b) => ( ! [V1t:$i] : (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)))))))))))).
tff(ax_thm_2Elist_2EFILTER,axiom,( ! [A_27a:del]: (( ! [V0P:$i] : (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:$i] : (mem(V1P,arr(A_27a,bool)) => ( ! [V2h:$i] : (mem(V2h,A_27a) => ( ! [V3t:$i] : (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)))))))))))).
tff(ax_thm_2Elist_2EFOLDR,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0f:$i] : (mem(V0f,arr(A_27a,arr(A_27b,A_27b))) => ( ! [V1e:$i] : (mem(V1e,A_27b) => (ap(ap(ap(c_2Elist_2EFOLDR(A_27a,A_27b),V0f),V1e),c_2Elist_2ENIL(A_27a)) = V1e))))) & ( ! [V2f:$i] : (mem(V2f,arr(A_27a,arr(A_27b,A_27b))) => ( ! [V3e:$i] : (mem(V3e,A_27b) => ( ! [V4x:$i] : (mem(V4x,A_27a) => ( ! [V5l:$i] : (mem(V5l,ty_2Elist_2Elist(A_27a)) => (ap(ap(ap(c_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))))))))))))))).
tff(ax_thm_2Elist_2EFOLDL,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0f:$i] : (mem(V0f,arr(A_27b,arr(A_27a,A_27b))) => ( ! [V1e:$i] : (mem(V1e,A_27b) => (ap(ap(ap(c_2Elist_2EFOLDL(A_27a,A_27b),V0f),V1e),c_2Elist_2ENIL(A_27a)) = V1e))))) & ( ! [V2f:$i] : (mem(V2f,arr(A_27b,arr(A_27a,A_27b))) => ( ! [V3e:$i] : (mem(V3e,A_27b) => ( ! [V4x:$i] : (mem(V4x,A_27a) => ( ! [V5l:$i] : (mem(V5l,ty_2Elist_2Elist(A_27a)) => (ap(ap(ap(c_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)))))))))))))).
tff(ax_thm_2Elist_2EEVERY__DEF,axiom,( ! [A_27a:del]: (( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => (p(ap(ap(c_2Elist_2EEVERY(A_27a),V0P),c_2Elist_2ENIL(A_27a))) <=> $true))) & ( ! [V1P:$i] : (mem(V1P,arr(A_27a,bool)) => ( ! [V2h:$i] : (mem(V2h,A_27a) => ( ! [V3t:$i] : (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))))))))))))).
tff(ax_thm_2Elist_2EEXISTS__DEF,axiom,( ! [A_27a:del]: (( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => (p(ap(ap(c_2Elist_2EEXISTS(A_27a),V0P),c_2Elist_2ENIL(A_27a))) <=> $false))) & ( ! [V1P:$i] : (mem(V1P,arr(A_27a,bool)) => ( ! [V2h:$i] : (mem(V2h,A_27a) => ( ! [V3t:$i] : (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))))))))))))).
tff(ax_thm_2Elist_2EEL,axiom,( ! [A_27a:del]: (( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => (ap(ap(c_2Elist_2EEL(A_27a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),V0l) = ap(c_2Elist_2EHD(A_27a),V0l)))) & ( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(A_27a)) => ( ! [V2n:tp__ty_2Enum_2Enum] : (ap(ap(c_2Elist_2EEL(A_27a),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V2n))),V1l) = ap(ap(c_2Elist_2EEL(A_27a),inj__ty_2Enum_2Enum(V2n)),ap(c_2Elist_2ETL(A_27a),V1l))))))))).
tff(conj_thm_2Elist_2EMAP2__ind,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0P:$i] : (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:$i] : (mem(V1f,arr(A_27b,arr(A_27c,A_27a))) => ( ! [V2h1:$i] : (mem(V2h1,A_27b) => ( ! [V3t1:$i] : (mem(V3t1,ty_2Elist_2Elist(A_27b)) => ( ! [V4h2:$i] : (mem(V4h2,A_27c) => ( ! [V5t2:$i] : (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:$i] : (mem(V6f,arr(A_27b,arr(A_27c,A_27a))) => ( ! [V7y:$i] : (mem(V7y,ty_2Elist_2Elist(A_27c)) => p(ap(ap(ap(V0P,V6f),c_2Elist_2ENIL(A_27b)),V7y)))))) & ( ! [V8f:$i] : (mem(V8f,arr(A_27b,arr(A_27c,A_27a))) => ( ! [V9v4:$i] : (mem(V9v4,A_27b) => ( ! [V10v5:$i] : (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:$i] : (mem(V11v,arr(A_27b,arr(A_27c,A_27a))) => ( ! [V12v1:$i] : (mem(V12v1,ty_2Elist_2Elist(A_27b)) => ( ! [V13v2:$i] : (mem(V13v2,ty_2Elist_2Elist(A_27c)) => p(ap(ap(ap(V0P,V11v),V12v1),V13v2)))))))))))))))).
tff(conj_thm_2Elist_2EMAP2__DEF,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: (( ! [V0t2:$i] : (mem(V0t2,ty_2Elist_2Elist(A_27c)) => ( ! [V1t1:$i] : (mem(V1t1,ty_2Elist_2Elist(A_27b)) => ( ! [V2h2:$i] : (mem(V2h2,A_27c) => ( ! [V3h1:$i] : (mem(V3h1,A_27b) => ( ! [V4f:$i] : (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:$i] : (mem(V5y,ty_2Elist_2Elist(A_27c)) => ( ! [V6f:$i] : (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:$i] : (mem(V7v5,ty_2Elist_2Elist(A_27b)) => ( ! [V8v4:$i] : (mem(V8v4,A_27b) => ( ! [V9f:$i] : (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))))))))))))))).
tff(conj_thm_2Elist_2EMAP2,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [A_27e:del]: ( ! [A_27f:del]: (( ! [V0f:$i] : (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:$i] : (mem(V1f,arr(A_27d,arr(A_27e,A_27f))) => ( ! [V2h1:$i] : (mem(V2h1,A_27d) => ( ! [V3t1:$i] : (mem(V3t1,ty_2Elist_2Elist(A_27d)) => ( ! [V4h2:$i] : (mem(V4h2,A_27e) => ( ! [V5t2:$i] : (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)))))))))))))))))))))).
tff(conj_thm_2Elist_2EMAP2__NIL,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27b,arr(A_27c,A_27a))) => ( ! [V1x:$i] : (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))))))))))).
tff(conj_thm_2Elist_2ELENGTH__MAP2,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,arr(A_27b,A_27c))) => ( ! [V1xs:$i] : (mem(V1xs,ty_2Elist_2Elist(A_27a)) => ( ! [V2ys:$i] : (mem(V2ys,ty_2Elist_2Elist(A_27b)) => (surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27c),ap(ap(ap(c_2Elist_2EMAP2(A_27c,A_27a,A_27b),V0f),V1xs),V2ys))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMIN,ap(c_2Elist_2ELENGTH(A_27a),V1xs)),ap(c_2Elist_2ELENGTH(A_27b),V2ys))))))))))))))).
tff(conj_thm_2Elist_2EEL__MAP2,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,arr(A_27b,A_27c))) => ( ! [V1ts:$i] : (mem(V1ts,ty_2Elist_2Elist(A_27a)) => ( ! [V2tt:$i] : (mem(V2tt,ty_2Elist_2Elist(A_27b)) => ( ! [V3n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(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),inj__ty_2Enum_2Enum(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),inj__ty_2Enum_2Enum(V3n)),V1ts)),ap(ap(c_2Elist_2EEL(A_27b),inj__ty_2Enum_2Enum(V3n)),V2tt)))))))))))))))).
tff(ax_thm_2Elist_2EINDEX__FIND__def,axiom,( ! [A_27a:del]: (( ! [V0i:tp__ty_2Enum_2Enum] : ( ! [V1P:$i] : (mem(V1P,arr(A_27a,bool)) => (ap(ap(ap(c_2Elist_2EINDEX__FIND(A_27a),inj__ty_2Enum_2Enum(V0i)),V1P),c_2Elist_2ENIL(A_27a)) = c_2Eoption_2ENONE(ty_2Epair_2Eprod(ty_2Enum_2Enum,A_27a)))))) & ( ! [V2i:tp__ty_2Enum_2Enum] : ( ! [V3P:$i] : (mem(V3P,arr(A_27a,bool)) => ( ! [V4h:$i] : (mem(V4h,A_27a) => ( ! [V5t:$i] : (mem(V5t,ty_2Elist_2Elist(A_27a)) => (ap(ap(ap(c_2Elist_2EINDEX__FIND(A_27a),inj__ty_2Enum_2Enum(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),inj__ty_2Enum_2Enum(V2i)),V4h))),ap(ap(ap(c_2Elist_2EINDEX__FIND(A_27a),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V2i))),V3P),V5t))))))))))))).
tff(ax_thm_2Elist_2EFIND__def,axiom,( ! [A_27a:del]: ( ! [V0P:$i] : (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),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),V0P))))))).
tff(ax_thm_2Elist_2EINDEX__OF__def,axiom,( ! [A_27a:del]: ( ! [V0x:$i] : (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),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(c_2Emin_2E_3D(A_27a),V0x)))))))).
tff(conj_thm_2Elist_2ENULL,lemma,(( ! [A_27a:del]: (p(ap(c_2Elist_2ENULL(A_27a),c_2Elist_2ENIL(A_27a))) & ( ! [V0h:$i] : (mem(V0h,A_27a) => ( ! [V1t:$i] : (mem(V1t,ty_2Elist_2Elist(A_27a)) => (~~ p(ap(c_2Elist_2ENULL(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V0h),V1t)))))))))))).
tff(conj_thm_2Elist_2Elist__INDUCT0,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Elist_2Elist(A_27a),bool)) => ((p(ap(V0P,c_2Elist_2ENIL(A_27a))) & ( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(A_27a)) => (p(ap(V0P,V1l)) => ( ! [V2a:$i] : (mem(V2a,A_27a) => p(ap(V0P,ap(ap(c_2Elist_2ECONS(A_27a),V2a),V1l))))))))) => ( ! [V3l:$i] : (mem(V3l,ty_2Elist_2Elist(A_27a)) => p(ap(V0P,V3l)))))))))).
tff(conj_thm_2Elist_2Elist__INDUCT,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Elist_2Elist(A_27a),bool)) => ((p(ap(V0P,c_2Elist_2ENIL(A_27a))) & ( ! [V1t:$i] : (mem(V1t,ty_2Elist_2Elist(A_27a)) => (p(ap(V0P,V1t)) => ( ! [V2h:$i] : (mem(V2h,A_27a) => p(ap(V0P,ap(ap(c_2Elist_2ECONS(A_27a),V2h),V1t))))))))) => ( ! [V3l:$i] : (mem(V3l,ty_2Elist_2Elist(A_27a)) => p(ap(V0P,V3l)))))))))).
tff(conj_thm_2Elist_2Elist__induction,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Elist_2Elist(A_27a),bool)) => ((p(ap(V0P,c_2Elist_2ENIL(A_27a))) & ( ! [V1t:$i] : (mem(V1t,ty_2Elist_2Elist(A_27a)) => (p(ap(V0P,V1t)) => ( ! [V2h:$i] : (mem(V2h,A_27a) => p(ap(V0P,ap(ap(c_2Elist_2ECONS(A_27a),V2h),V1t))))))))) => ( ! [V3l:$i] : (mem(V3l,ty_2Elist_2Elist(A_27a)) => p(ap(V0P,V3l)))))))))).
tff(conj_thm_2Elist_2Elist__CASES,lemma,(( ! [A_27a:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => ((V0l = c_2Elist_2ENIL(A_27a)) | (? [V1h:$i] : (mem(V1h,A_27a) & (? [V2t:$i] : (mem(V2t,ty_2Elist_2Elist(A_27a)) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V1h),V2t)))))))))))).
tff(conj_thm_2Elist_2Elist__nchotomy,lemma,(( ! [A_27a:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => ((V0l = c_2Elist_2ENIL(A_27a)) | (? [V1h:$i] : (mem(V1h,A_27a) & (? [V2t:$i] : (mem(V2t,ty_2Elist_2Elist(A_27a)) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V1h),V2t)))))))))))).
tff(conj_thm_2Elist_2Elist__case__compute,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0b:$i] : (mem(V0b,A_27b) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,arr(ty_2Elist_2Elist(A_27a),A_27b))) => ( ! [V2l:$i] : (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)))))))))))))).
tff(conj_thm_2Elist_2ECONS__11,lemma,(( ! [A_27a:del]: ( ! [V0a0:$i] : (mem(V0a0,A_27a) => ( ! [V1a1:$i] : (mem(V1a1,ty_2Elist_2Elist(A_27a)) => ( ! [V2a0_27:$i] : (mem(V2a0_27,A_27a) => ( ! [V3a1_27:$i] : (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)))))))))))))).
tff(conj_thm_2Elist_2ENOT__NIL__CONS,lemma,(( ! [A_27a:del]: ( ! [V0a1:$i] : (mem(V0a1,ty_2Elist_2Elist(A_27a)) => ( ! [V1a0:$i] : (mem(V1a0,A_27a) => (~~ (c_2Elist_2ENIL(A_27a) = ap(ap(c_2Elist_2ECONS(A_27a),V1a0),V0a1)))))))))).
tff(conj_thm_2Elist_2ENOT__CONS__NIL,lemma,(( ! [A_27a:del]: ( ! [V0a1:$i] : (mem(V0a1,ty_2Elist_2Elist(A_27a)) => ( ! [V1a0:$i] : (mem(V1a0,A_27a) => (~~ (ap(ap(c_2Elist_2ECONS(A_27a),V1a0),V0a1) = c_2Elist_2ENIL(A_27a)))))))))).
tff(conj_thm_2Elist_2ELIST__NOT__EQ,lemma,(( ! [A_27a:del]: ( ! [V0l1:$i] : (mem(V0l1,ty_2Elist_2Elist(A_27a)) => ( ! [V1l2:$i] : (mem(V1l2,ty_2Elist_2Elist(A_27a)) => ((~~ (V0l1 = V1l2)) => ( ! [V2h1:$i] : (mem(V2h1,A_27a) => ( ! [V3h2:$i] : (mem(V3h2,A_27a) => (~~ (ap(ap(c_2Elist_2ECONS(A_27a),V2h1),V0l1) = ap(ap(c_2Elist_2ECONS(A_27a),V3h2),V1l2))))))))))))))).
tff(conj_thm_2Elist_2ENOT__EQ__LIST,lemma,(( ! [A_27a:del]: ( ! [V0h1:$i] : (mem(V0h1,A_27a) => ( ! [V1h2:$i] : (mem(V1h2,A_27a) => ((~~ (V0h1 = V1h2)) => ( ! [V2l1:$i] : (mem(V2l1,ty_2Elist_2Elist(A_27a)) => ( ! [V3l2:$i] : (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))))))))))))))).
tff(conj_thm_2Elist_2EEQ__LIST,lemma,(( ! [A_27a:del]: ( ! [V0h1:$i] : (mem(V0h1,A_27a) => ( ! [V1h2:$i] : (mem(V1h2,A_27a) => ((V0h1 = V1h2) => ( ! [V2l1:$i] : (mem(V2l1,ty_2Elist_2Elist(A_27a)) => ( ! [V3l2:$i] : (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))))))))))))))).
tff(conj_thm_2Elist_2ECONS,lemma,(( ! [A_27a:del]: ( ! [V0l:$i] : (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))))))).
tff(conj_thm_2Elist_2EAPPEND__NIL,lemma,(( ! [A_27a:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => (ap(ap(c_2Elist_2EAPPEND(A_27a),V0l),c_2Elist_2ENIL(A_27a)) = V0l)))))).
tff(conj_thm_2Elist_2EAPPEND__ASSOC,lemma,(( ! [A_27a:del]: ( ! [V0l1:$i] : (mem(V0l1,ty_2Elist_2Elist(A_27a)) => ( ! [V1l2:$i] : (mem(V1l2,ty_2Elist_2Elist(A_27a)) => ( ! [V2l3:$i] : (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))))))))))).
tff(conj_thm_2Elist_2ELENGTH__APPEND,lemma,(( ! [A_27a:del]: ( ! [V0l1:$i] : (mem(V0l1,ty_2Elist_2Elist(A_27a)) => ( ! [V1l2:$i] : (mem(V1l2,ty_2Elist_2Elist(A_27a)) => (surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),ap(ap(c_2Elist_2EAPPEND(A_27a),V0l1),V1l2))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(c_2Elist_2ELENGTH(A_27a),V0l1)),ap(c_2Elist_2ELENGTH(A_27a),V1l2))))))))))).
tff(conj_thm_2Elist_2EMAP__APPEND,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27b)) => ( ! [V1l1:$i] : (mem(V1l1,ty_2Elist_2Elist(A_27a)) => ( ! [V2l2:$i] : (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))))))))))))).
tff(conj_thm_2Elist_2EMAP__ID,lemma,(( ! [A_27a:del]: ( ! [V0l:$i] : (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))))))).
tff(conj_thm_2Elist_2ELENGTH__MAP,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,A_27b)) => (surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27b),ap(ap(c_2Elist_2EMAP(A_27a,A_27b),V1f),V0l))) = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l))))))))))).
tff(conj_thm_2Elist_2EMAP__EQ__NIL,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ! [V1f:$i] : (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)))))))))))).
tff(conj_thm_2Elist_2EMAP__EQ__CONS,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27b)) => ( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(A_27a)) => ( ! [V2h:$i] : (mem(V2h,A_27b) => ( ! [V3t:$i] : (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:$i] : (mem(V4x0,A_27a) & (? [V5t0:$i] : (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))))))))))))))))))))).
tff(conj_thm_2Elist_2EMAP__EQ__SING,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27b)) => ( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(A_27a)) => ( ! [V2x:$i] : (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:$i] : (mem(V3x0,A_27a) & ((V1l = ap(ap(c_2Elist_2ECONS(A_27a),V3x0),c_2Elist_2ENIL(A_27a))) & (V2x = ap(V0f,V3x0)))))))))))))))).
tff(conj_thm_2Elist_2EMAP__EQ__f,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f1:$i] : (mem(V0f1,arr(A_27a,A_27b)) => ( ! [V1f2:$i] : (mem(V1f2,arr(A_27a,A_27b)) => ( ! [V2l:$i] : (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:$i] : (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)))))))))))))))).
tff(conj_thm_2Elist_2EMAP__o,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27b,A_27c)) => ( ! [V1g:$i] : (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)))))))))))).
tff(conj_thm_2Elist_2EMAP__MAP__o,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27b,A_27c)) => ( ! [V1g:$i] : (mem(V1g,arr(A_27a,A_27b)) => ( ! [V2l:$i] : (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))))))))))))).
tff(conj_thm_2Elist_2EEL__MAP,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(A_27a)) => (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0n)),ap(c_2Elist_2ELENGTH(A_27a),V1l))) => ( ! [V2f:$i] : (mem(V2f,arr(A_27a,A_27b)) => (ap(ap(c_2Elist_2EEL(A_27b),inj__ty_2Enum_2Enum(V0n)),ap(ap(c_2Elist_2EMAP(A_27a,A_27b),V2f),V1l)) = ap(V2f,ap(ap(c_2Elist_2EEL(A_27a),inj__ty_2Enum_2Enum(V0n)),V1l))))))))))))).
tff(conj_thm_2Elist_2EEL__APPEND__EQN,lemma,(( ! [A_27a:del]: ( ! [V0l1:$i] : (mem(V0l1,ty_2Elist_2Elist(A_27a)) => ( ! [V1l2:$i] : (mem(V1l2,ty_2Elist_2Elist(A_27a)) => ( ! [V2n:tp__ty_2Enum_2Enum] : (ap(ap(c_2Elist_2EEL(A_27a),inj__ty_2Enum_2Enum(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,inj__ty_2Enum_2Enum(V2n)),ap(c_2Elist_2ELENGTH(A_27a),V0l1))),ap(ap(c_2Elist_2EEL(A_27a),inj__ty_2Enum_2Enum(V2n)),V0l1)),ap(ap(c_2Elist_2EEL(A_27a),ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V2n)),ap(c_2Elist_2ELENGTH(A_27a),V0l1))),V1l2))))))))))).
tff(conj_thm_2Elist_2EMAP__TL,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ! [V1f:$i] : (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)))))))))))).
tff(conj_thm_2Elist_2EEVERY__EL,lemma,(( ! [A_27a:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ! [V1P:$i] : (mem(V1P,arr(A_27a,bool)) => (p(ap(ap(c_2Elist_2EEVERY(A_27a),V1P),V0l)) <=> ( ! [V2n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V2n)),ap(c_2Elist_2ELENGTH(A_27a),V0l))) => p(ap(V1P,ap(ap(c_2Elist_2EEL(A_27a),inj__ty_2Enum_2Enum(V2n)),V0l))))))))))))).
tff(conj_thm_2Elist_2EEVERY__CONJ,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1Q:$i] : (mem(V1Q,arr(A_27a,bool)) => ( ! [V2l:$i] : (mem(V2l,ty_2Elist_2Elist(A_27a)) => (p(ap(ap(c_2Elist_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))))))))))))).
tff(conj_thm_2Elist_2EEVERY__MEM,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(A_27a)) => (p(ap(ap(c_2Elist_2EEVERY(A_27a),V0P),V1l)) <=> ( ! [V2e:$i] : (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))))))))))))).
tff(conj_thm_2Elist_2EEVERY__MAP,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27b,bool)) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,A_27b)) => ( ! [V2l:$i] : (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))))))))))))).
tff(conj_thm_2Elist_2EEVERY__SIMP,lemma,(( ! [A_27a:del]: ( ! [V0c:tp__o] : ( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(A_27a)) => (p(ap(ap(c_2Elist_2EEVERY(A_27a),k(A_27a,inj__o(V0c))),V1l)) <=> ((V1l = c_2Elist_2ENIL(A_27a)) | p(inj__o(V0c)))))))))).
tff(conj_thm_2Elist_2EMONO__EVERY,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1Q:$i] : (mem(V1Q,arr(A_27a,bool)) => ( ! [V2l:$i] : (mem(V2l,ty_2Elist_2Elist(A_27a)) => (( ! [V3x:$i] : (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))))))))))))).
tff(conj_thm_2Elist_2EEXISTS__MEM,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(A_27a)) => (p(ap(ap(c_2Elist_2EEXISTS(A_27a),V0P),V1l)) <=> (? [V2e:$i] : (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))))))))))))).
tff(conj_thm_2Elist_2EEXISTS__MAP,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27b,bool)) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,A_27b)) => ( ! [V2l:$i] : (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))))))))))))).
tff(conj_thm_2Elist_2EEXISTS__SIMP,lemma,(( ! [A_27a:del]: ( ! [V0c:tp__o] : ( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(A_27a)) => (p(ap(ap(c_2Elist_2EEXISTS(A_27a),k(A_27a,inj__o(V0c))),V1l)) <=> ((~~ (V1l = c_2Elist_2ENIL(A_27a))) & p(inj__o(V0c)))))))))).
tff(conj_thm_2Elist_2EMONO__EXISTS,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1Q:$i] : (mem(V1Q,arr(A_27a,bool)) => ( ! [V2l:$i] : (mem(V2l,ty_2Elist_2Elist(A_27a)) => (( ! [V3x:$i] : (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))))))))))))).
tff(conj_thm_2Elist_2EEVERY__NOT__EXISTS,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(A_27a)) => (p(ap(ap(c_2Elist_2EEVERY(A_27a),V0P),V1l)) <=> (~~ p(ap(ap(c_2Elist_2EEXISTS(A_27a),f392(A_27a,V0P)),V1l))))))))))).
tff(conj_thm_2Elist_2EEXISTS__NOT__EVERY,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(A_27a)) => (p(ap(ap(c_2Elist_2EEXISTS(A_27a),V0P),V1l)) <=> (~~ p(ap(ap(c_2Elist_2EEVERY(A_27a),f392(A_27a,V0P)),V1l))))))))))).
tff(conj_thm_2Elist_2EMEM__APPEND,lemma,(( ! [A_27a:del]: ( ! [V0e:$i] : (mem(V0e,A_27a) => ( ! [V1l1:$i] : (mem(V1l1,ty_2Elist_2Elist(A_27a)) => ( ! [V2l2:$i] : (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)))))))))))))).
tff(conj_thm_2Elist_2EMEM__FILTER,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1L:$i] : (mem(V1L,ty_2Elist_2Elist(A_27a)) => ( ! [V2x:$i] : (mem(V2x,A_27a) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),ap(c_2Elist_2ELIST__TO__SET(A_27a),ap(ap(c_2Elist_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)))))))))))))).
tff(conj_thm_2Elist_2EMEM__FLAT,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1L:$i] : (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:$i] : (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)))))))))))))).
tff(conj_thm_2Elist_2EFLAT__APPEND,lemma,(( ! [A_27a:del]: ( ! [V0l1:$i] : (mem(V0l1,ty_2Elist_2Elist(ty_2Elist_2Elist(A_27a))) => ( ! [V1l2:$i] : (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)))))))))).
tff(conj_thm_2Elist_2EFLAT__compute,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0t:$i] : (mem(V0t,ty_2Elist_2Elist(ty_2Elist_2Elist(A_27b))) => ( ! [V1h:$i] : (mem(V1h,A_27c) => ( ! [V2t1:$i] : (mem(V2t1,ty_2Elist_2Elist(A_27c)) => ( ! [V3t2:$i] : (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))))))))))))))))))).
tff(conj_thm_2Elist_2EEVERY__APPEND,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1l1:$i] : (mem(V1l1,ty_2Elist_2Elist(A_27a)) => ( ! [V2l2:$i] : (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))))))))))))).
tff(conj_thm_2Elist_2EEXISTS__APPEND,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1l1:$i] : (mem(V1l1,ty_2Elist_2Elist(A_27a)) => ( ! [V2l2:$i] : (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))))))))))))).
tff(conj_thm_2Elist_2ENOT__EVERY,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(A_27a)) => ((~~ p(ap(ap(c_2Elist_2EEVERY(A_27a),V0P),V1l))) <=> p(ap(ap(c_2Elist_2EEXISTS(A_27a),ap(ap(c_2Ecombin_2Eo(A_27a,bool,bool),c_2Ebool_2E_7E),V0P)),V1l)))))))))).
tff(conj_thm_2Elist_2ENOT__EXISTS,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(A_27a)) => ((~~ p(ap(ap(c_2Elist_2EEXISTS(A_27a),V0P),V1l))) <=> p(ap(ap(c_2Elist_2EEVERY(A_27a),ap(ap(c_2Ecombin_2Eo(A_27a,bool,bool),c_2Ebool_2E_7E),V0P)),V1l)))))))))).
tff(conj_thm_2Elist_2EMEM__MAP,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,A_27b)) => ( ! [V2x:$i] : (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:$i] : (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))))))))))))))))).
tff(conj_thm_2Elist_2ELENGTH__NIL,lemma,(( ! [A_27a:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l)) = fo__c_2Enum_2E0) <=> (V0l = c_2Elist_2ENIL(A_27a)))))))).
tff(conj_thm_2Elist_2ELENGTH__NIL__SYM,lemma,(( ! [A_27a:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => ((fo__c_2Enum_2E0 = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l))) <=> (V0l = c_2Elist_2ENIL(A_27a)))))))).
tff(conj_thm_2Elist_2ENULL__EQ,lemma,(( ! [A_27a:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => (p(ap(c_2Elist_2ENULL(A_27a),V0l)) <=> (V0l = c_2Elist_2ENIL(A_27a)))))))).
tff(conj_thm_2Elist_2ENULL__LENGTH,lemma,(( ! [A_27a:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => (p(ap(c_2Elist_2ENULL(A_27a),V0l)) <=> (surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l)) = fo__c_2Enum_2E0))))))).
tff(conj_thm_2Elist_2ELENGTH__CONS,lemma,(( ! [A_27a:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ! [V1n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l)) = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1n)))) <=> (? [V2h:$i] : (mem(V2h,A_27a) & (? [V3l_27:$i] : (mem(V3l_27,ty_2Elist_2Elist(A_27a)) & ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V3l_27)) = V1n) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V2h),V3l_27)))))))))))))).
tff(conj_thm_2Elist_2ELENGTH__EQ__CONS,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Elist_2Elist(A_27a),bool)) => ( ! [V1n:tp__ty_2Enum_2Enum] : (( ! [V2l:$i] : (mem(V2l,ty_2Elist_2Elist(A_27a)) => ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V2l)) = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1n)))) => p(ap(V0P,V2l))))) <=> ( ! [V3l:$i] : (mem(V3l,ty_2Elist_2Elist(A_27a)) => ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V3l)) = V1n) => p(ap(f394(A_27a,V0P),V3l)))))))))))).
tff(conj_thm_2Elist_2ELENGTH__EQ__SUM,lemma,(( ! [A_27a:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ! [V1n1:tp__ty_2Enum_2Enum] : ( ! [V2n2:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l)) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1n1)),inj__ty_2Enum_2Enum(V2n2)))) <=> (? [V3l1:$i] : (mem(V3l1,ty_2Elist_2Elist(A_27a)) & (? [V4l2:$i] : (mem(V4l2,ty_2Elist_2Elist(A_27a)) & ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V3l1)) = V1n1) & ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V4l2)) = V2n2) & (V0l = ap(ap(c_2Elist_2EAPPEND(A_27a),V3l1),V4l2)))))))))))))))).
tff(conj_thm_2Elist_2ELENGTH__EQ__NUM,lemma,(( ! [A_27a:del]: (( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l)) = fo__c_2Enum_2E0) <=> (V0l = c_2Elist_2ENIL(A_27a))))) & (( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(A_27a)) => ( ! [V2n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V1l)) = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V2n)))) <=> (? [V3h:$i] : (mem(V3h,A_27a) & (? [V4l_27:$i] : (mem(V4l_27,ty_2Elist_2Elist(A_27a)) & ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V4l_27)) = V2n) & (V1l = ap(ap(c_2Elist_2ECONS(A_27a),V3h),V4l_27))))))))))) & ( ! [V5l:$i] : (mem(V5l,ty_2Elist_2Elist(A_27a)) => ( ! [V6n1:tp__ty_2Enum_2Enum] : ( ! [V7n2:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V5l)) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V6n1)),inj__ty_2Enum_2Enum(V7n2)))) <=> (? [V8l1:$i] : (mem(V8l1,ty_2Elist_2Elist(A_27a)) & (? [V9l2:$i] : (mem(V9l2,ty_2Elist_2Elist(A_27a)) & ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V8l1)) = V6n1) & ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V9l2)) = V7n2) & (V5l = ap(ap(c_2Elist_2EAPPEND(A_27a),V8l1),V9l2)))))))))))))))))).
tff(conj_thm_2Elist_2ELENGTH__EQ__NUM__compute,lemma,(( ! [A_27a:del]: (( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l)) = fo__c_2Enum_2E0) <=> (V0l = c_2Elist_2ENIL(A_27a))))) & (( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(A_27a)) => ( ! [V2n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V1l)) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V2n))))) <=> (? [V3h:$i] : (mem(V3h,A_27a) & (? [V4l_27:$i] : (mem(V4l_27,ty_2Elist_2Elist(A_27a)) & ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V4l_27)) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V2n)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))) & (V1l = ap(ap(c_2Elist_2ECONS(A_27a),V3h),V4l_27))))))))))) & (( ! [V5l:$i] : (mem(V5l,ty_2Elist_2Elist(A_27a)) => ( ! [V6n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V5l)) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V6n))))) <=> (? [V7h:$i] : (mem(V7h,A_27a) & (? [V8l_27:$i] : (mem(V8l_27,ty_2Elist_2Elist(A_27a)) & ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V8l_27)) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V6n))))) & (V5l = ap(ap(c_2Elist_2ECONS(A_27a),V7h),V8l_27))))))))))) & ( ! [V9l:$i] : (mem(V9l,ty_2Elist_2Elist(A_27a)) => ( ! [V10n1:tp__ty_2Enum_2Enum] : ( ! [V11n2:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V9l)) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V10n1)),inj__ty_2Enum_2Enum(V11n2)))) <=> (? [V12l1:$i] : (mem(V12l1,ty_2Elist_2Elist(A_27a)) & (? [V13l2:$i] : (mem(V13l2,ty_2Elist_2Elist(A_27a)) & ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V12l1)) = V10n1) & ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V13l2)) = V11n2) & (V9l = ap(ap(c_2Elist_2EAPPEND(A_27a),V12l1),V13l2))))))))))))))))))).
tff(conj_thm_2Elist_2ELENGTH__EQ__NIL,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Elist_2Elist(A_27a),bool)) => (( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(A_27a)) => ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V1l)) = fo__c_2Enum_2E0) => p(ap(V0P,V1l))))) <=> p(ap(V0P,c_2Elist_2ENIL(A_27a))))))))).
tff(conj_thm_2Elist_2ECONS__ACYCLIC,lemma,(( ! [A_27a:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ! [V1x:$i] : (mem(V1x,A_27a) => ((~~ (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V1x),V0l))) & (~~ (ap(ap(c_2Elist_2ECONS(A_27a),V1x),V0l) = V0l)))))))))).
tff(conj_thm_2Elist_2EAPPEND__eq__NIL,lemma,(( ! [A_27a:del]: (( ! [V0l1:$i] : (mem(V0l1,ty_2Elist_2Elist(A_27a)) => ( ! [V1l2:$i] : (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:$i] : (mem(V2l1,ty_2Elist_2Elist(A_27a)) => ( ! [V3l2:$i] : (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)))))))))))).
tff(conj_thm_2Elist_2EMAP__EQ__APPEND,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27b)) => ( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(A_27a)) => ( ! [V2l1:$i] : (mem(V2l1,ty_2Elist_2Elist(A_27b)) => ( ! [V3l2:$i] : (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:$i] : (mem(V4l10,ty_2Elist_2Elist(A_27a)) & (? [V5l20:$i] : (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))))))))))))))))))))).
tff(conj_thm_2Elist_2EAPPEND__EQ__SING,lemma,(( ! [A_27a:del]: ( ! [V0l1:$i] : (mem(V0l1,ty_2Elist_2Elist(A_27a)) => ( ! [V1l2:$i] : (mem(V1l2,ty_2Elist_2Elist(A_27a)) => ( ! [V2e:$i] : (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))))))))))))))).
tff(conj_thm_2Elist_2EAPPEND__11,lemma,(( ! [A_27a:del]: (( ! [V0l1:$i] : (mem(V0l1,ty_2Elist_2Elist(A_27a)) => ( ! [V1l2:$i] : (mem(V1l2,ty_2Elist_2Elist(A_27a)) => ( ! [V2l3:$i] : (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:$i] : (mem(V3l1,ty_2Elist_2Elist(A_27a)) => ( ! [V4l2:$i] : (mem(V4l2,ty_2Elist_2Elist(A_27a)) => ( ! [V5l3:$i] : (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)))))))))))).
tff(conj_thm_2Elist_2EAPPEND__LENGTH__EQ,lemma,(( ! [A_27a:del]: ( ! [V0l1:$i] : (mem(V0l1,ty_2Elist_2Elist(A_27a)) => ( ! [V1l1_27:$i] : (mem(V1l1_27,ty_2Elist_2Elist(A_27a)) => ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l1)) = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V1l1_27))) => ( ! [V2l2:$i] : (mem(V2l2,ty_2Elist_2Elist(A_27a)) => ( ! [V3l2_27:$i] : (mem(V3l2_27,ty_2Elist_2Elist(A_27a)) => ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V2l2)) = surj__ty_2Enum_2Enum(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)))))))))))))))).
tff(conj_thm_2Elist_2EAPPEND__11__LENGTH,lemma,(( ! [A_27a:del]: (( ! [V0l1:$i] : (mem(V0l1,ty_2Elist_2Elist(A_27a)) => ( ! [V1l2:$i] : (mem(V1l2,ty_2Elist_2Elist(A_27a)) => ( ! [V2l1_27:$i] : (mem(V2l1_27,ty_2Elist_2Elist(A_27a)) => ( ! [V3l2_27:$i] : (mem(V3l2_27,ty_2Elist_2Elist(A_27a)) => ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l1)) = surj__ty_2Enum_2Enum(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:$i] : (mem(V4l1,ty_2Elist_2Elist(A_27a)) => ( ! [V5l2:$i] : (mem(V5l2,ty_2Elist_2Elist(A_27a)) => ( ! [V6l1_27:$i] : (mem(V6l1_27,ty_2Elist_2Elist(A_27a)) => ( ! [V7l2_27:$i] : (mem(V7l2_27,ty_2Elist_2Elist(A_27a)) => ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V5l2)) = surj__ty_2Enum_2Enum(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)))))))))))))))).
tff(conj_thm_2Elist_2EAPPEND__EQ__SELF,lemma,(( ! [A_27a:del]: (( ! [V0l1:$i] : (mem(V0l1,ty_2Elist_2Elist(A_27a)) => ( ! [V1l2:$i] : (mem(V1l2,ty_2Elist_2Elist(A_27a)) => ((ap(ap(c_2Elist_2EAPPEND(A_27a),V0l1),V1l2) = V0l1) <=> (V1l2 = c_2Elist_2ENIL(A_27a))))))) & (( ! [V2l1:$i] : (mem(V2l1,ty_2Elist_2Elist(A_27a)) => ( ! [V3l2:$i] : (mem(V3l2,ty_2Elist_2Elist(A_27a)) => ((ap(ap(c_2Elist_2EAPPEND(A_27a),V2l1),V3l2) = V3l2) <=> (V2l1 = c_2Elist_2ENIL(A_27a))))))) & (( ! [V4l1:$i] : (mem(V4l1,ty_2Elist_2Elist(A_27a)) => ( ! [V5l2:$i] : (mem(V5l2,ty_2Elist_2Elist(A_27a)) => ((V4l1 = ap(ap(c_2Elist_2EAPPEND(A_27a),V4l1),V5l2)) <=> (V5l2 = c_2Elist_2ENIL(A_27a))))))) & ( ! [V6l1:$i] : (mem(V6l1,ty_2Elist_2Elist(A_27a)) => ( ! [V7l2:$i] : (mem(V7l2,ty_2Elist_2Elist(A_27a)) => ((V7l2 = ap(ap(c_2Elist_2EAPPEND(A_27a),V6l1),V7l2)) <=> (V6l1 = c_2Elist_2ENIL(A_27a))))))))))))).
tff(conj_thm_2Elist_2EMEM__SPLIT,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(A_27a)) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V0x),ap(c_2Elist_2ELIST__TO__SET(A_27a),V1l))) <=> (? [V2l1:$i] : (mem(V2l1,ty_2Elist_2Elist(A_27a)) & (? [V3l2:$i] : (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))))))))))))))).
tff(conj_thm_2Elist_2ELIST__EQ__REWRITE,lemma,(( ! [A_27a:del]: ( ! [V0l1:$i] : (mem(V0l1,ty_2Elist_2Elist(A_27a)) => ( ! [V1l2:$i] : (mem(V1l2,ty_2Elist_2Elist(A_27a)) => ((V0l1 = V1l2) <=> ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l1)) = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V1l2))) & ( ! [V2x:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V2x)),ap(c_2Elist_2ELENGTH(A_27a),V0l1))) => (ap(ap(c_2Elist_2EEL(A_27a),inj__ty_2Enum_2Enum(V2x)),V0l1) = ap(ap(c_2Elist_2EEL(A_27a),inj__ty_2Enum_2Enum(V2x)),V1l2))))))))))))).
tff(conj_thm_2Elist_2ELIST__EQ,lemma,(( ! [A_27a:del]: ( ! [V0l1:$i] : (mem(V0l1,ty_2Elist_2Elist(A_27a)) => ( ! [V1l2:$i] : (mem(V1l2,ty_2Elist_2Elist(A_27a)) => (((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l1)) = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V1l2))) & ( ! [V2x:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V2x)),ap(c_2Elist_2ELENGTH(A_27a),V0l1))) => (ap(ap(c_2Elist_2EEL(A_27a),inj__ty_2Enum_2Enum(V2x)),V0l1) = ap(ap(c_2Elist_2EEL(A_27a),inj__ty_2Enum_2Enum(V2x)),V1l2))))) => (V0l1 = V1l2))))))))).
tff(conj_thm_2Elist_2EFOLDL__EQ__FOLDR,lemma,(( ! [A_27a:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,arr(A_27a,A_27a))) => ( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(A_27a)) => ( ! [V2e:$i] : (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)))))))))))).
tff(conj_thm_2Elist_2EFOLDR__CONS,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27b)) => ( ! [V1ls:$i] : (mem(V1ls,ty_2Elist_2Elist(A_27a)) => ( ! [V2a:$i] : (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)))))))))))).
tff(conj_thm_2Elist_2ELENGTH__TL,lemma,(( ! [A_27a:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(c_2Elist_2ELENGTH(A_27a),V0l))) => (surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),ap(c_2Elist_2ETL(A_27a),V0l))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,ap(c_2Elist_2ELENGTH(A_27a),V0l)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))).
tff(conj_thm_2Elist_2EFILTER__EQ__NIL,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(A_27a)) => ((ap(ap(c_2Elist_2EFILTER(A_27a),V0P),V1l) = c_2Elist_2ENIL(A_27a)) <=> p(ap(ap(c_2Elist_2EEVERY(A_27a),f392(A_27a,V0P)),V1l)))))))))).
tff(conj_thm_2Elist_2EFILTER__NEQ__NIL,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(A_27a)) => ((~~ (ap(ap(c_2Elist_2EFILTER(A_27a),V0P),V1l) = c_2Elist_2ENIL(A_27a))) <=> (? [V2x:$i] : (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))))))))))))).
tff(conj_thm_2Elist_2EFILTER__EQ__ID,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(A_27a)) => ((ap(ap(c_2Elist_2EFILTER(A_27a),V0P),V1l) = V1l) <=> p(ap(ap(c_2Elist_2EEVERY(A_27a),V0P),V1l)))))))))).
tff(conj_thm_2Elist_2EFILTER__NEQ__ID,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(A_27a)) => ((~~ (ap(ap(c_2Elist_2EFILTER(A_27a),V0P),V1l) = V1l)) <=> (? [V2x:$i] : (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)))))))))))))).
tff(conj_thm_2Elist_2EFILTER__EQ__CONS,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(A_27a)) => ( ! [V2h:$i] : (mem(V2h,A_27a) => ( ! [V3lr:$i] : (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:$i] : (mem(V4l1,ty_2Elist_2Elist(A_27a)) & (? [V5l2:$i] : (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))))))))))))))))))))).
tff(conj_thm_2Elist_2EFILTER__APPEND__DISTRIB,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1L:$i] : (mem(V1L,ty_2Elist_2Elist(A_27a)) => ( ! [V2M:$i] : (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)))))))))))).
tff(conj_thm_2Elist_2EMEM,lemma,(( ! [A_27a:del]: (( ! [V0x:$i] : (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:$i] : (mem(V1x,A_27a) => ( ! [V2h:$i] : (mem(V2h,A_27a) => ( ! [V3t:$i] : (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))))))))))))))).
tff(conj_thm_2Elist_2EFILTER__EQ__APPEND,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(A_27a)) => ( ! [V2l1:$i] : (mem(V2l1,ty_2Elist_2Elist(A_27a)) => ( ! [V3l2:$i] : (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:$i] : (mem(V4l3,ty_2Elist_2Elist(A_27a)) & (? [V5l4:$i] : (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))))))))))))))))))).
tff(conj_thm_2Elist_2EEVERY__FILTER,lemma,(( ! [A_27a:del]: ( ! [V0P1:$i] : (mem(V0P1,arr(A_27a,bool)) => ( ! [V1P2:$i] : (mem(V1P2,arr(A_27a,bool)) => ( ! [V2l:$i] : (mem(V2l,ty_2Elist_2Elist(A_27a)) => (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)))))))))))).
tff(conj_thm_2Elist_2EEVERY__FILTER__IMP,lemma,(( ! [A_27a:del]: ( ! [V0P1:$i] : (mem(V0P1,arr(A_27a,bool)) => ( ! [V1P2:$i] : (mem(V1P2,arr(A_27a,bool)) => ( ! [V2l:$i] : (mem(V2l,ty_2Elist_2Elist(A_27a)) => (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))))))))))))).
tff(conj_thm_2Elist_2EFILTER__COND__REWRITE,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(A_27a)) => ((ap(ap(c_2Elist_2EFILTER(A_27a),V0P),c_2Elist_2ENIL(A_27a)) = c_2Elist_2ENIL(A_27a)) & (( ! [V2h:$i] : (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:$i] : (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)))))))))))))).
tff(conj_thm_2Elist_2ENOT__NULL__MEM,lemma,(( ! [A_27a:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => ((~~ p(ap(c_2Elist_2ENULL(A_27a),V0l))) <=> (? [V1e:$i] : (mem(V1e,A_27a) & p(ap(ap(c_2Ebool_2EIN(A_27a),V1e),ap(c_2Elist_2ELIST__TO__SET(A_27a),V0l))))))))))).
tff(conj_thm_2Elist_2EEL__compute,lemma,(( ! [A_27a:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ! [V1n:tp__ty_2Enum_2Enum] : (ap(ap(c_2Elist_2EEL(A_27a),inj__ty_2Enum_2Enum(V1n)),V0l) = ap(ap(ap(c_2Ebool_2ECOND(A_27a),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(c_2Elist_2EHD(A_27a),V0l)),ap(ap(c_2Elist_2EEL(A_27a),ap(c_2Eprim__rec_2EPRE,inj__ty_2Enum_2Enum(V1n))),ap(c_2Elist_2ETL(A_27a),V0l)))))))))).
tff(conj_thm_2Elist_2EEL__simp,lemma,(( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(A_27a)) => ((ap(ap(c_2Elist_2EEL(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n)))),V1l) = ap(ap(c_2Elist_2EEL(A_27a),ap(c_2Eprim__rec_2EPRE,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))))),ap(c_2Elist_2ETL(A_27a),V1l))) & (ap(ap(c_2Elist_2EEL(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n)))),V1l) = ap(ap(c_2Elist_2EEL(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n)))),ap(c_2Elist_2ETL(A_27a),V1l)))))))))).
tff(conj_thm_2Elist_2EEL__restricted,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : (mem(V1l,A_27b) => ( ! [V2ls:$i] : (mem(V2ls,ty_2Elist_2Elist(A_27b)) => ((ap(c_2Elist_2EEL(A_27a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)) = c_2Elist_2EHD(A_27a)) & (ap(ap(c_2Elist_2EEL(A_27b),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),ap(ap(c_2Elist_2ECONS(A_27b),V1l),V2ls)) = ap(ap(c_2Elist_2EEL(A_27b),inj__ty_2Enum_2Enum(V0n)),V2ls)))))))))))).
tff(conj_thm_2Elist_2EEL__simp__restricted,lemma,(( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : (mem(V1l,A_27a) => ( ! [V2ls:$i] : (mem(V2ls,ty_2Elist_2Elist(A_27a)) => ((ap(ap(c_2Elist_2EEL(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(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,inj__ty_2Enum_2Enum(V0n))))),V2ls)) & (ap(ap(c_2Elist_2EEL(A_27a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(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,inj__ty_2Enum_2Enum(V0n)))),V2ls))))))))))).
tff(conj_thm_2Elist_2ESUM__eq__0,lemma,(( ! [V0ls:tp__c_ty_2Elist_2Elist_ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ESUM,inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum(V0ls))) = fo__c_2Enum_2E0) <=> ( ! [V1x:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V1x)),ap(c_2Elist_2ELIST__TO__SET(ty_2Enum_2Enum),inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum(V0ls)))) => (V1x = fo__c_2Enum_2E0))))))).
tff(conj_thm_2Elist_2ENULL__FILTER,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1ls:$i] : (mem(V1ls,ty_2Elist_2Elist(A_27a)) => (p(ap(c_2Elist_2ENULL(A_27a),ap(ap(c_2Elist_2EFILTER(A_27a),V0P),V1ls))) <=> ( ! [V2x:$i] : (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)))))))))))))).
tff(conj_thm_2Elist_2EWF__LIST__PRED,lemma,(( ! [A_27a:del]: p(ap(c_2Erelation_2EWF(ty_2Elist_2Elist(A_27a)),f400(A_27a)))))).
tff(conj_thm_2Elist_2ELIST__REL__rules,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R:$i] : (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:$i] : (mem(V1h1,A_27a) => ( ! [V2h2:$i] : (mem(V2h2,A_27b) => ( ! [V3t1:$i] : (mem(V3t1,ty_2Elist_2Elist(A_27a)) => ( ! [V4t2:$i] : (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))))))))))))))))))).
tff(conj_thm_2Elist_2ELIST__REL__ind,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R:$i] : (mem(V0R,arr(A_27a,arr(A_27b,bool))) => ( ! [V1LIST__REL_27:$i] : (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:$i] : (mem(V2h1,A_27a) => ( ! [V3h2:$i] : (mem(V3h2,A_27b) => ( ! [V4t1:$i] : (mem(V4t1,ty_2Elist_2Elist(A_27a)) => ( ! [V5t2:$i] : (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:$i] : (mem(V6a0,ty_2Elist_2Elist(A_27a)) => ( ! [V7a1:$i] : (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)))))))))))))))).
tff(conj_thm_2Elist_2ELIST__REL__strongind,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R:$i] : (mem(V0R,arr(A_27a,arr(A_27b,bool))) => ( ! [V1LIST__REL_27:$i] : (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:$i] : (mem(V2h1,A_27a) => ( ! [V3h2:$i] : (mem(V3h2,A_27b) => ( ! [V4t1:$i] : (mem(V4t1,ty_2Elist_2Elist(A_27a)) => ( ! [V5t2:$i] : (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:$i] : (mem(V6a0,ty_2Elist_2Elist(A_27a)) => ( ! [V7a1:$i] : (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)))))))))))))))).
tff(conj_thm_2Elist_2ELIST__REL__cases,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R:$i] : (mem(V0R,arr(A_27a,arr(A_27b,bool))) => ( ! [V1a0:$i] : (mem(V1a0,ty_2Elist_2Elist(A_27a)) => ( ! [V2a1:$i] : (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:$i] : (mem(V3h1,A_27a) & (? [V4h2:$i] : (mem(V4h2,A_27b) & (? [V5t1:$i] : (mem(V5t1,ty_2Elist_2Elist(A_27a)) & (? [V6t2:$i] : (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))))))))))))))))))))))))).
tff(conj_thm_2Elist_2ELIST__REL__EL__EQN,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R:$i] : (mem(V0R,arr(A_27a,arr(A_27b,bool))) => ( ! [V1l1:$i] : (mem(V1l1,ty_2Elist_2Elist(A_27a)) => ( ! [V2l2:$i] : (mem(V2l2,ty_2Elist_2Elist(A_27b)) => (p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27b),V0R),V1l1),V2l2)) <=> ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V1l1)) = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27b),V2l2))) & ( ! [V3n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V3n)),ap(c_2Elist_2ELENGTH(A_27a),V1l1))) => p(ap(ap(V0R,ap(ap(c_2Elist_2EEL(A_27a),inj__ty_2Enum_2Enum(V3n)),V1l1)),ap(ap(c_2Elist_2EEL(A_27b),inj__ty_2Enum_2Enum(V3n)),V2l2))))))))))))))))).
tff(conj_thm_2Elist_2ELIST__REL__def,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R:$i] : (mem(V0R,arr(A_27a,arr(A_27b,bool))) => ( ! [V1a:$i] : (mem(V1a,A_27a) => ( ! [V2as:$i] : (mem(V2as,ty_2Elist_2Elist(A_27a)) => ( ! [V3b:$i] : (mem(V3b,A_27b) => ( ! [V4bs:$i] : (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))))))))))))))))))))).
tff(conj_thm_2Elist_2ELIST__REL__mono,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R1:$i] : (mem(V0R1,arr(A_27a,arr(A_27b,bool))) => ( ! [V1R2:$i] : (mem(V1R2,arr(A_27a,arr(A_27b,bool))) => ( ! [V2l1:$i] : (mem(V2l1,ty_2Elist_2Elist(A_27a)) => ( ! [V3l2:$i] : (mem(V3l2,ty_2Elist_2Elist(A_27b)) => (( ! [V4x:$i] : (mem(V4x,A_27a) => ( ! [V5y:$i] : (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)))))))))))))))).
tff(conj_thm_2Elist_2ELIST__REL__NIL,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R:$i] : (mem(V0R,arr(A_27a,arr(A_27b,bool))) => ( ! [V1y:$i] : (mem(V1y,ty_2Elist_2Elist(A_27b)) => ( ! [V2x:$i] : (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)))))))))))))).
tff(conj_thm_2Elist_2ELIST__REL__CONS1,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R:$i] : (mem(V0R,arr(A_27a,arr(A_27b,bool))) => ( ! [V1h:$i] : (mem(V1h,A_27a) => ( ! [V2t:$i] : (mem(V2t,ty_2Elist_2Elist(A_27a)) => ( ! [V3xs:$i] : (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:$i] : (mem(V4h_27,A_27b) & (? [V5t_27:$i] : (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))))))))))))))))))))).
tff(conj_thm_2Elist_2ELIST__REL__CONS2,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R:$i] : (mem(V0R,arr(A_27a,arr(A_27b,bool))) => ( ! [V1xs:$i] : (mem(V1xs,ty_2Elist_2Elist(A_27a)) => ( ! [V2h:$i] : (mem(V2h,A_27b) => ( ! [V3t:$i] : (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:$i] : (mem(V4h_27,A_27a) & (? [V5t_27:$i] : (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))))))))))))))))))))).
tff(conj_thm_2Elist_2ELIST__REL__CONJ,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,arr(A_27b,bool))) => ( ! [V1Q:$i] : (mem(V1Q,arr(A_27a,arr(A_27b,bool))) => ( ! [V2l1:$i] : (mem(V2l1,ty_2Elist_2Elist(A_27a)) => ( ! [V3l2:$i] : (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)))))))))))))))).
tff(conj_thm_2Elist_2ELIST__REL__MAP1,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0R:$i] : (mem(V0R,arr(A_27a,arr(A_27b,bool))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27c,A_27a)) => ( ! [V2l1:$i] : (mem(V2l1,ty_2Elist_2Elist(A_27c)) => ( ! [V3l2:$i] : (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)))))))))))))))).
tff(conj_thm_2Elist_2ELIST__REL__MAP2,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0R:$i] : (mem(V0R,arr(A_27a,arr(A_27b,bool))) => ( ! [V1l1:$i] : (mem(V1l1,ty_2Elist_2Elist(A_27a)) => ( ! [V2f:$i] : (mem(V2f,arr(A_27c,A_27b)) => ( ! [V3l2:$i] : (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)))))))))))))))).
tff(conj_thm_2Elist_2ELIST__REL__LENGTH,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R:$i] : (mem(V0R,arr(A_27a,arr(A_27b,bool))) => ( ! [V1x:$i] : (mem(V1x,ty_2Elist_2Elist(A_27a)) => ( ! [V2y:$i] : (mem(V2y,ty_2Elist_2Elist(A_27b)) => (p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27b),V0R),V1x),V2y)) => (surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V1x)) = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27b),V2y)))))))))))))).
tff(conj_thm_2Elist_2ELIST__REL__SPLIT1,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,arr(A_27b,bool))) => ( ! [V1xs2:$i] : (mem(V1xs2,ty_2Elist_2Elist(A_27a)) => ( ! [V2xs1:$i] : (mem(V2xs1,ty_2Elist_2Elist(A_27a)) => ( ! [V3zs:$i] : (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:$i] : (mem(V4ys1,ty_2Elist_2Elist(A_27b)) & (? [V5ys2:$i] : (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))))))))))))))))))))).
tff(conj_thm_2Elist_2ELIST__REL__SPLIT2,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27b,arr(A_27a,bool))) => ( ! [V1xs2:$i] : (mem(V1xs2,ty_2Elist_2Elist(A_27a)) => ( ! [V2xs1:$i] : (mem(V2xs1,ty_2Elist_2Elist(A_27a)) => ( ! [V3zs:$i] : (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:$i] : (mem(V4ys1,ty_2Elist_2Elist(A_27b)) & (? [V5ys2:$i] : (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))))))))))))))))))))).
tff(conj_thm_2Elist_2Elist__size__cong,lemma,(( ! [A_27a:del]: ( ! [V0M:$i] : (mem(V0M,ty_2Elist_2Elist(A_27a)) => ( ! [V1N:$i] : (mem(V1N,ty_2Elist_2Elist(A_27a)) => ( ! [V2f:$i] : (mem(V2f,arr(A_27a,ty_2Enum_2Enum)) => ( ! [V3f_27:$i] : (mem(V3f_27,arr(A_27a,ty_2Enum_2Enum)) => (((V0M = V1N) & ( ! [V4x:$i] : (mem(V4x,A_27a) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V4x),ap(c_2Elist_2ELIST__TO__SET(A_27a),V1N))) => (surj__ty_2Enum_2Enum(ap(V2f,V4x)) = surj__ty_2Enum_2Enum(ap(V3f_27,V4x))))))) => (surj__ty_2Enum_2Enum(ap(ap(c_2Elist_2Elist__size(A_27a),V2f),V0M)) = surj__ty_2Enum_2Enum(ap(ap(c_2Elist_2Elist__size(A_27a),V3f_27),V1N))))))))))))))).
tff(conj_thm_2Elist_2EFOLDR__CONG,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ! [V1l_27:$i] : (mem(V1l_27,ty_2Elist_2Elist(A_27a)) => ( ! [V2b:$i] : (mem(V2b,A_27b) => ( ! [V3b_27:$i] : (mem(V3b_27,A_27b) => ( ! [V4f:$i] : (mem(V4f,arr(A_27a,arr(A_27b,A_27b))) => ( ! [V5f_27:$i] : (mem(V5f_27,arr(A_27a,arr(A_27b,A_27b))) => (((V0l = V1l_27) & ((V2b = V3b_27) & ( ! [V6x:$i] : (mem(V6x,A_27a) => ( ! [V7a:$i] : (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))))))))))))))))))).
tff(conj_thm_2Elist_2EFOLDL__CONG,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ! [V1l_27:$i] : (mem(V1l_27,ty_2Elist_2Elist(A_27a)) => ( ! [V2b:$i] : (mem(V2b,A_27b) => ( ! [V3b_27:$i] : (mem(V3b_27,A_27b) => ( ! [V4f:$i] : (mem(V4f,arr(A_27b,arr(A_27a,A_27b))) => ( ! [V5f_27:$i] : (mem(V5f_27,arr(A_27b,arr(A_27a,A_27b))) => (((V0l = V1l_27) & ((V2b = V3b_27) & ( ! [V6x:$i] : (mem(V6x,A_27a) => ( ! [V7a:$i] : (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))))))))))))))))))).
tff(conj_thm_2Elist_2EMAP__CONG,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0l1:$i] : (mem(V0l1,ty_2Elist_2Elist(A_27a)) => ( ! [V1l2:$i] : (mem(V1l2,ty_2Elist_2Elist(A_27a)) => ( ! [V2f:$i] : (mem(V2f,arr(A_27a,A_27b)) => ( ! [V3f_27:$i] : (mem(V3f_27,arr(A_27a,A_27b)) => (((V0l1 = V1l2) & ( ! [V4x:$i] : (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))))))))))))))).
tff(conj_thm_2Elist_2EMAP2__CONG,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0l1:$i] : (mem(V0l1,ty_2Elist_2Elist(A_27a)) => ( ! [V1l1_27:$i] : (mem(V1l1_27,ty_2Elist_2Elist(A_27a)) => ( ! [V2l2:$i] : (mem(V2l2,ty_2Elist_2Elist(A_27b)) => ( ! [V3l2_27:$i] : (mem(V3l2_27,ty_2Elist_2Elist(A_27b)) => ( ! [V4f:$i] : (mem(V4f,arr(A_27a,arr(A_27b,A_27c))) => ( ! [V5f_27:$i] : (mem(V5f_27,arr(A_27a,arr(A_27b,A_27c))) => (((V0l1 = V1l1_27) & ((V2l2 = V3l2_27) & ( ! [V6x:$i] : (mem(V6x,A_27a) => ( ! [V7y:$i] : (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)))))))))))))))))))).
tff(conj_thm_2Elist_2EEXISTS__CONG,lemma,(( ! [A_27a:del]: ( ! [V0l1:$i] : (mem(V0l1,ty_2Elist_2Elist(A_27a)) => ( ! [V1l2:$i] : (mem(V1l2,ty_2Elist_2Elist(A_27a)) => ( ! [V2P:$i] : (mem(V2P,arr(A_27a,bool)) => ( ! [V3P_27:$i] : (mem(V3P_27,arr(A_27a,bool)) => (((V0l1 = V1l2) & ( ! [V4x:$i] : (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))))))))))))))).
tff(conj_thm_2Elist_2EEVERY__CONG,lemma,(( ! [A_27a:del]: ( ! [V0l1:$i] : (mem(V0l1,ty_2Elist_2Elist(A_27a)) => ( ! [V1l2:$i] : (mem(V1l2,ty_2Elist_2Elist(A_27a)) => ( ! [V2P:$i] : (mem(V2P,arr(A_27a,bool)) => ( ! [V3P_27:$i] : (mem(V3P_27,arr(A_27a,bool)) => (((V0l1 = V1l2) & ( ! [V4x:$i] : (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))))))))))))))).
tff(conj_thm_2Elist_2EEVERY__MONOTONIC,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1Q:$i] : (mem(V1Q,arr(A_27a,bool)) => (( ! [V2x:$i] : (mem(V2x,A_27a) => (p(ap(V0P,V2x)) => p(ap(V1Q,V2x))))) => ( ! [V3l:$i] : (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))))))))))))).
tff(ax_thm_2Elist_2EZIP__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0l2:$i] : (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:$i] : (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:$i] : (mem(V2x1,A_27a) => ( ! [V3l1:$i] : (mem(V3l1,ty_2Elist_2Elist(A_27a)) => ( ! [V4x2:$i] : (mem(V4x2,A_27b) => ( ! [V5l2:$i] : (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))))))))))))))))).
tff(conj_thm_2Elist_2EZIP,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ((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:$i] : (mem(V0x1,A_27a) => ( ! [V1l1:$i] : (mem(V1l1,ty_2Elist_2Elist(A_27a)) => ( ! [V2x2:$i] : (mem(V2x2,A_27b) => ( ! [V3l2:$i] : (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))))))))))))))))))).
tff(ax_thm_2Elist_2EUNZIP,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ((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:$i] : (mem(V0x,ty_2Epair_2Eprod(A_27a,A_27b)) => ( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => (ap(c_2Elist_2EUNZIP(A_27a,A_27b),ap(ap(c_2Elist_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))))))))))))).
tff(conj_thm_2Elist_2EUNZIP__THM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1y:$i] : (mem(V1y,A_27b) => ( ! [V2t:$i] : (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)))))))))))))).
tff(conj_thm_2Elist_2EUNZIP__MAP,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0L:$i] : (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))))))))).
tff(conj_thm_2Elist_2ELENGTH__ZIP,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0l1:$i] : (mem(V0l1,ty_2Elist_2Elist(A_27a)) => ( ! [V1l2:$i] : (mem(V1l2,ty_2Elist_2Elist(A_27b)) => ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l1)) = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27b),V1l2))) => ((surj__ty_2Enum_2Enum(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)))) = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l1))) & (surj__ty_2Enum_2Enum(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)))) = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27b),V1l2))))))))))))).
tff(conj_thm_2Elist_2ELENGTH__UNZIP,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0pl:$i] : (mem(V0pl,ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27a,A_27b))) => ((surj__ty_2Enum_2Enum(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)))) = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(ty_2Epair_2Eprod(A_27a,A_27b)),V0pl))) & (surj__ty_2Enum_2Enum(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)))) = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(ty_2Epair_2Eprod(A_27a,A_27b)),V0pl)))))))))).
tff(conj_thm_2Elist_2EZIP__UNZIP,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0l:$i] : (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))))))).
tff(conj_thm_2Elist_2EUNZIP__ZIP,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0l1:$i] : (mem(V0l1,ty_2Elist_2Elist(A_27a)) => ( ! [V1l2:$i] : (mem(V1l2,ty_2Elist_2Elist(A_27b)) => ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l1)) = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27b),V1l2))) => (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))))))))))).
tff(conj_thm_2Elist_2EZIP__MAP,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [V0l1:$i] : (mem(V0l1,ty_2Elist_2Elist(A_27a)) => ( ! [V1l2:$i] : (mem(V1l2,ty_2Elist_2Elist(A_27b)) => ( ! [V2f1:$i] : (mem(V2f1,arr(A_27a,A_27c)) => ( ! [V3f2:$i] : (mem(V3f2,arr(A_27b,A_27d)) => ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l1)) = surj__ty_2Enum_2Enum(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)))))))))))))))))))).
tff(conj_thm_2Elist_2EMEM__ZIP,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0l1:$i] : (mem(V0l1,ty_2Elist_2Elist(A_27a)) => ( ! [V1l2:$i] : (mem(V1l2,ty_2Elist_2Elist(A_27b)) => ( ! [V2p:$i] : (mem(V2p,ty_2Epair_2Eprod(A_27a,A_27b)) => ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l1)) = surj__ty_2Enum_2Enum(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:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(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),inj__ty_2Enum_2Enum(V3n)),V0l1)),ap(ap(c_2Elist_2EEL(A_27b),inj__ty_2Enum_2Enum(V3n)),V1l2))))))))))))))))).
tff(conj_thm_2Elist_2EEL__ZIP,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0l1:$i] : (mem(V0l1,ty_2Elist_2Elist(A_27a)) => ( ! [V1l2:$i] : (mem(V1l2,ty_2Elist_2Elist(A_27b)) => ( ! [V2n:tp__ty_2Enum_2Enum] : (((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l1)) = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27b),V1l2))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V2n)),ap(c_2Elist_2ELENGTH(A_27a),V0l1)))) => (ap(ap(c_2Elist_2EEL(ty_2Epair_2Eprod(A_27a,A_27b)),inj__ty_2Enum_2Enum(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),inj__ty_2Enum_2Enum(V2n)),V0l1)),ap(ap(c_2Elist_2EEL(A_27b),inj__ty_2Enum_2Enum(V2n)),V1l2))))))))))))).
tff(conj_thm_2Elist_2EMAP2__ZIP,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0l1:$i] : (mem(V0l1,ty_2Elist_2Elist(A_27a)) => ( ! [V1l2:$i] : (mem(V1l2,ty_2Elist_2Elist(A_27b)) => ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l1)) = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27b),V1l2))) => ( ! [V2f:$i] : (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)))))))))))))))).
tff(conj_thm_2Elist_2EMAP2__MAP,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0l1:$i] : (mem(V0l1,ty_2Elist_2Elist(A_27a)) => ( ! [V1l2:$i] : (mem(V1l2,ty_2Elist_2Elist(A_27b)) => ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l1)) = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27b),V1l2))) => ( ! [V2f:$i] : (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)))))))))))))))).
tff(conj_thm_2Elist_2EMAP__ZIP,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [V0l1:$i] : (mem(V0l1,ty_2Elist_2Elist(A_27a)) => ( ! [V1l2:$i] : (mem(V1l2,ty_2Elist_2Elist(A_27b)) => ( ! [V2f:$i] : (mem(V2f,arr(A_27a,A_27c)) => ( ! [V3g:$i] : (mem(V3g,arr(A_27b,A_27d)) => ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l1)) = surj__ty_2Enum_2Enum(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)))))))))))))))))))).
tff(conj_thm_2Elist_2EMEM__EL,lemma,(( ! [A_27a:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ! [V1x:$i] : (mem(V1x,A_27a) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V1x),ap(c_2Elist_2ELIST__TO__SET(A_27a),V0l))) <=> (? [V2n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V2n)),ap(c_2Elist_2ELENGTH(A_27a),V0l))) & (V1x = ap(ap(c_2Elist_2EEL(A_27a),inj__ty_2Enum_2Enum(V2n)),V0l)))))))))))).
tff(conj_thm_2Elist_2ESUM__MAP__PLUS__ZIP,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,arr(ty_2Epair_2Eprod(A_27a,A_27b),ty_2Enum_2Enum)) => ( ! [V1g:$i] : (mem(V1g,arr(A_27a,ty_2Enum_2Enum)) => ( ! [V2h:$i] : (mem(V2h,arr(A_27b,ty_2Enum_2Enum)) => ( ! [V3ls1:$i] : (mem(V3ls1,ty_2Elist_2Elist(A_27a)) => ( ! [V4ls2:$i] : (mem(V4ls2,ty_2Elist_2Elist(A_27b)) => (((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V3ls1)) = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27b),V4ls2))) & ( ! [V5x:$i] : (mem(V5x,A_27a) => ( ! [V6y:$i] : (mem(V6y,A_27b) => (surj__ty_2Enum_2Enum(ap(V0f,ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V5x),V6y))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(V1g,V5x)),ap(V2h,V6y))))))))) => (surj__ty_2Enum_2Enum(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))))) = surj__ty_2Enum_2Enum(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)))))))))))))))))))).
tff(conj_thm_2Elist_2ELIST__REL__EVERY__ZIP,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R:$i] : (mem(V0R,arr(A_27a,arr(A_27b,bool))) => ( ! [V1l1:$i] : (mem(V1l1,ty_2Elist_2Elist(A_27a)) => ( ! [V2l2:$i] : (mem(V2l2,ty_2Elist_2Elist(A_27b)) => (p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27b),V0R),V1l1),V2l2)) <=> ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V1l1)) = surj__ty_2Enum_2Enum(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)))))))))))))))).
tff(ax_thm_2Elist_2EREVERSE__DEF,axiom,( ! [A_27a:del]: ((ap(c_2Elist_2EREVERSE(A_27a),c_2Elist_2ENIL(A_27a)) = c_2Elist_2ENIL(A_27a)) & ( ! [V0h:$i] : (mem(V0h,A_27a) => ( ! [V1t:$i] : (mem(V1t,ty_2Elist_2Elist(A_27a)) => (ap(c_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))))))))))).
tff(conj_thm_2Elist_2EREVERSE__APPEND,lemma,(( ! [A_27a:del]: ( ! [V0l1:$i] : (mem(V0l1,ty_2Elist_2Elist(A_27a)) => ( ! [V1l2:$i] : (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)))))))))).
tff(conj_thm_2Elist_2EREVERSE__REVERSE,lemma,(( ! [A_27a:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => (ap(c_2Elist_2EREVERSE(A_27a),ap(c_2Elist_2EREVERSE(A_27a),V0l)) = V0l)))))).
tff(conj_thm_2Elist_2EREVERSE__11,lemma,(( ! [A_27a:del]: ( ! [V0l1:$i] : (mem(V0l1,ty_2Elist_2Elist(A_27a)) => ( ! [V1l2:$i] : (mem(V1l2,ty_2Elist_2Elist(A_27a)) => ((ap(c_2Elist_2EREVERSE(A_27a),V0l1) = ap(c_2Elist_2EREVERSE(A_27a),V1l2)) <=> (V0l1 = V1l2))))))))).
tff(conj_thm_2Elist_2EMEM__REVERSE,lemma,(( ! [A_27a:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ! [V1x:$i] : (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))))))))))).
tff(conj_thm_2Elist_2ELENGTH__REVERSE,lemma,(( ! [A_27a:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => (surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),ap(c_2Elist_2EREVERSE(A_27a),V0l))) = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l)))))))).
tff(conj_thm_2Elist_2EREVERSE__EQ__NIL,lemma,(( ! [A_27a:del]: ( ! [V0l:$i] : (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)))))))).
tff(conj_thm_2Elist_2EREVERSE__EQ__SING,lemma,(( ! [A_27a:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ! [V1e:$i] : (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))))))))))).
tff(conj_thm_2Elist_2EFILTER__REVERSE,lemma,(( ! [A_27a:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ! [V1P:$i] : (mem(V1P,arr(A_27a,bool)) => (ap(ap(c_2Elist_2EFILTER(A_27a),V1P),ap(c_2Elist_2EREVERSE(A_27a),V0l)) = ap(c_2Elist_2EREVERSE(A_27a),ap(ap(c_2Elist_2EFILTER(A_27a),V1P),V0l)))))))))).
tff(ax_thm_2Elist_2ELAST__DEF,axiom,( ! [A_27a:del]: ( ! [V0h:$i] : (mem(V0h,A_27a) => ( ! [V1t:$i] : (mem(V1t,ty_2Elist_2Elist(A_27a)) => (ap(c_2Elist_2ELAST(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V0h),V1t)) = ap(ap(ap(c_2Ebool_2ECOND(A_27a),ap(ap(c_2Emin_2E_3D(ty_2Elist_2Elist(A_27a)),V1t),c_2Elist_2ENIL(A_27a))),V0h),ap(c_2Elist_2ELAST(A_27a),V1t))))))))).
tff(ax_thm_2Elist_2EFRONT__DEF,axiom,( ! [A_27a:del]: ( ! [V0h:$i] : (mem(V0h,A_27a) => ( ! [V1t:$i] : (mem(V1t,ty_2Elist_2Elist(A_27a)) => (ap(c_2Elist_2EFRONT(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V0h),V1t)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Elist_2Elist(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Elist_2Elist(A_27a)),V1t),c_2Elist_2ENIL(A_27a))),c_2Elist_2ENIL(A_27a)),ap(ap(c_2Elist_2ECONS(A_27a),V0h),ap(c_2Elist_2EFRONT(A_27a),V1t)))))))))).
tff(conj_thm_2Elist_2ELAST__CONS,lemma,(( ! [A_27a:del]: (( ! [V0x:$i] : (mem(V0x,A_27a) => (ap(c_2Elist_2ELAST(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V0x),c_2Elist_2ENIL(A_27a))) = V0x))) & ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => ( ! [V3z:$i] : (mem(V3z,ty_2Elist_2Elist(A_27a)) => (ap(c_2Elist_2ELAST(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V1x),ap(ap(c_2Elist_2ECONS(A_27a),V2y),V3z))) = ap(c_2Elist_2ELAST(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V2y),V3z))))))))))))).
tff(conj_thm_2Elist_2ELAST__EL,lemma,(( ! [A_27a:del]: ( ! [V0ls:$i] : (mem(V0ls,ty_2Elist_2Elist(A_27a)) => ((~~ (V0ls = c_2Elist_2ENIL(A_27a))) => (ap(c_2Elist_2ELAST(A_27a),V0ls) = ap(ap(c_2Elist_2EEL(A_27a),ap(c_2Eprim__rec_2EPRE,ap(c_2Elist_2ELENGTH(A_27a),V0ls))),V0ls)))))))).
tff(conj_thm_2Elist_2ELAST__MAP,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,A_27b)) => ((~~ (V0l = c_2Elist_2ENIL(A_27a))) => (ap(c_2Elist_2ELAST(A_27b),ap(ap(c_2Elist_2EMAP(A_27a,A_27b),V1f),V0l)) = ap(V1f,ap(c_2Elist_2ELAST(A_27a),V0l)))))))))))).
tff(conj_thm_2Elist_2EFRONT__CONS,lemma,(( ! [A_27a:del]: (( ! [V0x:$i] : (mem(V0x,A_27a) => (ap(c_2Elist_2EFRONT(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V0x),c_2Elist_2ENIL(A_27a))) = c_2Elist_2ENIL(A_27a)))) & ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => ( ! [V3z:$i] : (mem(V3z,ty_2Elist_2Elist(A_27a)) => (ap(c_2Elist_2EFRONT(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V1x),ap(ap(c_2Elist_2ECONS(A_27a),V2y),V3z))) = ap(ap(c_2Elist_2ECONS(A_27a),V1x),ap(c_2Elist_2EFRONT(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V2y),V3z)))))))))))))).
tff(conj_thm_2Elist_2ELENGTH__FRONT__CONS,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1xs:$i] : (mem(V1xs,ty_2Elist_2Elist(A_27a)) => (surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),ap(c_2Elist_2EFRONT(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V0x),V1xs)))) = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V1xs)))))))))).
tff(conj_thm_2Elist_2EFRONT__CONS__EQ__NIL,lemma,(( ! [A_27a:del]: (( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1xs:$i] : (mem(V1xs,ty_2Elist_2Elist(A_27a)) => ((ap(c_2Elist_2EFRONT(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V0x),V1xs)) = c_2Elist_2ENIL(A_27a)) <=> (V1xs = c_2Elist_2ENIL(A_27a))))))) & (( ! [V2x:$i] : (mem(V2x,A_27a) => ( ! [V3xs:$i] : (mem(V3xs,ty_2Elist_2Elist(A_27a)) => ((c_2Elist_2ENIL(A_27a) = ap(c_2Elist_2EFRONT(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V2x),V3xs))) <=> (V3xs = c_2Elist_2ENIL(A_27a))))))) & ( ! [V4x:$i] : (mem(V4x,A_27a) => ( ! [V5xs:$i] : (mem(V5xs,ty_2Elist_2Elist(A_27a)) => (p(ap(c_2Elist_2ENULL(A_27a),ap(c_2Elist_2EFRONT(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V4x),V5xs)))) <=> p(ap(c_2Elist_2ENULL(A_27a),V5xs)))))))))))).
tff(conj_thm_2Elist_2EAPPEND__FRONT__LAST,lemma,(( ! [A_27a:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => ((~~ (V0l = c_2Elist_2ENIL(A_27a))) => (ap(ap(c_2Elist_2EAPPEND(A_27a),ap(c_2Elist_2EFRONT(A_27a),V0l)),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2ELAST(A_27a),V0l)),c_2Elist_2ENIL(A_27a))) = V0l))))))).
tff(conj_thm_2Elist_2ELAST__CONS__cond,lemma,(( ! [A_27a:del]: ( ! [V0h:$i] : (mem(V0h,A_27a) => ( ! [V1t:$i] : (mem(V1t,ty_2Elist_2Elist(A_27a)) => (ap(c_2Elist_2ELAST(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V0h),V1t)) = ap(ap(ap(c_2Ebool_2ECOND(A_27a),ap(ap(c_2Emin_2E_3D(ty_2Elist_2Elist(A_27a)),V1t),c_2Elist_2ENIL(A_27a))),V0h),ap(c_2Elist_2ELAST(A_27a),V1t)))))))))).
tff(conj_thm_2Elist_2ELAST__APPEND__CONS,lemma,(( ! [A_27a:del]: ( ! [V0h:$i] : (mem(V0h,A_27a) => ( ! [V1l1:$i] : (mem(V1l1,ty_2Elist_2Elist(A_27a)) => ( ! [V2l2:$i] : (mem(V2l2,ty_2Elist_2Elist(A_27a)) => (ap(c_2Elist_2ELAST(A_27a),ap(ap(c_2Elist_2EAPPEND(A_27a),V1l1),ap(ap(c_2Elist_2ECONS(A_27a),V0h),V2l2))) = ap(c_2Elist_2ELAST(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V0h),V2l2)))))))))))).
tff(ax_thm_2Elist_2ETAKE__def,axiom,( ! [A_27a:del]: (( ! [V0n:tp__ty_2Enum_2Enum] : (ap(ap(c_2Elist_2ETAKE(A_27a),inj__ty_2Enum_2Enum(V0n)),c_2Elist_2ENIL(A_27a)) = c_2Elist_2ENIL(A_27a))) & ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2x:$i] : (mem(V2x,A_27a) => ( ! [V3xs:$i] : (mem(V3xs,ty_2Elist_2Elist(A_27a)) => (ap(ap(c_2Elist_2ETAKE(A_27a),inj__ty_2Enum_2Enum(V1n)),ap(ap(c_2Elist_2ECONS(A_27a),V2x),V3xs)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Elist_2Elist(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),c_2Elist_2ENIL(A_27a)),ap(ap(c_2Elist_2ECONS(A_27a),V2x),ap(ap(c_2Elist_2ETAKE(A_27a),ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V1n)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),V3xs)))))))))))).
tff(ax_thm_2Elist_2EDROP__def,axiom,( ! [A_27a:del]: (( ! [V0n:tp__ty_2Enum_2Enum] : (ap(ap(c_2Elist_2EDROP(A_27a),inj__ty_2Enum_2Enum(V0n)),c_2Elist_2ENIL(A_27a)) = c_2Elist_2ENIL(A_27a))) & ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2x:$i] : (mem(V2x,A_27a) => ( ! [V3xs:$i] : (mem(V3xs,ty_2Elist_2Elist(A_27a)) => (ap(ap(c_2Elist_2EDROP(A_27a),inj__ty_2Enum_2Enum(V1n)),ap(ap(c_2Elist_2ECONS(A_27a),V2x),V3xs)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Elist_2Elist(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(ap(c_2Elist_2ECONS(A_27a),V2x),V3xs)),ap(ap(c_2Elist_2EDROP(A_27a),ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V1n)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),V3xs))))))))))).
tff(conj_thm_2Elist_2ETAKE__nil,lemma,(( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : (ap(ap(c_2Elist_2ETAKE(A_27a),inj__ty_2Enum_2Enum(V0n)),c_2Elist_2ENIL(A_27a)) = c_2Elist_2ENIL(A_27a)))))).
tff(conj_thm_2Elist_2ETAKE__cons,lemma,(( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2xs:$i] : (mem(V2xs,ty_2Elist_2Elist(A_27a)) => (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n))) => (ap(ap(c_2Elist_2ETAKE(A_27a),inj__ty_2Enum_2Enum(V0n)),ap(ap(c_2Elist_2ECONS(A_27a),V1x),V2xs)) = ap(ap(c_2Elist_2ECONS(A_27a),V1x),ap(ap(c_2Elist_2ETAKE(A_27a),ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0n)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),V2xs)))))))))))).
tff(conj_thm_2Elist_2EDROP__nil,lemma,(( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : (ap(ap(c_2Elist_2EDROP(A_27a),inj__ty_2Enum_2Enum(V0n)),c_2Elist_2ENIL(A_27a)) = c_2Elist_2ENIL(A_27a)))))).
tff(conj_thm_2Elist_2EDROP__cons,lemma,(( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2xs:$i] : (mem(V2xs,ty_2Elist_2Elist(A_27a)) => (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n))) => (ap(ap(c_2Elist_2EDROP(A_27a),inj__ty_2Enum_2Enum(V0n)),ap(ap(c_2Elist_2ECONS(A_27a),V1x),V2xs)) = ap(ap(c_2Elist_2EDROP(A_27a),ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0n)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),V2xs))))))))))).
tff(conj_thm_2Elist_2ETAKE__0,lemma,(( ! [A_27a:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => (ap(ap(c_2Elist_2ETAKE(A_27a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),V0l) = c_2Elist_2ENIL(A_27a))))))).
tff(conj_thm_2Elist_2ETAKE__LENGTH__ID,lemma,(( ! [A_27a:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => (ap(ap(c_2Elist_2ETAKE(A_27a),ap(c_2Elist_2ELENGTH(A_27a),V0l)),V0l) = V0l)))))).
tff(conj_thm_2Elist_2ELENGTH__TAKE,lemma,(( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(A_27a)) => (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0n)),ap(c_2Elist_2ELENGTH(A_27a),V1l))) => (surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),ap(ap(c_2Elist_2ETAKE(A_27a),inj__ty_2Enum_2Enum(V0n)),V1l))) = V0n)))))))).
tff(conj_thm_2Elist_2EMAP__TAKE,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27b)) => ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2l:$i] : (mem(V2l,ty_2Elist_2Elist(A_27a)) => (ap(ap(c_2Elist_2EMAP(A_27a,A_27b),V0f),ap(ap(c_2Elist_2ETAKE(A_27a),inj__ty_2Enum_2Enum(V1n)),V2l)) = ap(ap(c_2Elist_2ETAKE(A_27b),inj__ty_2Enum_2Enum(V1n)),ap(ap(c_2Elist_2EMAP(A_27a,A_27b),V0f),V2l)))))))))))).
tff(conj_thm_2Elist_2ETAKE__APPEND1,lemma,(( ! [A_27a:del]: ( ! [V0l1:$i] : (mem(V0l1,ty_2Elist_2Elist(A_27a)) => ( ! [V1l2:$i] : (mem(V1l2,ty_2Elist_2Elist(A_27a)) => ( ! [V2n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V2n)),ap(c_2Elist_2ELENGTH(A_27a),V0l1))) => (ap(ap(c_2Elist_2ETAKE(A_27a),inj__ty_2Enum_2Enum(V2n)),ap(ap(c_2Elist_2EAPPEND(A_27a),V0l1),V1l2)) = ap(ap(c_2Elist_2ETAKE(A_27a),inj__ty_2Enum_2Enum(V2n)),V0l1))))))))))).
tff(conj_thm_2Elist_2ETAKE__APPEND2,lemma,(( ! [A_27a:del]: ( ! [V0l1:$i] : (mem(V0l1,ty_2Elist_2Elist(A_27a)) => ( ! [V1l2:$i] : (mem(V1l2,ty_2Elist_2Elist(A_27a)) => ( ! [V2n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Elist_2ELENGTH(A_27a),V0l1)),inj__ty_2Enum_2Enum(V2n))) => (ap(ap(c_2Elist_2ETAKE(A_27a),inj__ty_2Enum_2Enum(V2n)),ap(ap(c_2Elist_2EAPPEND(A_27a),V0l1),V1l2)) = ap(ap(c_2Elist_2EAPPEND(A_27a),V0l1),ap(ap(c_2Elist_2ETAKE(A_27a),ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V2n)),ap(c_2Elist_2ELENGTH(A_27a),V0l1))),V1l2)))))))))))).
tff(conj_thm_2Elist_2EDROP__0,lemma,(( ! [A_27a:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => (ap(ap(c_2Elist_2EDROP(A_27a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),V0l) = V0l)))))).
tff(conj_thm_2Elist_2ETAKE__DROP,lemma,(( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(A_27a)) => (ap(ap(c_2Elist_2EAPPEND(A_27a),ap(ap(c_2Elist_2ETAKE(A_27a),inj__ty_2Enum_2Enum(V0n)),V1l)),ap(ap(c_2Elist_2EDROP(A_27a),inj__ty_2Enum_2Enum(V0n)),V1l)) = V1l))))))).
tff(conj_thm_2Elist_2ELENGTH__DROP,lemma,(( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(A_27a)) => (surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),ap(ap(c_2Elist_2EDROP(A_27a),inj__ty_2Enum_2Enum(V0n)),V1l))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,ap(c_2Elist_2ELENGTH(A_27a),V1l)),inj__ty_2Enum_2Enum(V0n)))))))))).
tff(conj_thm_2Elist_2EMEM__DROP,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1ls:$i] : (mem(V1ls,ty_2Elist_2Elist(A_27a)) => ( ! [V2n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Ebool_2EIN(A_27a),V0x),ap(c_2Elist_2ELIST__TO__SET(A_27a),ap(ap(c_2Elist_2EDROP(A_27a),inj__ty_2Enum_2Enum(V2n)),V1ls)))) <=> ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V2n)),ap(c_2Elist_2ELENGTH(A_27a),V1ls))) & (V0x = ap(ap(c_2Elist_2EEL(A_27a),inj__ty_2Enum_2Enum(V2n)),V1ls))) | p(ap(ap(c_2Ebool_2EIN(A_27a),V0x),ap(c_2Elist_2ELIST__TO__SET(A_27a),ap(ap(c_2Elist_2EDROP(A_27a),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V2n))),V1ls)))))))))))))).
tff(conj_thm_2Elist_2EDROP__NIL,lemma,(( ! [A_27a:del]: ( ! [V0ls:$i] : (mem(V0ls,ty_2Elist_2Elist(A_27a)) => ( ! [V1n:tp__ty_2Enum_2Enum] : ((ap(ap(c_2Elist_2EDROP(A_27a),inj__ty_2Enum_2Enum(V1n)),V0ls) = c_2Elist_2ENIL(A_27a)) <=> p(ap(ap(c_2Earithmetic_2E_3E_3D,inj__ty_2Enum_2Enum(V1n)),ap(c_2Elist_2ELENGTH(A_27a),V0ls)))))))))).
tff(conj_thm_2Elist_2EFOLDL2__ind,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0P:$i] : (mem(V0P,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),bool))))) => ((( ! [V1f:$i] : (mem(V1f,arr(A_27a,arr(A_27b,arr(A_27c,A_27a)))) => ( ! [V2a:$i] : (mem(V2a,A_27a) => ( ! [V3b:$i] : (mem(V3b,A_27b) => ( ! [V4bs:$i] : (mem(V4bs,ty_2Elist_2Elist(A_27b)) => ( ! [V5c:$i] : (mem(V5c,A_27c) => ( ! [V6cs:$i] : (mem(V6cs,ty_2Elist_2Elist(A_27c)) => (p(ap(ap(ap(ap(V0P,V1f),ap(ap(ap(V1f,V2a),V3b),V5c)),V4bs),V6cs)) => p(ap(ap(ap(ap(V0P,V1f),V2a),ap(ap(c_2Elist_2ECONS(A_27b),V3b),V4bs)),ap(ap(c_2Elist_2ECONS(A_27c),V5c),V6cs)))))))))))))))) & (( ! [V7f:$i] : (mem(V7f,arr(A_27a,arr(A_27b,arr(A_27c,A_27a)))) => ( ! [V8a:$i] : (mem(V8a,A_27a) => ( ! [V9cs:$i] : (mem(V9cs,ty_2Elist_2Elist(A_27c)) => p(ap(ap(ap(ap(V0P,V7f),V8a),c_2Elist_2ENIL(A_27b)),V9cs)))))))) & ( ! [V10f:$i] : (mem(V10f,arr(A_27a,arr(A_27b,arr(A_27c,A_27a)))) => ( ! [V11a:$i] : (mem(V11a,A_27a) => ( ! [V12v6:$i] : (mem(V12v6,A_27b) => ( ! [V13v7:$i] : (mem(V13v7,ty_2Elist_2Elist(A_27b)) => p(ap(ap(ap(ap(V0P,V10f),V11a),ap(ap(c_2Elist_2ECONS(A_27b),V12v6),V13v7)),c_2Elist_2ENIL(A_27c))))))))))))) => ( ! [V14v:$i] : (mem(V14v,arr(A_27a,arr(A_27b,arr(A_27c,A_27a)))) => ( ! [V15v1:$i] : (mem(V15v1,A_27a) => ( ! [V16v2:$i] : (mem(V16v2,ty_2Elist_2Elist(A_27b)) => ( ! [V17v3:$i] : (mem(V17v3,ty_2Elist_2Elist(A_27c)) => p(ap(ap(ap(ap(V0P,V14v),V15v1),V16v2),V17v3)))))))))))))))))).
tff(conj_thm_2Elist_2EFOLDL2__def,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: (( ! [V0f:$i] : (mem(V0f,arr(A_27a,arr(A_27b,arr(A_27c,A_27a)))) => ( ! [V1cs:$i] : (mem(V1cs,ty_2Elist_2Elist(A_27c)) => ( ! [V2c:$i] : (mem(V2c,A_27c) => ( ! [V3bs:$i] : (mem(V3bs,ty_2Elist_2Elist(A_27b)) => ( ! [V4b:$i] : (mem(V4b,A_27b) => ( ! [V5a:$i] : (mem(V5a,A_27a) => (ap(ap(ap(ap(c_2Elist_2EFOLDL2(A_27a,A_27b,A_27c),V0f),V5a),ap(ap(c_2Elist_2ECONS(A_27b),V4b),V3bs)),ap(ap(c_2Elist_2ECONS(A_27c),V2c),V1cs)) = ap(ap(ap(ap(c_2Elist_2EFOLDL2(A_27a,A_27b,A_27c),V0f),ap(ap(ap(V0f,V5a),V4b),V2c)),V3bs),V1cs)))))))))))))) & (( ! [V6f:$i] : (mem(V6f,arr(A_27a,arr(A_27b,arr(A_27c,A_27a)))) => ( ! [V7cs:$i] : (mem(V7cs,ty_2Elist_2Elist(A_27c)) => ( ! [V8a:$i] : (mem(V8a,A_27a) => (ap(ap(ap(ap(c_2Elist_2EFOLDL2(A_27a,A_27b,A_27c),V6f),V8a),c_2Elist_2ENIL(A_27b)),V7cs) = V8a))))))) & ( ! [V9v7:$i] : (mem(V9v7,ty_2Elist_2Elist(A_27b)) => ( ! [V10v6:$i] : (mem(V10v6,A_27b) => ( ! [V11f:$i] : (mem(V11f,arr(A_27a,arr(A_27b,arr(A_27c,A_27a)))) => ( ! [V12a:$i] : (mem(V12a,A_27a) => (ap(ap(ap(ap(c_2Elist_2EFOLDL2(A_27a,A_27b,A_27c),V11f),V12a),ap(ap(c_2Elist_2ECONS(A_27b),V10v6),V9v7)),c_2Elist_2ENIL(A_27c)) = V12a)))))))))))))))).
tff(conj_thm_2Elist_2EFOLDL2__cong,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0l1:$i] : (mem(V0l1,ty_2Elist_2Elist(A_27a)) => ( ! [V1l1_27:$i] : (mem(V1l1_27,ty_2Elist_2Elist(A_27a)) => ( ! [V2l2:$i] : (mem(V2l2,ty_2Elist_2Elist(A_27b)) => ( ! [V3l2_27:$i] : (mem(V3l2_27,ty_2Elist_2Elist(A_27b)) => ( ! [V4a:$i] : (mem(V4a,A_27c) => ( ! [V5a_27:$i] : (mem(V5a_27,A_27c) => ( ! [V6f:$i] : (mem(V6f,arr(A_27c,arr(A_27a,arr(A_27b,A_27c)))) => ( ! [V7f_27:$i] : (mem(V7f_27,arr(A_27c,arr(A_27a,arr(A_27b,A_27c)))) => (((V0l1 = V1l1_27) & ((V2l2 = V3l2_27) & ((V4a = V5a_27) & ( ! [V8z:$i] : (mem(V8z,A_27c) => ( ! [V9b:$i] : (mem(V9b,A_27a) => ( ! [V10c:$i] : (mem(V10c,A_27b) => ((p(ap(ap(c_2Ebool_2EIN(A_27a),V9b),ap(c_2Elist_2ELIST__TO__SET(A_27a),V1l1_27))) & p(ap(ap(c_2Ebool_2EIN(A_27b),V10c),ap(c_2Elist_2ELIST__TO__SET(A_27b),V3l2_27)))) => (ap(ap(ap(V6f,V8z),V9b),V10c) = ap(ap(ap(V7f_27,V8z),V9b),V10c)))))))))))) => (ap(ap(ap(ap(c_2Elist_2EFOLDL2(A_27c,A_27a,A_27b),V6f),V4a),V0l1),V2l2) = ap(ap(ap(ap(c_2Elist_2EFOLDL2(A_27c,A_27a,A_27b),V7f_27),V5a_27),V1l1_27),V3l2_27)))))))))))))))))))))))).
tff(conj_thm_2Elist_2EFOLDL2__FOLDL,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0l1:$i] : (mem(V0l1,ty_2Elist_2Elist(A_27a)) => ( ! [V1l2:$i] : (mem(V1l2,ty_2Elist_2Elist(A_27b)) => ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l1)) = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27b),V1l2))) => ( ! [V2f:$i] : (mem(V2f,arr(A_27c,arr(A_27a,arr(A_27b,A_27c)))) => ( ! [V3a:$i] : (mem(V3a,A_27c) => (ap(ap(ap(ap(c_2Elist_2EFOLDL2(A_27c,A_27a,A_27b),V2f),V3a),V0l1),V1l2) = ap(ap(ap(c_2Elist_2EFOLDL(ty_2Epair_2Eprod(A_27a,A_27b),A_27c),f415(A_27b,A_27a,A_27c,V2f)),V3a),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)))))))))))))))))).
tff(conj_thm_2Elist_2EEVERY2__cong,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0l1:$i] : (mem(V0l1,ty_2Elist_2Elist(A_27a)) => ( ! [V1l1_27:$i] : (mem(V1l1_27,ty_2Elist_2Elist(A_27a)) => ( ! [V2l2:$i] : (mem(V2l2,ty_2Elist_2Elist(A_27b)) => ( ! [V3l2_27:$i] : (mem(V3l2_27,ty_2Elist_2Elist(A_27b)) => ( ! [V4P:$i] : (mem(V4P,arr(A_27a,arr(A_27b,bool))) => ( ! [V5P_27:$i] : (mem(V5P_27,arr(A_27a,arr(A_27b,bool))) => (((V0l1 = V1l1_27) & ((V2l2 = V3l2_27) & ( ! [V6x:$i] : (mem(V6x,A_27a) => ( ! [V7y:$i] : (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)))) => (p(ap(ap(V4P,V6x),V7y)) <=> p(ap(ap(V5P_27,V6x),V7y)))))))))) => (p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27b),V4P),V0l1),V2l2)) <=> p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27b),V5P_27),V1l1_27),V3l2_27)))))))))))))))))))).
tff(conj_thm_2Elist_2EMAP__EQ__EVERY2,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f1:$i] : (mem(V0f1,arr(A_27a,A_27b)) => ( ! [V1f2:$i] : (mem(V1f2,arr(A_27c,A_27b)) => ( ! [V2l1:$i] : (mem(V2l1,ty_2Elist_2Elist(A_27a)) => ( ! [V3l2:$i] : (mem(V3l2,ty_2Elist_2Elist(A_27c)) => ((ap(ap(c_2Elist_2EMAP(A_27a,A_27b),V0f1),V2l1) = ap(ap(c_2Elist_2EMAP(A_27c,A_27b),V1f2),V3l2)) <=> ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V2l1)) = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27c),V3l2))) & p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27c),f417(A_27a,A_27b,A_27c,V0f1,V1f2)),V2l1),V3l2))))))))))))))))).
tff(conj_thm_2Elist_2EEVERY2__EVERY,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0l1:$i] : (mem(V0l1,ty_2Elist_2Elist(A_27a)) => ( ! [V1l2:$i] : (mem(V1l2,ty_2Elist_2Elist(A_27b)) => ( ! [V2f:$i] : (mem(V2f,arr(A_27a,arr(A_27b,bool))) => (p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27b),V2f),V0l1),V1l2)) <=> ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l1)) = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27b),V1l2))) & p(ap(ap(c_2Elist_2EEVERY(ty_2Epair_2Eprod(A_27a,A_27b)),ap(c_2Epair_2EUNCURRY(A_27a,A_27b,bool),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)))))))))))))))).
tff(conj_thm_2Elist_2EEVERY2__LENGTH,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,arr(A_27b,bool))) => ( ! [V1l1:$i] : (mem(V1l1,ty_2Elist_2Elist(A_27a)) => ( ! [V2l2:$i] : (mem(V2l2,ty_2Elist_2Elist(A_27b)) => (p(ap(ap(ap(c_2Elist_2ELIST__REL(A_27a,A_27b),V0P),V1l1),V2l2)) => (surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V1l1)) = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27b),V2l2)))))))))))))).
tff(conj_thm_2Elist_2EEVERY2__mono,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R1:$i] : (mem(V0R1,arr(A_27a,arr(A_27b,bool))) => ( ! [V1R2:$i] : (mem(V1R2,arr(A_27a,arr(A_27b,bool))) => ( ! [V2l1:$i] : (mem(V2l1,ty_2Elist_2Elist(A_27a)) => ( ! [V3l2:$i] : (mem(V3l2,ty_2Elist_2Elist(A_27b)) => (( ! [V4x:$i] : (mem(V4x,A_27a) => ( ! [V5y:$i] : (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)))))))))))))))).
tff(ax_thm_2Elist_2EALL__DISTINCT,axiom,( ! [A_27a:del]: ((p(ap(c_2Elist_2EALL__DISTINCT(A_27a),c_2Elist_2ENIL(A_27a))) <=> $true) & ( ! [V0h:$i] : (mem(V0h,A_27a) => ( ! [V1t:$i] : (mem(V1t,ty_2Elist_2Elist(A_27a)) => (p(ap(c_2Elist_2EALL__DISTINCT(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V0h),V1t))) <=> ((~~ p(ap(ap(c_2Ebool_2EIN(A_27a),V0h),ap(c_2Elist_2ELIST__TO__SET(A_27a),V1t)))) & p(ap(c_2Elist_2EALL__DISTINCT(A_27a),V1t))))))))))).
tff(conj_thm_2Elist_2EALL__DISTINCT__FILTER,lemma,(( ! [A_27a:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => (p(ap(c_2Elist_2EALL__DISTINCT(A_27a),V0l)) <=> ( ! [V1x:$i] : (mem(V1x,A_27a) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V1x),ap(c_2Elist_2ELIST__TO__SET(A_27a),V0l))) => (ap(ap(c_2Elist_2EFILTER(A_27a),ap(c_2Emin_2E_3D(A_27a),V1x)),V0l) = ap(ap(c_2Elist_2ECONS(A_27a),V1x),c_2Elist_2ENIL(A_27a)))))))))))).
tff(conj_thm_2Elist_2EFILTER__ALL__DISTINCT,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(A_27a)) => (p(ap(c_2Elist_2EALL__DISTINCT(A_27a),V1l)) => p(ap(c_2Elist_2EALL__DISTINCT(A_27a),ap(ap(c_2Elist_2EFILTER(A_27a),V0P),V1l))))))))))).
tff(conj_thm_2Elist_2EALL__DISTINCT__MAP,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27b)) => ( ! [V1ls:$i] : (mem(V1ls,ty_2Elist_2Elist(A_27a)) => (p(ap(c_2Elist_2EALL__DISTINCT(A_27b),ap(ap(c_2Elist_2EMAP(A_27a,A_27b),V0f),V1ls))) => p(ap(c_2Elist_2EALL__DISTINCT(A_27a),V1ls))))))))))).
tff(conj_thm_2Elist_2EEL__ALL__DISTINCT__EL__EQ,lemma,(( ! [A_27a:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => (p(ap(c_2Elist_2EALL__DISTINCT(A_27a),V0l)) <=> ( ! [V1n1:tp__ty_2Enum_2Enum] : ( ! [V2n2:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1n1)),ap(c_2Elist_2ELENGTH(A_27a),V0l))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V2n2)),ap(c_2Elist_2ELENGTH(A_27a),V0l)))) => ((ap(ap(c_2Elist_2EEL(A_27a),inj__ty_2Enum_2Enum(V1n1)),V0l) = ap(ap(c_2Elist_2EEL(A_27a),inj__ty_2Enum_2Enum(V2n2)),V0l)) <=> (V1n1 = V2n2))))))))))).
tff(conj_thm_2Elist_2EALL__DISTINCT__EL__IMP,lemma,(( ! [A_27a:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => ( ! [V1n1:tp__ty_2Enum_2Enum] : ( ! [V2n2:tp__ty_2Enum_2Enum] : ((p(ap(c_2Elist_2EALL__DISTINCT(A_27a),V0l)) & (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1n1)),ap(c_2Elist_2ELENGTH(A_27a),V0l))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V2n2)),ap(c_2Elist_2ELENGTH(A_27a),V0l))))) => ((ap(ap(c_2Elist_2EEL(A_27a),inj__ty_2Enum_2Enum(V1n1)),V0l) = ap(ap(c_2Elist_2EEL(A_27a),inj__ty_2Enum_2Enum(V2n2)),V0l)) <=> (V1n1 = V2n2)))))))))).
tff(conj_thm_2Elist_2EALL__DISTINCT__APPEND,lemma,(( ! [A_27a:del]: ( ! [V0l1:$i] : (mem(V0l1,ty_2Elist_2Elist(A_27a)) => ( ! [V1l2:$i] : (mem(V1l2,ty_2Elist_2Elist(A_27a)) => (p(ap(c_2Elist_2EALL__DISTINCT(A_27a),ap(ap(c_2Elist_2EAPPEND(A_27a),V0l1),V1l2))) <=> (p(ap(c_2Elist_2EALL__DISTINCT(A_27a),V0l1)) & (p(ap(c_2Elist_2EALL__DISTINCT(A_27a),V1l2)) & ( ! [V2e:$i] : (mem(V2e,A_27a) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V2e),ap(c_2Elist_2ELIST__TO__SET(A_27a),V0l1))) => (~~ p(ap(ap(c_2Ebool_2EIN(A_27a),V2e),ap(c_2Elist_2ELIST__TO__SET(A_27a),V1l2))))))))))))))))).
tff(conj_thm_2Elist_2EALL__DISTINCT__SING,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => p(ap(c_2Elist_2EALL__DISTINCT(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V0x),c_2Elist_2ENIL(A_27a))))))))).
tff(conj_thm_2Elist_2EALL__DISTINCT__ZIP,conjecture,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0l1:$i] : (mem(V0l1,ty_2Elist_2Elist(A_27a)) => ( ! [V1l2:$i] : (mem(V1l2,ty_2Elist_2Elist(A_27b)) => ((p(ap(c_2Elist_2EALL__DISTINCT(A_27a),V0l1)) & (surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l1)) = surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27b),V1l2)))) => p(ap(c_2Elist_2EALL__DISTINCT(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))))))))))))).
