include('Axioms/bit^2.ax').
thf(tp_c_2Epred__set_2EBIGINTER,type,(c_2Epred__set_2EBIGINTER:(del>$i))).
thf(mem_c_2Epred__set_2EBIGINTER,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2EBIGINTER@A_27a)@(arr@(arr@(arr@A_27a@bool)@bool)@(arr@A_27a@bool))))).
thf(tp_c_2Epred__set_2EBIGUNION,type,(c_2Epred__set_2EBIGUNION:(del>$i))).
thf(mem_c_2Epred__set_2EBIGUNION,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2EBIGUNION@A_27a)@(arr@(arr@(arr@A_27a@bool)@bool)@(arr@A_27a@bool))))).
thf(tp_c_2Epred__set_2EBIJ,type,(c_2Epred__set_2EBIJ:(del>(del>$i)))).
thf(mem_c_2Epred__set_2EBIJ,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Epred__set_2EBIJ@A_27a@A_27b)@(arr@(arr@A_27a@A_27b)@(arr@(arr@A_27a@bool)@(arr@(arr@A_27b@bool)@bool))))))).
thf(tp_c_2Epred__set_2ECARD,type,(c_2Epred__set_2ECARD:(del>$i))).
thf(mem_c_2Epred__set_2ECARD,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2ECARD@A_27a)@(arr@(arr@A_27a@bool)@ty_2Enum_2Enum)))).
thf(tp_c_2Epred__set_2ECHOICE,type,(c_2Epred__set_2ECHOICE:(del>$i))).
thf(mem_c_2Epred__set_2ECHOICE,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2ECHOICE@A_27a)@(arr@(arr@A_27a@bool)@A_27a)))).
thf(tp_c_2Epred__set_2ECOMPL,type,(c_2Epred__set_2ECOMPL:(del>$i))).
thf(mem_c_2Epred__set_2ECOMPL,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2ECOMPL@A_27a)@(arr@(arr@A_27a@bool)@(arr@A_27a@bool))))).
thf(tp_c_2Epred__set_2ECROSS,type,(c_2Epred__set_2ECROSS:(del>(del>$i)))).
thf(mem_c_2Epred__set_2ECROSS,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Epred__set_2ECROSS@A_27a@A_27b)@(arr@(arr@A_27a@bool)@(arr@(arr@A_27b@bool)@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@bool))))))).
thf(tp_c_2Epred__set_2EDELETE,type,(c_2Epred__set_2EDELETE:(del>$i))).
thf(mem_c_2Epred__set_2EDELETE,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2EDELETE@A_27a)@(arr@(arr@A_27a@bool)@(arr@A_27a@(arr@A_27a@bool)))))).
thf(tp_c_2Epred__set_2EDFUNSET,type,(c_2Epred__set_2EDFUNSET:(del>(del>$i)))).
thf(mem_c_2Epred__set_2EDFUNSET,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Epred__set_2EDFUNSET@A_27a@A_27b)@(arr@(arr@A_27a@bool)@(arr@(arr@A_27a@(arr@A_27b@bool))@(arr@(arr@A_27a@A_27b)@bool))))))).
thf(tp_c_2Epred__set_2EDIFF,type,(c_2Epred__set_2EDIFF:(del>$i))).
thf(mem_c_2Epred__set_2EDIFF,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2EDIFF@A_27a)@(arr@(arr@A_27a@bool)@(arr@(arr@A_27a@bool)@(arr@A_27a@bool)))))).
thf(tp_c_2Epred__set_2EDISJOINT,type,(c_2Epred__set_2EDISJOINT:(del>$i))).
thf(mem_c_2Epred__set_2EDISJOINT,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2EDISJOINT@A_27a)@(arr@(arr@A_27a@bool)@(arr@(arr@A_27a@bool)@bool))))).
thf(tp_c_2Epred__set_2EEMPTY,type,(c_2Epred__set_2EEMPTY:(del>$i))).
thf(mem_c_2Epred__set_2EEMPTY,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2EEMPTY@A_27a)@(arr@A_27a@bool)))).
thf(tp_c_2Epred__set_2EFINITE,type,(c_2Epred__set_2EFINITE:(del>$i))).
thf(mem_c_2Epred__set_2EFINITE,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2EFINITE@A_27a)@(arr@(arr@A_27a@bool)@bool)))).
thf(tp_c_2Epred__set_2EFUNSET,type,(c_2Epred__set_2EFUNSET:(del>(del>$i)))).
thf(mem_c_2Epred__set_2EFUNSET,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Epred__set_2EFUNSET@A_27a@A_27b)@(arr@(arr@A_27a@bool)@(arr@(arr@A_27b@bool)@(arr@(arr@A_27a@A_27b)@bool))))))).
thf(tp_c_2Epred__set_2EGSPEC,type,(c_2Epred__set_2EGSPEC:(del>(del>$i)))).
thf(mem_c_2Epred__set_2EGSPEC,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Epred__set_2EGSPEC@A_27a@A_27b)@(arr@(arr@A_27b@(ty_2Epair_2Eprod@A_27a@bool))@(arr@A_27a@bool)))))).
thf(tp_c_2Epred__set_2EIMAGE,type,(c_2Epred__set_2EIMAGE:(del>(del>$i)))).
thf(mem_c_2Epred__set_2EIMAGE,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@(arr@(arr@A_27a@A_27b)@(arr@(arr@A_27a@bool)@(arr@A_27b@bool))))))).
thf(tp_c_2Epred__set_2EINJ,type,(c_2Epred__set_2EINJ:(del>(del>$i)))).
thf(mem_c_2Epred__set_2EINJ,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Epred__set_2EINJ@A_27a@A_27b)@(arr@(arr@A_27a@A_27b)@(arr@(arr@A_27a@bool)@(arr@(arr@A_27b@bool)@bool))))))).
thf(tp_c_2Epred__set_2EINSERT,type,(c_2Epred__set_2EINSERT:(del>$i))).
thf(mem_c_2Epred__set_2EINSERT,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2EINSERT@A_27a)@(arr@A_27a@(arr@(arr@A_27a@bool)@(arr@A_27a@bool)))))).
thf(tp_c_2Epred__set_2EINTER,type,(c_2Epred__set_2EINTER:(del>$i))).
thf(mem_c_2Epred__set_2EINTER,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2EINTER@A_27a)@(arr@(arr@A_27a@bool)@(arr@(arr@A_27a@bool)@(arr@A_27a@bool)))))).
thf(tp_c_2Epred__set_2EITSET,type,(c_2Epred__set_2EITSET:(del>(del>$i)))).
thf(mem_c_2Epred__set_2EITSET,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Epred__set_2EITSET@A_27a@A_27b)@(arr@(arr@A_27a@(arr@A_27b@A_27b))@(arr@(arr@A_27a@bool)@(arr@A_27b@A_27b))))))).
thf(tp_c_2Epred__set_2ELINV,type,(c_2Epred__set_2ELINV:(del>(del>$i)))).
thf(mem_c_2Epred__set_2ELINV,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Epred__set_2ELINV@A_27a@A_27b)@(arr@(arr@A_27a@A_27b)@(arr@(arr@A_27a@bool)@(arr@A_27b@A_27a))))))).
thf(tp_c_2Epred__set_2ELINV__OPT,type,(c_2Epred__set_2ELINV__OPT:(del>(del>$i)))).
thf(mem_c_2Epred__set_2ELINV__OPT,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Epred__set_2ELINV__OPT@A_27a@A_27b)@(arr@(arr@A_27a@A_27b)@(arr@(arr@A_27a@bool)@(arr@A_27b@(ty_2Eoption_2Eoption@A_27a)))))))).
thf(tp_c_2Epred__set_2EMAX__SET,type,(c_2Epred__set_2EMAX__SET:$i)).
thf(mem_c_2Epred__set_2EMAX__SET,axiom,(mem@c_2Epred__set_2EMAX__SET@(arr@(arr@ty_2Enum_2Enum@bool)@ty_2Enum_2Enum))).
thf(tp_c_2Epred__set_2EMIN__SET,type,(c_2Epred__set_2EMIN__SET:$i)).
thf(mem_c_2Epred__set_2EMIN__SET,axiom,(mem@c_2Epred__set_2EMIN__SET@(arr@(arr@ty_2Enum_2Enum@bool)@ty_2Enum_2Enum))).
thf(tp_c_2Epred__set_2EPOW,type,(c_2Epred__set_2EPOW:(del>$i))).
thf(mem_c_2Epred__set_2EPOW,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2EPOW@A_27a)@(arr@(arr@A_27a@bool)@(arr@(arr@A_27a@bool)@bool))))).
thf(tp_c_2Epred__set_2EPREIMAGE,type,(c_2Epred__set_2EPREIMAGE:(del>(del>$i)))).
thf(mem_c_2Epred__set_2EPREIMAGE,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Epred__set_2EPREIMAGE@A_27a@A_27b)@(arr@(arr@A_27a@A_27b)@(arr@(arr@A_27b@bool)@(arr@A_27a@bool))))))).
thf(tp_c_2Epred__set_2EPROD__IMAGE,type,(c_2Epred__set_2EPROD__IMAGE:(del>$i))).
thf(mem_c_2Epred__set_2EPROD__IMAGE,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2EPROD__IMAGE@A_27a)@(arr@(arr@A_27a@ty_2Enum_2Enum)@(arr@(arr@A_27a@bool)@ty_2Enum_2Enum))))).
thf(tp_c_2Epred__set_2EPROD__SET,type,(c_2Epred__set_2EPROD__SET:$i)).
thf(mem_c_2Epred__set_2EPROD__SET,axiom,(mem@c_2Epred__set_2EPROD__SET@(arr@(arr@ty_2Enum_2Enum@bool)@ty_2Enum_2Enum))).
thf(tp_c_2Epred__set_2EPSUBSET,type,(c_2Epred__set_2EPSUBSET:(del>$i))).
thf(mem_c_2Epred__set_2EPSUBSET,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2EPSUBSET@A_27a)@(arr@(arr@A_27a@bool)@(arr@(arr@A_27a@bool)@bool))))).
thf(tp_c_2Epred__set_2EREL__RESTRICT,type,(c_2Epred__set_2EREL__RESTRICT:(del>$i))).
thf(mem_c_2Epred__set_2EREL__RESTRICT,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2EREL__RESTRICT@A_27a)@(arr@(arr@A_27a@(arr@A_27a@bool))@(arr@(arr@A_27a@bool)@(arr@A_27a@(arr@A_27a@bool))))))).
thf(tp_c_2Epred__set_2EREST,type,(c_2Epred__set_2EREST:(del>$i))).
thf(mem_c_2Epred__set_2EREST,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2EREST@A_27a)@(arr@(arr@A_27a@bool)@(arr@A_27a@bool))))).
thf(tp_c_2Epred__set_2ERINV,type,(c_2Epred__set_2ERINV:(del>(del>$i)))).
thf(mem_c_2Epred__set_2ERINV,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Epred__set_2ERINV@A_27a@A_27b)@(arr@(arr@A_27a@A_27b)@(arr@(arr@A_27a@bool)@(arr@A_27b@A_27a))))))).
thf(tp_c_2Epred__set_2ESING,type,(c_2Epred__set_2ESING:(del>$i))).
thf(mem_c_2Epred__set_2ESING,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2ESING@A_27a)@(arr@(arr@A_27a@bool)@bool)))).
thf(tp_c_2Epred__set_2ESUBSET,type,(c_2Epred__set_2ESUBSET:(del>$i))).
thf(mem_c_2Epred__set_2ESUBSET,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2ESUBSET@A_27a)@(arr@(arr@A_27a@bool)@(arr@(arr@A_27a@bool)@bool))))).
thf(tp_c_2Epred__set_2ESUM__IMAGE,type,(c_2Epred__set_2ESUM__IMAGE:(del>$i))).
thf(mem_c_2Epred__set_2ESUM__IMAGE,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2ESUM__IMAGE@A_27a)@(arr@(arr@A_27a@ty_2Enum_2Enum)@(arr@(arr@A_27a@bool)@ty_2Enum_2Enum))))).
thf(tp_c_2Epred__set_2ESUM__SET,type,(c_2Epred__set_2ESUM__SET:$i)).
thf(mem_c_2Epred__set_2ESUM__SET,axiom,(mem@c_2Epred__set_2ESUM__SET@(arr@(arr@ty_2Enum_2Enum@bool)@ty_2Enum_2Enum))).
thf(tp_c_2Epred__set_2ESURJ,type,(c_2Epred__set_2ESURJ:(del>(del>$i)))).
thf(mem_c_2Epred__set_2ESURJ,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Epred__set_2ESURJ@A_27a@A_27b)@(arr@(arr@A_27a@A_27b)@(arr@(arr@A_27a@bool)@(arr@(arr@A_27b@bool)@bool))))))).
thf(tp_c_2Epred__set_2EUNION,type,(c_2Epred__set_2EUNION:(del>$i))).
thf(mem_c_2Epred__set_2EUNION,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2EUNION@A_27a)@(arr@(arr@A_27a@bool)@(arr@(arr@A_27a@bool)@(arr@A_27a@bool)))))).
thf(tp_c_2Epred__set_2EUNIV,type,(c_2Epred__set_2EUNIV:(del>$i))).
thf(mem_c_2Epred__set_2EUNIV,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2EUNIV@A_27a)@(arr@A_27a@bool)))).
thf(tp_c_2Epred__set_2Echooser,type,(c_2Epred__set_2Echooser:(del>$i))).
thf(mem_c_2Epred__set_2Echooser,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2Echooser@A_27a)@(arr@(arr@A_27a@bool)@(arr@ty_2Enum_2Enum@A_27a))))).
thf(tp_c_2Epred__set_2Ecount,type,(c_2Epred__set_2Ecount:$i)).
thf(mem_c_2Epred__set_2Ecount,axiom,(mem@c_2Epred__set_2Ecount@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@bool)))).
thf(tp_c_2Epred__set_2Ecountable,type,(c_2Epred__set_2Ecountable:(del>$i))).
thf(mem_c_2Epred__set_2Ecountable,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2Ecountable@A_27a)@(arr@(arr@A_27a@bool)@bool)))).
thf(tp_c_2Epred__set_2Eenumerate,type,(c_2Epred__set_2Eenumerate:(del>$i))).
thf(mem_c_2Epred__set_2Eenumerate,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2Eenumerate@A_27a)@(arr@(arr@A_27a@bool)@(arr@ty_2Enum_2Enum@A_27a))))).
thf(tp_c_2Epred__set_2Eequiv__on,type,(c_2Epred__set_2Eequiv__on:(del>$i))).
thf(mem_c_2Epred__set_2Eequiv__on,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2Eequiv__on@A_27a)@(arr@(arr@A_27a@(arr@A_27a@bool))@(arr@(arr@A_27a@bool)@bool))))).
thf(tp_c_2Epred__set_2Eis__measure__maximal,type,(c_2Epred__set_2Eis__measure__maximal:(del>$i))).
thf(mem_c_2Epred__set_2Eis__measure__maximal,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2Eis__measure__maximal@A_27a)@(arr@(arr@A_27a@ty_2Enum_2Enum)@(arr@(arr@A_27a@bool)@(arr@A_27a@bool)))))).
thf(tp_c_2Epred__set_2Enum__to__pair,type,(c_2Epred__set_2Enum__to__pair:$i)).
thf(mem_c_2Epred__set_2Enum__to__pair,axiom,(mem@c_2Epred__set_2Enum__to__pair@(arr@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)))).
thf(tp_c_2Epred__set_2Epair__to__num,type,(c_2Epred__set_2Epair__to__num:$i)).
thf(mem_c_2Epred__set_2Epair__to__num,axiom,(mem@c_2Epred__set_2Epair__to__num@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@ty_2Enum_2Enum))).
thf(stp_fo_c_2Epred__set_2Epair__to__num,type,(fo__c_2Epred__set_2Epair__to__num:(tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2Epred__set_2Epair__to__num,axiom,( ! [X0:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ (fo__c_2Epred__set_2Epair__to__num @ X0)) = (ap @ c_2Epred__set_2Epair__to__num @ (inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ X0))))).
thf(tp_c_2Epred__set_2Epairwise,type,(c_2Epred__set_2Epairwise:(del>$i))).
thf(mem_c_2Epred__set_2Epairwise,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2Epairwise@A_27a)@(arr@(arr@A_27a@(arr@A_27a@bool))@(arr@(arr@A_27a@bool)@bool))))).
thf(tp_c_2Epred__set_2Epartition,type,(c_2Epred__set_2Epartition:(del>$i))).
thf(mem_c_2Epred__set_2Epartition,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2Epartition@A_27a)@(arr@(arr@A_27a@(arr@A_27a@bool))@(arr@(arr@A_27a@bool)@(arr@(arr@A_27a@bool)@bool)))))).
thf(tp_c_2Epred__set_2Eschroeder__close,type,(c_2Epred__set_2Eschroeder__close:(del>$i))).
thf(mem_c_2Epred__set_2Eschroeder__close,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2Eschroeder__close@A_27a)@(arr@(arr@A_27a@A_27a)@(arr@(arr@A_27a@bool)@(arr@A_27a@bool)))))).
thf(conj_thm_2Epred__set_2ESPECIFICATION,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1x)@V0P)) <=> (p@(ap@V0P@V1x))))))))).
thf(conj_thm_2Epred__set_2EIN__APP,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1P:$i] : ((mem@V1P@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@V1P)) <=> (p@(ap@V1P@V0x))))))))).
thf(conj_thm_2Epred__set_2EIN__ABS,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1P:$i] : ((mem@V1P@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@(lam@A_27a@(^ [V2x:$i] : (ap@V1P@V2x))))) <=> (p@(ap@V1P@V0x))))))))).
thf(conj_thm_2Epred__set_2EEXTENSION,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((V0s = V1t) <=> ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V0s)) <=> (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V1t)))))))))))).
thf(conj_thm_2Epred__set_2ENOT__EQUAL__SETS,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((~~ (V0s = V1t)) <=> (? [V2x:$i] : ((mem@V2x@A_27a) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V1t)) <=> (~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V0s))))))))))))).
thf(conj_thm_2Epred__set_2ENUM__SET__WOP,lemma,( ! [V0s:$i] : ((mem@V0s@(arr@ty_2Enum_2Enum@bool)) => ((? [V1n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@(c_2Ebool_2EIN@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V1n))@V0s))) <=> (? [V2n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@(c_2Ebool_2EIN@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V2n))@V0s)) & ( ! [V3m:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@(c_2Ebool_2EIN@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V3m))@V0s)) => (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V2n))@(inj__ty_2Enum_2Enum @ V3m))))))))))).
thf(ax_thm_2Epred__set_2EGSPECIFICATION,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27b@(ty_2Epair_2Eprod@A_27a@bool))) => ( ! [V1v:$i] : ((mem@V1v@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1v)@(ap@(c_2Epred__set_2EGSPEC@A_27a@A_27b)@V0f))) <=> (? [V2x:$i] : ((mem@V2x@A_27b) & ((ap@(ap@(c_2Epair_2E_2C@A_27a@bool)@V1v)@c_2Ebool_2ET) = (ap@V0f@V2x)))))))))))).
thf(conj_thm_2Epred__set_2EGSPECIFICATION__applied,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27b@(ty_2Epair_2Eprod@A_27a@bool))) => ( ! [V1v:$i] : ((mem@V1v@A_27a) => ((p@(ap@(ap@(c_2Epred__set_2EGSPEC@A_27a@A_27b)@V0f)@V1v)) <=> (? [V2x:$i] : ((mem@V2x@A_27b) & ((ap@(ap@(c_2Epair_2E_2C@A_27a@bool)@V1v)@c_2Ebool_2ET) = (ap@V0f@V2x)))))))))))).
thf(conj_thm_2Epred__set_2EGSPEC__ETA,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ((ap@(c_2Epred__set_2EGSPEC@A_27a@A_27a)@(lam@A_27a@(^ [V1x:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27a@bool)@V1x)@(ap@V0P@V1x))))) = V0P))))).
thf(conj_thm_2Epred__set_2EGSPEC__PAIR__ETA,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@(arr@A_27b@bool))) => ((ap@(c_2Epred__set_2EGSPEC@(ty_2Epair_2Eprod@A_27a@A_27b)@(ty_2Epair_2Eprod@A_27a@A_27b))@(ap@(c_2Epair_2EUNCURRY@A_27a@A_27b@(ty_2Epair_2Eprod@(ty_2Epair_2Eprod@A_27a@A_27b)@bool))@(lam@A_27a@(^ [V1x:$i] : (lam@A_27b@(^ [V2y:$i] : (ap@(ap@(c_2Epair_2E_2C@(ty_2Epair_2Eprod@A_27a@A_27b)@bool)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V1x)@V2y))@(ap@(ap@V0P@V1x)@V2y)))))))) = (ap@(c_2Epair_2EUNCURRY@A_27a@A_27b@bool)@V0P))))))).
thf(conj_thm_2Epred__set_2EIN__GSPEC__IFF,lemma,( ! [A_27a:del]: ( ! [V0y:$i] : ((mem@V0y@A_27a) => ( ! [V1P:$i] : ((mem@V1P@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0y)@(ap@(c_2Epred__set_2EGSPEC@A_27a@A_27a)@(lam@A_27a@(^ [V2x:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27a@bool)@V2x)@(ap@V1P@V2x))))))) <=> (p@(ap@V1P@V0y))))))))).
thf(conj_thm_2Epred__set_2EPAIR__IN__GSPEC__IFF,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1y:$i] : ((mem@V1y@A_27b) => ( ! [V2P:$i] : ((mem@V2P@(arr@A_27a@(arr@A_27b@bool))) => ((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27b))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V0x)@V1y))@(ap@(c_2Epred__set_2EGSPEC@(ty_2Epair_2Eprod@A_27a@A_27b)@(ty_2Epair_2Eprod@A_27a@A_27b))@(ap@(c_2Epair_2EUNCURRY@A_27a@A_27b@(ty_2Epair_2Eprod@(ty_2Epair_2Eprod@A_27a@A_27b)@bool))@(lam@A_27a@(^ [V3x:$i] : (lam@A_27b@(^ [V4y:$i] : (ap@(ap@(c_2Epair_2E_2C@(ty_2Epair_2Eprod@A_27a@A_27b)@bool)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V3x)@V4y))@(ap@(ap@V2P@V3x)@V4y)))))))))) <=> (p@(ap@(ap@V2P@V0x)@V1y)))))))))))).
thf(conj_thm_2Epred__set_2EIN__GSPEC,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1y:$i] : ((mem@V1y@A_27a) => ( ! [V2x:$i] : ((mem@V2x@A_27b) => ( ! [V3P:$i] : ((mem@V3P@(arr@A_27a@bool)) => (((p@(ap@V3P@V1y)) & (V2x = (ap@V0f@V1y))) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V2x)@(ap@(c_2Epred__set_2EGSPEC@A_27b@A_27a)@(lam@A_27a@(^ [V4x:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27b@bool)@(ap@V0f@V4x))@(ap@V3P@V4x))))))))))))))))))).
thf(conj_thm_2Epred__set_2EPAIR__IN__GSPEC__1,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0a:$i] : ((mem@V0a@A_27a) => ( ! [V1b:$i] : ((mem@V1b@A_27b) => ( ! [V2x:$i] : ((mem@V2x@A_27b) => ( ! [V3P:$i] : ((mem@V3P@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27b))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V0a)@V1b))@(ap@(c_2Epred__set_2EGSPEC@(ty_2Epair_2Eprod@A_27a@A_27b)@A_27a)@(lam@A_27a@(^ [V4y:$i] : (ap@(ap@(c_2Epair_2E_2C@(ty_2Epair_2Eprod@A_27a@A_27b)@bool)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V4y)@V2x))@(ap@V3P@V4y))))))) <=> ((p@(ap@V3P@V0a)) & (V1b = V2x)))))))))))))).
thf(conj_thm_2Epred__set_2EPAIR__IN__GSPEC__2,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0a:$i] : ((mem@V0a@A_27a) => ( ! [V1b:$i] : ((mem@V1b@A_27b) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ( ! [V3P:$i] : ((mem@V3P@(arr@A_27b@bool)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27b))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V0a)@V1b))@(ap@(c_2Epred__set_2EGSPEC@(ty_2Epair_2Eprod@A_27a@A_27b)@A_27b)@(lam@A_27b@(^ [V4y:$i] : (ap@(ap@(c_2Epair_2E_2C@(ty_2Epair_2Eprod@A_27a@A_27b)@bool)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V2x)@V4y))@(ap@V3P@V4y))))))) <=> ((p@(ap@V3P@V1b)) & (V0a = V2x)))))))))))))).
thf(conj_thm_2Epred__set_2EPAIR__IN__GSPEC__same,lemma,( ! [A_27a:del]: ( ! [V0a:$i] : ((mem@V0a@A_27a) => ( ! [V1b:$i] : ((mem@V1b@A_27a) => ( ! [V2P:$i] : ((mem@V2P@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V0a)@V1b))@(ap@(c_2Epred__set_2EGSPEC@(ty_2Epair_2Eprod@A_27a@A_27a)@A_27a)@(lam@A_27a@(^ [V3x:$i] : (ap@(ap@(c_2Epair_2E_2C@(ty_2Epair_2Eprod@A_27a@A_27a)@bool)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V3x)@V3x))@(ap@V2P@V3x))))))) <=> ((p@(ap@V2P@V0a)) & (V0a = V1b))))))))))).
thf(conj_thm_2Epred__set_2ESET__MINIMUM,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1M:$i] : ((mem@V1M@(arr@A_27a@ty_2Enum_2Enum)) => ((? [V2x:$i] : ((mem@V2x@A_27a) & (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V0s)))) <=> (? [V3x:$i] : ((mem@V3x@A_27a) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@V0s)) & ( ! [V4y:$i] : ((mem@V4y@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V4y)@V0s)) => (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@V1M@V3x))@(ap@V1M@V4y)))))))))))))))).
thf(ax_thm_2Epred__set_2EEMPTY__DEF,axiom,( ! [A_27a:del]: ((c_2Epred__set_2EEMPTY@A_27a) = (lam@A_27a@(^ [V0x:$i] : c_2Ebool_2EF))))).
thf(conj_thm_2Epred__set_2ENOT__IN__EMPTY,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => (~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@(c_2Epred__set_2EEMPTY@A_27a)))))))).
thf(conj_thm_2Epred__set_2EMEMBER__NOT__EMPTY,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((? [V1x:$i] : ((mem@V1x@A_27a) & (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1x)@V0s)))) <=> (~~ (V0s = (c_2Epred__set_2EEMPTY@A_27a)))))))).
thf(conj_thm_2Epred__set_2EEMPTY__applied,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ((p@(ap@(c_2Epred__set_2EEMPTY@A_27a)@V0x)) <=> $false))))).
thf(ax_thm_2Epred__set_2EUNIV__DEF,axiom,( ! [A_27a:del]: ((c_2Epred__set_2EUNIV@A_27a) = (lam@A_27a@(^ [V0x:$i] : c_2Ebool_2ET))))).
thf(conj_thm_2Epred__set_2EIN__UNIV,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@(c_2Epred__set_2EUNIV@A_27a))))))).
thf(conj_thm_2Epred__set_2EUNIV__applied,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => (p@(ap@(c_2Epred__set_2EUNIV@A_27a)@V0x)))))).
thf(conj_thm_2Epred__set_2EUNIV__NOT__EMPTY,lemma,( ! [A_27a:del]: (~~ ((c_2Epred__set_2EUNIV@A_27a) = (c_2Epred__set_2EEMPTY@A_27a))))).
thf(conj_thm_2Epred__set_2EEMPTY__NOT__UNIV,lemma,( ! [A_27a:del]: (~~ ((c_2Epred__set_2EEMPTY@A_27a) = (c_2Epred__set_2EUNIV@A_27a))))).
thf(conj_thm_2Epred__set_2EEQ__UNIV,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => (( ! [V1x:$i] : ((mem@V1x@A_27a) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1x)@V0s)))) <=> (V0s = (c_2Epred__set_2EUNIV@A_27a))))))).
thf(conj_thm_2Epred__set_2EIN__EQ__UNIV__IMP,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((V0s = (c_2Epred__set_2EUNIV@A_27a)) => ( ! [V1v:$i] : ((mem@V1v@A_27a) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1v)@V0s))))))))).
thf(ax_thm_2Epred__set_2ESUBSET__DEF,axiom,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V0s)@V1t)) <=> ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V0s)) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V1t)))))))))))).
thf(conj_thm_2Epred__set_2ESUBSET__THM,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1Q:$i] : ((mem@V1Q@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V0P)@V1Q)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V0P)) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V1Q)))))))))))).
thf(conj_thm_2Epred__set_2ESUBSET__applied,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V0s)@V1t)) <=> ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@V0s@V2x)) => (p@(ap@V1t@V2x)))))))))))).
thf(conj_thm_2Epred__set_2ESUBSET__TRANS,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ( ! [V2u:$i] : ((mem@V2u@(arr@A_27a@bool)) => (((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V0s)@V1t)) & (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V1t)@V2u))) => (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V0s)@V2u))))))))))).
thf(conj_thm_2Epred__set_2ESUBSET__REFL,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V0s)@V0s)))))).
thf(conj_thm_2Epred__set_2ESUBSET__ANTISYM,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => (((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V0s)@V1t)) & (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V1t)@V0s))) => (V0s = V1t)))))))).
thf(conj_thm_2Epred__set_2EEMPTY__SUBSET,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@(c_2Epred__set_2EEMPTY@A_27a))@V0s)))))).
thf(conj_thm_2Epred__set_2ESUBSET__EMPTY,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V0s)@(c_2Epred__set_2EEMPTY@A_27a))) <=> (V0s = (c_2Epred__set_2EEMPTY@A_27a))))))).
thf(conj_thm_2Epred__set_2ESUBSET__UNIV,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V0s)@(c_2Epred__set_2EUNIV@A_27a))))))).
thf(conj_thm_2Epred__set_2EUNIV__SUBSET,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@(c_2Epred__set_2EUNIV@A_27a))@V0s)) <=> (V0s = (c_2Epred__set_2EUNIV@A_27a))))))).
thf(conj_thm_2Epred__set_2EEQ__SUBSET__SUBSET,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((V0s = V1t) => ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V0s)@V1t)) & (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V1t)@V0s)))))))))).
thf(conj_thm_2Epred__set_2ESUBSET__SUBSET__EQ,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => (((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V0s)@V1t)) & (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V1t)@V0s))) <=> (V0s = V1t)))))))).
thf(conj_thm_2Epred__set_2ESUBSET__ADD,lemma,( ! [A_27a:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@(arr@A_27a@bool))) => ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2d:tp__ty_2Enum_2Enum] : (( ! [V3n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@(ap@V0f@(inj__ty_2Enum_2Enum @ V3n)))@(ap@V0f@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V3n)))))) => (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@(ap@V0f@(inj__ty_2Enum_2Enum @ V1n)))@(ap@V0f@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V1n))@(inj__ty_2Enum_2Enum @ V2d)))))))))))).
thf(conj_thm_2Epred__set_2EK__SUBSET,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@bool) => ( ! [V1y:$i] : ((mem@V1y@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@(ap@(c_2Ecombin_2EK@bool@A_27a)@V0x))@V1y)) <=> ((~~ (p@V0x)) | (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@(c_2Epred__set_2EUNIV@A_27a))@V1y)))))))))).
thf(conj_thm_2Epred__set_2ESUBSET__K,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@(arr@A_27a@bool)) => ( ! [V1y:$i] : ((mem@V1y@bool) => ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V0x)@(ap@(c_2Ecombin_2EK@bool@A_27a)@V1y))) <=> ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V0x)@(c_2Epred__set_2EEMPTY@A_27a))) | (p@V1y))))))))).
thf(ax_thm_2Epred__set_2EPSUBSET__DEF,axiom,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2EPSUBSET@A_27a)@V0s)@V1t)) <=> ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V0s)@V1t)) & (~ (V0s = V1t)))))))))).
thf(conj_thm_2Epred__set_2EPSUBSET__TRANS,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ( ! [V2u:$i] : ((mem@V2u@(arr@A_27a@bool)) => (((p@(ap@(ap@(c_2Epred__set_2EPSUBSET@A_27a)@V0s)@V1t)) & (p@(ap@(ap@(c_2Epred__set_2EPSUBSET@A_27a)@V1t)@V2u))) => (p@(ap@(ap@(c_2Epred__set_2EPSUBSET@A_27a)@V0s)@V2u))))))))))).
thf(conj_thm_2Epred__set_2EPSUBSET__IRREFL,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => (~~ (p@(ap@(ap@(c_2Epred__set_2EPSUBSET@A_27a)@V0s)@V0s))))))).
thf(conj_thm_2Epred__set_2ENOT__PSUBSET__EMPTY,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => (~~ (p@(ap@(ap@(c_2Epred__set_2EPSUBSET@A_27a)@V0s)@(c_2Epred__set_2EEMPTY@A_27a)))))))).
thf(conj_thm_2Epred__set_2ENOT__UNIV__PSUBSET,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => (~~ (p@(ap@(ap@(c_2Epred__set_2EPSUBSET@A_27a)@(c_2Epred__set_2EUNIV@A_27a))@V0s))))))).
thf(conj_thm_2Epred__set_2EPSUBSET__UNIV,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2EPSUBSET@A_27a)@V0s)@(c_2Epred__set_2EUNIV@A_27a))) <=> (? [V1x:$i] : ((mem@V1x@A_27a) & (~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1x)@V0s)))))))))).
thf(ax_thm_2Epred__set_2EUNION__DEF,axiom,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V0s)@V1t) = (ap@(c_2Epred__set_2EGSPEC@A_27a@A_27a)@(lam@A_27a@(^ [V2x:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27a@bool)@V2x)@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V0s))@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V1t))))))))))))).
thf(conj_thm_2Epred__set_2EIN__UNION,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V0s)@V1t))) <=> ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V0s)) | (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V1t)))))))))))).
thf(conj_thm_2Epred__set_2EUNION__applied,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V0s)@V1t)@V2x)) <=> ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V0s)) | (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V1t)))))))))))).
thf(conj_thm_2Epred__set_2EUNION__ASSOC,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ( ! [V2u:$i] : ((mem@V2u@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V0s)@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V1t)@V2u)) = (ap@(ap@(c_2Epred__set_2EUNION@A_27a)@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V0s)@V1t))@V2u)))))))))).
thf(conj_thm_2Epred__set_2EUNION__IDEMPOT,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V0s)@V0s) = V0s))))).
thf(conj_thm_2Epred__set_2EUNION__COMM,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V0s)@V1t) = (ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V1t)@V0s)))))))).
thf(conj_thm_2Epred__set_2ESUBSET__UNION,lemma,( ! [A_27a:del]: (( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V0s)@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V0s)@V1t))))))) & ( ! [V2s:$i] : ((mem@V2s@(arr@A_27a@bool)) => ( ! [V3t:$i] : ((mem@V3t@(arr@A_27a@bool)) => (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V2s)@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V3t)@V2s)))))))))).
thf(conj_thm_2Epred__set_2EUNION__SUBSET,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ( ! [V2u:$i] : ((mem@V2u@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V0s)@V1t))@V2u)) <=> ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V0s)@V2u)) & (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V1t)@V2u)))))))))))).
thf(conj_thm_2Epred__set_2ESUBSET__UNION__ABSORPTION,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V0s)@V1t)) <=> ((ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V0s)@V1t) = V1t)))))))).
thf(conj_thm_2Epred__set_2EUNION__EMPTY,lemma,( ! [A_27a:del]: (( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EUNION@A_27a)@(c_2Epred__set_2EEMPTY@A_27a))@V0s) = V0s))) & ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V1s)@(c_2Epred__set_2EEMPTY@A_27a)) = V1s)))))).
thf(conj_thm_2Epred__set_2EUNION__UNIV,lemma,( ! [A_27a:del]: (( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EUNION@A_27a)@(c_2Epred__set_2EUNIV@A_27a))@V0s) = (c_2Epred__set_2EUNIV@A_27a)))) & ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V1s)@(c_2Epred__set_2EUNIV@A_27a)) = (c_2Epred__set_2EUNIV@A_27a))))))).
thf(conj_thm_2Epred__set_2EEMPTY__UNION,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => (((ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V0s)@V1t) = (c_2Epred__set_2EEMPTY@A_27a)) <=> ((V0s = (c_2Epred__set_2EEMPTY@A_27a)) & (V1t = (c_2Epred__set_2EEMPTY@A_27a)))))))))).
thf(conj_thm_2Epred__set_2EFORALL__IN__UNION,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27a@bool)) => (( ! [V3x:$i] : ((mem@V3x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V1s)@V2t))) => (p@(ap@V0P@V3x))))) <=> (( ! [V4x:$i] : ((mem@V4x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V4x)@V1s)) => (p@(ap@V0P@V4x))))) & ( ! [V5x:$i] : ((mem@V5x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V5x)@V2t)) => (p@(ap@V0P@V5x))))))))))))))).
thf(ax_thm_2Epred__set_2EINTER__DEF,axiom,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V0s)@V1t) = (ap@(c_2Epred__set_2EGSPEC@A_27a@A_27a)@(lam@A_27a@(^ [V2x:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27a@bool)@V2x)@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V0s))@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V1t))))))))))))).
thf(conj_thm_2Epred__set_2EIN__INTER,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V0s)@V1t))) <=> ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V0s)) & (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V1t)))))))))))).
thf(conj_thm_2Epred__set_2EINTER__applied,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V0s)@V1t)@V2x)) <=> ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V0s)) & (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V1t)))))))))))).
thf(conj_thm_2Epred__set_2EINTER__ASSOC,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ( ! [V2u:$i] : ((mem@V2u@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V0s)@(ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V1t)@V2u)) = (ap@(ap@(c_2Epred__set_2EINTER@A_27a)@(ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V0s)@V1t))@V2u)))))))))).
thf(conj_thm_2Epred__set_2EINTER__IDEMPOT,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V0s)@V0s) = V0s))))).
thf(conj_thm_2Epred__set_2EINTER__COMM,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V0s)@V1t) = (ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V1t)@V0s)))))))).
thf(conj_thm_2Epred__set_2EINTER__SUBSET,lemma,( ! [A_27a:del]: (( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@(ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V0s)@V1t))@V0s)))))) & ( ! [V2s:$i] : ((mem@V2s@(arr@A_27a@bool)) => ( ! [V3t:$i] : ((mem@V3t@(arr@A_27a@bool)) => (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@(ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V3t)@V2s))@V2s))))))))).
thf(conj_thm_2Epred__set_2ESUBSET__INTER,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ( ! [V2u:$i] : ((mem@V2u@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V0s)@(ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V1t)@V2u))) <=> ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V0s)@V1t)) & (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V0s)@V2u)))))))))))).
thf(conj_thm_2Epred__set_2ESUBSET__INTER__ABSORPTION,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V0s)@V1t)) <=> ((ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V0s)@V1t) = V0s)))))))).
thf(conj_thm_2Epred__set_2ESUBSET__INTER1,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V0s)@V1t)) => ((ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V0s)@V1t) = V0s)))))))).
thf(conj_thm_2Epred__set_2ESUBSET__INTER2,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V0s)@V1t)) => ((ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V1t)@V0s) = V0s)))))))).
thf(conj_thm_2Epred__set_2EINTER__EMPTY,lemma,( ! [A_27a:del]: (( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EINTER@A_27a)@(c_2Epred__set_2EEMPTY@A_27a))@V0s) = (c_2Epred__set_2EEMPTY@A_27a)))) & ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V1s)@(c_2Epred__set_2EEMPTY@A_27a)) = (c_2Epred__set_2EEMPTY@A_27a))))))).
thf(conj_thm_2Epred__set_2EINTER__UNIV,lemma,( ! [A_27a:del]: (( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EINTER@A_27a)@(c_2Epred__set_2EUNIV@A_27a))@V0s) = V0s))) & ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V1s)@(c_2Epred__set_2EUNIV@A_27a)) = V1s)))))).
thf(conj_thm_2Epred__set_2EUNION__OVER__INTER,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ( ! [V2u:$i] : ((mem@V2u@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V0s)@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V1t)@V2u)) = (ap@(ap@(c_2Epred__set_2EUNION@A_27a)@(ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V0s)@V1t))@(ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V0s)@V2u))))))))))).
thf(conj_thm_2Epred__set_2EINTER__OVER__UNION,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ( ! [V2u:$i] : ((mem@V2u@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V0s)@(ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V1t)@V2u)) = (ap@(ap@(c_2Epred__set_2EINTER@A_27a)@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V0s)@V1t))@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V0s)@V2u))))))))))).
thf(ax_thm_2Epred__set_2EDISJOINT__DEF,axiom,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@V0s)@V1t)) <=> ((ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V0s)@V1t) = (c_2Epred__set_2EEMPTY@A_27a))))))))).
thf(conj_thm_2Epred__set_2EIN__DISJOINT,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@V0s)@V1t)) <=> (~~ (? [V2x:$i] : ((mem@V2x@A_27a) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V0s)) & (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V1t))))))))))))).
thf(conj_thm_2Epred__set_2EDISJOINT__SYM,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@V0s)@V1t)) <=> (p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@V1t)@V0s))))))))).
thf(conj_thm_2Epred__set_2EDISJOINT__ALT,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@V0s)@V1t)) <=> ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V0s)) => (~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V1t))))))))))))).
thf(conj_thm_2Epred__set_2EDISJOINT__EMPTY,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@(c_2Epred__set_2EEMPTY@A_27a))@V0s)) & (p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@V0s)@(c_2Epred__set_2EEMPTY@A_27a)))))))).
thf(conj_thm_2Epred__set_2EDISJOINT__EMPTY__REFL,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((V0s = (c_2Epred__set_2EEMPTY@A_27a)) <=> (p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@V0s)@V0s))))))).
thf(conj_thm_2Epred__set_2EDISJOINT__EMPTY__REFL__RWT,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@V0s)@V0s)) <=> (V0s = (c_2Epred__set_2EEMPTY@A_27a))))))).
thf(conj_thm_2Epred__set_2EDISJOINT__UNION,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ( ! [V2u:$i] : ((mem@V2u@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V0s)@V1t))@V2u)) <=> ((p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@V0s)@V2u)) & (p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@V1t)@V2u)))))))))))).
thf(conj_thm_2Epred__set_2EDISJOINT__UNION__BOTH,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ( ! [V2u:$i] : ((mem@V2u@(arr@A_27a@bool)) => (((p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V0s)@V1t))@V2u)) <=> ((p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@V0s)@V2u)) & (p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@V1t)@V2u)))) & ((p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@V2u)@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V0s)@V1t))) <=> ((p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@V0s)@V2u)) & (p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@V1t)@V2u))))))))))))).
thf(conj_thm_2Epred__set_2EDISJOINT__SUBSET,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ( ! [V2u:$i] : ((mem@V2u@(arr@A_27a@bool)) => (((p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@V0s)@V1t)) & (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V2u)@V1t))) => (p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@V0s)@V2u))))))))))).
thf(ax_thm_2Epred__set_2EDIFF__DEF,axiom,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@V0s)@V1t) = (ap@(c_2Epred__set_2EGSPEC@A_27a@A_27a)@(lam@A_27a@(^ [V2x:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27a@bool)@V2x)@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V0s))@(ap@c_2Ebool_2E_7E@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V1t)))))))))))))).
thf(conj_thm_2Epred__set_2EIN__DIFF,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@V0s)@V1t))) <=> ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V0s)) & (~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V1t))))))))))))).
thf(conj_thm_2Epred__set_2EDIFF__applied,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@V0s)@V1t)@V2x)) <=> ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V0s)) & (~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V1t))))))))))))).
thf(conj_thm_2Epred__set_2EDIFF__EMPTY,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@V0s)@(c_2Epred__set_2EEMPTY@A_27a)) = V0s))))).
thf(conj_thm_2Epred__set_2EEMPTY__DIFF,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@(c_2Epred__set_2EEMPTY@A_27a))@V0s) = (c_2Epred__set_2EEMPTY@A_27a)))))).
thf(conj_thm_2Epred__set_2EDIFF__UNIV,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@V0s)@(c_2Epred__set_2EUNIV@A_27a)) = (c_2Epred__set_2EEMPTY@A_27a)))))).
thf(conj_thm_2Epred__set_2EDIFF__DIFF,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@(ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@V0s)@V1t))@V1t) = (ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@V0s)@V1t)))))))).
thf(conj_thm_2Epred__set_2EDIFF__EQ__EMPTY,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@V0s)@V0s) = (c_2Epred__set_2EEMPTY@A_27a)))))).
thf(conj_thm_2Epred__set_2EDIFF__SUBSET,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@(ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@V0s)@V1t))@V0s)))))))).
thf(conj_thm_2Epred__set_2EUNION__DIFF,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V0s)@V1t)) => (((ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V0s)@(ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@V1t)@V0s)) = V1t) & ((ap@(ap@(c_2Epred__set_2EUNION@A_27a)@(ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@V1t)@V0s))@V0s) = V1t))))))))).
thf(conj_thm_2Epred__set_2EDIFF__DIFF__SUBSET,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V1t)@V0s)) => ((ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@V0s)@(ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@V0s)@V1t)) = V1t)))))))).
thf(conj_thm_2Epred__set_2EDIFF__UNION,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@(arr@A_27a@bool)) => ( ! [V1y:$i] : ((mem@V1y@(arr@A_27a@bool)) => ( ! [V2z:$i] : ((mem@V2z@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@V0x)@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V1y)@V2z)) = (ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@(ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@V0x)@V1y))@V2z)))))))))).
thf(conj_thm_2Epred__set_2EDIFF__COMM,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@(arr@A_27a@bool)) => ( ! [V1y:$i] : ((mem@V1y@(arr@A_27a@bool)) => ( ! [V2z:$i] : ((mem@V2z@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@(ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@V0x)@V1y))@V2z) = (ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@(ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@V0x)@V2z))@V1y)))))))))).
thf(conj_thm_2Epred__set_2EDIFF__SAME__UNION,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@(arr@A_27a@bool)) => ( ! [V1y:$i] : ((mem@V1y@(arr@A_27a@bool)) => (((ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V0x)@V1y))@V0x) = (ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@V1y)@V0x)) & ((ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V0x)@V1y))@V1y) = (ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@V0x)@V1y))))))))).
thf(conj_thm_2Epred__set_2EDIFF__INTER,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ( ! [V2g:$i] : ((mem@V2g@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EINTER@A_27a)@(ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@V0s)@V1t))@V2g) = (ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@(ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V0s)@V2g))@V1t)))))))))).
thf(conj_thm_2Epred__set_2EDIFF__INTER2,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@V0s)@(ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V1t)@V0s)) = (ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@V0s)@V1t)))))))).
thf(conj_thm_2Epred__set_2EDISJOINT__DIFF,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@V1t)@(ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@V0s)@V1t))) & (p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@(ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@V0s)@V1t))@V1t))))))))).
thf(conj_thm_2Epred__set_2EDISJOINT__DIFFS,lemma,( ! [A_27a:del]: ( ! [V0g:$i] : ((mem@V0g@(arr@ty_2Enum_2Enum@(arr@A_27a@bool))) => ( ! [V1f:$i] : ((mem@V1f@(arr@ty_2Enum_2Enum@(arr@A_27a@bool))) => ( ! [V2m:tp__ty_2Enum_2Enum] : ( ! [V3n:tp__ty_2Enum_2Enum] : ((( ! [V4n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@(ap@V1f@(inj__ty_2Enum_2Enum @ V4n)))@(ap@V1f@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V4n)))))) & (( ! [V5n:tp__ty_2Enum_2Enum] : ((ap@V0g@(inj__ty_2Enum_2Enum @ V5n)) = (ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@(ap@V1f@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V5n))))@(ap@V1f@(inj__ty_2Enum_2Enum @ V5n))))) & (~~ (V2m = V3n)))) => (p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@(ap@V0g@(inj__ty_2Enum_2Enum @ V2m)))@(ap@V0g@(inj__ty_2Enum_2Enum @ V3n))))))))))))).
thf(ax_thm_2Epred__set_2EINSERT__DEF,axiom,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@V1s) = (ap@(c_2Epred__set_2EGSPEC@A_27a@A_27a)@(lam@A_27a@(^ [V2y:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27a@bool)@V2y)@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@(c_2Emin_2E_3D@A_27a)@V2y)@V0x))@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2y)@V1s))))))))))))).
thf(conj_thm_2Epred__set_2EIN__INSERT,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1y:$i] : ((mem@V1y@A_27a) => ( ! [V2s:$i] : ((mem@V2s@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V1y)@V2s))) <=> ((V0x = V1y) | (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@V2s)))))))))))).
thf(conj_thm_2Epred__set_2EINSERT__applied,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1y:$i] : ((mem@V1y@A_27a) => ( ! [V2s:$i] : ((mem@V2s@(arr@A_27a@bool)) => ((p@(ap@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V1y)@V2s)@V0x)) <=> ((V0x = V1y) | (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@V2s)))))))))))).
thf(conj_thm_2Epred__set_2ECOMPONENT,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@V1s))))))))).
thf(conj_thm_2Epred__set_2ESET__CASES,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((V0s = (c_2Epred__set_2EEMPTY@A_27a)) | (? [V1x:$i] : ((mem@V1x@A_27a) & (? [V2t:$i] : ((mem@V2t@(arr@A_27a@bool)) & ((V0s = (ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V1x)@V2t)) & (~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1x)@V2t))))))))))))).
thf(conj_thm_2Epred__set_2EDECOMPOSITION,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1x)@V0s)) <=> (? [V2t:$i] : ((mem@V2t@(arr@A_27a@bool)) & ((V0s = (ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V1x)@V2t)) & (~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1x)@V2t))))))))))))).
thf(conj_thm_2Epred__set_2EABSORPTION,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@V1s)) <=> ((ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@V1s) = V1s)))))))).
thf(conj_thm_2Epred__set_2EABSORPTION__RWT,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@V1s)) => ((ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@V1s) = V1s)))))))).
thf(conj_thm_2Epred__set_2EINSERT__INSERT,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@V1s)) = (ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@V1s)))))))).
thf(conj_thm_2Epred__set_2EINSERT__COMM,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1y:$i] : ((mem@V1y@A_27a) => ( ! [V2s:$i] : ((mem@V2s@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V1y)@V2s)) = (ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V1y)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@V2s))))))))))).
thf(conj_thm_2Epred__set_2EINSERT__UNIV,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ((ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@(c_2Epred__set_2EUNIV@A_27a)) = (c_2Epred__set_2EUNIV@A_27a)))))).
thf(conj_thm_2Epred__set_2ENOT__INSERT__EMPTY,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => (~~ ((ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@V1s) = (c_2Epred__set_2EEMPTY@A_27a))))))))).
thf(conj_thm_2Epred__set_2ENOT__EMPTY__INSERT,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => (~~ ((c_2Epred__set_2EEMPTY@A_27a) = (ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@V1s))))))))).
thf(conj_thm_2Epred__set_2EINSERT__UNION,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EUNION@A_27a)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@V1s))@V2t) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(arr@A_27a@bool))@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@V2t))@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V1s)@V2t))@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V1s)@V2t)))))))))))).
thf(conj_thm_2Epred__set_2EINSERT__UNION__EQ,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EUNION@A_27a)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@V1s))@V2t) = (ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V1s)@V2t))))))))))).
thf(conj_thm_2Epred__set_2EINSERT__INTER,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EINTER@A_27a)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@V1s))@V2t) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(arr@A_27a@bool))@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@V2t))@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@(ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V1s)@V2t)))@(ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V1s)@V2t))))))))))).
thf(conj_thm_2Epred__set_2EDISJOINT__INSERT,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@V1s))@V2t)) <=> ((p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@V1s)@V2t)) & (~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@V2t))))))))))))).
thf(conj_thm_2Epred__set_2EDISJOINT__INSERT_27,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@V2t)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@V1s))) <=> ((p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@V2t)@V1s)) & (~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@V2t))))))))))))).
thf(conj_thm_2Epred__set_2EINSERT__SUBSET,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@V1s))@V2t)) <=> ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@V2t)) & (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V1s)@V2t)))))))))))).
thf(conj_thm_2Epred__set_2ESUBSET__INSERT,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ((~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@V1s))) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V1s)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@V2t))) <=> (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V1s)@V2t)))))))))))).
thf(conj_thm_2Epred__set_2EINSERT__DIFF,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V2x)@V0s))@V1t) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(arr@A_27a@bool))@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V1t))@(ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@V0s)@V1t))@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V2x)@(ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@V0s)@V1t)))))))))))).
thf(conj_thm_2Epred__set_2EUNIV__BOOL,lemma,((c_2Epred__set_2EUNIV@bool) = (ap@(ap@(c_2Epred__set_2EINSERT@bool)@c_2Ebool_2ET)@(ap@(ap@(c_2Epred__set_2EINSERT@bool)@c_2Ebool_2EF)@(c_2Epred__set_2EEMPTY@bool))))).
thf(conj_thm_2Epred__set_2EFORALL__IN__INSERT,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1a:$i] : ((mem@V1a@A_27a) => ( ! [V2s:$i] : ((mem@V2s@(arr@A_27a@bool)) => (( ! [V3x:$i] : ((mem@V3x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V1a)@V2s))) => (p@(ap@V0P@V3x))))) <=> ((p@(ap@V0P@V1a)) & ( ! [V4x:$i] : ((mem@V4x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V4x)@V2s)) => (p@(ap@V0P@V4x))))))))))))))).
thf(conj_thm_2Epred__set_2EEXISTS__IN__INSERT,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1a:$i] : ((mem@V1a@A_27a) => ( ! [V2s:$i] : ((mem@V2s@(arr@A_27a@bool)) => ((? [V3x:$i] : ((mem@V3x@A_27a) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V1a)@V2s))) & (p@(ap@V0P@V3x))))) <=> ((p@(ap@V0P@V1a)) | (? [V4x:$i] : ((mem@V4x@A_27a) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V4x)@V2s)) & (p@(ap@V0P@V4x))))))))))))))).
thf(ax_thm_2Epred__set_2EDELETE__DEF,axiom,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ((ap@(ap@(c_2Epred__set_2EDELETE@A_27a)@V0s)@V1x) = (ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@V0s)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V1x)@(c_2Epred__set_2EEMPTY@A_27a)))))))))).
thf(conj_thm_2Epred__set_2EIN__DELETE,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ( ! [V2y:$i] : ((mem@V2y@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1x)@(ap@(ap@(c_2Epred__set_2EDELETE@A_27a)@V0s)@V2y))) <=> ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1x)@V0s)) & (~~ (V1x = V2y)))))))))))).
thf(conj_thm_2Epred__set_2EDELETE__applied,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ( ! [V2y:$i] : ((mem@V2y@A_27a) => ((p@(ap@(ap@(ap@(c_2Epred__set_2EDELETE@A_27a)@V0s)@V2y)@V1x)) <=> ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1x)@V0s)) & (~~ (V1x = V2y)))))))))))).
thf(conj_thm_2Epred__set_2EDELETE__NON__ELEMENT,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ((~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@V1s))) <=> ((ap@(ap@(c_2Epred__set_2EDELETE@A_27a)@V1s)@V0x) = V1s)))))))).
thf(conj_thm_2Epred__set_2EDELETE__NON__ELEMENT__RWT,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ((~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1x)@V0s))) => ((ap@(ap@(c_2Epred__set_2EDELETE@A_27a)@V0s)@V1x) = V0s)))))))).
thf(conj_thm_2Epred__set_2EIN__DELETE__EQ,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ( ! [V2x_27:$i] : ((mem@V2x_27@A_27a) => (((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1x)@V0s)) <=> (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x_27)@V0s))) <=> ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1x)@(ap@(ap@(c_2Epred__set_2EDELETE@A_27a)@V0s)@V2x_27))) <=> (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x_27)@(ap@(ap@(c_2Epred__set_2EDELETE@A_27a)@V0s)@V1x))))))))))))).
thf(conj_thm_2Epred__set_2EEMPTY__DELETE,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ((ap@(ap@(c_2Epred__set_2EDELETE@A_27a)@(c_2Epred__set_2EEMPTY@A_27a))@V0x) = (c_2Epred__set_2EEMPTY@A_27a)))))).
thf(conj_thm_2Epred__set_2EELT__IN__DELETE,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => (~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@(ap@(ap@(c_2Epred__set_2EDELETE@A_27a)@V1s)@V0x)))))))))).
thf(conj_thm_2Epred__set_2EDELETE__DELETE,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EDELETE@A_27a)@(ap@(ap@(c_2Epred__set_2EDELETE@A_27a)@V1s)@V0x))@V0x) = (ap@(ap@(c_2Epred__set_2EDELETE@A_27a)@V1s)@V0x)))))))).
thf(conj_thm_2Epred__set_2EDELETE__COMM,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1y:$i] : ((mem@V1y@A_27a) => ( ! [V2s:$i] : ((mem@V2s@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EDELETE@A_27a)@(ap@(ap@(c_2Epred__set_2EDELETE@A_27a)@V2s)@V0x))@V1y) = (ap@(ap@(c_2Epred__set_2EDELETE@A_27a)@(ap@(ap@(c_2Epred__set_2EDELETE@A_27a)@V2s)@V1y))@V0x)))))))))).
thf(conj_thm_2Epred__set_2EDELETE__SUBSET,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@(ap@(ap@(c_2Epred__set_2EDELETE@A_27a)@V1s)@V0x))@V1s)))))))).
thf(conj_thm_2Epred__set_2ESUBSET__DELETE,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V1s)@(ap@(ap@(c_2Epred__set_2EDELETE@A_27a)@V2t)@V0x))) <=> ((~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@V1s))) & (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V1s)@V2t)))))))))))).
thf(conj_thm_2Epred__set_2ESUBSET__INSERT__DELETE,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V1s)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@V2t))) <=> (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@(ap@(ap@(c_2Epred__set_2EDELETE@A_27a)@V1s)@V0x))@V2t))))))))))).
thf(conj_thm_2Epred__set_2ESUBSET__OF__INSERT,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V1s)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@V1s))))))))).
thf(conj_thm_2Epred__set_2EDIFF__INSERT,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@V0s)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V2x)@V1t)) = (ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@(ap@(ap@(c_2Epred__set_2EDELETE@A_27a)@V0s)@V2x))@V1t)))))))))).
thf(conj_thm_2Epred__set_2EPSUBSET__INSERT__SUBSET,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2EPSUBSET@A_27a)@V0s)@V1t)) <=> (? [V2x:$i] : ((mem@V2x@A_27a) & ((~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V0s))) & (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V2x)@V0s))@V1t)))))))))))).
thf(conj_thm_2Epred__set_2EPSUBSET__MEMBER,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2EPSUBSET@A_27a)@V0s)@V1t)) <=> ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V0s)@V1t)) & (? [V2y:$i] : ((mem@V2y@A_27a) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2y)@V1t)) & (~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2y)@V0s)))))))))))))).
thf(conj_thm_2Epred__set_2EDELETE__INSERT,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1y:$i] : ((mem@V1y@A_27a) => ( ! [V2s:$i] : ((mem@V2s@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EDELETE@A_27a)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@V2s))@V1y) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(arr@A_27a@bool))@(ap@(ap@(c_2Emin_2E_3D@A_27a)@V0x)@V1y))@(ap@(ap@(c_2Epred__set_2EDELETE@A_27a)@V2s)@V1y))@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@(ap@(ap@(c_2Epred__set_2EDELETE@A_27a)@V2s)@V1y)))))))))))).
thf(conj_thm_2Epred__set_2EINSERT__DELETE,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@V1s)) => ((ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@(ap@(ap@(c_2Epred__set_2EDELETE@A_27a)@V1s)@V0x)) = V1s)))))))).
thf(conj_thm_2Epred__set_2EDELETE__INTER,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((ap@(ap@(c_2Epred__set_2EINTER@A_27a)@(ap@(ap@(c_2Epred__set_2EDELETE@A_27a)@V0s)@V2x))@V1t) = (ap@(ap@(c_2Epred__set_2EDELETE@A_27a)@(ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V0s)@V1t))@V2x)))))))))).
thf(conj_thm_2Epred__set_2EDISJOINT__DELETE__SYM,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@(ap@(ap@(c_2Epred__set_2EDELETE@A_27a)@V0s)@V2x))@V1t)) <=> (p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@(ap@(ap@(c_2Epred__set_2EDELETE@A_27a)@V1t)@V2x))@V0s))))))))))).
thf(ax_thm_2Epred__set_2ECHOICE__DEF,axiom,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((~ (V0s = (c_2Epred__set_2EEMPTY@A_27a))) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@(ap@(c_2Epred__set_2ECHOICE@A_27a)@V0s))@V0s))))))).
thf(ax_thm_2Epred__set_2EREST__DEF,axiom,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((ap@(c_2Epred__set_2EREST@A_27a)@V0s) = (ap@(ap@(c_2Epred__set_2EDELETE@A_27a)@V0s)@(ap@(c_2Epred__set_2ECHOICE@A_27a)@V0s))))))).
thf(conj_thm_2Epred__set_2EIN__REST,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@(ap@(c_2Epred__set_2EREST@A_27a)@V1s))) <=> ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@V1s)) & (~~ (V0x = (ap@(c_2Epred__set_2ECHOICE@A_27a)@V1s))))))))))).
thf(conj_thm_2Epred__set_2EREST__applied,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2EREST@A_27a)@V1s)@V0x)) <=> ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@V1s)) & (~~ (V0x = (ap@(c_2Epred__set_2ECHOICE@A_27a)@V1s))))))))))).
thf(conj_thm_2Epred__set_2ECHOICE__NOT__IN__REST,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => (~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@(ap@(c_2Epred__set_2ECHOICE@A_27a)@V0s))@(ap@(c_2Epred__set_2EREST@A_27a)@V0s)))))))).
thf(conj_thm_2Epred__set_2ECHOICE__INSERT__REST,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((~~ (V0s = (c_2Epred__set_2EEMPTY@A_27a))) => ((ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@(ap@(c_2Epred__set_2ECHOICE@A_27a)@V0s))@(ap@(c_2Epred__set_2EREST@A_27a)@V0s)) = V0s)))))).
thf(conj_thm_2Epred__set_2EREST__SUBSET,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@(ap@(c_2Epred__set_2EREST@A_27a)@V0s))@V0s)))))).
thf(conj_thm_2Epred__set_2EREST__PSUBSET,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((~~ (V0s = (c_2Epred__set_2EEMPTY@A_27a))) => (p@(ap@(ap@(c_2Epred__set_2EPSUBSET@A_27a)@(ap@(c_2Epred__set_2EREST@A_27a)@V0s))@V0s))))))).
thf(ax_thm_2Epred__set_2ESING__DEF,axiom,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2ESING@A_27a)@V0s)) <=> (? [V1x:$i] : ((mem@V1x@A_27a) & (V0s = (ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V1x)@(c_2Epred__set_2EEMPTY@A_27a)))))))))).
thf(conj_thm_2Epred__set_2ESING,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => (p@(ap@(c_2Epred__set_2ESING@A_27a)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@(c_2Epred__set_2EEMPTY@A_27a)))))))).
thf(conj_thm_2Epred__set_2ESING__EMPTY,lemma,( ! [A_27a:del]: ((p@(ap@(c_2Epred__set_2ESING@A_27a)@(c_2Epred__set_2EEMPTY@A_27a))) <=> $false))).
thf(conj_thm_2Epred__set_2ESING__INSERT,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2ESING@A_27a)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@V1s))) <=> ((V1s = (c_2Epred__set_2EEMPTY@A_27a)) | (V1s = (ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@(c_2Epred__set_2EEMPTY@A_27a))))))))))).
thf(conj_thm_2Epred__set_2ESING__UNION,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2ESING@A_27a)@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V0s)@V1t))) <=> (((p@(ap@(c_2Epred__set_2ESING@A_27a)@V0s)) & (V1t = (c_2Epred__set_2EEMPTY@A_27a))) | (((p@(ap@(c_2Epred__set_2ESING@A_27a)@V1t)) & (V0s = (c_2Epred__set_2EEMPTY@A_27a))) | ((p@(ap@(c_2Epred__set_2ESING@A_27a)@V0s)) & ((p@(ap@(c_2Epred__set_2ESING@A_27a)@V1t)) & (V0s = V1t)))))))))))).
thf(conj_thm_2Epred__set_2EIN__SING,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1y:$i] : ((mem@V1y@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V1y)@(c_2Epred__set_2EEMPTY@A_27a)))) <=> (V0x = V1y)))))))).
thf(conj_thm_2Epred__set_2ESING__applied,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1y:$i] : ((mem@V1y@A_27a) => ((p@(ap@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V1y)@(c_2Epred__set_2EEMPTY@A_27a))@V0x)) <=> (V0x = V1y)))))))).
thf(conj_thm_2Epred__set_2ENOT__SING__EMPTY,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => (~~ ((ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@(c_2Epred__set_2EEMPTY@A_27a)) = (c_2Epred__set_2EEMPTY@A_27a))))))).
thf(conj_thm_2Epred__set_2ENOT__EMPTY__SING,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => (~~ ((c_2Epred__set_2EEMPTY@A_27a) = (ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@(c_2Epred__set_2EEMPTY@A_27a)))))))).
thf(conj_thm_2Epred__set_2EEQUAL__SING,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1y:$i] : ((mem@V1y@A_27a) => (((ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@(c_2Epred__set_2EEMPTY@A_27a)) = (ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V1y)@(c_2Epred__set_2EEMPTY@A_27a))) <=> (V0x = V1y)))))))).
thf(conj_thm_2Epred__set_2EDISJOINT__SING__EMPTY,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => (p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@(c_2Epred__set_2EEMPTY@A_27a)))@(c_2Epred__set_2EEMPTY@A_27a))))))).
thf(conj_thm_2Epred__set_2EINSERT__SING__UNION,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ((ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V1x)@V0s) = (ap@(ap@(c_2Epred__set_2EUNION@A_27a)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V1x)@(c_2Epred__set_2EEMPTY@A_27a)))@V0s)))))))).
thf(conj_thm_2Epred__set_2ESING__DELETE,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ((ap@(ap@(c_2Epred__set_2EDELETE@A_27a)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@(c_2Epred__set_2EEMPTY@A_27a)))@V0x) = (c_2Epred__set_2EEMPTY@A_27a)))))).
thf(conj_thm_2Epred__set_2EDELETE__EQ__SING,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1x)@V0s)) => (((ap@(ap@(c_2Epred__set_2EDELETE@A_27a)@V0s)@V1x) = (c_2Epred__set_2EEMPTY@A_27a)) <=> (V0s = (ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V1x)@(c_2Epred__set_2EEMPTY@A_27a))))))))))).
thf(conj_thm_2Epred__set_2ECHOICE__SING,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ((ap@(c_2Epred__set_2ECHOICE@A_27a)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@(c_2Epred__set_2EEMPTY@A_27a))) = V0x))))).
thf(conj_thm_2Epred__set_2EREST__SING,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ((ap@(c_2Epred__set_2EREST@A_27a)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@(c_2Epred__set_2EEMPTY@A_27a))) = (c_2Epred__set_2EEMPTY@A_27a)))))).
thf(conj_thm_2Epred__set_2ESING__IFF__EMPTY__REST,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2ESING@A_27a)@V0s)) <=> ((~~ (V0s = (c_2Epred__set_2EEMPTY@A_27a))) & ((ap@(c_2Epred__set_2EREST@A_27a)@V0s) = (c_2Epred__set_2EEMPTY@A_27a)))))))).
thf(ax_thm_2Epred__set_2EIMAGE__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@V1s) = (ap@(c_2Epred__set_2EGSPEC@A_27b@A_27a)@(lam@A_27a@(^ [V2x:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27b@bool)@(ap@V0f@V2x))@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V1s))))))))))))).
thf(conj_thm_2Epred__set_2EIN__IMAGE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0y:$i] : ((mem@V0y@A_27b) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27b)) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V0y)@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V2f)@V1s))) <=> (? [V3x:$i] : ((mem@V3x@A_27a) & ((V0y = (ap@V2f@V3x)) & (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@V1s))))))))))))))).
thf(conj_thm_2Epred__set_2EIMAGE__applied,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0y:$i] : ((mem@V0y@A_27b) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27b)) => ((p@(ap@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V2f)@V1s)@V0y)) <=> (? [V3x:$i] : ((mem@V3x@A_27a) & ((V0y = (ap@V2f@V3x)) & (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@V1s))))))))))))))).
thf(conj_thm_2Epred__set_2EIMAGE__IN,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@V1s)) => ( ! [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27b)) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@(ap@V2f@V0x))@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V2f)@V1s))))))))))))).
thf(conj_thm_2Epred__set_2EIMAGE__EMPTY,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ((ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@(c_2Epred__set_2EEMPTY@A_27a)) = (c_2Epred__set_2EEMPTY@A_27b))))))).
thf(conj_thm_2Epred__set_2EIMAGE__ID,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27a)@(lam@A_27a@(^ [V1x:$i] : V1x)))@V0s) = V0s))))).
thf(conj_thm_2Epred__set_2EIMAGE__I,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27a)@(c_2Ecombin_2EI@A_27a))@V0s) = V0s))))).
thf(conj_thm_2Epred__set_2EIMAGE__II,lemma,( ! [A_27a:del]: ((ap@(c_2Epred__set_2EIMAGE@A_27a@A_27a)@(c_2Ecombin_2EI@A_27a)) = (c_2Ecombin_2EI@(arr@A_27a@bool))))).
thf(conj_thm_2Epred__set_2EIMAGE__COMPOSE,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)) => ( ! [V2s:$i] : ((mem@V2s@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27c)@(ap@(ap@(c_2Ecombin_2Eo@A_27a@A_27c@A_27b)@V0f)@V1g))@V2s) = (ap@(ap@(c_2Epred__set_2EIMAGE@A_27b@A_27c)@V0f)@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V1g)@V2s))))))))))))).
thf(conj_thm_2Epred__set_2EIMAGE__INSERT,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ( ! [V2s:$i] : ((mem@V2s@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V1x)@V2s)) = (ap@(ap@(c_2Epred__set_2EINSERT@A_27b)@(ap@V0f@V1x))@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@V2s)))))))))))).
thf(conj_thm_2Epred__set_2EIMAGE__EQ__EMPTY,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27a@A_27b)) => (((ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V1f)@V0s) = (c_2Epred__set_2EEMPTY@A_27b)) <=> (V0s = (c_2Epred__set_2EEMPTY@A_27a)))))))))).
thf(conj_thm_2Epred__set_2EIMAGE__DELETE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ( ! [V2s:$i] : ((mem@V2s@(arr@A_27a@bool)) => ((~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1x)@V2s))) => ((ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@(ap@(ap@(c_2Epred__set_2EDELETE@A_27a)@V2s)@V1x)) = (ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@V2s)))))))))))).
thf(conj_thm_2Epred__set_2EIMAGE__UNION,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V1s)@V2t)) = (ap@(ap@(c_2Epred__set_2EUNION@A_27b)@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@V1s))@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@V2t)))))))))))).
thf(conj_thm_2Epred__set_2EIMAGE__SUBSET,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V0s)@V1t)) => ( ! [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27b)) => (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27b)@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V2f)@V0s))@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V2f)@V1t))))))))))))).
thf(conj_thm_2Epred__set_2EIMAGE__INTER,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27a@bool)) => (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27b)@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@(ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V1s)@V2t)))@(ap@(ap@(c_2Epred__set_2EINTER@A_27b)@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@V1s))@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@V2t))))))))))))).
thf(conj_thm_2Epred__set_2EIMAGE__11,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s1:$i] : ((mem@V1s1@(arr@A_27a@bool)) => ( ! [V2s2:$i] : ((mem@V2s2@(arr@A_27a@bool)) => (( ! [V3x:$i] : ((mem@V3x@A_27a) => ( ! [V4y:$i] : ((mem@V4y@A_27a) => (((ap@V0f@V3x) = (ap@V0f@V4y)) <=> (V3x = V4y)))))) => (((ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@V1s1) = (ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@V2s2)) <=> (V1s1 = V2s2)))))))))))).
thf(conj_thm_2Epred__set_2EDISJOINT__IMAGE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s1:$i] : ((mem@V1s1@(arr@A_27a@bool)) => ( ! [V2s2:$i] : ((mem@V2s2@(arr@A_27a@bool)) => (( ! [V3x:$i] : ((mem@V3x@A_27a) => ( ! [V4y:$i] : ((mem@V4y@A_27a) => (((ap@V0f@V3x) = (ap@V0f@V4y)) <=> (V3x = V4y)))))) => ((p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27b)@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@V1s1))@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@V2s2))) <=> (p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@V1s1)@V2s2))))))))))))).
thf(conj_thm_2Epred__set_2EIMAGE__CONG,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2f_27:$i] : ((mem@V2f_27@(arr@A_27a@A_27b)) => ( ! [V3s_27:$i] : ((mem@V3s_27@(arr@A_27a@bool)) => (((V1s = V3s_27) & ( ! [V4x:$i] : ((mem@V4x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V4x)@V3s_27)) => ((ap@V0f@V4x) = (ap@V2f_27@V4x)))))) => ((ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@V1s) = (ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V2f_27)@V3s_27)))))))))))))).
thf(conj_thm_2Epred__set_2EGSPEC__IMAGE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27b@(ty_2Epair_2Eprod@A_27a@bool))) => ((ap@(c_2Epred__set_2EGSPEC@A_27a@A_27b)@V0f) = (ap@(ap@(c_2Epred__set_2EIMAGE@A_27b@A_27a)@(ap@(ap@(c_2Ecombin_2Eo@A_27b@A_27a@(ty_2Epair_2Eprod@A_27a@bool))@(c_2Epair_2EFST@A_27a@bool))@V0f))@(ap@(ap@(c_2Ecombin_2Eo@A_27b@bool@(ty_2Epair_2Eprod@A_27a@bool))@(c_2Epair_2ESND@A_27a@bool))@V0f)))))))).
thf(conj_thm_2Epred__set_2EIMAGE__IMAGE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1g:$i] : ((mem@V1g@(arr@A_27c@A_27a)) => ( ! [V2s:$i] : ((mem@V2s@(arr@A_27c@bool)) => ((ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27c@A_27a)@V1g)@V2s)) = (ap@(ap@(c_2Epred__set_2EIMAGE@A_27c@A_27b)@(ap@(ap@(c_2Ecombin_2Eo@A_27c@A_27b@A_27a)@V0f)@V1g))@V2s)))))))))))).
thf(conj_thm_2Epred__set_2EFORALL__IN__IMAGE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27b@A_27a)) => ( ! [V2s:$i] : ((mem@V2s@(arr@A_27b@bool)) => (( ! [V3y:$i] : ((mem@V3y@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3y)@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27b@A_27a)@V1f)@V2s))) => (p@(ap@V0P@V3y))))) <=> ( ! [V4x:$i] : ((mem@V4x@A_27b) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V4x)@V2s)) => (p@(ap@V0P@(ap@V1f@V4x)))))))))))))))).
thf(conj_thm_2Epred__set_2EEXISTS__IN__IMAGE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27b@A_27a)) => ( ! [V2s:$i] : ((mem@V2s@(arr@A_27b@bool)) => ((? [V3y:$i] : ((mem@V3y@A_27a) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3y)@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27b@A_27a)@V1f)@V2s))) & (p@(ap@V0P@V3y))))) <=> (? [V4x:$i] : ((mem@V4x@A_27b) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V4x)@V2s)) & (p@(ap@V0P@(ap@V1f@V4x)))))))))))))))).
thf(ax_thm_2Epred__set_2EINJ__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27b@bool)) => ((p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27a@A_27b)@V0f)@V1s)@V2t)) <=> (( ! [V3x:$i] : ((mem@V3x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@V1s)) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@(ap@V0f@V3x))@V2t))))) & ( ! [V4x:$i] : ((mem@V4x@A_27a) => ( ! [V5y:$i] : ((mem@V5y@A_27a) => (((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V4x)@V1s)) & (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V5y)@V1s))) => (((ap@V0f@V4x) = (ap@V0f@V5y)) => (V4x = V5y)))))))))))))))))).
thf(conj_thm_2Epred__set_2EINJ__IFF,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27b@bool)) => ((p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27a@A_27b)@V0f)@V1s)@V2t)) <=> (( ! [V3x:$i] : ((mem@V3x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@V1s)) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@(ap@V0f@V3x))@V2t))))) & ( ! [V4x:$i] : ((mem@V4x@A_27a) => ( ! [V5y:$i] : ((mem@V5y@A_27a) => (((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V4x)@V1s)) & (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V5y)@V1s))) => (((ap@V0f@V4x) = (ap@V0f@V5y)) <=> (V4x = V5y)))))))))))))))))).
thf(conj_thm_2Epred__set_2EINJ__ID,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => (p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27a@A_27a)@(lam@A_27a@(^ [V1x:$i] : V1x)))@V0s)@V0s)))))).
thf(conj_thm_2Epred__set_2EINJ__COMPOSE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1g:$i] : ((mem@V1g@(arr@A_27b@A_27c)) => ( ! [V2s:$i] : ((mem@V2s@(arr@A_27a@bool)) => ( ! [V3t:$i] : ((mem@V3t@(arr@A_27b@bool)) => ( ! [V4u:$i] : ((mem@V4u@(arr@A_27c@bool)) => (((p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27a@A_27b)@V0f)@V2s)@V3t)) & (p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27b@A_27c)@V1g)@V3t)@V4u))) => (p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27a@A_27c)@(ap@(ap@(c_2Ecombin_2Eo@A_27a@A_27c@A_27b)@V1g)@V0f))@V2s)@V4u))))))))))))))))).
thf(conj_thm_2Epred__set_2EINJ__EMPTY,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => (( ! [V1s:$i] : ((mem@V1s@(arr@A_27b@bool)) => (p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27a@A_27b)@V0f)@(c_2Epred__set_2EEMPTY@A_27a))@V1s)))) & ( ! [V2s:$i] : ((mem@V2s@(arr@A_27a@bool)) => ((p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27a@A_27b)@V0f)@V2s)@(c_2Epred__set_2EEMPTY@A_27b))) <=> (V2s = (c_2Epred__set_2EEMPTY@A_27a))))))))))).
thf(conj_thm_2Epred__set_2EINJ__DELETE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => ( ! [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27b)) => ((p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27a@A_27b)@V2f)@V0s)@V1t)) => ( ! [V3e:$i] : ((mem@V3e@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3e)@V0s)) => (p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27a@A_27b)@V2f)@(ap@(ap@(c_2Epred__set_2EDELETE@A_27a)@V0s)@V3e))@(ap@(ap@(c_2Epred__set_2EDELETE@A_27b)@V1t)@(ap@V2f@V3e))))))))))))))))).
thf(conj_thm_2Epred__set_2EINJ__INSERT,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ( ! [V2s:$i] : ((mem@V2s@(arr@A_27a@bool)) => ( ! [V3t:$i] : ((mem@V3t@(arr@A_27b@bool)) => ((p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27a@A_27b)@V0f)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V1x)@V2s))@V3t)) <=> ((p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27a@A_27b)@V0f)@V2s)@V3t)) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@(ap@V0f@V1x))@V3t)) & ( ! [V4y:$i] : ((mem@V4y@A_27a) => (((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V4y)@V2s)) & ((ap@V0f@V1x) = (ap@V0f@V4y))) => (V1x = V4y)))))))))))))))))).
thf(conj_thm_2Epred__set_2EINJ__EXTEND,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27b@bool)) => ( ! [V3x:$i] : ((mem@V3x@A_27a) => ( ! [V4y:$i] : ((mem@V4y@A_27b) => (((p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27a@A_27b)@V0b)@V1s)@V2t)) & ((~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@V1s))) & (~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V4y)@V2t))))) => (p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27a@A_27b)@(ap@(ap@(ap@(c_2Ecombin_2EUPDATE@A_27a@A_27b)@V3x)@V4y)@V0b))@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V3x)@V1s))@(ap@(ap@(c_2Epred__set_2EINSERT@A_27b)@V4y)@V2t))))))))))))))))).
thf(conj_thm_2Epred__set_2EINJ__SUBSET,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27b@bool)) => ( ! [V3s0:$i] : ((mem@V3s0@(arr@A_27a@bool)) => ( ! [V4t0:$i] : ((mem@V4t0@(arr@A_27b@bool)) => (((p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27a@A_27b)@V0f)@V1s)@V2t)) & ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V3s0)@V1s)) & (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27b)@V2t)@V4t0)))) => (p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27a@A_27b)@V0f)@V3s0)@V4t0)))))))))))))))).
thf(conj_thm_2Epred__set_2EINJ__IMAGE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27b@bool)) => ((p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27a@A_27b)@V0f)@V1s)@V2t)) => (p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27a@A_27b)@V0f)@V1s)@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@V1s))))))))))))).
thf(conj_thm_2Epred__set_2EINJ__IMAGE__SUBSET,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27b@bool)) => ((p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27a@A_27b)@V0f)@V1s)@V2t)) => (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27b)@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@V1s))@V2t)))))))))))).
thf(ax_thm_2Epred__set_2ESURJ__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27b@bool)) => ((p@(ap@(ap@(ap@(c_2Epred__set_2ESURJ@A_27a@A_27b)@V0f)@V1s)@V2t)) <=> (( ! [V3x:$i] : ((mem@V3x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@V1s)) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@(ap@V0f@V3x))@V2t))))) & ( ! [V4x:$i] : ((mem@V4x@A_27b) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V4x)@V2t)) => (? [V5y:$i] : ((mem@V5y@A_27a) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V5y)@V1s)) & ((ap@V0f@V5y) = V4x)))))))))))))))))).
thf(conj_thm_2Epred__set_2ESURJ__ID,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => (p@(ap@(ap@(ap@(c_2Epred__set_2ESURJ@A_27a@A_27a)@(lam@A_27a@(^ [V1x:$i] : V1x)))@V0s)@V0s)))))).
thf(conj_thm_2Epred__set_2ESURJ__COMPOSE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1g:$i] : ((mem@V1g@(arr@A_27b@A_27c)) => ( ! [V2s:$i] : ((mem@V2s@(arr@A_27a@bool)) => ( ! [V3t:$i] : ((mem@V3t@(arr@A_27b@bool)) => ( ! [V4u:$i] : ((mem@V4u@(arr@A_27c@bool)) => (((p@(ap@(ap@(ap@(c_2Epred__set_2ESURJ@A_27a@A_27b)@V0f)@V2s)@V3t)) & (p@(ap@(ap@(ap@(c_2Epred__set_2ESURJ@A_27b@A_27c)@V1g)@V3t)@V4u))) => (p@(ap@(ap@(ap@(c_2Epred__set_2ESURJ@A_27a@A_27c)@(ap@(ap@(c_2Ecombin_2Eo@A_27a@A_27c@A_27b)@V1g)@V0f))@V2s)@V4u))))))))))))))))).
thf(conj_thm_2Epred__set_2ESURJ__EMPTY,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => (( ! [V1s:$i] : ((mem@V1s@(arr@A_27b@bool)) => ((p@(ap@(ap@(ap@(c_2Epred__set_2ESURJ@A_27a@A_27b)@V0f)@(c_2Epred__set_2EEMPTY@A_27a))@V1s)) <=> (V1s = (c_2Epred__set_2EEMPTY@A_27b))))) & ( ! [V2s:$i] : ((mem@V2s@(arr@A_27a@bool)) => ((p@(ap@(ap@(ap@(c_2Epred__set_2ESURJ@A_27a@A_27b)@V0f)@V2s)@(c_2Epred__set_2EEMPTY@A_27b))) <=> (V2s = (c_2Epred__set_2EEMPTY@A_27a))))))))))).
thf(conj_thm_2Epred__set_2EIMAGE__SURJ,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27b@bool)) => ((p@(ap@(ap@(ap@(c_2Epred__set_2ESURJ@A_27a@A_27b)@V0f)@V1s)@V2t)) <=> ((ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@V1s) = V2t))))))))))).
thf(conj_thm_2Epred__set_2ESURJ__IMAGE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => (p@(ap@(ap@(ap@(c_2Epred__set_2ESURJ@A_27a@A_27b)@V0f)@V1s)@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@V1s)))))))))).
thf(conj_thm_2Epred__set_2ESURJ__IMP__INJ,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => ((? [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27b)) & (p@(ap@(ap@(ap@(c_2Epred__set_2ESURJ@A_27a@A_27b)@V2f)@V0s)@V1t)))) => (? [V3g:$i] : ((mem@V3g@(arr@A_27b@A_27a)) & (p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27b@A_27a)@V3g)@V1t)@V0s)))))))))))).
thf(ax_thm_2Epred__set_2EBIJ__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27b@bool)) => ((p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27b)@V0f)@V1s)@V2t)) <=> ((p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27a@A_27b)@V0f)@V1s)@V2t)) & (p@(ap@(ap@(ap@(c_2Epred__set_2ESURJ@A_27a@A_27b)@V0f)@V1s)@V2t))))))))))))).
thf(conj_thm_2Epred__set_2EBIJ__ID,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => (p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27a)@(lam@A_27a@(^ [V1x:$i] : V1x)))@V0s)@V0s)))))).
thf(conj_thm_2Epred__set_2EBIJ__IMP__11,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ((p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27b)@V0f)@(c_2Epred__set_2EUNIV@A_27a))@(c_2Epred__set_2EUNIV@A_27b))) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ( ! [V2y:$i] : ((mem@V2y@A_27a) => (((ap@V0f@V1x) = (ap@V0f@V2y)) <=> (V1x = V2y)))))))))))).
thf(conj_thm_2Epred__set_2EBIJ__EMPTY,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => (( ! [V1s:$i] : ((mem@V1s@(arr@A_27b@bool)) => ((p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27b)@V0f)@(c_2Epred__set_2EEMPTY@A_27a))@V1s)) <=> (V1s = (c_2Epred__set_2EEMPTY@A_27b))))) & ( ! [V2s:$i] : ((mem@V2s@(arr@A_27a@bool)) => ((p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27b)@V0f)@V2s)@(c_2Epred__set_2EEMPTY@A_27b))) <=> (V2s = (c_2Epred__set_2EEMPTY@A_27a))))))))))).
thf(conj_thm_2Epred__set_2EBIJ__COMPOSE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1g:$i] : ((mem@V1g@(arr@A_27b@A_27c)) => ( ! [V2s:$i] : ((mem@V2s@(arr@A_27a@bool)) => ( ! [V3t:$i] : ((mem@V3t@(arr@A_27b@bool)) => ( ! [V4u:$i] : ((mem@V4u@(arr@A_27c@bool)) => (((p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27b)@V0f)@V2s)@V3t)) & (p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27b@A_27c)@V1g)@V3t)@V4u))) => (p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27c)@(ap@(ap@(c_2Ecombin_2Eo@A_27a@A_27c@A_27b)@V1g)@V0f))@V2s)@V4u))))))))))))))))).
thf(conj_thm_2Epred__set_2EBIJ__DELETE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => ( ! [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27b)) => ((p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27b)@V2f)@V0s)@V1t)) => ( ! [V3e:$i] : ((mem@V3e@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3e)@V0s)) => (p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27b)@V2f)@(ap@(ap@(c_2Epred__set_2EDELETE@A_27a)@V0s)@V3e))@(ap@(ap@(c_2Epred__set_2EDELETE@A_27b)@V1t)@(ap@V2f@V3e))))))))))))))))).
thf(conj_thm_2Epred__set_2EINJ__IMAGE__BIJ,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27a@A_27b)) => ((? [V2t:$i] : ((mem@V2t@(arr@A_27b@bool)) & (p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27a@A_27b)@V1f)@V0s)@V2t)))) => (p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27b)@V1f)@V0s)@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V1f)@V0s))))))))))).
thf(conj_thm_2Epred__set_2EINJ__BIJ__SUBSET,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s0:$i] : ((mem@V0s0@(arr@A_27a@bool)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27b)) => ( ! [V3t:$i] : ((mem@V3t@(arr@A_27b@bool)) => (((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V0s0)@V1s)) & (p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27a@A_27b)@V2f)@V1s)@V3t))) => (p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27b)@V2f)@V0s0)@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V2f)@V0s0))))))))))))))).
thf(conj_thm_2Epred__set_2EBIJ__SYM__IMP,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => ((? [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27b)) & (p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27b)@V2f)@V0s)@V1t)))) => (? [V3g:$i] : ((mem@V3g@(arr@A_27b@A_27a)) & (p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27b@A_27a)@V3g)@V1t)@V0s)))))))))))).
thf(conj_thm_2Epred__set_2EBIJ__SYM,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => ((? [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27b)) & (p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27b)@V2f)@V0s)@V1t)))) <=> (? [V3g:$i] : ((mem@V3g@(arr@A_27b@A_27a)) & (p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27b@A_27a)@V3g)@V1t)@V0s)))))))))))).
thf(conj_thm_2Epred__set_2EBIJ__TRANS,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27c@bool)) => ( ! [V2u:$i] : ((mem@V2u@(arr@A_27b@bool)) => (((? [V3f:$i] : ((mem@V3f@(arr@A_27a@A_27c)) & (p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27c)@V3f)@V0s)@V1t)))) & (? [V4g:$i] : ((mem@V4g@(arr@A_27c@A_27b)) & (p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27c@A_27b)@V4g)@V1t)@V2u))))) => (? [V5h:$i] : ((mem@V5h@(arr@A_27a@A_27b)) & (p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27b)@V5h)@V0s)@V2u))))))))))))))).
thf(conj_thm_2Epred__set_2EBIJ__INV,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27b@bool)) => ((p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27b)@V0f)@V1s)@V2t)) => (? [V3g:$i] : ((mem@V3g@(arr@A_27b@A_27a)) & ((p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27b@A_27a)@V3g)@V2t)@V1s)) & (( ! [V4x:$i] : ((mem@V4x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V4x)@V1s)) => ((ap@(ap@(ap@(c_2Ecombin_2Eo@A_27a@A_27a@A_27b)@V3g)@V0f)@V4x) = V4x)))) & ( ! [V5x:$i] : ((mem@V5x@A_27b) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V5x)@V2t)) => ((ap@(ap@(ap@(c_2Ecombin_2Eo@A_27b@A_27b@A_27a)@V0f)@V3g)@V5x) = V5x)))))))))))))))))).
thf(ax_thm_2Epred__set_2EFUNSET,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1Q:$i] : ((mem@V1Q@(arr@A_27b@bool)) => ((ap@(ap@(c_2Epred__set_2EFUNSET@A_27a@A_27b)@V0P)@V1Q) = (lam@(arr@A_27a@A_27b)@(^ [V2f:$i] : (ap@(c_2Ebool_2E_21@A_27a)@(lam@A_27a@(^ [V3x:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@V0P))@(ap@(ap@(c_2Ebool_2EIN@A_27b)@(ap@V2f@V3x))@V1Q))))))))))))))).
thf(ax_thm_2Epred__set_2EDFUNSET,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1Q:$i] : ((mem@V1Q@(arr@A_27a@(arr@A_27b@bool))) => ((ap@(ap@(c_2Epred__set_2EDFUNSET@A_27a@A_27b)@V0P)@V1Q) = (lam@(arr@A_27a@A_27b)@(^ [V2f:$i] : (ap@(c_2Ebool_2E_21@A_27a)@(lam@A_27a@(^ [V3x:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@V0P))@(ap@(ap@(c_2Ebool_2EIN@A_27b)@(ap@V2f@V3x))@(ap@V1Q@V3x)))))))))))))))).
thf(conj_thm_2Epred__set_2EIN__FUNSET,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1P:$i] : ((mem@V1P@(arr@A_27a@bool)) => ( ! [V2Q:$i] : ((mem@V2Q@(arr@A_27b@bool)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@A_27b))@V0f)@(ap@(ap@(c_2Epred__set_2EFUNSET@A_27a@A_27b)@V1P)@V2Q))) <=> ( ! [V3x:$i] : ((mem@V3x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@V1P)) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@(ap@V0f@V3x))@V2Q))))))))))))))).
thf(conj_thm_2Epred__set_2EFUNSET__applied,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1P:$i] : ((mem@V1P@(arr@A_27a@bool)) => ( ! [V2Q:$i] : ((mem@V2Q@(arr@A_27b@bool)) => ((p@(ap@(ap@(ap@(c_2Epred__set_2EFUNSET@A_27a@A_27b)@V1P)@V2Q)@V0f)) <=> ( ! [V3x:$i] : ((mem@V3x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@V1P)) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@(ap@V0f@V3x))@V2Q))))))))))))))).
thf(conj_thm_2Epred__set_2EIN__DFUNSET,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1P:$i] : ((mem@V1P@(arr@A_27a@bool)) => ( ! [V2Q:$i] : ((mem@V2Q@(arr@A_27a@(arr@A_27b@bool))) => ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@A_27b))@V0f)@(ap@(ap@(c_2Epred__set_2EDFUNSET@A_27a@A_27b)@V1P)@V2Q))) <=> ( ! [V3x:$i] : ((mem@V3x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@V1P)) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@(ap@V0f@V3x))@(ap@V2Q@V3x)))))))))))))))).
thf(conj_thm_2Epred__set_2EDFUNSET__applied,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1P:$i] : ((mem@V1P@(arr@A_27a@bool)) => ( ! [V2Q:$i] : ((mem@V2Q@(arr@A_27a@(arr@A_27b@bool))) => ((p@(ap@(ap@(ap@(c_2Epred__set_2EDFUNSET@A_27a@A_27b)@V1P)@V2Q)@V0f)) <=> ( ! [V3x:$i] : ((mem@V3x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@V1P)) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@(ap@V0f@V3x))@(ap@V2Q@V3x)))))))))))))))).
thf(conj_thm_2Epred__set_2EFUNSET__THM,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => ( ! [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27b)) => ( ! [V3x:$i] : ((mem@V3x@A_27a) => (((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@A_27b))@V2f)@(ap@(ap@(c_2Epred__set_2EFUNSET@A_27a@A_27b)@V0s)@V1t))) & (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@V0s))) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@(ap@V2f@V3x))@V1t)))))))))))))).
thf(conj_thm_2Epred__set_2EUNIV__FUNSET__UNIV,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ((ap@(ap@(c_2Epred__set_2EFUNSET@A_27a@A_27b)@(c_2Epred__set_2EUNIV@A_27a))@(c_2Epred__set_2EUNIV@A_27b)) = (c_2Epred__set_2EUNIV@(arr@A_27a@A_27b)))))).
thf(conj_thm_2Epred__set_2EFUNSET__DFUNSET,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : ((mem@V0x@(arr@A_27a@bool)) => ( ! [V1y:$i] : ((mem@V1y@(arr@A_27b@bool)) => ((ap@(ap@(c_2Epred__set_2EFUNSET@A_27a@A_27b)@V0x)@V1y) = (ap@(ap@(c_2Epred__set_2EDFUNSET@A_27a@A_27b)@V0x)@(ap@(c_2Ecombin_2EK@(arr@A_27b@bool)@A_27a)@V1y)))))))))).
thf(conj_thm_2Epred__set_2EEMPTY__FUNSET,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27b@bool)) => ((ap@(ap@(c_2Epred__set_2EFUNSET@A_27a@A_27b)@(c_2Epred__set_2EEMPTY@A_27a))@V0s) = (c_2Epred__set_2EUNIV@(arr@A_27a@A_27b)))))))).
thf(conj_thm_2Epred__set_2EFUNSET__EMPTY,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27a@A_27b)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@A_27b))@V1f)@(ap@(ap@(c_2Epred__set_2EFUNSET@A_27a@A_27b)@V0s)@(c_2Epred__set_2EEMPTY@A_27b)))) <=> (V0s = (c_2Epred__set_2EEMPTY@A_27a)))))))))).
thf(conj_thm_2Epred__set_2EFUNSET__INTER,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0a:$i] : ((mem@V0a@(arr@A_27a@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@A_27b@bool)) => ( ! [V2c:$i] : ((mem@V2c@(arr@A_27b@bool)) => ((ap@(ap@(c_2Epred__set_2EFUNSET@A_27a@A_27b)@V0a)@(ap@(ap@(c_2Epred__set_2EINTER@A_27b)@V1b)@V2c)) = (ap@(ap@(c_2Epred__set_2EINTER@(arr@A_27a@A_27b))@(ap@(ap@(c_2Epred__set_2EFUNSET@A_27a@A_27b)@V0a)@V1b))@(ap@(ap@(c_2Epred__set_2EFUNSET@A_27a@A_27b)@V0a)@V2c)))))))))))).
thf(ax_thm_2Epred__set_2Eschroeder__close__def,axiom,( ! [A_27a:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27a)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@(ap@(c_2Epred__set_2Eschroeder__close@A_27a)@V0f)@V1s)@V2x)) <=> (? [V3n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(ap@(ap@(c_2Earithmetic_2EFUNPOW@(arr@A_27a@bool))@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27a)@V0f))@(inj__ty_2Enum_2Enum @ V3n))@V1s))))))))))))).
thf(conj_thm_2Epred__set_2ESCHROEDER__CLOSE,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27a@A_27a)) => ( ! [V2s:$i] : ((mem@V2s@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@(ap@(ap@(c_2Epred__set_2Eschroeder__close@A_27a)@V1f)@V2s))) <=> (? [V3n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@(ap@(ap@(ap@(c_2Earithmetic_2EFUNPOW@(arr@A_27a@bool))@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27a)@V1f))@(inj__ty_2Enum_2Enum @ V3n))@V2s))))))))))))).
thf(conj_thm_2Epred__set_2ESCHROEDER__CLOSED,lemma,( ! [A_27a:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27a)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27a)@V0f)@(ap@(ap@(c_2Epred__set_2Eschroeder__close@A_27a)@V0f)@V1s)))@(ap@(ap@(c_2Epred__set_2Eschroeder__close@A_27a)@V0f)@V1s))))))))).
thf(conj_thm_2Epred__set_2ESCHROEDER__CLOSE__SUBSET,lemma,( ! [A_27a:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27a)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V1s)@(ap@(ap@(c_2Epred__set_2Eschroeder__close@A_27a)@V0f)@V1s))))))))).
thf(conj_thm_2Epred__set_2ESCHROEDER__CLOSE__SET,lemma,( ! [A_27a:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27a)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27a@bool)) => (((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@A_27a))@V0f)@(ap@(ap@(c_2Epred__set_2EFUNSET@A_27a@A_27a)@V1s)@V1s))) & (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V2t)@V1s))) => (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@(ap@(ap@(c_2Epred__set_2Eschroeder__close@A_27a)@V0f)@V2t))@V1s))))))))))).
thf(conj_thm_2Epred__set_2ESCHROEDER__BERNSTEIN__AUTO,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => (((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V1t)@V0s)) & (? [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27a)) & (p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27a@A_27a)@V2f)@V0s)@V1t))))) => (? [V3g:$i] : ((mem@V3g@(arr@A_27a@A_27a)) & (p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27a)@V3g)@V0s)@V1t))))))))))).
thf(conj_thm_2Epred__set_2ESCHROEDER__BERNSTEIN,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => (((? [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27b)) & (p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27a@A_27b)@V2f)@V0s)@V1t)))) & (? [V3g:$i] : ((mem@V3g@(arr@A_27b@A_27a)) & (p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27b@A_27a)@V3g)@V1t)@V0s))))) => (? [V4h:$i] : ((mem@V4h@(arr@A_27a@A_27b)) & (p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27b)@V4h)@V0s)@V1t)))))))))))).
thf(conj_thm_2Epred__set_2EBIJ__INJ__SURJ,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => (((? [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27b)) & (p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27a@A_27b)@V2f)@V0s)@V1t)))) & (? [V3g:$i] : ((mem@V3g@(arr@A_27a@A_27b)) & (p@(ap@(ap@(ap@(c_2Epred__set_2ESURJ@A_27a@A_27b)@V3g)@V0s)@V1t))))) => (? [V4h:$i] : ((mem@V4h@(arr@A_27a@A_27b)) & (p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27b)@V4h)@V0s)@V1t)))))))))))).
thf(conj_thm_2Epred__set_2EBIJ__ALT,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27b@bool)) => ((p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27b)@V0f)@V1s)@V2t)) <=> ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@A_27b))@V0f)@(ap@(ap@(c_2Epred__set_2EFUNSET@A_27a@A_27b)@V1s)@V2t))) & ( ! [V3y:$i] : ((mem@V3y@A_27b) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V3y)@V2t)) => (p@(ap@(c_2Ebool_2E_3F_21@A_27a)@(lam@A_27a@(^ [V4x:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V4x)@V1s))@(ap@(ap@(c_2Emin_2E_3D@A_27b)@V3y)@(ap@V0f@V4x))))))))))))))))))))).
thf(conj_thm_2Epred__set_2EBIJ__INSERT__IMP,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1e:$i] : ((mem@V1e@A_27a) => ( ! [V2s:$i] : ((mem@V2s@(arr@A_27a@bool)) => ( ! [V3t:$i] : ((mem@V3t@(arr@A_27b@bool)) => (((~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1e)@V2s))) & (p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27b)@V0f)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V1e)@V2s))@V3t))) => (? [V4u:$i] : ((mem@V4u@(arr@A_27b@bool)) & (((ap@(ap@(c_2Epred__set_2EINSERT@A_27b)@(ap@V0f@V1e))@V4u) = V3t) & ((~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@(ap@V0f@V1e))@V4u))) & (p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27b)@V0f)@V2s)@V4u)))))))))))))))))).
thf(conj_thm_2Epred__set_2EBIJ__IMAGE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27b@bool)) => ((p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27b)@V0f)@V1s)@V2t)) => (V2t = (ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@V1s)))))))))))).
thf(ax_thm_2Epred__set_2ELINV__OPT__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2y:$i] : ((mem@V2y@A_27b) => ((ap@(ap@(ap@(c_2Epred__set_2ELINV__OPT@A_27a@A_27b)@V0f)@V1s)@V2y) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@A_27a))@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V2y)@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@V1s)))@(ap@(c_2Eoption_2ESOME@A_27a)@(ap@(c_2Emin_2E_40@A_27a)@(lam@A_27a@(^ [V3x:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@V1s))@(ap@(ap@(c_2Emin_2E_3D@A_27b)@(ap@V0f@V3x))@V2y)))))))@(c_2Eoption_2ENONE@A_27a)))))))))))).
thf(conj_thm_2Epred__set_2ELINV__OPT__THM,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2y:$i] : ((mem@V2y@A_27b) => ( ! [V3x:$i] : ((mem@V3x@A_27a) => (((ap@(ap@(ap@(c_2Epred__set_2ELINV__OPT@A_27a@A_27b)@V0f)@V1s)@V2y) = (ap@(c_2Eoption_2ESOME@A_27a)@V3x)) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@V1s)) & ((ap@V0f@V3x) = V2y)))))))))))))).
thf(conj_thm_2Epred__set_2EINJ__LINV__OPT__IMAGE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27b@A_27a)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27b@bool)) => (p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27a@(ty_2Eoption_2Eoption@A_27b))@(ap@(ap@(c_2Epred__set_2ELINV__OPT@A_27b@A_27a)@V0f)@V1s))@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27b@A_27a)@V0f)@V1s))@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27b@(ty_2Eoption_2Eoption@A_27b))@(c_2Eoption_2ESOME@A_27b))@V1s)))))))))).
thf(conj_thm_2Epred__set_2EINJ__LINV__OPT,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27b@bool)) => ((p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27a@A_27b)@V0f)@V1s)@V2t)) => ( ! [V3x:$i] : ((mem@V3x@A_27a) => ( ! [V4y:$i] : ((mem@V4y@A_27b) => (((ap@(ap@(ap@(c_2Epred__set_2ELINV__OPT@A_27a@A_27b)@V0f)@V1s)@V4y) = (ap@(c_2Eoption_2ESOME@A_27a)@V3x)) <=> ((V4y = (ap@V0f@V3x)) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@V1s)) & (p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V4y)@V2t))))))))))))))))))).
thf(ax_thm_2Epred__set_2ELINV__LO,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2y:$i] : ((mem@V2y@A_27b) => ((ap@(ap@(ap@(c_2Epred__set_2ELINV@A_27a@A_27b)@V0f)@V1s)@V2y) = (ap@(c_2Eoption_2ETHE@A_27a)@(ap@(ap@(ap@(c_2Epred__set_2ELINV__OPT@A_27a@A_27b)@V0f)@V1s)@V2y)))))))))))).
thf(conj_thm_2Epred__set_2ELINV__DEF,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27b@bool)) => ((p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27a@A_27b)@V0f)@V1s)@V2t)) => ( ! [V3x:$i] : ((mem@V3x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@V1s)) => ((ap@(ap@(ap@(c_2Epred__set_2ELINV@A_27a@A_27b)@V0f)@V1s)@(ap@V0f@V3x)) = V3x)))))))))))))).
thf(conj_thm_2Epred__set_2EBIJ__LINV__INV,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27b@bool)) => ((p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27b)@V0f)@V1s)@V2t)) => ( ! [V3x:$i] : ((mem@V3x@A_27b) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V3x)@V2t)) => ((ap@V0f@(ap@(ap@(ap@(c_2Epred__set_2ELINV@A_27a@A_27b)@V0f)@V1s)@V3x)) = V3x)))))))))))))).
thf(conj_thm_2Epred__set_2EBIJ__LINV__BIJ,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27b@bool)) => ((p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27b)@V0f)@V1s)@V2t)) => (p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27b@A_27a)@(ap@(ap@(c_2Epred__set_2ELINV@A_27a@A_27b)@V0f)@V1s))@V2t)@V1s)))))))))))).
thf(conj_thm_2Epred__set_2EBIJ__IFF__INV,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27b@bool)) => ((p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27b)@V0f)@V1s)@V2t)) <=> (( ! [V3x:$i] : ((mem@V3x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@V1s)) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@(ap@V0f@V3x))@V2t))))) & (? [V4g:$i] : ((mem@V4g@(arr@A_27b@A_27a)) & (( ! [V5x:$i] : ((mem@V5x@A_27b) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V5x)@V2t)) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@(ap@V4g@V5x))@V1s))))) & (( ! [V6x:$i] : ((mem@V6x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V6x)@V1s)) => ((ap@V4g@(ap@V0f@V6x)) = V6x)))) & ( ! [V7x:$i] : ((mem@V7x@A_27b) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V7x)@V2t)) => ((ap@V0f@(ap@V4g@V7x)) = V7x))))))))))))))))))).
thf(conj_thm_2Epred__set_2EBIJ__INSERT,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1e:$i] : ((mem@V1e@A_27a) => ( ! [V2s:$i] : ((mem@V2s@(arr@A_27a@bool)) => ( ! [V3t:$i] : ((mem@V3t@(arr@A_27b@bool)) => ((p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27b)@V0f)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V1e)@V2s))@V3t)) <=> (((~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1e)@V2s))) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@(ap@V0f@V1e))@V3t)) & (p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27b)@V0f)@V2s)@(ap@(ap@(c_2Epred__set_2EDELETE@A_27b)@V3t)@(ap@V0f@V1e)))))) | ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1e)@V2s)) & (p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27b)@V0f)@V2s)@V3t)))))))))))))))).
thf(ax_thm_2Epred__set_2ERINV__LO,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2y:$i] : ((mem@V2y@A_27b) => ((ap@(ap@(ap@(c_2Epred__set_2ERINV@A_27a@A_27b)@V0f)@V1s)@V2y) = (ap@(c_2Eoption_2ETHE@A_27a)@(ap@(ap@(ap@(c_2Epred__set_2ELINV__OPT@A_27a@A_27b)@V0f)@V1s)@V2y)))))))))))).
thf(conj_thm_2Epred__set_2ERINV__DEF,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27b@bool)) => ((p@(ap@(ap@(ap@(c_2Epred__set_2ESURJ@A_27a@A_27b)@V0f)@V1s)@V2t)) => ( ! [V3x:$i] : ((mem@V3x@A_27b) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V3x)@V2t)) => ((ap@V0f@(ap@(ap@(ap@(c_2Epred__set_2ERINV@A_27a@A_27b)@V0f)@V1s)@V3x)) = V3x)))))))))))))).
thf(conj_thm_2Epred__set_2ESURJ__INJ__INV,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27b@bool)) => ((p@(ap@(ap@(ap@(c_2Epred__set_2ESURJ@A_27a@A_27b)@V0f)@V1s)@V2t)) => (? [V3g:$i] : ((mem@V3g@(arr@A_27b@A_27a)) & ((p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27b@A_27a)@V3g)@V2t)@V1s)) & ( ! [V4y:$i] : ((mem@V4y@A_27b) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V4y)@V2t)) => ((ap@V0f@(ap@V3g@V4y)) = V4y))))))))))))))))).
thf(ax_thm_2Epred__set_2EFINITE__DEF,axiom,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s)) <=> ( ! [V1P:$i] : ((mem@V1P@(arr@(arr@A_27a@bool)@bool)) => (((p@(ap@V1P@(c_2Epred__set_2EEMPTY@A_27a))) & ( ! [V2s:$i] : ((mem@V2s@(arr@A_27a@bool)) => ((p@(ap@V1P@V2s)) => ( ! [V3e:$i] : ((mem@V3e@A_27a) => (p@(ap@V1P@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V3e)@V2s))))))))) => (p@(ap@V1P@V0s)))))))))).
thf(conj_thm_2Epred__set_2EFINITE__EMPTY,lemma,( ! [A_27a:del]: (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@(c_2Epred__set_2EEMPTY@A_27a))))).
thf(conj_thm_2Epred__set_2EFINITE__INDUCT,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@(arr@A_27a@bool)@bool)) => (((p@(ap@V0P@(c_2Epred__set_2EEMPTY@A_27a))) & ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => (((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1s)) & (p@(ap@V0P@V1s))) => ( ! [V2e:$i] : ((mem@V2e@A_27a) => ((~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2e)@V1s))) => (p@(ap@V0P@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V2e)@V1s)))))))))) => ( ! [V3s:$i] : ((mem@V3s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V3s)) => (p@(ap@V0P@V3s)))))))))).
thf(conj_thm_2Epred__set_2EFINITE__INSERT,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@V1s))) <=> (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1s))))))))).
thf(conj_thm_2Epred__set_2EFINITE__DELETE,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@(ap@(ap@(c_2Epred__set_2EDELETE@A_27a)@V1s)@V0x))) <=> (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1s))))))))).
thf(conj_thm_2Epred__set_2EFINITE__REST,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s)) => (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@(ap@(c_2Epred__set_2EREST@A_27a)@V0s)))))))).
thf(conj_thm_2Epred__set_2EFINITE__REST__EQ,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@(ap@(c_2Epred__set_2EREST@A_27a)@V0s))) <=> (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s))))))).
thf(conj_thm_2Epred__set_2EFINITE__UNION,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V0s)@V1t))) <=> ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s)) & (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1t)))))))))).
thf(conj_thm_2Epred__set_2EINTER__FINITE,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@(ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V0s)@V1t)))))))))).
thf(conj_thm_2Epred__set_2ESUBSET__FINITE,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V1t)@V0s)) => (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1t)))))))))).
thf(conj_thm_2Epred__set_2ESUBSET__FINITE__I,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => (((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s)) & (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V1t)@V0s))) => (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1t))))))))).
thf(conj_thm_2Epred__set_2EPSUBSET__FINITE,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2EPSUBSET@A_27a)@V1t)@V0s)) => (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1t)))))))))).
thf(conj_thm_2Epred__set_2EFINITE__DIFF,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@(ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@V0s)@V1t)))))))))).
thf(conj_thm_2Epred__set_2EFINITE__DIFF__down,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1Q:$i] : ((mem@V1Q@(arr@A_27a@bool)) => (((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@(ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@V0P)@V1Q))) & (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1Q))) => (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0P))))))))).
thf(conj_thm_2Epred__set_2EFINITE__SING,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@(c_2Epred__set_2EEMPTY@A_27a)))))))).
thf(conj_thm_2Epred__set_2ESING__FINITE,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2ESING@A_27a)@V0s)) => (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s))))))).
thf(conj_thm_2Epred__set_2EIMAGE__FINITE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s)) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27a@A_27b)) => (p@(ap@(c_2Epred__set_2EFINITE@A_27b)@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V1f)@V0s))))))))))).
thf(conj_thm_2Epred__set_2EFINITELY__INJECTIVE__IMAGE__FINITE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => (( ! [V1x:$i] : ((mem@V1x@A_27b) => (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@(ap@(c_2Epred__set_2EGSPEC@A_27a@A_27a)@(lam@A_27a@(^ [V2y:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27a@bool)@V2y)@(ap@(ap@(c_2Emin_2E_3D@A_27b)@V1x)@(ap@V0f@V2y)))))))))) => ( ! [V3s:$i] : ((mem@V3s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27b)@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@V3s))) <=> (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V3s))))))))))).
thf(conj_thm_2Epred__set_2EINJECTIVE__IMAGE__FINITE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => (( ! [V1x:$i] : ((mem@V1x@A_27a) => ( ! [V2y:$i] : ((mem@V2y@A_27a) => (((ap@V0f@V1x) = (ap@V0f@V2y)) <=> (V1x = V2y)))))) => ( ! [V3s:$i] : ((mem@V3s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27b)@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@V3s))) <=> (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V3s))))))))))).
thf(conj_thm_2Epred__set_2EFINITE__INJ,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27b@bool)) => (((p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27a@A_27b)@V0f)@V1s)@V2t)) & (p@(ap@(c_2Epred__set_2EFINITE@A_27b)@V2t))) => (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1s)))))))))))).
thf(ax_thm_2Epred__set_2EREL__RESTRICT__DEF,axiom,( ! [A_27a:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27a@bool))) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ( ! [V3y:$i] : ((mem@V3y@A_27a) => ((p@(ap@(ap@(ap@(ap@(c_2Epred__set_2EREL__RESTRICT@A_27a)@V0R)@V1s)@V2x)@V3y)) <=> ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V1s)) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3y)@V1s)) & (p@(ap@(ap@V0R@V2x)@V3y))))))))))))))).
thf(conj_thm_2Epred__set_2EREL__RESTRICT__EMPTY,lemma,( ! [A_27a:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27a@bool))) => ((ap@(ap@(c_2Epred__set_2EREL__RESTRICT@A_27a)@V0R)@(c_2Epred__set_2EEMPTY@A_27a)) = (c_2Erelation_2EEMPTY__REL@A_27a)))))).
thf(conj_thm_2Epred__set_2EREL__RESTRICT__SUBSET,lemma,( ! [A_27a:del]: ( ! [V0s1:$i] : ((mem@V0s1@(arr@A_27a@bool)) => ( ! [V1s2:$i] : ((mem@V1s2@(arr@A_27a@bool)) => ( ! [V2R:$i] : ((mem@V2R@(arr@A_27a@(arr@A_27a@bool))) => ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V0s1)@V1s2)) => (p@(ap@(ap@(c_2Erelation_2ERSUBSET@A_27a@A_27a)@(ap@(ap@(c_2Epred__set_2EREL__RESTRICT@A_27a)@V2R)@V0s1))@(ap@(ap@(c_2Epred__set_2EREL__RESTRICT@A_27a)@V2R)@V1s2)))))))))))).
thf(ax_thm_2Epred__set_2ECARD__DEF,axiom,( ! [A_27a:del]: (((surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27a)@(c_2Epred__set_2EEMPTY@A_27a))) = fo__c_2Enum_2E0) & ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ((surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27a)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V1x)@V0s))) = (surj__ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1x)@V0s))@(ap@(c_2Epred__set_2ECARD@A_27a)@V0s))@(ap@c_2Enum_2ESUC@(ap@(c_2Epred__set_2ECARD@A_27a)@V0s))))))))))))).
thf(conj_thm_2Epred__set_2ECARD__EMPTY,lemma,( ! [A_27a:del]: ((surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27a)@(c_2Epred__set_2EEMPTY@A_27a))) = fo__c_2Enum_2E0))).
thf(conj_thm_2Epred__set_2ECARD__INSERT,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ((surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27a)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V1x)@V0s))) = (surj__ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1x)@V0s))@(ap@(c_2Epred__set_2ECARD@A_27a)@V0s))@(ap@c_2Enum_2ESUC@(ap@(c_2Epred__set_2ECARD@A_27a)@V0s)))))))))))).
thf(conj_thm_2Epred__set_2ECARD__EQ__0,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s)) => (((surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27a)@V0s)) = fo__c_2Enum_2E0) <=> (V0s = (c_2Epred__set_2EEMPTY@A_27a)))))))).
thf(conj_thm_2Epred__set_2ECARD__DELETE,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ((surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27a)@(ap@(ap@(c_2Epred__set_2EDELETE@A_27a)@V0s)@V1x))) = (surj__ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1x)@V0s))@(ap@(ap@c_2Earithmetic_2E_2D@(ap@(c_2Epred__set_2ECARD@A_27a)@V0s))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@(c_2Epred__set_2ECARD@A_27a)@V0s))))))))))).
thf(conj_thm_2Epred__set_2ECARD__INTER__LESS__EQ,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(c_2Epred__set_2ECARD@A_27a)@(ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V0s)@V1t)))@(ap@(c_2Epred__set_2ECARD@A_27a)@V0s)))))))))).
thf(conj_thm_2Epred__set_2ECARD__UNION,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1t)) => ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(ap@(c_2Epred__set_2ECARD@A_27a)@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V0s)@V1t)))@(ap@(c_2Epred__set_2ECARD@A_27a)@(ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V0s)@V1t)))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(ap@(c_2Epred__set_2ECARD@A_27a)@V0s))@(ap@(c_2Epred__set_2ECARD@A_27a)@V1t)))))))))))).
thf(conj_thm_2Epred__set_2ECARD__UNION__EQN,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => (((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s)) & (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1t))) => ((surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27a)@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V0s)@V1t))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2D@(ap@(ap@c_2Earithmetic_2E_2B@(ap@(c_2Epred__set_2ECARD@A_27a)@V0s))@(ap@(c_2Epred__set_2ECARD@A_27a)@V1t)))@(ap@(c_2Epred__set_2ECARD@A_27a)@(ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V0s)@V1t)))))))))))).
thf(conj_thm_2Epred__set_2ECARD__SUBSET,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V1t)@V0s)) => (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(c_2Epred__set_2ECARD@A_27a)@V1t))@(ap@(c_2Epred__set_2ECARD@A_27a)@V0s))))))))))).
thf(conj_thm_2Epred__set_2ECARD__PSUBSET,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2EPSUBSET@A_27a)@V1t)@V0s)) => (p@(ap@(ap@c_2Eprim__rec_2E_3C@(ap@(c_2Epred__set_2ECARD@A_27a)@V1t))@(ap@(c_2Epred__set_2ECARD@A_27a)@V0s))))))))))).
thf(conj_thm_2Epred__set_2ESUBSET__EQ__CARD,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => (((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1t)) & (((surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27a)@V0s)) = (surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27a)@V1t))) & (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V0s)@V1t)))) => (V0s = V1t))))))))).
thf(conj_thm_2Epred__set_2ECARD__SING,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ((surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27a)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@(c_2Epred__set_2EEMPTY@A_27a)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))).
thf(conj_thm_2Epred__set_2ESING__IFF__CARD1,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2ESING@A_27a)@V0s)) <=> (((surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27a)@V0s)) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))) & (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s)))))))).
thf(conj_thm_2Epred__set_2ECARD__DIFF,lemma,( ! [A_27a:del]: ( ! [V0t:$i] : ((mem@V0t@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0t)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1s)) => ((surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27a)@(ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@V1s)@V0t))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2D@(ap@(c_2Epred__set_2ECARD@A_27a)@V1s))@(ap@(c_2Epred__set_2ECARD@A_27a)@(ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V1s)@V0t))))))))))))).
thf(conj_thm_2Epred__set_2ECARD__DIFF__EQN,lemma,( ! [A_27a:del]: ( ! [V0t:$i] : ((mem@V0t@(arr@A_27a@bool)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1s)) => ((surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27a)@(ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@V1s)@V0t))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2D@(ap@(c_2Epred__set_2ECARD@A_27a)@V1s))@(ap@(c_2Epred__set_2ECARD@A_27a)@(ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V1s)@V0t)))))))))))).
thf(conj_thm_2Epred__set_2ELESS__CARD__DIFF,lemma,( ! [A_27a:del]: ( ! [V0t:$i] : ((mem@V0t@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0t)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1s)) => ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(ap@(c_2Epred__set_2ECARD@A_27a)@V0t))@(ap@(c_2Epred__set_2ECARD@A_27a)@V1s))) => (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@(c_2Epred__set_2ECARD@A_27a)@(ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@V1s)@V0t))))))))))))).
thf(conj_thm_2Epred__set_2EBIJ__FINITE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27b@bool)) => (((p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27b)@V0f)@V1s)@V2t)) & (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1s))) => (p@(ap@(c_2Epred__set_2EFINITE@A_27b)@V2t)))))))))))).
thf(conj_thm_2Epred__set_2EBIJ__FINITE__SUBSET,lemma,( ! [A_27a:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@A_27a)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27a@bool)) => (((p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@ty_2Enum_2Enum@A_27a)@V0f)@(c_2Epred__set_2EUNIV@ty_2Enum_2Enum))@V1s)) & ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V2t)) & (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V2t)@V1s)))) => (? [V3N:tp__ty_2Enum_2Enum] : ( ! [V4n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V3N))@(inj__ty_2Enum_2Enum @ V4n))) => (~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@(ap@V0f@(inj__ty_2Enum_2Enum @ V4n)))@V2t))))))))))))))).
thf(conj_thm_2Epred__set_2EFINITE__BIJ,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27b@bool)) => (((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1s)) & (p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27b)@V0f)@V1s)@V2t))) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27b)@V2t)) & ((surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27a)@V1s)) = (surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27b)@V2t)))))))))))))).
thf(conj_thm_2Epred__set_2EFINITE__BIJ__CARD,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27b@bool)) => (((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1s)) & (p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27b)@V0f)@V1s)@V2t))) => ((surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27a)@V1s)) = (surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27b)@V2t))))))))))))).
thf(conj_thm_2Epred__set_2EFINITE__BIJ__CARD__EQ,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0S:$i] : ((mem@V0S@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0S)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => ( ! [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27b)) => (((p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27b)@V2f)@V0S)@V1t)) & (p@(ap@(c_2Epred__set_2EFINITE@A_27b)@V1t))) => ((surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27a)@V0S)) = (surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27b)@V1t)))))))))))))).
thf(conj_thm_2Epred__set_2ECARD__INJ__IMAGE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ((( ! [V2x:$i] : ((mem@V2x@A_27a) => ( ! [V3y:$i] : ((mem@V3y@A_27a) => (((ap@V0f@V2x) = (ap@V0f@V3y)) <=> (V2x = V3y)))))) & (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1s))) => ((surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27b)@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@V1s))) = (surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27a)@V1s))))))))))).
thf(conj_thm_2Epred__set_2ECARD__IMAGE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1s)) => (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(c_2Epred__set_2ECARD@A_27b)@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@V1s)))@(ap@(c_2Epred__set_2ECARD@A_27a)@V1s))))))))))).
thf(conj_thm_2Epred__set_2ESURJ__CARD,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1s)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27b@bool)) => ((p@(ap@(ap@(ap@(c_2Epred__set_2ESURJ@A_27a@A_27b)@V0f)@V1s)@V2t)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27b)@V2t)) & (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(c_2Epred__set_2ECARD@A_27b)@V2t))@(ap@(c_2Epred__set_2ECARD@A_27a)@V1s))))))))))))))).
thf(conj_thm_2Epred__set_2EFINITE__SURJ,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27a@A_27b)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27b@bool)) => (((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s)) & (p@(ap@(ap@(ap@(c_2Epred__set_2ESURJ@A_27a@A_27b)@V1f)@V0s)@V2t))) => (p@(ap@(c_2Epred__set_2EFINITE@A_27b)@V2t)))))))))))).
thf(conj_thm_2Epred__set_2EFINITE__SURJ__BIJ,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27a@A_27b)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27b@bool)) => (((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s)) & ((p@(ap@(ap@(ap@(c_2Epred__set_2ESURJ@A_27a@A_27b)@V1f)@V0s)@V2t)) & ((surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27b)@V2t)) = (surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27a)@V0s))))) => (p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27b)@V1f)@V0s)@V2t)))))))))))).
thf(conj_thm_2Epred__set_2EFINITE__COMPLETE__INDUCTION,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@(arr@A_27a@bool)@bool)) => (( ! [V1x:$i] : ((mem@V1x@(arr@A_27a@bool)) => (( ! [V2y:$i] : ((mem@V2y@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2EPSUBSET@A_27a)@V2y)@V1x)) => (p@(ap@V0P@V2y))))) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1x)) => (p@(ap@V0P@V1x)))))) => ( ! [V3x:$i] : ((mem@V3x@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V3x)) => (p@(ap@V0P@V3x)))))))))).
thf(conj_thm_2Epred__set_2EINJ__CARD__IMAGE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => ( ! [V2s:$i] : ((mem@V2s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V2s)) => ((p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27a@A_27b)@V0f)@V2s)@V1t)) => ((surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27b)@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@V2s))) = (surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27a)@V2s)))))))))))))).
thf(conj_thm_2Epred__set_2EINJ__CARD,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27b@bool)) => (((p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27a@A_27b)@V0f)@V1s)@V2t)) & (p@(ap@(c_2Epred__set_2EFINITE@A_27b)@V2t))) => (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(c_2Epred__set_2ECARD@A_27a)@V1s))@(ap@(c_2Epred__set_2ECARD@A_27b)@V2t))))))))))))).
thf(conj_thm_2Epred__set_2EPHP,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27b@bool)) => (((p@(ap@(c_2Epred__set_2EFINITE@A_27b)@V2t)) & (p@(ap@(ap@c_2Eprim__rec_2E_3C@(ap@(c_2Epred__set_2ECARD@A_27b)@V2t))@(ap@(c_2Epred__set_2ECARD@A_27a)@V1s)))) => (~~ (p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27a@A_27b)@V0f)@V1s)@V2t))))))))))))).
thf(conj_thm_2Epred__set_2EINJ__CARD__IMAGE__EQ,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27b@bool)) => ((p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27a@A_27b)@V0f)@V1s)@V2t)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1s)) => ((surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27b)@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@V1s))) = (surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27a)@V1s)))))))))))))).
thf(ax_thm_2Epred__set_2Ecount__def,axiom,( ! [V0n:tp__ty_2Enum_2Enum] : ((ap@c_2Epred__set_2Ecount@(inj__ty_2Enum_2Enum @ V0n)) = (ap@(c_2Epred__set_2EGSPEC@ty_2Enum_2Enum@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V1m:$i] : (ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@bool)@V1m)@(ap@(ap@c_2Eprim__rec_2E_3C@V1m)@(inj__ty_2Enum_2Enum @ V0n))))))))).
thf(conj_thm_2Epred__set_2EIN__COUNT,lemma,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@(c_2Ebool_2EIN@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V0m))@(ap@c_2Epred__set_2Ecount@(inj__ty_2Enum_2Enum @ V1n)))) <=> (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V1n))))))).
thf(conj_thm_2Epred__set_2ECOUNT__applied,lemma,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Epred__set_2Ecount@(inj__ty_2Enum_2Enum @ V1n))@(inj__ty_2Enum_2Enum @ V0m))) <=> (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V1n))))))).
thf(conj_thm_2Epred__set_2ECOUNT__ZERO,lemma,((ap@c_2Epred__set_2Ecount@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)) = (c_2Epred__set_2EEMPTY@ty_2Enum_2Enum))).
thf(conj_thm_2Epred__set_2ECOUNT__SUC,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ((ap@c_2Epred__set_2Ecount@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V0n))) = (ap@(ap@(c_2Epred__set_2EINSERT@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V0n))@(ap@c_2Epred__set_2Ecount@(inj__ty_2Enum_2Enum @ V0n)))))).
thf(conj_thm_2Epred__set_2EFINITE__COUNT,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : (p@(ap@(c_2Epred__set_2EFINITE@ty_2Enum_2Enum)@(ap@c_2Epred__set_2Ecount@(inj__ty_2Enum_2Enum @ V0n)))))).
thf(conj_thm_2Epred__set_2ECARD__COUNT,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@ty_2Enum_2Enum)@(ap@c_2Epred__set_2Ecount@(inj__ty_2Enum_2Enum @ V0n)))) = V0n))).
thf(conj_thm_2Epred__set_2ECOUNT__11,lemma,( ! [V0n1:tp__ty_2Enum_2Enum] : ( ! [V1n2:tp__ty_2Enum_2Enum] : (((ap@c_2Epred__set_2Ecount@(inj__ty_2Enum_2Enum @ V0n1)) = (ap@c_2Epred__set_2Ecount@(inj__ty_2Enum_2Enum @ V1n2))) <=> (V0n1 = V1n2))))).
thf(conj_thm_2Epred__set_2ENOT__IN__FINITE,lemma,( ! [A_27a:del]: ((~~ (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@(c_2Epred__set_2EUNIV@A_27a)))) <=> ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s)) => (? [V1x:$i] : ((mem@V1x@A_27a) & (~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1x)@V0s))))))))))).
thf(conj_thm_2Epred__set_2EINFINITE__INHAB,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ((~~ (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0P))) => (? [V1x:$i] : ((mem@V1x@A_27a) & (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1x)@V0P))))))))).
thf(conj_thm_2Epred__set_2EIMAGE__11__INFINITE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => (( ! [V1x:$i] : ((mem@V1x@A_27a) => ( ! [V2y:$i] : ((mem@V2y@A_27a) => (((ap@V0f@V1x) = (ap@V0f@V2y)) => (V1x = V2y)))))) => ( ! [V3s:$i] : ((mem@V3s@(arr@A_27a@bool)) => ((~~ (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V3s))) => (~~ (p@(ap@(c_2Epred__set_2EFINITE@A_27b)@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@V3s))))))))))))).
thf(conj_thm_2Epred__set_2EINFINITE__SUBSET,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((~~ (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s))) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V0s)@V1t)) => (~~ (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1t))))))))))).
thf(conj_thm_2Epred__set_2EIN__INFINITE__NOT__FINITE,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => (((~~ (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s))) & (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1t))) => (? [V2x:$i] : ((mem@V2x@A_27a) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V0s)) & (~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V1t))))))))))))).
thf(conj_thm_2Epred__set_2EINFINITE__INJ,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27b@bool)) => (((p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27a@A_27b)@V0f)@V1s)@V2t)) & (~~ (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1s)))) => (~~ (p@(ap@(c_2Epred__set_2EFINITE@A_27b)@V2t))))))))))))).
thf(conj_thm_2Epred__set_2EINFINITE__INJ__NOT__SURJ,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((~~ (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s))) <=> (? [V1f:$i] : ((mem@V1f@(arr@A_27a@A_27a)) & ((p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27a@A_27a)@V1f)@V0s)@V0s)) & (~~ (p@(ap@(ap@(ap@(c_2Epred__set_2ESURJ@A_27a@A_27a)@V1f)@V0s)@V0s))))))))))).
thf(conj_thm_2Epred__set_2EINFINITE__UNIV,lemma,( ! [A_27a:del]: ((~~ (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@(c_2Epred__set_2EUNIV@A_27a)))) <=> (? [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27a)) & (( ! [V1x:$i] : ((mem@V1x@A_27a) => ( ! [V2y:$i] : ((mem@V2y@A_27a) => (((ap@V0f@V1x) = (ap@V0f@V2y)) => (V1x = V2y)))))) & (? [V3y:$i] : ((mem@V3y@A_27a) & ( ! [V4x:$i] : ((mem@V4x@A_27a) => (~~ ((ap@V0f@V4x) = V3y)))))))))))).
thf(conj_thm_2Epred__set_2EINFINITE__NUM__UNIV,lemma,(~~ (p@(ap@(c_2Epred__set_2EFINITE@ty_2Enum_2Enum)@(c_2Epred__set_2EUNIV@ty_2Enum_2Enum))))).
thf(conj_thm_2Epred__set_2EFINITE__PSUBSET__INFINITE,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((~~ (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s))) <=> ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1t)) => ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V1t)@V0s)) => (p@(ap@(ap@(c_2Epred__set_2EPSUBSET@A_27a)@V1t)@V0s))))))))))).
thf(conj_thm_2Epred__set_2EFINITE__PSUBSET__UNIV,lemma,( ! [A_27a:del]: ((~~ (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@(c_2Epred__set_2EUNIV@A_27a)))) <=> ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s)) => (p@(ap@(ap@(c_2Epred__set_2EPSUBSET@A_27a)@V0s)@(c_2Epred__set_2EUNIV@A_27a))))))))).
thf(conj_thm_2Epred__set_2EINFINITE__DIFF__FINITE,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => (((~~ (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s))) & (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1t))) => (~~ ((ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@V0s)@V1t) = (c_2Epred__set_2EEMPTY@A_27a)))))))))).
thf(conj_thm_2Epred__set_2EFINITE__BIJ__COUNT__EQ,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s)) <=> (? [V1c:$i] : ((mem@V1c@(arr@ty_2Enum_2Enum@A_27a)) & (? [V2n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@ty_2Enum_2Enum@A_27a)@V1c)@(ap@c_2Epred__set_2Ecount@(inj__ty_2Enum_2Enum @ V2n)))@V0s)))))))))).
thf(conj_thm_2Epred__set_2EFINITE__BIJ__COUNT,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s)) => (? [V1f:$i] : ((mem@V1f@(arr@ty_2Enum_2Enum@A_27a)) & (? [V2b:tp__ty_2Enum_2Enum] : (p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@ty_2Enum_2Enum@A_27a)@V1f)@(ap@c_2Epred__set_2Ecount@(inj__ty_2Enum_2Enum @ V2b)))@V0s)))))))))).
thf(conj_thm_2Epred__set_2EFINITE__ISO__NUM,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s)) => (? [V1f:$i] : ((mem@V1f@(arr@ty_2Enum_2Enum@A_27a)) & (( ! [V2n:tp__ty_2Enum_2Enum] : ( ! [V3m:tp__ty_2Enum_2Enum] : (((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V2n))@(ap@(c_2Epred__set_2ECARD@A_27a)@V0s))) & (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V3m))@(ap@(c_2Epred__set_2ECARD@A_27a)@V0s)))) => (((ap@V1f@(inj__ty_2Enum_2Enum @ V2n)) = (ap@V1f@(inj__ty_2Enum_2Enum @ V3m))) => (V2n = V3m))))) & (V0s = (ap@(c_2Epred__set_2EGSPEC@A_27a@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V4n:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27a@bool)@(ap@V1f@V4n))@(ap@(ap@c_2Eprim__rec_2E_3C@V4n)@(ap@(c_2Epred__set_2ECARD@A_27a)@V0s))))))))))))))).
thf(conj_thm_2Epred__set_2EFINITE__WEAK__ENUMERATE,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s)) <=> (? [V1f:$i] : ((mem@V1f@(arr@ty_2Enum_2Enum@A_27a)) & (? [V2b:tp__ty_2Enum_2Enum] : ( ! [V3e:$i] : ((mem@V3e@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3e)@V0s)) <=> (? [V4n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V4n))@(inj__ty_2Enum_2Enum @ V2b))) & (V3e = (ap@V1f@(inj__ty_2Enum_2Enum @ V4n)))))))))))))))).
thf(conj_thm_2Epred__set_2EFINITE__WF__noloops,lemma,( ! [A_27a:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27a@bool))) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1s)) => ((p@(ap@(c_2Erelation_2EWF@A_27a)@(ap@(ap@(c_2Epred__set_2EREL__RESTRICT@A_27a)@V0R)@V1s))) <=> (p@(ap@(c_2Erelation_2Eirreflexive@A_27a)@(ap@(c_2Erelation_2ETC@A_27a)@(ap@(ap@(c_2Epred__set_2EREL__RESTRICT@A_27a)@V0R)@V1s)))))))))))).
thf(conj_thm_2Epred__set_2EFINITE__StrongOrder__WF,lemma,( ! [A_27a:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27a@bool))) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => (((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1s)) & (p@(ap@(c_2Erelation_2EStrongOrder@A_27a)@(ap@(ap@(c_2Epred__set_2EREL__RESTRICT@A_27a)@V0R)@V1s)))) => (p@(ap@(c_2Erelation_2EWF@A_27a)@(ap@(ap@(c_2Epred__set_2EREL__RESTRICT@A_27a)@V0R)@V1s)))))))))).
thf(ax_thm_2Epred__set_2EBIGUNION,axiom,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@(arr@A_27a@bool)@bool)) => ((ap@(c_2Epred__set_2EBIGUNION@A_27a)@V0P) = (ap@(c_2Epred__set_2EGSPEC@A_27a@A_27a)@(lam@A_27a@(^ [V1x:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27a@bool)@V1x)@(ap@(c_2Ebool_2E_3F@(arr@A_27a@bool))@(lam@(arr@A_27a@bool)@(^ [V2s:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@bool))@V2s)@V0P))@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1x)@V2s)))))))))))))).
thf(conj_thm_2Epred__set_2EIN__BIGUNION,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1sos:$i] : ((mem@V1sos@(arr@(arr@A_27a@bool)@bool)) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@(ap@(c_2Epred__set_2EBIGUNION@A_27a)@V1sos))) <=> (? [V2s:$i] : ((mem@V2s@(arr@A_27a@bool)) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@V2s)) & (p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@bool))@V2s)@V1sos)))))))))))).
thf(conj_thm_2Epred__set_2EBIGUNION__applied,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1sos:$i] : ((mem@V1sos@(arr@(arr@A_27a@bool)@bool)) => ((p@(ap@(ap@(c_2Epred__set_2EBIGUNION@A_27a)@V1sos)@V0x)) <=> (? [V2s:$i] : ((mem@V2s@(arr@A_27a@bool)) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@V2s)) & (p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@bool))@V2s)@V1sos)))))))))))).
thf(conj_thm_2Epred__set_2EIN__BIGUNION__IMAGE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(arr@A_27b@bool))) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2y:$i] : ((mem@V2y@A_27b) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V2y)@(ap@(c_2Epred__set_2EBIGUNION@A_27b)@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@(arr@A_27b@bool))@V0f)@V1s)))) <=> (? [V3x:$i] : ((mem@V3x@A_27a) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@V1s)) & (p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V2y)@(ap@V0f@V3x)))))))))))))))).
thf(conj_thm_2Epred__set_2EBIGUNION__EMPTY,lemma,( ! [A_27a:del]: ((ap@(c_2Epred__set_2EBIGUNION@A_27a)@(c_2Epred__set_2EEMPTY@(arr@A_27a@bool))) = (c_2Epred__set_2EEMPTY@A_27a)))).
thf(conj_thm_2Epred__set_2EBIGUNION__EQ__EMPTY,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@(arr@A_27a@bool)@bool)) => ((((ap@(c_2Epred__set_2EBIGUNION@A_27a)@V0P) = (c_2Epred__set_2EEMPTY@A_27a)) <=> ((V0P = (c_2Epred__set_2EEMPTY@(arr@A_27a@bool))) | (V0P = (ap@(ap@(c_2Epred__set_2EINSERT@(arr@A_27a@bool))@(c_2Epred__set_2EEMPTY@A_27a))@(c_2Epred__set_2EEMPTY@(arr@A_27a@bool)))))) & (((c_2Epred__set_2EEMPTY@A_27a) = (ap@(c_2Epred__set_2EBIGUNION@A_27a)@V0P)) <=> ((V0P = (c_2Epred__set_2EEMPTY@(arr@A_27a@bool))) | (V0P = (ap@(ap@(c_2Epred__set_2EINSERT@(arr@A_27a@bool))@(c_2Epred__set_2EEMPTY@A_27a))@(c_2Epred__set_2EEMPTY@(arr@A_27a@bool))))))))))).
thf(conj_thm_2Epred__set_2EBIGUNION__SING,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@(arr@A_27a@bool)) => ((ap@(c_2Epred__set_2EBIGUNION@A_27a)@(ap@(ap@(c_2Epred__set_2EINSERT@(arr@A_27a@bool))@V0x)@(c_2Epred__set_2EEMPTY@(arr@A_27a@bool)))) = V0x))))).
thf(conj_thm_2Epred__set_2EBIGUNION__PAIR,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((ap@(c_2Epred__set_2EBIGUNION@A_27a)@(ap@(ap@(c_2Epred__set_2EINSERT@(arr@A_27a@bool))@V0s)@(ap@(ap@(c_2Epred__set_2EINSERT@(arr@A_27a@bool))@V1t)@(c_2Epred__set_2EEMPTY@(arr@A_27a@bool))))) = (ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V0s)@V1t)))))))).
thf(conj_thm_2Epred__set_2EBIGUNION__UNION,lemma,( ! [A_27a:del]: ( ! [V0s1:$i] : ((mem@V0s1@(arr@(arr@A_27a@bool)@bool)) => ( ! [V1s2:$i] : ((mem@V1s2@(arr@(arr@A_27a@bool)@bool)) => ((ap@(c_2Epred__set_2EBIGUNION@A_27a)@(ap@(ap@(c_2Epred__set_2EUNION@(arr@A_27a@bool))@V0s1)@V1s2)) = (ap@(ap@(c_2Epred__set_2EUNION@A_27a)@(ap@(c_2Epred__set_2EBIGUNION@A_27a)@V0s1))@(ap@(c_2Epred__set_2EBIGUNION@A_27a)@V1s2))))))))).
thf(conj_thm_2Epred__set_2EDISJOINT__BIGUNION,lemma,( ! [A_27a:del]: (( ! [V0s:$i] : ((mem@V0s@(arr@(arr@A_27a@bool)@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@(ap@(c_2Epred__set_2EBIGUNION@A_27a)@V0s))@V1t)) <=> ( ! [V2s_27:$i] : ((mem@V2s_27@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@bool))@V2s_27)@V0s)) => (p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@V2s_27)@V1t)))))))))) & ( ! [V3s:$i] : ((mem@V3s@(arr@(arr@A_27a@bool)@bool)) => ( ! [V4t:$i] : ((mem@V4t@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@V4t)@(ap@(c_2Epred__set_2EBIGUNION@A_27a)@V3s))) <=> ( ! [V5s_27:$i] : ((mem@V5s_27@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@bool))@V5s_27)@V3s)) => (p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@V4t)@V5s_27))))))))))))).
thf(conj_thm_2Epred__set_2EBIGUNION__INSERT,conjecture,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1P:$i] : ((mem@V1P@(arr@(arr@A_27a@bool)@bool)) => ((ap@(c_2Epred__set_2EBIGUNION@A_27a)@(ap@(ap@(c_2Epred__set_2EINSERT@(arr@A_27a@bool))@V0s)@V1P)) = (ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V0s)@(ap@(c_2Epred__set_2EBIGUNION@A_27a)@V1P))))))))).
