include('Axioms/bit_2.ax').
tff(tp_c_2Epred__set_2EBIGINTER,type,(c_2Epred__set_2EBIGINTER:del > $i)).
tff(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))))).
tff(tp_c_2Epred__set_2EBIGUNION,type,(c_2Epred__set_2EBIGUNION:del > $i)).
tff(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))))).
tff(tp_c_2Epred__set_2EBIJ,type,(c_2Epred__set_2EBIJ:(del * del) > $i)).
tff(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))))))).
tff(tp_c_2Epred__set_2ECARD,type,(c_2Epred__set_2ECARD:del > $i)).
tff(mem_c_2Epred__set_2ECARD,axiom,( ! [A_27a:del] : mem(c_2Epred__set_2ECARD(A_27a),arr(arr(A_27a,bool),ty_2Enum_2Enum)))).
tff(tp_c_2Epred__set_2ECHOICE,type,(c_2Epred__set_2ECHOICE:del > $i)).
tff(mem_c_2Epred__set_2ECHOICE,axiom,( ! [A_27a:del] : mem(c_2Epred__set_2ECHOICE(A_27a),arr(arr(A_27a,bool),A_27a)))).
tff(tp_c_2Epred__set_2ECOMPL,type,(c_2Epred__set_2ECOMPL:del > $i)).
tff(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))))).
tff(tp_c_2Epred__set_2ECROSS,type,(c_2Epred__set_2ECROSS:(del * del) > $i)).
tff(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))))))).
tff(tp_c_2Epred__set_2EDELETE,type,(c_2Epred__set_2EDELETE:del > $i)).
tff(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)))))).
tff(tp_c_2Epred__set_2EDFUNSET,type,(c_2Epred__set_2EDFUNSET:(del * del) > $i)).
tff(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))))))).
tff(tp_c_2Epred__set_2EDIFF,type,(c_2Epred__set_2EDIFF:del > $i)).
tff(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)))))).
tff(tp_c_2Epred__set_2EDISJOINT,type,(c_2Epred__set_2EDISJOINT:del > $i)).
tff(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))))).
tff(tp_c_2Epred__set_2EEMPTY,type,(c_2Epred__set_2EEMPTY:del > $i)).
tff(mem_c_2Epred__set_2EEMPTY,axiom,( ! [A_27a:del] : mem(c_2Epred__set_2EEMPTY(A_27a),arr(A_27a,bool)))).
tff(tp_c_2Epred__set_2EFINITE,type,(c_2Epred__set_2EFINITE:del > $i)).
tff(mem_c_2Epred__set_2EFINITE,axiom,( ! [A_27a:del] : mem(c_2Epred__set_2EFINITE(A_27a),arr(arr(A_27a,bool),bool)))).
tff(tp_c_2Epred__set_2EFUNSET,type,(c_2Epred__set_2EFUNSET:(del * del) > $i)).
tff(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))))))).
tff(tp_c_2Epred__set_2EGSPEC,type,(c_2Epred__set_2EGSPEC:(del * del) > $i)).
tff(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)))))).
tff(tp_c_2Epred__set_2EIMAGE,type,(c_2Epred__set_2EIMAGE:(del * del) > $i)).
tff(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))))))).
tff(tp_c_2Epred__set_2EINJ,type,(c_2Epred__set_2EINJ:(del * del) > $i)).
tff(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))))))).
tff(tp_c_2Epred__set_2EINSERT,type,(c_2Epred__set_2EINSERT:del > $i)).
tff(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)))))).
tff(tp_c_2Epred__set_2EINTER,type,(c_2Epred__set_2EINTER:del > $i)).
tff(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)))))).
tff(tp_c_2Epred__set_2EITSET,type,(c_2Epred__set_2EITSET:(del * del) > $i)).
tff(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))))))).
tff(tp_c_2Epred__set_2ELINV,type,(c_2Epred__set_2ELINV:(del * del) > $i)).
tff(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))))))).
tff(tp_c_2Epred__set_2ELINV__OPT,type,(c_2Epred__set_2ELINV__OPT:(del * del) > $i)).
tff(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)))))))).
tff(tp_c_2Epred__set_2EMAX__SET,type,(c_2Epred__set_2EMAX__SET:$i)).
tff(mem_c_2Epred__set_2EMAX__SET,axiom,mem(c_2Epred__set_2EMAX__SET,arr(arr(ty_2Enum_2Enum,bool),ty_2Enum_2Enum))).
tff(tp_c_2Epred__set_2EMIN__SET,type,(c_2Epred__set_2EMIN__SET:$i)).
tff(mem_c_2Epred__set_2EMIN__SET,axiom,mem(c_2Epred__set_2EMIN__SET,arr(arr(ty_2Enum_2Enum,bool),ty_2Enum_2Enum))).
tff(tp_c_2Epred__set_2EPOW,type,(c_2Epred__set_2EPOW:del > $i)).
tff(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))))).
tff(tp_c_2Epred__set_2EPREIMAGE,type,(c_2Epred__set_2EPREIMAGE:(del * del) > $i)).
tff(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))))))).
tff(tp_c_2Epred__set_2EPROD__IMAGE,type,(c_2Epred__set_2EPROD__IMAGE:del > $i)).
tff(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))))).
tff(tp_c_2Epred__set_2EPROD__SET,type,(c_2Epred__set_2EPROD__SET:$i)).
tff(mem_c_2Epred__set_2EPROD__SET,axiom,mem(c_2Epred__set_2EPROD__SET,arr(arr(ty_2Enum_2Enum,bool),ty_2Enum_2Enum))).
tff(tp_c_2Epred__set_2EPSUBSET,type,(c_2Epred__set_2EPSUBSET:del > $i)).
tff(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))))).
tff(tp_c_2Epred__set_2EREL__RESTRICT,type,(c_2Epred__set_2EREL__RESTRICT:del > $i)).
tff(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))))))).
tff(tp_c_2Epred__set_2EREST,type,(c_2Epred__set_2EREST:del > $i)).
tff(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))))).
tff(tp_c_2Epred__set_2ERINV,type,(c_2Epred__set_2ERINV:(del * del) > $i)).
tff(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))))))).
tff(tp_c_2Epred__set_2ESING,type,(c_2Epred__set_2ESING:del > $i)).
tff(mem_c_2Epred__set_2ESING,axiom,( ! [A_27a:del] : mem(c_2Epred__set_2ESING(A_27a),arr(arr(A_27a,bool),bool)))).
tff(tp_c_2Epred__set_2ESUBSET,type,(c_2Epred__set_2ESUBSET:del > $i)).
tff(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))))).
tff(tp_c_2Epred__set_2ESUM__IMAGE,type,(c_2Epred__set_2ESUM__IMAGE:del > $i)).
tff(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))))).
tff(tp_c_2Epred__set_2ESUM__SET,type,(c_2Epred__set_2ESUM__SET:$i)).
tff(mem_c_2Epred__set_2ESUM__SET,axiom,mem(c_2Epred__set_2ESUM__SET,arr(arr(ty_2Enum_2Enum,bool),ty_2Enum_2Enum))).
tff(tp_c_2Epred__set_2ESURJ,type,(c_2Epred__set_2ESURJ:(del * del) > $i)).
tff(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))))))).
tff(tp_c_2Epred__set_2EUNION,type,(c_2Epred__set_2EUNION:del > $i)).
tff(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)))))).
tff(tp_c_2Epred__set_2EUNIV,type,(c_2Epred__set_2EUNIV:del > $i)).
tff(mem_c_2Epred__set_2EUNIV,axiom,( ! [A_27a:del] : mem(c_2Epred__set_2EUNIV(A_27a),arr(A_27a,bool)))).
tff(tp_c_2Epred__set_2Echooser,type,(c_2Epred__set_2Echooser:del > $i)).
tff(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))))).
tff(tp_c_2Epred__set_2Ecount,type,(c_2Epred__set_2Ecount:$i)).
tff(mem_c_2Epred__set_2Ecount,axiom,mem(c_2Epred__set_2Ecount,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool)))).
tff(stp_fo_c_2Epred__set_2Ecount,type,(fo__c_2Epred__set_2Ecount:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__o)).
tff(stp_eq_fo_c_2Epred__set_2Ecount,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__o(fo__c_2Epred__set_2Ecount(X0,X1)) = ap(ap(c_2Epred__set_2Ecount,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Epred__set_2Ecountable,type,(c_2Epred__set_2Ecountable:del > $i)).
tff(mem_c_2Epred__set_2Ecountable,axiom,( ! [A_27a:del] : mem(c_2Epred__set_2Ecountable(A_27a),arr(arr(A_27a,bool),bool)))).
tff(tp_c_2Epred__set_2Eenumerate,type,(c_2Epred__set_2Eenumerate:del > $i)).
tff(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))))).
tff(tp_c_2Epred__set_2Eequiv__on,type,(c_2Epred__set_2Eequiv__on:del > $i)).
tff(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))))).
tff(tp_c_2Epred__set_2Eis__measure__maximal,type,(c_2Epred__set_2Eis__measure__maximal:del > $i)).
tff(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)))))).
tff(tp_c_2Epred__set_2Enum__to__pair,type,(c_2Epred__set_2Enum__to__pair:$i)).
tff(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)))).
tff(tp_c_2Epred__set_2Epair__to__num,type,(c_2Epred__set_2Epair__to__num:$i)).
tff(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))).
tff(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)).
tff(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))))).
tff(tp_c_2Epred__set_2Epairwise,type,(c_2Epred__set_2Epairwise:del > $i)).
tff(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))))).
tff(tp_c_2Epred__set_2Epartition,type,(c_2Epred__set_2Epartition:del > $i)).
tff(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)))))).
tff(tp_c_2Epred__set_2Eschroeder__close,type,(c_2Epred__set_2Eschroeder__close:del > $i)).
tff(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)))))).
tff(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)))))))))).
tff(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)))))))))).
tff(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),f252(A_27a,V1P))) <=> p(ap(V1P,V0x)))))))))).
tff(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))))))))))))).
tff(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)))))))))))))).
tff(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)))))))))))).
tff(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),inj__o(fo__c_2Ebool_2ET)) = ap(V0f,V2x)))))))))))).
tff(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),inj__o(fo__c_2Ebool_2ET)) = ap(V0f,V2x))))))))))))).
tff(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),f253(A_27a,V0P)) = V0P)))))).
tff(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)),f255(A_27a,A_27b,V0P))) = ap(c_2Epair_2EUNCURRY(A_27a,A_27b,bool),V0P)))))))).
tff(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),f256(A_27a,V1P)))) <=> p(ap(V1P,V0y)))))))))).
tff(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)),f258(A_27a,A_27b,V2P))))) <=> p(ap(ap(V2P,V0x),V1y))))))))))))).
tff(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),f259(A_27b,A_27a,V0f,V3P))))))))))))))))).
tff(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),f260(A_27b,A_27a,V2x,V3P)))) <=> (p(ap(V3P,V0a)) & (V1b = V2x))))))))))))))).
tff(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),f261(A_27a,A_27b,V2x,V3P)))) <=> (p(ap(V3P,V1b)) & (V0a = V2x))))))))))))))).
tff(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),f262(A_27a,V2P)))) <=> (p(ap(V2P,V0a)) & (V0a = V1b)))))))))))).
tff(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))))))))))))))))).
tff(ax_thm_2Epred__set_2EEMPTY__DEF,axiom,( ! [A_27a:del]: (c_2Epred__set_2EEMPTY(A_27a) = k(A_27a,c_2Ebool_2EF)))).
tff(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))))))))).
tff(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))))))))).
tff(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)))))).
tff(ax_thm_2Epred__set_2EUNIV__DEF,axiom,( ! [A_27a:del]: (c_2Epred__set_2EUNIV(A_27a) = k(A_27a,c_2Ebool_2ET)))).
tff(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)))))))).
tff(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))))))).
tff(conj_thm_2Epred__set_2EUNIV__NOT__EMPTY,lemma,(( ! [A_27a:del]: (~~ (c_2Epred__set_2EUNIV(A_27a) = c_2Epred__set_2EEMPTY(A_27a)))))).
tff(conj_thm_2Epred__set_2EEMPTY__NOT__UNIV,lemma,(( ! [A_27a:del]: (~~ (c_2Epred__set_2EEMPTY(A_27a) = c_2Epred__set_2EUNIV(A_27a)))))).
tff(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)))))))).
tff(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)))))))))).
tff(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)))))))))))).
tff(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))))))))))))).
tff(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))))))))))))).
tff(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)))))))))))).
tff(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))))))).
tff(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))))))))).
tff(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))))))).
tff(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)))))))).
tff(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)))))))).
tff(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)))))))).
tff(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))))))))))).
tff(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))))))))).
tff(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))))))))))))).
tff(conj_thm_2Epred__set_2EK__SUBSET,lemma,(( ! [A_27a:del]: ( ! [V0x:tp__o] : ( ! [V1y:$i] : (mem(V1y,arr(A_27a,bool)) => (p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Ecombin_2EK(bool,A_27a),inj__o(V0x))),V1y)) <=> ((~~ p(inj__o(V0x))) | p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),c_2Epred__set_2EUNIV(A_27a)),V1y)))))))))).
tff(conj_thm_2Epred__set_2ESUBSET__K,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,arr(A_27a,bool)) => ( ! [V1y:tp__o] : (p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),V0x),ap(c_2Ecombin_2EK(bool,A_27a),inj__o(V1y)))) <=> (p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),V0x),c_2Epred__set_2EEMPTY(A_27a))) | p(inj__o(V1y)))))))))).
tff(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)))))))))).
tff(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)))))))))))).
tff(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)))))))).
tff(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))))))))).
tff(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)))))))).
tff(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))))))))))).
tff(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),f263(A_27a,V1t,V0s))))))))).
tff(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))))))))))))).
tff(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))))))))))))).
tff(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))))))))))).
tff(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)))))).
tff(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))))))))).
tff(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))))))))))).
tff(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))))))))))))).
tff(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))))))))).
tff(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))))))).
tff(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)))))))).
tff(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))))))))))).
tff(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)))))))))))))))).
tff(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),f264(A_27a,V1t,V0s))))))))).
tff(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))))))))))))).
tff(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))))))))))))).
tff(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))))))))))).
tff(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)))))).
tff(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))))))))).
tff(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)))))))))).
tff(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))))))))))))).
tff(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))))))))).
tff(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))))))))).
tff(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))))))))).
tff(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)))))))).
tff(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))))))).
tff(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)))))))))))).
tff(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)))))))))))).
tff(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))))))))).
tff(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)))))))))))))).
tff(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)))))))))).
tff(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)))))))))))))).
tff(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))))))))).
tff(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)))))))).
tff(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)))))))).
tff(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))))))))))))).
tff(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)))))))))))))).
tff(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)))))))))))).
tff(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),f265(A_27a,V1t,V0s))))))))).
tff(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)))))))))))))).
tff(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)))))))))))))).
tff(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)))))).
tff(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))))))).
tff(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))))))).
tff(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))))))))).
tff(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))))))).
tff(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))))))))).
tff(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)))))))))).
tff(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))))))))).
tff(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))))))))))).
tff(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))))))))))).
tff(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)))))))))).
tff(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))))))))))).
tff(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))))))))).
tff(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)))))))))).
tff(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)))))))))))))).
tff(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),f266(A_27a,V1s,V0x))))))))).
tff(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))))))))))))).
tff(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))))))))))))).
tff(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)))))))))).
tff(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)))))))))))))).
tff(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)))))))))))))).
tff(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))))))))).
tff(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))))))))).
tff(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))))))))).
tff(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)))))))))))).
tff(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))))))).
tff(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)))))))))).
tff(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)))))))))).
tff(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))))))))))))).
tff(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)))))))))))).
tff(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)))))))))))).
tff(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)))))))))))))).
tff(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)))))))))))))).
tff(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))))))))))))).
tff(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))))))))))))).
tff(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))))))))))))).
tff(conj_thm_2Epred__set_2EUNIV__BOOL,lemma,((c_2Epred__set_2EUNIV(bool) = ap(ap(c_2Epred__set_2EINSERT(bool),inj__o(fo__c_2Ebool_2ET)),ap(ap(c_2Epred__set_2EINSERT(bool),inj__o(fo__c_2Ebool_2EF)),c_2Epred__set_2EEMPTY(bool)))))).
tff(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)))))))))))))))).
tff(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)))))))))))))))).
tff(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)))))))))).
tff(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))))))))))))).
tff(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))))))))))))).
tff(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))))))))).
tff(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))))))))).
tff(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)))))))))))))).
tff(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))))))).
tff(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))))))))))).
tff(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))))))))).
tff(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))))))))))).
tff(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))))))))).
tff(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))))))))))))).
tff(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)))))))))))).
tff(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)))))))))).
tff(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))))))))))).
tff(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))))))))))))).
tff(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))))))))))))))).
tff(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))))))))))))).
tff(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))))))))).
tff(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))))))))))).
tff(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)))))))))))).
tff(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))))))).
tff(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))))))).
tff(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)))))))))))).
tff(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)))))))))))).
tff(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))))))))).
tff(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))))))).
tff(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))))))).
tff(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)))))))).
tff(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)))))))))).
tff(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))))))))).
tff(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)))).
tff(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)))))))))))).
tff(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))))))))))))).
tff(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))))))))).
tff(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))))))))).
tff(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)))))))).
tff(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))))))))).
tff(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))))))))).
tff(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)))))))).
tff(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))))))))).
tff(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))))))).
tff(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)))))))))))).
tff(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)))))).
tff(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))))))).
tff(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))))))))).
tff(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),f267(A_27b,A_27a,V0f,V1s)))))))))).
tff(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)))))))))))))))).
tff(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)))))))))))))))).
tff(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)))))))))))))).
tff(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)))))))).
tff(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),i(A_27a)),V0s) = V0s)))))).
tff(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)))))).
tff(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)))))).
tff(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)))))))))))))).
tff(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))))))))))))).
tff(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))))))))))).
tff(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))))))))))))).
tff(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))))))))))))).
tff(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)))))))))))))).
tff(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)))))))))))))).
tff(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))))))))))))).
tff(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)))))))))))))).
tff(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))))))))))))))).
tff(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))))))))).
tff(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))))))))))))).
tff(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))))))))))))))))).
tff(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))))))))))))))))).
tff(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)))))))))))))))))).
tff(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))))))))))))))))))).
tff(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),i(A_27a)),V0s),V0s))))))).
tff(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)))))))))))))))))).
tff(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)))))))))))).
tff(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)))))))))))))))))).
tff(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))))))))))))))))))).
tff(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)))))))))))))))))).
tff(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))))))))))))))))).
tff(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)))))))))))))).
tff(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))))))))))))).
tff(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)))))))))))))))))).
tff(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),i(A_27a)),V0s),V0s))))))).
tff(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)))))))))))))))))).
tff(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)))))))))))).
tff(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)))))))))))).
tff(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))))))))))).
tff(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))))))))))))).
tff(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))))))))))))).
tff(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),i(A_27a)),V0s),V0s))))))).
tff(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))))))))))))).
tff(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)))))))))))).
tff(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)))))))))))))))))).
tff(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)))))))))))))))))).
tff(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)))))))))))).
tff(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)))))))))))))))).
tff(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))))))))))))).
tff(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))))))))))))).
tff(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)))))))))))))))).
tff(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))))))))))))))))))).
tff(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) = f269(A_27b,A_27a,V0P,V1Q))))))))).
tff(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) = f271(A_27b,A_27a,V0P,V1Q))))))))).
tff(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)))))))))))))))).
tff(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)))))))))))))))).
tff(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))))))))))))))))).
tff(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))))))))))))))))).
tff(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))))))))))))))).
tff(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))))))).
tff(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))))))))))).
tff(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))))))))).
tff(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))))))))))).
tff(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))))))))))))).
tff(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))))))))))))).
tff(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)))))))))))))).
tff(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)))))))))).
tff(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)))))))))).
tff(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)))))))))))).
tff(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)))))))))))).
tff(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))))))))))))).
tff(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))))))))))))).
tff(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),f272(A_27b,A_27a,V3y,V0f,V1s)))))))))))))))))).
tff(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))))))))))))))))))).
tff(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))))))))))))).
tff(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),f273(A_27b,A_27a,V2y,V0f,V1s)))),c_2Eoption_2ENONE(A_27a)))))))))))).
tff(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))))))))))))))).
tff(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))))))))))).
tff(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)))))))))))))))))))).
tff(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)))))))))))).
tff(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))))))))))))))).
tff(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))))))))))))))).
tff(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))))))))))))).
tff(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)))))))))))))))))))).
tff(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))))))))))))))))).
tff(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)))))))))))).
tff(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))))))))))))))).
tff(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)))))))))))))))))).
tff(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)))))))))).
tff(conj_thm_2Epred__set_2EFINITE__EMPTY,lemma,(( ! [A_27a:del]: p(ap(c_2Epred__set_2EFINITE(A_27a),c_2Epred__set_2EEMPTY(A_27a)))))).
tff(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))))))))))).
tff(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)))))))))).
tff(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)))))))))).
tff(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))))))))).
tff(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)))))))).
tff(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))))))))))).
tff(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))))))))))).
tff(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))))))))))).
tff(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)))))))))).
tff(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))))))))))).
tff(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))))))))))).
tff(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)))))))))).
tff(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))))))))).
tff(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)))))))).
tff(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)))))))))))).
tff(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),f274(A_27b,A_27a,V1x,V0f)))))) => ( ! [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)))))))))))).
tff(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)))))))))))).
tff(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))))))))))))).
tff(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))))))))))))))).
tff(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))))))).
tff(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))))))))))))).
tff(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))))))))))))).
tff(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)))).
tff(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))))))))))))).
tff(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))))))))).
tff(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)))))))))))).
tff(conj_thm_2Epred__set_2ECARD__INTER__LESS__EQ,conjecture,(( ! [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))))))))))).
