include('Axioms/EncodeVar+2.ax').
fof(ne_ty_2Eenumeral_2Ebl,axiom,( ! [A0] : ( ne(A0) => ne(ty_2Eenumeral_2Ebl(A0)) ) )).
fof(ne_ty_2Eenumeral_2Ebt,axiom,( ! [A0] : ( ne(A0) => ne(ty_2Eenumeral_2Ebt(A0)) ) )).
fof(mem_c_2Eenumeral_2EBL__ACCUM,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2EBL__ACCUM(A_27a),arr(A_27a,arr(ty_2Eenumeral_2Ebt(A_27a),arr(ty_2Eenumeral_2Ebl(A_27a),ty_2Eenumeral_2Ebl(A_27a))))) ) )).
fof(mem_c_2Eenumeral_2EBL__CONS,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2EBL__CONS(A_27a),arr(A_27a,arr(ty_2Eenumeral_2Ebl(A_27a),ty_2Eenumeral_2Ebl(A_27a)))) ) )).
fof(mem_c_2Eenumeral_2EENUMERAL,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2EENUMERAL(A_27a),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Eenumeral_2Ebt(A_27a),arr(A_27a,bool)))) ) )).
fof(mem_c_2Eenumeral_2EK2,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2EK2(A_27a),arr(A_27a,ty_2Enum_2Enum)) ) )).
fof(mem_c_2Eenumeral_2ELESS__ALL,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2ELESS__ALL(A_27a),arr(ty_2Etoto_2Etoto(A_27a),arr(A_27a,arr(arr(A_27a,bool),bool)))) ) )).
fof(mem_c_2Eenumeral_2EOL,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2EOL(A_27a),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Elist_2Elist(A_27a),bool))) ) )).
fof(mem_c_2Eenumeral_2EOL__bt,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2EOL__bt(A_27a),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Eenumeral_2Ebt(A_27a),bool))) ) )).
fof(mem_c_2Eenumeral_2EOL__bt__lb,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2EOL__bt__lb(A_27a),arr(ty_2Etoto_2Etoto(A_27a),arr(A_27a,arr(ty_2Eenumeral_2Ebt(A_27a),bool)))) ) )).
fof(mem_c_2Eenumeral_2EOL__bt__lb__ub,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2EOL__bt__lb__ub(A_27a),arr(ty_2Etoto_2Etoto(A_27a),arr(A_27a,arr(ty_2Eenumeral_2Ebt(A_27a),arr(A_27a,bool))))) ) )).
fof(mem_c_2Eenumeral_2EOL__bt__ub,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2EOL__bt__ub(A_27a),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Eenumeral_2Ebt(A_27a),arr(A_27a,bool)))) ) )).
fof(mem_c_2Eenumeral_2EOL__sublists,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2EOL__sublists(A_27a),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a))),bool))) ) )).
fof(mem_c_2Eenumeral_2EOU,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2EOU(A_27a),arr(ty_2Etoto_2Etoto(A_27a),arr(arr(A_27a,bool),arr(arr(A_27a,bool),arr(A_27a,bool))))) ) )).
fof(mem_c_2Eenumeral_2EOWL,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2EOWL(A_27a),arr(ty_2Etoto_2Etoto(A_27a),arr(arr(A_27a,bool),arr(ty_2Elist_2Elist(A_27a),bool)))) ) )).
fof(mem_c_2Eenumeral_2EUO,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2EUO(A_27a),arr(ty_2Etoto_2Etoto(A_27a),arr(arr(A_27a,bool),arr(arr(A_27a,bool),arr(A_27a,bool))))) ) )).
fof(mem_c_2Eenumeral_2Ebl__CASE,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Eenumeral_2Ebl__CASE(A_27a,A_27b),arr(ty_2Eenumeral_2Ebl(A_27a),arr(A_27b,arr(arr(ty_2Eenumeral_2Ebl(A_27a),A_27b),arr(arr(A_27a,arr(ty_2Eenumeral_2Ebt(A_27a),arr(ty_2Eenumeral_2Ebl(A_27a),A_27b))),A_27b))))) ) ) )).
fof(mem_c_2Eenumeral_2Ebl__rev,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2Ebl__rev(A_27a),arr(ty_2Eenumeral_2Ebt(A_27a),arr(ty_2Eenumeral_2Ebl(A_27a),ty_2Eenumeral_2Ebt(A_27a)))) ) )).
fof(mem_c_2Eenumeral_2Ebl__size,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2Ebl__size(A_27a),arr(arr(A_27a,ty_2Enum_2Enum),arr(ty_2Eenumeral_2Ebl(A_27a),ty_2Enum_2Enum))) ) )).
fof(mem_c_2Eenumeral_2Ebl__to__bt,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2Ebl__to__bt(A_27a),arr(ty_2Eenumeral_2Ebl(A_27a),ty_2Eenumeral_2Ebt(A_27a))) ) )).
fof(mem_c_2Eenumeral_2Ebl__to__set,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2Ebl__to__set(A_27a),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Eenumeral_2Ebl(A_27a),arr(A_27a,bool)))) ) )).
fof(mem_c_2Eenumeral_2Ebt__CASE,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Eenumeral_2Ebt__CASE(A_27a,A_27b),arr(ty_2Eenumeral_2Ebt(A_27a),arr(A_27b,arr(arr(ty_2Eenumeral_2Ebt(A_27a),arr(A_27a,arr(ty_2Eenumeral_2Ebt(A_27a),A_27b))),A_27b)))) ) ) )).
fof(mem_c_2Eenumeral_2Ebt__rev,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2Ebt__rev(A_27a),arr(ty_2Eenumeral_2Ebt(A_27a),arr(ty_2Eenumeral_2Ebl(A_27a),ty_2Eenumeral_2Ebl(A_27a)))) ) )).
fof(mem_c_2Eenumeral_2Ebt__size,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2Ebt__size(A_27a),arr(arr(A_27a,ty_2Enum_2Enum),arr(ty_2Eenumeral_2Ebt(A_27a),ty_2Enum_2Enum))) ) )).
fof(mem_c_2Eenumeral_2Ebt__to__bl,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2Ebt__to__bl(A_27a),arr(ty_2Eenumeral_2Ebt(A_27a),ty_2Eenumeral_2Ebl(A_27a))) ) )).
fof(mem_c_2Eenumeral_2Ebt__to__list,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2Ebt__to__list(A_27a),arr(ty_2Eenumeral_2Ebt(A_27a),ty_2Elist_2Elist(A_27a))) ) )).
fof(mem_c_2Eenumeral_2Ebt__to__list__ac,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2Ebt__to__list__ac(A_27a),arr(ty_2Eenumeral_2Ebt(A_27a),arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a)))) ) )).
fof(mem_c_2Eenumeral_2Ebt__to__ol,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2Ebt__to__ol(A_27a),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Eenumeral_2Ebt(A_27a),ty_2Elist_2Elist(A_27a)))) ) )).
fof(mem_c_2Eenumeral_2Ebt__to__ol__ac,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2Ebt__to__ol__ac(A_27a),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Eenumeral_2Ebt(A_27a),arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a))))) ) )).
fof(mem_c_2Eenumeral_2Ebt__to__ol__lb,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2Ebt__to__ol__lb(A_27a),arr(ty_2Etoto_2Etoto(A_27a),arr(A_27a,arr(ty_2Eenumeral_2Ebt(A_27a),ty_2Elist_2Elist(A_27a))))) ) )).
fof(mem_c_2Eenumeral_2Ebt__to__ol__lb__ac,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2Ebt__to__ol__lb__ac(A_27a),arr(ty_2Etoto_2Etoto(A_27a),arr(A_27a,arr(ty_2Eenumeral_2Ebt(A_27a),arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a)))))) ) )).
fof(mem_c_2Eenumeral_2Ebt__to__ol__lb__ub,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2Ebt__to__ol__lb__ub(A_27a),arr(ty_2Etoto_2Etoto(A_27a),arr(A_27a,arr(ty_2Eenumeral_2Ebt(A_27a),arr(A_27a,ty_2Elist_2Elist(A_27a)))))) ) )).
fof(mem_c_2Eenumeral_2Ebt__to__ol__lb__ub__ac,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2Ebt__to__ol__lb__ub__ac(A_27a),arr(ty_2Etoto_2Etoto(A_27a),arr(A_27a,arr(ty_2Eenumeral_2Ebt(A_27a),arr(A_27a,arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a))))))) ) )).
fof(mem_c_2Eenumeral_2Ebt__to__ol__ub,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2Ebt__to__ol__ub(A_27a),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Eenumeral_2Ebt(A_27a),arr(A_27a,ty_2Elist_2Elist(A_27a))))) ) )).
fof(mem_c_2Eenumeral_2Ebt__to__ol__ub__ac,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2Ebt__to__ol__ub__ac(A_27a),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Eenumeral_2Ebt(A_27a),arr(A_27a,arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a)))))) ) )).
fof(mem_c_2Eenumeral_2Ebt__to__set__lb,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2Ebt__to__set__lb(A_27a),arr(ty_2Etoto_2Etoto(A_27a),arr(A_27a,arr(ty_2Eenumeral_2Ebt(A_27a),arr(A_27a,bool))))) ) )).
fof(mem_c_2Eenumeral_2Ebt__to__set__lb__ub,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2Ebt__to__set__lb__ub(A_27a),arr(ty_2Etoto_2Etoto(A_27a),arr(A_27a,arr(ty_2Eenumeral_2Ebt(A_27a),arr(A_27a,arr(A_27a,bool)))))) ) )).
fof(mem_c_2Eenumeral_2Ebt__to__set__ub,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2Ebt__to__set__ub(A_27a),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Eenumeral_2Ebt(A_27a),arr(A_27a,arr(A_27a,bool))))) ) )).
fof(mem_c_2Eenumeral_2Eincr__sbuild,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2Eincr__sbuild(A_27a),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a)))))) ) )).
fof(mem_c_2Eenumeral_2Eincr__smerge,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2Eincr__smerge(A_27a),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Elist_2Elist(A_27a),arr(ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a))),ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a))))))) ) )).
fof(mem_c_2Eenumeral_2Eincr__ssort,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2Eincr__ssort(A_27a),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a)))) ) )).
fof(mem_c_2Eenumeral_2Elist__to__bl,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2Elist__to__bl(A_27a),arr(ty_2Elist_2Elist(A_27a),ty_2Eenumeral_2Ebl(A_27a))) ) )).
fof(mem_c_2Eenumeral_2Elist__to__bt,axiom,( ! [A_27c] : ( ne(A_27c) => mem(c_2Eenumeral_2Elist__to__bt(A_27c),arr(ty_2Elist_2Elist(A_27c),ty_2Eenumeral_2Ebt(A_27c))) ) )).
fof(mem_c_2Eenumeral_2Elol__set,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2Elol__set(A_27a),arr(ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a))),arr(A_27a,bool))) ) )).
fof(mem_c_2Eenumeral_2Enbl,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2Enbl(A_27a),ty_2Eenumeral_2Ebl(A_27a)) ) )).
fof(mem_c_2Eenumeral_2Enode,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2Enode(A_27a),arr(ty_2Eenumeral_2Ebt(A_27a),arr(A_27a,arr(ty_2Eenumeral_2Ebt(A_27a),ty_2Eenumeral_2Ebt(A_27a))))) ) )).
fof(mem_c_2Eenumeral_2Ent,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2Ent(A_27a),ty_2Eenumeral_2Ebt(A_27a)) ) )).
fof(mem_c_2Eenumeral_2Eonebl,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2Eonebl(A_27a),arr(A_27a,arr(ty_2Eenumeral_2Ebt(A_27a),arr(ty_2Eenumeral_2Ebl(A_27a),ty_2Eenumeral_2Ebl(A_27a))))) ) )).
fof(mem_c_2Eenumeral_2Esdiff,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2Esdiff(A_27a),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Elist_2Elist(A_27a),arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a))))) ) )).
fof(mem_c_2Eenumeral_2Esinter,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2Esinter(A_27a),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Elist_2Elist(A_27a),arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a))))) ) )).
fof(mem_c_2Eenumeral_2Esmerge,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2Esmerge(A_27a),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Elist_2Elist(A_27a),arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a))))) ) )).
fof(mem_c_2Eenumeral_2Esmerge__out,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2Esmerge__out(A_27a),arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Elist_2Elist(A_27a),arr(ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a))),ty_2Elist_2Elist(A_27a))))) ) )).
fof(mem_c_2Eenumeral_2Ezerbl,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Eenumeral_2Ezerbl(A_27a),arr(ty_2Eenumeral_2Ebl(A_27a),ty_2Eenumeral_2Ebl(A_27a))) ) )).
fof(ax_thm_2Eenumeral_2Ebt__TY__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ? [V0rep] : ( mem(V0rep,arr(ty_2Eenumeral_2Ebt(A_27a),ty_2Eind__type_2Erecspace(A_27a))) & p(ap(ap(c_2Ebool_2ETYPE__DEFINITION(ty_2Eind__type_2Erecspace(A_27a),ty_2Eenumeral_2Ebt(A_27a)),f2452(A_27a)),V0rep)) ) ) )).
fof(ax_thm_2Eenumeral_2Ebt__size__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0f] : ( mem(V0f,arr(A_27a,ty_2Enum_2Enum)) => ( ap(ap(c_2Eenumeral_2Ebt__size(A_27a),V0f),c_2Eenumeral_2Ent(A_27a)) = c_2Enum_2E0 ) ) ) & ! [V1f] : ( mem(V1f,arr(A_27a,ty_2Enum_2Enum)) => ! [V2a0] : ( mem(V2a0,ty_2Eenumeral_2Ebt(A_27a)) => ! [V3a1] : ( mem(V3a1,A_27a) => ! [V4a2] : ( mem(V4a2,ty_2Eenumeral_2Ebt(A_27a)) => ( ap(ap(c_2Eenumeral_2Ebt__size(A_27a),V1f),ap(ap(ap(c_2Eenumeral_2Enode(A_27a),V2a0),V3a1),V4a2)) = ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Eenumeral_2Ebt__size(A_27a),V1f),V2a0)),ap(ap(c_2Earithmetic_2E_2B,ap(V1f,V3a1)),ap(ap(c_2Eenumeral_2Ebt__size(A_27a),V1f),V4a2)))) ) ) ) ) ) ) ) )).
fof(conj_thm_2Eenumeral_2Edatatype__bt,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0bt] : ( mem(V0bt,arr(ty_2Eenumeral_2Ebt(A_27a),arr(arr(ty_2Eenumeral_2Ebt(A_27a),arr(A_27a,arr(ty_2Eenumeral_2Ebt(A_27a),ty_2Eenumeral_2Ebt(A_27a)))),bool))) => p(ap(c_2Ebool_2EDATATYPE(bool),ap(ap(V0bt,c_2Eenumeral_2Ent(A_27a)),c_2Eenumeral_2Enode(A_27a)))) )))).
fof(conj_thm_2Eenumeral_2Ebt__nchotomy,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0bb] : ( mem(V0bb,ty_2Eenumeral_2Ebt(A_27a)) => ( ( V0bb = c_2Eenumeral_2Ent(A_27a) ) | ? [V1b] : ( mem(V1b,ty_2Eenumeral_2Ebt(A_27a)) & ? [V2a] : ( mem(V2a,A_27a) & ? [V3b0] : ( mem(V3b0,ty_2Eenumeral_2Ebt(A_27a)) & ( V0bb = ap(ap(ap(c_2Eenumeral_2Enode(A_27a),V1b),V2a),V3b0) ) ) ) ) ) )))).
fof(conj_thm_2Eenumeral_2Ebt__Axiom,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f0] : ( mem(V0f0,A_27b) => ! [V1f1] : ( mem(V1f1,arr(A_27a,arr(ty_2Eenumeral_2Ebt(A_27a),arr(ty_2Eenumeral_2Ebt(A_27a),arr(A_27b,arr(A_27b,A_27b)))))) => ? [V2fn] : ( mem(V2fn,arr(ty_2Eenumeral_2Ebt(A_27a),A_27b)) & ( ( ap(V2fn,c_2Eenumeral_2Ent(A_27a)) = V0f0 ) & ! [V3a0] : ( mem(V3a0,ty_2Eenumeral_2Ebt(A_27a)) => ! [V4a1] : ( mem(V4a1,A_27a) => ! [V5a2] : ( mem(V5a2,ty_2Eenumeral_2Ebt(A_27a)) => ( ap(V2fn,ap(ap(ap(c_2Eenumeral_2Enode(A_27a),V3a0),V4a1),V5a2)) = ap(ap(ap(ap(ap(V1f1,V4a1),V3a0),V5a2),ap(V2fn,V3a0)),ap(V2fn,V5a2)) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Eenumeral_2Ebt__induction,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(ty_2Eenumeral_2Ebt(A_27a),bool)) => ( ( p(ap(V0P,c_2Eenumeral_2Ent(A_27a))) & ! [V1b] : ( mem(V1b,ty_2Eenumeral_2Ebt(A_27a)) => ! [V2b0] : ( mem(V2b0,ty_2Eenumeral_2Ebt(A_27a)) => ( ( p(ap(V0P,V1b)) & p(ap(V0P,V2b0)) ) => ! [V3a] : ( mem(V3a,A_27a) => p(ap(V0P,ap(ap(ap(c_2Eenumeral_2Enode(A_27a),V1b),V3a),V2b0))) ) ) ) ) ) => ! [V4b] : ( mem(V4b,ty_2Eenumeral_2Ebt(A_27a)) => p(ap(V0P,V4b)) ) ) )))).
fof(conj_thm_2Eenumeral_2Ebt__case__cong,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0v_27] : ( mem(V0v_27,A_27b) => ! [V1f_27] : ( mem(V1f_27,arr(ty_2Eenumeral_2Ebt(A_27a),arr(A_27a,arr(ty_2Eenumeral_2Ebt(A_27a),A_27b)))) => ! [V2M] : ( mem(V2M,ty_2Eenumeral_2Ebt(A_27a)) => ! [V3M_27] : ( mem(V3M_27,ty_2Eenumeral_2Ebt(A_27a)) => ! [V4v] : ( mem(V4v,A_27b) => ! [V5f] : ( mem(V5f,arr(ty_2Eenumeral_2Ebt(A_27a),arr(A_27a,arr(ty_2Eenumeral_2Ebt(A_27a),A_27b)))) => ( ( ( V2M = V3M_27 ) & ( ( ( V3M_27 = c_2Eenumeral_2Ent(A_27a) ) => ( V4v = V0v_27 ) ) & ! [V6a0] : ( mem(V6a0,ty_2Eenumeral_2Ebt(A_27a)) => ! [V7a1] : ( mem(V7a1,A_27a) => ! [V8a2] : ( mem(V8a2,ty_2Eenumeral_2Ebt(A_27a)) => ( ( V3M_27 = ap(ap(ap(c_2Eenumeral_2Enode(A_27a),V6a0),V7a1),V8a2) ) => ( ap(ap(ap(V5f,V6a0),V7a1),V8a2) = ap(ap(ap(V1f_27,V6a0),V7a1),V8a2) ) ) ) ) ) ) ) => ( ap(ap(ap(c_2Eenumeral_2Ebt__CASE(A_27a,A_27b),V2M),V4v),V5f) = ap(ap(ap(c_2Eenumeral_2Ebt__CASE(A_27a,A_27b),V3M_27),V0v_27),V1f_27) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Eenumeral_2Ebt__case__eq,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0x] : ( mem(V0x,ty_2Eenumeral_2Ebt(A_27a)) => ! [V1v] : ( mem(V1v,A_27b) => ! [V2f] : ( mem(V2f,arr(ty_2Eenumeral_2Ebt(A_27a),arr(A_27a,arr(ty_2Eenumeral_2Ebt(A_27a),A_27b)))) => ! [V3v_27] : ( mem(V3v_27,A_27b) => ( ( ap(ap(ap(c_2Eenumeral_2Ebt__CASE(A_27a,A_27b),V0x),V1v),V2f) = V3v_27 ) <=> ( ( ( V0x = c_2Eenumeral_2Ent(A_27a) ) & ( V1v = V3v_27 ) ) | ? [V4b] : ( mem(V4b,ty_2Eenumeral_2Ebt(A_27a)) & ? [V5a] : ( mem(V5a,A_27a) & ? [V6b0] : ( mem(V6b0,ty_2Eenumeral_2Ebt(A_27a)) & ( ( V0x = ap(ap(ap(c_2Eenumeral_2Enode(A_27a),V4b),V5a),V6b0) ) & ( ap(ap(ap(V2f,V4b),V5a),V6b0) = V3v_27 ) ) ) ) ) ) ) ) ) ) ))))).
fof(ax_thm_2Eenumeral_2Ebl__TY__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ? [V0rep] : ( mem(V0rep,arr(ty_2Eenumeral_2Ebl(A_27a),ty_2Eind__type_2Erecspace(ty_2Epair_2Eprod(A_27a,ty_2Eenumeral_2Ebt(A_27a))))) & p(ap(ap(c_2Ebool_2ETYPE__DEFINITION(ty_2Eind__type_2Erecspace(ty_2Epair_2Eprod(A_27a,ty_2Eenumeral_2Ebt(A_27a))),ty_2Eenumeral_2Ebl(A_27a)),f2463(A_27a)),V0rep)) ) ) )).
fof(ax_thm_2Eenumeral_2Ebl__case__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ( ( ! [V0v] : ( mem(V0v,A_27b) => ! [V1f] : ( mem(V1f,arr(ty_2Eenumeral_2Ebl(A_27a),A_27b)) => ! [V2f1] : ( mem(V2f1,arr(A_27a,arr(ty_2Eenumeral_2Ebt(A_27a),arr(ty_2Eenumeral_2Ebl(A_27a),A_27b)))) => ( ap(ap(ap(ap(c_2Eenumeral_2Ebl__CASE(A_27a,A_27b),c_2Eenumeral_2Enbl(A_27a)),V0v),V1f),V2f1) = V0v ) ) ) ) ) & ( ( ! [V3a] : ( mem(V3a,ty_2Eenumeral_2Ebl(A_27a)) => ! [V4v] : ( mem(V4v,A_27b) => ! [V5f] : ( mem(V5f,arr(ty_2Eenumeral_2Ebl(A_27a),A_27b)) => ! [V6f1] : ( mem(V6f1,arr(A_27a,arr(ty_2Eenumeral_2Ebt(A_27a),arr(ty_2Eenumeral_2Ebl(A_27a),A_27b)))) => ( ap(ap(ap(ap(c_2Eenumeral_2Ebl__CASE(A_27a,A_27b),ap(c_2Eenumeral_2Ezerbl(A_27a),V3a)),V4v),V5f),V6f1) = ap(V5f,V3a) ) ) ) ) ) ) & ! [V7a0] : ( mem(V7a0,A_27a) => ! [V8a1] : ( mem(V8a1,ty_2Eenumeral_2Ebt(A_27a)) => ! [V9a2] : ( mem(V9a2,ty_2Eenumeral_2Ebl(A_27a)) => ! [V10v] : ( mem(V10v,A_27b) => ! [V11f] : ( mem(V11f,arr(ty_2Eenumeral_2Ebl(A_27a),A_27b)) => ! [V12f1] : ( mem(V12f1,arr(A_27a,arr(ty_2Eenumeral_2Ebt(A_27a),arr(ty_2Eenumeral_2Ebl(A_27a),A_27b)))) => ( ap(ap(ap(ap(c_2Eenumeral_2Ebl__CASE(A_27a,A_27b),ap(ap(ap(c_2Eenumeral_2Eonebl(A_27a),V7a0),V8a1),V9a2)),V10v),V11f),V12f1) = ap(ap(ap(V12f1,V7a0),V8a1),V9a2) ) ) ) ) ) ) ) ) ) ) ) )).
fof(ax_thm_2Eenumeral_2Ebl__size__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0f] : ( mem(V0f,arr(A_27a,ty_2Enum_2Enum)) => ( ap(ap(c_2Eenumeral_2Ebl__size(A_27a),V0f),c_2Eenumeral_2Enbl(A_27a)) = c_2Enum_2E0 ) ) ) & ( ( ! [V1f] : ( mem(V1f,arr(A_27a,ty_2Enum_2Enum)) => ! [V2a] : ( mem(V2a,ty_2Eenumeral_2Ebl(A_27a)) => ( ap(ap(c_2Eenumeral_2Ebl__size(A_27a),V1f),ap(c_2Eenumeral_2Ezerbl(A_27a),V2a)) = ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),ap(ap(c_2Eenumeral_2Ebl__size(A_27a),V1f),V2a)) ) ) ) ) & ! [V3f] : ( mem(V3f,arr(A_27a,ty_2Enum_2Enum)) => ! [V4a0] : ( mem(V4a0,A_27a) => ! [V5a1] : ( mem(V5a1,ty_2Eenumeral_2Ebt(A_27a)) => ! [V6a2] : ( mem(V6a2,ty_2Eenumeral_2Ebl(A_27a)) => ( ap(ap(c_2Eenumeral_2Ebl__size(A_27a),V3f),ap(ap(ap(c_2Eenumeral_2Eonebl(A_27a),V4a0),V5a1),V6a2)) = ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,c_2Earithmetic_2EZERO))),ap(ap(c_2Earithmetic_2E_2B,ap(V3f,V4a0)),ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Eenumeral_2Ebt__size(A_27a),V3f),V5a1)),ap(ap(c_2Eenumeral_2Ebl__size(A_27a),V3f),V6a2)))) ) ) ) ) ) ) ) ) )).
fof(conj_thm_2Eenumeral_2Edatatype__bl,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0bl] : ( mem(V0bl,arr(ty_2Eenumeral_2Ebl(A_27a),arr(arr(ty_2Eenumeral_2Ebl(A_27a),ty_2Eenumeral_2Ebl(A_27a)),arr(arr(A_27a,arr(ty_2Eenumeral_2Ebt(A_27a),arr(ty_2Eenumeral_2Ebl(A_27a),ty_2Eenumeral_2Ebl(A_27a)))),bool)))) => p(ap(c_2Ebool_2EDATATYPE(bool),ap(ap(ap(V0bl,c_2Eenumeral_2Enbl(A_27a)),c_2Eenumeral_2Ezerbl(A_27a)),c_2Eenumeral_2Eonebl(A_27a)))) )))).
fof(conj_thm_2Eenumeral_2Ebl__11,lemma,( ! [A_27a]: ( ne(A_27a) => ( ( ! [V0a] : ( mem(V0a,ty_2Eenumeral_2Ebl(A_27a)) => ! [V1a_27] : ( mem(V1a_27,ty_2Eenumeral_2Ebl(A_27a)) => ( ( ap(c_2Eenumeral_2Ezerbl(A_27a),V0a) = ap(c_2Eenumeral_2Ezerbl(A_27a),V1a_27) ) <=> ( V0a = V1a_27 ) ) ) ) ) & ! [V2a0] : ( mem(V2a0,A_27a) => ! [V3a1] : ( mem(V3a1,ty_2Eenumeral_2Ebt(A_27a)) => ! [V4a2] : ( mem(V4a2,ty_2Eenumeral_2Ebl(A_27a)) => ! [V5a0_27] : ( mem(V5a0_27,A_27a) => ! [V6a1_27] : ( mem(V6a1_27,ty_2Eenumeral_2Ebt(A_27a)) => ! [V7a2_27] : ( mem(V7a2_27,ty_2Eenumeral_2Ebl(A_27a)) => ( ( ap(ap(ap(c_2Eenumeral_2Eonebl(A_27a),V2a0),V3a1),V4a2) = ap(ap(ap(c_2Eenumeral_2Eonebl(A_27a),V5a0_27),V6a1_27),V7a2_27) ) <=> ( ( V2a0 = V5a0_27 ) & ( ( V3a1 = V6a1_27 ) & ( V4a2 = V7a2_27 ) ) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Eenumeral_2Ebl__distinct,lemma,( ! [A_27a]: ( ne(A_27a) => ( ( ! [V0a] : ( mem(V0a,ty_2Eenumeral_2Ebl(A_27a)) => ( ~~ ( c_2Eenumeral_2Enbl(A_27a) = ap(c_2Eenumeral_2Ezerbl(A_27a),V0a) ) ) ) ) & ( ( ! [V1a2] : ( mem(V1a2,ty_2Eenumeral_2Ebl(A_27a)) => ! [V2a1] : ( mem(V2a1,ty_2Eenumeral_2Ebt(A_27a)) => ! [V3a0] : ( mem(V3a0,A_27a) => ( ~~ ( c_2Eenumeral_2Enbl(A_27a) = ap(ap(ap(c_2Eenumeral_2Eonebl(A_27a),V3a0),V2a1),V1a2) ) ) ) ) ) ) & ! [V4a2] : ( mem(V4a2,ty_2Eenumeral_2Ebl(A_27a)) => ! [V5a1] : ( mem(V5a1,ty_2Eenumeral_2Ebt(A_27a)) => ! [V6a0] : ( mem(V6a0,A_27a) => ! [V7a] : ( mem(V7a,ty_2Eenumeral_2Ebl(A_27a)) => ( ~~ ( ap(c_2Eenumeral_2Ezerbl(A_27a),V7a) = ap(ap(ap(c_2Eenumeral_2Eonebl(A_27a),V6a0),V5a1),V4a2) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Eenumeral_2Ebl__nchotomy,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0bb] : ( mem(V0bb,ty_2Eenumeral_2Ebl(A_27a)) => ( ( V0bb = c_2Eenumeral_2Enbl(A_27a) ) | ( ( ? [V1b] : ( mem(V1b,ty_2Eenumeral_2Ebl(A_27a)) & ( V0bb = ap(c_2Eenumeral_2Ezerbl(A_27a),V1b) ) ) ) | ? [V2a] : ( mem(V2a,A_27a) & ? [V3b0] : ( mem(V3b0,ty_2Eenumeral_2Ebt(A_27a)) & ? [V4b] : ( mem(V4b,ty_2Eenumeral_2Ebl(A_27a)) & ( V0bb = ap(ap(ap(c_2Eenumeral_2Eonebl(A_27a),V2a),V3b0),V4b) ) ) ) ) ) ) )))).
fof(conj_thm_2Eenumeral_2Ebl__Axiom,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f0] : ( mem(V0f0,A_27b) => ! [V1f1] : ( mem(V1f1,arr(ty_2Eenumeral_2Ebl(A_27a),arr(A_27b,A_27b))) => ! [V2f2] : ( mem(V2f2,arr(A_27a,arr(ty_2Eenumeral_2Ebt(A_27a),arr(ty_2Eenumeral_2Ebl(A_27a),arr(A_27b,A_27b))))) => ? [V3fn] : ( mem(V3fn,arr(ty_2Eenumeral_2Ebl(A_27a),A_27b)) & ( ( ap(V3fn,c_2Eenumeral_2Enbl(A_27a)) = V0f0 ) & ( ( ! [V4a] : ( mem(V4a,ty_2Eenumeral_2Ebl(A_27a)) => ( ap(V3fn,ap(c_2Eenumeral_2Ezerbl(A_27a),V4a)) = ap(ap(V1f1,V4a),ap(V3fn,V4a)) ) ) ) & ! [V5a0] : ( mem(V5a0,A_27a) => ! [V6a1] : ( mem(V6a1,ty_2Eenumeral_2Ebt(A_27a)) => ! [V7a2] : ( mem(V7a2,ty_2Eenumeral_2Ebl(A_27a)) => ( ap(V3fn,ap(ap(ap(c_2Eenumeral_2Eonebl(A_27a),V5a0),V6a1),V7a2)) = ap(ap(ap(ap(V2f2,V5a0),V6a1),V7a2),ap(V3fn,V7a2)) ) ) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Eenumeral_2Ebl__induction,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(ty_2Eenumeral_2Ebl(A_27a),bool)) => ( ( p(ap(V0P,c_2Eenumeral_2Enbl(A_27a))) & ( ( ! [V1b] : ( mem(V1b,ty_2Eenumeral_2Ebl(A_27a)) => ( p(ap(V0P,V1b)) => p(ap(V0P,ap(c_2Eenumeral_2Ezerbl(A_27a),V1b))) ) ) ) & ! [V2b] : ( mem(V2b,ty_2Eenumeral_2Ebl(A_27a)) => ( p(ap(V0P,V2b)) => ! [V3b0] : ( mem(V3b0,ty_2Eenumeral_2Ebt(A_27a)) => ! [V4a] : ( mem(V4a,A_27a) => p(ap(V0P,ap(ap(ap(c_2Eenumeral_2Eonebl(A_27a),V4a),V3b0),V2b))) ) ) ) ) ) ) => ! [V5b] : ( mem(V5b,ty_2Eenumeral_2Ebl(A_27a)) => p(ap(V0P,V5b)) ) ) )))).
fof(conj_thm_2Eenumeral_2Ebl__case__cong,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0v_27] : ( mem(V0v_27,A_27b) => ! [V1f_27] : ( mem(V1f_27,arr(ty_2Eenumeral_2Ebl(A_27a),A_27b)) => ! [V2f1_27] : ( mem(V2f1_27,arr(A_27a,arr(ty_2Eenumeral_2Ebt(A_27a),arr(ty_2Eenumeral_2Ebl(A_27a),A_27b)))) => ! [V3M] : ( mem(V3M,ty_2Eenumeral_2Ebl(A_27a)) => ! [V4M_27] : ( mem(V4M_27,ty_2Eenumeral_2Ebl(A_27a)) => ! [V5v] : ( mem(V5v,A_27b) => ! [V6f] : ( mem(V6f,arr(ty_2Eenumeral_2Ebl(A_27a),A_27b)) => ! [V7f1] : ( mem(V7f1,arr(A_27a,arr(ty_2Eenumeral_2Ebt(A_27a),arr(ty_2Eenumeral_2Ebl(A_27a),A_27b)))) => ( ( ( V3M = V4M_27 ) & ( ( ( V4M_27 = c_2Eenumeral_2Enbl(A_27a) ) => ( V5v = V0v_27 ) ) & ( ( ! [V8a] : ( mem(V8a,ty_2Eenumeral_2Ebl(A_27a)) => ( ( V4M_27 = ap(c_2Eenumeral_2Ezerbl(A_27a),V8a) ) => ( ap(V6f,V8a) = ap(V1f_27,V8a) ) ) ) ) & ! [V9a0] : ( mem(V9a0,A_27a) => ! [V10a1] : ( mem(V10a1,ty_2Eenumeral_2Ebt(A_27a)) => ! [V11a2] : ( mem(V11a2,ty_2Eenumeral_2Ebl(A_27a)) => ( ( V4M_27 = ap(ap(ap(c_2Eenumeral_2Eonebl(A_27a),V9a0),V10a1),V11a2) ) => ( ap(ap(ap(V7f1,V9a0),V10a1),V11a2) = ap(ap(ap(V2f1_27,V9a0),V10a1),V11a2) ) ) ) ) ) ) ) ) => ( ap(ap(ap(ap(c_2Eenumeral_2Ebl__CASE(A_27a,A_27b),V3M),V5v),V6f),V7f1) = ap(ap(ap(ap(c_2Eenumeral_2Ebl__CASE(A_27a,A_27b),V4M_27),V0v_27),V1f_27),V2f1_27) ) ) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Eenumeral_2Ebl__case__eq,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0x] : ( mem(V0x,ty_2Eenumeral_2Ebl(A_27a)) => ! [V1v] : ( mem(V1v,A_27b) => ! [V2f] : ( mem(V2f,arr(ty_2Eenumeral_2Ebl(A_27a),A_27b)) => ! [V3f1] : ( mem(V3f1,arr(A_27a,arr(ty_2Eenumeral_2Ebt(A_27a),arr(ty_2Eenumeral_2Ebl(A_27a),A_27b)))) => ! [V4v_27] : ( mem(V4v_27,A_27b) => ( ( ap(ap(ap(ap(c_2Eenumeral_2Ebl__CASE(A_27a,A_27b),V0x),V1v),V2f),V3f1) = V4v_27 ) <=> ( ( ( V0x = c_2Eenumeral_2Enbl(A_27a) ) & ( V1v = V4v_27 ) ) | ( ( ? [V5b] : ( mem(V5b,ty_2Eenumeral_2Ebl(A_27a)) & ( ( V0x = ap(c_2Eenumeral_2Ezerbl(A_27a),V5b) ) & ( ap(V2f,V5b) = V4v_27 ) ) ) ) | ? [V6a] : ( mem(V6a,A_27a) & ? [V7b0] : ( mem(V7b0,ty_2Eenumeral_2Ebt(A_27a)) & ? [V8b] : ( mem(V8b,ty_2Eenumeral_2Ebl(A_27a)) & ( ( V0x = ap(ap(ap(c_2Eenumeral_2Eonebl(A_27a),V6a),V7b0),V8b) ) & ( ap(ap(ap(V3f1,V6a),V7b0),V8b) = V4v_27 ) ) ) ) ) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Eenumeral_2Ebt__11,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a0] : ( mem(V0a0,ty_2Eenumeral_2Ebt(A_27a)) => ! [V1a1] : ( mem(V1a1,A_27a) => ! [V2a2] : ( mem(V2a2,ty_2Eenumeral_2Ebt(A_27a)) => ! [V3a0_27] : ( mem(V3a0_27,ty_2Eenumeral_2Ebt(A_27a)) => ! [V4a1_27] : ( mem(V4a1_27,A_27a) => ! [V5a2_27] : ( mem(V5a2_27,ty_2Eenumeral_2Ebt(A_27a)) => ( ( ap(ap(ap(c_2Eenumeral_2Enode(A_27a),V0a0),V1a1),V2a2) = ap(ap(ap(c_2Eenumeral_2Enode(A_27a),V3a0_27),V4a1_27),V5a2_27) ) <=> ( ( V0a0 = V3a0_27 ) & ( ( V1a1 = V4a1_27 ) & ( V2a2 = V5a2_27 ) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Eenumeral_2Ebt__distinct,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a2] : ( mem(V0a2,ty_2Eenumeral_2Ebt(A_27a)) => ! [V1a1] : ( mem(V1a1,A_27a) => ! [V2a0] : ( mem(V2a0,ty_2Eenumeral_2Ebt(A_27a)) => ( ~~ ( c_2Eenumeral_2Ent(A_27a) = ap(ap(ap(c_2Eenumeral_2Enode(A_27a),V2a0),V1a1),V0a2) ) ) ) ) )))).
fof(conj_thm_2Eenumeral_2Ebt__case__def,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ( ( ! [V0v] : ( mem(V0v,A_27b) => ! [V1f] : ( mem(V1f,arr(ty_2Eenumeral_2Ebt(A_27a),arr(A_27a,arr(ty_2Eenumeral_2Ebt(A_27a),A_27b)))) => ( ap(ap(ap(c_2Eenumeral_2Ebt__CASE(A_27a,A_27b),c_2Eenumeral_2Ent(A_27a)),V0v),V1f) = V0v ) ) ) ) & ! [V2a0] : ( mem(V2a0,ty_2Eenumeral_2Ebt(A_27a)) => ! [V3a1] : ( mem(V3a1,A_27a) => ! [V4a2] : ( mem(V4a2,ty_2Eenumeral_2Ebt(A_27a)) => ! [V5v] : ( mem(V5v,A_27b) => ! [V6f] : ( mem(V6f,arr(ty_2Eenumeral_2Ebt(A_27a),arr(A_27a,arr(ty_2Eenumeral_2Ebt(A_27a),A_27b)))) => ( ap(ap(ap(c_2Eenumeral_2Ebt__CASE(A_27a,A_27b),ap(ap(ap(c_2Eenumeral_2Enode(A_27a),V2a0),V3a1),V4a2)),V5v),V6f) = ap(ap(ap(V6f,V2a0),V3a1),V4a2) ) ) ) ) ) ) ))))).
fof(ax_thm_2Eenumeral_2EBL__ACCUM,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0a] : ( mem(V0a,A_27a) => ! [V1ac] : ( mem(V1ac,ty_2Eenumeral_2Ebt(A_27a)) => ( ap(ap(ap(c_2Eenumeral_2EBL__ACCUM(A_27a),V0a),V1ac),c_2Eenumeral_2Enbl(A_27a)) = ap(ap(ap(c_2Eenumeral_2Eonebl(A_27a),V0a),V1ac),c_2Eenumeral_2Enbl(A_27a)) ) ) ) ) & ( ( ! [V2a] : ( mem(V2a,A_27a) => ! [V3ac] : ( mem(V3ac,ty_2Eenumeral_2Ebt(A_27a)) => ! [V4bl] : ( mem(V4bl,ty_2Eenumeral_2Ebl(A_27a)) => ( ap(ap(ap(c_2Eenumeral_2EBL__ACCUM(A_27a),V2a),V3ac),ap(c_2Eenumeral_2Ezerbl(A_27a),V4bl)) = ap(ap(ap(c_2Eenumeral_2Eonebl(A_27a),V2a),V3ac),V4bl) ) ) ) ) ) & ! [V5a] : ( mem(V5a,A_27a) => ! [V6ac] : ( mem(V6ac,ty_2Eenumeral_2Ebt(A_27a)) => ! [V7r] : ( mem(V7r,A_27a) => ! [V8rft] : ( mem(V8rft,ty_2Eenumeral_2Ebt(A_27a)) => ! [V9bl] : ( mem(V9bl,ty_2Eenumeral_2Ebl(A_27a)) => ( ap(ap(ap(c_2Eenumeral_2EBL__ACCUM(A_27a),V5a),V6ac),ap(ap(ap(c_2Eenumeral_2Eonebl(A_27a),V7r),V8rft),V9bl)) = ap(c_2Eenumeral_2Ezerbl(A_27a),ap(ap(ap(c_2Eenumeral_2EBL__ACCUM(A_27a),V5a),ap(ap(ap(c_2Eenumeral_2Enode(A_27a),V6ac),V7r),V8rft)),V9bl)) ) ) ) ) ) ) ) ) ) )).
fof(ax_thm_2Eenumeral_2EBL__CONS,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0a] : ( mem(V0a,A_27a) => ! [V1bl] : ( mem(V1bl,ty_2Eenumeral_2Ebl(A_27a)) => ( ap(ap(c_2Eenumeral_2EBL__CONS(A_27a),V0a),V1bl) = ap(ap(ap(c_2Eenumeral_2EBL__ACCUM(A_27a),V0a),c_2Eenumeral_2Ent(A_27a)),V1bl) ) ) ) ) )).
fof(ax_thm_2Eenumeral_2Elist__to__bl,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ap(c_2Eenumeral_2Elist__to__bl(A_27a),c_2Elist_2ENIL(A_27a)) = c_2Eenumeral_2Enbl(A_27a) ) & ! [V0a] : ( mem(V0a,A_27a) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ( ap(c_2Eenumeral_2Elist__to__bl(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V0a),V1l)) = ap(ap(c_2Eenumeral_2EBL__CONS(A_27a),V0a),ap(c_2Eenumeral_2Elist__to__bl(A_27a),V1l)) ) ) ) ) ) )).
fof(ax_thm_2Eenumeral_2Ebt__to__list,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ap(c_2Eenumeral_2Ebt__to__list(A_27a),c_2Eenumeral_2Ent(A_27a)) = c_2Elist_2ENIL(A_27a) ) & ! [V0l] : ( mem(V0l,ty_2Eenumeral_2Ebt(A_27a)) => ! [V1x] : ( mem(V1x,A_27a) => ! [V2r] : ( mem(V2r,ty_2Eenumeral_2Ebt(A_27a)) => ( ap(c_2Eenumeral_2Ebt__to__list(A_27a),ap(ap(ap(c_2Eenumeral_2Enode(A_27a),V0l),V1x),V2r)) = ap(ap(c_2Elist_2EAPPEND(A_27a),ap(ap(c_2Elist_2EAPPEND(A_27a),ap(c_2Eenumeral_2Ebt__to__list(A_27a),V0l)),ap(ap(c_2Elist_2ECONS(A_27a),V1x),c_2Elist_2ENIL(A_27a)))),ap(c_2Eenumeral_2Ebt__to__list(A_27a),V2r)) ) ) ) ) ) ) )).
fof(ax_thm_2Eenumeral_2Ebt__to__list__ac,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0m] : ( mem(V0m,ty_2Elist_2Elist(A_27a)) => ( ap(ap(c_2Eenumeral_2Ebt__to__list__ac(A_27a),c_2Eenumeral_2Ent(A_27a)),V0m) = V0m ) ) ) & ! [V1l] : ( mem(V1l,ty_2Eenumeral_2Ebt(A_27a)) => ! [V2x] : ( mem(V2x,A_27a) => ! [V3r] : ( mem(V3r,ty_2Eenumeral_2Ebt(A_27a)) => ! [V4m] : ( mem(V4m,ty_2Elist_2Elist(A_27a)) => ( ap(ap(c_2Eenumeral_2Ebt__to__list__ac(A_27a),ap(ap(ap(c_2Eenumeral_2Enode(A_27a),V1l),V2x),V3r)),V4m) = ap(ap(c_2Eenumeral_2Ebt__to__list__ac(A_27a),V1l),ap(ap(c_2Elist_2ECONS(A_27a),V2x),ap(ap(c_2Eenumeral_2Ebt__to__list__ac(A_27a),V3r),V4m))) ) ) ) ) ) ) ) )).
fof(conj_thm_2Eenumeral_2Ebt__to__list__thm,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0t] : ( mem(V0t,ty_2Eenumeral_2Ebt(A_27a)) => ( ap(c_2Eenumeral_2Ebt__to__list(A_27a),V0t) = ap(ap(c_2Eenumeral_2Ebt__to__list__ac(A_27a),V0t),c_2Elist_2ENIL(A_27a)) ) )))).
fof(ax_thm_2Eenumeral_2Ebt__rev,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0bl] : ( mem(V0bl,ty_2Eenumeral_2Ebl(A_27a)) => ( ap(ap(c_2Eenumeral_2Ebt__rev(A_27a),c_2Eenumeral_2Ent(A_27a)),V0bl) = V0bl ) ) ) & ! [V1lft] : ( mem(V1lft,ty_2Eenumeral_2Ebt(A_27a)) => ! [V2r] : ( mem(V2r,A_27a) => ! [V3rft] : ( mem(V3rft,ty_2Eenumeral_2Ebt(A_27a)) => ! [V4bl] : ( mem(V4bl,ty_2Eenumeral_2Ebl(A_27a)) => ( ap(ap(c_2Eenumeral_2Ebt__rev(A_27a),ap(ap(ap(c_2Eenumeral_2Enode(A_27a),V1lft),V2r),V3rft)),V4bl) = ap(ap(c_2Eenumeral_2Ebt__rev(A_27a),V1lft),ap(ap(ap(c_2Eenumeral_2Eonebl(A_27a),V2r),V3rft),V4bl)) ) ) ) ) ) ) ) )).
fof(ax_thm_2Eenumeral_2EK2,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0a] : ( mem(V0a,A_27a) => ( ap(c_2Eenumeral_2EK2(A_27a),V0a) = ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,c_2Earithmetic_2EZERO)) ) ) ) )).
fof(ax_thm_2Eenumeral_2Ebl__rev,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0ft] : ( mem(V0ft,ty_2Eenumeral_2Ebt(A_27a)) => ( ap(ap(c_2Eenumeral_2Ebl__rev(A_27a),V0ft),c_2Eenumeral_2Enbl(A_27a)) = V0ft ) ) ) & ( ( ! [V1ft] : ( mem(V1ft,ty_2Eenumeral_2Ebt(A_27a)) => ! [V2b] : ( mem(V2b,ty_2Eenumeral_2Ebl(A_27a)) => ( ap(ap(c_2Eenumeral_2Ebl__rev(A_27a),V1ft),ap(c_2Eenumeral_2Ezerbl(A_27a),V2b)) = ap(ap(c_2Eenumeral_2Ebl__rev(A_27a),V1ft),V2b) ) ) ) ) & ! [V3ft] : ( mem(V3ft,ty_2Eenumeral_2Ebt(A_27a)) => ! [V4a] : ( mem(V4a,A_27a) => ! [V5f] : ( mem(V5f,ty_2Eenumeral_2Ebt(A_27a)) => ! [V6b] : ( mem(V6b,ty_2Eenumeral_2Ebl(A_27a)) => ( ap(ap(c_2Eenumeral_2Ebl__rev(A_27a),V3ft),ap(ap(ap(c_2Eenumeral_2Eonebl(A_27a),V4a),V5f),V6b)) = ap(ap(c_2Eenumeral_2Ebl__rev(A_27a),ap(ap(ap(c_2Eenumeral_2Enode(A_27a),V3ft),V4a),V5f)),V6b) ) ) ) ) ) ) ) ) )).
fof(ax_thm_2Eenumeral_2Ebl__to__bt,axiom,( ! [A_27a] : ( ne(A_27a) => ( c_2Eenumeral_2Ebl__to__bt(A_27a) = ap(c_2Eenumeral_2Ebl__rev(A_27a),c_2Eenumeral_2Ent(A_27a)) ) ) )).
fof(ax_thm_2Eenumeral_2Ebt__to__bl,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0t] : ( mem(V0t,ty_2Eenumeral_2Ebt(A_27a)) => ( ap(c_2Eenumeral_2Ebt__to__bl(A_27a),V0t) = ap(ap(c_2Eenumeral_2Ebt__rev(A_27a),V0t),c_2Eenumeral_2Enbl(A_27a)) ) ) ) )).
fof(ax_thm_2Eenumeral_2Elist__to__bt,axiom,( ! [A_27c] : ( ne(A_27c) => ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27c)) => ( ap(c_2Eenumeral_2Elist__to__bt(A_27c),V0l) = ap(c_2Eenumeral_2Ebl__to__bt(A_27c),ap(c_2Eenumeral_2Elist__to__bl(A_27c),V0l)) ) ) ) )).
fof(ax_thm_2Eenumeral_2EOL,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( p(ap(ap(c_2Eenumeral_2EOL(A_27a),V0cmp),c_2Elist_2ENIL(A_27a))) <=> $true ) ) ) & ! [V1cmp] : ( mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V2a] : ( mem(V2a,A_27a) => ! [V3l] : ( mem(V3l,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Eenumeral_2EOL(A_27a),V1cmp),ap(ap(c_2Elist_2ECONS(A_27a),V2a),V3l))) <=> ( p(ap(ap(c_2Eenumeral_2EOL(A_27a),V1cmp),V3l)) & ! [V4p] : ( mem(V4p,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V4p),ap(c_2Elist_2ELIST__TO__SET(A_27a),V3l))) => ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V1cmp),V2a),V4p) = c_2EternaryComparisons_2ELESS ) ) ) ) ) ) ) ) ) ) )).
fof(conj_thm_2Eenumeral_2Esmerge__ind,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Elist_2Elist(A_27a),arr(ty_2Elist_2Elist(A_27a),bool)))) => ( ( ( ! [V1cmp] : ( mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => p(ap(ap(ap(V0P,V1cmp),c_2Elist_2ENIL(A_27a)),c_2Elist_2ENIL(A_27a))) ) ) & ( ( ! [V2cmp] : ( mem(V2cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V3x] : ( mem(V3x,A_27a) => ! [V4l] : ( mem(V4l,ty_2Elist_2Elist(A_27a)) => p(ap(ap(ap(V0P,V2cmp),ap(ap(c_2Elist_2ECONS(A_27a),V3x),V4l)),c_2Elist_2ENIL(A_27a))) ) ) ) ) & ( ( ! [V5cmp] : ( mem(V5cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V6y] : ( mem(V6y,A_27a) => ! [V7m] : ( mem(V7m,ty_2Elist_2Elist(A_27a)) => p(ap(ap(ap(V0P,V5cmp),c_2Elist_2ENIL(A_27a)),ap(ap(c_2Elist_2ECONS(A_27a),V6y),V7m))) ) ) ) ) & ! [V8cmp] : ( mem(V8cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V9x] : ( mem(V9x,A_27a) => ! [V10l] : ( mem(V10l,ty_2Elist_2Elist(A_27a)) => ! [V11y] : ( mem(V11y,A_27a) => ! [V12m] : ( mem(V12m,ty_2Elist_2Elist(A_27a)) => ( ( ( ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V8cmp),V9x),V11y) = c_2EternaryComparisons_2EEQUAL ) => p(ap(ap(ap(V0P,V8cmp),V10l),V12m)) ) & ( ( ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V8cmp),V9x),V11y) = c_2EternaryComparisons_2EGREATER ) => p(ap(ap(ap(V0P,V8cmp),ap(ap(c_2Elist_2ECONS(A_27a),V9x),V10l)),V12m)) ) & ( ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V8cmp),V9x),V11y) = c_2EternaryComparisons_2ELESS ) => p(ap(ap(ap(V0P,V8cmp),V10l),ap(ap(c_2Elist_2ECONS(A_27a),V11y),V12m))) ) ) ) => p(ap(ap(ap(V0P,V8cmp),ap(ap(c_2Elist_2ECONS(A_27a),V9x),V10l)),ap(ap(c_2Elist_2ECONS(A_27a),V11y),V12m))) ) ) ) ) ) ) ) ) ) => ! [V13v] : ( mem(V13v,ty_2Etoto_2Etoto(A_27a)) => ! [V14v1] : ( mem(V14v1,ty_2Elist_2Elist(A_27a)) => ! [V15v2] : ( mem(V15v2,ty_2Elist_2Elist(A_27a)) => p(ap(ap(ap(V0P,V13v),V14v1),V15v2)) ) ) ) ) )))).
fof(conj_thm_2Eenumeral_2Esmerge,lemma,( ! [A_27a]: ( ne(A_27a) => ( ( ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(ap(c_2Eenumeral_2Esmerge(A_27a),V0cmp),c_2Elist_2ENIL(A_27a)),c_2Elist_2ENIL(A_27a)) = c_2Elist_2ENIL(A_27a) ) ) ) & ( ( ! [V1x] : ( mem(V1x,A_27a) => ! [V2l] : ( mem(V2l,ty_2Elist_2Elist(A_27a)) => ! [V3cmp] : ( mem(V3cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(ap(c_2Eenumeral_2Esmerge(A_27a),V3cmp),ap(ap(c_2Elist_2ECONS(A_27a),V1x),V2l)),c_2Elist_2ENIL(A_27a)) = ap(ap(c_2Elist_2ECONS(A_27a),V1x),V2l) ) ) ) ) ) & ( ( ! [V4y] : ( mem(V4y,A_27a) => ! [V5m] : ( mem(V5m,ty_2Elist_2Elist(A_27a)) => ! [V6cmp] : ( mem(V6cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(ap(c_2Eenumeral_2Esmerge(A_27a),V6cmp),c_2Elist_2ENIL(A_27a)),ap(ap(c_2Elist_2ECONS(A_27a),V4y),V5m)) = ap(ap(c_2Elist_2ECONS(A_27a),V4y),V5m) ) ) ) ) ) & ! [V7y] : ( mem(V7y,A_27a) => ! [V8x] : ( mem(V8x,A_27a) => ! [V9m] : ( mem(V9m,ty_2Elist_2Elist(A_27a)) => ! [V10l] : ( mem(V10l,ty_2Elist_2Elist(A_27a)) => ! [V11cmp] : ( mem(V11cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(ap(c_2Eenumeral_2Esmerge(A_27a),V11cmp),ap(ap(c_2Elist_2ECONS(A_27a),V8x),V10l)),ap(ap(c_2Elist_2ECONS(A_27a),V7y),V9m)) = ap(ap(ap(ap(c_2EternaryComparisons_2Eordering__CASE(ty_2Elist_2Elist(A_27a)),ap(ap(ap(c_2Etoto_2Eapto(A_27a),V11cmp),V8x),V7y)),ap(ap(c_2Elist_2ECONS(A_27a),V8x),ap(ap(ap(c_2Eenumeral_2Esmerge(A_27a),V11cmp),V10l),ap(ap(c_2Elist_2ECONS(A_27a),V7y),V9m)))),ap(ap(c_2Elist_2ECONS(A_27a),V8x),ap(ap(ap(c_2Eenumeral_2Esmerge(A_27a),V11cmp),V10l),V9m))),ap(ap(c_2Elist_2ECONS(A_27a),V7y),ap(ap(ap(c_2Eenumeral_2Esmerge(A_27a),V11cmp),ap(ap(c_2Elist_2ECONS(A_27a),V8x),V10l)),V9m))) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Eenumeral_2Esmerge__nil,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ( ( ap(ap(ap(c_2Eenumeral_2Esmerge(A_27a),V0cmp),V1l),c_2Elist_2ENIL(A_27a)) = V1l ) & ( ap(ap(ap(c_2Eenumeral_2Esmerge(A_27a),V0cmp),c_2Elist_2ENIL(A_27a)),V1l) = V1l ) ) ) )))).
fof(conj_thm_2Eenumeral_2Esmerge__OL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ! [V2m] : ( mem(V2m,ty_2Elist_2Elist(A_27a)) => ( ( p(ap(ap(c_2Eenumeral_2EOL(A_27a),V0cmp),V1l)) & p(ap(ap(c_2Eenumeral_2EOL(A_27a),V0cmp),V2m)) ) => p(ap(ap(c_2Eenumeral_2EOL(A_27a),V0cmp),ap(ap(ap(c_2Eenumeral_2Esmerge(A_27a),V0cmp),V1l),V2m))) ) ) ) )))).
fof(conj_thm_2Eenumeral_2EOL__sublists__ind,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a))),bool))) => ( ( ( ! [V1cmp] : ( mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => p(ap(ap(V0P,V1cmp),c_2Elist_2ENIL(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a))))) ) ) & ( ( ! [V2cmp] : ( mem(V2cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V3lol] : ( mem(V3lol,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a)))) => ( p(ap(ap(V0P,V2cmp),V3lol)) => p(ap(ap(V0P,V2cmp),ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a))),c_2Eoption_2ENONE(ty_2Elist_2Elist(A_27a))),V3lol))) ) ) ) ) & ! [V4cmp] : ( mem(V4cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V5m] : ( mem(V5m,ty_2Elist_2Elist(A_27a)) => ! [V6lol] : ( mem(V6lol,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a)))) => ( p(ap(ap(V0P,V4cmp),V6lol)) => p(ap(ap(V0P,V4cmp),ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a))),ap(c_2Eoption_2ESOME(ty_2Elist_2Elist(A_27a)),V5m)),V6lol))) ) ) ) ) ) ) => ! [V7v] : ( mem(V7v,ty_2Etoto_2Etoto(A_27a)) => ! [V8v1] : ( mem(V8v1,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a)))) => p(ap(ap(V0P,V7v),V8v1)) ) ) ) )))).
fof(conj_thm_2Eenumeral_2EOL__sublists,lemma,( ! [A_27a]: ( ne(A_27a) => ( ( ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( p(ap(ap(c_2Eenumeral_2EOL__sublists(A_27a),V0cmp),c_2Elist_2ENIL(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a))))) <=> $true ) ) ) & ( ( ! [V1lol] : ( mem(V1lol,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a)))) => ! [V2cmp] : ( mem(V2cmp,ty_2Etoto_2Etoto(A_27a)) => ( p(ap(ap(c_2Eenumeral_2EOL__sublists(A_27a),V2cmp),ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a))),c_2Eoption_2ENONE(ty_2Elist_2Elist(A_27a))),V1lol))) <=> p(ap(ap(c_2Eenumeral_2EOL__sublists(A_27a),V2cmp),V1lol)) ) ) ) ) & ! [V3m] : ( mem(V3m,ty_2Elist_2Elist(A_27a)) => ! [V4lol] : ( mem(V4lol,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a)))) => ! [V5cmp] : ( mem(V5cmp,ty_2Etoto_2Etoto(A_27a)) => ( p(ap(ap(c_2Eenumeral_2EOL__sublists(A_27a),V5cmp),ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a))),ap(c_2Eoption_2ESOME(ty_2Elist_2Elist(A_27a)),V3m)),V4lol))) <=> ( p(ap(ap(c_2Eenumeral_2EOL(A_27a),V5cmp),V3m)) & p(ap(ap(c_2Eenumeral_2EOL__sublists(A_27a),V5cmp),V4lol)) ) ) ) ) ) ) )))).
fof(ax_thm_2Eenumeral_2Elol__set__primitive,axiom,( ! [A_27a] : ( ne(A_27a) => ( c_2Eenumeral_2Elol__set(A_27a) = ap(ap(c_2Erelation_2EWFREC(ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a))),arr(A_27a,bool)),ap(c_2Emin_2E_40(arr(ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a))),arr(ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a))),bool))),f2467(A_27a))),f2472(A_27a)) ) ) )).
fof(conj_thm_2Eenumeral_2Elol__set__ind,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a))),bool)) => ( ( p(ap(V0P,c_2Elist_2ENIL(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a))))) & ( ( ! [V1lol] : ( mem(V1lol,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a)))) => ( p(ap(V0P,V1lol)) => p(ap(V0P,ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a))),c_2Eoption_2ENONE(ty_2Elist_2Elist(A_27a))),V1lol))) ) ) ) & ! [V2m] : ( mem(V2m,ty_2Elist_2Elist(A_27a)) => ! [V3lol] : ( mem(V3lol,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a)))) => ( p(ap(V0P,V3lol)) => p(ap(V0P,ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a))),ap(c_2Eoption_2ESOME(ty_2Elist_2Elist(A_27a)),V2m)),V3lol))) ) ) ) ) ) => ! [V4v] : ( mem(V4v,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a)))) => p(ap(V0P,V4v)) ) ) )))).
fof(conj_thm_2Eenumeral_2Elol__set,lemma,( ! [A_27a]: ( ne(A_27a) => ( ( ap(c_2Eenumeral_2Elol__set(A_27a),c_2Elist_2ENIL(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a)))) = c_2Epred__set_2EEMPTY(A_27a) ) & ( ( ! [V0lol] : ( mem(V0lol,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a)))) => ( ap(c_2Eenumeral_2Elol__set(A_27a),ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a))),c_2Eoption_2ENONE(ty_2Elist_2Elist(A_27a))),V0lol)) = ap(c_2Eenumeral_2Elol__set(A_27a),V0lol) ) ) ) & ! [V1m] : ( mem(V1m,ty_2Elist_2Elist(A_27a)) => ! [V2lol] : ( mem(V2lol,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a)))) => ( ap(c_2Eenumeral_2Elol__set(A_27a),ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a))),ap(c_2Eoption_2ESOME(ty_2Elist_2Elist(A_27a)),V1m)),V2lol)) = ap(ap(c_2Epred__set_2EUNION(A_27a),ap(c_2Elist_2ELIST__TO__SET(A_27a),V1m)),ap(c_2Eenumeral_2Elol__set(A_27a),V2lol)) ) ) ) ) )))).
fof(conj_thm_2Eenumeral_2Eincr__smerge__ind,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Elist_2Elist(A_27a),arr(ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a))),bool)))) => ( ( ( ! [V1cmp] : ( mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V2l] : ( mem(V2l,ty_2Elist_2Elist(A_27a)) => p(ap(ap(ap(V0P,V1cmp),V2l),c_2Elist_2ENIL(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a))))) ) ) ) & ( ( ! [V3cmp] : ( mem(V3cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V4l] : ( mem(V4l,ty_2Elist_2Elist(A_27a)) => ! [V5lol] : ( mem(V5lol,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a)))) => p(ap(ap(ap(V0P,V3cmp),V4l),ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a))),c_2Eoption_2ENONE(ty_2Elist_2Elist(A_27a))),V5lol))) ) ) ) ) & ! [V6cmp] : ( mem(V6cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V7l] : ( mem(V7l,ty_2Elist_2Elist(A_27a)) => ! [V8m] : ( mem(V8m,ty_2Elist_2Elist(A_27a)) => ! [V9lol] : ( mem(V9lol,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a)))) => ( p(ap(ap(ap(V0P,V6cmp),ap(ap(ap(c_2Eenumeral_2Esmerge(A_27a),V6cmp),V7l),V8m)),V9lol)) => p(ap(ap(ap(V0P,V6cmp),V7l),ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a))),ap(c_2Eoption_2ESOME(ty_2Elist_2Elist(A_27a)),V8m)),V9lol))) ) ) ) ) ) ) ) => ! [V10v] : ( mem(V10v,ty_2Etoto_2Etoto(A_27a)) => ! [V11v1] : ( mem(V11v1,ty_2Elist_2Elist(A_27a)) => ! [V12v2] : ( mem(V12v2,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a)))) => p(ap(ap(ap(V0P,V10v),V11v1),V12v2)) ) ) ) ) )))).
fof(conj_thm_2Eenumeral_2Eincr__smerge,lemma,( ! [A_27a]: ( ne(A_27a) => ( ( ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ! [V1cmp] : ( mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(ap(c_2Eenumeral_2Eincr__smerge(A_27a),V1cmp),V0l),c_2Elist_2ENIL(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a)))) = ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a))),ap(c_2Eoption_2ESOME(ty_2Elist_2Elist(A_27a)),V0l)),c_2Elist_2ENIL(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a)))) ) ) ) ) & ( ( ! [V2lol] : ( mem(V2lol,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a)))) => ! [V3l] : ( mem(V3l,ty_2Elist_2Elist(A_27a)) => ! [V4cmp] : ( mem(V4cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(ap(c_2Eenumeral_2Eincr__smerge(A_27a),V4cmp),V3l),ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a))),c_2Eoption_2ENONE(ty_2Elist_2Elist(A_27a))),V2lol)) = ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a))),ap(c_2Eoption_2ESOME(ty_2Elist_2Elist(A_27a)),V3l)),V2lol) ) ) ) ) ) & ! [V5m] : ( mem(V5m,ty_2Elist_2Elist(A_27a)) => ! [V6lol] : ( mem(V6lol,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a)))) => ! [V7l] : ( mem(V7l,ty_2Elist_2Elist(A_27a)) => ! [V8cmp] : ( mem(V8cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(ap(c_2Eenumeral_2Eincr__smerge(A_27a),V8cmp),V7l),ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a))),ap(c_2Eoption_2ESOME(ty_2Elist_2Elist(A_27a)),V5m)),V6lol)) = ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a))),c_2Eoption_2ENONE(ty_2Elist_2Elist(A_27a))),ap(ap(ap(c_2Eenumeral_2Eincr__smerge(A_27a),V8cmp),ap(ap(ap(c_2Eenumeral_2Esmerge(A_27a),V8cmp),V7l),V5m)),V6lol)) ) ) ) ) ) ) )))).
fof(conj_thm_2Eenumeral_2Eincr__smerge__OL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1lol] : ( mem(V1lol,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a)))) => ! [V2l] : ( mem(V2l,ty_2Elist_2Elist(A_27a)) => ( ( p(ap(ap(c_2Eenumeral_2EOL__sublists(A_27a),V0cmp),V1lol)) & p(ap(ap(c_2Eenumeral_2EOL(A_27a),V0cmp),V2l)) ) => p(ap(ap(c_2Eenumeral_2EOL__sublists(A_27a),V0cmp),ap(ap(ap(c_2Eenumeral_2Eincr__smerge(A_27a),V0cmp),V2l),V1lol))) ) ) ) )))).
fof(conj_thm_2Eenumeral_2Esmerge__out__ind,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Elist_2Elist(A_27a),arr(ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a))),bool)))) => ( ( ( ! [V1cmp] : ( mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V2l] : ( mem(V2l,ty_2Elist_2Elist(A_27a)) => p(ap(ap(ap(V0P,V1cmp),V2l),c_2Elist_2ENIL(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a))))) ) ) ) & ( ( ! [V3cmp] : ( mem(V3cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V4l] : ( mem(V4l,ty_2Elist_2Elist(A_27a)) => ! [V5lol] : ( mem(V5lol,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a)))) => ( p(ap(ap(ap(V0P,V3cmp),V4l),V5lol)) => p(ap(ap(ap(V0P,V3cmp),V4l),ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a))),c_2Eoption_2ENONE(ty_2Elist_2Elist(A_27a))),V5lol))) ) ) ) ) ) & ! [V6cmp] : ( mem(V6cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V7l] : ( mem(V7l,ty_2Elist_2Elist(A_27a)) => ! [V8m] : ( mem(V8m,ty_2Elist_2Elist(A_27a)) => ! [V9lol] : ( mem(V9lol,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a)))) => ( p(ap(ap(ap(V0P,V6cmp),ap(ap(ap(c_2Eenumeral_2Esmerge(A_27a),V6cmp),V7l),V8m)),V9lol)) => p(ap(ap(ap(V0P,V6cmp),V7l),ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a))),ap(c_2Eoption_2ESOME(ty_2Elist_2Elist(A_27a)),V8m)),V9lol))) ) ) ) ) ) ) ) => ! [V10v] : ( mem(V10v,ty_2Etoto_2Etoto(A_27a)) => ! [V11v1] : ( mem(V11v1,ty_2Elist_2Elist(A_27a)) => ! [V12v2] : ( mem(V12v2,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a)))) => p(ap(ap(ap(V0P,V10v),V11v1),V12v2)) ) ) ) ) )))).
fof(conj_thm_2Eenumeral_2Esmerge__out,lemma,( ! [A_27a]: ( ne(A_27a) => ( ( ! [V0l] : ( mem(V0l,ty_2Elist_2Elist(A_27a)) => ! [V1cmp] : ( mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(ap(c_2Eenumeral_2Esmerge__out(A_27a),V1cmp),V0l),c_2Elist_2ENIL(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a)))) = V0l ) ) ) ) & ( ( ! [V2lol] : ( mem(V2lol,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a)))) => ! [V3l] : ( mem(V3l,ty_2Elist_2Elist(A_27a)) => ! [V4cmp] : ( mem(V4cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(ap(c_2Eenumeral_2Esmerge__out(A_27a),V4cmp),V3l),ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a))),c_2Eoption_2ENONE(ty_2Elist_2Elist(A_27a))),V2lol)) = ap(ap(ap(c_2Eenumeral_2Esmerge__out(A_27a),V4cmp),V3l),V2lol) ) ) ) ) ) & ! [V5m] : ( mem(V5m,ty_2Elist_2Elist(A_27a)) => ! [V6lol] : ( mem(V6lol,ty_2Elist_2Elist(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a)))) => ! [V7l] : ( mem(V7l,ty_2Elist_2Elist(A_27a)) => ! [V8cmp] : ( mem(V8cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(ap(c_2Eenumeral_2Esmerge__out(A_27a),V8cmp),V7l),ap(ap(c_2Elist_2ECONS(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a))),ap(c_2Eoption_2ESOME(ty_2Elist_2Elist(A_27a)),V5m)),V6lol)) = ap(ap(ap(c_2Eenumeral_2Esmerge__out(A_27a),V8cmp),ap(ap(ap(c_2Eenumeral_2Esmerge(A_27a),V8cmp),V7l),V5m)),V6lol) ) ) ) ) ) ) )))).
fof(ax_thm_2Eenumeral_2Eincr__sbuild,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(c_2Eenumeral_2Eincr__sbuild(A_27a),V0cmp),c_2Elist_2ENIL(A_27a)) = c_2Elist_2ENIL(ty_2Eoption_2Eoption(ty_2Elist_2Elist(A_27a))) ) ) ) & ! [V1cmp] : ( mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V2x] : ( mem(V2x,A_27a) => ! [V3l] : ( mem(V3l,ty_2Elist_2Elist(A_27a)) => ( ap(ap(c_2Eenumeral_2Eincr__sbuild(A_27a),V1cmp),ap(ap(c_2Elist_2ECONS(A_27a),V2x),V3l)) = ap(ap(ap(c_2Eenumeral_2Eincr__smerge(A_27a),V1cmp),ap(ap(c_2Elist_2ECONS(A_27a),V2x),c_2Elist_2ENIL(A_27a))),ap(ap(c_2Eenumeral_2Eincr__sbuild(A_27a),V1cmp),V3l)) ) ) ) ) ) ) )).
fof(ax_thm_2Eenumeral_2Eincr__ssort,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ( ap(ap(c_2Eenumeral_2Eincr__ssort(A_27a),V0cmp),V1l) = ap(ap(ap(c_2Eenumeral_2Esmerge__out(A_27a),V0cmp),c_2Elist_2ENIL(A_27a)),ap(ap(c_2Eenumeral_2Eincr__sbuild(A_27a),V0cmp),V1l)) ) ) ) ) )).
fof(ax_thm_2Eenumeral_2Ebt__to__set,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(c_2Eenumeral_2EENUMERAL(A_27a),V0cmp),c_2Eenumeral_2Ent(A_27a)) = c_2Epred__set_2EEMPTY(A_27a) ) ) ) & ! [V1cmp] : ( mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V2l] : ( mem(V2l,ty_2Eenumeral_2Ebt(A_27a)) => ! [V3x] : ( mem(V3x,A_27a) => ! [V4r] : ( mem(V4r,ty_2Eenumeral_2Ebt(A_27a)) => ( ap(ap(c_2Eenumeral_2EENUMERAL(A_27a),V1cmp),ap(ap(ap(c_2Eenumeral_2Enode(A_27a),V2l),V3x),V4r)) = ap(ap(c_2Epred__set_2EUNION(A_27a),ap(ap(c_2Epred__set_2EUNION(A_27a),ap(c_2Epred__set_2EGSPEC(A_27a,A_27a),f2473(A_27a,V3x,V1cmp,V2l))),ap(ap(c_2Epred__set_2EINSERT(A_27a),V3x),c_2Epred__set_2EEMPTY(A_27a)))),ap(c_2Epred__set_2EGSPEC(A_27a,A_27a),f2474(A_27a,V1cmp,V3x,V4r))) ) ) ) ) ) ) ) )).
fof(ax_thm_2Eenumeral_2Ebt__to__set__lb,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1lb] : ( mem(V1lb,A_27a) => ! [V2t] : ( mem(V2t,ty_2Eenumeral_2Ebt(A_27a)) => ( ap(ap(ap(c_2Eenumeral_2Ebt__to__set__lb(A_27a),V0cmp),V1lb),V2t) = ap(c_2Epred__set_2EGSPEC(A_27a,A_27a),f2475(A_27a,V0cmp,V1lb,V2t)) ) ) ) ) ) )).
fof(ax_thm_2Eenumeral_2Ebt__to__set__ub,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1t] : ( mem(V1t,ty_2Eenumeral_2Ebt(A_27a)) => ! [V2ub] : ( mem(V2ub,A_27a) => ( ap(ap(ap(c_2Eenumeral_2Ebt__to__set__ub(A_27a),V0cmp),V1t),V2ub) = ap(c_2Epred__set_2EGSPEC(A_27a,A_27a),f2476(A_27a,V2ub,V0cmp,V1t)) ) ) ) ) ) )).
fof(ax_thm_2Eenumeral_2Ebt__to__set__lb__ub,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1lb] : ( mem(V1lb,A_27a) => ! [V2t] : ( mem(V2t,ty_2Eenumeral_2Ebt(A_27a)) => ! [V3ub] : ( mem(V3ub,A_27a) => ( ap(ap(ap(ap(c_2Eenumeral_2Ebt__to__set__lb__ub(A_27a),V0cmp),V1lb),V2t),V3ub) = ap(c_2Epred__set_2EGSPEC(A_27a,A_27a),f2477(A_27a,V2t,V0cmp,V1lb,V3ub)) ) ) ) ) ) ) )).
fof(conj_thm_2Eenumeral_2EIN__bt__to__set,lemma,( ! [A_27a]: ( ne(A_27a) => ( ( ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1y] : ( mem(V1y,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V1y),ap(ap(c_2Eenumeral_2EENUMERAL(A_27a),V0cmp),c_2Eenumeral_2Ent(A_27a)))) <=> $false ) ) ) ) & ! [V2cmp] : ( mem(V2cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V3l] : ( mem(V3l,ty_2Eenumeral_2Ebt(A_27a)) => ! [V4x] : ( mem(V4x,A_27a) => ! [V5r] : ( mem(V5r,ty_2Eenumeral_2Ebt(A_27a)) => ! [V6y] : ( mem(V6y,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V6y),ap(ap(c_2Eenumeral_2EENUMERAL(A_27a),V2cmp),ap(ap(ap(c_2Eenumeral_2Enode(A_27a),V3l),V4x),V5r)))) <=> ( ( p(ap(ap(c_2Ebool_2EIN(A_27a),V6y),ap(ap(c_2Eenumeral_2EENUMERAL(A_27a),V2cmp),V3l))) & ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V2cmp),V6y),V4x) = c_2EternaryComparisons_2ELESS ) ) | ( ( V6y = V4x ) | ( p(ap(ap(c_2Ebool_2EIN(A_27a),V6y),ap(ap(c_2Eenumeral_2EENUMERAL(A_27a),V2cmp),V5r))) & ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V2cmp),V4x),V6y) = c_2EternaryComparisons_2ELESS ) ) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Eenumeral_2ENOT__IN__nt,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1y] : ( mem(V1y,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V1y),ap(ap(c_2Eenumeral_2EENUMERAL(A_27a),V0cmp),c_2Eenumeral_2Ent(A_27a)))) <=> $false ) ) )))).
fof(conj_thm_2Eenumeral_2EIN__node,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1x] : ( mem(V1x,A_27a) => ! [V2l] : ( mem(V2l,ty_2Eenumeral_2Ebt(A_27a)) => ! [V3y] : ( mem(V3y,A_27a) => ! [V4r] : ( mem(V4r,ty_2Eenumeral_2Ebt(A_27a)) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V1x),ap(ap(c_2Eenumeral_2EENUMERAL(A_27a),V0cmp),ap(ap(ap(c_2Eenumeral_2Enode(A_27a),V2l),V3y),V4r)))) <=> p(ap(ap(ap(ap(c_2EternaryComparisons_2Eordering__CASE(bool),ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0cmp),V1x),V3y)),ap(ap(c_2Ebool_2EIN(A_27a),V1x),ap(ap(c_2Eenumeral_2EENUMERAL(A_27a),V0cmp),V2l))),c_2Ebool_2ET),ap(ap(c_2Ebool_2EIN(A_27a),V1x),ap(ap(c_2Eenumeral_2EENUMERAL(A_27a),V0cmp),V4r)))) ) ) ) ) ) )))).
fof(ax_thm_2Eenumeral_2Ebt__to__ol__lb__ub,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1lb] : ( mem(V1lb,A_27a) => ! [V2ub] : ( mem(V2ub,A_27a) => ( ap(ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__lb__ub(A_27a),V0cmp),V1lb),c_2Eenumeral_2Ent(A_27a)),V2ub) = c_2Elist_2ENIL(A_27a) ) ) ) ) ) & ! [V3cmp] : ( mem(V3cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V4lb] : ( mem(V4lb,A_27a) => ! [V5l] : ( mem(V5l,ty_2Eenumeral_2Ebt(A_27a)) => ! [V6x] : ( mem(V6x,A_27a) => ! [V7r] : ( mem(V7r,ty_2Eenumeral_2Ebt(A_27a)) => ! [V8ub] : ( mem(V8ub,A_27a) => ( ap(ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__lb__ub(A_27a),V3cmp),V4lb),ap(ap(ap(c_2Eenumeral_2Enode(A_27a),V5l),V6x),V7r)),V8ub) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Elist_2Elist(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2EternaryComparisons_2Eordering),ap(ap(ap(c_2Etoto_2Eapto(A_27a),V3cmp),V4lb),V6x)),c_2EternaryComparisons_2ELESS)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Elist_2Elist(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2EternaryComparisons_2Eordering),ap(ap(ap(c_2Etoto_2Eapto(A_27a),V3cmp),V6x),V8ub)),c_2EternaryComparisons_2ELESS)),ap(ap(c_2Elist_2EAPPEND(A_27a),ap(ap(c_2Elist_2EAPPEND(A_27a),ap(ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__lb__ub(A_27a),V3cmp),V4lb),V5l),V6x)),ap(ap(c_2Elist_2ECONS(A_27a),V6x),c_2Elist_2ENIL(A_27a)))),ap(ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__lb__ub(A_27a),V3cmp),V6x),V7r),V8ub))),ap(ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__lb__ub(A_27a),V3cmp),V4lb),V5l),V8ub))),ap(ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__lb__ub(A_27a),V3cmp),V4lb),V7r),V8ub)) ) ) ) ) ) ) ) ) ) )).
fof(ax_thm_2Eenumeral_2Ebt__to__ol__lb,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1lb] : ( mem(V1lb,A_27a) => ( ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__lb(A_27a),V0cmp),V1lb),c_2Eenumeral_2Ent(A_27a)) = c_2Elist_2ENIL(A_27a) ) ) ) ) & ! [V2cmp] : ( mem(V2cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V3lb] : ( mem(V3lb,A_27a) => ! [V4l] : ( mem(V4l,ty_2Eenumeral_2Ebt(A_27a)) => ! [V5x] : ( mem(V5x,A_27a) => ! [V6r] : ( mem(V6r,ty_2Eenumeral_2Ebt(A_27a)) => ( ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__lb(A_27a),V2cmp),V3lb),ap(ap(ap(c_2Eenumeral_2Enode(A_27a),V4l),V5x),V6r)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Elist_2Elist(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2EternaryComparisons_2Eordering),ap(ap(ap(c_2Etoto_2Eapto(A_27a),V2cmp),V3lb),V5x)),c_2EternaryComparisons_2ELESS)),ap(ap(c_2Elist_2EAPPEND(A_27a),ap(ap(c_2Elist_2EAPPEND(A_27a),ap(ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__lb__ub(A_27a),V2cmp),V3lb),V4l),V5x)),ap(ap(c_2Elist_2ECONS(A_27a),V5x),c_2Elist_2ENIL(A_27a)))),ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__lb(A_27a),V2cmp),V5x),V6r))),ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__lb(A_27a),V2cmp),V3lb),V6r)) ) ) ) ) ) ) ) ) )).
fof(ax_thm_2Eenumeral_2Ebt__to__ol__ub,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1ub] : ( mem(V1ub,A_27a) => ( ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__ub(A_27a),V0cmp),c_2Eenumeral_2Ent(A_27a)),V1ub) = c_2Elist_2ENIL(A_27a) ) ) ) ) & ! [V2cmp] : ( mem(V2cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V3l] : ( mem(V3l,ty_2Eenumeral_2Ebt(A_27a)) => ! [V4x] : ( mem(V4x,A_27a) => ! [V5r] : ( mem(V5r,ty_2Eenumeral_2Ebt(A_27a)) => ! [V6ub] : ( mem(V6ub,A_27a) => ( ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__ub(A_27a),V2cmp),ap(ap(ap(c_2Eenumeral_2Enode(A_27a),V3l),V4x),V5r)),V6ub) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Elist_2Elist(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2EternaryComparisons_2Eordering),ap(ap(ap(c_2Etoto_2Eapto(A_27a),V2cmp),V4x),V6ub)),c_2EternaryComparisons_2ELESS)),ap(ap(c_2Elist_2EAPPEND(A_27a),ap(ap(c_2Elist_2EAPPEND(A_27a),ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__ub(A_27a),V2cmp),V3l),V4x)),ap(ap(c_2Elist_2ECONS(A_27a),V4x),c_2Elist_2ENIL(A_27a)))),ap(ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__lb__ub(A_27a),V2cmp),V4x),V5r),V6ub))),ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__ub(A_27a),V2cmp),V3l),V6ub)) ) ) ) ) ) ) ) ) )).
fof(ax_thm_2Eenumeral_2Ebt__to__ol,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(c_2Eenumeral_2Ebt__to__ol(A_27a),V0cmp),c_2Eenumeral_2Ent(A_27a)) = c_2Elist_2ENIL(A_27a) ) ) ) & ! [V1cmp] : ( mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V2l] : ( mem(V2l,ty_2Eenumeral_2Ebt(A_27a)) => ! [V3x] : ( mem(V3x,A_27a) => ! [V4r] : ( mem(V4r,ty_2Eenumeral_2Ebt(A_27a)) => ( ap(ap(c_2Eenumeral_2Ebt__to__ol(A_27a),V1cmp),ap(ap(ap(c_2Eenumeral_2Enode(A_27a),V2l),V3x),V4r)) = ap(ap(c_2Elist_2EAPPEND(A_27a),ap(ap(c_2Elist_2EAPPEND(A_27a),ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__ub(A_27a),V1cmp),V2l),V3x)),ap(ap(c_2Elist_2ECONS(A_27a),V3x),c_2Elist_2ENIL(A_27a)))),ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__lb(A_27a),V1cmp),V3x),V4r)) ) ) ) ) ) ) ) )).
fof(conj_thm_2Eenumeral_2Eol__set,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1t] : ( mem(V1t,ty_2Eenumeral_2Ebt(A_27a)) => ( ap(ap(c_2Eenumeral_2EENUMERAL(A_27a),V0cmp),V1t) = ap(c_2Elist_2ELIST__TO__SET(A_27a),ap(ap(c_2Eenumeral_2Ebt__to__ol(A_27a),V0cmp),V1t)) ) ) )))).
fof(conj_thm_2Eenumeral_2EOL__bt__to__ol__lb__ub,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1t] : ( mem(V1t,ty_2Eenumeral_2Ebt(A_27a)) => ! [V2lb] : ( mem(V2lb,A_27a) => ! [V3ub] : ( mem(V3ub,A_27a) => p(ap(ap(c_2Eenumeral_2EOL(A_27a),V0cmp),ap(ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__lb__ub(A_27a),V0cmp),V2lb),V1t),V3ub))) ) ) ) )))).
fof(conj_thm_2Eenumeral_2EOL__bt__to__ol__lb,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1t] : ( mem(V1t,ty_2Eenumeral_2Ebt(A_27a)) => ! [V2lb] : ( mem(V2lb,A_27a) => p(ap(ap(c_2Eenumeral_2EOL(A_27a),V0cmp),ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__lb(A_27a),V0cmp),V2lb),V1t))) ) ) )))).
fof(conj_thm_2Eenumeral_2EOL__bt__to__ol__ub,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1t] : ( mem(V1t,ty_2Eenumeral_2Ebt(A_27a)) => ! [V2ub] : ( mem(V2ub,A_27a) => p(ap(ap(c_2Eenumeral_2EOL(A_27a),V0cmp),ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__ub(A_27a),V0cmp),V1t),V2ub))) ) ) )))).
fof(conj_thm_2Eenumeral_2EOL__bt__to__ol,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1t] : ( mem(V1t,ty_2Eenumeral_2Ebt(A_27a)) => p(ap(ap(c_2Eenumeral_2EOL(A_27a),V0cmp),ap(ap(c_2Eenumeral_2Ebt__to__ol(A_27a),V0cmp),V1t))) ) )))).
fof(ax_thm_2Eenumeral_2Ebt__to__ol__lb__ub__ac,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1lb] : ( mem(V1lb,A_27a) => ! [V2ub] : ( mem(V2ub,A_27a) => ! [V3m] : ( mem(V3m,ty_2Elist_2Elist(A_27a)) => ( ap(ap(ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__lb__ub__ac(A_27a),V0cmp),V1lb),c_2Eenumeral_2Ent(A_27a)),V2ub),V3m) = V3m ) ) ) ) ) ) & ! [V4cmp] : ( mem(V4cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V5lb] : ( mem(V5lb,A_27a) => ! [V6l] : ( mem(V6l,ty_2Eenumeral_2Ebt(A_27a)) => ! [V7x] : ( mem(V7x,A_27a) => ! [V8r] : ( mem(V8r,ty_2Eenumeral_2Ebt(A_27a)) => ! [V9ub] : ( mem(V9ub,A_27a) => ! [V10m] : ( mem(V10m,ty_2Elist_2Elist(A_27a)) => ( ap(ap(ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__lb__ub__ac(A_27a),V4cmp),V5lb),ap(ap(ap(c_2Eenumeral_2Enode(A_27a),V6l),V7x),V8r)),V9ub),V10m) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Elist_2Elist(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2EternaryComparisons_2Eordering),ap(ap(ap(c_2Etoto_2Eapto(A_27a),V4cmp),V5lb),V7x)),c_2EternaryComparisons_2ELESS)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Elist_2Elist(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2EternaryComparisons_2Eordering),ap(ap(ap(c_2Etoto_2Eapto(A_27a),V4cmp),V7x),V9ub)),c_2EternaryComparisons_2ELESS)),ap(ap(ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__lb__ub__ac(A_27a),V4cmp),V5lb),V6l),V7x),ap(ap(c_2Elist_2ECONS(A_27a),V7x),ap(ap(ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__lb__ub__ac(A_27a),V4cmp),V7x),V8r),V9ub),V10m)))),ap(ap(ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__lb__ub__ac(A_27a),V4cmp),V5lb),V6l),V9ub),V10m))),ap(ap(ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__lb__ub__ac(A_27a),V4cmp),V5lb),V8r),V9ub),V10m)) ) ) ) ) ) ) ) ) ) ) )).
fof(ax_thm_2Eenumeral_2Ebt__to__ol__lb__ac,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1lb] : ( mem(V1lb,A_27a) => ! [V2m] : ( mem(V2m,ty_2Elist_2Elist(A_27a)) => ( ap(ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__lb__ac(A_27a),V0cmp),V1lb),c_2Eenumeral_2Ent(A_27a)),V2m) = V2m ) ) ) ) ) & ! [V3cmp] : ( mem(V3cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V4lb] : ( mem(V4lb,A_27a) => ! [V5l] : ( mem(V5l,ty_2Eenumeral_2Ebt(A_27a)) => ! [V6x] : ( mem(V6x,A_27a) => ! [V7r] : ( mem(V7r,ty_2Eenumeral_2Ebt(A_27a)) => ! [V8m] : ( mem(V8m,ty_2Elist_2Elist(A_27a)) => ( ap(ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__lb__ac(A_27a),V3cmp),V4lb),ap(ap(ap(c_2Eenumeral_2Enode(A_27a),V5l),V6x),V7r)),V8m) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Elist_2Elist(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2EternaryComparisons_2Eordering),ap(ap(ap(c_2Etoto_2Eapto(A_27a),V3cmp),V4lb),V6x)),c_2EternaryComparisons_2ELESS)),ap(ap(ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__lb__ub__ac(A_27a),V3cmp),V4lb),V5l),V6x),ap(ap(c_2Elist_2ECONS(A_27a),V6x),ap(ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__lb__ac(A_27a),V3cmp),V6x),V7r),V8m)))),ap(ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__lb__ac(A_27a),V3cmp),V4lb),V7r),V8m)) ) ) ) ) ) ) ) ) ) )).
fof(ax_thm_2Eenumeral_2Ebt__to__ol__ub__ac,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1ub] : ( mem(V1ub,A_27a) => ! [V2m] : ( mem(V2m,ty_2Elist_2Elist(A_27a)) => ( ap(ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__ub__ac(A_27a),V0cmp),c_2Eenumeral_2Ent(A_27a)),V1ub),V2m) = V2m ) ) ) ) ) & ! [V3cmp] : ( mem(V3cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V4l] : ( mem(V4l,ty_2Eenumeral_2Ebt(A_27a)) => ! [V5x] : ( mem(V5x,A_27a) => ! [V6r] : ( mem(V6r,ty_2Eenumeral_2Ebt(A_27a)) => ! [V7ub] : ( mem(V7ub,A_27a) => ! [V8m] : ( mem(V8m,ty_2Elist_2Elist(A_27a)) => ( ap(ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__ub__ac(A_27a),V3cmp),ap(ap(ap(c_2Eenumeral_2Enode(A_27a),V4l),V5x),V6r)),V7ub),V8m) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Elist_2Elist(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2EternaryComparisons_2Eordering),ap(ap(ap(c_2Etoto_2Eapto(A_27a),V3cmp),V5x),V7ub)),c_2EternaryComparisons_2ELESS)),ap(ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__ub__ac(A_27a),V3cmp),V4l),V5x),ap(ap(c_2Elist_2ECONS(A_27a),V5x),ap(ap(ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__lb__ub__ac(A_27a),V3cmp),V5x),V6r),V7ub),V8m)))),ap(ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__ub__ac(A_27a),V3cmp),V4l),V7ub),V8m)) ) ) ) ) ) ) ) ) ) )).
fof(ax_thm_2Eenumeral_2Ebt__to__ol__ac,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1m] : ( mem(V1m,ty_2Elist_2Elist(A_27a)) => ( ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__ac(A_27a),V0cmp),c_2Eenumeral_2Ent(A_27a)),V1m) = V1m ) ) ) ) & ! [V2cmp] : ( mem(V2cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V3l] : ( mem(V3l,ty_2Eenumeral_2Ebt(A_27a)) => ! [V4x] : ( mem(V4x,A_27a) => ! [V5r] : ( mem(V5r,ty_2Eenumeral_2Ebt(A_27a)) => ! [V6m] : ( mem(V6m,ty_2Elist_2Elist(A_27a)) => ( ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__ac(A_27a),V2cmp),ap(ap(ap(c_2Eenumeral_2Enode(A_27a),V3l),V4x),V5r)),V6m) = ap(ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__ub__ac(A_27a),V2cmp),V3l),V4x),ap(ap(c_2Elist_2ECONS(A_27a),V4x),ap(ap(ap(ap(c_2Eenumeral_2Ebt__to__ol__lb__ac(A_27a),V2cmp),V4x),V5r),V6m))) ) ) ) ) ) ) ) ) )).
fof(ax_thm_2Eenumeral_2EOWL,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ! [V2l] : ( mem(V2l,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(ap(c_2Eenumeral_2EOWL(A_27a),V0cmp),V1s),V2l)) <=> ( ( V1s = ap(c_2Elist_2ELIST__TO__SET(A_27a),V2l) ) & p(ap(ap(c_2Eenumeral_2EOL(A_27a),V0cmp),V2l)) ) ) ) ) ) ) )).
fof(conj_thm_2Eenumeral_2EOWL__bt__to__ol,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1t] : ( mem(V1t,ty_2Eenumeral_2Ebt(A_27a)) => p(ap(ap(ap(c_2Eenumeral_2EOWL(A_27a),V0cmp),ap(ap(c_2Eenumeral_2EENUMERAL(A_27a),V0cmp),V1t)),ap(ap(c_2Eenumeral_2Ebt__to__ol(A_27a),V0cmp),V1t))) ) )))).
fof(ax_thm_2Eenumeral_2EOU,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1t] : ( mem(V1t,arr(A_27a,bool)) => ! [V2u] : ( mem(V2u,arr(A_27a,bool)) => ( ap(ap(ap(c_2Eenumeral_2EOU(A_27a),V0cmp),V1t),V2u) = ap(ap(c_2Epred__set_2EUNION(A_27a),ap(c_2Epred__set_2EGSPEC(A_27a,A_27a),f2479(A_27a,V1t,V2u,V0cmp))),V2u) ) ) ) ) ) )).
fof(ax_thm_2Eenumeral_2EUO,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ! [V2t] : ( mem(V2t,arr(A_27a,bool)) => ( ap(ap(ap(c_2Eenumeral_2EUO(A_27a),V0cmp),V1s),V2t) = ap(ap(c_2Epred__set_2EUNION(A_27a),V1s),ap(c_2Epred__set_2EGSPEC(A_27a,A_27a),f2481(A_27a,V2t,V1s,V0cmp))) ) ) ) ) ) )).
fof(conj_thm_2Eenumeral_2EEMPTY__OU,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1sl] : ( mem(V1sl,arr(A_27a,bool)) => ( ap(ap(ap(c_2Eenumeral_2EOU(A_27a),V0cmp),c_2Epred__set_2EEMPTY(A_27a)),V1sl) = V1sl ) ) )))).
fof(conj_thm_2Eenumeral_2EOU__EMPTY,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1t] : ( mem(V1t,arr(A_27a,bool)) => ( ap(ap(ap(c_2Eenumeral_2EOU(A_27a),V0cmp),V1t),c_2Epred__set_2EEMPTY(A_27a)) = V1t ) ) )))).
fof(conj_thm_2Eenumeral_2ELESS__UO__LEM,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1x] : ( mem(V1x,A_27a) => ! [V2y] : ( mem(V2y,A_27a) => ! [V3s] : ( mem(V3s,arr(A_27a,bool)) => ( ( ! [V4z] : ( mem(V4z,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V4z),ap(ap(ap(c_2Eenumeral_2EUO(A_27a),V0cmp),ap(ap(c_2Epred__set_2EINSERT(A_27a),V1x),c_2Epred__set_2EEMPTY(A_27a))),V3s))) => ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0cmp),V2y),V4z) = c_2EternaryComparisons_2ELESS ) ) ) ) <=> ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0cmp),V2y),V1x) = c_2EternaryComparisons_2ELESS ) ) ) ) ) )))).
fof(ax_thm_2Eenumeral_2ELESS__ALL,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1x] : ( mem(V1x,A_27a) => ! [V2s] : ( mem(V2s,arr(A_27a,bool)) => ( p(ap(ap(ap(c_2Eenumeral_2ELESS__ALL(A_27a),V0cmp),V1x),V2s)) <=> ! [V3y] : ( mem(V3y,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V3y),V2s)) => ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V0cmp),V1x),V3y) = c_2EternaryComparisons_2ELESS ) ) ) ) ) ) ) ) )).
fof(conj_thm_2Eenumeral_2ELESS__ALL__OU,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1x] : ( mem(V1x,A_27a) => ! [V2u] : ( mem(V2u,arr(A_27a,bool)) => ! [V3v] : ( mem(V3v,arr(A_27a,bool)) => ( p(ap(ap(ap(c_2Eenumeral_2ELESS__ALL(A_27a),V0cmp),V1x),ap(ap(ap(c_2Eenumeral_2EOU(A_27a),V0cmp),V2u),V3v))) <=> ( p(ap(ap(ap(c_2Eenumeral_2ELESS__ALL(A_27a),V0cmp),V1x),V2u)) & p(ap(ap(ap(c_2Eenumeral_2ELESS__ALL(A_27a),V0cmp),V1x),V3v)) ) ) ) ) ) )))).
fof(conj_thm_2Eenumeral_2EOU__ASSOC,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1a] : ( mem(V1a,arr(A_27a,bool)) => ! [V2b] : ( mem(V2b,arr(A_27a,bool)) => ! [V3c] : ( mem(V3c,arr(A_27a,bool)) => ( ap(ap(ap(c_2Eenumeral_2EOU(A_27a),V0cmp),V1a),ap(ap(ap(c_2Eenumeral_2EOU(A_27a),V0cmp),V2b),V3c)) = ap(ap(ap(c_2Eenumeral_2EOU(A_27a),V0cmp),ap(ap(ap(c_2Eenumeral_2EOU(A_27a),V0cmp),V1a),V2b)),V3c) ) ) ) ) )))).
fof(ax_thm_2Eenumeral_2Ebl__to__set,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(c_2Eenumeral_2Ebl__to__set(A_27a),V0cmp),c_2Eenumeral_2Enbl(A_27a)) = c_2Epred__set_2EEMPTY(A_27a) ) ) ) & ( ( ! [V1cmp] : ( mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V2b] : ( mem(V2b,ty_2Eenumeral_2Ebl(A_27a)) => ( ap(ap(c_2Eenumeral_2Ebl__to__set(A_27a),V1cmp),ap(c_2Eenumeral_2Ezerbl(A_27a),V2b)) = ap(ap(c_2Eenumeral_2Ebl__to__set(A_27a),V1cmp),V2b) ) ) ) ) & ! [V3cmp] : ( mem(V3cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V4x] : ( mem(V4x,A_27a) => ! [V5t] : ( mem(V5t,ty_2Eenumeral_2Ebt(A_27a)) => ! [V6b] : ( mem(V6b,ty_2Eenumeral_2Ebl(A_27a)) => ( ap(ap(c_2Eenumeral_2Ebl__to__set(A_27a),V3cmp),ap(ap(ap(c_2Eenumeral_2Eonebl(A_27a),V4x),V5t),V6b)) = ap(ap(ap(c_2Eenumeral_2EOU(A_27a),V3cmp),ap(ap(c_2Epred__set_2EUNION(A_27a),ap(ap(c_2Epred__set_2EINSERT(A_27a),V4x),c_2Epred__set_2EEMPTY(A_27a))),ap(c_2Epred__set_2EGSPEC(A_27a,A_27a),f2482(A_27a,V3cmp,V4x,V5t)))),ap(ap(c_2Eenumeral_2Ebl__to__set(A_27a),V3cmp),V6b)) ) ) ) ) ) ) ) ) )).
fof(conj_thm_2Eenumeral_2ELESS__ALL__UO__LEM,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1a] : ( mem(V1a,A_27a) => ! [V2s] : ( mem(V2s,arr(A_27a,bool)) => ( p(ap(ap(ap(c_2Eenumeral_2ELESS__ALL(A_27a),V0cmp),V1a),V2s)) => ( ap(ap(ap(c_2Eenumeral_2EUO(A_27a),V0cmp),ap(ap(c_2Epred__set_2EINSERT(A_27a),V1a),c_2Epred__set_2EEMPTY(A_27a))),V2s) = ap(ap(c_2Epred__set_2EINSERT(A_27a),V1a),V2s) ) ) ) ) )))).
fof(conj_thm_2Eenumeral_2ELESS__ALL__OU__UO__LEM,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1a] : ( mem(V1a,A_27a) => ! [V2s] : ( mem(V2s,arr(A_27a,bool)) => ! [V3t] : ( mem(V3t,arr(A_27a,bool)) => ( ( p(ap(ap(ap(c_2Eenumeral_2ELESS__ALL(A_27a),V0cmp),V1a),V2s)) & p(ap(ap(ap(c_2Eenumeral_2ELESS__ALL(A_27a),V0cmp),V1a),V3t)) ) => ( ap(ap(ap(c_2Eenumeral_2EOU(A_27a),V0cmp),ap(ap(ap(c_2Eenumeral_2EUO(A_27a),V0cmp),ap(ap(c_2Epred__set_2EINSERT(A_27a),V1a),c_2Epred__set_2EEMPTY(A_27a))),V2s)),V3t) = ap(ap(c_2Epred__set_2EINSERT(A_27a),V1a),ap(ap(ap(c_2Eenumeral_2EOU(A_27a),V0cmp),V2s),V3t)) ) ) ) ) ) )))).
fof(conj_thm_2Eenumeral_2Ebt__to__ol__ID__IMP,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Eenumeral_2EOL(A_27a),V0cmp),V1l)) => ( ap(ap(c_2Eenumeral_2Ebt__to__ol(A_27a),V0cmp),ap(c_2Eenumeral_2Elist__to__bt(A_27a),V1l)) = V1l ) ) ) )))).
fof(conj_thm_2Eenumeral_2EOL__UNION__IMP,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Eenumeral_2EOL(A_27a),V0cmp),V1l)) => ! [V2m] : ( mem(V2m,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Eenumeral_2EOL(A_27a),V0cmp),V2m)) => ( p(ap(ap(c_2Eenumeral_2EOL(A_27a),V0cmp),ap(ap(ap(c_2Eenumeral_2Esmerge(A_27a),V0cmp),V1l),V2m))) & ( ap(c_2Elist_2ELIST__TO__SET(A_27a),ap(ap(ap(c_2Eenumeral_2Esmerge(A_27a),V0cmp),V1l),V2m)) = ap(ap(c_2Epred__set_2EUNION(A_27a),ap(c_2Elist_2ELIST__TO__SET(A_27a),V1l)),ap(c_2Elist_2ELIST__TO__SET(A_27a),V2m)) ) ) ) ) ) ) )))).
fof(conj_thm_2Eenumeral_2Esinter__ind,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Elist_2Elist(A_27a),arr(ty_2Elist_2Elist(A_27a),bool)))) => ( ( ( ! [V1cmp] : ( mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => p(ap(ap(ap(V0P,V1cmp),c_2Elist_2ENIL(A_27a)),c_2Elist_2ENIL(A_27a))) ) ) & ( ( ! [V2cmp] : ( mem(V2cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V3x] : ( mem(V3x,A_27a) => ! [V4l] : ( mem(V4l,ty_2Elist_2Elist(A_27a)) => p(ap(ap(ap(V0P,V2cmp),ap(ap(c_2Elist_2ECONS(A_27a),V3x),V4l)),c_2Elist_2ENIL(A_27a))) ) ) ) ) & ( ( ! [V5cmp] : ( mem(V5cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V6y] : ( mem(V6y,A_27a) => ! [V7m] : ( mem(V7m,ty_2Elist_2Elist(A_27a)) => p(ap(ap(ap(V0P,V5cmp),c_2Elist_2ENIL(A_27a)),ap(ap(c_2Elist_2ECONS(A_27a),V6y),V7m))) ) ) ) ) & ! [V8cmp] : ( mem(V8cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V9x] : ( mem(V9x,A_27a) => ! [V10l] : ( mem(V10l,ty_2Elist_2Elist(A_27a)) => ! [V11y] : ( mem(V11y,A_27a) => ! [V12m] : ( mem(V12m,ty_2Elist_2Elist(A_27a)) => ( ( ( ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V8cmp),V9x),V11y) = c_2EternaryComparisons_2EEQUAL ) => p(ap(ap(ap(V0P,V8cmp),V10l),V12m)) ) & ( ( ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V8cmp),V9x),V11y) = c_2EternaryComparisons_2EGREATER ) => p(ap(ap(ap(V0P,V8cmp),ap(ap(c_2Elist_2ECONS(A_27a),V9x),V10l)),V12m)) ) & ( ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V8cmp),V9x),V11y) = c_2EternaryComparisons_2ELESS ) => p(ap(ap(ap(V0P,V8cmp),V10l),ap(ap(c_2Elist_2ECONS(A_27a),V11y),V12m))) ) ) ) => p(ap(ap(ap(V0P,V8cmp),ap(ap(c_2Elist_2ECONS(A_27a),V9x),V10l)),ap(ap(c_2Elist_2ECONS(A_27a),V11y),V12m))) ) ) ) ) ) ) ) ) ) => ! [V13v] : ( mem(V13v,ty_2Etoto_2Etoto(A_27a)) => ! [V14v1] : ( mem(V14v1,ty_2Elist_2Elist(A_27a)) => ! [V15v2] : ( mem(V15v2,ty_2Elist_2Elist(A_27a)) => p(ap(ap(ap(V0P,V13v),V14v1),V15v2)) ) ) ) ) )))).
fof(conj_thm_2Eenumeral_2Esinter,lemma,( ! [A_27a]: ( ne(A_27a) => ( ( ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(ap(c_2Eenumeral_2Esinter(A_27a),V0cmp),c_2Elist_2ENIL(A_27a)),c_2Elist_2ENIL(A_27a)) = c_2Elist_2ENIL(A_27a) ) ) ) & ( ( ! [V1x] : ( mem(V1x,A_27a) => ! [V2l] : ( mem(V2l,ty_2Elist_2Elist(A_27a)) => ! [V3cmp] : ( mem(V3cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(ap(c_2Eenumeral_2Esinter(A_27a),V3cmp),ap(ap(c_2Elist_2ECONS(A_27a),V1x),V2l)),c_2Elist_2ENIL(A_27a)) = c_2Elist_2ENIL(A_27a) ) ) ) ) ) & ( ( ! [V4y] : ( mem(V4y,A_27a) => ! [V5m] : ( mem(V5m,ty_2Elist_2Elist(A_27a)) => ! [V6cmp] : ( mem(V6cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(ap(c_2Eenumeral_2Esinter(A_27a),V6cmp),c_2Elist_2ENIL(A_27a)),ap(ap(c_2Elist_2ECONS(A_27a),V4y),V5m)) = c_2Elist_2ENIL(A_27a) ) ) ) ) ) & ! [V7y] : ( mem(V7y,A_27a) => ! [V8x] : ( mem(V8x,A_27a) => ! [V9m] : ( mem(V9m,ty_2Elist_2Elist(A_27a)) => ! [V10l] : ( mem(V10l,ty_2Elist_2Elist(A_27a)) => ! [V11cmp] : ( mem(V11cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(ap(c_2Eenumeral_2Esinter(A_27a),V11cmp),ap(ap(c_2Elist_2ECONS(A_27a),V8x),V10l)),ap(ap(c_2Elist_2ECONS(A_27a),V7y),V9m)) = ap(ap(ap(ap(c_2EternaryComparisons_2Eordering__CASE(ty_2Elist_2Elist(A_27a)),ap(ap(ap(c_2Etoto_2Eapto(A_27a),V11cmp),V8x),V7y)),ap(ap(ap(c_2Eenumeral_2Esinter(A_27a),V11cmp),V10l),ap(ap(c_2Elist_2ECONS(A_27a),V7y),V9m))),ap(ap(c_2Elist_2ECONS(A_27a),V8x),ap(ap(ap(c_2Eenumeral_2Esinter(A_27a),V11cmp),V10l),V9m))),ap(ap(ap(c_2Eenumeral_2Esinter(A_27a),V11cmp),ap(ap(c_2Elist_2ECONS(A_27a),V8x),V10l)),V9m)) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Eenumeral_2EOL__INTER__IMP,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Eenumeral_2EOL(A_27a),V0cmp),V1l)) => ! [V2m] : ( mem(V2m,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Eenumeral_2EOL(A_27a),V0cmp),V2m)) => ( p(ap(ap(c_2Eenumeral_2EOL(A_27a),V0cmp),ap(ap(ap(c_2Eenumeral_2Esinter(A_27a),V0cmp),V1l),V2m))) & ( ap(c_2Elist_2ELIST__TO__SET(A_27a),ap(ap(ap(c_2Eenumeral_2Esinter(A_27a),V0cmp),V1l),V2m)) = ap(ap(c_2Epred__set_2EINTER(A_27a),ap(c_2Elist_2ELIST__TO__SET(A_27a),V1l)),ap(c_2Elist_2ELIST__TO__SET(A_27a),V2m)) ) ) ) ) ) ) )))).
fof(conj_thm_2Eenumeral_2Esdiff__ind,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(ty_2Etoto_2Etoto(A_27a),arr(ty_2Elist_2Elist(A_27a),arr(ty_2Elist_2Elist(A_27a),bool)))) => ( ( ( ! [V1cmp] : ( mem(V1cmp,ty_2Etoto_2Etoto(A_27a)) => p(ap(ap(ap(V0P,V1cmp),c_2Elist_2ENIL(A_27a)),c_2Elist_2ENIL(A_27a))) ) ) & ( ( ! [V2cmp] : ( mem(V2cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V3x] : ( mem(V3x,A_27a) => ! [V4l] : ( mem(V4l,ty_2Elist_2Elist(A_27a)) => p(ap(ap(ap(V0P,V2cmp),ap(ap(c_2Elist_2ECONS(A_27a),V3x),V4l)),c_2Elist_2ENIL(A_27a))) ) ) ) ) & ( ( ! [V5cmp] : ( mem(V5cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V6y] : ( mem(V6y,A_27a) => ! [V7m] : ( mem(V7m,ty_2Elist_2Elist(A_27a)) => p(ap(ap(ap(V0P,V5cmp),c_2Elist_2ENIL(A_27a)),ap(ap(c_2Elist_2ECONS(A_27a),V6y),V7m))) ) ) ) ) & ! [V8cmp] : ( mem(V8cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V9x] : ( mem(V9x,A_27a) => ! [V10l] : ( mem(V10l,ty_2Elist_2Elist(A_27a)) => ! [V11y] : ( mem(V11y,A_27a) => ! [V12m] : ( mem(V12m,ty_2Elist_2Elist(A_27a)) => ( ( ( ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V8cmp),V9x),V11y) = c_2EternaryComparisons_2EEQUAL ) => p(ap(ap(ap(V0P,V8cmp),V10l),V12m)) ) & ( ( ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V8cmp),V9x),V11y) = c_2EternaryComparisons_2EGREATER ) => p(ap(ap(ap(V0P,V8cmp),ap(ap(c_2Elist_2ECONS(A_27a),V9x),V10l)),V12m)) ) & ( ( ap(ap(ap(c_2Etoto_2Eapto(A_27a),V8cmp),V9x),V11y) = c_2EternaryComparisons_2ELESS ) => p(ap(ap(ap(V0P,V8cmp),V10l),ap(ap(c_2Elist_2ECONS(A_27a),V11y),V12m))) ) ) ) => p(ap(ap(ap(V0P,V8cmp),ap(ap(c_2Elist_2ECONS(A_27a),V9x),V10l)),ap(ap(c_2Elist_2ECONS(A_27a),V11y),V12m))) ) ) ) ) ) ) ) ) ) => ! [V13v] : ( mem(V13v,ty_2Etoto_2Etoto(A_27a)) => ! [V14v1] : ( mem(V14v1,ty_2Elist_2Elist(A_27a)) => ! [V15v2] : ( mem(V15v2,ty_2Elist_2Elist(A_27a)) => p(ap(ap(ap(V0P,V13v),V14v1),V15v2)) ) ) ) ) )))).
fof(conj_thm_2Eenumeral_2Esdiff,lemma,( ! [A_27a]: ( ne(A_27a) => ( ( ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(ap(c_2Eenumeral_2Esdiff(A_27a),V0cmp),c_2Elist_2ENIL(A_27a)),c_2Elist_2ENIL(A_27a)) = c_2Elist_2ENIL(A_27a) ) ) ) & ( ( ! [V1x] : ( mem(V1x,A_27a) => ! [V2l] : ( mem(V2l,ty_2Elist_2Elist(A_27a)) => ! [V3cmp] : ( mem(V3cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(ap(c_2Eenumeral_2Esdiff(A_27a),V3cmp),ap(ap(c_2Elist_2ECONS(A_27a),V1x),V2l)),c_2Elist_2ENIL(A_27a)) = ap(ap(c_2Elist_2ECONS(A_27a),V1x),V2l) ) ) ) ) ) & ( ( ! [V4y] : ( mem(V4y,A_27a) => ! [V5m] : ( mem(V5m,ty_2Elist_2Elist(A_27a)) => ! [V6cmp] : ( mem(V6cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(ap(c_2Eenumeral_2Esdiff(A_27a),V6cmp),c_2Elist_2ENIL(A_27a)),ap(ap(c_2Elist_2ECONS(A_27a),V4y),V5m)) = c_2Elist_2ENIL(A_27a) ) ) ) ) ) & ! [V7y] : ( mem(V7y,A_27a) => ! [V8x] : ( mem(V8x,A_27a) => ! [V9m] : ( mem(V9m,ty_2Elist_2Elist(A_27a)) => ! [V10l] : ( mem(V10l,ty_2Elist_2Elist(A_27a)) => ! [V11cmp] : ( mem(V11cmp,ty_2Etoto_2Etoto(A_27a)) => ( ap(ap(ap(c_2Eenumeral_2Esdiff(A_27a),V11cmp),ap(ap(c_2Elist_2ECONS(A_27a),V8x),V10l)),ap(ap(c_2Elist_2ECONS(A_27a),V7y),V9m)) = ap(ap(ap(ap(c_2EternaryComparisons_2Eordering__CASE(ty_2Elist_2Elist(A_27a)),ap(ap(ap(c_2Etoto_2Eapto(A_27a),V11cmp),V8x),V7y)),ap(ap(c_2Elist_2ECONS(A_27a),V8x),ap(ap(ap(c_2Eenumeral_2Esdiff(A_27a),V11cmp),V10l),ap(ap(c_2Elist_2ECONS(A_27a),V7y),V9m)))),ap(ap(ap(c_2Eenumeral_2Esdiff(A_27a),V11cmp),V10l),V9m)),ap(ap(ap(c_2Eenumeral_2Esdiff(A_27a),V11cmp),ap(ap(c_2Elist_2ECONS(A_27a),V8x),V10l)),V9m)) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Eenumeral_2EOL__DIFF__IMP,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Eenumeral_2EOL(A_27a),V0cmp),V1l)) => ! [V2m] : ( mem(V2m,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Eenumeral_2EOL(A_27a),V0cmp),V2m)) => ( p(ap(ap(c_2Eenumeral_2EOL(A_27a),V0cmp),ap(ap(ap(c_2Eenumeral_2Esdiff(A_27a),V0cmp),V1l),V2m))) & ( ap(c_2Elist_2ELIST__TO__SET(A_27a),ap(ap(ap(c_2Eenumeral_2Esdiff(A_27a),V0cmp),V1l),V2m)) = ap(ap(c_2Epred__set_2EDIFF(A_27a),ap(c_2Elist_2ELIST__TO__SET(A_27a),V1l)),ap(c_2Elist_2ELIST__TO__SET(A_27a),V2m)) ) ) ) ) ) ) )))).
fof(conj_thm_2Eenumeral_2EENUMERAL__set,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ( ap(c_2Elist_2ELIST__TO__SET(A_27a),V1l) = ap(ap(c_2Eenumeral_2EENUMERAL(A_27a),V0cmp),ap(c_2Eenumeral_2Elist__to__bt(A_27a),ap(ap(c_2Eenumeral_2Eincr__ssort(A_27a),V0cmp),V1l))) ) ) )))).
fof(conj_thm_2Eenumeral_2EOL__ENUMERAL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1l] : ( mem(V1l,ty_2Elist_2Elist(A_27a)) => ( p(ap(ap(c_2Eenumeral_2EOL(A_27a),V0cmp),V1l)) => ( ap(c_2Elist_2ELIST__TO__SET(A_27a),V1l) = ap(ap(c_2Eenumeral_2EENUMERAL(A_27a),V0cmp),ap(c_2Eenumeral_2Elist__to__bt(A_27a),V1l)) ) ) ) )))).
fof(conj_thm_2Eenumeral_2EOWL__UNION__THM,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ! [V2l] : ( mem(V2l,ty_2Elist_2Elist(A_27a)) => ! [V3t] : ( mem(V3t,arr(A_27a,bool)) => ! [V4m] : ( mem(V4m,ty_2Elist_2Elist(A_27a)) => ( ( p(ap(ap(ap(c_2Eenumeral_2EOWL(A_27a),V0cmp),V1s),V2l)) & p(ap(ap(ap(c_2Eenumeral_2EOWL(A_27a),V0cmp),V3t),V4m)) ) => p(ap(ap(ap(c_2Eenumeral_2EOWL(A_27a),V0cmp),ap(ap(c_2Epred__set_2EUNION(A_27a),V1s),V3t)),ap(ap(ap(c_2Eenumeral_2Esmerge(A_27a),V0cmp),V2l),V4m))) ) ) ) ) ) )))).
fof(conj_thm_2Eenumeral_2EOWL__INTER__THM,conjecture,( ! [A_27a]: ( ne(A_27a) => ! [V0cmp] : ( mem(V0cmp,ty_2Etoto_2Etoto(A_27a)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ! [V2l] : ( mem(V2l,ty_2Elist_2Elist(A_27a)) => ! [V3t] : ( mem(V3t,arr(A_27a,bool)) => ! [V4m] : ( mem(V4m,ty_2Elist_2Elist(A_27a)) => ( ( p(ap(ap(ap(c_2Eenumeral_2EOWL(A_27a),V0cmp),V1s),V2l)) & p(ap(ap(ap(c_2Eenumeral_2EOWL(A_27a),V0cmp),V3t),V4m)) ) => p(ap(ap(ap(c_2Eenumeral_2EOWL(A_27a),V0cmp),ap(ap(c_2Epred__set_2EINTER(A_27a),V1s),V3t)),ap(ap(ap(c_2Eenumeral_2Esinter(A_27a),V0cmp),V2l),V4m))) ) ) ) ) ) )))).
