include('Axioms/readerMonad_2.ax').
tff(tp_c_2Ebag_2EBAG__ALL__DISTINCT,type,(c_2Ebag_2EBAG__ALL__DISTINCT:del > $i)).
tff(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)))).
tff(tp_c_2Ebag_2EBAG__CARD,type,(c_2Ebag_2EBAG__CARD:del > $i)).
tff(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)))).
tff(tp_c_2Ebag_2EBAG__CARD__RELn,type,(c_2Ebag_2EBAG__CARD__RELn:del > $i)).
tff(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))))).
tff(tp_c_2Ebag_2EBAG__CHOICE,type,(c_2Ebag_2EBAG__CHOICE:del > $i)).
tff(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)))).
tff(tp_c_2Ebag_2EBAG__DELETE,type,(c_2Ebag_2EBAG__DELETE:del > $i)).
tff(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)))))).
tff(tp_c_2Ebag_2EBAG__DIFF,type,(c_2Ebag_2EBAG__DIFF:del > $i)).
tff(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)))))).
tff(tp_c_2Ebag_2EBAG__DISJOINT,type,(c_2Ebag_2EBAG__DISJOINT:del > $i)).
tff(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))))).
tff(tp_c_2Ebag_2EBAG__EVERY,type,(c_2Ebag_2EBAG__EVERY:del > $i)).
tff(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))))).
tff(tp_c_2Ebag_2EBAG__FILTER,type,(c_2Ebag_2EBAG__FILTER:del > $i)).
tff(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)))))).
tff(tp_c_2Ebag_2EBAG__GEN__PROD,type,(c_2Ebag_2EBAG__GEN__PROD:$i)).
tff(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)))).
tff(tp_c_2Ebag_2EBAG__GEN__SUM,type,(c_2Ebag_2EBAG__GEN__SUM:$i)).
tff(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)))).
tff(tp_c_2Ebag_2EBAG__IMAGE,type,(c_2Ebag_2EBAG__IMAGE:(del * del) > $i)).
tff(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))))))).
tff(tp_c_2Ebag_2EBAG__IN,type,(c_2Ebag_2EBAG__IN:del > $i)).
tff(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))))).
tff(tp_c_2Ebag_2EBAG__INN,type,(c_2Ebag_2EBAG__INN:del > $i)).
tff(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)))))).
tff(tp_c_2Ebag_2EBAG__INSERT,type,(c_2Ebag_2EBAG__INSERT:del > $i)).
tff(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)))))).
tff(tp_c_2Ebag_2EBAG__INTER,type,(c_2Ebag_2EBAG__INTER:del > $i)).
tff(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)))))).
tff(tp_c_2Ebag_2EBAG__MERGE,type,(c_2Ebag_2EBAG__MERGE:del > $i)).
tff(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)))))).
tff(tp_c_2Ebag_2EBAG__OF__SET,type,(c_2Ebag_2EBAG__OF__SET:del > $i)).
tff(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))))).
tff(tp_c_2Ebag_2EBAG__REST,type,(c_2Ebag_2EBAG__REST:del > $i)).
tff(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))))).
tff(tp_c_2Ebag_2EBAG__UNION,type,(c_2Ebag_2EBAG__UNION:del > $i)).
tff(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)))))).
tff(tp_c_2Ebag_2EBIG__BAG__UNION,type,(c_2Ebag_2EBIG__BAG__UNION:del > $i)).
tff(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))))).
tff(tp_c_2Ebag_2EEL__BAG,type,(c_2Ebag_2EEL__BAG:del > $i)).
tff(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))))).
tff(tp_c_2Ebag_2EEMPTY__BAG,type,(c_2Ebag_2EEMPTY__BAG:del > $i)).
tff(mem_c_2Ebag_2EEMPTY__BAG,axiom,( ! [A_27a:del] : mem(c_2Ebag_2EEMPTY__BAG(A_27a),arr(A_27a,ty_2Enum_2Enum)))).
tff(tp_c_2Ebag_2EFINITE__BAG,type,(c_2Ebag_2EFINITE__BAG:del > $i)).
tff(mem_c_2Ebag_2EFINITE__BAG,axiom,( ! [A_27a:del] : mem(c_2Ebag_2EFINITE__BAG(A_27a),arr(arr(A_27a,ty_2Enum_2Enum),bool)))).
tff(tp_c_2Ebag_2EITBAG,type,(c_2Ebag_2EITBAG:(del * del) > $i)).
tff(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))))))).
tff(tp_c_2Ebag_2EPSUB__BAG,type,(c_2Ebag_2EPSUB__BAG:del > $i)).
tff(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))))).
tff(tp_c_2Ebag_2ESET__OF__BAG,type,(c_2Ebag_2ESET__OF__BAG:del > $i)).
tff(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))))).
tff(tp_c_2Ebag_2ESING__BAG,type,(c_2Ebag_2ESING__BAG:del > $i)).
tff(mem_c_2Ebag_2ESING__BAG,axiom,( ! [A_27a:del] : mem(c_2Ebag_2ESING__BAG(A_27a),arr(arr(A_27a,ty_2Enum_2Enum),bool)))).
tff(tp_c_2Ebag_2ESUB__BAG,type,(c_2Ebag_2ESUB__BAG:del > $i)).
tff(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))))).
tff(tp_c_2Ebag_2Ebag__size,type,(c_2Ebag_2Ebag__size:del > $i)).
tff(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))))).
tff(tp_c_2Ebag_2Edominates,type,(c_2Ebag_2Edominates:(del * del) > $i)).
tff(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))))))).
tff(tp_c_2Ebag_2Emlt1,type,(c_2Ebag_2Emlt1:del > $i)).
tff(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)))))).
tff(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))))).
tff(conj_thm_2Ebag_2EEMPTY__BAG__alt,lemma,(( ! [A_27a:del]: (c_2Ebag_2EEMPTY__BAG(A_27a) = k(A_27a,c_2Enum_2E0))))).
tff(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))))))))))).
tff(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))))))))))))).
tff(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)))))))))).
tff(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))))))))).
tff(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) = f960(A_27a,V0b,V1c)))))))).
tff(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) = f961(A_27a,V0b1,V1b2)))))))).
tff(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) = f962(A_27a,V0e,V1b)))))))).
tff(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)))))))))))).
tff(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) = f963(A_27a,V0b1,V1b2)))))))).
tff(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) = f964(A_27a,V1b2,V0b1)))))))).
tff(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)))))).
tff(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))))))))).
tff(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)))))))))))).
tff(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))))))))))))).
tff(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)))))))))))))).
tff(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))))))))))))))).
tff(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)))))))))).
tff(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)))))))))).
tff(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))))))))))))).
tff(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))))))))))))))))).
tff(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)))))))))))))).
tff(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))))))))))))).
tff(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)))))))))))))).
tff(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))))))))))))).
tff(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))))))))).
tff(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)))))))))).
tff(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))))))))))).
tff(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))))))))))).
tff(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)))))))))))).
tff(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)))))))))))).
tff(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))))))))))).
tff(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))))))))).
tff(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))))))))))).
tff(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))))))))))).
tff(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))))))))))))))).
tff(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))))))))))).
tff(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)))))))))).
tff(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))))))))))))))))))).
tff(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)))))))))))))))).
tff(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))))))))))))).
tff(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)))))))))))).
tff(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)))))))))))))))).
tff(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))))))))))))))).
tff(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)))))))))))))).
tff(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)))))))))))).
tff(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 = f965(A_27a,V2e,V0b0))))))))))))).
tff(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))))))))).
tff(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)))))))))))))))))).
tff(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))))))))))))))))))).
tff(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)))))))))).
tff(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))))))))).
tff(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))))))).
tff(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))))))))).
tff(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))))))))))))).
tff(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)))))))).
tff(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))))))))).
tff(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))))))))))))))).
tff(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)))))))))).
tff(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))))))))).
tff(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)))))))).
tff(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))))))))).
tff(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))))))))))))).
tff(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))))))))).
tff(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))))))).
tff(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)))))))).
tff(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))))))))).
tff(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))))))))))).
tff(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)))))))))))).
tff(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)))))))))))).
tff(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)))))))))).
tff(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)))))))))).
tff(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)))))))))))))))).
tff(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))))))))))).
tff(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)))))))))).
tff(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))))))))))).
tff(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))))))))))))).
tff(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)))))))))))).
tff(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))))))))))))).
tff(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)))))))))))).
tff(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))))))))))))).
tff(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)))))))))))).
tff(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)))))))))))).
tff(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)))))))))))))))))).
tff(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)))))))))))))).
tff(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))))))))))))))).
tff(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)))))))))))).
tff(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))))))))))))))))))))))))))))))))))))))))).
tff(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)))))))))).
tff(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)))))))))))).
tff(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))))))))))))).
tff(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))))))))))))).
tff(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)))))))))))).
tff(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)))))))))))).
tff(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))))))))))))).
tff(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))))))))))))).
tff(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)))))))))))))))))).
tff(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)))))))))).
tff(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)))))))))))).
tff(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) = f966(A_27a,V0b)))))).
tff(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) = f967(A_27a,V0P)))))).
tff(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))))).
tff(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)))))))))).
tff(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))))).
tff(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)))))).
tff(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))))))))))).
tff(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)))))))))).
tff(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)))))))))).
tff(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)))))))))).
tff(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)))))))).
tff(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))))))))))).
tff(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)))))))))).
tff(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)))))))))).
tff(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))))))))).
tff(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)))))))))).
tff(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)))))))).
tff(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)))))))))).
tff(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)))))))))))))).
tff(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))))))))))))))).
tff(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)))))))))))))).
tff(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)))))))))).
tff(conj_thm_2Ebag_2EFINITE__EMPTY__BAG,lemma,(( ! [A_27a:del]: p(ap(c_2Ebag_2EFINITE__BAG(A_27a),c_2Ebag_2EEMPTY__BAG(A_27a)))))).
tff(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))))))))))).
tff(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))))))))))).
tff(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))))))))))).
tff(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))))))))))).
tff(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))))))))))).
tff(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))))))))))).
tff(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))))))))))).
tff(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))))))))))).
tff(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)))))))))))).
tff(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)))))))).
tff(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)))).
tff(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))))))))).
tff(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))))))))))))))).
tff(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)))))))))))).
tff(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)))))))))))))).
tff(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))))))))))))).
tff(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))))))))))).
tff(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))))))))))).
tff(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))))))))))))).
tff(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) = f968(A_27a,V1b,V0P)))))))).
tff(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))))))).
tff(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)))))))))))).
tff(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))))))))))).
tff(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))))))))))))))).
tff(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))))))))))))).
tff(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),f969(A_27a,V0P,V1Q)),V2b))))))))))).
tff(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))))))))).
tff(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)))))))))))))))))))).
tff(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)))))))).
tff(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) = f972(A_27a,A_27b,V1b,V0f))))))))).
tff(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)))))))).
tff(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)))))))))))))).
tff(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)))))))))))))).
tff(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)))))))))))).
tff(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))))))))))))))).
tff(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))))))).
tff(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))))))))))))))))).
tff(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)))))))))))).
tff(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))))))).
tff(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)))))))).
tff(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))))))))).
tff(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)))))).
tff(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))))))).
tff(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))))))).
tff(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)))))))).
tff(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))))))))))).
tff(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))))))))))).
tff(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))))))))))))).
tff(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)))))))))).
tff(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))))))))))))))).
tff(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))))))))))))))).
tff(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))))))))).
tff(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)))))))))))))))).
tff(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)))))))))))))))).
tff(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)))))))))))))))).
tff(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)))))))).
tff(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)))))))).
tff(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)))).
tff(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)))).
tff(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)))))))))))).
tff(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)))))))))))).
tff(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)))))))))))).
tff(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)))))))))))).
tff(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)))))))))))).
tff(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))))))))))))).
tff(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)))))))))))).
tff(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)))))))))))).
tff(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))))))))))))))).
tff(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))))))))))))).
tff(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))))))))))))).
tff(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),f418(A_27a,V0P)))))))))))).
tff(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)))))))))).
tff(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))))))))))).
tff(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),f973(A_27a,V0f)),V1b))) => (ap(ap(c_2Ebag_2EBAG__IMAGE(A_27a,A_27a),V0f),V1b) = V1b))))))))).
tff(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)))))))))))).
tff(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))))))))))))).
tff(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))))))))))).
tff(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)))))))))))).
tff(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))))))))))).
tff(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))))))))))))))).
tff(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))))))).
tff(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)))))))).
tff(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))))))))))))))).
tff(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)))))))))))))).
tff(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)))))))))))))).
tff(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)))))))))))))).
tff(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))))))))))).
tff(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))))))))))).
tff(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))))))))))).
tff(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))))))))))))))).
tff(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)))))))))))))).
tff(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) = f975(A_27a,V0sob)))))).
tff(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))))).
tff(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)))))))))))).
tff(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))))))))))).
tff(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))))))))).
tff(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))))))))).
tff(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)))))))))))))).
tff(conj_thm_2Ebag_2EBIG__BAG__UNION__EQ__EMPTY__BAG,conjecture,(( ! [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)))))))))))).
