include('Axioms/set_relation^2.ax').
thf(tp_ty_2Elist_2Elist,type,( ty_2Elist_2Elist: del >del )).
thf(tp_c_2Elist_2EALL__DISTINCT,type,(c_2Elist_2EALL__DISTINCT:(del>$i))).
thf(mem_c_2Elist_2EALL__DISTINCT,axiom,( ! [A_27a:del] : (mem@(c_2Elist_2EALL__DISTINCT@A_27a)@(arr@(ty_2Elist_2Elist@A_27a)@bool)))).
thf(tp_c_2Elist_2EAPPEND,type,(c_2Elist_2EAPPEND:(del>$i))).
thf(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)))))).
thf(tp_c_2Elist_2ECONS,type,(c_2Elist_2ECONS:(del>$i))).
thf(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)))))).
thf(tp_c_2Elist_2EDROP,type,(c_2Elist_2EDROP:(del>$i))).
thf(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)))))).
thf(tp_c_2Elist_2EEL,type,(c_2Elist_2EEL:(del>$i))).
thf(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))))).
thf(tp_c_2Elist_2EEVERY,type,(c_2Elist_2EEVERY:(del>$i))).
thf(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))))).
thf(tp_c_2Elist_2EEVERYi,type,(c_2Elist_2EEVERYi:(del>$i))).
thf(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))))).
thf(tp_c_2Elist_2EEXISTS,type,(c_2Elist_2EEXISTS:(del>$i))).
thf(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))))).
thf(tp_c_2Elist_2EFILTER,type,(c_2Elist_2EFILTER:(del>$i))).
thf(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)))))).
thf(tp_c_2Elist_2EFIND,type,(c_2Elist_2EFIND:(del>$i))).
thf(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)))))).
thf(tp_c_2Elist_2EFLAT,type,(c_2Elist_2EFLAT:(del>$i))).
thf(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))))).
thf(tp_c_2Elist_2EFOLDL,type,(c_2Elist_2EFOLDL:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2Elist_2EFOLDL2,type,(c_2Elist_2EFOLDL2:(del>(del>(del>$i))))).
thf(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))))))))).
thf(tp_c_2Elist_2EFOLDR,type,(c_2Elist_2EFOLDR:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2Elist_2EFRONT,type,(c_2Elist_2EFRONT:(del>$i))).
thf(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))))).
thf(tp_c_2Elist_2EGENLIST,type,(c_2Elist_2EGENLIST:(del>$i))).
thf(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)))))).
thf(tp_c_2Elist_2EGENLIST__AUX,type,(c_2Elist_2EGENLIST__AUX:(del>$i))).
thf(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))))))).
thf(tp_c_2Elist_2EHD,type,(c_2Elist_2EHD:(del>$i))).
thf(mem_c_2Elist_2EHD,axiom,( ! [A_27a:del] : (mem@(c_2Elist_2EHD@A_27a)@(arr@(ty_2Elist_2Elist@A_27a)@A_27a)))).
thf(tp_c_2Elist_2EINDEX__FIND,type,(c_2Elist_2EINDEX__FIND:(del>$i))).
thf(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)))))))).
thf(tp_c_2Elist_2EINDEX__OF,type,(c_2Elist_2EINDEX__OF:(del>$i))).
thf(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)))))).
thf(tp_c_2Elist_2ELAST,type,(c_2Elist_2ELAST:(del>$i))).
thf(mem_c_2Elist_2ELAST,axiom,( ! [A_27a:del] : (mem@(c_2Elist_2ELAST@A_27a)@(arr@(ty_2Elist_2Elist@A_27a)@A_27a)))).
thf(tp_c_2Elist_2ELEN,type,(c_2Elist_2ELEN:(del>$i))).
thf(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))))).
thf(tp_c_2Elist_2ELENGTH,type,(c_2Elist_2ELENGTH:(del>$i))).
thf(mem_c_2Elist_2ELENGTH,axiom,( ! [A_27a:del] : (mem@(c_2Elist_2ELENGTH@A_27a)@(arr@(ty_2Elist_2Elist@A_27a)@ty_2Enum_2Enum)))).
thf(tp_c_2Elist_2ELIST__APPLY,type,(c_2Elist_2ELIST__APPLY:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2Elist_2ELIST__BIND,type,(c_2Elist_2ELIST__BIND:(del>(del>$i)))).
thf(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))))))).
thf(stp_c_ty_2Elist_2Elist_ty_2Eone_2Eone,type,(tp__c_ty_2Elist_2Elist_ty_2Eone_2Eone : $tType)).
thf(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))).
thf(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))).
thf(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))).
thf(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)))).
thf(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)))))).
thf(tp_c_2Elist_2ELIST__GUARD,type,(c_2Elist_2ELIST__GUARD:$i)).
thf(mem_c_2Elist_2ELIST__GUARD,axiom,(mem@c_2Elist_2ELIST__GUARD@(arr@bool@(ty_2Elist_2Elist@ty_2Eone_2Eone)))).
thf(tp_c_2Elist_2ELIST__IGNORE__BIND,type,(c_2Elist_2ELIST__IGNORE__BIND:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2Elist_2ELIST__LIFT2,type,(c_2Elist_2ELIST__LIFT2:(del>(del>(del>$i))))).
thf(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))))))))).
thf(tp_c_2Elist_2ELIST__REL,type,(c_2Elist_2ELIST__REL:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2Elist_2ELIST__TO__SET,type,(c_2Elist_2ELIST__TO__SET:(del>$i))).
thf(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))))).
thf(tp_c_2Elist_2ELLEX,type,(c_2Elist_2ELLEX:(del>$i))).
thf(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)))))).
thf(tp_c_2Elist_2ELRC,type,(c_2Elist_2ELRC:(del>$i))).
thf(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))))))).
thf(tp_c_2Elist_2ELUPDATE,type,(c_2Elist_2ELUPDATE:(del>$i))).
thf(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))))))).
thf(tp_c_2Elist_2EMAP,type,(c_2Elist_2EMAP:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2Elist_2EMAP2,type,(c_2Elist_2EMAP2:(del>(del>(del>$i))))).
thf(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))))))))).
thf(tp_c_2Elist_2ENIL,type,(c_2Elist_2ENIL:(del>$i))).
thf(mem_c_2Elist_2ENIL,axiom,( ! [A_27a:del] : (mem@(c_2Elist_2ENIL@A_27a)@(ty_2Elist_2Elist@A_27a)))).
thf(tp_c_2Elist_2ENULL,type,(c_2Elist_2ENULL:(del>$i))).
thf(mem_c_2Elist_2ENULL,axiom,( ! [A_27a:del] : (mem@(c_2Elist_2ENULL@A_27a)@(arr@(ty_2Elist_2Elist@A_27a)@bool)))).
thf(tp_c_2Elist_2EOPT__MMAP,type,(c_2Elist_2EOPT__MMAP:(del>(del>$i)))).
thf(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)))))))).
thf(tp_c_2Elist_2EPAD__LEFT,type,(c_2Elist_2EPAD__LEFT:(del>$i))).
thf(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))))))).
thf(tp_c_2Elist_2EPAD__RIGHT,type,(c_2Elist_2EPAD__RIGHT:(del>$i))).
thf(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))))))).
thf(tp_c_2Elist_2EREV,type,(c_2Elist_2EREV:(del>$i))).
thf(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)))))).
thf(tp_c_2Elist_2EREVERSE,type,(c_2Elist_2EREVERSE:(del>$i))).
thf(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))))).
thf(tp_c_2Elist_2ESET__TO__LIST,type,(c_2Elist_2ESET__TO__LIST:(del>$i))).
thf(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))))).
thf(tp_c_2Elist_2ESHORTLEX,type,(c_2Elist_2ESHORTLEX:(del>$i))).
thf(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)))))).
thf(tp_c_2Elist_2ESNOC,type,(c_2Elist_2ESNOC:(del>$i))).
thf(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)))))).
thf(stp_c_ty_2Elist_2Elist_ty_2Enum_2Enum,type,(tp__c_ty_2Elist_2Elist_ty_2Enum_2Enum : $tType)).
thf(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))).
thf(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))).
thf(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))).
thf(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)))).
thf(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)))))).
thf(tp_c_2Elist_2ESUM,type,(c_2Elist_2ESUM:$i)).
thf(mem_c_2Elist_2ESUM,axiom,(mem@c_2Elist_2ESUM@(arr@(ty_2Elist_2Elist@ty_2Enum_2Enum)@ty_2Enum_2Enum))).
thf(stp_fo_c_2Elist_2ESUM,type,(fo__c_2Elist_2ESUM:(tp__c_ty_2Elist_2Elist_ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(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))))).
thf(tp_c_2Elist_2ESUM__ACC,type,(c_2Elist_2ESUM__ACC:$i)).
thf(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)))).
thf(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)))).
thf(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)))))).
thf(tp_c_2Elist_2ETAKE,type,(c_2Elist_2ETAKE:(del>$i))).
thf(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)))))).
thf(tp_c_2Elist_2ETL,type,(c_2Elist_2ETL:(del>$i))).
thf(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))))).
thf(tp_c_2Elist_2EUNIQUE,type,(c_2Elist_2EUNIQUE:(del>$i))).
thf(mem_c_2Elist_2EUNIQUE,axiom,( ! [A_27a:del] : (mem@(c_2Elist_2EUNIQUE@A_27a)@(arr@A_27a@(arr@(ty_2Elist_2Elist@A_27a)@bool))))).
thf(tp_c_2Elist_2EUNZIP,type,(c_2Elist_2EUNZIP:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2Elist_2EZIP,type,(c_2Elist_2EZIP:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2Elist_2EdropWhile,type,(c_2Elist_2EdropWhile:(del>$i))).
thf(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)))))).
thf(tp_c_2Elist_2EisPREFIX,type,(c_2Elist_2EisPREFIX:(del>$i))).
thf(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))))).
thf(tp_c_2Elist_2Elist__CASE,type,(c_2Elist_2Elist__CASE:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2Elist_2Elist__size,type,(c_2Elist_2Elist__size:(del>$i))).
thf(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))))).
thf(tp_c_2Elist_2Enub,type,(c_2Elist_2Enub:(del>$i))).
thf(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))))).
thf(tp_c_2Elist_2EoEL,type,(c_2Elist_2EoEL:(del>$i))).
thf(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)))))).
thf(tp_c_2Elist_2EoHD,type,(c_2Elist_2EoHD:(del>$i))).
thf(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))))).
thf(tp_c_2Elist_2EsplitAtPki,type,(c_2Elist_2EsplitAtPki:(del>(del>$i)))).
thf(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))))))).
thf(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))@(lam@(ty_2Eind__type_2Erecspace@A_27a)@(^ [V1a0_27:$i] : (ap@(c_2Ebool_2E_21@(arr@(ty_2Eind__type_2Erecspace@A_27a)@bool))@(lam@(arr@(ty_2Eind__type_2Erecspace@A_27a)@bool)@(^ [V2_27list_27:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@(c_2Ebool_2E_21@(ty_2Eind__type_2Erecspace@A_27a))@(lam@(ty_2Eind__type_2Erecspace@A_27a)@(^ [V3a0_27:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@(c_2Emin_2E_3D@(ty_2Eind__type_2Erecspace@A_27a))@V3a0_27)@(ap@(ap@(ap@(c_2Eind__type_2ECONSTR@A_27a)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(c_2Ebool_2EARB@A_27a))@(lam@ty_2Enum_2Enum@(^ [V4n:$i] : (c_2Eind__type_2EBOTTOM@A_27a))))))@(ap@(c_2Ebool_2E_3F@A_27a)@(lam@A_27a@(^ [V5a0:$i] : (ap@(c_2Ebool_2E_3F@(ty_2Eind__type_2Erecspace@A_27a))@(lam@(ty_2Eind__type_2Erecspace@A_27a)@(^ [V6a1:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Emin_2E_3D@(ty_2Eind__type_2Erecspace@A_27a))@V3a0_27)@(ap@(ap@(lam@A_27a@(^ [V7a0:$i] : (lam@(ty_2Eind__type_2Erecspace@A_27a)@(^ [V8a1:$i] : (ap@(ap@(ap@(c_2Eind__type_2ECONSTR@A_27a)@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@V7a0)@(ap@(ap@(c_2Eind__type_2EFCONS@(ty_2Eind__type_2Erecspace@A_27a))@V8a1)@(lam@ty_2Enum_2Enum@(^ [V9n:$i] : (c_2Eind__type_2EBOTTOM@A_27a)))))))))@V5a0)@V6a1)))@(ap@V2_27list_27@V6a1))))))))))@(ap@V2_27list_27@V3a0_27))))))@(ap@V2_27list_27@V1a0_27))))))))@V0rep)))))).
thf(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)))))))))))))).
thf(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)))))))))))))).
thf(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)))))))).
thf(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))))))))))))).
thf(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))))))))).
thf(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))))))))))))))))).
thf(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)))))))))))))))))).
thf(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))))))))))))))))))).
thf(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))@(lam@(arr@(ty_2Elist_2Elist@A_27a)@A_27b)@(^ [V2fn1:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Emin_2E_3D@A_27b)@(ap@V2fn1@(c_2Elist_2ENIL@A_27a)))@V0x))@(ap@(c_2Ebool_2E_21@A_27a)@(lam@A_27a@(^ [V3h:$i] : (ap@(c_2Ebool_2E_21@(ty_2Elist_2Elist@A_27a))@(lam@(ty_2Elist_2Elist@A_27a)@(^ [V4t:$i] : (ap@(ap@(c_2Emin_2E_3D@A_27b)@(ap@V2fn1@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V3h)@V4t)))@(ap@(ap@(ap@V1f@(ap@V2fn1@V4t))@V3h)@V4t)))))))))))))))))))).
thf(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)))))))).
thf(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))))))).
thf(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)))))))).
thf(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))))))).
thf(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))))))))).
thf(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)))))))))))).
thf(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)))))))))).
thf(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))))))))))).
thf(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))))))))))))).
thf(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))))))))))))).
thf(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))))))))))).
thf(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)))))))))))).
thf(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))))))))))))))).
thf(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)))))))))))))).
thf(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))))))))))))).
thf(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))))))))))))).
thf(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))))))))).
thf(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))))))))))))))).
thf(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)))))))))))))).
thf(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))))))))))))))))))))).
thf(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)))))))))).
thf(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)))))))))))))).
thf(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))))))))))))))).
thf(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))))))))))))).
thf(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))))))).
thf(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)))))))).
thf(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))))))))))).
thf(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))))))))).
thf(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))))))))).
thf(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))))))))).
thf(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))))))))))).
thf(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))))))))))).
thf(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))))))))))))).
thf(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))))))))))))).
thf(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))))))))).
thf(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))))))))).
thf(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)))))))))))))).
thf(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)))))))))))))).
thf(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)))))))))))))).
thf(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)))))).
thf(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))))).
thf(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)))))))))).
thf(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)))))))))).
thf(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)))))))))))).
thf(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)@(lam@A_27a@(^ [V1x:$i] : V1x)))@V0l) = V0l) & ((ap@(ap@(c_2Elist_2EMAP@A_27a@A_27a)@(c_2Ecombin_2EI@A_27a))@V0l) = V0l)))))).
thf(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)))))))))).
thf(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))))))))))).
thf(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)))))))))))))))))))).
thf(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))))))))))))))).
thf(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))))))))))))))).
thf(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))))))))))).
thf(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)))))))))))).
thf(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)))))))))))).
thf(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)))))))))).
thf(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))))))))))).
thf(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)))))))))))).
thf(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)@(lam@A_27a@(^ [V3x:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0P@V3x))@(ap@V1Q@V3x)))))@V2l)) <=> ((p@(ap@(ap@(c_2Elist_2EEVERY@A_27a)@V0P)@V2l)) & (p@(ap@(ap@(c_2Elist_2EEVERY@A_27a)@V1Q)@V2l)))))))))))).
thf(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)))))))))))).
thf(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)@(lam@A_27a@(^ [V3x:$i] : (ap@V0P@(ap@V1f@V3x)))))@V2l)))))))))))).
thf(conj_thm_2Elist_2EEVERY__SIMP,lemma,( ! [A_27a:del]: ( ! [V0c:$i] : ((mem@V0c@bool) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Elist_2EEVERY@A_27a)@(lam@A_27a@(^ [V2x:$i] : V0c)))@V1l)) <=> ((V1l = (c_2Elist_2ENIL@A_27a)) | (p@V0c))))))))).
thf(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)))))))))))).
thf(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)))))))))))).
thf(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)@(lam@A_27a@(^ [V3x:$i] : (ap@V0P@(ap@V1f@V3x)))))@V2l)))))))))))).
thf(conj_thm_2Elist_2EEXISTS__SIMP,lemma,( ! [A_27a:del]: ( ! [V0c:$i] : ((mem@V0c@bool) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Elist_2EEXISTS@A_27a)@(lam@A_27a@(^ [V2x:$i] : V0c)))@V1l)) <=> ((~~ (V1l = (c_2Elist_2ENIL@A_27a))) & (p@V0c))))))))).
thf(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)))))))))))).
thf(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)@(lam@A_27a@(^ [V2x:$i] : (ap@c_2Ebool_2E_7E@(ap@V0P@V2x)))))@V1l)))))))))).
thf(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)@(lam@A_27a@(^ [V2x:$i] : (ap@c_2Ebool_2E_7E@(ap@V0P@V2x)))))@V1l)))))))))).
thf(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))))))))))))).
thf(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))))))))))))).
thf(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))))))))))))).
thf(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))))))))).
thf(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)))))))))))))))))).
thf(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)))))))))))).
thf(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)))))))))))).
thf(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))))))))).
thf(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))))))))).
thf(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)))))))))))))))).
thf(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))))))).
thf(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))))))).
thf(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))))))).
thf(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)))))).
thf(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))))))))))))).
thf(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@(lam@(ty_2Elist_2Elist@A_27a)@(^ [V4l:$i] : (ap@(c_2Ebool_2E_21@A_27a)@(lam@A_27a@(^ [V5x:$i] : (ap@V0P@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V5x)@V4l)))))))@V3l))))))))))).
thf(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))))))))))))))).
thf(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))))))))))))))))).
thf(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)))))))))))))))))).
thf(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)))))))).
thf(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))))))))).
thf(conj_thm_2Elist_2EAPPEND__eq__NIL,conjecture,( ! [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))))))))))).
