include('Axioms/semi_ring+2.ax').
fof(ne_ty_2Ewellorder_2Ewellorder,axiom,( ! [A0] : ( ne(A0) => ne(ty_2Ewellorder_2Ewellorder(A0)) ) )).
fof(mem_c_2Ewellorder_2EADD1,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewellorder_2EADD1(A_27a),arr(A_27a,arr(ty_2Ewellorder_2Ewellorder(A_27a),ty_2Ewellorder_2Ewellorder(A_27a)))) ) )).
fof(mem_c_2Ewellorder_2EChain,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewellorder_2EChain(A_27a),arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),arr(arr(A_27a,bool),bool))) ) )).
fof(mem_c_2Ewellorder_2EelsOf,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewellorder_2EelsOf(A_27a),arr(ty_2Ewellorder_2Ewellorder(A_27a),arr(A_27a,bool))) ) )).
fof(mem_c_2Ewellorder_2Efinite,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewellorder_2Efinite(A_27a),arr(ty_2Ewellorder_2Ewellorder(A_27a),bool)) ) )).
fof(mem_c_2Ewellorder_2Efl,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewellorder_2Efl(A_27a),arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),arr(A_27a,bool))) ) )).
fof(mem_c_2Ewellorder_2EfromNatWO,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewellorder_2EfromNatWO(A_27a),arr(ty_2Enum_2Enum,ty_2Ewellorder_2Ewellorder(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)))) ) )).
fof(mem_c_2Ewellorder_2Eiseg,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewellorder_2Eiseg(A_27a),arr(ty_2Ewellorder_2Ewellorder(A_27a),arr(A_27a,arr(A_27a,bool)))) ) )).
fof(mem_c_2Ewellorder_2Eorderiso,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Ewellorder_2Eorderiso(A_27a,A_27b),arr(ty_2Ewellorder_2Ewellorder(A_27a),arr(ty_2Ewellorder_2Ewellorder(A_27b),bool))) ) ) )).
fof(mem_c_2Ewellorder_2Eorderlt,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Ewellorder_2Eorderlt(A_27a,A_27b),arr(ty_2Ewellorder_2Ewellorder(A_27a),arr(ty_2Ewellorder_2Ewellorder(A_27b),bool))) ) ) )).
fof(mem_c_2Ewellorder_2Eposet,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewellorder_2Eposet(A_27a),arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),bool)) ) )).
fof(mem_c_2Ewellorder_2Eremove,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewellorder_2Eremove(A_27a),arr(A_27a,arr(ty_2Ewellorder_2Ewellorder(A_27a),ty_2Ewellorder_2Ewellorder(A_27a)))) ) )).
fof(mem_c_2Ewellorder_2EwZERO,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewellorder_2EwZERO(A_27a),ty_2Ewellorder_2Ewellorder(A_27a)) ) )).
fof(mem_c_2Ewellorder_2Ewellfounded,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewellorder_2Ewellfounded(A_27a),arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),bool)) ) )).
fof(mem_c_2Ewellorder_2Ewellorder,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewellorder_2Ewellorder(A_27a),arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),bool)) ) )).
fof(mem_c_2Ewellorder_2Ewellorder__ABS,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewellorder_2Ewellorder__ABS(A_27a),arr(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),ty_2Ewellorder_2Ewellorder(A_27a))) ) )).
fof(mem_c_2Ewellorder_2Ewellorder__REP,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewellorder_2Ewellorder__REP(A_27a),arr(ty_2Ewellorder_2Ewellorder(A_27a),arr(ty_2Epair_2Eprod(A_27a,A_27a),bool))) ) )).
fof(mem_c_2Ewellorder_2Ewleast,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewellorder_2Ewleast(A_27a),arr(ty_2Ewellorder_2Ewellorder(A_27a),arr(arr(A_27a,bool),ty_2Eoption_2Eoption(A_27a)))) ) )).
fof(mem_c_2Ewellorder_2Ewo2wo,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => mem(c_2Ewellorder_2Ewo2wo(A_27a,A_27b),arr(ty_2Ewellorder_2Ewellorder(A_27a),arr(ty_2Ewellorder_2Ewellorder(A_27b),arr(A_27a,ty_2Eoption_2Eoption(A_27b))))) ) ) )).
fof(mem_c_2Ewellorder_2Ewobound,axiom,( ! [A_27a] : ( ne(A_27a) => mem(c_2Ewellorder_2Ewobound(A_27a),arr(A_27a,arr(ty_2Ewellorder_2Ewellorder(A_27a),ty_2Ewellorder_2Ewellorder(A_27a)))) ) )).
fof(ax_thm_2Ewellorder_2Ewellfounded__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0R] : ( mem(V0R,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( p(ap(c_2Ewellorder_2Ewellfounded(A_27a),V0R)) <=> ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ( ( ? [V2w] : ( mem(V2w,A_27a) & p(ap(ap(c_2Ebool_2EIN(A_27a),V2w),V1s)) ) ) => ? [V3min] : ( mem(V3min,A_27a) & ( p(ap(ap(c_2Ebool_2EIN(A_27a),V3min),V1s)) & ! [V4w] : ( mem(V4w,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V4w),V3min)),V0R)) => ( ~~ p(ap(ap(c_2Ebool_2EIN(A_27a),V4w),V1s)) ) ) ) ) ) ) ) ) ) ) )).
fof(conj_thm_2Ewellorder_2Ewellfounded__WF,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0R] : ( mem(V0R,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( p(ap(c_2Ewellorder_2Ewellfounded(A_27a),V0R)) <=> p(ap(c_2Erelation_2EWF(A_27a),ap(c_2Epair_2ECURRY(A_27a,A_27a,bool),V0R))) ) )))).
fof(ax_thm_2Ewellorder_2Ewellorder__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0R] : ( mem(V0R,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( p(ap(c_2Ewellorder_2Ewellorder(A_27a),V0R)) <=> ( p(ap(c_2Ewellorder_2Ewellfounded(A_27a),ap(c_2Eset__relation_2Estrict(A_27a),V0R))) & ( p(ap(ap(c_2Eset__relation_2Elinear__order(A_27a),V0R),ap(ap(c_2Epred__set_2EUNION(A_27a),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),V0R)),ap(c_2Eset__relation_2Erange(A_27a,A_27a),V0R)))) & p(ap(ap(c_2Eset__relation_2Ereflexive(A_27a),V0R),ap(ap(c_2Epred__set_2EUNION(A_27a),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),V0R)),ap(c_2Eset__relation_2Erange(A_27a,A_27a),V0R)))) ) ) ) ) ) )).
fof(conj_thm_2Ewellorder_2Ewellorder__EMPTY,lemma,( ! [A_27a]: ( ne(A_27a) => p(ap(c_2Ewellorder_2Ewellorder(A_27a),c_2Epred__set_2EEMPTY(ty_2Epair_2Eprod(A_27a,A_27a))))))).
fof(conj_thm_2Ewellorder_2Ewellorder__SING,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1y] : ( mem(V1y,A_27a) => ( p(ap(c_2Ewellorder_2Ewellorder(A_27a),ap(ap(c_2Epred__set_2EINSERT(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V0x),V1y)),c_2Epred__set_2EEMPTY(ty_2Epair_2Eprod(A_27a,A_27a))))) <=> ( V0x = V1y ) ) ) )))).
fof(conj_thm_2Ewellorder_2Errestrict__SUBSET,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V0r),V1s)),V0r)) ) )))).
fof(conj_thm_2Ewellorder_2Ewellfounded__subset,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r0] : ( mem(V0r0,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1r] : ( mem(V1r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ( p(ap(c_2Ewellorder_2Ewellfounded(A_27a),V1r)) & p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Epair_2Eprod(A_27a,A_27a)),V0r0),V1r)) ) => p(ap(c_2Ewellorder_2Ewellfounded(A_27a),V0r0)) ) ) )))).
fof(ax_thm_2Ewellorder_2Ewellorder__TY__DEF,axiom,( ! [A_27a] : ( ne(A_27a) => ? [V0rep] : ( mem(V0rep,arr(ty_2Ewellorder_2Ewellorder(A_27a),arr(ty_2Epair_2Eprod(A_27a,A_27a),bool))) & p(ap(ap(c_2Ebool_2ETYPE__DEFINITION(arr(ty_2Epair_2Eprod(A_27a,A_27a),bool),ty_2Ewellorder_2Ewellorder(A_27a)),c_2Ewellorder_2Ewellorder(A_27a)),V0rep)) ) ) )).
fof(ax_thm_2Ewellorder_2Ewellorder__ABSREP,axiom,( ! [A_27a] : ( ne(A_27a) => ( ( ! [V0a] : ( mem(V0a,ty_2Ewellorder_2Ewellorder(A_27a)) => ( ap(c_2Ewellorder_2Ewellorder__ABS(A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V0a)) = V0a ) ) ) & ! [V1r] : ( mem(V1r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( p(ap(c_2Ewellorder_2Ewellorder(A_27a),V1r)) <=> ( ap(c_2Ewellorder_2Ewellorder__REP(A_27a),ap(c_2Ewellorder_2Ewellorder__ABS(A_27a),V1r)) = V1r ) ) ) ) ) )).
fof(conj_thm_2Ewellorder_2EmkWO__destWO,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,ty_2Ewellorder_2Ewellorder(A_27a)) => ( ap(c_2Ewellorder_2Ewellorder__ABS(A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V0a)) = V0a ) )))).
fof(conj_thm_2Ewellorder_2EdestWO__mkWO,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( p(ap(c_2Ewellorder_2Ewellorder(A_27a),V0r)) => ( ap(c_2Ewellorder_2Ewellorder__REP(A_27a),ap(c_2Ewellorder_2Ewellorder__ABS(A_27a),V0r)) = V0r ) ) )))).
fof(ax_thm_2Ewellorder_2EelsOf__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Ewellorder_2Ewellorder(A_27a)) => ( ap(c_2Ewellorder_2EelsOf(A_27a),V0w) = ap(ap(c_2Epred__set_2EUNION(A_27a),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V0w))),ap(c_2Eset__relation_2Erange(A_27a,A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V0w))) ) ) ) )).
fof(conj_thm_2Ewellorder_2EWIN__elsOf,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1y] : ( mem(V1y,A_27a) => ! [V2w] : ( mem(V2w,ty_2Ewellorder_2Ewellorder(A_27a)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V0x),V1y)),ap(c_2Eset__relation_2Estrict(A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V2w)))) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V0x),ap(c_2Ewellorder_2EelsOf(A_27a),V2w))) & p(ap(ap(c_2Ebool_2EIN(A_27a),V1y),ap(c_2Ewellorder_2EelsOf(A_27a),V2w))) ) ) ) ) )))).
fof(conj_thm_2Ewellorder_2EWLE__elsOf,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1y] : ( mem(V1y,A_27a) => ! [V2w] : ( mem(V2w,ty_2Ewellorder_2Ewellorder(A_27a)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V0x),V1y)),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V2w))) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V0x),ap(c_2Ewellorder_2EelsOf(A_27a),V2w))) & p(ap(ap(c_2Ebool_2EIN(A_27a),V1y),ap(c_2Ewellorder_2EelsOf(A_27a),V2w))) ) ) ) ) )))).
fof(conj_thm_2Ewellorder_2EWIN__trichotomy,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Ewellorder_2Ewellorder(A_27a)) => ! [V1x] : ( mem(V1x,A_27a) => ! [V2y] : ( mem(V2y,A_27a) => ( ( p(ap(ap(c_2Ebool_2EIN(A_27a),V1x),ap(c_2Ewellorder_2EelsOf(A_27a),V0w))) & p(ap(ap(c_2Ebool_2EIN(A_27a),V2y),ap(c_2Ewellorder_2EelsOf(A_27a),V0w))) ) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V2y)),ap(c_2Eset__relation_2Estrict(A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V0w)))) | ( ( V1x = V2y ) | p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2y),V1x)),ap(c_2Eset__relation_2Estrict(A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V0w)))) ) ) ) ) ) )))).
fof(conj_thm_2Ewellorder_2EWIN__REFL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1w] : ( mem(V1w,ty_2Ewellorder_2Ewellorder(A_27a)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V0x),V0x)),ap(c_2Eset__relation_2Estrict(A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V1w)))) <=> $false ) ) )))).
fof(conj_thm_2Ewellorder_2EWLE__TRANS,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1y] : ( mem(V1y,A_27a) => ! [V2w] : ( mem(V2w,ty_2Ewellorder_2Ewellorder(A_27a)) => ! [V3z] : ( mem(V3z,A_27a) => ( ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V0x),V1y)),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V2w))) & p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1y),V3z)),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V2w))) ) => p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V0x),V3z)),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V2w))) ) ) ) ) )))).
fof(conj_thm_2Ewellorder_2EWLE__ANTISYM,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1y] : ( mem(V1y,A_27a) => ! [V2w] : ( mem(V2w,ty_2Ewellorder_2Ewellorder(A_27a)) => ( ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V0x),V1y)),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V2w))) & p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1y),V0x)),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V2w))) ) => ( V0x = V1y ) ) ) ) )))).
fof(conj_thm_2Ewellorder_2EWIN__WLE,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1y] : ( mem(V1y,A_27a) => ! [V2w] : ( mem(V2w,ty_2Ewellorder_2Ewellorder(A_27a)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V0x),V1y)),ap(c_2Eset__relation_2Estrict(A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V2w)))) => p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V0x),V1y)),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V2w))) ) ) ) )))).
fof(conj_thm_2Ewellorder_2EelsOf__WLE,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1w] : ( mem(V1w,ty_2Ewellorder_2Ewellorder(A_27a)) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V0x),ap(c_2Ewellorder_2EelsOf(A_27a),V1w))) <=> p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V0x),V0x)),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V1w))) ) ) )))).
fof(conj_thm_2Ewellorder_2Etransitive__strict,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ( p(ap(c_2Eset__relation_2Etransitive(A_27a),V0r)) & p(ap(c_2Eset__relation_2Eantisym(A_27a),V0r)) ) => p(ap(c_2Eset__relation_2Etransitive(A_27a),ap(c_2Eset__relation_2Estrict(A_27a),V0r))) ) )))).
fof(conj_thm_2Ewellorder_2EWIN__TRANS,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1y] : ( mem(V1y,A_27a) => ! [V2w] : ( mem(V2w,ty_2Ewellorder_2Ewellorder(A_27a)) => ! [V3z] : ( mem(V3z,A_27a) => ( ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V0x),V1y)),ap(c_2Eset__relation_2Estrict(A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V2w)))) & p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1y),V3z)),ap(c_2Eset__relation_2Estrict(A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V2w)))) ) => p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V0x),V3z)),ap(c_2Eset__relation_2Estrict(A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V2w)))) ) ) ) ) )))).
fof(conj_thm_2Ewellorder_2EWIN__WF,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Ewellorder_2Ewellorder(A_27a)) => p(ap(c_2Ewellorder_2Ewellfounded(A_27a),f1018(A_27a,V0w))) )))).
fof(conj_thm_2Ewellorder_2EWIN__WF2,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Ewellorder_2Ewellorder(A_27a)) => p(ap(c_2Erelation_2EWF(A_27a),f1020(A_27a,V0w))) )))).
fof(ax_thm_2Ewellorder_2Eiseg__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Ewellorder_2Ewellorder(A_27a)) => ! [V1x] : ( mem(V1x,A_27a) => ( ap(ap(c_2Ewellorder_2Eiseg(A_27a),V0w),V1x) = ap(c_2Epred__set_2EGSPEC(A_27a,A_27a),f1021(A_27a,V0w,V1x)) ) ) ) ) )).
fof(conj_thm_2Ewellorder_2Estrict__subset,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r1] : ( mem(V0r1,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1r2] : ( mem(V1r2,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Epair_2Eprod(A_27a,A_27a)),V0r1),V1r2)) => p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Epair_2Eprod(A_27a,A_27a)),ap(c_2Eset__relation_2Estrict(A_27a),V0r1)),ap(c_2Eset__relation_2Estrict(A_27a),V1r2))) ) ) )))).
fof(conj_thm_2Ewellorder_2Etransitive__rrestrict,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ( p(ap(c_2Eset__relation_2Etransitive(A_27a),V0r)) => p(ap(c_2Eset__relation_2Etransitive(A_27a),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V0r),V1s))) ) ) )))).
fof(conj_thm_2Ewellorder_2Eantisym__rrestrict,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ( p(ap(c_2Eset__relation_2Eantisym(A_27a),V0r)) => p(ap(c_2Eset__relation_2Eantisym(A_27a),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V0r),V1s))) ) ) )))).
fof(conj_thm_2Ewellorder_2Elinear__order__rrestrict,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ( p(ap(ap(c_2Eset__relation_2Elinear__order(A_27a),V0r),ap(ap(c_2Epred__set_2EUNION(A_27a),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),V0r)),ap(c_2Eset__relation_2Erange(A_27a,A_27a),V0r)))) => p(ap(ap(c_2Eset__relation_2Elinear__order(A_27a),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V0r),V1s)),ap(ap(c_2Epred__set_2EUNION(A_27a),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V0r),V1s))),ap(c_2Eset__relation_2Erange(A_27a,A_27a),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V0r),V1s))))) ) ) )))).
fof(conj_thm_2Ewellorder_2Ereflexive__rrestrict,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ( p(ap(ap(c_2Eset__relation_2Ereflexive(A_27a),V0r),ap(ap(c_2Epred__set_2EUNION(A_27a),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),V0r)),ap(c_2Eset__relation_2Erange(A_27a,A_27a),V0r)))) => p(ap(ap(c_2Eset__relation_2Ereflexive(A_27a),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V0r),V1s)),ap(ap(c_2Epred__set_2EUNION(A_27a),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V0r),V1s))),ap(c_2Eset__relation_2Erange(A_27a,A_27a),ap(ap(c_2Eset__relation_2Errestrict(A_27a),V0r),V1s))))) ) ) )))).
fof(conj_thm_2Ewellorder_2Ewellorder__rrestrict,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Ewellorder_2Ewellorder(A_27a)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => p(ap(c_2Ewellorder_2Ewellorder(A_27a),ap(ap(c_2Eset__relation_2Errestrict(A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V0w)),V1s))) ) )))).
fof(ax_thm_2Ewellorder_2Ewobound__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1w] : ( mem(V1w,ty_2Ewellorder_2Ewellorder(A_27a)) => ( ap(ap(c_2Ewellorder_2Ewobound(A_27a),V0x),V1w) = ap(c_2Ewellorder_2Ewellorder__ABS(A_27a),ap(ap(c_2Eset__relation_2Errestrict(A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V1w)),ap(ap(c_2Ewellorder_2Eiseg(A_27a),V1w),V0x))) ) ) ) ) )).
fof(conj_thm_2Ewellorder_2EWIN__wobound,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1y] : ( mem(V1y,A_27a) => ! [V2z] : ( mem(V2z,A_27a) => ! [V3w] : ( mem(V3w,ty_2Ewellorder_2Ewellorder(A_27a)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V0x),V1y)),ap(c_2Eset__relation_2Estrict(A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),ap(ap(c_2Ewellorder_2Ewobound(A_27a),V2z),V3w))))) <=> ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V0x),V2z)),ap(c_2Eset__relation_2Estrict(A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V3w)))) & ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1y),V2z)),ap(c_2Eset__relation_2Estrict(A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V3w)))) & p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V0x),V1y)),ap(c_2Eset__relation_2Estrict(A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V3w)))) ) ) ) ) ) ) )))).
fof(conj_thm_2Ewellorder_2EWLE__wobound,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1y] : ( mem(V1y,A_27a) => ! [V2z] : ( mem(V2z,A_27a) => ! [V3w] : ( mem(V3w,ty_2Ewellorder_2Ewellorder(A_27a)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V0x),V1y)),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),ap(ap(c_2Ewellorder_2Ewobound(A_27a),V2z),V3w)))) <=> ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V0x),V2z)),ap(c_2Eset__relation_2Estrict(A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V3w)))) & ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1y),V2z)),ap(c_2Eset__relation_2Estrict(A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V3w)))) & p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V0x),V1y)),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V3w))) ) ) ) ) ) ) )))).
fof(conj_thm_2Ewellorder_2Ewellorder__cases,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Ewellorder_2Ewellorder(A_27a)) => ? [V1s] : ( mem(V1s,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) & ( p(ap(c_2Ewellorder_2Ewellorder(A_27a),V1s)) & ( V0w = ap(c_2Ewellorder_2Ewellorder__ABS(A_27a),V1s) ) ) ) )))).
fof(conj_thm_2Ewellorder_2EWEXTENSION,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0w1] : ( mem(V0w1,ty_2Ewellorder_2Ewellorder(A_27a)) => ! [V1w2] : ( mem(V1w2,ty_2Ewellorder_2Ewellorder(A_27a)) => ( ( V0w1 = V1w2 ) <=> ! [V2a] : ( mem(V2a,A_27a) => ! [V3b] : ( mem(V3b,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2a),V3b)),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V0w1))) <=> p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2a),V3b)),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V1w2))) ) ) ) ) ) )))).
fof(conj_thm_2Ewellorder_2Ewobound2,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0a] : ( mem(V0a,A_27a) => ! [V1b] : ( mem(V1b,A_27a) => ! [V2w] : ( mem(V2w,ty_2Ewellorder_2Ewellorder(A_27a)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V0a),V1b)),ap(c_2Eset__relation_2Estrict(A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V2w)))) => ( ap(ap(c_2Ewellorder_2Ewobound(A_27a),V0a),ap(ap(c_2Ewellorder_2Ewobound(A_27a),V1b),V2w)) = ap(ap(c_2Ewellorder_2Ewobound(A_27a),V0a),V2w) ) ) ) ) )))).
fof(conj_thm_2Ewellorder_2Ewellorder__fromNat,lemma,(! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => p(ap(c_2Ewellorder_2Ewellorder(ty_2Enum_2Enum),ap(c_2Epred__set_2EGSPEC(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),ap(c_2Epair_2EUNCURRY(ty_2Enum_2Enum,ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),bool)),f1023(V0n))))) ))).
fof(conj_thm_2Ewellorder_2EINJ__preserves__transitive,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1f] : ( mem(V1f,arr(A_27a,A_27b)) => ! [V2t] : ( mem(V2t,arr(A_27b,bool)) => ( ( p(ap(c_2Eset__relation_2Etransitive(A_27a),V0r)) & p(ap(ap(ap(c_2Epred__set_2EINJ(A_27a,A_27b),V1f),ap(ap(c_2Epred__set_2EUNION(A_27a),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),V0r)),ap(c_2Eset__relation_2Erange(A_27a,A_27a),V0r))),V2t)) ) => p(ap(c_2Eset__relation_2Etransitive(A_27b),ap(ap(c_2Epred__set_2EIMAGE(ty_2Epair_2Eprod(A_27a,A_27a),ty_2Epair_2Eprod(A_27b,A_27b)),ap(ap(c_2Epair_2E_23_23(A_27a,A_27a,A_27b,A_27b),V1f),V1f)),V0r))) ) ) ) ))))).
fof(conj_thm_2Ewellorder_2EINJ__preserves__antisym,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1f] : ( mem(V1f,arr(A_27a,A_27b)) => ! [V2t] : ( mem(V2t,arr(A_27b,bool)) => ( ( p(ap(c_2Eset__relation_2Eantisym(A_27a),V0r)) & p(ap(ap(ap(c_2Epred__set_2EINJ(A_27a,A_27b),V1f),ap(ap(c_2Epred__set_2EUNION(A_27a),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),V0r)),ap(c_2Eset__relation_2Erange(A_27a,A_27a),V0r))),V2t)) ) => p(ap(c_2Eset__relation_2Eantisym(A_27b),ap(ap(c_2Epred__set_2EIMAGE(ty_2Epair_2Eprod(A_27a,A_27a),ty_2Epair_2Eprod(A_27b,A_27b)),ap(ap(c_2Epair_2E_23_23(A_27a,A_27a,A_27b,A_27b),V1f),V1f)),V0r))) ) ) ) ))))).
fof(conj_thm_2Ewellorder_2EINJ__preserves__linear__order,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1f] : ( mem(V1f,arr(A_27a,A_27b)) => ! [V2t] : ( mem(V2t,arr(A_27b,bool)) => ( ( p(ap(ap(c_2Eset__relation_2Elinear__order(A_27a),V0r),ap(ap(c_2Epred__set_2EUNION(A_27a),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),V0r)),ap(c_2Eset__relation_2Erange(A_27a,A_27a),V0r)))) & p(ap(ap(ap(c_2Epred__set_2EINJ(A_27a,A_27b),V1f),ap(ap(c_2Epred__set_2EUNION(A_27a),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),V0r)),ap(c_2Eset__relation_2Erange(A_27a,A_27a),V0r))),V2t)) ) => p(ap(ap(c_2Eset__relation_2Elinear__order(A_27b),ap(ap(c_2Epred__set_2EIMAGE(ty_2Epair_2Eprod(A_27a,A_27a),ty_2Epair_2Eprod(A_27b,A_27b)),ap(ap(c_2Epair_2E_23_23(A_27a,A_27a,A_27b,A_27b),V1f),V1f)),V0r)),ap(ap(c_2Epred__set_2EIMAGE(A_27a,A_27b),V1f),ap(ap(c_2Epred__set_2EUNION(A_27a),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),V0r)),ap(c_2Eset__relation_2Erange(A_27a,A_27a),V0r))))) ) ) ) ))))).
fof(conj_thm_2Ewellorder_2Edomain__IMAGE__ff,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) =>  ! [A_27d]: ( ne(A_27d) => ! [V0f] : ( mem(V0f,arr(A_27c,A_27a)) => ! [V1g] : ( mem(V1g,arr(A_27d,A_27b)) => ! [V2r] : ( mem(V2r,arr(ty_2Epair_2Eprod(A_27c,A_27d),bool)) => ( ap(c_2Eset__relation_2Edomain(A_27a,A_27b),ap(ap(c_2Epred__set_2EIMAGE(ty_2Epair_2Eprod(A_27c,A_27d),ty_2Epair_2Eprod(A_27a,A_27b)),ap(ap(c_2Epair_2E_23_23(A_27c,A_27d,A_27a,A_27b),V0f),V1g)),V2r)) = ap(ap(c_2Epred__set_2EIMAGE(A_27c,A_27a),V0f),ap(c_2Eset__relation_2Edomain(A_27c,A_27d),V2r)) ) ) ) ))))))).
fof(conj_thm_2Ewellorder_2Erange__IMAGE__ff,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) =>  ! [A_27d]: ( ne(A_27d) => ! [V0f] : ( mem(V0f,arr(A_27c,A_27b)) => ! [V1g] : ( mem(V1g,arr(A_27d,A_27a)) => ! [V2r] : ( mem(V2r,arr(ty_2Epair_2Eprod(A_27c,A_27d),bool)) => ( ap(c_2Eset__relation_2Erange(A_27a,A_27b),ap(ap(c_2Epred__set_2EIMAGE(ty_2Epair_2Eprod(A_27c,A_27d),ty_2Epair_2Eprod(A_27b,A_27a)),ap(ap(c_2Epair_2E_23_23(A_27c,A_27d,A_27b,A_27a),V0f),V1g)),V2r)) = ap(ap(c_2Epred__set_2EIMAGE(A_27d,A_27a),V1g),ap(c_2Eset__relation_2Erange(A_27d,A_27c),V2r)) ) ) ) ))))))).
fof(conj_thm_2Ewellorder_2EINJ__preserves__wellorder,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0r] : ( mem(V0r,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1f] : ( mem(V1f,arr(A_27a,A_27b)) => ! [V2t] : ( mem(V2t,arr(A_27b,bool)) => ( ( p(ap(c_2Ewellorder_2Ewellorder(A_27a),V0r)) & p(ap(ap(ap(c_2Epred__set_2EINJ(A_27a,A_27b),V1f),ap(ap(c_2Epred__set_2EUNION(A_27a),ap(c_2Eset__relation_2Edomain(A_27a,A_27a),V0r)),ap(c_2Eset__relation_2Erange(A_27a,A_27a),V0r))),V2t)) ) => p(ap(c_2Ewellorder_2Ewellorder(A_27b),ap(ap(c_2Epred__set_2EIMAGE(ty_2Epair_2Eprod(A_27a,A_27a),ty_2Epair_2Eprod(A_27b,A_27b)),ap(ap(c_2Epair_2E_23_23(A_27a,A_27a,A_27b,A_27b),V1f),V1f)),V0r))) ) ) ) ))))).
fof(conj_thm_2Ewellorder_2Ewellorder__fromNat__SUM,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => p(ap(c_2Ewellorder_2Ewellorder(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),ap(c_2Epred__set_2EGSPEC(ty_2Epair_2Eprod(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a),ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),ap(c_2Epair_2EUNCURRY(ty_2Enum_2Enum,ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epair_2Eprod(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a),ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),bool)),f1025(A_27a,V0n))))) )))).
fof(ax_thm_2Ewellorder_2EfromNatWO__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(c_2Ewellorder_2EfromNatWO(A_27a),V0n) = ap(c_2Ewellorder_2Ewellorder__ABS(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),ap(c_2Epred__set_2EGSPEC(ty_2Epair_2Eprod(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a),ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),ap(c_2Epair_2EUNCURRY(ty_2Enum_2Enum,ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Epair_2Eprod(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a),ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),bool)),f1025(A_27a,V0n)))) ) ) ) )).
fof(conj_thm_2Ewellorder_2EfromNatWO__11,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0i] : ( mem(V0i,ty_2Enum_2Enum) => ! [V1j] : ( mem(V1j,ty_2Enum_2Enum) => ( ( ap(c_2Ewellorder_2EfromNatWO(A_27a),V0i) = ap(c_2Ewellorder_2EfromNatWO(A_27a),V1j) ) <=> ( V0i = V1j ) ) ) )))).
fof(conj_thm_2Ewellorder_2EelsOf__fromNatWO,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0n] : ( mem(V0n,ty_2Enum_2Enum) => ( ap(c_2Ewellorder_2EelsOf(ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),ap(c_2Ewellorder_2EfromNatWO(A_27a),V0n)) = ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,ty_2Esum_2Esum(ty_2Enum_2Enum,A_27a)),c_2Esum_2EINL(ty_2Enum_2Enum,A_27a)),ap(c_2Epred__set_2Ecount,V0n)) ) )))).
fof(conj_thm_2Ewellorder_2EWLE__WIN,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1y] : ( mem(V1y,A_27a) => ! [V2w] : ( mem(V2w,ty_2Ewellorder_2Ewellorder(A_27a)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V0x),V1y)),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V2w))) => ( ( V0x = V1y ) | p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V0x),V1y)),ap(c_2Eset__relation_2Estrict(A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V2w)))) ) ) ) ) )))).
fof(conj_thm_2Ewellorder_2EelsOf__wobound,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1w] : ( mem(V1w,ty_2Ewellorder_2Ewellorder(A_27a)) => ( ap(c_2Ewellorder_2EelsOf(A_27a),ap(ap(c_2Ewellorder_2Ewobound(A_27a),V0x),V1w)) = ap(c_2Epred__set_2EGSPEC(A_27a,A_27a),f1026(A_27a,V1w,V0x)) ) ) )))).
fof(ax_thm_2Ewellorder_2Eorderiso__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0w1] : ( mem(V0w1,ty_2Ewellorder_2Ewellorder(A_27a)) => ! [V1w2] : ( mem(V1w2,ty_2Ewellorder_2Ewellorder(A_27b)) => ( p(ap(ap(c_2Ewellorder_2Eorderiso(A_27a,A_27b),V0w1),V1w2)) <=> ? [V2f] : ( mem(V2f,arr(A_27a,A_27b)) & ( ( ! [V3x] : ( mem(V3x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V3x),ap(c_2Ewellorder_2EelsOf(A_27a),V0w1))) => p(ap(ap(c_2Ebool_2EIN(A_27b),ap(V2f,V3x)),ap(c_2Ewellorder_2EelsOf(A_27b),V1w2))) ) ) ) & ( ( ! [V4x1] : ( mem(V4x1,A_27a) => ! [V5x2] : ( mem(V5x2,A_27a) => ( ( p(ap(ap(c_2Ebool_2EIN(A_27a),V4x1),ap(c_2Ewellorder_2EelsOf(A_27a),V0w1))) & p(ap(ap(c_2Ebool_2EIN(A_27a),V5x2),ap(c_2Ewellorder_2EelsOf(A_27a),V0w1))) ) => ( ( ap(V2f,V4x1) = ap(V2f,V5x2) ) <=> ( V4x1 = V5x2 ) ) ) ) ) ) & ( ( ! [V6y] : ( mem(V6y,A_27b) => ( p(ap(ap(c_2Ebool_2EIN(A_27b),V6y),ap(c_2Ewellorder_2EelsOf(A_27b),V1w2))) => ? [V7x] : ( mem(V7x,A_27a) & ( p(ap(ap(c_2Ebool_2EIN(A_27a),V7x),ap(c_2Ewellorder_2EelsOf(A_27a),V0w1))) & ( ap(V2f,V7x) = V6y ) ) ) ) ) ) & ! [V8x] : ( mem(V8x,A_27a) => ! [V9y] : ( mem(V9y,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V8x),V9y)),ap(c_2Eset__relation_2Estrict(A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V0w1)))) => p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27b,A_27b)),ap(ap(c_2Epair_2E_2C(A_27b,A_27b),ap(V2f,V8x)),ap(V2f,V9y))),ap(c_2Eset__relation_2Estrict(A_27b),ap(c_2Ewellorder_2Ewellorder__REP(A_27b),V1w2)))) ) ) ) ) ) ) ) ) ) ) ) ) )).
fof(conj_thm_2Ewellorder_2Eorderiso__thm,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0w1] : ( mem(V0w1,ty_2Ewellorder_2Ewellorder(A_27a)) => ! [V1w2] : ( mem(V1w2,ty_2Ewellorder_2Ewellorder(A_27b)) => ( p(ap(ap(c_2Ewellorder_2Eorderiso(A_27a,A_27b),V0w1),V1w2)) <=> ? [V2f] : ( mem(V2f,arr(A_27a,A_27b)) & ( p(ap(ap(ap(c_2Epred__set_2EBIJ(A_27a,A_27b),V2f),ap(c_2Ewellorder_2EelsOf(A_27a),V0w1)),ap(c_2Ewellorder_2EelsOf(A_27b),V1w2))) & ! [V3x] : ( mem(V3x,A_27a) => ! [V4y] : ( mem(V4y,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V3x),V4y)),ap(c_2Eset__relation_2Estrict(A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V0w1)))) => p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27b,A_27b)),ap(ap(c_2Epair_2E_2C(A_27b,A_27b),ap(V2f,V3x)),ap(V2f,V4y))),ap(c_2Eset__relation_2Estrict(A_27b),ap(c_2Ewellorder_2Ewellorder__REP(A_27b),V1w2)))) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Ewellorder_2Eorderiso__REFL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Ewellorder_2Ewellorder(A_27a)) => p(ap(ap(c_2Ewellorder_2Eorderiso(A_27a,A_27a),V0w),V0w)) )))).
fof(conj_thm_2Ewellorder_2Eorderiso__SYM,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0w1] : ( mem(V0w1,ty_2Ewellorder_2Ewellorder(A_27a)) => ! [V1w2] : ( mem(V1w2,ty_2Ewellorder_2Ewellorder(A_27b)) => ( p(ap(ap(c_2Ewellorder_2Eorderiso(A_27a,A_27b),V0w1),V1w2)) => p(ap(ap(c_2Ewellorder_2Eorderiso(A_27b,A_27a),V1w2),V0w1)) ) ) ))))).
fof(conj_thm_2Ewellorder_2Eorderiso__TRANS,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0w1] : ( mem(V0w1,ty_2Ewellorder_2Ewellorder(A_27a)) => ! [V1w2] : ( mem(V1w2,ty_2Ewellorder_2Ewellorder(A_27b)) => ! [V2w3] : ( mem(V2w3,ty_2Ewellorder_2Ewellorder(A_27c)) => ( ( p(ap(ap(c_2Ewellorder_2Eorderiso(A_27a,A_27b),V0w1),V1w2)) & p(ap(ap(c_2Ewellorder_2Eorderiso(A_27b,A_27c),V1w2),V2w3)) ) => p(ap(ap(c_2Ewellorder_2Eorderiso(A_27a,A_27c),V0w1),V2w3)) ) ) ) )))))).
fof(ax_thm_2Ewellorder_2Eorderlt__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0w1] : ( mem(V0w1,ty_2Ewellorder_2Ewellorder(A_27a)) => ! [V1w2] : ( mem(V1w2,ty_2Ewellorder_2Ewellorder(A_27b)) => ( p(ap(ap(c_2Ewellorder_2Eorderlt(A_27a,A_27b),V0w1),V1w2)) <=> ? [V2x] : ( mem(V2x,A_27b) & ( p(ap(ap(c_2Ebool_2EIN(A_27b),V2x),ap(c_2Ewellorder_2EelsOf(A_27b),V1w2))) & p(ap(ap(c_2Ewellorder_2Eorderiso(A_27a,A_27b),V0w1),ap(ap(c_2Ewellorder_2Ewobound(A_27b),V2x),V1w2))) ) ) ) ) ) ) ) )).
fof(conj_thm_2Ewellorder_2Eorderlt__REFL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Ewellorder_2Ewellorder(A_27a)) => ( p(ap(ap(c_2Ewellorder_2Eorderlt(A_27a,A_27a),V0w),V0w)) <=> $false ) )))).
fof(conj_thm_2Ewellorder_2Ewobounds__preserve__bijections,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(A_27a,A_27b)) => ! [V1w1] : ( mem(V1w1,ty_2Ewellorder_2Ewellorder(A_27a)) => ! [V2w2] : ( mem(V2w2,ty_2Ewellorder_2Ewellorder(A_27b)) => ! [V3x] : ( mem(V3x,A_27a) => ( ( p(ap(ap(ap(c_2Epred__set_2EBIJ(A_27a,A_27b),V0f),ap(c_2Ewellorder_2EelsOf(A_27a),V1w1)),ap(c_2Ewellorder_2EelsOf(A_27b),V2w2))) & ( p(ap(ap(c_2Ebool_2EIN(A_27a),V3x),ap(c_2Ewellorder_2EelsOf(A_27a),V1w1))) & ! [V4x] : ( mem(V4x,A_27a) => ! [V5y] : ( mem(V5y,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V4x),V5y)),ap(c_2Eset__relation_2Estrict(A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V1w1)))) => p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27b,A_27b)),ap(ap(c_2Epair_2E_2C(A_27b,A_27b),ap(V0f,V4x)),ap(V0f,V5y))),ap(c_2Eset__relation_2Estrict(A_27b),ap(c_2Ewellorder_2Ewellorder__REP(A_27b),V2w2)))) ) ) ) ) ) => p(ap(ap(ap(c_2Epred__set_2EBIJ(A_27a,A_27b),V0f),ap(c_2Ewellorder_2EelsOf(A_27a),ap(ap(c_2Ewellorder_2Ewobound(A_27a),V3x),V1w1))),ap(c_2Ewellorder_2EelsOf(A_27b),ap(ap(c_2Ewellorder_2Ewobound(A_27b),ap(V0f,V3x)),V2w2)))) ) ) ) ) ))))).
fof(conj_thm_2Ewellorder_2Eorderlt__TRANS,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) => ! [V0w1] : ( mem(V0w1,ty_2Ewellorder_2Ewellorder(A_27a)) => ! [V1w2] : ( mem(V1w2,ty_2Ewellorder_2Ewellorder(A_27b)) => ! [V2w3] : ( mem(V2w3,ty_2Ewellorder_2Ewellorder(A_27c)) => ( ( p(ap(ap(c_2Ewellorder_2Eorderlt(A_27a,A_27b),V0w1),V1w2)) & p(ap(ap(c_2Ewellorder_2Eorderlt(A_27b,A_27c),V1w2),V2w3)) ) => p(ap(ap(c_2Ewellorder_2Eorderlt(A_27a,A_27c),V0w1),V2w3)) ) ) ) )))))).
fof(ax_thm_2Ewellorder_2Ewleast__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Ewellorder_2Ewellorder(A_27a)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ( ap(ap(c_2Ewellorder_2Ewleast(A_27a),V0w),V1s) = ap(c_2Eoption_2Esome(A_27a),f1028(A_27a,V1s,V0w)) ) ) ) ) )).
fof(ax_thm_2Ewellorder_2Ewo2wo__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [A_27b] : ( ne(A_27b) => ! [V0w1] : ( mem(V0w1,ty_2Ewellorder_2Ewellorder(A_27a)) => ! [V1w2] : ( mem(V1w2,ty_2Ewellorder_2Ewellorder(A_27b)) => ( ap(ap(c_2Ewellorder_2Ewo2wo(A_27a,A_27b),V0w1),V1w2) = ap(ap(c_2Erelation_2EWFREC(A_27a,ty_2Eoption_2Eoption(A_27b)),f1030(A_27a,V0w1)),f1034(A_27a,A_27b,V0w1,V1w2)) ) ) ) ) ) )).
fof(conj_thm_2Ewellorder_2Ewo2wo__thm,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0w] : ( mem(V0w,ty_2Ewellorder_2Ewellorder(A_27a)) => ! [V1w2] : ( mem(V1w2,ty_2Ewellorder_2Ewellorder(A_27b)) => ! [V2x] : ( mem(V2x,A_27a) => ( ap(ap(ap(c_2Ewellorder_2Ewo2wo(A_27a,A_27b),V0w),V1w2),V2x) = ap(ap(c_2Ebool_2ELET(arr(ty_2Eoption_2Eoption(A_27b),bool),ty_2Eoption_2Eoption(A_27b)),f1036(A_27b,V1w2)),ap(ap(c_2Epred__set_2EIMAGE(A_27a,ty_2Eoption_2Eoption(A_27b)),ap(ap(c_2Ewellorder_2Ewo2wo(A_27a,A_27b),V0w),V1w2)),ap(ap(c_2Ewellorder_2Eiseg(A_27a),V0w),V2x))) ) ) ) ))))).
fof(conj_thm_2Ewellorder_2Ewleast__IN__wo,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Ewellorder_2Ewellorder(A_27a)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ! [V2x] : ( mem(V2x,A_27a) => ( ( ap(ap(c_2Ewellorder_2Ewleast(A_27a),V0w),V1s) = ap(c_2Eoption_2ESOME(A_27a),V2x) ) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),ap(c_2Ewellorder_2EelsOf(A_27a),V0w))) & ( ( ~~ p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V1s)) ) & ! [V3y] : ( mem(V3y,A_27a) => ( ( p(ap(ap(c_2Ebool_2EIN(A_27a),V3y),ap(c_2Ewellorder_2EelsOf(A_27a),V0w))) & ( ( ~~ p(ap(ap(c_2Ebool_2EIN(A_27a),V3y),V1s)) ) & ( ~~ ( V2x = V3y ) ) ) ) => p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2x),V3y)),ap(c_2Eset__relation_2Estrict(A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V0w)))) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Ewellorder_2Ewleast__EQ__NONE,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Ewellorder_2Ewellorder(A_27a)) => ! [V1s] : ( mem(V1s,arr(A_27a,bool)) => ( ( ap(ap(c_2Ewellorder_2Ewleast(A_27a),V0w),V1s) = c_2Eoption_2ENONE(A_27a) ) => p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Ewellorder_2EelsOf(A_27a),V0w)),V1s)) ) ) )))).
fof(conj_thm_2Ewellorder_2Ewo2wo__IN__w2,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0w1] : ( mem(V0w1,ty_2Ewellorder_2Ewellorder(A_27a)) => ! [V1w2] : ( mem(V1w2,ty_2Ewellorder_2Ewellorder(A_27b)) => ! [V2x] : ( mem(V2x,A_27a) => ! [V3y] : ( mem(V3y,A_27b) => ( ( ap(ap(ap(c_2Ewellorder_2Ewo2wo(A_27a,A_27b),V0w1),V1w2),V2x) = ap(c_2Eoption_2ESOME(A_27b),V3y) ) => p(ap(ap(c_2Ebool_2EIN(A_27b),V3y),ap(c_2Ewellorder_2EelsOf(A_27b),V1w2))) ) ) ) ) ))))).
fof(conj_thm_2Ewellorder_2EIMAGE__wo2wo__SUBSET,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0w1] : ( mem(V0w1,ty_2Ewellorder_2Ewellorder(A_27b)) => ! [V1w2] : ( mem(V1w2,ty_2Ewellorder_2Ewellorder(A_27a)) => ! [V2x] : ( mem(V2x,A_27b) => p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Eoption_2Eoption(A_27a),A_27a),c_2Eoption_2ETHE(A_27a)),ap(ap(c_2Epred__set_2EDELETE(ty_2Eoption_2Eoption(A_27a)),ap(ap(c_2Epred__set_2EIMAGE(A_27b,ty_2Eoption_2Eoption(A_27a)),ap(ap(c_2Ewellorder_2Ewo2wo(A_27b,A_27a),V0w1),V1w2)),ap(ap(c_2Ewellorder_2Eiseg(A_27b),V0w1),V2x))),c_2Eoption_2ENONE(A_27a)))),ap(c_2Ewellorder_2EelsOf(A_27a),V1w2))) ) ) ))))).
fof(conj_thm_2Ewellorder_2Ewo2wo__EQ__NONE,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0w1] : ( mem(V0w1,ty_2Ewellorder_2Ewellorder(A_27a)) => ! [V1w2] : ( mem(V1w2,ty_2Ewellorder_2Ewellorder(A_27b)) => ! [V2x] : ( mem(V2x,A_27a) => ( ( ap(ap(ap(c_2Ewellorder_2Ewo2wo(A_27a,A_27b),V0w1),V1w2),V2x) = c_2Eoption_2ENONE(A_27b) ) => ! [V3y] : ( mem(V3y,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2x),V3y)),ap(c_2Eset__relation_2Estrict(A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V0w1)))) => ( ap(ap(ap(c_2Ewellorder_2Ewo2wo(A_27a,A_27b),V0w1),V1w2),V3y) = c_2Eoption_2ENONE(A_27b) ) ) ) ) ) ) ))))).
fof(conj_thm_2Ewellorder_2Ewo2wo__EQ__SOME__downwards,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0w1] : ( mem(V0w1,ty_2Ewellorder_2Ewellorder(A_27a)) => ! [V1w2] : ( mem(V1w2,ty_2Ewellorder_2Ewellorder(A_27b)) => ! [V2x] : ( mem(V2x,A_27a) => ! [V3y] : ( mem(V3y,A_27b) => ( ( ap(ap(ap(c_2Ewellorder_2Ewo2wo(A_27a,A_27b),V0w1),V1w2),V2x) = ap(c_2Eoption_2ESOME(A_27b),V3y) ) => ! [V4x0] : ( mem(V4x0,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V4x0),V2x)),ap(c_2Eset__relation_2Estrict(A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V0w1)))) => ? [V5y0] : ( mem(V5y0,A_27b) & ( ap(ap(ap(c_2Ewellorder_2Ewo2wo(A_27a,A_27b),V0w1),V1w2),V4x0) = ap(c_2Eoption_2ESOME(A_27b),V5y0) ) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Ewellorder_2Emono__woseg,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0x1] : ( mem(V0x1,A_27a) => ! [V1x2] : ( mem(V1x2,A_27a) => ! [V2w1] : ( mem(V2w1,ty_2Ewellorder_2Ewellorder(A_27a)) => ! [V3w2] : ( mem(V3w2,ty_2Ewellorder_2Ewellorder(A_27b)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V0x1),V1x2)),ap(c_2Eset__relation_2Estrict(A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V2w1)))) => p(ap(ap(c_2Epred__set_2ESUBSET(A_27b),ap(ap(c_2Epred__set_2EIMAGE(ty_2Eoption_2Eoption(A_27b),A_27b),c_2Eoption_2ETHE(A_27b)),ap(ap(c_2Epred__set_2EDELETE(ty_2Eoption_2Eoption(A_27b)),ap(ap(c_2Epred__set_2EIMAGE(A_27a,ty_2Eoption_2Eoption(A_27b)),ap(ap(c_2Ewellorder_2Ewo2wo(A_27a,A_27b),V2w1),V3w2)),ap(ap(c_2Ewellorder_2Eiseg(A_27a),V2w1),V0x1))),c_2Eoption_2ENONE(A_27b)))),ap(ap(c_2Epred__set_2EIMAGE(ty_2Eoption_2Eoption(A_27b),A_27b),c_2Eoption_2ETHE(A_27b)),ap(ap(c_2Epred__set_2EDELETE(ty_2Eoption_2Eoption(A_27b)),ap(ap(c_2Epred__set_2EIMAGE(A_27a,ty_2Eoption_2Eoption(A_27b)),ap(ap(c_2Ewellorder_2Ewo2wo(A_27a,A_27b),V2w1),V3w2)),ap(ap(c_2Ewellorder_2Eiseg(A_27a),V2w1),V1x2))),c_2Eoption_2ENONE(A_27b))))) ) ) ) ) ))))).
fof(conj_thm_2Ewellorder_2Ewo2wo__11,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0x1] : ( mem(V0x1,A_27a) => ! [V1w1] : ( mem(V1w1,ty_2Ewellorder_2Ewellorder(A_27a)) => ! [V2x2] : ( mem(V2x2,A_27a) => ! [V3w2] : ( mem(V3w2,ty_2Ewellorder_2Ewellorder(A_27b)) => ! [V4y] : ( mem(V4y,A_27b) => ( ( p(ap(ap(c_2Ebool_2EIN(A_27a),V0x1),ap(c_2Ewellorder_2EelsOf(A_27a),V1w1))) & ( p(ap(ap(c_2Ebool_2EIN(A_27a),V2x2),ap(c_2Ewellorder_2EelsOf(A_27a),V1w1))) & ( ( ap(ap(ap(c_2Ewellorder_2Ewo2wo(A_27a,A_27b),V1w1),V3w2),V0x1) = ap(c_2Eoption_2ESOME(A_27b),V4y) ) & ( ap(ap(ap(c_2Ewellorder_2Ewo2wo(A_27a,A_27b),V1w1),V3w2),V2x2) = ap(c_2Eoption_2ESOME(A_27b),V4y) ) ) ) ) => ( V0x1 = V2x2 ) ) ) ) ) ) ))))).
fof(conj_thm_2Ewellorder_2Ewleast__SUBSET,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Ewellorder_2Ewellorder(A_27a)) => ! [V1s1] : ( mem(V1s1,arr(A_27a,bool)) => ! [V2x] : ( mem(V2x,A_27a) => ! [V3s2] : ( mem(V3s2,arr(A_27a,bool)) => ! [V4y] : ( mem(V4y,A_27a) => ( ( ( ap(ap(c_2Ewellorder_2Ewleast(A_27a),V0w),V1s1) = ap(c_2Eoption_2ESOME(A_27a),V2x) ) & ( ( ap(ap(c_2Ewellorder_2Ewleast(A_27a),V0w),V3s2) = ap(c_2Eoption_2ESOME(A_27a),V4y) ) & p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),V1s1),V3s2)) ) ) => ( ( V2x = V4y ) | p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2x),V4y)),ap(c_2Eset__relation_2Estrict(A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V0w)))) ) ) ) ) ) ) )))).
fof(conj_thm_2Ewellorder_2Ewo2wo__mono,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0w1] : ( mem(V0w1,ty_2Ewellorder_2Ewellorder(A_27b)) => ! [V1w2] : ( mem(V1w2,ty_2Ewellorder_2Ewellorder(A_27a)) => ! [V2x0] : ( mem(V2x0,A_27b) => ! [V3y0] : ( mem(V3y0,A_27a) => ! [V4x] : ( mem(V4x,A_27b) => ! [V5y] : ( mem(V5y,A_27a) => ( ( ( ap(ap(ap(c_2Ewellorder_2Ewo2wo(A_27b,A_27a),V0w1),V1w2),V2x0) = ap(c_2Eoption_2ESOME(A_27a),V3y0) ) & ( ( ap(ap(ap(c_2Ewellorder_2Ewo2wo(A_27b,A_27a),V0w1),V1w2),V4x) = ap(c_2Eoption_2ESOME(A_27a),V5y) ) & p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27b,A_27b)),ap(ap(c_2Epair_2E_2C(A_27b,A_27b),V2x0),V4x)),ap(c_2Eset__relation_2Estrict(A_27b),ap(c_2Ewellorder_2Ewellorder__REP(A_27b),V0w1)))) ) ) => p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V3y0),V5y)),ap(c_2Eset__relation_2Estrict(A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V1w2)))) ) ) ) ) ) ) ))))).
fof(conj_thm_2Ewellorder_2Ewo2wo__ONTO,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1w1] : ( mem(V1w1,ty_2Ewellorder_2Ewellorder(A_27a)) => ! [V2w2] : ( mem(V2w2,ty_2Ewellorder_2Ewellorder(A_27b)) => ! [V3y] : ( mem(V3y,A_27b) => ! [V4y0] : ( mem(V4y0,A_27b) => ( ( p(ap(ap(c_2Ebool_2EIN(A_27a),V0x),ap(c_2Ewellorder_2EelsOf(A_27a),V1w1))) & ( ( ap(ap(ap(c_2Ewellorder_2Ewo2wo(A_27a,A_27b),V1w1),V2w2),V0x) = ap(c_2Eoption_2ESOME(A_27b),V3y) ) & p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27b,A_27b)),ap(ap(c_2Epair_2E_2C(A_27b,A_27b),V4y0),V3y)),ap(c_2Eset__relation_2Estrict(A_27b),ap(c_2Ewellorder_2Ewellorder__REP(A_27b),V2w2)))) ) ) => ? [V5x0] : ( mem(V5x0,A_27a) & ( p(ap(ap(c_2Ebool_2EIN(A_27a),V5x0),ap(c_2Ewellorder_2EelsOf(A_27a),V1w1))) & ( ap(ap(ap(c_2Ewellorder_2Ewo2wo(A_27a,A_27b),V1w1),V2w2),V5x0) = ap(c_2Eoption_2ESOME(A_27b),V4y0) ) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Ewellorder_2Ewo2wo__EQ__NONE__woseg,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0w1] : ( mem(V0w1,ty_2Ewellorder_2Ewellorder(A_27b)) => ! [V1w2] : ( mem(V1w2,ty_2Ewellorder_2Ewellorder(A_27a)) => ! [V2x] : ( mem(V2x,A_27b) => ( ( ap(ap(ap(c_2Ewellorder_2Ewo2wo(A_27b,A_27a),V0w1),V1w2),V2x) = c_2Eoption_2ENONE(A_27a) ) => ( ap(c_2Ewellorder_2EelsOf(A_27a),V1w2) = ap(ap(c_2Epred__set_2EIMAGE(ty_2Eoption_2Eoption(A_27a),A_27a),c_2Eoption_2ETHE(A_27a)),ap(ap(c_2Epred__set_2EDELETE(ty_2Eoption_2Eoption(A_27a)),ap(ap(c_2Epred__set_2EIMAGE(A_27b,ty_2Eoption_2Eoption(A_27a)),ap(ap(c_2Ewellorder_2Ewo2wo(A_27b,A_27a),V0w1),V1w2)),ap(ap(c_2Ewellorder_2Eiseg(A_27b),V0w1),V2x))),c_2Eoption_2ENONE(A_27a))) ) ) ) ) ))))).
fof(conj_thm_2Ewellorder_2Eorderlt__trichotomy,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0w1] : ( mem(V0w1,ty_2Ewellorder_2Ewellorder(A_27a)) => ! [V1w2] : ( mem(V1w2,ty_2Ewellorder_2Ewellorder(A_27b)) => ( p(ap(ap(c_2Ewellorder_2Eorderlt(A_27a,A_27b),V0w1),V1w2)) | ( p(ap(ap(c_2Ewellorder_2Eorderiso(A_27a,A_27b),V0w1),V1w2)) | p(ap(ap(c_2Ewellorder_2Eorderlt(A_27b,A_27a),V1w2),V0w1)) ) ) ) ))))).
fof(ax_thm_2Ewellorder_2EwZERO__def,axiom,( ! [A_27a] : ( ne(A_27a) => ( c_2Ewellorder_2EwZERO(A_27a) = ap(c_2Ewellorder_2Ewellorder__ABS(A_27a),c_2Epred__set_2EEMPTY(ty_2Epair_2Eprod(A_27a,A_27a))) ) ) )).
fof(conj_thm_2Ewellorder_2EelsOf__wZERO,lemma,( ! [A_27a]: ( ne(A_27a) => ( ap(c_2Ewellorder_2EelsOf(A_27a),c_2Ewellorder_2EwZERO(A_27a)) = c_2Epred__set_2EEMPTY(A_27a) )))).
fof(conj_thm_2Ewellorder_2EWIN__wZERO,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1y] : ( mem(V1y,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V0x),V1y)),ap(c_2Eset__relation_2Estrict(A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),c_2Ewellorder_2EwZERO(A_27a))))) <=> $false ) ) )))).
fof(conj_thm_2Ewellorder_2EWLE__wZERO,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1y] : ( mem(V1y,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V0x),V1y)),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),c_2Ewellorder_2EwZERO(A_27a)))) <=> $false ) ) )))).
fof(conj_thm_2Ewellorder_2Eorderiso__wZERO,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0w] : ( mem(V0w,ty_2Ewellorder_2Ewellorder(A_27b)) => ( p(ap(ap(c_2Ewellorder_2Eorderiso(A_27a,A_27b),c_2Ewellorder_2EwZERO(A_27a)),V0w)) <=> ( V0w = c_2Ewellorder_2EwZERO(A_27b) ) ) ))))).
fof(conj_thm_2Ewellorder_2EelsOf__EQ__EMPTY,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Ewellorder_2Ewellorder(A_27a)) => ( ( ap(c_2Ewellorder_2EelsOf(A_27a),V0w) = c_2Epred__set_2EEMPTY(A_27a) ) <=> ( V0w = c_2Ewellorder_2EwZERO(A_27a) ) ) )))).
fof(conj_thm_2Ewellorder_2ELT__wZERO,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0w] : ( mem(V0w,ty_2Ewellorder_2Ewellorder(A_27a)) => ( p(ap(ap(c_2Ewellorder_2Eorderlt(A_27a,A_27b),V0w),c_2Ewellorder_2EwZERO(A_27b))) <=> $false ) ))))).
fof(conj_thm_2Ewellorder_2Eorderlt__WF,lemma,( ! [A_27a]: ( ne(A_27a) => p(ap(c_2Erelation_2EWF(ty_2Ewellorder_2Ewellorder(A_27a)),c_2Ewellorder_2Eorderlt(A_27a,A_27a)))))).
fof(conj_thm_2Ewellorder_2Eorderlt__orderiso,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) =>  ! [A_27c]: ( ne(A_27c) =>  ! [A_27d]: ( ne(A_27d) => ! [V0x0] : ( mem(V0x0,ty_2Ewellorder_2Ewellorder(A_27a)) => ! [V1y0] : ( mem(V1y0,ty_2Ewellorder_2Ewellorder(A_27b)) => ! [V2a0] : ( mem(V2a0,ty_2Ewellorder_2Ewellorder(A_27c)) => ! [V3b0] : ( mem(V3b0,ty_2Ewellorder_2Ewellorder(A_27d)) => ( ( p(ap(ap(c_2Ewellorder_2Eorderiso(A_27a,A_27b),V0x0),V1y0)) & p(ap(ap(c_2Ewellorder_2Eorderiso(A_27c,A_27d),V2a0),V3b0)) ) => ( p(ap(ap(c_2Ewellorder_2Eorderlt(A_27a,A_27c),V0x0),V2a0)) <=> p(ap(ap(c_2Ewellorder_2Eorderlt(A_27b,A_27d),V1y0),V3b0)) ) ) ) ) ) ))))))).
fof(ax_thm_2Ewellorder_2Efinite__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0w] : ( mem(V0w,ty_2Ewellorder_2Ewellorder(A_27a)) => ( p(ap(c_2Ewellorder_2Efinite(A_27a),V0w)) <=> p(ap(c_2Epred__set_2EFINITE(A_27a),ap(c_2Ewellorder_2EelsOf(A_27a),V0w))) ) ) ) )).
fof(conj_thm_2Ewellorder_2Efinite__iso,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0w1] : ( mem(V0w1,ty_2Ewellorder_2Ewellorder(A_27a)) => ! [V1w2] : ( mem(V1w2,ty_2Ewellorder_2Ewellorder(A_27b)) => ( p(ap(ap(c_2Ewellorder_2Eorderiso(A_27a,A_27b),V0w1),V1w2)) => ( p(ap(c_2Ewellorder_2Efinite(A_27a),V0w1)) <=> p(ap(c_2Ewellorder_2Efinite(A_27b),V1w2)) ) ) ) ))))).
fof(conj_thm_2Ewellorder_2Efinite__wZERO,lemma,( ! [A_27a]: ( ne(A_27a) => p(ap(c_2Ewellorder_2Efinite(A_27a),c_2Ewellorder_2EwZERO(A_27a)))))).
fof(conj_thm_2Ewellorder_2Eorderiso__unique,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f1] : ( mem(V0f1,arr(A_27a,A_27b)) => ! [V1w1] : ( mem(V1w1,ty_2Ewellorder_2Ewellorder(A_27a)) => ! [V2w2] : ( mem(V2w2,ty_2Ewellorder_2Ewellorder(A_27b)) => ! [V3f2] : ( mem(V3f2,arr(A_27a,A_27b)) => ( ( p(ap(ap(ap(c_2Epred__set_2EBIJ(A_27a,A_27b),V0f1),ap(c_2Ewellorder_2EelsOf(A_27a),V1w1)),ap(c_2Ewellorder_2EelsOf(A_27b),V2w2))) & ( p(ap(ap(ap(c_2Epred__set_2EBIJ(A_27a,A_27b),V3f2),ap(c_2Ewellorder_2EelsOf(A_27a),V1w1)),ap(c_2Ewellorder_2EelsOf(A_27b),V2w2))) & ( ( ! [V4x] : ( mem(V4x,A_27a) => ! [V5y] : ( mem(V5y,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V4x),V5y)),ap(c_2Eset__relation_2Estrict(A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V1w1)))) => p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27b,A_27b)),ap(ap(c_2Epair_2E_2C(A_27b,A_27b),ap(V0f1,V4x)),ap(V0f1,V5y))),ap(c_2Eset__relation_2Estrict(A_27b),ap(c_2Ewellorder_2Ewellorder__REP(A_27b),V2w2)))) ) ) ) ) & ! [V6x] : ( mem(V6x,A_27a) => ! [V7y] : ( mem(V7y,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V6x),V7y)),ap(c_2Eset__relation_2Estrict(A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V1w1)))) => p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27b,A_27b)),ap(ap(c_2Epair_2E_2C(A_27b,A_27b),ap(V3f2,V6x)),ap(V3f2,V7y))),ap(c_2Eset__relation_2Estrict(A_27b),ap(c_2Ewellorder_2Ewellorder__REP(A_27b),V2w2)))) ) ) ) ) ) ) => ! [V8x] : ( mem(V8x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V8x),ap(c_2Ewellorder_2EelsOf(A_27a),V1w1))) => ( ap(V0f1,V8x) = ap(V3f2,V8x) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Ewellorder_2Eseteq__wlog,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0P] : ( mem(V0P,arr(A_27a,arr(A_27a,bool))) => ! [V1f] : ( mem(V1f,arr(A_27a,arr(A_27b,bool))) => ( ( ( ! [V2a] : ( mem(V2a,A_27a) => ! [V3b] : ( mem(V3b,A_27a) => ( p(ap(ap(V0P,V2a),V3b)) => p(ap(ap(V0P,V3b),V2a)) ) ) ) ) & ! [V4x] : ( mem(V4x,A_27b) => ! [V5a] : ( mem(V5a,A_27a) => ! [V6b] : ( mem(V6b,A_27a) => ( ( p(ap(ap(V0P,V5a),V6b)) & p(ap(ap(c_2Ebool_2EIN(A_27b),V4x),ap(V1f,V5a))) ) => p(ap(ap(c_2Ebool_2EIN(A_27b),V4x),ap(V1f,V6b))) ) ) ) ) ) => ! [V7a] : ( mem(V7a,A_27a) => ! [V8b] : ( mem(V8b,A_27a) => ( p(ap(ap(V0P,V7a),V8b)) => ( ap(V1f,V7a) = ap(V1f,V8b) ) ) ) ) ) ) ))))).
fof(conj_thm_2Ewellorder_2Ewo__INDUCTION,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(A_27a,bool)) => ! [V1w] : ( mem(V1w,ty_2Ewellorder_2Ewellorder(A_27a)) => ( ( ! [V2x] : ( mem(V2x,A_27a) => ( ( ! [V3y] : ( mem(V3y,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V3y),V2x)),ap(c_2Eset__relation_2Estrict(A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V1w)))) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V3y),ap(c_2Ewellorder_2EelsOf(A_27a),V1w))) => p(ap(V0P,V3y)) ) ) ) ) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),ap(c_2Ewellorder_2EelsOf(A_27a),V1w))) => p(ap(V0P,V2x)) ) ) ) ) => ! [V4x] : ( mem(V4x,A_27a) => ( p(ap(ap(c_2Ebool_2EIN(A_27a),V4x),ap(c_2Ewellorder_2EelsOf(A_27a),V1w))) => p(ap(V0P,V4x)) ) ) ) ) )))).
fof(conj_thm_2Ewellorder_2EFORALL__NUM,lemma,(! [V0P] : ( mem(V0P,arr(ty_2Enum_2Enum,bool)) => ( ( ! [V1n] : ( mem(V1n,ty_2Enum_2Enum) => p(ap(V0P,V1n)) ) ) <=> ( p(ap(V0P,c_2Enum_2E0)) & ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => p(ap(V0P,ap(c_2Enum_2ESUC,V2n))) ) ) ) ))).
fof(conj_thm_2Ewellorder_2Estrict__UNION,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0r1] : ( mem(V0r1,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1r2] : ( mem(V1r2,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ap(c_2Eset__relation_2Estrict(A_27a),ap(ap(c_2Epred__set_2EUNION(ty_2Epair_2Eprod(A_27a,A_27a)),V0r1),V1r2)) = ap(ap(c_2Epred__set_2EUNION(ty_2Epair_2Eprod(A_27a,A_27a)),ap(c_2Eset__relation_2Estrict(A_27a),V0r1)),ap(c_2Eset__relation_2Estrict(A_27a),V1r2)) ) ) )))).
fof(conj_thm_2Ewellorder_2EWLE__WIN__EQ,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1y] : ( mem(V1y,A_27a) => ! [V2w] : ( mem(V2w,ty_2Ewellorder_2Ewellorder(A_27a)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V0x),V1y)),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V2w))) <=> ( ( ( V0x = V1y ) & p(ap(ap(c_2Ebool_2EIN(A_27a),V0x),ap(c_2Ewellorder_2EelsOf(A_27a),V2w))) ) | p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V0x),V1y)),ap(c_2Eset__relation_2Estrict(A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V2w)))) ) ) ) ) )))).
fof(ax_thm_2Ewellorder_2Eremove__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0e] : ( mem(V0e,A_27a) => ! [V1w] : ( mem(V1w,ty_2Ewellorder_2Ewellorder(A_27a)) => ( ap(ap(c_2Ewellorder_2Eremove(A_27a),V0e),V1w) = ap(c_2Ewellorder_2Ewellorder__ABS(A_27a),ap(c_2Epred__set_2EGSPEC(ty_2Epair_2Eprod(A_27a,A_27a),ty_2Epair_2Eprod(A_27a,A_27a)),ap(c_2Epair_2EUNCURRY(A_27a,A_27a,ty_2Epair_2Eprod(ty_2Epair_2Eprod(A_27a,A_27a),bool)),f1038(A_27a,V0e,V1w)))) ) ) ) ) )).
fof(conj_thm_2Ewellorder_2Ewellorder__remove,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0e] : ( mem(V0e,A_27a) => ! [V1w] : ( mem(V1w,ty_2Ewellorder_2Ewellorder(A_27a)) => p(ap(c_2Ewellorder_2Ewellorder(A_27a),ap(c_2Epred__set_2EGSPEC(ty_2Epair_2Eprod(A_27a,A_27a),ty_2Epair_2Eprod(A_27a,A_27a)),ap(c_2Epair_2EUNCURRY(A_27a,A_27a,ty_2Epair_2Eprod(ty_2Epair_2Eprod(A_27a,A_27a),bool)),f1038(A_27a,V0e,V1w))))) ) )))).
fof(conj_thm_2Ewellorder_2EelsOf__remove,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0e] : ( mem(V0e,A_27a) => ! [V1w] : ( mem(V1w,ty_2Ewellorder_2Ewellorder(A_27a)) => ( ap(c_2Ewellorder_2EelsOf(A_27a),ap(ap(c_2Ewellorder_2Eremove(A_27a),V0e),V1w)) = ap(ap(c_2Epred__set_2EDELETE(A_27a),ap(c_2Ewellorder_2EelsOf(A_27a),V1w)),V0e) ) ) )))).
fof(conj_thm_2Ewellorder_2EWIN__remove,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1y] : ( mem(V1y,A_27a) => ! [V2e] : ( mem(V2e,A_27a) => ! [V3w] : ( mem(V3w,ty_2Ewellorder_2Ewellorder(A_27a)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V0x),V1y)),ap(c_2Eset__relation_2Estrict(A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),ap(ap(c_2Ewellorder_2Eremove(A_27a),V2e),V3w))))) <=> ( ( ~~ ( V0x = V2e ) ) & ( ( ~~ ( V1y = V2e ) ) & p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V0x),V1y)),ap(c_2Eset__relation_2Estrict(A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V3w)))) ) ) ) ) ) ) )))).
fof(ax_thm_2Ewellorder_2EADD1__def,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0e] : ( mem(V0e,A_27a) => ! [V1w] : ( mem(V1w,ty_2Ewellorder_2Ewellorder(A_27a)) => ( ap(ap(c_2Ewellorder_2EADD1(A_27a),V0e),V1w) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Ewellorder_2Ewellorder(A_27a)),ap(ap(c_2Ebool_2EIN(A_27a),V0e),ap(c_2Ewellorder_2EelsOf(A_27a),V1w))),V1w),ap(c_2Ewellorder_2Ewellorder__ABS(A_27a),ap(ap(c_2Epred__set_2EUNION(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epred__set_2EUNION(ty_2Epair_2Eprod(A_27a,A_27a)),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V1w)),ap(c_2Epred__set_2EGSPEC(ty_2Epair_2Eprod(A_27a,A_27a),A_27a),f1039(A_27a,V0e,V1w)))),ap(ap(c_2Epred__set_2EINSERT(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V0e),V0e)),c_2Epred__set_2EEMPTY(ty_2Epair_2Eprod(A_27a,A_27a)))))) ) ) ) ) )).
fof(conj_thm_2Ewellorder_2Ewellorder__ADD1,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0e] : ( mem(V0e,A_27a) => ! [V1w] : ( mem(V1w,ty_2Ewellorder_2Ewellorder(A_27a)) => ( ( ~~ p(ap(ap(c_2Ebool_2EIN(A_27a),V0e),ap(c_2Ewellorder_2EelsOf(A_27a),V1w))) ) => p(ap(c_2Ewellorder_2Ewellorder(A_27a),ap(ap(c_2Epred__set_2EUNION(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epred__set_2EUNION(ty_2Epair_2Eprod(A_27a,A_27a)),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V1w)),ap(c_2Epred__set_2EGSPEC(ty_2Epair_2Eprod(A_27a,A_27a),A_27a),f1039(A_27a,V0e,V1w)))),ap(ap(c_2Epred__set_2EINSERT(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V0e),V0e)),c_2Epred__set_2EEMPTY(ty_2Epair_2Eprod(A_27a,A_27a)))))) ) ) )))).
fof(conj_thm_2Ewellorder_2EelsOf__ADD1,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0e] : ( mem(V0e,A_27a) => ! [V1w] : ( mem(V1w,ty_2Ewellorder_2Ewellorder(A_27a)) => ( ap(c_2Ewellorder_2EelsOf(A_27a),ap(ap(c_2Ewellorder_2EADD1(A_27a),V0e),V1w)) = ap(ap(c_2Epred__set_2EINSERT(A_27a),V0e),ap(c_2Ewellorder_2EelsOf(A_27a),V1w)) ) ) )))).
fof(conj_thm_2Ewellorder_2EWIN__ADD1,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0x] : ( mem(V0x,A_27a) => ! [V1y] : ( mem(V1y,A_27a) => ! [V2e] : ( mem(V2e,A_27a) => ! [V3w] : ( mem(V3w,ty_2Ewellorder_2Ewellorder(A_27a)) => ( p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V0x),V1y)),ap(c_2Eset__relation_2Estrict(A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),ap(ap(c_2Ewellorder_2EADD1(A_27a),V2e),V3w))))) <=> ( ( ( ~~ p(ap(ap(c_2Ebool_2EIN(A_27a),V2e),ap(c_2Ewellorder_2EelsOf(A_27a),V3w))) ) & ( p(ap(ap(c_2Ebool_2EIN(A_27a),V0x),ap(c_2Ewellorder_2EelsOf(A_27a),V3w))) & ( V1y = V2e ) ) ) | p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(A_27a,A_27a)),ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V0x),V1y)),ap(c_2Eset__relation_2Estrict(A_27a),ap(c_2Ewellorder_2Ewellorder__REP(A_27a),V3w)))) ) ) ) ) ) )))).
fof(conj_thm_2Ewellorder_2EelsOf__cardeq__iso,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0f] : ( mem(V0f,arr(A_27b,A_27a)) => ! [V1wo] : ( mem(V1wo,ty_2Ewellorder_2Ewellorder(A_27b)) => ( p(ap(ap(ap(c_2Epred__set_2EINJ(A_27b,A_27a),V0f),ap(c_2Ewellorder_2EelsOf(A_27b),V1wo)),c_2Epred__set_2EUNIV(A_27a))) => ? [V2wo_27] : ( mem(V2wo_27,ty_2Ewellorder_2Ewellorder(A_27a)) & p(ap(ap(c_2Ewellorder_2Eorderiso(A_27b,A_27a),V1wo),V2wo_27)) ) ) ) ))))).
fof(conj_thm_2Ewellorder_2Eallsets__wellorderable,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0s] : ( mem(V0s,arr(A_27a,bool)) => ? [V1wo] : ( mem(V1wo,ty_2Ewellorder_2Ewellorder(A_27a)) & ( ap(c_2Ewellorder_2EelsOf(A_27a),V1wo) = V0s ) ) )))).
fof(conj_thm_2Ewellorder_2EWF,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0_3C_3C] : ( mem(V0_3C_3C,arr(A_27a,arr(A_27a,bool))) => ( p(ap(c_2Erelation_2EWF(A_27a),V0_3C_3C)) <=> ! [V1P] : ( mem(V1P,arr(A_27a,bool)) => ( ( ? [V2x] : ( mem(V2x,A_27a) & p(ap(V1P,V2x)) ) ) => ? [V3x] : ( mem(V3x,A_27a) & ( p(ap(V1P,V3x)) & ! [V4y] : ( mem(V4y,A_27a) => ( p(ap(ap(V0_3C_3C,V4y),V3x)) => ( ~~ p(ap(V1P,V4y)) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Ewellorder_2EWF__EQ,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0_3C_3C] : ( mem(V0_3C_3C,arr(A_27a,arr(A_27a,bool))) => ( p(ap(c_2Erelation_2EWF(A_27a),V0_3C_3C)) <=> ! [V1P] : ( mem(V1P,arr(A_27a,bool)) => ( ( ? [V2x] : ( mem(V2x,A_27a) & p(ap(V1P,V2x)) ) ) <=> ? [V3x] : ( mem(V3x,A_27a) & ( p(ap(V1P,V3x)) & ! [V4y] : ( mem(V4y,A_27a) => ( p(ap(ap(V0_3C_3C,V4y),V3x)) => ( ~~ p(ap(V1P,V4y)) ) ) ) ) ) ) ) ) )))).
fof(conj_thm_2Ewellorder_2EWF__IND,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0_3C_3C] : ( mem(V0_3C_3C,arr(A_27a,arr(A_27a,bool))) => ( p(ap(c_2Erelation_2EWF(A_27a),V0_3C_3C)) <=> ! [V1P] : ( mem(V1P,arr(A_27a,bool)) => ( ( ! [V2x] : ( mem(V2x,A_27a) => ( ( ! [V3y] : ( mem(V3y,A_27a) => ( p(ap(ap(V0_3C_3C,V3y),V2x)) => p(ap(V1P,V3y)) ) ) ) => p(ap(V1P,V2x)) ) ) ) => ! [V4x] : ( mem(V4x,A_27a) => p(ap(V1P,V4x)) ) ) ) ) )))).
fof(conj_thm_2Ewellorder_2EWF__DCHAIN,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0_3C_3C] : ( mem(V0_3C_3C,arr(A_27a,arr(A_27a,bool))) => ( p(ap(c_2Erelation_2EWF(A_27a),V0_3C_3C)) <=> ( ~~ ? [V1s] : ( mem(V1s,arr(ty_2Enum_2Enum,A_27a)) & ! [V2n] : ( mem(V2n,ty_2Enum_2Enum) => p(ap(ap(V0_3C_3C,ap(V1s,ap(c_2Enum_2ESUC,V2n))),ap(V1s,V2n))) ) ) ) ) )))).
fof(conj_thm_2Ewellorder_2EWF__UREC,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0_3C_3C] : ( mem(V0_3C_3C,arr(A_27a,arr(A_27a,bool))) => ( p(ap(c_2Erelation_2EWF(A_27a),V0_3C_3C)) => ! [V1H] : ( mem(V1H,arr(arr(A_27a,A_27b),arr(A_27a,A_27b))) => ( ( ! [V2f] : ( mem(V2f,arr(A_27a,A_27b)) => ! [V3g] : ( mem(V3g,arr(A_27a,A_27b)) => ! [V4x] : ( mem(V4x,A_27a) => ( ( ! [V5z] : ( mem(V5z,A_27a) => ( p(ap(ap(V0_3C_3C,V5z),V4x)) => ( ap(V2f,V5z) = ap(V3g,V5z) ) ) ) ) => ( ap(ap(V1H,V2f),V4x) = ap(ap(V1H,V3g),V4x) ) ) ) ) ) ) => ! [V6f] : ( mem(V6f,arr(A_27a,A_27b)) => ! [V7g] : ( mem(V7g,arr(A_27a,A_27b)) => ( ( ( ! [V8x] : ( mem(V8x,A_27a) => ( ap(V6f,V8x) = ap(ap(V1H,V6f),V8x) ) ) ) & ! [V9x] : ( mem(V9x,A_27a) => ( ap(V7g,V9x) = ap(ap(V1H,V7g),V9x) ) ) ) => ( V6f = V7g ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Ewellorder_2EWF__UREC__WF,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0_3C_3C] : ( mem(V0_3C_3C,arr(A_27a,arr(A_27a,bool))) => ( ( ! [V1H] : ( mem(V1H,arr(arr(A_27a,bool),arr(A_27a,bool))) => ( ( ! [V2f] : ( mem(V2f,arr(A_27a,bool)) => ! [V3g] : ( mem(V3g,arr(A_27a,bool)) => ! [V4x] : ( mem(V4x,A_27a) => ( ( ! [V5z] : ( mem(V5z,A_27a) => ( p(ap(ap(V0_3C_3C,V5z),V4x)) => ( p(ap(V2f,V5z)) <=> p(ap(V3g,V5z)) ) ) ) ) => ( p(ap(ap(V1H,V2f),V4x)) <=> p(ap(ap(V1H,V3g),V4x)) ) ) ) ) ) ) => ! [V6f] : ( mem(V6f,arr(A_27a,bool)) => ! [V7g] : ( mem(V7g,arr(A_27a,bool)) => ( ( ( ! [V8x] : ( mem(V8x,A_27a) => ( p(ap(V6f,V8x)) <=> p(ap(ap(V1H,V6f),V8x)) ) ) ) & ! [V9x] : ( mem(V9x,A_27a) => ( p(ap(V7g,V9x)) <=> p(ap(ap(V1H,V7g),V9x)) ) ) ) => ( V6f = V7g ) ) ) ) ) ) ) => p(ap(c_2Erelation_2EWF(A_27a),V0_3C_3C)) ) )))).
fof(conj_thm_2Ewellorder_2EWF__REC__INVARIANT,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0_3C_3C] : ( mem(V0_3C_3C,arr(A_27a,arr(A_27a,bool))) => ( p(ap(c_2Erelation_2EWF(A_27a),V0_3C_3C)) => ! [V1H] : ( mem(V1H,arr(arr(A_27a,A_27b),arr(A_27a,A_27b))) => ! [V2S] : ( mem(V2S,arr(A_27a,arr(A_27b,bool))) => ( ( ! [V3f] : ( mem(V3f,arr(A_27a,A_27b)) => ! [V4g] : ( mem(V4g,arr(A_27a,A_27b)) => ! [V5x] : ( mem(V5x,A_27a) => ( ( ! [V6z] : ( mem(V6z,A_27a) => ( p(ap(ap(V0_3C_3C,V6z),V5x)) => ( ( ap(V3f,V6z) = ap(V4g,V6z) ) & p(ap(ap(V2S,V6z),ap(V3f,V6z))) ) ) ) ) => ( ( ap(ap(V1H,V3f),V5x) = ap(ap(V1H,V4g),V5x) ) & p(ap(ap(V2S,V5x),ap(ap(V1H,V3f),V5x))) ) ) ) ) ) ) => ? [V7f] : ( mem(V7f,arr(A_27a,A_27b)) & ! [V8x] : ( mem(V8x,A_27a) => ( ap(V7f,V8x) = ap(ap(V1H,V7f),V8x) ) ) ) ) ) ) ) ))))).
fof(conj_thm_2Ewellorder_2EWF__REC,lemma,( ! [A_27a]: ( ne(A_27a) =>  ! [A_27b]: ( ne(A_27b) => ! [V0_3C_3C] : ( mem(V0_3C_3C,arr(A_27a,arr(A_27a,bool))) => ( p(ap(c_2Erelation_2EWF(A_27a),V0_3C_3C)) => ! [V1H] : ( mem(V1H,arr(arr(A_27a,A_27b),arr(A_27a,A_27b))) => ( ( ! [V2f] : ( mem(V2f,arr(A_27a,A_27b)) => ! [V3g] : ( mem(V3g,arr(A_27a,A_27b)) => ! [V4x] : ( mem(V4x,A_27a) => ( ( ! [V5z] : ( mem(V5z,A_27a) => ( p(ap(ap(V0_3C_3C,V5z),V4x)) => ( ap(V2f,V5z) = ap(V3g,V5z) ) ) ) ) => ( ap(ap(V1H,V2f),V4x) = ap(ap(V1H,V3g),V4x) ) ) ) ) ) ) => ? [V6f] : ( mem(V6f,arr(A_27a,A_27b)) & ! [V7x] : ( mem(V7x,A_27a) => ( ap(V6f,V7x) = ap(ap(V1H,V6f),V7x) ) ) ) ) ) ) ))))).
fof(conj_thm_2Ewellorder_2EWF__num,lemma,(p(ap(c_2Erelation_2EWF(ty_2Enum_2Enum),c_2Eprim__rec_2E_3C)))).
fof(conj_thm_2Ewellorder_2EWF__REC__num,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0H] : ( mem(V0H,arr(arr(ty_2Enum_2Enum,A_27a),arr(ty_2Enum_2Enum,A_27a))) => ( ( ! [V1f] : ( mem(V1f,arr(ty_2Enum_2Enum,A_27a)) => ! [V2g] : ( mem(V2g,arr(ty_2Enum_2Enum,A_27a)) => ! [V3n] : ( mem(V3n,ty_2Enum_2Enum) => ( ( ! [V4m] : ( mem(V4m,ty_2Enum_2Enum) => ( p(ap(ap(c_2Eprim__rec_2E_3C,V4m),V3n)) => ( ap(V1f,V4m) = ap(V2g,V4m) ) ) ) ) => ( ap(ap(V0H,V1f),V3n) = ap(ap(V0H,V2g),V3n) ) ) ) ) ) ) => ? [V5f] : ( mem(V5f,arr(ty_2Enum_2Enum,A_27a)) & ! [V6n] : ( mem(V6n,ty_2Enum_2Enum) => ( ap(V5f,V6n) = ap(ap(V0H,V5f),V6n) ) ) ) ) )))).
fof(ax_thm_2Ewellorder_2Efl,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0l] : ( mem(V0l,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1x] : ( mem(V1x,A_27a) => ( p(ap(ap(c_2Ewellorder_2Efl(A_27a),V0l),V1x)) <=> ? [V2y] : ( mem(V2y,A_27a) & ( p(ap(V0l,ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V2y))) | p(ap(V0l,ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2y),V1x))) ) ) ) ) ) ) )).
fof(ax_thm_2Ewellorder_2Eposet,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0l] : ( mem(V0l,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( p(ap(c_2Ewellorder_2Eposet(A_27a),V0l)) <=> ( ( ! [V1x] : ( mem(V1x,A_27a) => ( p(ap(ap(c_2Ewellorder_2Efl(A_27a),V0l),V1x)) => p(ap(V0l,ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V1x),V1x))) ) ) ) & ( ( ! [V2x] : ( mem(V2x,A_27a) => ! [V3y] : ( mem(V3y,A_27a) => ! [V4z] : ( mem(V4z,A_27a) => ( ( p(ap(V0l,ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2x),V3y))) & p(ap(V0l,ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V3y),V4z))) ) => p(ap(V0l,ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2x),V4z))) ) ) ) ) ) & ! [V5x] : ( mem(V5x,A_27a) => ! [V6y] : ( mem(V6y,A_27a) => ( ( p(ap(V0l,ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V5x),V6y))) & p(ap(V0l,ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V6y),V5x))) ) => ( V5x = V6y ) ) ) ) ) ) ) ) ) )).
fof(ax_thm_2Ewellorder_2Echain,axiom,( ! [A_27a] : ( ne(A_27a) => ! [V0l] : ( mem(V0l,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ! [V1P] : ( mem(V1P,arr(A_27a,bool)) => ( p(ap(ap(c_2Ewellorder_2EChain(A_27a),V0l),V1P)) <=> ! [V2x] : ( mem(V2x,A_27a) => ! [V3y] : ( mem(V3y,A_27a) => ( ( p(ap(V1P,V2x)) & p(ap(V1P,V3y)) ) => ( p(ap(V0l,ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V2x),V3y))) | p(ap(V0l,ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V3y),V2x))) ) ) ) ) ) ) ) ) )).
fof(conj_thm_2Ewellorder_2EZL,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0l] : ( mem(V0l,arr(ty_2Epair_2Eprod(A_27a,A_27a),bool)) => ( ( p(ap(c_2Ewellorder_2Eposet(A_27a),V0l)) & ( ( ? [V1x] : ( mem(V1x,A_27a) & p(ap(f1040(A_27a,V0l),V1x)) ) ) & ! [V3P] : ( mem(V3P,arr(A_27a,bool)) => ( p(ap(ap(c_2Ewellorder_2EChain(A_27a),V0l),V3P)) => ? [V4y] : ( mem(V4y,A_27a) & ( p(ap(ap(c_2Ewellorder_2Efl(A_27a),V0l),V4y)) & ! [V5x] : ( mem(V5x,A_27a) => ( p(ap(V3P,V5x)) => p(ap(V0l,ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V5x),V4y))) ) ) ) ) ) ) ) ) => ? [V6y] : ( mem(V6y,A_27a) & ( p(ap(ap(c_2Ewellorder_2Efl(A_27a),V0l),V6y)) & ! [V7x] : ( mem(V7x,A_27a) => ( p(ap(V0l,ap(ap(c_2Epair_2E_2C(A_27a,A_27a),V6y),V7x))) => ( V6y = V7x ) ) ) ) ) ) )))).
fof(conj_thm_2Ewellorder_2EPOSET__RESTRICTED__SUBSET,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(arr(A_27a,bool),bool)) => p(ap(c_2Ewellorder_2Eposet(arr(A_27a,bool)),ap(c_2Epair_2EUNCURRY(arr(A_27a,bool),arr(A_27a,bool),bool),f1042(A_27a,V0P)))) )))).
fof(conj_thm_2Ewellorder_2EFL__RESTRICTED__SUBSET,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(arr(A_27a,bool),bool)) => ( ap(c_2Ewellorder_2Efl(arr(A_27a,bool)),ap(c_2Epair_2EUNCURRY(arr(A_27a,bool),arr(A_27a,bool),bool),f1042(A_27a,V0P))) = V0P ) )))).
fof(conj_thm_2Ewellorder_2EZL__SUBSETS,lemma,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(arr(A_27a,bool),bool)) => ( ( ! [V1c] : ( mem(V1c,arr(arr(A_27a,bool),bool)) => ( ( ( ! [V2x] : ( mem(V2x,arr(A_27a,bool)) => ( p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V2x),V1c)) => p(ap(V0P,V2x)) ) ) ) & ! [V3x] : ( mem(V3x,arr(A_27a,bool)) => ! [V4y] : ( mem(V4y,arr(A_27a,bool)) => ( ( p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V3x),V1c)) & p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V4y),V1c)) ) => ( p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),V3x),V4y)) | p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),V4y),V3x)) ) ) ) ) ) => ? [V5z] : ( mem(V5z,arr(A_27a,bool)) & ( p(ap(V0P,V5z)) & ! [V6x] : ( mem(V6x,arr(A_27a,bool)) => ( p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V6x),V1c)) => p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),V6x),V5z)) ) ) ) ) ) ) ) => ? [V7a] : ( mem(V7a,arr(A_27a,bool)) & ( p(ap(V0P,V7a)) & ! [V8x] : ( mem(V8x,arr(A_27a,bool)) => ( ( p(ap(V0P,V8x)) & p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),V7a),V8x)) ) => ( V7a = V8x ) ) ) ) ) ) )))).
fof(conj_thm_2Ewellorder_2EZL__SUBSETS__BIGUNION,conjecture,( ! [A_27a]: ( ne(A_27a) => ! [V0P] : ( mem(V0P,arr(arr(A_27a,bool),bool)) => ( ( ! [V1c] : ( mem(V1c,arr(arr(A_27a,bool),bool)) => ( ( ( ! [V2x] : ( mem(V2x,arr(A_27a,bool)) => ( p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V2x),V1c)) => p(ap(V0P,V2x)) ) ) ) & ! [V3x] : ( mem(V3x,arr(A_27a,bool)) => ! [V4y] : ( mem(V4y,arr(A_27a,bool)) => ( ( p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V3x),V1c)) & p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V4y),V1c)) ) => ( p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),V3x),V4y)) | p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),V4y),V3x)) ) ) ) ) ) => p(ap(V0P,ap(c_2Epred__set_2EBIGUNION(A_27a),V1c))) ) ) ) => ? [V5a] : ( mem(V5a,arr(A_27a,bool)) & ( p(ap(V0P,V5a)) & ! [V6x] : ( mem(V6x,arr(A_27a,bool)) => ( ( p(ap(V0P,V6x)) & p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),V5a),V6x)) ) => ( V5a = V6x ) ) ) ) ) ) )))).
