include('Axioms/readerMonad^2.ax').
thf(tp_c_2Ebag_2EBAG__ALL__DISTINCT,type,(c_2Ebag_2EBAG__ALL__DISTINCT:(del>$i))).
thf(mem_c_2Ebag_2EBAG__ALL__DISTINCT,axiom,( ! [A_27a:del] : (mem@(c_2Ebag_2EBAG__ALL__DISTINCT@A_27a)@(arr@(arr@A_27a@ty_2Enum_2Enum)@bool)))).
thf(tp_c_2Ebag_2EBAG__CARD,type,(c_2Ebag_2EBAG__CARD:(del>$i))).
thf(mem_c_2Ebag_2EBAG__CARD,axiom,( ! [A_27a:del] : (mem@(c_2Ebag_2EBAG__CARD@A_27a)@(arr@(arr@A_27a@ty_2Enum_2Enum)@ty_2Enum_2Enum)))).
thf(tp_c_2Ebag_2EBAG__CARD__RELn,type,(c_2Ebag_2EBAG__CARD__RELn:(del>$i))).
thf(mem_c_2Ebag_2EBAG__CARD__RELn,axiom,( ! [A_27a:del] : (mem@(c_2Ebag_2EBAG__CARD__RELn@A_27a)@(arr@(arr@A_27a@ty_2Enum_2Enum)@(arr@ty_2Enum_2Enum@bool))))).
thf(tp_c_2Ebag_2EBAG__CHOICE,type,(c_2Ebag_2EBAG__CHOICE:(del>$i))).
thf(mem_c_2Ebag_2EBAG__CHOICE,axiom,( ! [A_27a:del] : (mem@(c_2Ebag_2EBAG__CHOICE@A_27a)@(arr@(arr@A_27a@ty_2Enum_2Enum)@A_27a)))).
thf(tp_c_2Ebag_2EBAG__DELETE,type,(c_2Ebag_2EBAG__DELETE:(del>$i))).
thf(mem_c_2Ebag_2EBAG__DELETE,axiom,( ! [A_27a:del] : (mem@(c_2Ebag_2EBAG__DELETE@A_27a)@(arr@(arr@A_27a@ty_2Enum_2Enum)@(arr@A_27a@(arr@(arr@A_27a@ty_2Enum_2Enum)@bool)))))).
thf(tp_c_2Ebag_2EBAG__DIFF,type,(c_2Ebag_2EBAG__DIFF:(del>$i))).
thf(mem_c_2Ebag_2EBAG__DIFF,axiom,( ! [A_27a:del] : (mem@(c_2Ebag_2EBAG__DIFF@A_27a)@(arr@(arr@A_27a@ty_2Enum_2Enum)@(arr@(arr@A_27a@ty_2Enum_2Enum)@(arr@A_27a@ty_2Enum_2Enum)))))).
thf(tp_c_2Ebag_2EBAG__DISJOINT,type,(c_2Ebag_2EBAG__DISJOINT:(del>$i))).
thf(mem_c_2Ebag_2EBAG__DISJOINT,axiom,( ! [A_27a:del] : (mem@(c_2Ebag_2EBAG__DISJOINT@A_27a)@(arr@(arr@A_27a@ty_2Enum_2Enum)@(arr@(arr@A_27a@ty_2Enum_2Enum)@bool))))).
thf(tp_c_2Ebag_2EBAG__EVERY,type,(c_2Ebag_2EBAG__EVERY:(del>$i))).
thf(mem_c_2Ebag_2EBAG__EVERY,axiom,( ! [A_27a:del] : (mem@(c_2Ebag_2EBAG__EVERY@A_27a)@(arr@(arr@A_27a@bool)@(arr@(arr@A_27a@ty_2Enum_2Enum)@bool))))).
thf(tp_c_2Ebag_2EBAG__FILTER,type,(c_2Ebag_2EBAG__FILTER:(del>$i))).
thf(mem_c_2Ebag_2EBAG__FILTER,axiom,( ! [A_27a:del] : (mem@(c_2Ebag_2EBAG__FILTER@A_27a)@(arr@(arr@A_27a@bool)@(arr@(arr@A_27a@ty_2Enum_2Enum)@(arr@A_27a@ty_2Enum_2Enum)))))).
thf(tp_c_2Ebag_2EBAG__GEN__PROD,type,(c_2Ebag_2EBAG__GEN__PROD:$i)).
thf(mem_c_2Ebag_2EBAG__GEN__PROD,axiom,(mem@c_2Ebag_2EBAG__GEN__PROD@(arr@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)))).
thf(tp_c_2Ebag_2EBAG__GEN__SUM,type,(c_2Ebag_2EBAG__GEN__SUM:$i)).
thf(mem_c_2Ebag_2EBAG__GEN__SUM,axiom,(mem@c_2Ebag_2EBAG__GEN__SUM@(arr@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)))).
thf(tp_c_2Ebag_2EBAG__IMAGE,type,(c_2Ebag_2EBAG__IMAGE:(del>(del>$i)))).
thf(mem_c_2Ebag_2EBAG__IMAGE,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Ebag_2EBAG__IMAGE@A_27a@A_27b)@(arr@(arr@A_27b@A_27a)@(arr@(arr@A_27b@ty_2Enum_2Enum)@(arr@A_27a@ty_2Enum_2Enum))))))).
thf(tp_c_2Ebag_2EBAG__IN,type,(c_2Ebag_2EBAG__IN:(del>$i))).
thf(mem_c_2Ebag_2EBAG__IN,axiom,( ! [A_27a:del] : (mem@(c_2Ebag_2EBAG__IN@A_27a)@(arr@A_27a@(arr@(arr@A_27a@ty_2Enum_2Enum)@bool))))).
thf(tp_c_2Ebag_2EBAG__INN,type,(c_2Ebag_2EBAG__INN:(del>$i))).
thf(mem_c_2Ebag_2EBAG__INN,axiom,( ! [A_27a:del] : (mem@(c_2Ebag_2EBAG__INN@A_27a)@(arr@A_27a@(arr@ty_2Enum_2Enum@(arr@(arr@A_27a@ty_2Enum_2Enum)@bool)))))).
thf(tp_c_2Ebag_2EBAG__INSERT,type,(c_2Ebag_2EBAG__INSERT:(del>$i))).
thf(mem_c_2Ebag_2EBAG__INSERT,axiom,( ! [A_27a:del] : (mem@(c_2Ebag_2EBAG__INSERT@A_27a)@(arr@A_27a@(arr@(arr@A_27a@ty_2Enum_2Enum)@(arr@A_27a@ty_2Enum_2Enum)))))).
thf(tp_c_2Ebag_2EBAG__INTER,type,(c_2Ebag_2EBAG__INTER:(del>$i))).
thf(mem_c_2Ebag_2EBAG__INTER,axiom,( ! [A_27a:del] : (mem@(c_2Ebag_2EBAG__INTER@A_27a)@(arr@(arr@A_27a@ty_2Enum_2Enum)@(arr@(arr@A_27a@ty_2Enum_2Enum)@(arr@A_27a@ty_2Enum_2Enum)))))).
thf(tp_c_2Ebag_2EBAG__MERGE,type,(c_2Ebag_2EBAG__MERGE:(del>$i))).
thf(mem_c_2Ebag_2EBAG__MERGE,axiom,( ! [A_27a:del] : (mem@(c_2Ebag_2EBAG__MERGE@A_27a)@(arr@(arr@A_27a@ty_2Enum_2Enum)@(arr@(arr@A_27a@ty_2Enum_2Enum)@(arr@A_27a@ty_2Enum_2Enum)))))).
thf(tp_c_2Ebag_2EBAG__OF__SET,type,(c_2Ebag_2EBAG__OF__SET:(del>$i))).
thf(mem_c_2Ebag_2EBAG__OF__SET,axiom,( ! [A_27a:del] : (mem@(c_2Ebag_2EBAG__OF__SET@A_27a)@(arr@(arr@A_27a@bool)@(arr@A_27a@ty_2Enum_2Enum))))).
thf(tp_c_2Ebag_2EBAG__REST,type,(c_2Ebag_2EBAG__REST:(del>$i))).
thf(mem_c_2Ebag_2EBAG__REST,axiom,( ! [A_27a:del] : (mem@(c_2Ebag_2EBAG__REST@A_27a)@(arr@(arr@A_27a@ty_2Enum_2Enum)@(arr@A_27a@ty_2Enum_2Enum))))).
thf(tp_c_2Ebag_2EBAG__UNION,type,(c_2Ebag_2EBAG__UNION:(del>$i))).
thf(mem_c_2Ebag_2EBAG__UNION,axiom,( ! [A_27a:del] : (mem@(c_2Ebag_2EBAG__UNION@A_27a)@(arr@(arr@A_27a@ty_2Enum_2Enum)@(arr@(arr@A_27a@ty_2Enum_2Enum)@(arr@A_27a@ty_2Enum_2Enum)))))).
thf(tp_c_2Ebag_2EBIG__BAG__UNION,type,(c_2Ebag_2EBIG__BAG__UNION:(del>$i))).
thf(mem_c_2Ebag_2EBIG__BAG__UNION,axiom,( ! [A_27a:del] : (mem@(c_2Ebag_2EBIG__BAG__UNION@A_27a)@(arr@(arr@(arr@A_27a@ty_2Enum_2Enum)@bool)@(arr@A_27a@ty_2Enum_2Enum))))).
thf(tp_c_2Ebag_2EEL__BAG,type,(c_2Ebag_2EEL__BAG:(del>$i))).
thf(mem_c_2Ebag_2EEL__BAG,axiom,( ! [A_27a:del] : (mem@(c_2Ebag_2EEL__BAG@A_27a)@(arr@A_27a@(arr@A_27a@ty_2Enum_2Enum))))).
thf(tp_c_2Ebag_2EEMPTY__BAG,type,(c_2Ebag_2EEMPTY__BAG:(del>$i))).
thf(mem_c_2Ebag_2EEMPTY__BAG,axiom,( ! [A_27a:del] : (mem@(c_2Ebag_2EEMPTY__BAG@A_27a)@(arr@A_27a@ty_2Enum_2Enum)))).
thf(tp_c_2Ebag_2EFINITE__BAG,type,(c_2Ebag_2EFINITE__BAG:(del>$i))).
thf(mem_c_2Ebag_2EFINITE__BAG,axiom,( ! [A_27a:del] : (mem@(c_2Ebag_2EFINITE__BAG@A_27a)@(arr@(arr@A_27a@ty_2Enum_2Enum)@bool)))).
thf(tp_c_2Ebag_2EITBAG,type,(c_2Ebag_2EITBAG:(del>(del>$i)))).
thf(mem_c_2Ebag_2EITBAG,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Ebag_2EITBAG@A_27a@A_27b)@(arr@(arr@A_27a@(arr@A_27b@A_27b))@(arr@(arr@A_27a@ty_2Enum_2Enum)@(arr@A_27b@A_27b))))))).
thf(tp_c_2Ebag_2EPSUB__BAG,type,(c_2Ebag_2EPSUB__BAG:(del>$i))).
thf(mem_c_2Ebag_2EPSUB__BAG,axiom,( ! [A_27a:del] : (mem@(c_2Ebag_2EPSUB__BAG@A_27a)@(arr@(arr@A_27a@ty_2Enum_2Enum)@(arr@(arr@A_27a@ty_2Enum_2Enum)@bool))))).
thf(tp_c_2Ebag_2ESET__OF__BAG,type,(c_2Ebag_2ESET__OF__BAG:(del>$i))).
thf(mem_c_2Ebag_2ESET__OF__BAG,axiom,( ! [A_27a:del] : (mem@(c_2Ebag_2ESET__OF__BAG@A_27a)@(arr@(arr@A_27a@ty_2Enum_2Enum)@(arr@A_27a@bool))))).
thf(tp_c_2Ebag_2ESING__BAG,type,(c_2Ebag_2ESING__BAG:(del>$i))).
thf(mem_c_2Ebag_2ESING__BAG,axiom,( ! [A_27a:del] : (mem@(c_2Ebag_2ESING__BAG@A_27a)@(arr@(arr@A_27a@ty_2Enum_2Enum)@bool)))).
thf(tp_c_2Ebag_2ESUB__BAG,type,(c_2Ebag_2ESUB__BAG:(del>$i))).
thf(mem_c_2Ebag_2ESUB__BAG,axiom,( ! [A_27a:del] : (mem@(c_2Ebag_2ESUB__BAG@A_27a)@(arr@(arr@A_27a@ty_2Enum_2Enum)@(arr@(arr@A_27a@ty_2Enum_2Enum)@bool))))).
thf(tp_c_2Ebag_2Ebag__size,type,(c_2Ebag_2Ebag__size:(del>$i))).
thf(mem_c_2Ebag_2Ebag__size,axiom,( ! [A_27a:del] : (mem@(c_2Ebag_2Ebag__size@A_27a)@(arr@(arr@A_27a@ty_2Enum_2Enum)@(arr@(arr@A_27a@ty_2Enum_2Enum)@ty_2Enum_2Enum))))).
thf(tp_c_2Ebag_2Edominates,type,(c_2Ebag_2Edominates:(del>(del>$i)))).
thf(mem_c_2Ebag_2Edominates,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Ebag_2Edominates@A_27a@A_27b)@(arr@(arr@A_27a@(arr@A_27b@bool))@(arr@(arr@A_27a@bool)@(arr@(arr@A_27b@bool)@bool))))))).
thf(tp_c_2Ebag_2Emlt1,type,(c_2Ebag_2Emlt1:(del>$i))).
thf(mem_c_2Ebag_2Emlt1,axiom,( ! [A_27a:del] : (mem@(c_2Ebag_2Emlt1@A_27a)@(arr@(arr@A_27a@(arr@A_27a@bool))@(arr@(arr@A_27a@ty_2Enum_2Enum)@(arr@(arr@A_27a@ty_2Enum_2Enum)@bool)))))).
thf(ax_thm_2Ebag_2EEMPTY__BAG,axiom,( ! [A_27a:del]: ((c_2Ebag_2EEMPTY__BAG@A_27a) = (ap@(c_2Ecombin_2EK@ty_2Enum_2Enum@A_27a)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))).
thf(conj_thm_2Ebag_2EEMPTY__BAG__alt,lemma,( ! [A_27a:del]: ((c_2Ebag_2EEMPTY__BAG@A_27a) = (lam@A_27a@(^ [V0x:$i] : (inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))).
thf(ax_thm_2Ebag_2EBAG__INN,axiom,( ! [A_27a:del]: ( ! [V0e:$i] : ((mem@V0e@A_27a) => ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2b:$i] : ((mem@V2b@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(ap@(c_2Ebag_2EBAG__INN@A_27a)@V0e)@(inj__ty_2Enum_2Enum @ V1n))@V2b)) <=> (p@(ap@(ap@c_2Earithmetic_2E_3E_3D@(ap@V2b@V0e))@(inj__ty_2Enum_2Enum @ V1n))))))))))).
thf(ax_thm_2Ebag_2ESUB__BAG,axiom,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V0b1)@V1b2)) <=> ( ! [V2x:$i] : ((mem@V2x@A_27a) => ( ! [V3n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@(ap@(c_2Ebag_2EBAG__INN@A_27a)@V2x)@(inj__ty_2Enum_2Enum @ V3n))@V0b1)) => (p@(ap@(ap@(ap@(c_2Ebag_2EBAG__INN@A_27a)@V2x)@(inj__ty_2Enum_2Enum @ V3n))@V1b2))))))))))))).
thf(ax_thm_2Ebag_2EPSUB__BAG,axiom,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2EPSUB__BAG@A_27a)@V0b1)@V1b2)) <=> ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V0b1)@V1b2)) & (~ (V0b1 = V1b2)))))))))).
thf(ax_thm_2Ebag_2EBAG__IN,axiom,( ! [A_27a:del]: ( ! [V0e:$i] : ((mem@V0e@A_27a) => ( ! [V1b:$i] : ((mem@V1b@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V0e)@V1b)) <=> (p@(ap@(ap@(ap@(c_2Ebag_2EBAG__INN@A_27a)@V0e)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@V1b))))))))).
thf(ax_thm_2Ebag_2EBAG__UNION,axiom,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1c:$i] : ((mem@V1c@(arr@A_27a@ty_2Enum_2Enum)) => ((ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V0b)@V1c) = (lam@A_27a@(^ [V2x:$i] : (ap@(ap@c_2Earithmetic_2E_2B@(ap@V0b@V2x))@(ap@V1c@V2x))))))))))).
thf(ax_thm_2Ebag_2EBAG__DIFF,axiom,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ((ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V0b1)@V1b2) = (lam@A_27a@(^ [V2x:$i] : (ap@(ap@c_2Earithmetic_2E_2D@(ap@V0b1@V2x))@(ap@V1b2@V2x))))))))))).
thf(ax_thm_2Ebag_2EBAG__INSERT,axiom,( ! [A_27a:del]: ( ! [V0e:$i] : ((mem@V0e@A_27a) => ( ! [V1b:$i] : ((mem@V1b@(arr@A_27a@ty_2Enum_2Enum)) => ((ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V0e)@V1b) = (lam@A_27a@(^ [V2x:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@(c_2Emin_2E_3D@A_27a)@V2x)@V0e))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@V1b@V0e))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@V1b@V2x))))))))))).
thf(conj_thm_2Ebag_2EBAG__cases,lemma,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ((V0b = (c_2Ebag_2EEMPTY__BAG@A_27a)) | (? [V1b0:$i] : ((mem@V1b0@(arr@A_27a@ty_2Enum_2Enum)) & (? [V2e:$i] : ((mem@V2e@A_27a) & (V0b = (ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V2e)@V1b0))))))))))).
thf(ax_thm_2Ebag_2EBAG__INTER,axiom,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ((ap@(ap@(c_2Ebag_2EBAG__INTER@A_27a)@V0b1)@V1b2) = (lam@A_27a@(^ [V2x:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@c_2Eprim__rec_2E_3C@(ap@V0b1@V2x))@(ap@V1b2@V2x)))@(ap@V0b1@V2x))@(ap@V1b2@V2x))))))))))).
thf(ax_thm_2Ebag_2EBAG__MERGE,axiom,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ((ap@(ap@(c_2Ebag_2EBAG__MERGE@A_27a)@V0b1)@V1b2) = (lam@A_27a@(^ [V2x:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@c_2Eprim__rec_2E_3C@(ap@V0b1@V2x))@(ap@V1b2@V2x)))@(ap@V1b2@V2x))@(ap@V0b1@V2x))))))))))).
thf(conj_thm_2Ebag_2EBAG__MERGE__IDEM,lemma,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ((ap@(ap@(c_2Ebag_2EBAG__MERGE@A_27a)@V0b)@V0b) = V0b))))).
thf(conj_thm_2Ebag_2EBAG__INN__0,lemma,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1e:$i] : ((mem@V1e@A_27a) => (p@(ap@(ap@(ap@(c_2Ebag_2EBAG__INN@A_27a)@V1e)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@V0b)))))))).
thf(conj_thm_2Ebag_2EBAG__INN__LESS,lemma,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1e:$i] : ((mem@V1e@A_27a) => ( ! [V2n:tp__ty_2Enum_2Enum] : ( ! [V3m:tp__ty_2Enum_2Enum] : (((p@(ap@(ap@(ap@(c_2Ebag_2EBAG__INN@A_27a)@V1e)@(inj__ty_2Enum_2Enum @ V2n))@V0b)) & (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V3m))@(inj__ty_2Enum_2Enum @ V2n)))) => (p@(ap@(ap@(ap@(c_2Ebag_2EBAG__INN@A_27a)@V1e)@(inj__ty_2Enum_2Enum @ V3m))@V0b))))))))))).
thf(conj_thm_2Ebag_2EBAG__IN__BAG__INSERT,lemma,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1e1:$i] : ((mem@V1e1@A_27a) => ( ! [V2e2:$i] : ((mem@V2e2@A_27a) => ((p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V1e1)@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V2e2)@V0b))) <=> ((V1e1 = V2e2) | (p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V1e1)@V0b)))))))))))).
thf(conj_thm_2Ebag_2EBAG__INN__BAG__INSERT,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1b:$i] : ((mem@V1b@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2e1:$i] : ((mem@V2e1@A_27a) => ( ! [V3e2:$i] : ((mem@V3e2@A_27a) => ((p@(ap@(ap@(ap@(c_2Ebag_2EBAG__INN@A_27a)@V2e1)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V3e2)@V1b))) <=> (((p@(ap@(ap@(ap@(c_2Ebag_2EBAG__INN@A_27a)@V2e1)@(ap@(ap@c_2Earithmetic_2E_2D@(inj__ty_2Enum_2Enum @ V0n))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@V1b)) & (V2e1 = V3e2)) | (p@(ap@(ap@(ap@(c_2Ebag_2EBAG__INN@A_27a)@V2e1)@(inj__ty_2Enum_2Enum @ V0n))@V1b))))))))))))).
thf(conj_thm_2Ebag_2EBAG__INN__BAG__INSERT__STRONG,lemma,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2e1:$i] : ((mem@V2e1@A_27a) => ( ! [V3e2:$i] : ((mem@V3e2@A_27a) => ((p@(ap@(ap@(ap@(c_2Ebag_2EBAG__INN@A_27a)@V2e1)@(inj__ty_2Enum_2Enum @ V1n))@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V3e2)@V0b))) <=> (((p@(ap@(ap@(ap@(c_2Ebag_2EBAG__INN@A_27a)@V2e1)@(ap@(ap@c_2Earithmetic_2E_2D@(inj__ty_2Enum_2Enum @ V1n))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@V0b)) & (V2e1 = V3e2)) | ((p@(ap@(ap@(ap@(c_2Ebag_2EBAG__INN@A_27a)@V2e1)@(inj__ty_2Enum_2Enum @ V1n))@V0b)) & (~~ (V2e1 = V3e2)))))))))))))).
thf(conj_thm_2Ebag_2EBAG__UNION__EQ__LCANCEL1,lemma,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1c:$i] : ((mem@V1c@(arr@A_27a@ty_2Enum_2Enum)) => ((V0b = (ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V0b)@V1c)) <=> (V1c = (c_2Ebag_2EEMPTY__BAG@A_27a))))))))).
thf(conj_thm_2Ebag_2EBAG__UNION__EQ__RCANCEL1,lemma,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1c:$i] : ((mem@V1c@(arr@A_27a@ty_2Enum_2Enum)) => ((V0b = (ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V1c)@V0b)) <=> (V1c = (c_2Ebag_2EEMPTY__BAG@A_27a))))))))).
thf(conj_thm_2Ebag_2EBAG__IN__BAG__UNION,lemma,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2e:$i] : ((mem@V2e@A_27a) => ((p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V2e)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V0b1)@V1b2))) <=> ((p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V2e)@V0b1)) | (p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V2e)@V1b2)))))))))))).
thf(conj_thm_2Ebag_2EBAG__INN__BAG__UNION,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1e:$i] : ((mem@V1e@A_27a) => ( ! [V2b1:$i] : ((mem@V2b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V3b2:$i] : ((mem@V3b2@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(ap@(c_2Ebag_2EBAG__INN@A_27a)@V1e)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V2b1)@V3b2))) <=> (? [V4m1:tp__ty_2Enum_2Enum] : (? [V5m2:tp__ty_2Enum_2Enum] : ((V0n = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V4m1))@(inj__ty_2Enum_2Enum @ V5m2)))) & ((p@(ap@(ap@(ap@(c_2Ebag_2EBAG__INN@A_27a)@V1e)@(inj__ty_2Enum_2Enum @ V4m1))@V2b1)) & (p@(ap@(ap@(ap@(c_2Ebag_2EBAG__INN@A_27a)@V1e)@(inj__ty_2Enum_2Enum @ V5m2))@V3b2)))))))))))))))).
thf(conj_thm_2Ebag_2EBAG__INN__BAG__MERGE,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1e:$i] : ((mem@V1e@A_27a) => ( ! [V2b1:$i] : ((mem@V2b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V3b2:$i] : ((mem@V3b2@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(ap@(c_2Ebag_2EBAG__INN@A_27a)@V1e)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(ap@(c_2Ebag_2EBAG__MERGE@A_27a)@V2b1)@V3b2))) <=> ((p@(ap@(ap@(ap@(c_2Ebag_2EBAG__INN@A_27a)@V1e)@(inj__ty_2Enum_2Enum @ V0n))@V2b1)) | (p@(ap@(ap@(ap@(c_2Ebag_2EBAG__INN@A_27a)@V1e)@(inj__ty_2Enum_2Enum @ V0n))@V3b2))))))))))))).
thf(conj_thm_2Ebag_2EBAG__IN__BAG__MERGE,lemma,( ! [A_27a:del]: ( ! [V0e:$i] : ((mem@V0e@A_27a) => ( ! [V1b1:$i] : ((mem@V1b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2b2:$i] : ((mem@V2b2@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V0e)@(ap@(ap@(c_2Ebag_2EBAG__MERGE@A_27a)@V1b1)@V2b2))) <=> ((p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V0e)@V1b1)) | (p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V0e)@V2b2)))))))))))).
thf(conj_thm_2Ebag_2EBAG__EXTENSION,lemma,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ((V0b1 = V1b2) <=> ( ! [V2n:tp__ty_2Enum_2Enum] : ( ! [V3e:$i] : ((mem@V3e@A_27a) => ((p@(ap@(ap@(ap@(c_2Ebag_2EBAG__INN@A_27a)@V3e)@(inj__ty_2Enum_2Enum @ V2n))@V0b1)) <=> (p@(ap@(ap@(ap@(c_2Ebag_2EBAG__INN@A_27a)@V3e)@(inj__ty_2Enum_2Enum @ V2n))@V1b2))))))))))))).
thf(conj_thm_2Ebag_2EBAG__UNION__INSERT,lemma,( ! [A_27a:del]: ( ! [V0e:$i] : ((mem@V0e@A_27a) => ( ! [V1b1:$i] : ((mem@V1b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2b2:$i] : ((mem@V2b2@(arr@A_27a@ty_2Enum_2Enum)) => (((ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V0e)@V1b1))@V2b2) = (ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V0e)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V1b1)@V2b2))) & ((ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V1b1)@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V0e)@V2b2)) = (ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V0e)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V1b1)@V2b2)))))))))))).
thf(conj_thm_2Ebag_2EBAG__INSERT__DIFF,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1b:$i] : ((mem@V1b@(arr@A_27a@ty_2Enum_2Enum)) => (~~ ((ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V0x)@V1b) = V1b)))))))).
thf(conj_thm_2Ebag_2EBAG__INSERT__NOT__EMPTY,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1b:$i] : ((mem@V1b@(arr@A_27a@ty_2Enum_2Enum)) => (~~ ((ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V0x)@V1b) = (c_2Ebag_2EEMPTY__BAG@A_27a))))))))).
thf(conj_thm_2Ebag_2EBAG__INSERT__ONE__ONE,lemma,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => (((ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V2x)@V0b1) = (ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V2x)@V1b2)) <=> (V0b1 = V1b2)))))))))).
thf(conj_thm_2Ebag_2EC__BAG__INSERT__ONE__ONE,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1y:$i] : ((mem@V1y@A_27a) => ( ! [V2b:$i] : ((mem@V2b@(arr@A_27a@ty_2Enum_2Enum)) => (((ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V0x)@V2b) = (ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V1y)@V2b)) <=> (V0x = V1y)))))))))).
thf(conj_thm_2Ebag_2EBAG__INSERT__commutes,lemma,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1e1:$i] : ((mem@V1e1@A_27a) => ( ! [V2e2:$i] : ((mem@V2e2@A_27a) => ((ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V1e1)@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V2e2)@V0b)) = (ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V2e2)@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V1e1)@V0b))))))))))).
thf(conj_thm_2Ebag_2EBAG__DECOMPOSE,lemma,( ! [A_27a:del]: ( ! [V0e:$i] : ((mem@V0e@A_27a) => ( ! [V1b:$i] : ((mem@V1b@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V0e)@V1b)) => (? [V2b_27:$i] : ((mem@V2b_27@(arr@A_27a@ty_2Enum_2Enum)) & (V1b = (ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V0e)@V2b_27))))))))))).
thf(conj_thm_2Ebag_2EBAG__UNION__LEFT__CANCEL,lemma,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b1:$i] : ((mem@V1b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2b2:$i] : ((mem@V2b2@(arr@A_27a@ty_2Enum_2Enum)) => (((ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V0b)@V1b1) = (ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V0b)@V2b2)) <=> (V1b1 = V2b2)))))))))).
thf(conj_thm_2Ebag_2ECOMM__BAG__UNION,lemma,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ((ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V0b1)@V1b2) = (ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V1b2)@V0b1)))))))).
thf(conj_thm_2Ebag_2EBAG__UNION__RIGHT__CANCEL,lemma,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b1:$i] : ((mem@V1b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2b2:$i] : ((mem@V2b2@(arr@A_27a@ty_2Enum_2Enum)) => (((ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V1b1)@V0b) = (ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V2b2)@V0b)) <=> (V1b1 = V2b2)))))))))).
thf(conj_thm_2Ebag_2EASSOC__BAG__UNION,lemma,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2b3:$i] : ((mem@V2b3@(arr@A_27a@ty_2Enum_2Enum)) => ((ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V0b1)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V1b2)@V2b3)) = (ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V0b1)@V1b2))@V2b3)))))))))).
thf(conj_thm_2Ebag_2EBAG__UNION__EMPTY,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: (( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ((ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V0b)@(c_2Ebag_2EEMPTY__BAG@A_27a)) = V0b))) & (( ! [V1b:$i] : ((mem@V1b@(arr@A_27b@ty_2Enum_2Enum)) => ((ap@(ap@(c_2Ebag_2EBAG__UNION@A_27b)@(c_2Ebag_2EEMPTY__BAG@A_27b))@V1b) = V1b))) & ( ! [V2b1:$i] : ((mem@V2b1@(arr@A_27c@ty_2Enum_2Enum)) => ( ! [V3b2:$i] : ((mem@V3b2@(arr@A_27c@ty_2Enum_2Enum)) => (((ap@(ap@(c_2Ebag_2EBAG__UNION@A_27c)@V2b1)@V3b2) = (c_2Ebag_2EEMPTY__BAG@A_27c)) <=> ((V2b1 = (c_2Ebag_2EEMPTY__BAG@A_27c)) & (V3b2 = (c_2Ebag_2EEMPTY__BAG@A_27c)))))))))))))).
thf(ax_thm_2Ebag_2EBAG__DELETE,axiom,( ! [A_27a:del]: ( ! [V0b0:$i] : ((mem@V0b0@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1e:$i] : ((mem@V1e@A_27a) => ( ! [V2b:$i] : ((mem@V2b@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(ap@(c_2Ebag_2EBAG__DELETE@A_27a)@V0b0)@V1e)@V2b)) <=> (V0b0 = (ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V1e)@V2b))))))))))).
thf(conj_thm_2Ebag_2EBAG__DELETE__EMPTY,lemma,( ! [A_27a:del]: ( ! [V0e:$i] : ((mem@V0e@A_27a) => ( ! [V1b:$i] : ((mem@V1b@(arr@A_27a@ty_2Enum_2Enum)) => (~~ (p@(ap@(ap@(ap@(c_2Ebag_2EBAG__DELETE@A_27a)@(c_2Ebag_2EEMPTY__BAG@A_27a))@V0e)@V1b))))))))).
thf(conj_thm_2Ebag_2EBAG__DELETE__commutes,lemma,( ! [A_27a:del]: ( ! [V0b0:$i] : ((mem@V0b0@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b1:$i] : ((mem@V1b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2b2:$i] : ((mem@V2b2@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V3e1:$i] : ((mem@V3e1@A_27a) => ( ! [V4e2:$i] : ((mem@V4e2@A_27a) => (((p@(ap@(ap@(ap@(c_2Ebag_2EBAG__DELETE@A_27a)@V0b0)@V3e1)@V1b1)) & (p@(ap@(ap@(ap@(c_2Ebag_2EBAG__DELETE@A_27a)@V1b1)@V4e2)@V2b2))) => (? [V5b_27:$i] : ((mem@V5b_27@(arr@A_27a@ty_2Enum_2Enum)) & ((p@(ap@(ap@(ap@(c_2Ebag_2EBAG__DELETE@A_27a)@V0b0)@V4e2)@V5b_27)) & (p@(ap@(ap@(ap@(c_2Ebag_2EBAG__DELETE@A_27a)@V5b_27)@V3e1)@V2b2)))))))))))))))))).
thf(conj_thm_2Ebag_2EBAG__DELETE__11,lemma,( ! [A_27a:del]: ( ! [V0b0:$i] : ((mem@V0b0@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1e1:$i] : ((mem@V1e1@A_27a) => ( ! [V2e2:$i] : ((mem@V2e2@A_27a) => ( ! [V3b1:$i] : ((mem@V3b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V4b2:$i] : ((mem@V4b2@(arr@A_27a@ty_2Enum_2Enum)) => (((p@(ap@(ap@(ap@(c_2Ebag_2EBAG__DELETE@A_27a)@V0b0)@V1e1)@V3b1)) & (p@(ap@(ap@(ap@(c_2Ebag_2EBAG__DELETE@A_27a)@V0b0)@V2e2)@V4b2))) => ((V1e1 = V2e2) <=> (V3b1 = V4b2))))))))))))))).
thf(conj_thm_2Ebag_2EBAG__INN__BAG__DELETE,lemma,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2e:$i] : ((mem@V2e@A_27a) => (((p@(ap@(ap@(ap@(c_2Ebag_2EBAG__INN@A_27a)@V2e)@(inj__ty_2Enum_2Enum @ V1n))@V0b)) & (p@(ap@(ap@c_2Earithmetic_2E_3E@(inj__ty_2Enum_2Enum @ V1n))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) => (? [V3b_27:$i] : ((mem@V3b_27@(arr@A_27a@ty_2Enum_2Enum)) & (p@(ap@(ap@(ap@(c_2Ebag_2EBAG__DELETE@A_27a)@V0b)@V2e)@V3b_27)))))))))))).
thf(conj_thm_2Ebag_2EBAG__IN__BAG__DELETE,lemma,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1e:$i] : ((mem@V1e@A_27a) => ((p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V1e)@V0b)) => (? [V2b_27:$i] : ((mem@V2b_27@(arr@A_27a@ty_2Enum_2Enum)) & (p@(ap@(ap@(ap@(c_2Ebag_2EBAG__DELETE@A_27a)@V0b)@V1e)@V2b_27))))))))))).
thf(conj_thm_2Ebag_2EBAG__DELETE__INSERT,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1y:$i] : ((mem@V1y@A_27a) => ( ! [V2b1:$i] : ((mem@V2b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V3b2:$i] : ((mem@V3b2@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(ap@(c_2Ebag_2EBAG__DELETE@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V0x)@V2b1))@V1y)@V3b2)) => (((V0x = V1y) & (V2b1 = V3b2)) | ((? [V4b3:$i] : ((mem@V4b3@(arr@A_27a@ty_2Enum_2Enum)) & (p@(ap@(ap@(ap@(c_2Ebag_2EBAG__DELETE@A_27a)@V2b1)@V1y)@V4b3)))) & (~~ (V0x = V1y))))))))))))))).
thf(conj_thm_2Ebag_2EBAG__DELETE__BAG__IN__up,lemma,( ! [A_27a:del]: ( ! [V0b0:$i] : ((mem@V0b0@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b:$i] : ((mem@V1b@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2e:$i] : ((mem@V2e@A_27a) => ((p@(ap@(ap@(ap@(c_2Ebag_2EBAG__DELETE@A_27a)@V0b0)@V2e)@V1b)) => ( ! [V3e_27:$i] : ((mem@V3e_27@A_27a) => ((p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V3e_27)@V1b)) => (p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V3e_27)@V0b0)))))))))))))).
thf(conj_thm_2Ebag_2EBAG__DELETE__BAG__IN__down,lemma,( ! [A_27a:del]: ( ! [V0b0:$i] : ((mem@V0b0@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b:$i] : ((mem@V1b@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2e1:$i] : ((mem@V2e1@A_27a) => ( ! [V3e2:$i] : ((mem@V3e2@A_27a) => (((p@(ap@(ap@(ap@(c_2Ebag_2EBAG__DELETE@A_27a)@V0b0)@V2e1)@V1b)) & ((~~ (V2e1 = V3e2)) & (p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V3e2)@V0b0)))) => (p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V3e2)@V1b))))))))))))).
thf(conj_thm_2Ebag_2EBAG__DELETE__BAG__IN,lemma,( ! [A_27a:del]: ( ! [V0b0:$i] : ((mem@V0b0@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b:$i] : ((mem@V1b@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2e:$i] : ((mem@V2e@A_27a) => ((p@(ap@(ap@(ap@(c_2Ebag_2EBAG__DELETE@A_27a)@V0b0)@V2e)@V1b)) => (p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V2e)@V0b0))))))))))).
thf(conj_thm_2Ebag_2EBAG__DELETE__concrete,lemma,( ! [A_27a:del]: ( ! [V0b0:$i] : ((mem@V0b0@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b:$i] : ((mem@V1b@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2e:$i] : ((mem@V2e@A_27a) => ((p@(ap@(ap@(ap@(c_2Ebag_2EBAG__DELETE@A_27a)@V0b0)@V2e)@V1b)) <=> ((p@(ap@(ap@c_2Earithmetic_2E_3E@(ap@V0b0@V2e))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) & (V1b = (lam@A_27a@(^ [V3x:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@(c_2Emin_2E_3D@A_27a)@V3x)@V2e))@(ap@(ap@c_2Earithmetic_2E_2D@(ap@V0b0@V2e))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@V0b0@V3x))))))))))))))).
thf(conj_thm_2Ebag_2EBAG__UNION__DIFF__eliminate,lemma,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1c:$i] : ((mem@V1c@(arr@A_27a@ty_2Enum_2Enum)) => (((ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V0b)@V1c))@V1c) = V0b) & ((ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V1c)@V0b))@V1c) = V0b)))))))).
thf(conj_thm_2Ebag_2EBAG__INSERT__EQUAL,lemma,( ! [A_27a:del]: ( ! [V0a:$i] : ((mem@V0a@A_27a) => ( ! [V1M:$i] : ((mem@V1M@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2b:$i] : ((mem@V2b@A_27a) => ( ! [V3N:$i] : ((mem@V3N@(arr@A_27a@ty_2Enum_2Enum)) => (((ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V0a)@V1M) = (ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V2b)@V3N)) <=> (((V1M = V3N) & (V0a = V2b)) | (? [V4k:$i] : ((mem@V4k@(arr@A_27a@ty_2Enum_2Enum)) & ((V1M = (ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V2b)@V4k)) & (V3N = (ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V0a)@V4k))))))))))))))))).
thf(conj_thm_2Ebag_2EBAG__DELETE__TWICE,lemma,( ! [A_27a:del]: ( ! [V0b0:$i] : ((mem@V0b0@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1e1:$i] : ((mem@V1e1@A_27a) => ( ! [V2e2:$i] : ((mem@V2e2@A_27a) => ( ! [V3b1:$i] : ((mem@V3b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V4b2:$i] : ((mem@V4b2@(arr@A_27a@ty_2Enum_2Enum)) => (((p@(ap@(ap@(ap@(c_2Ebag_2EBAG__DELETE@A_27a)@V0b0)@V1e1)@V3b1)) & ((p@(ap@(ap@(ap@(c_2Ebag_2EBAG__DELETE@A_27a)@V0b0)@V2e2)@V4b2)) & (~~ (V3b1 = V4b2)))) => (? [V5b:$i] : ((mem@V5b@(arr@A_27a@ty_2Enum_2Enum)) & ((p@(ap@(ap@(ap@(c_2Ebag_2EBAG__DELETE@A_27a)@V3b1)@V2e2)@V5b)) & (p@(ap@(ap@(ap@(c_2Ebag_2EBAG__DELETE@A_27a)@V4b2)@V1e1)@V5b)))))))))))))))))).
thf(ax_thm_2Ebag_2ESING__BAG,axiom,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(c_2Ebag_2ESING__BAG@A_27a)@V0b)) <=> (? [V1x:$i] : ((mem@V1x@A_27a) & (V0b = (ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V1x)@(c_2Ebag_2EEMPTY__BAG@A_27a)))))))))).
thf(conj_thm_2Ebag_2ESING__BAG__THM,lemma,( ! [A_27a:del]: ( ! [V0e:$i] : ((mem@V0e@A_27a) => (p@(ap@(c_2Ebag_2ESING__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V0e)@(c_2Ebag_2EEMPTY__BAG@A_27a)))))))).
thf(ax_thm_2Ebag_2EEL__BAG,axiom,( ! [A_27a:del]: ( ! [V0e:$i] : ((mem@V0e@A_27a) => ((ap@(c_2Ebag_2EEL__BAG@A_27a)@V0e) = (ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V0e)@(c_2Ebag_2EEMPTY__BAG@A_27a))))))).
thf(conj_thm_2Ebag_2EEL__BAG__11,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1y:$i] : ((mem@V1y@A_27a) => (((ap@(c_2Ebag_2EEL__BAG@A_27a)@V0x) = (ap@(c_2Ebag_2EEL__BAG@A_27a)@V1y)) => (V0x = V1y)))))))).
thf(conj_thm_2Ebag_2EEL__BAG__INSERT__squeeze,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1b:$i] : ((mem@V1b@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2y:$i] : ((mem@V2y@A_27a) => (((ap@(c_2Ebag_2EEL__BAG@A_27a)@V0x) = (ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V2y)@V1b)) => ((V0x = V2y) & (V1b = (c_2Ebag_2EEMPTY__BAG@A_27a)))))))))))).
thf(conj_thm_2Ebag_2ESING__EL__BAG,lemma,( ! [A_27a:del]: ( ! [V0e:$i] : ((mem@V0e@A_27a) => (p@(ap@(c_2Ebag_2ESING__BAG@A_27a)@(ap@(c_2Ebag_2EEL__BAG@A_27a)@V0e))))))).
thf(conj_thm_2Ebag_2EBAG__INSERT__UNION,lemma,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1e:$i] : ((mem@V1e@A_27a) => ((ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V1e)@V0b) = (ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@(ap@(c_2Ebag_2EEL__BAG@A_27a)@V1e))@V0b)))))))).
thf(conj_thm_2Ebag_2EBAG__INSERT__EQ__UNION,lemma,( ! [A_27a:del]: ( ! [V0e:$i] : ((mem@V0e@A_27a) => ( ! [V1b1:$i] : ((mem@V1b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2b2:$i] : ((mem@V2b2@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V3b:$i] : ((mem@V3b@(arr@A_27a@ty_2Enum_2Enum)) => (((ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V0e)@V3b) = (ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V1b1)@V2b2)) => ((p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V0e)@V1b1)) | (p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V0e)@V2b2)))))))))))))).
thf(conj_thm_2Ebag_2EBAG__DELETE__SING,lemma,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1e:$i] : ((mem@V1e@A_27a) => ((p@(ap@(ap@(ap@(c_2Ebag_2EBAG__DELETE@A_27a)@V0b)@V1e)@(c_2Ebag_2EEMPTY__BAG@A_27a))) => (p@(ap@(c_2Ebag_2ESING__BAG@A_27a)@V0b))))))))).
thf(conj_thm_2Ebag_2ENOT__IN__EMPTY__BAG,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => (~~ (p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V0x)@(c_2Ebag_2EEMPTY__BAG@A_27a)))))))).
thf(conj_thm_2Ebag_2EBAG__INN__EMPTY__BAG,lemma,( ! [A_27a:del]: ( ! [V0e:$i] : ((mem@V0e@A_27a) => ( ! [V1n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@(ap@(c_2Ebag_2EBAG__INN@A_27a)@V0e)@(inj__ty_2Enum_2Enum @ V1n))@(c_2Ebag_2EEMPTY__BAG@A_27a))) <=> (V1n = fo__c_2Enum_2E0))))))).
thf(conj_thm_2Ebag_2EMEMBER__NOT__EMPTY,lemma,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ((? [V1x:$i] : ((mem@V1x@A_27a) & (p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V1x)@V0b)))) <=> (~~ (V0b = (c_2Ebag_2EEMPTY__BAG@A_27a)))))))).
thf(conj_thm_2Ebag_2ESUB__BAG__LEQ,lemma,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V0b1)@V1b2)) <=> ( ! [V2x:$i] : ((mem@V2x@A_27a) => (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@V0b1@V2x))@(ap@V1b2@V2x)))))))))))).
thf(conj_thm_2Ebag_2ESUB__BAG__EMPTY,lemma,( ! [A_27a:del]: (( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(c_2Ebag_2EEMPTY__BAG@A_27a))@V0b)))) & ( ! [V1b:$i] : ((mem@V1b@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V1b)@(c_2Ebag_2EEMPTY__BAG@A_27a))) <=> (V1b = (c_2Ebag_2EEMPTY__BAG@A_27a)))))))).
thf(conj_thm_2Ebag_2ESUB__BAG__REFL,lemma,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V0b)@V0b)))))).
thf(conj_thm_2Ebag_2EPSUB__BAG__IRREFL,lemma,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => (~~ (p@(ap@(ap@(c_2Ebag_2EPSUB__BAG@A_27a)@V0b)@V0b))))))).
thf(conj_thm_2Ebag_2ESUB__BAG__ANTISYM,lemma,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => (((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V0b1)@V1b2)) & (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V1b2)@V0b1))) => (V0b1 = V1b2)))))))).
thf(conj_thm_2Ebag_2EPSUB__BAG__ANTISYM,lemma,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => (~~ ((p@(ap@(ap@(c_2Ebag_2EPSUB__BAG@A_27a)@V0b1)@V1b2)) & (p@(ap@(ap@(c_2Ebag_2EPSUB__BAG@A_27a)@V1b2)@V0b1)))))))))).
thf(conj_thm_2Ebag_2ESUB__BAG__TRANS,lemma,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2b3:$i] : ((mem@V2b3@(arr@A_27a@ty_2Enum_2Enum)) => (((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V0b1)@V1b2)) & (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V1b2)@V2b3))) => (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V0b1)@V2b3))))))))))).
thf(conj_thm_2Ebag_2EPSUB__BAG__TRANS,lemma,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2b3:$i] : ((mem@V2b3@(arr@A_27a@ty_2Enum_2Enum)) => (((p@(ap@(ap@(c_2Ebag_2EPSUB__BAG@A_27a)@V0b1)@V1b2)) & (p@(ap@(ap@(c_2Ebag_2EPSUB__BAG@A_27a)@V1b2)@V2b3))) => (p@(ap@(ap@(c_2Ebag_2EPSUB__BAG@A_27a)@V0b1)@V2b3))))))))))).
thf(conj_thm_2Ebag_2EPSUB__BAG__SUB__BAG,lemma,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2EPSUB__BAG@A_27a)@V0b1)@V1b2)) => (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V0b1)@V1b2))))))))).
thf(conj_thm_2Ebag_2EPSUB__BAG__NOT__EQ,lemma,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2EPSUB__BAG@A_27a)@V0b1)@V1b2)) => (~~ (V0b1 = V1b2))))))))).
thf(conj_thm_2Ebag_2EBAG__DIFF__EMPTY,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: (( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ((ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V0b)@V0b) = (c_2Ebag_2EEMPTY__BAG@A_27a)))) & (( ! [V1b:$i] : ((mem@V1b@(arr@A_27b@ty_2Enum_2Enum)) => ((ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27b)@V1b)@(c_2Ebag_2EEMPTY__BAG@A_27b)) = V1b))) & (( ! [V2b:$i] : ((mem@V2b@(arr@A_27c@ty_2Enum_2Enum)) => ((ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27c)@(c_2Ebag_2EEMPTY__BAG@A_27c))@V2b) = (c_2Ebag_2EEMPTY__BAG@A_27c)))) & ( ! [V3b1:$i] : ((mem@V3b1@(arr@A_27d@ty_2Enum_2Enum)) => ( ! [V4b2:$i] : ((mem@V4b2@(arr@A_27d@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27d)@V3b1)@V4b2)) => ((ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27d)@V3b1)@V4b2) = (c_2Ebag_2EEMPTY__BAG@A_27d))))))))))))))).
thf(conj_thm_2Ebag_2EBAG__DIFF__EMPTY__simple,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: (( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ((ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V0b)@V0b) = (c_2Ebag_2EEMPTY__BAG@A_27a)))) & (( ! [V1b:$i] : ((mem@V1b@(arr@A_27b@ty_2Enum_2Enum)) => ((ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27b)@V1b)@(c_2Ebag_2EEMPTY__BAG@A_27b)) = V1b))) & ( ! [V2b:$i] : ((mem@V2b@(arr@A_27c@ty_2Enum_2Enum)) => ((ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27c)@(c_2Ebag_2EEMPTY__BAG@A_27c))@V2b) = (c_2Ebag_2EEMPTY__BAG@A_27c)))))))))).
thf(conj_thm_2Ebag_2EBAG__DIFF__EQ__EMPTY,lemma,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1c:$i] : ((mem@V1c@(arr@A_27a@ty_2Enum_2Enum)) => (((ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V0b)@V1c) = (c_2Ebag_2EEMPTY__BAG@A_27a)) <=> (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V0b)@V1c))))))))).
thf(conj_thm_2Ebag_2EBAG__DIFF__INSERT__same,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1b1:$i] : ((mem@V1b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2b2:$i] : ((mem@V2b2@(arr@A_27a@ty_2Enum_2Enum)) => ((ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V0x)@V1b1))@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V0x)@V2b2)) = (ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V1b1)@V2b2)))))))))).
thf(conj_thm_2Ebag_2EBAG__DIFF__INSERT,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1b1:$i] : ((mem@V1b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2b2:$i] : ((mem@V2b2@(arr@A_27a@ty_2Enum_2Enum)) => ((~~ (p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V0x)@V1b1))) => ((ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V0x)@V2b2))@V1b1) = (ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V0x)@(ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V2b2)@V1b1)))))))))))).
thf(conj_thm_2Ebag_2ENOT__IN__BAG__DIFF,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1b1:$i] : ((mem@V1b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2b2:$i] : ((mem@V2b2@(arr@A_27a@ty_2Enum_2Enum)) => ((~~ (p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V0x)@V1b1))) => ((ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V1b1)@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V0x)@V2b2)) = (ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V1b1)@V2b2))))))))))).
thf(conj_thm_2Ebag_2EBAG__IN__DIFF__I,lemma,( ! [A_27a:del]: ( ! [V0e:$i] : ((mem@V0e@A_27a) => ( ! [V1b1:$i] : ((mem@V1b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2b2:$i] : ((mem@V2b2@(arr@A_27a@ty_2Enum_2Enum)) => (((p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V0e)@V1b1)) & (~~ (p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V0e)@V2b2)))) => (p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V0e)@(ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V1b1)@V2b2)))))))))))).
thf(conj_thm_2Ebag_2EBAG__IN__DIFF__E,lemma,( ! [A_27a:del]: ( ! [V0e:$i] : ((mem@V0e@A_27a) => ( ! [V1b1:$i] : ((mem@V1b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2b2:$i] : ((mem@V2b2@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V0e)@(ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V1b1)@V2b2))) => (p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V0e)@V1b1))))))))))).
thf(conj_thm_2Ebag_2EBAG__UNION__DIFF,lemma,( ! [A_27a:del]: ( ! [V0X:$i] : ((mem@V0X@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1Y:$i] : ((mem@V1Y@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2Z:$i] : ((mem@V2Z@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V2Z)@V1Y)) => (((ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V0X)@(ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V1Y)@V2Z)) = (ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V0X)@V1Y))@V2Z)) & ((ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V1Y)@V2Z))@V0X) = (ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V0X)@V1Y))@V2Z)))))))))))).
thf(conj_thm_2Ebag_2EBAG__DIFF__2L,lemma,( ! [A_27a:del]: ( ! [V0X:$i] : ((mem@V0X@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1Y:$i] : ((mem@V1Y@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2Z:$i] : ((mem@V2Z@(arr@A_27a@ty_2Enum_2Enum)) => ((ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V0X)@V1Y))@V2Z) = (ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V0X)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V1Y)@V2Z))))))))))).
thf(conj_thm_2Ebag_2EBAG__DIFF__2R,lemma,( ! [A_27a:del]: ( ! [V0A:$i] : ((mem@V0A@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1B:$i] : ((mem@V1B@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2C:$i] : ((mem@V2C@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V2C)@V1B)) => ((ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V0A)@(ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V1B)@V2C)) = (ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V0A)@V2C))@V1B))))))))))).
thf(conj_thm_2Ebag_2ESUB__BAG__BAG__DIFF,lemma,( ! [A_27a:del]: ( ! [V0X:$i] : ((mem@V0X@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1Y:$i] : ((mem@V1Y@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2Y_27:$i] : ((mem@V2Y_27@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V3Z:$i] : ((mem@V3Z@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V4W:$i] : ((mem@V4W@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V0X)@V1Y))@(ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V3Z)@V4W))) => (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V0X)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V1Y)@V2Y_27)))@(ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V3Z)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V4W)@V2Y_27))))))))))))))))).
thf(conj_thm_2Ebag_2EBAG__DIFF__UNION__eliminate,lemma,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2b3:$i] : ((mem@V2b3@(arr@A_27a@ty_2Enum_2Enum)) => (((ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V0b1)@V1b2))@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V0b1)@V2b3)) = (ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V1b2)@V2b3)) & (((ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V0b1)@V1b2))@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V2b3)@V0b1)) = (ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V1b2)@V2b3)) & (((ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V1b2)@V0b1))@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V0b1)@V2b3)) = (ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V1b2)@V2b3)) & ((ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V1b2)@V0b1))@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V2b3)@V0b1)) = (ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V1b2)@V2b3))))))))))))).
thf(conj_thm_2Ebag_2ESUB__BAG__UNION__eliminate,lemma,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2b3:$i] : ((mem@V2b3@(arr@A_27a@ty_2Enum_2Enum)) => (((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V0b1)@V1b2))@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V0b1)@V2b3))) <=> (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V1b2)@V2b3))) & (((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V0b1)@V1b2))@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V2b3)@V0b1))) <=> (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V1b2)@V2b3))) & (((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V1b2)@V0b1))@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V0b1)@V2b3))) <=> (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V1b2)@V2b3))) & ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V1b2)@V0b1))@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V2b3)@V0b1))) <=> (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V1b2)@V2b3)))))))))))))).
thf(conj_thm_2Ebag_2Emove__BAG__UNION__over__eq,lemma,( ! [A_27a:del]: ( ! [V0X:$i] : ((mem@V0X@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1Y:$i] : ((mem@V1Y@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2Z:$i] : ((mem@V2Z@(arr@A_27a@ty_2Enum_2Enum)) => (((ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V0X)@V1Y) = V2Z) => (V0X = (ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V2Z)@V1Y))))))))))).
thf(conj_thm_2Ebag_2ESUB__BAG__UNION,lemma,( ! [A_27a:del]: (( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V0b1)@V1b2)) => ( ! [V2b:$i] : ((mem@V2b@(arr@A_27a@ty_2Enum_2Enum)) => (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V0b1)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V1b2)@V2b)))))))))) & (( ! [V3b1:$i] : ((mem@V3b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V4b2:$i] : ((mem@V4b2@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V3b1)@V4b2)) => ( ! [V5b:$i] : ((mem@V5b@(arr@A_27a@ty_2Enum_2Enum)) => (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V3b1)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V5b)@V4b2)))))))))) & (( ! [V6b1:$i] : ((mem@V6b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V7b2:$i] : ((mem@V7b2@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V8b3:$i] : ((mem@V8b3@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V6b1)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V7b2)@V8b3))) => ( ! [V9b:$i] : ((mem@V9b@(arr@A_27a@ty_2Enum_2Enum)) => (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V6b1)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V7b2)@V9b))@V8b3)))))))))))) & (( ! [V10b1:$i] : ((mem@V10b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V11b2:$i] : ((mem@V11b2@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V12b3:$i] : ((mem@V12b3@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V10b1)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V11b2)@V12b3))) => ( ! [V13b:$i] : ((mem@V13b@(arr@A_27a@ty_2Enum_2Enum)) => (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V10b1)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V13b)@V11b2))@V12b3)))))))))))) & (( ! [V14b1:$i] : ((mem@V14b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V15b2:$i] : ((mem@V15b2@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V16b3:$i] : ((mem@V16b3@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V14b1)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V16b3)@V15b2))) => ( ! [V17b:$i] : ((mem@V17b@(arr@A_27a@ty_2Enum_2Enum)) => (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V14b1)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V16b3)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V15b2)@V17b))))))))))))) & (( ! [V18b1:$i] : ((mem@V18b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V19b2:$i] : ((mem@V19b2@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V20b3:$i] : ((mem@V20b3@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V18b1)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V20b3)@V19b2))) => ( ! [V21b:$i] : ((mem@V21b@(arr@A_27a@ty_2Enum_2Enum)) => (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V18b1)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V20b3)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V21b)@V19b2))))))))))))) & (( ! [V22b1:$i] : ((mem@V22b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V23b2:$i] : ((mem@V23b2@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V24b3:$i] : ((mem@V24b3@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V25b4:$i] : ((mem@V25b4@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V22b1)@V24b3)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V23b2)@V25b4)) => (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V22b1)@V23b2))@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V24b3)@V25b4))))))))))))) & (( ! [V26b1:$i] : ((mem@V26b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V27b2:$i] : ((mem@V27b2@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V28b3:$i] : ((mem@V28b3@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V29b4:$i] : ((mem@V29b4@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V26b1)@V29b4)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V27b2)@V28b3)) => (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V26b1)@V27b2))@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V28b3)@V29b4))))))))))))) & (( ! [V30b1:$i] : ((mem@V30b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V31b2:$i] : ((mem@V31b2@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V32b3:$i] : ((mem@V32b3@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V33b4:$i] : ((mem@V33b4@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V34b5:$i] : ((mem@V34b5@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V30b1)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V32b3)@V34b5))) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V31b2)@V33b4)) => (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V30b1)@V31b2))@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V32b3)@V33b4))@V34b5))))))))))))))) & (( ! [V35b1:$i] : ((mem@V35b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V36b2:$i] : ((mem@V36b2@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V37b3:$i] : ((mem@V37b3@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V38b4:$i] : ((mem@V38b4@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V39b5:$i] : ((mem@V39b5@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V35b1)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V38b4)@V39b5))) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V36b2)@V37b3)) => (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V35b1)@V36b2))@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V37b3)@V38b4))@V39b5))))))))))))))) & (( ! [V40b1:$i] : ((mem@V40b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V41b2:$i] : ((mem@V41b2@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V42b3:$i] : ((mem@V42b3@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V43b4:$i] : ((mem@V43b4@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V44b5:$i] : ((mem@V44b5@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V41b2)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V42b3)@V44b5))) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V40b1)@V43b4)) => (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V40b1)@V41b2))@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V42b3)@V43b4))@V44b5))))))))))))))) & (( ! [V45b1:$i] : ((mem@V45b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V46b2:$i] : ((mem@V46b2@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V47b3:$i] : ((mem@V47b3@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V48b4:$i] : ((mem@V48b4@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V49b5:$i] : ((mem@V49b5@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V46b2)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V48b4)@V49b5))) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V45b1)@V47b3)) => (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V45b1)@V46b2))@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V47b3)@V48b4))@V49b5))))))))))))))) & (( ! [V50b1:$i] : ((mem@V50b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V51b2:$i] : ((mem@V51b2@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V52b3:$i] : ((mem@V52b3@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V53b4:$i] : ((mem@V53b4@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V54b5:$i] : ((mem@V54b5@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V50b1)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V54b5)@V52b3))) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V51b2)@V53b4)) => (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V51b2)@V50b1))@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V54b5)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V52b3)@V53b4)))))))))))))))) & (( ! [V55b1:$i] : ((mem@V55b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V56b2:$i] : ((mem@V56b2@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V57b3:$i] : ((mem@V57b3@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V58b4:$i] : ((mem@V58b4@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V59b5:$i] : ((mem@V59b5@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V55b1)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V59b5)@V58b4))) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V56b2)@V57b3)) => (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V56b2)@V55b1))@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V59b5)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V57b3)@V58b4)))))))))))))))) & (( ! [V60b1:$i] : ((mem@V60b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V61b2:$i] : ((mem@V61b2@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V62b3:$i] : ((mem@V62b3@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V63b4:$i] : ((mem@V63b4@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V64b5:$i] : ((mem@V64b5@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V61b2)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V64b5)@V62b3))) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V60b1)@V63b4)) => (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V61b2)@V60b1))@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V64b5)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V62b3)@V63b4)))))))))))))))) & (( ! [V65b1:$i] : ((mem@V65b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V66b2:$i] : ((mem@V66b2@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V67b3:$i] : ((mem@V67b3@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V68b4:$i] : ((mem@V68b4@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V69b5:$i] : ((mem@V69b5@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V66b2)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V69b5)@V68b4))) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V65b1)@V67b3)) => (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V66b2)@V65b1))@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V69b5)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V67b3)@V68b4)))))))))))))))) & (( ! [V70b1:$i] : ((mem@V70b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V71b2:$i] : ((mem@V71b2@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V72b3:$i] : ((mem@V72b3@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V73b4:$i] : ((mem@V73b4@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V74b5:$i] : ((mem@V74b5@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V70b1)@V71b2))@V73b4)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V72b3)@V74b5)) => (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V70b1)@V72b3))@V71b2))@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V73b4)@V74b5))))))))))))))) & (( ! [V75b1:$i] : ((mem@V75b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V76b2:$i] : ((mem@V76b2@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V77b3:$i] : ((mem@V77b3@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V78b4:$i] : ((mem@V78b4@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V79b5:$i] : ((mem@V79b5@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V75b1)@V76b2))@V79b5)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V77b3)@V78b4)) => (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V75b1)@V77b3))@V76b2))@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V78b4)@V79b5))))))))))))))) & (( ! [V80b1:$i] : ((mem@V80b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V81b2:$i] : ((mem@V81b2@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V82b3:$i] : ((mem@V82b3@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V83b4:$i] : ((mem@V83b4@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V84b5:$i] : ((mem@V84b5@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V82b3)@V81b2))@V83b4)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V80b1)@V84b5)) => (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V80b1)@V82b3))@V81b2))@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V83b4)@V84b5))))))))))))))) & (( ! [V85b1:$i] : ((mem@V85b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V86b2:$i] : ((mem@V86b2@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V87b3:$i] : ((mem@V87b3@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V88b4:$i] : ((mem@V88b4@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V89b5:$i] : ((mem@V89b5@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V87b3)@V86b2))@V89b5)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V85b1)@V88b4)) => (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V85b1)@V87b3))@V86b2))@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V88b4)@V89b5))))))))))))))) & (( ! [V90b1:$i] : ((mem@V90b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V91b2:$i] : ((mem@V91b2@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V92b3:$i] : ((mem@V92b3@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V93b4:$i] : ((mem@V93b4@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V94b5:$i] : ((mem@V94b5@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V91b2)@V90b1))@V93b4)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V92b3)@V94b5)) => (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V91b2)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V90b1)@V92b3)))@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V94b5)@V93b4))))))))))))))) & (( ! [V95b1:$i] : ((mem@V95b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V96b2:$i] : ((mem@V96b2@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V97b3:$i] : ((mem@V97b3@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V98b4:$i] : ((mem@V98b4@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V99b5:$i] : ((mem@V99b5@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V96b2)@V95b1))@V99b5)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V97b3)@V98b4)) => (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V96b2)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V95b1)@V97b3)))@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V99b5)@V98b4))))))))))))))) & (( ! [V100b1:$i] : ((mem@V100b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V101b2:$i] : ((mem@V101b2@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V102b3:$i] : ((mem@V102b3@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V103b4:$i] : ((mem@V103b4@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V104b5:$i] : ((mem@V104b5@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V101b2)@V102b3))@V103b4)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V100b1)@V104b5)) => (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V101b2)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V100b1)@V102b3)))@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V104b5)@V103b4))))))))))))))) & ( ! [V105b1:$i] : ((mem@V105b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V106b2:$i] : ((mem@V106b2@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V107b3:$i] : ((mem@V107b3@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V108b4:$i] : ((mem@V108b4@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V109b5:$i] : ((mem@V109b5@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V106b2)@V107b3))@V109b5)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V105b1)@V108b4)) => (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V106b2)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V105b1)@V107b3)))@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V109b5)@V108b4)))))))))))))))))))))))))))))))))))))))).
thf(conj_thm_2Ebag_2ESUB__BAG__EL__BAG,lemma,( ! [A_27a:del]: ( ! [V0e:$i] : ((mem@V0e@A_27a) => ( ! [V1b:$i] : ((mem@V1b@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(c_2Ebag_2EEL__BAG@A_27a)@V0e))@V1b)) <=> (p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V0e)@V1b))))))))).
thf(conj_thm_2Ebag_2ESUB__BAG__INSERT,lemma,( ! [A_27a:del]: ( ! [V0e:$i] : ((mem@V0e@A_27a) => ( ! [V1b1:$i] : ((mem@V1b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2b2:$i] : ((mem@V2b2@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V0e)@V1b1))@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V0e)@V2b2))) <=> (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V1b1)@V2b2))))))))))).
thf(conj_thm_2Ebag_2ESUB__BAG__INSERT__I,lemma,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1c:$i] : ((mem@V1c@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2e:$i] : ((mem@V2e@A_27a) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V0b)@V1c)) => (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V0b)@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V2e)@V1c)))))))))))).
thf(conj_thm_2Ebag_2ENOT__IN__SUB__BAG__INSERT,lemma,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2e:$i] : ((mem@V2e@A_27a) => ((~~ (p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V2e)@V0b1))) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V0b1)@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V2e)@V1b2))) <=> (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V0b1)@V1b2)))))))))))).
thf(conj_thm_2Ebag_2ESUB__BAG__BAG__IN,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1b1:$i] : ((mem@V1b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2b2:$i] : ((mem@V2b2@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V0x)@V1b1))@V2b2)) => (p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V0x)@V2b2))))))))))).
thf(conj_thm_2Ebag_2ESUB__BAG__EXISTS,lemma,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V0b1)@V1b2)) <=> (? [V2b:$i] : ((mem@V2b@(arr@A_27a@ty_2Enum_2Enum)) & (V1b2 = (ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V0b1)@V2b))))))))))).
thf(conj_thm_2Ebag_2ESUB__BAG__UNION__DIFF,lemma,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2b3:$i] : ((mem@V2b3@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V0b1)@V2b3)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V1b2)@(ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V2b3)@V0b1))) <=> (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V0b1)@V1b2))@V2b3)))))))))))).
thf(conj_thm_2Ebag_2ESUB__BAG__UNION__down,lemma,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2b3:$i] : ((mem@V2b3@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V0b1)@V1b2))@V2b3)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V0b1)@V2b3)) & (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V1b2)@V2b3)))))))))))).
thf(conj_thm_2Ebag_2ESUB__BAG__DIFF,lemma,( ! [A_27a:del]: (( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V0b1)@V1b2)) => ( ! [V2b3:$i] : ((mem@V2b3@(arr@A_27a@ty_2Enum_2Enum)) => (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V0b1)@V2b3))@V1b2))))))))) & ( ! [V3b1:$i] : ((mem@V3b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V4b2:$i] : ((mem@V4b2@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V5b3:$i] : ((mem@V5b3@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V6b4:$i] : ((mem@V6b4@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V4b2)@V3b1)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V6b4)@V5b3)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V3b1)@V4b2))@(ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V5b3)@V6b4))) <=> (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V3b1)@V6b4))@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V4b2)@V5b3))))))))))))))))).
thf(conj_thm_2Ebag_2ESUB__BAG__PSUB__BAG,lemma,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V0b1)@V1b2)) <=> ((p@(ap@(ap@(c_2Ebag_2EPSUB__BAG@A_27a)@V0b1)@V1b2)) | (V0b1 = V1b2))))))))).
thf(conj_thm_2Ebag_2EBAG__DELETE__PSUB__BAG,lemma,( ! [A_27a:del]: ( ! [V0b0:$i] : ((mem@V0b0@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1e:$i] : ((mem@V1e@A_27a) => ( ! [V2b:$i] : ((mem@V2b@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(ap@(c_2Ebag_2EBAG__DELETE@A_27a)@V0b0)@V1e)@V2b)) => (p@(ap@(ap@(c_2Ebag_2EPSUB__BAG@A_27a)@V2b)@V0b0))))))))))).
thf(ax_thm_2Ebag_2ESET__OF__BAG,axiom,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ((ap@(c_2Ebag_2ESET__OF__BAG@A_27a)@V0b) = (lam@A_27a@(^ [V1x:$i] : (ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V1x)@V0b)))))))).
thf(ax_thm_2Ebag_2EBAG__OF__SET,axiom,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ((ap@(c_2Ebag_2EBAG__OF__SET@A_27a)@V0P) = (lam@A_27a@(^ [V1x:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1x)@V0P))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))))))).
thf(conj_thm_2Ebag_2ESET__OF__EMPTY,lemma,( ! [A_27a:del]: ((ap@(c_2Ebag_2EBAG__OF__SET@A_27a)@(c_2Epred__set_2EEMPTY@A_27a)) = (c_2Ebag_2EEMPTY__BAG@A_27a)))).
thf(conj_thm_2Ebag_2EBAG__IN__BAG__OF__SET,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1p:$i] : ((mem@V1p@A_27a) => ((p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V1p)@(ap@(c_2Ebag_2EBAG__OF__SET@A_27a)@V0P))) <=> (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1p)@V0P))))))))).
thf(conj_thm_2Ebag_2EBAG__OF__EMPTY,lemma,( ! [A_27a:del]: ((ap@(c_2Ebag_2ESET__OF__BAG@A_27a)@(c_2Ebag_2EEMPTY__BAG@A_27a)) = (c_2Epred__set_2EEMPTY@A_27a)))).
thf(conj_thm_2Ebag_2ESET__BAG__I,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((ap@(c_2Ebag_2ESET__OF__BAG@A_27a)@(ap@(c_2Ebag_2EBAG__OF__SET@A_27a)@V0s)) = V0s))))).
thf(conj_thm_2Ebag_2ESUB__BAG__SET,lemma,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V0b1)@V1b2)) => (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@(ap@(c_2Ebag_2ESET__OF__BAG@A_27a)@V0b1))@(ap@(c_2Ebag_2ESET__OF__BAG@A_27a)@V1b2)))))))))).
thf(conj_thm_2Ebag_2ESET__OF__BAG__UNION,lemma,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ((ap@(c_2Ebag_2ESET__OF__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V0b1)@V1b2)) = (ap@(ap@(c_2Epred__set_2EUNION@A_27a)@(ap@(c_2Ebag_2ESET__OF__BAG@A_27a)@V0b1))@(ap@(c_2Ebag_2ESET__OF__BAG@A_27a)@V1b2))))))))).
thf(conj_thm_2Ebag_2ESET__OF__BAG__MERGE,lemma,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ((ap@(c_2Ebag_2ESET__OF__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__MERGE@A_27a)@V0b1)@V1b2)) = (ap@(ap@(c_2Epred__set_2EUNION@A_27a)@(ap@(c_2Ebag_2ESET__OF__BAG@A_27a)@V0b1))@(ap@(c_2Ebag_2ESET__OF__BAG@A_27a)@V1b2))))))))).
thf(conj_thm_2Ebag_2ESET__OF__BAG__INSERT,lemma,( ! [A_27a:del]: ( ! [V0e:$i] : ((mem@V0e@A_27a) => ( ! [V1b:$i] : ((mem@V1b@(arr@A_27a@ty_2Enum_2Enum)) => ((ap@(c_2Ebag_2ESET__OF__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V0e)@V1b)) = (ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0e)@(ap@(c_2Ebag_2ESET__OF__BAG@A_27a)@V1b))))))))).
thf(conj_thm_2Ebag_2ESET__OF__EL__BAG,lemma,( ! [A_27a:del]: ( ! [V0e:$i] : ((mem@V0e@A_27a) => ((ap@(c_2Ebag_2ESET__OF__BAG@A_27a)@(ap@(c_2Ebag_2EEL__BAG@A_27a)@V0e)) = (ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0e)@(c_2Epred__set_2EEMPTY@A_27a))))))).
thf(conj_thm_2Ebag_2ESET__OF__BAG__DIFF__SUBSET__down,lemma,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@(ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@(ap@(c_2Ebag_2ESET__OF__BAG@A_27a)@V0b1))@(ap@(c_2Ebag_2ESET__OF__BAG@A_27a)@V1b2)))@(ap@(c_2Ebag_2ESET__OF__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V0b1)@V1b2)))))))))).
thf(conj_thm_2Ebag_2ESET__OF__BAG__DIFF__SUBSET__up,lemma,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@(ap@(c_2Ebag_2ESET__OF__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V0b1)@V1b2)))@(ap@(c_2Ebag_2ESET__OF__BAG@A_27a)@V0b1))))))))).
thf(conj_thm_2Ebag_2EIN__SET__OF__BAG,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1b:$i] : ((mem@V1b@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@(ap@(c_2Ebag_2ESET__OF__BAG@A_27a)@V1b))) <=> (p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V0x)@V1b))))))))).
thf(conj_thm_2Ebag_2ESET__OF__BAG__EQ__EMPTY,lemma,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ((((c_2Epred__set_2EEMPTY@A_27a) = (ap@(c_2Ebag_2ESET__OF__BAG@A_27a)@V0b)) <=> (V0b = (c_2Ebag_2EEMPTY__BAG@A_27a))) & (((ap@(c_2Ebag_2ESET__OF__BAG@A_27a)@V0b) = (c_2Epred__set_2EEMPTY@A_27a)) <=> (V0b = (c_2Ebag_2EEMPTY__BAG@A_27a)))))))).
thf(ax_thm_2Ebag_2EBAG__DISJOINT,axiom,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2EBAG__DISJOINT@A_27a)@V0b1)@V1b2)) <=> (p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@(ap@(c_2Ebag_2ESET__OF__BAG@A_27a)@V0b1))@(ap@(c_2Ebag_2ESET__OF__BAG@A_27a)@V1b2)))))))))).
thf(conj_thm_2Ebag_2EBAG__DISJOINT__EMPTY,lemma,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2EBAG__DISJOINT@A_27a)@V0b)@(c_2Ebag_2EEMPTY__BAG@A_27a))) & (p@(ap@(ap@(c_2Ebag_2EBAG__DISJOINT@A_27a)@(c_2Ebag_2EEMPTY__BAG@A_27a))@V0b))))))).
thf(conj_thm_2Ebag_2EBAG__DISJOINT__DIFF,lemma,( ! [A_27a:del]: ( ! [V0B1:$i] : ((mem@V0B1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1B2:$i] : ((mem@V1B2@(arr@A_27a@ty_2Enum_2Enum)) => (p@(ap@(ap@(c_2Ebag_2EBAG__DISJOINT@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V0B1)@V1B2))@(ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V1B2)@V0B1))))))))).
thf(conj_thm_2Ebag_2EBAG__DISJOINT__BAG__IN,lemma,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2EBAG__DISJOINT@A_27a)@V0b1)@V1b2)) <=> ( ! [V2e:$i] : ((mem@V2e@A_27a) => ((~~ (p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V2e)@V0b1))) | (~~ (p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V2e)@V1b2))))))))))))).
thf(conj_thm_2Ebag_2EBAG__DISJOINT__BAG__INSERT,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2e1:$i] : ((mem@V2e1@A_27a) => ((p@(ap@(ap@(c_2Ebag_2EBAG__DISJOINT@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V2e1)@V0b1))@V1b2)) <=> ((~~ (p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V2e1)@V1b2))) & (p@(ap@(ap@(c_2Ebag_2EBAG__DISJOINT@A_27a)@V0b1)@V1b2)))))))))) & ( ! [V3b1:$i] : ((mem@V3b1@(arr@A_27b@ty_2Enum_2Enum)) => ( ! [V4b2:$i] : ((mem@V4b2@(arr@A_27b@ty_2Enum_2Enum)) => ( ! [V5e2:$i] : ((mem@V5e2@A_27b) => ((p@(ap@(ap@(c_2Ebag_2EBAG__DISJOINT@A_27b)@V3b1)@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27b)@V5e2)@V4b2))) <=> ((~~ (p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27b)@V5e2)@V3b1))) & (p@(ap@(ap@(c_2Ebag_2EBAG__DISJOINT@A_27b)@V3b1)@V4b2)))))))))))))).
thf(conj_thm_2Ebag_2EBAG__DISJOINT__BAG__UNION,lemma,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2b3:$i] : ((mem@V2b3@(arr@A_27a@ty_2Enum_2Enum)) => (((p@(ap@(ap@(c_2Ebag_2EBAG__DISJOINT@A_27a)@V0b1)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V1b2)@V2b3))) <=> ((p@(ap@(ap@(c_2Ebag_2EBAG__DISJOINT@A_27a)@V0b1)@V1b2)) & (p@(ap@(ap@(c_2Ebag_2EBAG__DISJOINT@A_27a)@V0b1)@V2b3)))) & ((p@(ap@(ap@(c_2Ebag_2EBAG__DISJOINT@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V0b1)@V1b2))@V2b3)) <=> ((p@(ap@(ap@(c_2Ebag_2EBAG__DISJOINT@A_27a)@V0b1)@V2b3)) & (p@(ap@(ap@(c_2Ebag_2EBAG__DISJOINT@A_27a)@V1b2)@V2b3))))))))))))).
thf(ax_thm_2Ebag_2EFINITE__BAG,axiom,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V0b)) <=> ( ! [V1P:$i] : ((mem@V1P@(arr@(arr@A_27a@ty_2Enum_2Enum)@bool)) => (((p@(ap@V1P@(c_2Ebag_2EEMPTY__BAG@A_27a))) & ( ! [V2b:$i] : ((mem@V2b@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@V1P@V2b)) => ( ! [V3e:$i] : ((mem@V3e@A_27a) => (p@(ap@V1P@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V3e)@V2b))))))))) => (p@(ap@V1P@V0b)))))))))).
thf(conj_thm_2Ebag_2EFINITE__EMPTY__BAG,lemma,( ! [A_27a:del]: (p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@(c_2Ebag_2EEMPTY__BAG@A_27a))))).
thf(conj_thm_2Ebag_2EFINITE__BAG__INSERT,lemma,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V0b)) => ( ! [V1e:$i] : ((mem@V1e@A_27a) => (p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V1e)@V0b)))))))))).
thf(conj_thm_2Ebag_2EFINITE__BAG__INDUCT,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@(arr@A_27a@ty_2Enum_2Enum)@bool)) => (((p@(ap@V0P@(c_2Ebag_2EEMPTY__BAG@A_27a))) & ( ! [V1b:$i] : ((mem@V1b@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@V0P@V1b)) => ( ! [V2e:$i] : ((mem@V2e@A_27a) => (p@(ap@V0P@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V2e)@V1b))))))))) => ( ! [V3b:$i] : ((mem@V3b@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V3b)) => (p@(ap@V0P@V3b)))))))))).
thf(conj_thm_2Ebag_2ESTRONG__FINITE__BAG__INDUCT,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@(arr@A_27a@ty_2Enum_2Enum)@bool)) => (((p@(ap@V0P@(c_2Ebag_2EEMPTY__BAG@A_27a))) & ( ! [V1b:$i] : ((mem@V1b@(arr@A_27a@ty_2Enum_2Enum)) => (((p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V1b)) & (p@(ap@V0P@V1b))) => ( ! [V2e:$i] : ((mem@V2e@A_27a) => (p@(ap@V0P@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V2e)@V1b))))))))) => ( ! [V3b:$i] : ((mem@V3b@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V3b)) => (p@(ap@V0P@V3b)))))))))).
thf(conj_thm_2Ebag_2EFINITE__BAG__THM,lemma,( ! [A_27a:del]: ((p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@(c_2Ebag_2EEMPTY__BAG@A_27a))) & ( ! [V0e:$i] : ((mem@V0e@A_27a) => ( ! [V1b:$i] : ((mem@V1b@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V0e)@V1b))) <=> (p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V1b)))))))))).
thf(conj_thm_2Ebag_2EFINITE__BAG__DIFF,lemma,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V0b1)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => (p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V0b1)@V1b2)))))))))).
thf(conj_thm_2Ebag_2EFINITE__BAG__DIFF__dual,lemma,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V0b1)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V1b2)@V0b1))) => (p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V1b2)))))))))).
thf(conj_thm_2Ebag_2EFINITE__BAG__UNION,lemma,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V0b1)@V1b2))) <=> ((p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V0b1)) & (p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V1b2)))))))))).
thf(conj_thm_2Ebag_2EFINITE__SUB__BAG,lemma,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V0b1)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V1b2)@V0b1)) => (p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V1b2)))))))))).
thf(ax_thm_2Ebag_2EBAG__CARD__RELn,axiom,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@(c_2Ebag_2EBAG__CARD__RELn@A_27a)@V0b)@(inj__ty_2Enum_2Enum @ V1n))) <=> ( ! [V2P:$i] : ((mem@V2P@(arr@(arr@A_27a@ty_2Enum_2Enum)@(arr@ty_2Enum_2Enum@bool))) => (((p@(ap@(ap@V2P@(c_2Ebag_2EEMPTY__BAG@A_27a))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) & ( ! [V3b:$i] : ((mem@V3b@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V4n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@V2P@V3b)@(inj__ty_2Enum_2Enum @ V4n))) => ( ! [V5e:$i] : ((mem@V5e@A_27a) => (p@(ap@(ap@V2P@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V5e)@V3b))@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V4n))))))))))) => (p@(ap@(ap@V2P@V0b)@(inj__ty_2Enum_2Enum @ V1n)))))))))))).
thf(ax_thm_2Ebag_2EBAG__CARD,axiom,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V0b)) => (p@(ap@(ap@(c_2Ebag_2EBAG__CARD__RELn@A_27a)@V0b)@(ap@(c_2Ebag_2EBAG__CARD@A_27a)@V0b)))))))).
thf(conj_thm_2Ebag_2EBAG__CARD__EMPTY,lemma,( ! [A_27a:del]: ((surj__ty_2Enum_2Enum @ (ap@(c_2Ebag_2EBAG__CARD@A_27a)@(c_2Ebag_2EEMPTY__BAG@A_27a))) = fo__c_2Enum_2E0))).
thf(conj_thm_2Ebag_2EBCARD__0,lemma,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V0b)) => (((surj__ty_2Enum_2Enum @ (ap@(c_2Ebag_2EBAG__CARD@A_27a)@V0b)) = fo__c_2Enum_2E0) <=> (V0b = (c_2Ebag_2EEMPTY__BAG@A_27a)))))))).
thf(conj_thm_2Ebag_2EBAG__CARD__THM,lemma,( ! [A_27a:del]: (((surj__ty_2Enum_2Enum @ (ap@(c_2Ebag_2EBAG__CARD@A_27a)@(c_2Ebag_2EEMPTY__BAG@A_27a))) = fo__c_2Enum_2E0) & ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V0b)) => ( ! [V1e:$i] : ((mem@V1e@A_27a) => ((surj__ty_2Enum_2Enum @ (ap@(c_2Ebag_2EBAG__CARD@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V1e)@V0b))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(ap@(c_2Ebag_2EBAG__CARD@A_27a)@V0b))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))))).
thf(conj_thm_2Ebag_2EBAG__CARD__UNION,lemma,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => (((p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V0b1)) & (p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V1b2))) => ((surj__ty_2Enum_2Enum @ (ap@(c_2Ebag_2EBAG__CARD@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V0b1)@V1b2))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(ap@(c_2Ebag_2EBAG__CARD@A_27a)@V0b1))@(ap@(c_2Ebag_2EBAG__CARD@A_27a)@V1b2))))))))))).
thf(conj_thm_2Ebag_2EBCARD__SUC,lemma,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V0b)) => ( ! [V1n:tp__ty_2Enum_2Enum] : (((surj__ty_2Enum_2Enum @ (ap@(c_2Ebag_2EBAG__CARD@A_27a)@V0b)) = (surj__ty_2Enum_2Enum @ (ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n)))) <=> (? [V2b0:$i] : ((mem@V2b0@(arr@A_27a@ty_2Enum_2Enum)) & (? [V3e:$i] : ((mem@V3e@A_27a) & ((V0b = (ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V3e)@V2b0)) & ((surj__ty_2Enum_2Enum @ (ap@(c_2Ebag_2EBAG__CARD@A_27a)@V2b0)) = V1n))))))))))))).
thf(conj_thm_2Ebag_2EBAG__CARD__BAG__INN,lemma,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V0b)) => ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2e:$i] : ((mem@V2e@A_27a) => ((p@(ap@(ap@(ap@(c_2Ebag_2EBAG__INN@A_27a)@V2e)@(inj__ty_2Enum_2Enum @ V1n))@V0b)) => (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V1n))@(ap@(c_2Ebag_2EBAG__CARD@A_27a)@V0b)))))))))))).
thf(conj_thm_2Ebag_2ESUB__BAG__DIFF__EQ,lemma,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V0b1)@V1b2)) => (V1b2 = (ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V0b1)@(ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V1b2)@V0b1)))))))))).
thf(conj_thm_2Ebag_2ESUB__BAG__CARD,lemma,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => (((p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V1b2)) & (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V0b1)@V1b2))) => (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(c_2Ebag_2EBAG__CARD@A_27a)@V0b1))@(ap@(c_2Ebag_2EBAG__CARD@A_27a)@V1b2)))))))))).
thf(conj_thm_2Ebag_2EBAG__CARD__DIFF,lemma,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V0b)) => ( ! [V1c:$i] : ((mem@V1c@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V1c)@V0b)) => ((surj__ty_2Enum_2Enum @ (ap@(c_2Ebag_2EBAG__CARD@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V0b)@V1c))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2D@(ap@(c_2Ebag_2EBAG__CARD@A_27a)@V0b))@(ap@(c_2Ebag_2EBAG__CARD@A_27a)@V1c)))))))))))).
thf(ax_thm_2Ebag_2EBAG__FILTER__DEF,axiom,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@A_27a@ty_2Enum_2Enum)) => ((ap@(ap@(c_2Ebag_2EBAG__FILTER@A_27a)@V0P)@V1b) = (lam@A_27a@(^ [V2e:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@V0P@V2e))@(ap@V1b@V2e))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))))))))).
thf(conj_thm_2Ebag_2EBAG__FILTER__EMPTY,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ((ap@(ap@(c_2Ebag_2EBAG__FILTER@A_27a)@V0P)@(c_2Ebag_2EEMPTY__BAG@A_27a)) = (c_2Ebag_2EEMPTY__BAG@A_27a)))))).
thf(conj_thm_2Ebag_2EBAG__FILTER__BAG__INSERT,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1e:$i] : ((mem@V1e@A_27a) => ( ! [V2b:$i] : ((mem@V2b@(arr@A_27a@ty_2Enum_2Enum)) => ((ap@(ap@(c_2Ebag_2EBAG__FILTER@A_27a)@V0P)@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V1e)@V2b)) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(arr@A_27a@ty_2Enum_2Enum))@(ap@V0P@V1e))@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V1e)@(ap@(ap@(c_2Ebag_2EBAG__FILTER@A_27a)@V0P)@V2b)))@(ap@(ap@(c_2Ebag_2EBAG__FILTER@A_27a)@V0P)@V2b))))))))))).
thf(conj_thm_2Ebag_2EFINITE__BAG__FILTER,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V1b)) => (p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__FILTER@A_27a)@V0P)@V1b)))))))))).
thf(conj_thm_2Ebag_2EBAG__INN__BAG__FILTER,lemma,( ! [A_27a:del]: ( ! [V0e:$i] : ((mem@V0e@A_27a) => ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2P:$i] : ((mem@V2P@(arr@A_27a@bool)) => ( ! [V3b:$i] : ((mem@V3b@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(ap@(c_2Ebag_2EBAG__INN@A_27a)@V0e)@(inj__ty_2Enum_2Enum @ V1n))@(ap@(ap@(c_2Ebag_2EBAG__FILTER@A_27a)@V2P)@V3b))) <=> ((V1n = fo__c_2Enum_2E0) | ((p@(ap@V2P@V0e)) & (p@(ap@(ap@(ap@(c_2Ebag_2EBAG__INN@A_27a)@V0e)@(inj__ty_2Enum_2Enum @ V1n))@V3b)))))))))))))).
thf(conj_thm_2Ebag_2EBAG__IN__BAG__FILTER,lemma,( ! [A_27a:del]: ( ! [V0e:$i] : ((mem@V0e@A_27a) => ( ! [V1P:$i] : ((mem@V1P@(arr@A_27a@bool)) => ( ! [V2b:$i] : ((mem@V2b@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V0e)@(ap@(ap@(c_2Ebag_2EBAG__FILTER@A_27a)@V1P)@V2b))) <=> ((p@(ap@V1P@V0e)) & (p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V0e)@V2b)))))))))))).
thf(conj_thm_2Ebag_2EBAG__FILTER__FILTER,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1Q:$i] : ((mem@V1Q@(arr@A_27a@bool)) => ( ! [V2b:$i] : ((mem@V2b@(arr@A_27a@ty_2Enum_2Enum)) => ((ap@(ap@(c_2Ebag_2EBAG__FILTER@A_27a)@V0P)@(ap@(ap@(c_2Ebag_2EBAG__FILTER@A_27a)@V1Q)@V2b)) = (ap@(ap@(c_2Ebag_2EBAG__FILTER@A_27a)@(lam@A_27a@(^ [V3a:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0P@V3a))@(ap@V1Q@V3a)))))@V2b)))))))))).
thf(conj_thm_2Ebag_2EBAG__FILTER__SUB__BAG,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@A_27a@ty_2Enum_2Enum)) => (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__FILTER@A_27a)@V0P)@V1b))@V1b)))))))).
thf(conj_thm_2Ebag_2ESET__OF__BAG__EQ__INSERT,lemma,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1e:$i] : ((mem@V1e@A_27a) => ( ! [V2s:$i] : ((mem@V2s@(arr@A_27a@bool)) => (((ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V1e)@V2s) = (ap@(c_2Ebag_2ESET__OF__BAG@A_27a)@V0b)) <=> (? [V3b0:$i] : ((mem@V3b0@(arr@A_27a@ty_2Enum_2Enum)) & (? [V4eb:$i] : ((mem@V4eb@(arr@A_27a@ty_2Enum_2Enum)) & ((V0b = (ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V4eb)@V3b0)) & ((V2s = (ap@(c_2Ebag_2ESET__OF__BAG@A_27a)@V3b0)) & (( ! [V5e_27:$i] : ((mem@V5e_27@A_27a) => ((p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V5e_27)@V4eb)) => (V5e_27 = V1e)))) & ((~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1e)@V2s))) => (p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V1e)@V4eb))))))))))))))))))).
thf(conj_thm_2Ebag_2EFINITE__SET__OF__BAG,lemma,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@(ap@(c_2Ebag_2ESET__OF__BAG@A_27a)@V0b))) <=> (p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V0b))))))).
thf(ax_thm_2Ebag_2EBAG__IMAGE__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27b@A_27a)) => ( ! [V1b:$i] : ((mem@V1b@(arr@A_27b@ty_2Enum_2Enum)) => ((ap@(ap@(c_2Ebag_2EBAG__IMAGE@A_27a@A_27b)@V0f)@V1b) = (lam@A_27a@(^ [V2e:$i] : (ap@(ap@(c_2Ebool_2ELET@(arr@A_27b@ty_2Enum_2Enum)@ty_2Enum_2Enum)@(lam@(arr@A_27b@ty_2Enum_2Enum)@(^ [V3sb:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(c_2Ebag_2EFINITE__BAG@A_27b)@V3sb))@(ap@(c_2Ebag_2EBAG__CARD@A_27b)@V3sb))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))@(ap@(ap@(c_2Ebag_2EBAG__FILTER@A_27b)@(lam@A_27b@(^ [V4e0:$i] : (ap@(ap@(c_2Emin_2E_3D@A_27a)@(ap@V0f@V4e0))@V2e))))@V1b)))))))))))).
thf(conj_thm_2Ebag_2EBAG__IMAGE__EMPTY,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ((ap@(ap@(c_2Ebag_2EBAG__IMAGE@A_27b@A_27a)@V0f)@(c_2Ebag_2EEMPTY__BAG@A_27a)) = (c_2Ebag_2EEMPTY__BAG@A_27b))))))).
thf(conj_thm_2Ebag_2EBAG__IMAGE__FINITE__INSERT,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27a@A_27b)) => ( ! [V2e:$i] : ((mem@V2e@A_27a) => ((p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V0b)) => ((ap@(ap@(c_2Ebag_2EBAG__IMAGE@A_27b@A_27a)@V1f)@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V2e)@V0b)) = (ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27b)@(ap@V1f@V2e))@(ap@(ap@(c_2Ebag_2EBAG__IMAGE@A_27b@A_27a)@V1f)@V0b))))))))))))).
thf(conj_thm_2Ebag_2EBAG__IMAGE__FINITE__UNION,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27b)) => (((p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V0b1)) & (p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V1b2))) => ((ap@(ap@(c_2Ebag_2EBAG__IMAGE@A_27b@A_27a)@V2f)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V0b1)@V1b2)) = (ap@(ap@(c_2Ebag_2EBAG__UNION@A_27b)@(ap@(ap@(c_2Ebag_2EBAG__IMAGE@A_27b@A_27a)@V2f)@V0b1))@(ap@(ap@(c_2Ebag_2EBAG__IMAGE@A_27b@A_27a)@V2f)@V1b2))))))))))))).
thf(conj_thm_2Ebag_2EBAG__IMAGE__FINITE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1b:$i] : ((mem@V1b@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V1b)) => (p@(ap@(c_2Ebag_2EFINITE__BAG@A_27b)@(ap@(ap@(c_2Ebag_2EBAG__IMAGE@A_27b@A_27a)@V0f)@V1b))))))))))).
thf(conj_thm_2Ebag_2EBAG__IMAGE__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_27c@A_27a)) => ( ! [V2b:$i] : ((mem@V2b@(arr@A_27c@ty_2Enum_2Enum)) => ((p@(ap@(c_2Ebag_2EFINITE__BAG@A_27c)@V2b)) => ((ap@(ap@(c_2Ebag_2EBAG__IMAGE@A_27b@A_27c)@(ap@(ap@(c_2Ecombin_2Eo@A_27c@A_27b@A_27a)@V0f)@V1g))@V2b) = (ap@(ap@(c_2Ebag_2EBAG__IMAGE@A_27b@A_27a)@V0f)@(ap@(ap@(c_2Ebag_2EBAG__IMAGE@A_27a@A_27c)@V1g)@V2b)))))))))))))).
thf(conj_thm_2Ebag_2EBAG__IMAGE__FINITE__I,lemma,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V0b)) => ((ap@(ap@(c_2Ebag_2EBAG__IMAGE@A_27a@A_27a)@(c_2Ecombin_2EI@A_27a))@V0b) = V0b)))))).
thf(conj_thm_2Ebag_2EBAG__IN__FINITE__BAG__IMAGE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1x:$i] : ((mem@V1x@A_27b) => ( ! [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27b)) => ((p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V0b)) => ((p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27b)@V1x)@(ap@(ap@(c_2Ebag_2EBAG__IMAGE@A_27b@A_27a)@V2f)@V0b))) <=> (? [V3y:$i] : ((mem@V3y@A_27a) & (((ap@V2f@V3y) = V1x) & (p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V3y)@V0b)))))))))))))))).
thf(conj_thm_2Ebag_2EBAG__IMAGE__EQ__EMPTY,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27a@A_27b)) => ((p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V0b)) => (((ap@(ap@(c_2Ebag_2EBAG__IMAGE@A_27b@A_27a)@V1f)@V0b) = (c_2Ebag_2EEMPTY__BAG@A_27b)) <=> (V0b = (c_2Ebag_2EEMPTY__BAG@A_27a))))))))))).
thf(ax_thm_2Ebag_2EBAG__CHOICE__DEF,axiom,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ((~ (V0b = (c_2Ebag_2EEMPTY__BAG@A_27a))) => (p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@(ap@(c_2Ebag_2EBAG__CHOICE@A_27a)@V0b))@V0b))))))).
thf(ax_thm_2Ebag_2EBAG__REST__DEF,axiom,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ((ap@(c_2Ebag_2EBAG__REST@A_27a)@V0b) = (ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V0b)@(ap@(c_2Ebag_2EEL__BAG@A_27a)@(ap@(c_2Ebag_2EBAG__CHOICE@A_27a)@V0b)))))))).
thf(conj_thm_2Ebag_2EBAG__INSERT__CHOICE__REST,lemma,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ((~~ (V0b = (c_2Ebag_2EEMPTY__BAG@A_27a))) => (V0b = (ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@(ap@(c_2Ebag_2EBAG__CHOICE@A_27a)@V0b))@(ap@(c_2Ebag_2EBAG__REST@A_27a)@V0b)))))))).
thf(conj_thm_2Ebag_2EBAG__CHOICE__SING,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ((ap@(c_2Ebag_2EBAG__CHOICE@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V0x)@(c_2Ebag_2EEMPTY__BAG@A_27a))) = V0x))))).
thf(conj_thm_2Ebag_2EBAG__REST__SING,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ((ap@(c_2Ebag_2EBAG__REST@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V0x)@(c_2Ebag_2EEMPTY__BAG@A_27a))) = (c_2Ebag_2EEMPTY__BAG@A_27a)))))).
thf(conj_thm_2Ebag_2ESUB__BAG__REST,lemma,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(c_2Ebag_2EBAG__REST@A_27a)@V0b))@V0b)))))).
thf(conj_thm_2Ebag_2EPSUB__BAG__REST,lemma,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ((~~ (V0b = (c_2Ebag_2EEMPTY__BAG@A_27a))) => (p@(ap@(ap@(c_2Ebag_2EPSUB__BAG@A_27a)@(ap@(c_2Ebag_2EBAG__REST@A_27a)@V0b))@V0b))))))).
thf(conj_thm_2Ebag_2ESUB__BAG__UNION__MONO,lemma,( ! [A_27a:del]: (( ! [V0x:$i] : ((mem@V0x@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1y:$i] : ((mem@V1y@(arr@A_27a@ty_2Enum_2Enum)) => (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V0x)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V0x)@V1y))))))) & ( ! [V2x:$i] : ((mem@V2x@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V3y:$i] : ((mem@V3y@(arr@A_27a@ty_2Enum_2Enum)) => (p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V2x)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V3y)@V2x)))))))))).
thf(conj_thm_2Ebag_2EPSUB__BAG__CARD,lemma,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => (((p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V1b2)) & (p@(ap@(ap@(c_2Ebag_2EPSUB__BAG@A_27a)@V0b1)@V1b2))) => (p@(ap@(ap@c_2Eprim__rec_2E_3C@(ap@(c_2Ebag_2EBAG__CARD@A_27a)@V0b1))@(ap@(c_2Ebag_2EBAG__CARD@A_27a)@V1b2)))))))))).
thf(conj_thm_2Ebag_2EEL__BAG__BAG__INSERT,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1y:$i] : ((mem@V1y@A_27a) => ( ! [V2b:$i] : ((mem@V2b@(arr@A_27a@ty_2Enum_2Enum)) => (((ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V0x)@(c_2Ebag_2EEMPTY__BAG@A_27a)) = (ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V1y)@V2b)) <=> ((V0x = V1y) & (V2b = (c_2Ebag_2EEMPTY__BAG@A_27a)))))))))))).
thf(conj_thm_2Ebag_2EEL__BAG__SUB__BAG,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1b:$i] : ((mem@V1b@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V0x)@(c_2Ebag_2EEMPTY__BAG@A_27a)))@V1b)) <=> (p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V0x)@V1b))))))))).
thf(conj_thm_2Ebag_2EITBAG__IND,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(arr@A_27b@A_27b))) => ( ! [V1P:$i] : ((mem@V1P@(arr@(arr@A_27a@ty_2Enum_2Enum)@(arr@A_27b@bool))) => (( ! [V2b:$i] : ((mem@V2b@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V3acc:$i] : ((mem@V3acc@A_27b) => ((((p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V2b)) & (~~ (V2b = (c_2Ebag_2EEMPTY__BAG@A_27a)))) => (p@(ap@(ap@V1P@(ap@(c_2Ebag_2EBAG__REST@A_27a)@V2b))@(ap@(ap@V0f@(ap@(c_2Ebag_2EBAG__CHOICE@A_27a)@V2b))@V3acc)))) => (p@(ap@(ap@V1P@V2b)@V3acc))))))) => ( ! [V4v:$i] : ((mem@V4v@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V5v1:$i] : ((mem@V5v1@A_27b) => (p@(ap@(ap@V1P@V4v)@V5v1)))))))))))))).
thf(conj_thm_2Ebag_2EITBAG__THM,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27a@(arr@A_27b@A_27b))) => ( ! [V2acc:$i] : ((mem@V2acc@A_27b) => ((p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V0b)) => ((ap@(ap@(ap@(c_2Ebag_2EITBAG@A_27a@A_27b)@V1f)@V0b)@V2acc) = (ap@(ap@(ap@(c_2Ebool_2ECOND@A_27b)@(ap@(ap@(c_2Emin_2E_3D@(arr@A_27a@ty_2Enum_2Enum))@V0b)@(c_2Ebag_2EEMPTY__BAG@A_27a)))@V2acc)@(ap@(ap@(ap@(c_2Ebag_2EITBAG@A_27a@A_27b)@V1f)@(ap@(c_2Ebag_2EBAG__REST@A_27a)@V0b))@(ap@(ap@V1f@(ap@(c_2Ebag_2EBAG__CHOICE@A_27a)@V0b))@V2acc)))))))))))))).
thf(conj_thm_2Ebag_2EITBAG__EMPTY,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(arr@A_27b@A_27b))) => ( ! [V1acc:$i] : ((mem@V1acc@A_27b) => ((ap@(ap@(ap@(c_2Ebag_2EITBAG@A_27a@A_27b)@V0f)@(c_2Ebag_2EEMPTY__BAG@A_27a))@V1acc) = V1acc)))))))).
thf(conj_thm_2Ebag_2EITBAG__INSERT,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ( ! [V2f:$i] : ((mem@V2f@(arr@A_27a@(arr@A_27b@A_27b))) => ( ! [V3acc:$i] : ((mem@V3acc@A_27b) => ((p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V0b)) => ((ap@(ap@(ap@(c_2Ebag_2EITBAG@A_27a@A_27b)@V2f)@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V1x)@V0b))@V3acc) = (ap@(ap@(ap@(c_2Ebag_2EITBAG@A_27a@A_27b)@V2f)@(ap@(c_2Ebag_2EBAG__REST@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V1x)@V0b)))@(ap@(ap@V2f@(ap@(c_2Ebag_2EBAG__CHOICE@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V1x)@V0b)))@V3acc))))))))))))))).
thf(conj_thm_2Ebag_2ECOMMUTING__ITBAG__INSERT,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(arr@A_27b@A_27b))) => ( ! [V1b:$i] : ((mem@V1b@(arr@A_27a@ty_2Enum_2Enum)) => ((( ! [V2x:$i] : ((mem@V2x@A_27a) => ( ! [V3y:$i] : ((mem@V3y@A_27a) => ( ! [V4z:$i] : ((mem@V4z@A_27b) => ((ap@(ap@V0f@V2x)@(ap@(ap@V0f@V3y)@V4z)) = (ap@(ap@V0f@V3y)@(ap@(ap@V0f@V2x)@V4z))))))))) & (p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V1b))) => ( ! [V5x:$i] : ((mem@V5x@A_27a) => ( ! [V6a:$i] : ((mem@V6a@A_27b) => ((ap@(ap@(ap@(c_2Ebag_2EITBAG@A_27a@A_27b)@V0f)@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V5x)@V1b))@V6a) = (ap@(ap@(ap@(c_2Ebag_2EITBAG@A_27a@A_27b)@V0f)@V1b)@(ap@(ap@V0f@V5x)@V6a))))))))))))))).
thf(conj_thm_2Ebag_2ECOMMUTING__ITBAG__RECURSES,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(arr@A_27b@A_27b))) => ( ! [V1e:$i] : ((mem@V1e@A_27a) => ( ! [V2b:$i] : ((mem@V2b@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V3a:$i] : ((mem@V3a@A_27b) => ((( ! [V4x:$i] : ((mem@V4x@A_27a) => ( ! [V5y:$i] : ((mem@V5y@A_27a) => ( ! [V6z:$i] : ((mem@V6z@A_27b) => ((ap@(ap@V0f@V4x)@(ap@(ap@V0f@V5y)@V6z)) = (ap@(ap@V0f@V5y)@(ap@(ap@V0f@V4x)@V6z))))))))) & (p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V2b))) => ((ap@(ap@(ap@(c_2Ebag_2EITBAG@A_27a@A_27b)@V0f)@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V1e)@V2b))@V3a) = (ap@(ap@V0f@V1e)@(ap@(ap@(ap@(c_2Ebag_2EITBAG@A_27a@A_27b)@V0f)@V2b)@V3a))))))))))))))).
thf(ax_thm_2Ebag_2EBAG__GEN__SUM__def,axiom,( ! [V0bag:$i] : ((mem@V0bag@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)) => ( ! [V1n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Ebag_2EBAG__GEN__SUM@V0bag)@(inj__ty_2Enum_2Enum @ V1n))) = (surj__ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ebag_2EITBAG@ty_2Enum_2Enum@ty_2Enum_2Enum)@c_2Earithmetic_2E_2B)@V0bag)@(inj__ty_2Enum_2Enum @ V1n)))))))).
thf(ax_thm_2Ebag_2EBAG__GEN__PROD__def,axiom,( ! [V0bag:$i] : ((mem@V0bag@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)) => ( ! [V1n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Ebag_2EBAG__GEN__PROD@V0bag)@(inj__ty_2Enum_2Enum @ V1n))) = (surj__ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ebag_2EITBAG@ty_2Enum_2Enum@ty_2Enum_2Enum)@c_2Earithmetic_2E_2A)@V0bag)@(inj__ty_2Enum_2Enum @ V1n)))))))).
thf(conj_thm_2Ebag_2EBAG__GEN__SUM__EMPTY,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Ebag_2EBAG__GEN__SUM@(c_2Ebag_2EEMPTY__BAG@ty_2Enum_2Enum))@(inj__ty_2Enum_2Enum @ V0n))) = V0n))).
thf(conj_thm_2Ebag_2EBAG__GEN__PROD__EMPTY,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Ebag_2EBAG__GEN__PROD@(c_2Ebag_2EEMPTY__BAG@ty_2Enum_2Enum))@(inj__ty_2Enum_2Enum @ V0n))) = V0n))).
thf(conj_thm_2Ebag_2EBAG__GEN__SUM__TAILREC,lemma,( ! [V0b:$i] : ((mem@V0b@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)) => ((p@(ap@(c_2Ebag_2EFINITE__BAG@ty_2Enum_2Enum)@V0b)) => ( ! [V1x:tp__ty_2Enum_2Enum] : ( ! [V2a:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Ebag_2EBAG__GEN__SUM@(ap@(ap@(c_2Ebag_2EBAG__INSERT@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V1x))@V0b))@(inj__ty_2Enum_2Enum @ V2a))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Ebag_2EBAG__GEN__SUM@V0b)@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V1x))@(inj__ty_2Enum_2Enum @ V2a))))))))))).
thf(conj_thm_2Ebag_2EBAG__GEN__SUM__REC,lemma,( ! [V0b:$i] : ((mem@V0b@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)) => ((p@(ap@(c_2Ebag_2EFINITE__BAG@ty_2Enum_2Enum)@V0b)) => ( ! [V1x:tp__ty_2Enum_2Enum] : ( ! [V2a:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Ebag_2EBAG__GEN__SUM@(ap@(ap@(c_2Ebag_2EBAG__INSERT@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V1x))@V0b))@(inj__ty_2Enum_2Enum @ V2a))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V1x))@(ap@(ap@c_2Ebag_2EBAG__GEN__SUM@V0b)@(inj__ty_2Enum_2Enum @ V2a))))))))))).
thf(conj_thm_2Ebag_2EBAG__GEN__PROD__TAILREC,lemma,( ! [V0b:$i] : ((mem@V0b@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)) => ((p@(ap@(c_2Ebag_2EFINITE__BAG@ty_2Enum_2Enum)@V0b)) => ( ! [V1x:tp__ty_2Enum_2Enum] : ( ! [V2a:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Ebag_2EBAG__GEN__PROD@(ap@(ap@(c_2Ebag_2EBAG__INSERT@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V1x))@V0b))@(inj__ty_2Enum_2Enum @ V2a))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Ebag_2EBAG__GEN__PROD@V0b)@(ap@(ap@c_2Earithmetic_2E_2A@(inj__ty_2Enum_2Enum @ V1x))@(inj__ty_2Enum_2Enum @ V2a))))))))))).
thf(conj_thm_2Ebag_2EBAG__GEN__PROD__REC,lemma,( ! [V0b:$i] : ((mem@V0b@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)) => ((p@(ap@(c_2Ebag_2EFINITE__BAG@ty_2Enum_2Enum)@V0b)) => ( ! [V1x:tp__ty_2Enum_2Enum] : ( ! [V2a:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Ebag_2EBAG__GEN__PROD@(ap@(ap@(c_2Ebag_2EBAG__INSERT@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V1x))@V0b))@(inj__ty_2Enum_2Enum @ V2a))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2A@(inj__ty_2Enum_2Enum @ V1x))@(ap@(ap@c_2Ebag_2EBAG__GEN__PROD@V0b)@(inj__ty_2Enum_2Enum @ V2a))))))))))).
thf(conj_thm_2Ebag_2EBAG__GEN__PROD__EQ__1,lemma,( ! [V0b:$i] : ((mem@V0b@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)) => ((p@(ap@(c_2Ebag_2EFINITE__BAG@ty_2Enum_2Enum)@V0b)) => ( ! [V1e:tp__ty_2Enum_2Enum] : (((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Ebag_2EBAG__GEN__PROD@V0b)@(inj__ty_2Enum_2Enum @ V1e))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))) => (V1e = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))).
thf(conj_thm_2Ebag_2EBAG__GEN__PROD__ALL__ONES,lemma,( ! [V0b:$i] : ((mem@V0b@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)) => ((p@(ap@(c_2Ebag_2EFINITE__BAG@ty_2Enum_2Enum)@V0b)) => (((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Ebag_2EBAG__GEN__PROD@V0b)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))) => ( ! [V1x:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@(c_2Ebag_2EBAG__IN@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V1x))@V0b)) => (V1x = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))).
thf(conj_thm_2Ebag_2EBAG__GEN__PROD__POSITIVE,lemma,( ! [V0b:$i] : ((mem@V0b@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)) => ((p@(ap@(c_2Ebag_2EFINITE__BAG@ty_2Enum_2Enum)@V0b)) => (( ! [V1x:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@(c_2Ebag_2EBAG__IN@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V1x))@V0b)) => (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V1x))))) => (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@(ap@c_2Ebag_2EBAG__GEN__PROD@V0b)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))).
thf(ax_thm_2Ebag_2EBAG__EVERY,axiom,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2EBAG__EVERY@A_27a)@V0P)@V1b)) <=> ( ! [V2e:$i] : ((mem@V2e@A_27a) => ((p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V2e)@V1b)) => (p@(ap@V0P@V2e)))))))))))).
thf(conj_thm_2Ebag_2EBAG__EVERY__THM,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => (p@(ap@(ap@(c_2Ebag_2EBAG__EVERY@A_27a)@V0P)@(c_2Ebag_2EEMPTY__BAG@A_27a))))) & ( ! [V1P:$i] : ((mem@V1P@(arr@A_27b@bool)) => ( ! [V2e:$i] : ((mem@V2e@A_27b) => ( ! [V3b:$i] : ((mem@V3b@(arr@A_27b@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2EBAG__EVERY@A_27b)@V1P)@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27b)@V2e)@V3b))) <=> ((p@(ap@V1P@V2e)) & (p@(ap@(ap@(c_2Ebag_2EBAG__EVERY@A_27b)@V1P)@V3b)))))))))))))).
thf(conj_thm_2Ebag_2EBAG__EVERY__UNION,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1b1:$i] : ((mem@V1b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2b2:$i] : ((mem@V2b2@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2EBAG__EVERY@A_27a)@V0P)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V1b1)@V2b2))) <=> ((p@(ap@(ap@(c_2Ebag_2EBAG__EVERY@A_27a)@V0P)@V1b1)) & (p@(ap@(ap@(c_2Ebag_2EBAG__EVERY@A_27a)@V0P)@V2b2)))))))))))).
thf(conj_thm_2Ebag_2EBAG__EVERY__MERGE,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1b1:$i] : ((mem@V1b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2b2:$i] : ((mem@V2b2@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2EBAG__EVERY@A_27a)@V0P)@(ap@(ap@(c_2Ebag_2EBAG__MERGE@A_27a)@V1b1)@V2b2))) <=> ((p@(ap@(ap@(c_2Ebag_2EBAG__EVERY@A_27a)@V0P)@V1b1)) & (p@(ap@(ap@(c_2Ebag_2EBAG__EVERY@A_27a)@V0P)@V2b2)))))))))))).
thf(conj_thm_2Ebag_2EBAG__EVERY__SET,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebag_2EBAG__EVERY@A_27a)@V0P)@V1b)) <=> (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@(ap@(c_2Ebag_2ESET__OF__BAG@A_27a)@V1b))@(ap@(c_2Epred__set_2EGSPEC@A_27a@A_27a)@(lam@A_27a@(^ [V2x:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27a@bool)@V2x)@(ap@V0P@V2x)))))))))))))).
thf(conj_thm_2Ebag_2EBAG__FILTER__EQ__EMPTY,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@A_27a@ty_2Enum_2Enum)) => (((ap@(ap@(c_2Ebag_2EBAG__FILTER@A_27a)@V0P)@V1b) = (c_2Ebag_2EEMPTY__BAG@A_27a)) <=> (p@(ap@(ap@(c_2Ebag_2EBAG__EVERY@A_27a)@(ap@(ap@(c_2Ecombin_2Eo@A_27a@bool@bool)@c_2Ebool_2E_7E)@V0P))@V1b))))))))).
thf(conj_thm_2Ebag_2ESET__OF__BAG__IMAGE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27b@A_27a)) => ( ! [V1b:$i] : ((mem@V1b@(arr@A_27b@ty_2Enum_2Enum)) => ((ap@(c_2Ebag_2ESET__OF__BAG@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__IMAGE@A_27a@A_27b)@V0f)@V1b)) = (ap@(ap@(c_2Epred__set_2EIMAGE@A_27b@A_27a)@V0f)@(ap@(c_2Ebag_2ESET__OF__BAG@A_27b)@V1b)))))))))).
thf(conj_thm_2Ebag_2EBAG__IMAGE__FINITE__RESTRICTED__I,lemma,( ! [A_27a:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27a)) => ( ! [V1b:$i] : ((mem@V1b@(arr@A_27a@ty_2Enum_2Enum)) => (((p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V1b)) & (p@(ap@(ap@(c_2Ebag_2EBAG__EVERY@A_27a)@(lam@A_27a@(^ [V2e:$i] : (ap@(ap@(c_2Emin_2E_3D@A_27a)@(ap@V0f@V2e))@V2e))))@V1b))) => ((ap@(ap@(c_2Ebag_2EBAG__IMAGE@A_27a@A_27a)@V0f)@V1b) = V1b)))))))).
thf(ax_thm_2Ebag_2EBAG__ALL__DISTINCT,axiom,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(c_2Ebag_2EBAG__ALL__DISTINCT@A_27a)@V0b)) <=> ( ! [V1e:$i] : ((mem@V1e@A_27a) => (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@V0b@V1e))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))).
thf(conj_thm_2Ebag_2EBAG__ALL__DISTINCT__THM,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ((p@(ap@(c_2Ebag_2EBAG__ALL__DISTINCT@A_27a)@(c_2Ebag_2EEMPTY__BAG@A_27a))) & ( ! [V0e:$i] : ((mem@V0e@A_27b) => ( ! [V1b:$i] : ((mem@V1b@(arr@A_27b@ty_2Enum_2Enum)) => ((p@(ap@(c_2Ebag_2EBAG__ALL__DISTINCT@A_27b)@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27b)@V0e)@V1b))) <=> ((~~ (p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27b)@V0e)@V1b))) & (p@(ap@(c_2Ebag_2EBAG__ALL__DISTINCT@A_27b)@V1b)))))))))))).
thf(conj_thm_2Ebag_2EBAG__ALL__DISTINCT__BAG__MERGE,lemma,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(c_2Ebag_2EBAG__ALL__DISTINCT@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__MERGE@A_27a)@V0b1)@V1b2))) <=> ((p@(ap@(c_2Ebag_2EBAG__ALL__DISTINCT@A_27a)@V0b1)) & (p@(ap@(c_2Ebag_2EBAG__ALL__DISTINCT@A_27a)@V1b2)))))))))).
thf(conj_thm_2Ebag_2EBAG__ALL__DISTINCT__BAG__UNION,lemma,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(c_2Ebag_2EBAG__ALL__DISTINCT@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V0b1)@V1b2))) <=> ((p@(ap@(c_2Ebag_2EBAG__ALL__DISTINCT@A_27a)@V0b1)) & ((p@(ap@(c_2Ebag_2EBAG__ALL__DISTINCT@A_27a)@V1b2)) & (p@(ap@(ap@(c_2Ebag_2EBAG__DISJOINT@A_27a)@V0b1)@V1b2))))))))))).
thf(conj_thm_2Ebag_2EBAG__ALL__DISTINCT__DIFF,lemma,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(c_2Ebag_2EBAG__ALL__DISTINCT@A_27a)@V0b1)) => (p@(ap@(c_2Ebag_2EBAG__ALL__DISTINCT@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V0b1)@V1b2)))))))))).
thf(conj_thm_2Ebag_2EBAG__ALL__DISTINCT__DELETE,lemma,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(c_2Ebag_2EBAG__ALL__DISTINCT@A_27a)@V0b)) <=> ( ! [V1e:$i] : ((mem@V1e@A_27a) => ((p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V1e)@V0b)) => (~~ (p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V1e)@(ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V0b)@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V1e)@(c_2Ebag_2EEMPTY__BAG@A_27a)))))))))))))).
thf(conj_thm_2Ebag_2EBAG__ALL__DISTINCT__SET,lemma,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(c_2Ebag_2EBAG__ALL__DISTINCT@A_27a)@V0b)) <=> ((ap@(c_2Ebag_2EBAG__OF__SET@A_27a)@(ap@(c_2Ebag_2ESET__OF__BAG@A_27a)@V0b)) = V0b)))))).
thf(conj_thm_2Ebag_2EBAG__ALL__DISTINCT__BAG__OF__SET,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => (p@(ap@(c_2Ebag_2EBAG__ALL__DISTINCT@A_27a)@(ap@(c_2Ebag_2EBAG__OF__SET@A_27a)@V0s))))))).
thf(conj_thm_2Ebag_2EBAG__IN__BAG__DIFF__ALL__DISTINCT,lemma,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2e:$i] : ((mem@V2e@A_27a) => ((p@(ap@(c_2Ebag_2EBAG__ALL__DISTINCT@A_27a)@V0b1)) => ((p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V2e)@(ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@V0b1)@V1b2))) <=> ((p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V2e)@V0b1)) & (~~ (p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V2e)@V1b2)))))))))))))).
thf(conj_thm_2Ebag_2ESUB__BAG__ALL__DISTINCT,lemma,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(c_2Ebag_2EBAG__ALL__DISTINCT@A_27a)@V0b1)) => ((p@(ap@(ap@(c_2Ebag_2ESUB__BAG@A_27a)@V0b1)@V1b2)) <=> ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V2x)@V0b1)) => (p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V2x)@V1b2))))))))))))).
thf(conj_thm_2Ebag_2EBAG__ALL__DISTINCT__BAG__INN,lemma,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2e:$i] : ((mem@V2e@A_27a) => ((p@(ap@(c_2Ebag_2EBAG__ALL__DISTINCT@A_27a)@V0b)) => ((p@(ap@(ap@(ap@(c_2Ebag_2EBAG__INN@A_27a)@V2e)@(inj__ty_2Enum_2Enum @ V1n))@V0b)) <=> ((V1n = fo__c_2Enum_2E0) | ((V1n = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))) & (p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V2e)@V0b))))))))))))).
thf(conj_thm_2Ebag_2EBAG__ALL__DISTINCT__EXTENSION,lemma,( ! [A_27a:del]: ( ! [V0b1:$i] : ((mem@V0b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => (((p@(ap@(c_2Ebag_2EBAG__ALL__DISTINCT@A_27a)@V0b1)) & (p@(ap@(c_2Ebag_2EBAG__ALL__DISTINCT@A_27a)@V1b2))) => ((V0b1 = V1b2) <=> ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V2x)@V0b1)) <=> (p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V2x)@V1b2))))))))))))).
thf(conj_thm_2Ebag_2ENOT__BAG__IN,lemma,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => (((surj__ty_2Enum_2Enum @ (ap@V0b@V1x)) = fo__c_2Enum_2E0) <=> (~~ (p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V1x)@V0b)))))))))).
thf(conj_thm_2Ebag_2EBAG__UNION__EQ__LEFT,lemma,( ! [A_27a:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V1c:$i] : ((mem@V1c@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2d:$i] : ((mem@V2d@(arr@A_27a@ty_2Enum_2Enum)) => (((ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V0b)@V1c) = (ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V0b)@V2d)) => (V1c = V2d)))))))))).
thf(conj_thm_2Ebag_2EBAG__IN__DIVIDES,lemma,( ! [V0b:$i] : ((mem@V0b@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)) => ( ! [V1x:tp__ty_2Enum_2Enum] : ( ! [V2a:tp__ty_2Enum_2Enum] : (((p@(ap@(c_2Ebag_2EFINITE__BAG@ty_2Enum_2Enum)@V0b)) & (p@(ap@(ap@(c_2Ebag_2EBAG__IN@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V1x))@V0b))) => (p@(ap@(ap@c_2Edivides_2Edivides@(inj__ty_2Enum_2Enum @ V1x))@(ap@(ap@c_2Ebag_2EBAG__GEN__PROD@V0b)@(inj__ty_2Enum_2Enum @ V2a)))))))))).
thf(conj_thm_2Ebag_2EBAG__GEN__PROD__UNION__LEM,lemma,( ! [V0b1:$i] : ((mem@V0b1@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)) => ((p@(ap@(c_2Ebag_2EFINITE__BAG@ty_2Enum_2Enum)@V0b1)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)) => ( ! [V2a:tp__ty_2Enum_2Enum] : ( ! [V3b:tp__ty_2Enum_2Enum] : ((p@(ap@(c_2Ebag_2EFINITE__BAG@ty_2Enum_2Enum)@V1b2)) => ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Ebag_2EBAG__GEN__PROD@(ap@(ap@(c_2Ebag_2EBAG__UNION@ty_2Enum_2Enum)@V0b1)@V1b2))@(ap@(ap@c_2Earithmetic_2E_2A@(inj__ty_2Enum_2Enum @ V2a))@(inj__ty_2Enum_2Enum @ V3b)))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2A@(ap@(ap@c_2Ebag_2EBAG__GEN__PROD@V0b1)@(inj__ty_2Enum_2Enum @ V2a)))@(ap@(ap@c_2Ebag_2EBAG__GEN__PROD@V1b2)@(inj__ty_2Enum_2Enum @ V3b)))))))))))))).
thf(conj_thm_2Ebag_2EBAG__GEN__PROD__UNION,lemma,( ! [V0b1:$i] : ((mem@V0b1@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)) => (((p@(ap@(c_2Ebag_2EFINITE__BAG@ty_2Enum_2Enum)@V0b1)) & (p@(ap@(c_2Ebag_2EFINITE__BAG@ty_2Enum_2Enum)@V1b2))) => ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Ebag_2EBAG__GEN__PROD@(ap@(ap@(c_2Ebag_2EBAG__UNION@ty_2Enum_2Enum)@V0b1)@V1b2))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2A@(ap@(ap@c_2Ebag_2EBAG__GEN__PROD@V0b1)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@(ap@c_2Ebag_2EBAG__GEN__PROD@V1b2)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))))).
thf(ax_thm_2Ebag_2EBIG__BAG__UNION__def,axiom,( ! [A_27a:del]: ( ! [V0sob:$i] : ((mem@V0sob@(arr@(arr@A_27a@ty_2Enum_2Enum)@bool)) => ((ap@(c_2Ebag_2EBIG__BAG__UNION@A_27a)@V0sob) = (lam@A_27a@(^ [V1x:$i] : (ap@(ap@(c_2Epred__set_2ESUM__IMAGE@(arr@A_27a@ty_2Enum_2Enum))@(lam@(arr@A_27a@ty_2Enum_2Enum)@(^ [V2b:$i] : (ap@V2b@V1x))))@V0sob)))))))).
thf(conj_thm_2Ebag_2EBIG__BAG__UNION__EMPTY,lemma,( ! [A_27a:del]: ((ap@(c_2Ebag_2EBIG__BAG__UNION@A_27a)@(c_2Epred__set_2EEMPTY@(arr@A_27a@ty_2Enum_2Enum))) = (c_2Ebag_2EEMPTY__BAG@A_27a)))).
thf(conj_thm_2Ebag_2EBIG__BAG__UNION__INSERT,lemma,( ! [A_27a:del]: ( ! [V0sob:$i] : ((mem@V0sob@(arr@(arr@A_27a@ty_2Enum_2Enum)@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(c_2Epred__set_2EFINITE@(arr@A_27a@ty_2Enum_2Enum))@V0sob)) => ((ap@(c_2Ebag_2EBIG__BAG__UNION@A_27a)@(ap@(ap@(c_2Epred__set_2EINSERT@(arr@A_27a@ty_2Enum_2Enum))@V1b)@V0sob)) = (ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V1b)@(ap@(c_2Ebag_2EBIG__BAG__UNION@A_27a)@(ap@(ap@(c_2Epred__set_2EDELETE@(arr@A_27a@ty_2Enum_2Enum))@V0sob)@V1b))))))))))).
thf(conj_thm_2Ebag_2EBIG__BAG__UNION__DELETE,lemma,( ! [A_27a:del]: ( ! [V0sob:$i] : ((mem@V0sob@(arr@(arr@A_27a@ty_2Enum_2Enum)@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(c_2Epred__set_2EFINITE@(arr@A_27a@ty_2Enum_2Enum))@V0sob)) => ((ap@(c_2Ebag_2EBIG__BAG__UNION@A_27a)@(ap@(ap@(c_2Epred__set_2EDELETE@(arr@A_27a@ty_2Enum_2Enum))@V0sob)@V1b)) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(arr@A_27a@ty_2Enum_2Enum))@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@ty_2Enum_2Enum))@V1b)@V0sob))@(ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@(ap@(c_2Ebag_2EBIG__BAG__UNION@A_27a)@V0sob))@V1b))@(ap@(c_2Ebag_2EBIG__BAG__UNION@A_27a)@V0sob)))))))))).
thf(conj_thm_2Ebag_2EBIG__BAG__UNION__ITSET__BAG__UNION,lemma,( ! [A_27a:del]: ( ! [V0sob:$i] : ((mem@V0sob@(arr@(arr@A_27a@ty_2Enum_2Enum)@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@(arr@A_27a@ty_2Enum_2Enum))@V0sob)) => ((ap@(c_2Ebag_2EBIG__BAG__UNION@A_27a)@V0sob) = (ap@(ap@(ap@(c_2Epred__set_2EITSET@(arr@A_27a@ty_2Enum_2Enum)@(arr@A_27a@ty_2Enum_2Enum))@(c_2Ebag_2EBAG__UNION@A_27a))@V0sob)@(c_2Ebag_2EEMPTY__BAG@A_27a)))))))).
thf(conj_thm_2Ebag_2EFINITE__BIG__BAG__UNION,lemma,( ! [A_27a:del]: ( ! [V0sob:$i] : ((mem@V0sob@(arr@(arr@A_27a@ty_2Enum_2Enum)@bool)) => (((p@(ap@(c_2Epred__set_2EFINITE@(arr@A_27a@ty_2Enum_2Enum))@V0sob)) & ( ! [V1b:$i] : ((mem@V1b@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@ty_2Enum_2Enum))@V1b)@V0sob)) => (p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V1b)))))) => (p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@(ap@(c_2Ebag_2EBIG__BAG__UNION@A_27a)@V0sob)))))))).
thf(conj_thm_2Ebag_2EBAG__IN__BIG__BAG__UNION,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@(arr@A_27a@ty_2Enum_2Enum)@bool)) => ( ! [V1e:$i] : ((mem@V1e@A_27a) => ((p@(ap@(c_2Epred__set_2EFINITE@(arr@A_27a@ty_2Enum_2Enum))@V0P)) => ((p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V1e)@(ap@(c_2Ebag_2EBIG__BAG__UNION@A_27a)@V0P))) <=> (? [V2b:$i] : ((mem@V2b@(arr@A_27a@ty_2Enum_2Enum)) & ((p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V1e)@V2b)) & (p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@ty_2Enum_2Enum))@V2b)@V0P))))))))))))).
thf(conj_thm_2Ebag_2EBIG__BAG__UNION__EQ__EMPTY__BAG,lemma,( ! [A_27a:del]: ( ! [V0sob:$i] : ((mem@V0sob@(arr@(arr@A_27a@ty_2Enum_2Enum)@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@(arr@A_27a@ty_2Enum_2Enum))@V0sob)) => (((ap@(c_2Ebag_2EBIG__BAG__UNION@A_27a)@V0sob) = (c_2Ebag_2EEMPTY__BAG@A_27a)) <=> ( ! [V1b:$i] : ((mem@V1b@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@ty_2Enum_2Enum))@V1b)@V0sob)) => (V1b = (c_2Ebag_2EEMPTY__BAG@A_27a))))))))))).
thf(conj_thm_2Ebag_2EBIG__BAG__UNION__UNION,lemma,( ! [A_27a:del]: ( ! [V0s1:$i] : ((mem@V0s1@(arr@(arr@A_27a@ty_2Enum_2Enum)@bool)) => ( ! [V1s2:$i] : ((mem@V1s2@(arr@(arr@A_27a@ty_2Enum_2Enum)@bool)) => (((p@(ap@(c_2Epred__set_2EFINITE@(arr@A_27a@ty_2Enum_2Enum))@V0s1)) & (p@(ap@(c_2Epred__set_2EFINITE@(arr@A_27a@ty_2Enum_2Enum))@V1s2))) => ((ap@(c_2Ebag_2EBIG__BAG__UNION@A_27a)@(ap@(ap@(c_2Epred__set_2EUNION@(arr@A_27a@ty_2Enum_2Enum))@V0s1)@V1s2)) = (ap@(ap@(c_2Ebag_2EBAG__DIFF@A_27a)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@(ap@(c_2Ebag_2EBIG__BAG__UNION@A_27a)@V0s1))@(ap@(c_2Ebag_2EBIG__BAG__UNION@A_27a)@V1s2)))@(ap@(c_2Ebag_2EBIG__BAG__UNION@A_27a)@(ap@(ap@(c_2Epred__set_2EINTER@(arr@A_27a@ty_2Enum_2Enum))@V0s1)@V1s2))))))))))).
thf(conj_thm_2Ebag_2EBIG__BAG__UNION__EQ__ELEMENT,lemma,( ! [A_27a:del]: ( ! [V0sob:$i] : ((mem@V0sob@(arr@(arr@A_27a@ty_2Enum_2Enum)@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@A_27a@ty_2Enum_2Enum)) => (((p@(ap@(c_2Epred__set_2EFINITE@(arr@A_27a@ty_2Enum_2Enum))@V0sob)) & (p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@ty_2Enum_2Enum))@V1b)@V0sob))) => (((ap@(c_2Ebag_2EBIG__BAG__UNION@A_27a)@V0sob) = V1b) <=> ( ! [V2b_27:$i] : ((mem@V2b_27@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@ty_2Enum_2Enum))@V2b_27)@V0sob)) => ((V2b_27 = V1b) | (V2b_27 = (c_2Ebag_2EEMPTY__BAG@A_27a)))))))))))))).
thf(ax_thm_2Ebag_2Emlt1__def,axiom,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(arr@A_27a@(arr@A_27a@bool))) => ( ! [V1b1:$i] : ((mem@V1b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2b2:$i] : ((mem@V2b2@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(ap@(c_2Ebag_2Emlt1@A_27a)@V0r)@V1b1)@V2b2)) <=> ((p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V1b1)) & ((p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V2b2)) & (? [V3e:$i] : ((mem@V3e@A_27a) & (? [V4rep:$i] : ((mem@V4rep@(arr@A_27a@ty_2Enum_2Enum)) & (? [V5res:$i] : ((mem@V5res@(arr@A_27a@ty_2Enum_2Enum)) & ((V1b1 = (ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V4rep)@V5res)) & ((V2b2 = (ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V5res)@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V3e)@(c_2Ebag_2EEMPTY__BAG@A_27a)))) & ( ! [V6e_27:$i] : ((mem@V6e_27@A_27a) => ((p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V6e_27)@V4rep)) => (p@(ap@(ap@V0r@V6e_27)@V3e)))))))))))))))))))))))).
thf(conj_thm_2Ebag_2EBAG__NOT__LESS__EMPTY,lemma,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(arr@A_27a@(arr@A_27a@bool))) => ( ! [V1b:$i] : ((mem@V1b@(arr@A_27a@ty_2Enum_2Enum)) => (~~ (p@(ap@(ap@(ap@(c_2Ebag_2Emlt1@A_27a)@V0r)@V1b)@(c_2Ebag_2EEMPTY__BAG@A_27a)))))))))).
thf(conj_thm_2Ebag_2ENOT__mlt__EMPTY,lemma,( ! [A_27a:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27a@bool))) => ( ! [V1b:$i] : ((mem@V1b@(arr@A_27a@ty_2Enum_2Enum)) => (~~ (p@(ap@(ap@(ap@(c_2Erelation_2ETC@(arr@A_27a@ty_2Enum_2Enum))@(ap@(c_2Ebag_2Emlt1@A_27a)@V0R))@V1b)@(c_2Ebag_2EEMPTY__BAG@A_27a)))))))))).
thf(conj_thm_2Ebag_2EBAG__LESS__ADD,lemma,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(arr@A_27a@(arr@A_27a@bool))) => ( ! [V1N:$i] : ((mem@V1N@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2M0:$i] : ((mem@V2M0@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V3a:$i] : ((mem@V3a@A_27a) => ((p@(ap@(ap@(ap@(c_2Ebag_2Emlt1@A_27a)@V0r)@V1N)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V2M0)@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V3a)@(c_2Ebag_2EEMPTY__BAG@A_27a))))) => ((? [V4M:$i] : ((mem@V4M@(arr@A_27a@ty_2Enum_2Enum)) & ((p@(ap@(ap@(ap@(c_2Ebag_2Emlt1@A_27a)@V0r)@V4M)@V2M0)) & (V1N = (ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V4M)@(ap@(ap@(c_2Ebag_2EBAG__INSERT@A_27a)@V3a)@(c_2Ebag_2EEMPTY__BAG@A_27a))))))) | (? [V5KK:$i] : ((mem@V5KK@(arr@A_27a@ty_2Enum_2Enum)) & (( ! [V6b:$i] : ((mem@V6b@A_27a) => ((p@(ap@(ap@(c_2Ebag_2EBAG__IN@A_27a)@V6b)@V5KK)) => (p@(ap@(ap@V0r@V6b)@V3a))))) & (V1N = (ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V2M0)@V5KK))))))))))))))))).
thf(conj_thm_2Ebag_2Emlt1__all__accessible,lemma,( ! [A_27a:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27a@bool))) => ((p@(ap@(c_2Erelation_2EWF@A_27a)@V0R)) => ( ! [V1M:$i] : ((mem@V1M@(arr@A_27a@ty_2Enum_2Enum)) => (p@(ap@(ap@(c_2Erelation_2EWFP@(arr@A_27a@ty_2Enum_2Enum))@(ap@(c_2Ebag_2Emlt1@A_27a)@V0R))@V1M))))))))).
thf(conj_thm_2Ebag_2EWF__mlt1,lemma,( ! [A_27a:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27a@bool))) => ((p@(ap@(c_2Erelation_2EWF@A_27a)@V0R)) => (p@(ap@(c_2Erelation_2EWF@(arr@A_27a@ty_2Enum_2Enum))@(ap@(c_2Ebag_2Emlt1@A_27a)@V0R)))))))).
thf(conj_thm_2Ebag_2ETC__mlt1__FINITE__BAG,lemma,( ! [A_27a:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27a@bool))) => ( ! [V1b1:$i] : ((mem@V1b1@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2b2:$i] : ((mem@V2b2@(arr@A_27a@ty_2Enum_2Enum)) => ((p@(ap@(ap@(ap@(c_2Erelation_2ETC@(arr@A_27a@ty_2Enum_2Enum))@(ap@(c_2Ebag_2Emlt1@A_27a)@V0R))@V1b1)@V2b2)) => ((p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V1b1)) & (p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V2b2)))))))))))).
thf(conj_thm_2Ebag_2ETC__mlt1__UNION2__I,conjecture,( ! [A_27a:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27a@bool))) => ( ! [V1b2:$i] : ((mem@V1b2@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2b1:$i] : ((mem@V2b1@(arr@A_27a@ty_2Enum_2Enum)) => (((p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V1b2)) & ((p@(ap@(c_2Ebag_2EFINITE__BAG@A_27a)@V2b1)) & (~~ (V1b2 = (c_2Ebag_2EEMPTY__BAG@A_27a))))) => (p@(ap@(ap@(ap@(c_2Erelation_2ETC@(arr@A_27a@ty_2Enum_2Enum))@(ap@(c_2Ebag_2Emlt1@A_27a)@V0R))@V2b1)@(ap@(ap@(c_2Ebag_2EBAG__UNION@A_27a)@V2b1)@V1b2)))))))))))).
