include('Axioms/lift_machine_ieee_2.ax').
tff(tp_c_2Eiterate_2E_2E_2E,type,(c_2Eiterate_2E_2E_2E:$i)).
tff(mem_c_2Eiterate_2E_2E_2E,axiom,mem(c_2Eiterate_2E_2E_2E,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool))))).
tff(stp_fo_c_2Eiterate_2E_2E_2E,type,(fo__c_2Eiterate_2E_2E_2E:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__o)).
tff(stp_eq_fo_c_2Eiterate_2E_2E_2E,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : ( ! [X2:tp__ty_2Enum_2Enum] : (inj__o(fo__c_2Eiterate_2E_2E_2E(X0,X1,X2)) = ap(ap(ap(c_2Eiterate_2E_2E_2E,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)),inj__ty_2Enum_2Enum(X2))))))).
tff(tp_c_2Eiterate_2EFINREC,type,(c_2Eiterate_2EFINREC:(del * del) > $i)).
tff(mem_c_2Eiterate_2EFINREC,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Eiterate_2EFINREC(A_27a,A_27b),arr(arr(A_27a,arr(A_27b,A_27b)),arr(A_27b,arr(arr(A_27a,bool),arr(A_27b,arr(ty_2Enum_2Enum,bool))))))))).
tff(tp_c_2Eiterate_2EITSET,type,(c_2Eiterate_2EITSET:(del * del) > $i)).
tff(mem_c_2Eiterate_2EITSET,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Eiterate_2EITSET(A_27a,A_27b),arr(arr(A_27b,arr(A_27a,A_27a)),arr(arr(A_27b,bool),arr(A_27a,A_27a))))))).
tff(tp_c_2Eiterate_2ESum,type,(c_2Eiterate_2ESum:del > $i)).
tff(mem_c_2Eiterate_2ESum,axiom,( ! [A_27a:del] : mem(c_2Eiterate_2ESum(A_27a),arr(arr(A_27a,bool),arr(arr(A_27a,ty_2Erealax_2Ereal),ty_2Erealax_2Ereal))))).
tff(tp_c_2Eiterate_2Einf,type,(c_2Eiterate_2Einf:$i)).
tff(mem_c_2Eiterate_2Einf,axiom,mem(c_2Eiterate_2Einf,arr(arr(ty_2Erealax_2Ereal,bool),ty_2Erealax_2Ereal))).
tff(tp_c_2Eiterate_2Eiterate,type,(c_2Eiterate_2Eiterate:(del * del) > $i)).
tff(mem_c_2Eiterate_2Eiterate,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Eiterate_2Eiterate(A_27a,A_27b),arr(arr(A_27b,arr(A_27b,A_27b)),arr(arr(A_27a,bool),arr(arr(A_27a,A_27b),A_27b))))))).
tff(tp_c_2Eiterate_2Emonoidal,type,(c_2Eiterate_2Emonoidal:del > $i)).
tff(mem_c_2Eiterate_2Emonoidal,axiom,( ! [A_27a:del] : mem(c_2Eiterate_2Emonoidal(A_27a),arr(arr(A_27a,arr(A_27a,A_27a)),bool)))).
tff(tp_c_2Eiterate_2Eneutral,type,(c_2Eiterate_2Eneutral:del > $i)).
tff(mem_c_2Eiterate_2Eneutral,axiom,( ! [A_27a:del] : mem(c_2Eiterate_2Eneutral(A_27a),arr(arr(A_27a,arr(A_27a,A_27a)),A_27a)))).
tff(tp_c_2Eiterate_2Ensum,type,(c_2Eiterate_2Ensum:del > $i)).
tff(mem_c_2Eiterate_2Ensum,axiom,( ! [A_27a:del] : mem(c_2Eiterate_2Ensum(A_27a),arr(arr(A_27a,bool),arr(arr(A_27a,ty_2Enum_2Enum),ty_2Enum_2Enum))))).
tff(tp_c_2Eiterate_2Epolynomial__function,type,(c_2Eiterate_2Epolynomial__function:$i)).
tff(mem_c_2Eiterate_2Epolynomial__function,axiom,mem(c_2Eiterate_2Epolynomial__function,arr(arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),bool))).
tff(tp_c_2Eiterate_2Esupport,type,(c_2Eiterate_2Esupport:(del * del) > $i)).
tff(mem_c_2Eiterate_2Esupport,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Eiterate_2Esupport(A_27a,A_27b),arr(arr(A_27b,arr(A_27b,A_27b)),arr(arr(A_27a,A_27b),arr(arr(A_27a,bool),arr(A_27a,bool)))))))).
tff(conj_thm_2Eiterate_2EREAL__LT__BETWEEN,lemma,(( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1b:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V0a)),inj__ty_2Erealax_2Ereal(V1b))) <=> (? [V2x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V0a)),inj__ty_2Erealax_2Ereal(V2x))) & p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V2x)),inj__ty_2Erealax_2Ereal(V1b)))))))))).
tff(conj_thm_2Eiterate_2ESIMP__REAL__ARCH,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : (? [V1n:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V0x)),ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(V1n)))))))).
tff(conj_thm_2Eiterate_2ELOWER__BOUND__FINITE__SET__REAL,lemma,(( ! [A_27a:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,ty_2Erealax_2Ereal)) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => (p(ap(c_2Epred__set_2EFINITE(A_27a),V1s)) => (? [V2a:tp__ty_2Erealax_2Ereal] : ( ! [V3x:$i] : (mem(V3x,A_27a) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V3x),V1s)) => p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V2a)),ap(V0f,V3x))))))))))))))).
tff(conj_thm_2Eiterate_2EUPPER__BOUND__FINITE__SET__REAL,lemma,(( ! [A_27a:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,ty_2Erealax_2Ereal)) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => (p(ap(c_2Epred__set_2EFINITE(A_27a),V1s)) => (? [V2a:tp__ty_2Erealax_2Ereal] : ( ! [V3x:$i] : (mem(V3x,A_27a) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V3x),V1s)) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(V0f,V3x)),inj__ty_2Erealax_2Ereal(V2a))))))))))))))).
tff(conj_thm_2Eiterate_2EREAL__WLOG__LT,lemma,(( ! [V0P:$i] : (mem(V0P,arr(ty_2Erealax_2Ereal,arr(ty_2Erealax_2Ereal,bool))) => ((( ! [V1x:tp__ty_2Erealax_2Ereal] : p(ap(ap(V0P,inj__ty_2Erealax_2Ereal(V1x)),inj__ty_2Erealax_2Ereal(V1x)))) & (( ! [V2x:tp__ty_2Erealax_2Ereal] : ( ! [V3y:tp__ty_2Erealax_2Ereal] : (p(ap(ap(V0P,inj__ty_2Erealax_2Ereal(V2x)),inj__ty_2Erealax_2Ereal(V3y))) <=> p(ap(ap(V0P,inj__ty_2Erealax_2Ereal(V3y)),inj__ty_2Erealax_2Ereal(V2x)))))) & ( ! [V4x:tp__ty_2Erealax_2Ereal] : ( ! [V5y:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V4x)),inj__ty_2Erealax_2Ereal(V5y))) => p(ap(ap(V0P,inj__ty_2Erealax_2Ereal(V4x)),inj__ty_2Erealax_2Ereal(V5y)))))))) => ( ! [V6x:tp__ty_2Erealax_2Ereal] : ( ! [V7y:tp__ty_2Erealax_2Ereal] : p(ap(ap(V0P,inj__ty_2Erealax_2Ereal(V6x)),inj__ty_2Erealax_2Ereal(V7y)))))))))).
tff(ax_thm_2Eiterate_2EFINREC__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0f:$i] : (mem(V0f,arr(A_27a,arr(A_27b,A_27b))) => ( ! [V1b:$i] : (mem(V1b,A_27b) => ( ! [V2s:$i] : (mem(V2s,arr(A_27a,bool)) => ( ! [V3a:$i] : (mem(V3a,A_27b) => (p(ap(ap(ap(ap(ap(c_2Eiterate_2EFINREC(A_27a,A_27b),V0f),V1b),V2s),V3a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) <=> ((V2s = c_2Epred__set_2EEMPTY(A_27a)) & (V3a = V1b))))))))))) & ( ! [V4f:$i] : (mem(V4f,arr(A_27a,arr(A_27b,A_27b))) => ( ! [V5b:$i] : (mem(V5b,A_27b) => ( ! [V6s:$i] : (mem(V6s,arr(A_27a,bool)) => ( ! [V7a:$i] : (mem(V7a,A_27b) => ( ! [V8n:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(ap(ap(c_2Eiterate_2EFINREC(A_27a,A_27b),V4f),V5b),V6s),V7a),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V8n)))) <=> (? [V9x:$i] : (mem(V9x,A_27a) & (? [V10c:$i] : (mem(V10c,A_27b) & (p(ap(ap(c_2Ebool_2EIN(A_27a),V9x),V6s)) & (p(ap(ap(ap(ap(ap(c_2Eiterate_2EFINREC(A_27a,A_27b),V4f),V5b),ap(ap(c_2Epred__set_2EDELETE(A_27a),V6s),V9x)),V10c),inj__ty_2Enum_2Enum(V8n))) & (V7a = ap(ap(V4f,V9x),V10c)))))))))))))))))))))).
tff(conj_thm_2Eiterate_2EFINREC__def__compute,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0f:$i] : (mem(V0f,arr(A_27a,arr(A_27b,A_27b))) => ( ! [V1b:$i] : (mem(V1b,A_27b) => ( ! [V2s:$i] : (mem(V2s,arr(A_27a,bool)) => ( ! [V3a:$i] : (mem(V3a,A_27b) => (p(ap(ap(ap(ap(ap(c_2Eiterate_2EFINREC(A_27a,A_27b),V0f),V1b),V2s),V3a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) <=> ((V2s = c_2Epred__set_2EEMPTY(A_27a)) & (V3a = V1b))))))))))) & (( ! [V4f:$i] : (mem(V4f,arr(A_27a,arr(A_27b,A_27b))) => ( ! [V5b:$i] : (mem(V5b,A_27b) => ( ! [V6s:$i] : (mem(V6s,arr(A_27a,bool)) => ( ! [V7a:$i] : (mem(V7a,A_27b) => ( ! [V8n:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(ap(ap(c_2Eiterate_2EFINREC(A_27a,A_27b),V4f),V5b),V6s),V7a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V8n))))) <=> (? [V9x:$i] : (mem(V9x,A_27a) & (? [V10c:$i] : (mem(V10c,A_27b) & (p(ap(ap(c_2Ebool_2EIN(A_27a),V9x),V6s)) & (p(ap(ap(ap(ap(ap(c_2Eiterate_2EFINREC(A_27a,A_27b),V4f),V5b),ap(ap(c_2Epred__set_2EDELETE(A_27a),V6s),V9x)),V10c),ap(ap(c_2Earithmetic_2E_2D,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V8n)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))) & (V7a = ap(ap(V4f,V9x),V10c)))))))))))))))))) & ( ! [V11f:$i] : (mem(V11f,arr(A_27a,arr(A_27b,A_27b))) => ( ! [V12b:$i] : (mem(V12b,A_27b) => ( ! [V13s:$i] : (mem(V13s,arr(A_27a,bool)) => ( ! [V14a:$i] : (mem(V14a,A_27b) => ( ! [V15n:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(ap(ap(c_2Eiterate_2EFINREC(A_27a,A_27b),V11f),V12b),V13s),V14a),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V15n))))) <=> (? [V16x:$i] : (mem(V16x,A_27a) & (? [V17c:$i] : (mem(V17c,A_27b) & (p(ap(ap(c_2Ebool_2EIN(A_27a),V16x),V13s)) & (p(ap(ap(ap(ap(ap(c_2Eiterate_2EFINREC(A_27a,A_27b),V11f),V12b),ap(ap(c_2Epred__set_2EDELETE(A_27a),V13s),V16x)),V17c),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V15n))))) & (V14a = ap(ap(V11f,V16x),V17c)))))))))))))))))))))))).
tff(conj_thm_2Eiterate_2EFINREC__1__LEMMA,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,arr(A_27b,A_27b))) => ( ! [V1b:$i] : (mem(V1b,A_27b) => ( ! [V2s:$i] : (mem(V2s,arr(A_27a,bool)) => ( ! [V3a:$i] : (mem(V3a,A_27b) => (p(ap(ap(ap(ap(ap(c_2Eiterate_2EFINREC(A_27a,A_27b),V0f),V1b),V2s),V3a),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) <=> (? [V4x:$i] : (mem(V4x,A_27a) & ((V2s = ap(ap(c_2Epred__set_2EINSERT(A_27a),V4x),c_2Epred__set_2EEMPTY(A_27a))) & (V3a = ap(ap(V0f,V4x),V1b)))))))))))))))))).
tff(conj_thm_2Eiterate_2EFINREC__SUC__LEMMA,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,arr(A_27b,A_27b))) => ( ! [V1b:$i] : (mem(V1b,A_27b) => (( ! [V2x:$i] : (mem(V2x,A_27a) => ( ! [V3y:$i] : (mem(V3y,A_27a) => ( ! [V4s:$i] : (mem(V4s,A_27b) => ((~~ (V2x = V3y)) => (ap(ap(V0f,V2x),ap(ap(V0f,V3y),V4s)) = ap(ap(V0f,V3y),ap(ap(V0f,V2x),V4s)))))))))) => ( ! [V5n:tp__ty_2Enum_2Enum] : ( ! [V6s:$i] : (mem(V6s,arr(A_27a,bool)) => ( ! [V7z:$i] : (mem(V7z,A_27b) => (p(ap(ap(ap(ap(ap(c_2Eiterate_2EFINREC(A_27a,A_27b),V0f),V1b),V6s),V7z),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V5n)))) => ( ! [V8x:$i] : (mem(V8x,A_27a) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V8x),V6s)) => (? [V9w:$i] : (mem(V9w,A_27b) & (p(ap(ap(ap(ap(ap(c_2Eiterate_2EFINREC(A_27a,A_27b),V0f),V1b),ap(ap(c_2Epred__set_2EDELETE(A_27a),V6s),V8x)),V9w),inj__ty_2Enum_2Enum(V5n))) & (V7z = ap(ap(V0f,V8x),V9w))))))))))))))))))))))).
tff(conj_thm_2Eiterate_2EFINREC__UNIQUE__LEMMA,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,arr(A_27b,A_27b))) => ( ! [V1b:$i] : (mem(V1b,A_27b) => (( ! [V2x:$i] : (mem(V2x,A_27a) => ( ! [V3y:$i] : (mem(V3y,A_27a) => ( ! [V4s:$i] : (mem(V4s,A_27b) => ((~~ (V2x = V3y)) => (ap(ap(V0f,V2x),ap(ap(V0f,V3y),V4s)) = ap(ap(V0f,V3y),ap(ap(V0f,V2x),V4s)))))))))) => ( ! [V5n1:tp__ty_2Enum_2Enum] : ( ! [V6n2:tp__ty_2Enum_2Enum] : ( ! [V7s:$i] : (mem(V7s,arr(A_27a,bool)) => ( ! [V8a1:$i] : (mem(V8a1,A_27b) => ( ! [V9a2:$i] : (mem(V9a2,A_27b) => ((p(ap(ap(ap(ap(ap(c_2Eiterate_2EFINREC(A_27a,A_27b),V0f),V1b),V7s),V8a1),inj__ty_2Enum_2Enum(V5n1))) & p(ap(ap(ap(ap(ap(c_2Eiterate_2EFINREC(A_27a,A_27b),V0f),V1b),V7s),V9a2),inj__ty_2Enum_2Enum(V6n2)))) => ((V8a1 = V9a2) & (V5n1 = V6n2)))))))))))))))))))).
tff(conj_thm_2Eiterate_2EFINREC__EXISTS__LEMMA,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,arr(A_27b,A_27b))) => ( ! [V1b:$i] : (mem(V1b,A_27b) => ( ! [V2s:$i] : (mem(V2s,arr(A_27a,bool)) => (p(ap(c_2Epred__set_2EFINITE(A_27a),V2s)) => (? [V3a:$i] : (mem(V3a,A_27b) & (? [V4n:tp__ty_2Enum_2Enum] : p(ap(ap(ap(ap(ap(c_2Eiterate_2EFINREC(A_27a,A_27b),V0f),V1b),V2s),V3a),inj__ty_2Enum_2Enum(V4n))))))))))))))))).
tff(conj_thm_2Eiterate_2EFINREC__FUN__LEMMA,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1R:$i] : (mem(V1R,arr(A_27a,arr(A_27b,arr(A_27c,bool)))) => ((( ! [V2s:$i] : (mem(V2s,A_27a) => (p(ap(V0P,V2s)) => (? [V3a:$i] : (mem(V3a,A_27b) & (? [V4n:$i] : (mem(V4n,A_27c) & p(ap(ap(ap(V1R,V2s),V3a),V4n))))))))) & ( ! [V5n1:$i] : (mem(V5n1,A_27c) => ( ! [V6n2:$i] : (mem(V6n2,A_27c) => ( ! [V7s:$i] : (mem(V7s,A_27a) => ( ! [V8a1:$i] : (mem(V8a1,A_27b) => ( ! [V9a2:$i] : (mem(V9a2,A_27b) => ((p(ap(ap(ap(V1R,V7s),V8a1),V5n1)) & p(ap(ap(ap(V1R,V7s),V9a2),V6n2))) => ((V8a1 = V9a2) & (V5n1 = V6n2)))))))))))))) => (? [V10f:$i] : (mem(V10f,arr(A_27a,A_27b)) & ( ! [V11s:$i] : (mem(V11s,A_27a) => ( ! [V12a:$i] : (mem(V12a,A_27b) => (p(ap(V0P,V11s)) => ((? [V13n:$i] : (mem(V13n,A_27c) & p(ap(ap(ap(V1R,V11s),V12a),V13n)))) <=> (ap(V10f,V11s) = V12a))))))))))))))))))).
tff(conj_thm_2Eiterate_2EFINREC__FUN,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,arr(A_27b,A_27b))) => ( ! [V1b:$i] : (mem(V1b,A_27b) => (( ! [V2x:$i] : (mem(V2x,A_27a) => ( ! [V3y:$i] : (mem(V3y,A_27a) => ( ! [V4s:$i] : (mem(V4s,A_27b) => ((~~ (V2x = V3y)) => (ap(ap(V0f,V2x),ap(ap(V0f,V3y),V4s)) = ap(ap(V0f,V3y),ap(ap(V0f,V2x),V4s)))))))))) => (? [V5g:$i] : (mem(V5g,arr(arr(A_27a,bool),A_27b)) & ((ap(V5g,c_2Epred__set_2EEMPTY(A_27a)) = V1b) & ( ! [V6s:$i] : (mem(V6s,arr(A_27a,bool)) => ( ! [V7x:$i] : (mem(V7x,A_27a) => ((p(ap(c_2Epred__set_2EFINITE(A_27a),V6s)) & p(ap(ap(c_2Ebool_2EIN(A_27a),V7x),V6s))) => (ap(V5g,V6s) = ap(ap(V0f,V7x),ap(V5g,ap(ap(c_2Epred__set_2EDELETE(A_27a),V6s),V7x))))))))))))))))))))).
tff(conj_thm_2Eiterate_2ESET__RECURSION__LEMMA,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,arr(A_27b,A_27b))) => ( ! [V1b:$i] : (mem(V1b,A_27b) => (( ! [V2x:$i] : (mem(V2x,A_27a) => ( ! [V3y:$i] : (mem(V3y,A_27a) => ( ! [V4s:$i] : (mem(V4s,A_27b) => ((~~ (V2x = V3y)) => (ap(ap(V0f,V2x),ap(ap(V0f,V3y),V4s)) = ap(ap(V0f,V3y),ap(ap(V0f,V2x),V4s)))))))))) => (? [V5g:$i] : (mem(V5g,arr(arr(A_27a,bool),A_27b)) & ((ap(V5g,c_2Epred__set_2EEMPTY(A_27a)) = V1b) & ( ! [V6x:$i] : (mem(V6x,A_27a) => ( ! [V7s:$i] : (mem(V7s,arr(A_27a,bool)) => (p(ap(c_2Epred__set_2EFINITE(A_27a),V7s)) => (ap(V5g,ap(ap(c_2Epred__set_2EINSERT(A_27a),V6x),V7s)) = ap(ap(ap(c_2Ebool_2ECOND(A_27b),ap(ap(c_2Ebool_2EIN(A_27a),V6x),V7s)),ap(V5g,V7s)),ap(ap(V0f,V6x),ap(V5g,V7s))))))))))))))))))))).
tff(ax_thm_2Eiterate_2EITSET__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27b,arr(A_27a,A_27a))) => ( ! [V1s:$i] : (mem(V1s,arr(A_27b,bool)) => ( ! [V2b:$i] : (mem(V2b,A_27a) => (ap(ap(ap(c_2Eiterate_2EITSET(A_27a,A_27b),V0f),V1s),V2b) = ap(ap(c_2Emin_2E_40(arr(arr(A_27b,bool),A_27a)),f3262(A_27a,A_27b,V2b,V0f)),V1s))))))))))).
tff(conj_thm_2Eiterate_2EFINITE__RECURSION,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,arr(A_27b,A_27b))) => ( ! [V1b:$i] : (mem(V1b,A_27b) => (( ! [V2x:$i] : (mem(V2x,A_27a) => ( ! [V3y:$i] : (mem(V3y,A_27a) => ( ! [V4s:$i] : (mem(V4s,A_27b) => ((~~ (V2x = V3y)) => (ap(ap(V0f,V2x),ap(ap(V0f,V3y),V4s)) = ap(ap(V0f,V3y),ap(ap(V0f,V2x),V4s)))))))))) => ((ap(ap(ap(c_2Eiterate_2EITSET(A_27b,A_27a),V0f),c_2Epred__set_2EEMPTY(A_27a)),V1b) = V1b) & ( ! [V5x:$i] : (mem(V5x,A_27a) => ( ! [V6s:$i] : (mem(V6s,arr(A_27a,bool)) => (p(ap(c_2Epred__set_2EFINITE(A_27a),V6s)) => (ap(ap(ap(c_2Eiterate_2EITSET(A_27b,A_27a),V0f),ap(ap(c_2Epred__set_2EINSERT(A_27a),V5x),V6s)),V1b) = ap(ap(ap(c_2Ebool_2ECOND(A_27b),ap(ap(c_2Ebool_2EIN(A_27a),V5x),V6s)),ap(ap(ap(c_2Eiterate_2EITSET(A_27b,A_27a),V0f),V6s),V1b)),ap(ap(V0f,V5x),ap(ap(ap(c_2Eiterate_2EITSET(A_27b,A_27a),V0f),V6s),V1b))))))))))))))))))).
tff(conj_thm_2Eiterate_2ECARD__UNION__EQ,lemma,(( ! [A_27a:del]: ( ! [V0s:$i] : (mem(V0s,arr(A_27a,bool)) => ( ! [V1t:$i] : (mem(V1t,arr(A_27a,bool)) => ( ! [V2u:$i] : (mem(V2u,arr(A_27a,bool)) => ((p(ap(c_2Epred__set_2EFINITE(A_27a),V2u)) & ((ap(ap(c_2Epred__set_2EINTER(A_27a),V0s),V1t) = c_2Epred__set_2EEMPTY(A_27a)) & (ap(ap(c_2Epred__set_2EUNION(A_27a),V0s),V1t) = V2u))) => (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(c_2Epred__set_2ECARD(A_27a),V0s)),ap(c_2Epred__set_2ECARD(A_27a),V1t))) = surj__ty_2Enum_2Enum(ap(c_2Epred__set_2ECARD(A_27a),V2u))))))))))))).
tff(conj_thm_2Eiterate_2ESUBSET__RESTRICT,lemma,(( ! [A_27a:del]: ( ! [V0s:$i] : (mem(V0s,arr(A_27a,bool)) => ( ! [V1P:$i] : (mem(V1P,arr(A_27a,bool)) => p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Epred__set_2EGSPEC(A_27a,A_27a),f1884(A_27a,V1P,V0s))),V0s))))))))).
tff(conj_thm_2Eiterate_2EFINITE__RESTRICT,lemma,(( ! [A_27a:del]: ( ! [V0s:$i] : (mem(V0s,arr(A_27a,bool)) => ( ! [V1P:$i] : (mem(V1P,arr(A_27a,bool)) => (p(ap(c_2Epred__set_2EFINITE(A_27a),V0s)) => p(ap(c_2Epred__set_2EFINITE(A_27a),ap(c_2Epred__set_2EGSPEC(A_27a,A_27a),f1884(A_27a,V1P,V0s)))))))))))).
tff(conj_thm_2Eiterate_2EFINITE__REAL__INTERVAL,lemma,((( ! [V0a:tp__ty_2Erealax_2Ereal] : (~~ p(ap(c_2Epred__set_2EFINITE(ty_2Erealax_2Ereal),ap(c_2Epred__set_2EGSPEC(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),f3263(V0a)))))) & (( ! [V2a:tp__ty_2Erealax_2Ereal] : (~~ p(ap(c_2Epred__set_2EFINITE(ty_2Erealax_2Ereal),ap(c_2Epred__set_2EGSPEC(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),f3264(V2a)))))) & (( ! [V4b:tp__ty_2Erealax_2Ereal] : (~~ p(ap(c_2Epred__set_2EFINITE(ty_2Erealax_2Ereal),ap(c_2Epred__set_2EGSPEC(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),f3265(V4b)))))) & (( ! [V6b:tp__ty_2Erealax_2Ereal] : (~~ p(ap(c_2Epred__set_2EFINITE(ty_2Erealax_2Ereal),ap(c_2Epred__set_2EGSPEC(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),f3266(V6b)))))) & (( ! [V8a:tp__ty_2Erealax_2Ereal] : ( ! [V9b:tp__ty_2Erealax_2Ereal] : (p(ap(c_2Epred__set_2EFINITE(ty_2Erealax_2Ereal),ap(c_2Epred__set_2EGSPEC(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),f3267(V9b,V8a)))) <=> p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V9b)),inj__ty_2Erealax_2Ereal(V8a)))))) & (( ! [V11a:tp__ty_2Erealax_2Ereal] : ( ! [V12b:tp__ty_2Erealax_2Ereal] : (p(ap(c_2Epred__set_2EFINITE(ty_2Erealax_2Ereal),ap(c_2Epred__set_2EGSPEC(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),f3268(V12b,V11a)))) <=> p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V12b)),inj__ty_2Erealax_2Ereal(V11a)))))) & (( ! [V14a:tp__ty_2Erealax_2Ereal] : ( ! [V15b:tp__ty_2Erealax_2Ereal] : (p(ap(c_2Epred__set_2EFINITE(ty_2Erealax_2Ereal),ap(c_2Epred__set_2EGSPEC(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),f3269(V15b,V14a)))) <=> p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V15b)),inj__ty_2Erealax_2Ereal(V14a)))))) & ( ! [V17a:tp__ty_2Erealax_2Ereal] : ( ! [V18b:tp__ty_2Erealax_2Ereal] : (p(ap(c_2Epred__set_2EFINITE(ty_2Erealax_2Ereal),ap(c_2Epred__set_2EGSPEC(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal),f3270(V18b,V17a)))) <=> p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V18b)),inj__ty_2Erealax_2Ereal(V17a))))))))))))))).
tff(conj_thm_2Eiterate_2Ereal__INFINITE,lemma,((~~ p(ap(c_2Epred__set_2EFINITE(ty_2Erealax_2Ereal),c_2Epred__set_2EUNIV(ty_2Erealax_2Ereal)))))).
tff(conj_thm_2Eiterate_2ESET__PROVE__CASES,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(arr(A_27a,bool),bool)) => ((p(ap(V0P,c_2Epred__set_2EEMPTY(A_27a))) & ( ! [V1a:$i] : (mem(V1a,A_27a) => ( ! [V2s:$i] : (mem(V2s,arr(A_27a,bool)) => ((~~ p(ap(ap(c_2Ebool_2EIN(A_27a),V1a),V2s))) => p(ap(V0P,ap(ap(c_2Epred__set_2EINSERT(A_27a),V1a),V2s))))))))) => ( ! [V3s:$i] : (mem(V3s,arr(A_27a,bool)) => p(ap(V0P,V3s)))))))))).
tff(conj_thm_2Eiterate_2ECHOOSE__SUBSET__STRONG,lemma,(( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => ((p(ap(c_2Epred__set_2EFINITE(A_27a),V1s)) => p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0n)),ap(c_2Epred__set_2ECARD(A_27a),V1s)))) => (? [V2t:$i] : (mem(V2t,arr(A_27a,bool)) & (p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),V2t),V1s)) & p(ap(ap(c_2Ecardinal_2EHAS__SIZE(A_27a),V2t),inj__ty_2Enum_2Enum(V0n))))))))))))).
tff(conj_thm_2Eiterate_2ECHOOSE__SUBSET,lemma,(( ! [A_27a:del]: ( ! [V0s:$i] : (mem(V0s,arr(A_27a,bool)) => (p(ap(c_2Epred__set_2EFINITE(A_27a),V0s)) => ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1n)),ap(c_2Epred__set_2ECARD(A_27a),V0s))) => (? [V2t:$i] : (mem(V2t,arr(A_27a,bool)) & (p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),V2t),V0s)) & p(ap(ap(c_2Ecardinal_2EHAS__SIZE(A_27a),V2t),inj__ty_2Enum_2Enum(V1n)))))))))))))).
tff(conj_thm_2Eiterate_2EREAL__COMPLETE,lemma,(( ! [V0P:$i] : (mem(V0P,arr(ty_2Erealax_2Ereal,bool)) => (((? [V1x:tp__ty_2Erealax_2Ereal] : p(ap(V0P,inj__ty_2Erealax_2Ereal(V1x)))) & (? [V2M:tp__ty_2Erealax_2Ereal] : ( ! [V3x:tp__ty_2Erealax_2Ereal] : (p(ap(V0P,inj__ty_2Erealax_2Ereal(V3x))) => p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V3x)),inj__ty_2Erealax_2Ereal(V2M))))))) => (? [V4M:tp__ty_2Erealax_2Ereal] : (( ! [V5x:tp__ty_2Erealax_2Ereal] : (p(ap(V0P,inj__ty_2Erealax_2Ereal(V5x))) => p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V5x)),inj__ty_2Erealax_2Ereal(V4M))))) & ( ! [V6M_27:tp__ty_2Erealax_2Ereal] : (( ! [V7x:tp__ty_2Erealax_2Ereal] : (p(ap(V0P,inj__ty_2Erealax_2Ereal(V7x))) => p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V7x)),inj__ty_2Erealax_2Ereal(V6M_27))))) => p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V4M)),inj__ty_2Erealax_2Ereal(V6M_27)))))))))))).
tff(conj_thm_2Eiterate_2Esup__alt,lemma,(( ! [V0s:$i] : (mem(V0s,arr(ty_2Erealax_2Ereal,bool)) => (surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Esup,V0s)) = surj__ty_2Erealax_2Ereal(ap(c_2Emin_2E_40(ty_2Erealax_2Ereal),f3274(V0s)))))))).
tff(conj_thm_2Eiterate_2ESUP__EQ,lemma,(( ! [V0s:$i] : (mem(V0s,arr(ty_2Erealax_2Ereal,bool)) => ( ! [V1t:$i] : (mem(V1t,arr(ty_2Erealax_2Ereal,bool)) => (( ! [V2b:tp__ty_2Erealax_2Ereal] : (( ! [V3x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V3x)),V0s)) => p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V3x)),inj__ty_2Erealax_2Ereal(V2b))))) <=> ( ! [V4x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V4x)),V1t)) => p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V4x)),inj__ty_2Erealax_2Ereal(V2b))))))) => (surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Esup,V0s)) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Esup,V1t)))))))))).
tff(conj_thm_2Eiterate_2ESUP,lemma,(( ! [V0s:$i] : (mem(V0s,arr(ty_2Erealax_2Ereal,bool)) => (((~~ (V0s = c_2Epred__set_2EEMPTY(ty_2Erealax_2Ereal))) & (? [V1b:tp__ty_2Erealax_2Ereal] : ( ! [V2x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V2x)),V0s)) => p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V2x)),inj__ty_2Erealax_2Ereal(V1b))))))) => (( ! [V3x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V3x)),V0s)) => p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V3x)),ap(c_2Ereal_2Esup,V0s))))) & ( ! [V4b:tp__ty_2Erealax_2Ereal] : (( ! [V5x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V5x)),V0s)) => p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V5x)),inj__ty_2Erealax_2Ereal(V4b))))) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Esup,V0s)),inj__ty_2Erealax_2Ereal(V4b))))))))))).
tff(conj_thm_2Eiterate_2ESUP__FINITE__LEMMA,lemma,(( ! [V0s:$i] : (mem(V0s,arr(ty_2Erealax_2Ereal,bool)) => ((p(ap(c_2Epred__set_2EFINITE(ty_2Erealax_2Ereal),V0s)) & (~~ (V0s = c_2Epred__set_2EEMPTY(ty_2Erealax_2Ereal)))) => (? [V1b:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V1b)),V0s)) & ( ! [V2x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V2x)),V0s)) => p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V2x)),inj__ty_2Erealax_2Ereal(V1b)))))))))))).
tff(conj_thm_2Eiterate_2ESUP__FINITE,lemma,(( ! [V0s:$i] : (mem(V0s,arr(ty_2Erealax_2Ereal,bool)) => ((p(ap(c_2Epred__set_2EFINITE(ty_2Erealax_2Ereal),V0s)) & (~~ (V0s = c_2Epred__set_2EEMPTY(ty_2Erealax_2Ereal)))) => (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),ap(c_2Ereal_2Esup,V0s)),V0s)) & ( ! [V1x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V1x)),V0s)) => p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V1x)),ap(c_2Ereal_2Esup,V0s))))))))))).
tff(conj_thm_2Eiterate_2EREAL__LE__SUP__FINITE,lemma,(( ! [V0s:$i] : (mem(V0s,arr(ty_2Erealax_2Ereal,bool)) => ( ! [V1a:tp__ty_2Erealax_2Ereal] : ((p(ap(c_2Epred__set_2EFINITE(ty_2Erealax_2Ereal),V0s)) & (~~ (V0s = c_2Epred__set_2EEMPTY(ty_2Erealax_2Ereal)))) => (p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V1a)),ap(c_2Ereal_2Esup,V0s))) <=> (? [V2x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V2x)),V0s)) & p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V1a)),inj__ty_2Erealax_2Ereal(V2x)))))))))))).
tff(conj_thm_2Eiterate_2EREAL__SUP__LE__FINITE,lemma,(( ! [V0s:$i] : (mem(V0s,arr(ty_2Erealax_2Ereal,bool)) => ( ! [V1a:tp__ty_2Erealax_2Ereal] : ((p(ap(c_2Epred__set_2EFINITE(ty_2Erealax_2Ereal),V0s)) & (~~ (V0s = c_2Epred__set_2EEMPTY(ty_2Erealax_2Ereal)))) => (p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Esup,V0s)),inj__ty_2Erealax_2Ereal(V1a))) <=> ( ! [V2x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V2x)),V0s)) => p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V2x)),inj__ty_2Erealax_2Ereal(V1a)))))))))))).
tff(conj_thm_2Eiterate_2EREAL__LT__SUP__FINITE,lemma,(( ! [V0s:$i] : (mem(V0s,arr(ty_2Erealax_2Ereal,bool)) => ( ! [V1a:tp__ty_2Erealax_2Ereal] : ((p(ap(c_2Epred__set_2EFINITE(ty_2Erealax_2Ereal),V0s)) & (~~ (V0s = c_2Epred__set_2EEMPTY(ty_2Erealax_2Ereal)))) => (p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V1a)),ap(c_2Ereal_2Esup,V0s))) <=> (? [V2x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V2x)),V0s)) & p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V1a)),inj__ty_2Erealax_2Ereal(V2x)))))))))))).
tff(conj_thm_2Eiterate_2EREAL__SUP__LT__FINITE,lemma,(( ! [V0s:$i] : (mem(V0s,arr(ty_2Erealax_2Ereal,bool)) => ( ! [V1a:tp__ty_2Erealax_2Ereal] : ((p(ap(c_2Epred__set_2EFINITE(ty_2Erealax_2Ereal),V0s)) & (~~ (V0s = c_2Epred__set_2EEMPTY(ty_2Erealax_2Ereal)))) => (p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Esup,V0s)),inj__ty_2Erealax_2Ereal(V1a))) <=> ( ! [V2x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V2x)),V0s)) => p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V2x)),inj__ty_2Erealax_2Ereal(V1a)))))))))))).
tff(conj_thm_2Eiterate_2EREAL__SUP__LE__EQ,lemma,(( ! [V0s:$i] : (mem(V0s,arr(ty_2Erealax_2Ereal,bool)) => ( ! [V1y:tp__ty_2Erealax_2Ereal] : (((~~ (V0s = c_2Epred__set_2EEMPTY(ty_2Erealax_2Ereal))) & (? [V2b:tp__ty_2Erealax_2Ereal] : ( ! [V3x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V3x)),V0s)) => p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V3x)),inj__ty_2Erealax_2Ereal(V2b))))))) => (p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Esup,V0s)),inj__ty_2Erealax_2Ereal(V1y))) <=> ( ! [V4x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V4x)),V0s)) => p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V4x)),inj__ty_2Erealax_2Ereal(V1y)))))))))))).
tff(conj_thm_2Eiterate_2EREAL__SUP__UNIQUE,lemma,(( ! [V0s:$i] : (mem(V0s,arr(ty_2Erealax_2Ereal,bool)) => ( ! [V1b:tp__ty_2Erealax_2Ereal] : ((( ! [V2x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V2x)),V0s)) => p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V2x)),inj__ty_2Erealax_2Ereal(V1b))))) & ( ! [V3b_27:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V3b_27)),inj__ty_2Erealax_2Ereal(V1b))) => (? [V4x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V4x)),V0s)) & p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V3b_27)),inj__ty_2Erealax_2Ereal(V4x)))))))) => (surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Esup,V0s)) = V1b))))))).
tff(conj_thm_2Eiterate_2EREAL__SUP__LE__S,lemma,(( ! [V0s:$i] : (mem(V0s,arr(ty_2Erealax_2Ereal,bool)) => ( ! [V1b:tp__ty_2Erealax_2Ereal] : (((~~ (V0s = c_2Epred__set_2EEMPTY(ty_2Erealax_2Ereal))) & ( ! [V2x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V2x)),V0s)) => p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V2x)),inj__ty_2Erealax_2Ereal(V1b)))))) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Esup,V0s)),inj__ty_2Erealax_2Ereal(V1b))))))))).
tff(conj_thm_2Eiterate_2EREAL__SUP__LE__SUBSET,lemma,(( ! [V0s:$i] : (mem(V0s,arr(ty_2Erealax_2Ereal,bool)) => ( ! [V1t:$i] : (mem(V1t,arr(ty_2Erealax_2Ereal,bool)) => (((~~ (V0s = c_2Epred__set_2EEMPTY(ty_2Erealax_2Ereal))) & (p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Erealax_2Ereal),V0s),V1t)) & (? [V2b:tp__ty_2Erealax_2Ereal] : ( ! [V3x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V3x)),V1t)) => p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V3x)),inj__ty_2Erealax_2Ereal(V2b)))))))) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Esup,V0s)),ap(c_2Ereal_2Esup,V1t)))))))))).
tff(conj_thm_2Eiterate_2EREAL__LE__SUP,lemma,(( ! [V0s:$i] : (mem(V0s,arr(ty_2Erealax_2Ereal,bool)) => ( ! [V1a:tp__ty_2Erealax_2Ereal] : ( ! [V2b:tp__ty_2Erealax_2Ereal] : ( ! [V3y:tp__ty_2Erealax_2Ereal] : ((p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V3y)),V0s)) & (p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V1a)),inj__ty_2Erealax_2Ereal(V3y))) & ( ! [V4x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V4x)),V0s)) => p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V4x)),inj__ty_2Erealax_2Ereal(V2b))))))) => p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V1a)),ap(c_2Ereal_2Esup,V0s))))))))))).
tff(conj_thm_2Eiterate_2EREAL__SUP__BOUNDS,lemma,(( ! [V0s:$i] : (mem(V0s,arr(ty_2Erealax_2Ereal,bool)) => ( ! [V1a:tp__ty_2Erealax_2Ereal] : ( ! [V2b:tp__ty_2Erealax_2Ereal] : (((~~ (V0s = c_2Epred__set_2EEMPTY(ty_2Erealax_2Ereal))) & ( ! [V3x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V3x)),V0s)) => (p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V1a)),inj__ty_2Erealax_2Ereal(V3x))) & p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V3x)),inj__ty_2Erealax_2Ereal(V2b))))))) => (p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V1a)),ap(c_2Ereal_2Esup,V0s))) & p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Esup,V0s)),inj__ty_2Erealax_2Ereal(V2b))))))))))).
tff(conj_thm_2Eiterate_2EREAL__ABS__SUP__LE,lemma,(( ! [V0s:$i] : (mem(V0s,arr(ty_2Erealax_2Ereal,bool)) => ( ! [V1a:tp__ty_2Erealax_2Ereal] : (((~~ (V0s = c_2Epred__set_2EEMPTY(ty_2Erealax_2Ereal))) & ( ! [V2x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V2x)),V0s)) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Eabs,inj__ty_2Erealax_2Ereal(V2x))),inj__ty_2Erealax_2Ereal(V1a)))))) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Eabs,ap(c_2Ereal_2Esup,V0s))),inj__ty_2Erealax_2Ereal(V1a))))))))).
tff(conj_thm_2Eiterate_2EREAL__SUP__ASCLOSE,lemma,(( ! [V0s:$i] : (mem(V0s,arr(ty_2Erealax_2Ereal,bool)) => ( ! [V1l:tp__ty_2Erealax_2Ereal] : ( ! [V2e:tp__ty_2Erealax_2Ereal] : (((~~ (V0s = c_2Epred__set_2EEMPTY(ty_2Erealax_2Ereal))) & ( ! [V3x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V3x)),V0s)) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Eabs,ap(ap(c_2Ereal_2Ereal__sub,inj__ty_2Erealax_2Ereal(V3x)),inj__ty_2Erealax_2Ereal(V1l)))),inj__ty_2Erealax_2Ereal(V2e)))))) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Eabs,ap(ap(c_2Ereal_2Ereal__sub,ap(c_2Ereal_2Esup,V0s)),inj__ty_2Erealax_2Ereal(V1l)))),inj__ty_2Erealax_2Ereal(V2e)))))))))).
tff(conj_thm_2Eiterate_2ESUP__SING,lemma,(( ! [V0a:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Esup,ap(ap(c_2Epred__set_2EINSERT(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V0a)),c_2Epred__set_2EEMPTY(ty_2Erealax_2Ereal)))) = V0a)))).
tff(conj_thm_2Eiterate_2ESUP__UNIQUE,lemma,(( ! [V0s:$i] : (mem(V0s,arr(ty_2Erealax_2Ereal,bool)) => ( ! [V1b:tp__ty_2Erealax_2Ereal] : (( ! [V2c:tp__ty_2Erealax_2Ereal] : (( ! [V3x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V3x)),V0s)) => p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V3x)),inj__ty_2Erealax_2Ereal(V2c))))) <=> p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V1b)),inj__ty_2Erealax_2Ereal(V2c))))) => (surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Esup,V0s)) = V1b))))))).
tff(conj_thm_2Eiterate_2ESUP__UNION,lemma,(( ! [V0s:$i] : (mem(V0s,arr(ty_2Erealax_2Ereal,bool)) => ( ! [V1t:$i] : (mem(V1t,arr(ty_2Erealax_2Ereal,bool)) => (((~~ (V0s = c_2Epred__set_2EEMPTY(ty_2Erealax_2Ereal))) & ((~~ (V1t = c_2Epred__set_2EEMPTY(ty_2Erealax_2Ereal))) & ((? [V2b:tp__ty_2Erealax_2Ereal] : ( ! [V3x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V3x)),V0s)) => p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V3x)),inj__ty_2Erealax_2Ereal(V2b)))))) & (? [V4c:tp__ty_2Erealax_2Ereal] : ( ! [V5x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V5x)),V1t)) => p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V5x)),inj__ty_2Erealax_2Ereal(V4c))))))))) => (surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Esup,ap(ap(c_2Epred__set_2EUNION(ty_2Erealax_2Ereal),V0s),V1t))) = surj__ty_2Erealax_2Ereal(ap(ap(c_2Ereal_2Emax,ap(c_2Ereal_2Esup,V0s)),ap(c_2Ereal_2Esup,V1t))))))))))).
tff(ax_thm_2Eiterate_2Einf,axiom,( ! [V0s:$i] : (mem(V0s,arr(ty_2Erealax_2Ereal,bool)) => (surj__ty_2Erealax_2Ereal(ap(c_2Eiterate_2Einf,V0s)) = surj__ty_2Erealax_2Ereal(ap(c_2Emin_2E_40(ty_2Erealax_2Ereal),f3278(V0s))))))).
tff(conj_thm_2Eiterate_2EINF__EQ,lemma,(( ! [V0s:$i] : (mem(V0s,arr(ty_2Erealax_2Ereal,bool)) => ( ! [V1t:$i] : (mem(V1t,arr(ty_2Erealax_2Ereal,bool)) => (( ! [V2a:tp__ty_2Erealax_2Ereal] : (( ! [V3x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V3x)),V0s)) => p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V2a)),inj__ty_2Erealax_2Ereal(V3x))))) <=> ( ! [V4x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V4x)),V1t)) => p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V2a)),inj__ty_2Erealax_2Ereal(V4x))))))) => (surj__ty_2Erealax_2Ereal(ap(c_2Eiterate_2Einf,V0s)) = surj__ty_2Erealax_2Ereal(ap(c_2Eiterate_2Einf,V1t)))))))))).
tff(conj_thm_2Eiterate_2EINF,lemma,(( ! [V0s:$i] : (mem(V0s,arr(ty_2Erealax_2Ereal,bool)) => (((~~ (V0s = c_2Epred__set_2EEMPTY(ty_2Erealax_2Ereal))) & (? [V1b:tp__ty_2Erealax_2Ereal] : ( ! [V2x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V2x)),V0s)) => p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V1b)),inj__ty_2Erealax_2Ereal(V2x))))))) => (( ! [V3x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V3x)),V0s)) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Eiterate_2Einf,V0s)),inj__ty_2Erealax_2Ereal(V3x))))) & ( ! [V4b:tp__ty_2Erealax_2Ereal] : (( ! [V5x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V5x)),V0s)) => p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V4b)),inj__ty_2Erealax_2Ereal(V5x))))) => p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V4b)),ap(c_2Eiterate_2Einf,V0s))))))))))).
tff(conj_thm_2Eiterate_2EINF__FINITE__LEMMA,lemma,(( ! [V0s:$i] : (mem(V0s,arr(ty_2Erealax_2Ereal,bool)) => ((p(ap(c_2Epred__set_2EFINITE(ty_2Erealax_2Ereal),V0s)) & (~~ (V0s = c_2Epred__set_2EEMPTY(ty_2Erealax_2Ereal)))) => (? [V1b:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V1b)),V0s)) & ( ! [V2x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V2x)),V0s)) => p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V1b)),inj__ty_2Erealax_2Ereal(V2x)))))))))))).
tff(conj_thm_2Eiterate_2EINF__FINITE,lemma,(( ! [V0s:$i] : (mem(V0s,arr(ty_2Erealax_2Ereal,bool)) => ((p(ap(c_2Epred__set_2EFINITE(ty_2Erealax_2Ereal),V0s)) & (~~ (V0s = c_2Epred__set_2EEMPTY(ty_2Erealax_2Ereal)))) => (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),ap(c_2Eiterate_2Einf,V0s)),V0s)) & ( ! [V1x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V1x)),V0s)) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Eiterate_2Einf,V0s)),inj__ty_2Erealax_2Ereal(V1x))))))))))).
tff(conj_thm_2Eiterate_2EREAL__LE__INF__FINITE,lemma,(( ! [V0s:$i] : (mem(V0s,arr(ty_2Erealax_2Ereal,bool)) => ( ! [V1a:tp__ty_2Erealax_2Ereal] : ((p(ap(c_2Epred__set_2EFINITE(ty_2Erealax_2Ereal),V0s)) & (~~ (V0s = c_2Epred__set_2EEMPTY(ty_2Erealax_2Ereal)))) => (p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V1a)),ap(c_2Eiterate_2Einf,V0s))) <=> ( ! [V2x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V2x)),V0s)) => p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V1a)),inj__ty_2Erealax_2Ereal(V2x)))))))))))).
tff(conj_thm_2Eiterate_2EREAL__INF__LE__FINITE,lemma,(( ! [V0s:$i] : (mem(V0s,arr(ty_2Erealax_2Ereal,bool)) => ( ! [V1a:tp__ty_2Erealax_2Ereal] : ((p(ap(c_2Epred__set_2EFINITE(ty_2Erealax_2Ereal),V0s)) & (~~ (V0s = c_2Epred__set_2EEMPTY(ty_2Erealax_2Ereal)))) => (p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Eiterate_2Einf,V0s)),inj__ty_2Erealax_2Ereal(V1a))) <=> (? [V2x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V2x)),V0s)) & p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V2x)),inj__ty_2Erealax_2Ereal(V1a)))))))))))).
tff(conj_thm_2Eiterate_2EREAL__LT__INF__FINITE,lemma,(( ! [V0s:$i] : (mem(V0s,arr(ty_2Erealax_2Ereal,bool)) => ( ! [V1a:tp__ty_2Erealax_2Ereal] : ((p(ap(c_2Epred__set_2EFINITE(ty_2Erealax_2Ereal),V0s)) & (~~ (V0s = c_2Epred__set_2EEMPTY(ty_2Erealax_2Ereal)))) => (p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V1a)),ap(c_2Eiterate_2Einf,V0s))) <=> ( ! [V2x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V2x)),V0s)) => p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V1a)),inj__ty_2Erealax_2Ereal(V2x)))))))))))).
tff(conj_thm_2Eiterate_2EREAL__INF__LT__FINITE,lemma,(( ! [V0s:$i] : (mem(V0s,arr(ty_2Erealax_2Ereal,bool)) => ( ! [V1a:tp__ty_2Erealax_2Ereal] : ((p(ap(c_2Epred__set_2EFINITE(ty_2Erealax_2Ereal),V0s)) & (~~ (V0s = c_2Epred__set_2EEMPTY(ty_2Erealax_2Ereal)))) => (p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Eiterate_2Einf,V0s)),inj__ty_2Erealax_2Ereal(V1a))) <=> (? [V2x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V2x)),V0s)) & p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V2x)),inj__ty_2Erealax_2Ereal(V1a)))))))))))).
tff(conj_thm_2Eiterate_2EREAL__INF__UNIQUE,lemma,(( ! [V0s:$i] : (mem(V0s,arr(ty_2Erealax_2Ereal,bool)) => ( ! [V1b:tp__ty_2Erealax_2Ereal] : ((( ! [V2x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V2x)),V0s)) => p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V1b)),inj__ty_2Erealax_2Ereal(V2x))))) & ( ! [V3b_27:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V1b)),inj__ty_2Erealax_2Ereal(V3b_27))) => (? [V4x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V4x)),V0s)) & p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V4x)),inj__ty_2Erealax_2Ereal(V3b_27)))))))) => (surj__ty_2Erealax_2Ereal(ap(c_2Eiterate_2Einf,V0s)) = V1b))))))).
tff(conj_thm_2Eiterate_2EREAL__LE__INF,lemma,(( ! [V0s:$i] : (mem(V0s,arr(ty_2Erealax_2Ereal,bool)) => ( ! [V1b:tp__ty_2Erealax_2Ereal] : (((~~ (V0s = c_2Epred__set_2EEMPTY(ty_2Erealax_2Ereal))) & ( ! [V2x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V2x)),V0s)) => p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V1b)),inj__ty_2Erealax_2Ereal(V2x)))))) => p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V1b)),ap(c_2Eiterate_2Einf,V0s))))))))).
tff(conj_thm_2Eiterate_2EREAL__LE__INF__SUBSET,lemma,(( ! [V0s:$i] : (mem(V0s,arr(ty_2Erealax_2Ereal,bool)) => ( ! [V1t:$i] : (mem(V1t,arr(ty_2Erealax_2Ereal,bool)) => (((~~ (V1t = c_2Epred__set_2EEMPTY(ty_2Erealax_2Ereal))) & (p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Erealax_2Ereal),V1t),V0s)) & (? [V2b:tp__ty_2Erealax_2Ereal] : ( ! [V3x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V3x)),V0s)) => p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V2b)),inj__ty_2Erealax_2Ereal(V3x)))))))) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Eiterate_2Einf,V0s)),ap(c_2Eiterate_2Einf,V1t)))))))))).
tff(conj_thm_2Eiterate_2EREAL__INF__BOUNDS,lemma,(( ! [V0s:$i] : (mem(V0s,arr(ty_2Erealax_2Ereal,bool)) => ( ! [V1a:tp__ty_2Erealax_2Ereal] : ( ! [V2b:tp__ty_2Erealax_2Ereal] : (((~~ (V0s = c_2Epred__set_2EEMPTY(ty_2Erealax_2Ereal))) & ( ! [V3x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V3x)),V0s)) => (p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V1a)),inj__ty_2Erealax_2Ereal(V3x))) & p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V3x)),inj__ty_2Erealax_2Ereal(V2b))))))) => (p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V1a)),ap(c_2Eiterate_2Einf,V0s))) & p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Eiterate_2Einf,V0s)),inj__ty_2Erealax_2Ereal(V2b))))))))))).
tff(conj_thm_2Eiterate_2EREAL__ABS__INF__LE,lemma,(( ! [V0s:$i] : (mem(V0s,arr(ty_2Erealax_2Ereal,bool)) => ( ! [V1a:tp__ty_2Erealax_2Ereal] : (((~~ (V0s = c_2Epred__set_2EEMPTY(ty_2Erealax_2Ereal))) & ( ! [V2x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V2x)),V0s)) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Eabs,inj__ty_2Erealax_2Ereal(V2x))),inj__ty_2Erealax_2Ereal(V1a)))))) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Eabs,ap(c_2Eiterate_2Einf,V0s))),inj__ty_2Erealax_2Ereal(V1a))))))))).
tff(conj_thm_2Eiterate_2EREAL__INF__ASCLOSE,lemma,(( ! [V0s:$i] : (mem(V0s,arr(ty_2Erealax_2Ereal,bool)) => ( ! [V1l:tp__ty_2Erealax_2Ereal] : ( ! [V2e:tp__ty_2Erealax_2Ereal] : (((~~ (V0s = c_2Epred__set_2EEMPTY(ty_2Erealax_2Ereal))) & ( ! [V3x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V3x)),V0s)) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Eabs,ap(ap(c_2Ereal_2Ereal__sub,inj__ty_2Erealax_2Ereal(V3x)),inj__ty_2Erealax_2Ereal(V1l)))),inj__ty_2Erealax_2Ereal(V2e)))))) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Eabs,ap(ap(c_2Ereal_2Ereal__sub,ap(c_2Eiterate_2Einf,V0s)),inj__ty_2Erealax_2Ereal(V1l)))),inj__ty_2Erealax_2Ereal(V2e)))))))))).
tff(conj_thm_2Eiterate_2ESUP__UNIQUE__FINITE,lemma,(( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1s:$i] : (mem(V1s,arr(ty_2Erealax_2Ereal,bool)) => ((p(ap(c_2Epred__set_2EFINITE(ty_2Erealax_2Ereal),V1s)) & (~~ (V1s = c_2Epred__set_2EEMPTY(ty_2Erealax_2Ereal)))) => ((surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Esup,V1s)) = V0a) <=> (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V0a)),V1s)) & ( ! [V2y:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V2y)),V1s)) => p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V2y)),inj__ty_2Erealax_2Ereal(V0a))))))))))))).
tff(conj_thm_2Eiterate_2EINF__UNIQUE__FINITE,lemma,(( ! [V0a:tp__ty_2Erealax_2Ereal] : ( ! [V1s:$i] : (mem(V1s,arr(ty_2Erealax_2Ereal,bool)) => ((p(ap(c_2Epred__set_2EFINITE(ty_2Erealax_2Ereal),V1s)) & (~~ (V1s = c_2Epred__set_2EEMPTY(ty_2Erealax_2Ereal)))) => ((surj__ty_2Erealax_2Ereal(ap(c_2Eiterate_2Einf,V1s)) = V0a) <=> (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V0a)),V1s)) & ( ! [V2y:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V2y)),V1s)) => p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V0a)),inj__ty_2Erealax_2Ereal(V2y))))))))))))).
tff(conj_thm_2Eiterate_2ESUP__INSERT__FINITE,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1s:$i] : (mem(V1s,arr(ty_2Erealax_2Ereal,bool)) => (p(ap(c_2Epred__set_2EFINITE(ty_2Erealax_2Ereal),V1s)) => (surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Esup,ap(ap(c_2Epred__set_2EINSERT(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V0x)),V1s))) = surj__ty_2Erealax_2Ereal(ap(ap(ap(c_2Ebool_2ECOND(ty_2Erealax_2Ereal),ap(ap(c_2Emin_2E_3D(arr(ty_2Erealax_2Ereal,bool)),V1s),c_2Epred__set_2EEMPTY(ty_2Erealax_2Ereal))),inj__ty_2Erealax_2Ereal(V0x)),ap(ap(c_2Ereal_2Emax,inj__ty_2Erealax_2Ereal(V0x)),ap(c_2Ereal_2Esup,V1s))))))))))).
tff(conj_thm_2Eiterate_2EINF__INSERT__FINITE,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1s:$i] : (mem(V1s,arr(ty_2Erealax_2Ereal,bool)) => (p(ap(c_2Epred__set_2EFINITE(ty_2Erealax_2Ereal),V1s)) => (surj__ty_2Erealax_2Ereal(ap(c_2Eiterate_2Einf,ap(ap(c_2Epred__set_2EINSERT(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V0x)),V1s))) = surj__ty_2Erealax_2Ereal(ap(ap(ap(c_2Ebool_2ECOND(ty_2Erealax_2Ereal),ap(ap(c_2Emin_2E_3D(arr(ty_2Erealax_2Ereal,bool)),V1s),c_2Epred__set_2EEMPTY(ty_2Erealax_2Ereal))),inj__ty_2Erealax_2Ereal(V0x)),ap(ap(c_2Ereal_2Emin,inj__ty_2Erealax_2Ereal(V0x)),ap(c_2Eiterate_2Einf,V1s))))))))))).
tff(conj_thm_2Eiterate_2EREAL__SUP__EQ__INF,lemma,(( ! [V0s:$i] : (mem(V0s,arr(ty_2Erealax_2Ereal,bool)) => (((~~ (V0s = c_2Epred__set_2EEMPTY(ty_2Erealax_2Ereal))) & (? [V1B:tp__ty_2Erealax_2Ereal] : ( ! [V2x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ebool_2EIN(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V2x)),V0s)) => p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Eabs,inj__ty_2Erealax_2Ereal(V2x))),inj__ty_2Erealax_2Ereal(V1B))))))) => ((surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Esup,V0s)) = surj__ty_2Erealax_2Ereal(ap(c_2Eiterate_2Einf,V0s))) <=> (? [V3a:tp__ty_2Erealax_2Ereal] : (V0s = ap(ap(c_2Epred__set_2EINSERT(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V3a)),c_2Epred__set_2EEMPTY(ty_2Erealax_2Ereal)))))))))).
tff(conj_thm_2Eiterate_2EINF__SING,lemma,(( ! [V0a:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(c_2Eiterate_2Einf,ap(ap(c_2Epred__set_2EINSERT(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V0a)),c_2Epred__set_2EEMPTY(ty_2Erealax_2Ereal)))) = V0a)))).
tff(ax_thm_2Eiterate_2Enumseg,axiom,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (ap(ap(c_2Eiterate_2E_2E_2E,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)) = ap(c_2Epred__set_2EGSPEC(ty_2Enum_2Enum,ty_2Enum_2Enum),f3279(V1n,V0m)))))).
tff(conj_thm_2Eiterate_2EFINITE__NUMSEG,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : p(ap(c_2Epred__set_2EFINITE(ty_2Enum_2Enum),ap(ap(c_2Eiterate_2E_2E_2E,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))))))).
tff(conj_thm_2Eiterate_2ENUMSEG__COMBINE__R,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1p:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1p)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))) & p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1p)),inj__ty_2Enum_2Enum(V2n)))) => (ap(ap(c_2Epred__set_2EUNION(ty_2Enum_2Enum),ap(ap(c_2Eiterate_2E_2E_2E,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1p))),ap(ap(c_2Eiterate_2E_2E_2E,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1p)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),inj__ty_2Enum_2Enum(V2n))) = ap(ap(c_2Eiterate_2E_2E_2E,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2n))))))))).
tff(conj_thm_2Eiterate_2ENUMSEG__COMBINE__L,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1p:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1p))) & p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1p)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V2n)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) => (ap(ap(c_2Epred__set_2EUNION(ty_2Enum_2Enum),ap(ap(c_2Eiterate_2E_2E_2E,inj__ty_2Enum_2Enum(V0m)),ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V1p)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),ap(ap(c_2Eiterate_2E_2E_2E,inj__ty_2Enum_2Enum(V1p)),inj__ty_2Enum_2Enum(V2n))) = ap(ap(c_2Eiterate_2E_2E_2E,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2n))))))))).
tff(conj_thm_2Eiterate_2ENUMSEG__LREC,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) => (ap(ap(c_2Epred__set_2EINSERT(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V0m)),ap(ap(c_2Eiterate_2E_2E_2E,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),inj__ty_2Enum_2Enum(V1n))) = ap(ap(c_2Eiterate_2E_2E_2E,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))))))).
tff(conj_thm_2Eiterate_2ENUMSEG__RREC,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) => (ap(ap(c_2Epred__set_2EINSERT(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V1n)),ap(ap(c_2Eiterate_2E_2E_2E,inj__ty_2Enum_2Enum(V0m)),ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V1n)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))) = ap(ap(c_2Eiterate_2E_2E_2E,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))))))).
tff(conj_thm_2Eiterate_2ENUMSEG__REC,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1n)))) => (ap(ap(c_2Eiterate_2E_2E_2E,inj__ty_2Enum_2Enum(V0m)),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1n))) = ap(ap(c_2Epred__set_2EINSERT(ty_2Enum_2Enum),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1n))),ap(ap(c_2Eiterate_2E_2E_2E,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))))))))).
tff(conj_thm_2Eiterate_2EIN__NUMSEG,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V2p)),ap(ap(c_2Eiterate_2E_2E_2E,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))) <=> (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2p))) & p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V2p)),inj__ty_2Enum_2Enum(V1n)))))))))).
tff(conj_thm_2Eiterate_2EIN__NUMSEG__0,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V0m)),ap(ap(c_2Eiterate_2E_2E_2E,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V1n)))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))))))).
tff(conj_thm_2Eiterate_2ENUMSEG__SING,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (ap(ap(c_2Eiterate_2E_2E_2E,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V0n)) = ap(ap(c_2Epred__set_2EINSERT(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V0n)),c_2Epred__set_2EEMPTY(ty_2Enum_2Enum)))))).
tff(conj_thm_2Eiterate_2ENUMSEG__EMPTY,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((ap(ap(c_2Eiterate_2E_2E_2E,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)) = c_2Epred__set_2EEMPTY(ty_2Enum_2Enum)) <=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V0m)))))))).
tff(conj_thm_2Eiterate_2ECARD__NUMSEG__LEMMA,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1d:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Epred__set_2ECARD(ty_2Enum_2Enum),ap(ap(c_2Eiterate_2E_2E_2E,inj__ty_2Enum_2Enum(V0m)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1d))))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1d)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))).
tff(conj_thm_2Eiterate_2ECARD__NUMSEG,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Epred__set_2ECARD(ty_2Enum_2Enum),ap(ap(c_2Eiterate_2E_2E_2E,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1n)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),inj__ty_2Enum_2Enum(V0m)))))))).
tff(conj_thm_2Eiterate_2EHAS__SIZE__NUMSEG,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Ecardinal_2EHAS__SIZE(ty_2Enum_2Enum),ap(ap(c_2Eiterate_2E_2E_2E,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),ap(ap(c_2Earithmetic_2E_2D,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1n)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),inj__ty_2Enum_2Enum(V0m)))))))).
tff(conj_thm_2Eiterate_2ECARD__NUMSEG__1,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Epred__set_2ECARD(ty_2Enum_2Enum),ap(ap(c_2Eiterate_2E_2E_2E,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(V0n)))) = V0n)))).
tff(conj_thm_2Eiterate_2EHAS__SIZE__NUMSEG__1,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Ecardinal_2EHAS__SIZE(ty_2Enum_2Enum),ap(ap(c_2Eiterate_2E_2E_2E,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(V0n))),inj__ty_2Enum_2Enum(V0n)))))).
tff(conj_thm_2Eiterate_2ENUMSEG__CLAUSES,lemma,((( ! [V0m:tp__ty_2Enum_2Enum] : (ap(ap(c_2Eiterate_2E_2E_2E,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)) = ap(ap(ap(c_2Ebool_2ECOND(arr(ty_2Enum_2Enum,bool)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(ap(c_2Epred__set_2EINSERT(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),c_2Epred__set_2EEMPTY(ty_2Enum_2Enum))),c_2Epred__set_2EEMPTY(ty_2Enum_2Enum)))) & ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : (ap(ap(c_2Eiterate_2E_2E_2E,inj__ty_2Enum_2Enum(V1m)),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V2n))) = ap(ap(ap(c_2Ebool_2ECOND(arr(ty_2Enum_2Enum,bool)),ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1m)),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V2n)))),ap(ap(c_2Epred__set_2EINSERT(ty_2Enum_2Enum),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V2n))),ap(ap(c_2Eiterate_2E_2E_2E,inj__ty_2Enum_2Enum(V1m)),inj__ty_2Enum_2Enum(V2n)))),ap(ap(c_2Eiterate_2E_2E_2E,inj__ty_2Enum_2Enum(V1m)),inj__ty_2Enum_2Enum(V2n))))))))).
tff(conj_thm_2Eiterate_2EFINITE__INDEX__NUMSEG,lemma,(( ! [A_27a:del]: ( ! [V0s:$i] : (mem(V0s,arr(A_27a,bool)) => (p(ap(c_2Epred__set_2EFINITE(A_27a),V0s)) <=> (? [V1f:$i] : (mem(V1f,arr(ty_2Enum_2Enum,A_27a)) & (( ! [V2i:tp__ty_2Enum_2Enum] : ( ! [V3j:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V2i)),ap(ap(c_2Eiterate_2E_2E_2E,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(c_2Epred__set_2ECARD(A_27a),V0s)))) & (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V3j)),ap(ap(c_2Eiterate_2E_2E_2E,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(c_2Epred__set_2ECARD(A_27a),V0s)))) & (ap(V1f,inj__ty_2Enum_2Enum(V2i)) = ap(V1f,inj__ty_2Enum_2Enum(V3j))))) => (V2i = V3j)))) & (V0s = ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,A_27a),V1f),ap(ap(c_2Eiterate_2E_2E_2E,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(c_2Epred__set_2ECARD(A_27a),V0s))))))))))))).
tff(conj_thm_2Eiterate_2EFINITE__INDEX__NUMBERS,lemma,(( ! [A_27a:del]: ( ! [V0s:$i] : (mem(V0s,arr(A_27a,bool)) => (p(ap(c_2Epred__set_2EFINITE(A_27a),V0s)) <=> (? [V1k:$i] : (mem(V1k,arr(ty_2Enum_2Enum,bool)) & (? [V2f:$i] : (mem(V2f,arr(ty_2Enum_2Enum,A_27a)) & (( ! [V3i:tp__ty_2Enum_2Enum] : ( ! [V4j:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V3i)),V1k)) & (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V4j)),V1k)) & (ap(V2f,inj__ty_2Enum_2Enum(V3i)) = ap(V2f,inj__ty_2Enum_2Enum(V4j))))) => (V3i = V4j)))) & (p(ap(c_2Epred__set_2EFINITE(ty_2Enum_2Enum),V1k)) & (V0s = ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,A_27a),V2f),V1k)))))))))))))).
tff(conj_thm_2Eiterate_2EDISJOINT__NUMSEG,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : ( ! [V3q:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Epred__set_2EDISJOINT(ty_2Enum_2Enum),ap(ap(c_2Eiterate_2E_2E_2E,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),ap(ap(c_2Eiterate_2E_2E_2E,inj__ty_2Enum_2Enum(V2p)),inj__ty_2Enum_2Enum(V3q)))) <=> (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p))) | (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V3q)),inj__ty_2Enum_2Enum(V0m))) | (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V0m))) | p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V3q)),inj__ty_2Enum_2Enum(V2p))))))))))))).
tff(conj_thm_2Eiterate_2ENUMSEG__ADD__SPLIT,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1n)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))) => (ap(ap(c_2Eiterate_2E_2E_2E,inj__ty_2Enum_2Enum(V0m)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p))) = ap(ap(c_2Epred__set_2EUNION(ty_2Enum_2Enum),ap(ap(c_2Eiterate_2E_2E_2E,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),ap(ap(c_2Eiterate_2E_2E_2E,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1n)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p))))))))))).
tff(conj_thm_2Eiterate_2ENUMSEG__OFFSET__IMAGE,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (ap(ap(c_2Eiterate_2E_2E_2E,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2p))),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p))) = ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,ty_2Enum_2Enum),f3280(V2p)),ap(ap(c_2Eiterate_2E_2E_2E,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))))))))).
tff(conj_thm_2Eiterate_2ESUBSET__NUMSEG,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : ( ! [V3q:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Epred__set_2ESUBSET(ty_2Enum_2Enum),ap(ap(c_2Eiterate_2E_2E_2E,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),ap(ap(c_2Eiterate_2E_2E_2E,inj__ty_2Enum_2Enum(V2p)),inj__ty_2Enum_2Enum(V3q)))) <=> (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V0m))) | (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V2p)),inj__ty_2Enum_2Enum(V0m))) & p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V3q)))))))))))).
tff(conj_thm_2Eiterate_2ENUMSEG__LE,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (ap(c_2Epred__set_2EGSPEC(ty_2Enum_2Enum,ty_2Enum_2Enum),f3281(V0n)) = ap(ap(c_2Eiterate_2E_2E_2E,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n)))))).
tff(conj_thm_2Eiterate_2ENUMSEG__LT,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (ap(c_2Epred__set_2EGSPEC(ty_2Enum_2Enum,ty_2Enum_2Enum),f3282(V0n)) = ap(ap(ap(c_2Ebool_2ECOND(arr(ty_2Enum_2Enum,bool)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),c_2Epred__set_2EEMPTY(ty_2Enum_2Enum)),ap(ap(c_2Eiterate_2E_2E_2E,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0n)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))).
tff(conj_thm_2Eiterate_2ETOPOLOGICAL__SORT,lemma,(( ! [A_27a:del]: ( ! [V0_3C_3C:$i] : (mem(V0_3C_3C,arr(A_27a,arr(A_27a,bool))) => ((( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => ((p(ap(ap(V0_3C_3C,V1x),V2y)) & p(ap(ap(V0_3C_3C,V2y),V1x))) => (V1x = V2y)))))) & ( ! [V3x:$i] : (mem(V3x,A_27a) => ( ! [V4y:$i] : (mem(V4y,A_27a) => ( ! [V5z:$i] : (mem(V5z,A_27a) => ((p(ap(ap(V0_3C_3C,V3x),V4y)) & p(ap(ap(V0_3C_3C,V4y),V5z))) => p(ap(ap(V0_3C_3C,V3x),V5z)))))))))) => ( ! [V6n:tp__ty_2Enum_2Enum] : ( ! [V7s:$i] : (mem(V7s,arr(A_27a,bool)) => (p(ap(ap(c_2Ecardinal_2EHAS__SIZE(A_27a),V7s),inj__ty_2Enum_2Enum(V6n))) => (? [V8f:$i] : (mem(V8f,arr(ty_2Enum_2Enum,A_27a)) & ((V7s = ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,A_27a),V8f),ap(ap(c_2Eiterate_2E_2E_2E,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(V6n)))) & ( ! [V9j:tp__ty_2Enum_2Enum] : ( ! [V10k:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V9j)),ap(ap(c_2Eiterate_2E_2E_2E,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(V6n)))) & (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V10k)),ap(ap(c_2Eiterate_2E_2E_2E,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(V6n)))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V9j)),inj__ty_2Enum_2Enum(V10k))))) => (~~ p(ap(ap(V0_3C_3C,ap(V8f,inj__ty_2Enum_2Enum(V10k))),ap(V8f,inj__ty_2Enum_2Enum(V9j))))))))))))))))))))).
tff(ax_thm_2Eiterate_2Eneutral,axiom,( ! [A_27a:del]: ( ! [V0op:$i] : (mem(V0op,arr(A_27a,arr(A_27a,A_27a))) => (ap(c_2Eiterate_2Eneutral(A_27a),V0op) = ap(c_2Emin_2E_40(A_27a),f3284(A_27a,V0op))))))).
tff(ax_thm_2Eiterate_2Emonoidal,axiom,( ! [A_27a:del]: ( ! [V0op:$i] : (mem(V0op,arr(A_27a,arr(A_27a,A_27a))) => (p(ap(c_2Eiterate_2Emonoidal(A_27a),V0op)) <=> (( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => (ap(ap(V0op,V1x),V2y) = ap(ap(V0op,V2y),V1x)))))) & (( ! [V3x:$i] : (mem(V3x,A_27a) => ( ! [V4y:$i] : (mem(V4y,A_27a) => ( ! [V5z:$i] : (mem(V5z,A_27a) => (ap(ap(V0op,V3x),ap(ap(V0op,V4y),V5z)) = ap(ap(V0op,ap(ap(V0op,V3x),V4y)),V5z)))))))) & ( ! [V6x:$i] : (mem(V6x,A_27a) => (ap(ap(V0op,ap(c_2Eiterate_2Eneutral(A_27a),V0op)),V6x) = V6x)))))))))).
tff(conj_thm_2Eiterate_2EMONOIDAL__AC,lemma,(( ! [A_27a:del]: ( ! [V0op:$i] : (mem(V0op,arr(A_27a,arr(A_27a,A_27a))) => (p(ap(c_2Eiterate_2Emonoidal(A_27a),V0op)) => (( ! [V1a:$i] : (mem(V1a,A_27a) => (ap(ap(V0op,ap(c_2Eiterate_2Eneutral(A_27a),V0op)),V1a) = V1a))) & (( ! [V2a:$i] : (mem(V2a,A_27a) => (ap(ap(V0op,V2a),ap(c_2Eiterate_2Eneutral(A_27a),V0op)) = V2a))) & (( ! [V3a:$i] : (mem(V3a,A_27a) => ( ! [V4b:$i] : (mem(V4b,A_27a) => (ap(ap(V0op,V3a),V4b) = ap(ap(V0op,V4b),V3a)))))) & (( ! [V5a:$i] : (mem(V5a,A_27a) => ( ! [V6b:$i] : (mem(V6b,A_27a) => ( ! [V7c:$i] : (mem(V7c,A_27a) => (ap(ap(V0op,ap(ap(V0op,V5a),V6b)),V7c) = ap(ap(V0op,V5a),ap(ap(V0op,V6b),V7c))))))))) & ( ! [V8a:$i] : (mem(V8a,A_27a) => ( ! [V9b:$i] : (mem(V9b,A_27a) => ( ! [V10c:$i] : (mem(V10c,A_27a) => (ap(ap(V0op,V8a),ap(ap(V0op,V9b),V10c)) = ap(ap(V0op,V9b),ap(ap(V0op,V8a),V10c))))))))))))))))))).
tff(ax_thm_2Eiterate_2Esupport,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0op:$i] : (mem(V0op,arr(A_27b,arr(A_27b,A_27b))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,A_27b)) => ( ! [V2s:$i] : (mem(V2s,arr(A_27a,bool)) => (ap(ap(ap(c_2Eiterate_2Esupport(A_27a,A_27b),V0op),V1f),V2s) = ap(c_2Epred__set_2EGSPEC(A_27a,A_27a),f3285(A_27b,A_27a,V2s,V0op,V1f)))))))))))).
tff(ax_thm_2Eiterate_2Eiterate,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0op:$i] : (mem(V0op,arr(A_27b,arr(A_27b,A_27b))) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => ( ! [V2f:$i] : (mem(V2f,arr(A_27a,A_27b)) => (ap(ap(ap(c_2Eiterate_2Eiterate(A_27a,A_27b),V0op),V1s),V2f) = ap(ap(ap(c_2Ebool_2ECOND(A_27b),ap(c_2Epred__set_2EFINITE(A_27a),ap(ap(ap(c_2Eiterate_2Esupport(A_27a,A_27b),V0op),V2f),V1s))),ap(ap(ap(c_2Eiterate_2EITSET(A_27b,A_27a),f3287(A_27a,A_27b,V0op,V2f)),ap(ap(ap(c_2Eiterate_2Esupport(A_27a,A_27b),V0op),V2f),V1s)),ap(c_2Eiterate_2Eneutral(A_27b),V0op))),ap(c_2Eiterate_2Eneutral(A_27b),V0op)))))))))))).
tff(conj_thm_2Eiterate_2EIN__SUPPORT,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0op:$i] : (mem(V0op,arr(A_27a,arr(A_27a,A_27a))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27b,A_27a)) => ( ! [V2x:$i] : (mem(V2x,A_27b) => ( ! [V3s:$i] : (mem(V3s,arr(A_27b,bool)) => (p(ap(ap(c_2Ebool_2EIN(A_27b),V2x),ap(ap(ap(c_2Eiterate_2Esupport(A_27b,A_27a),V0op),V1f),V3s))) <=> (p(ap(ap(c_2Ebool_2EIN(A_27b),V2x),V3s)) & (~~ (ap(V1f,V2x) = ap(c_2Eiterate_2Eneutral(A_27a),V0op))))))))))))))))).
tff(conj_thm_2Eiterate_2ESUPPORT__SUPPORT,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0op:$i] : (mem(V0op,arr(A_27a,arr(A_27a,A_27a))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27b,A_27a)) => ( ! [V2s:$i] : (mem(V2s,arr(A_27b,bool)) => (ap(ap(ap(c_2Eiterate_2Esupport(A_27b,A_27a),V0op),V1f),ap(ap(ap(c_2Eiterate_2Esupport(A_27b,A_27a),V0op),V1f),V2s)) = ap(ap(ap(c_2Eiterate_2Esupport(A_27b,A_27a),V0op),V1f),V2s)))))))))))).
tff(conj_thm_2Eiterate_2ESUPPORT__EMPTY,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0op:$i] : (mem(V0op,arr(A_27a,arr(A_27a,A_27a))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27b,A_27a)) => ( ! [V2s:$i] : (mem(V2s,arr(A_27b,bool)) => (( ! [V3x:$i] : (mem(V3x,A_27b) => (p(ap(ap(c_2Ebool_2EIN(A_27b),V3x),V2s)) => (ap(V1f,V3x) = ap(c_2Eiterate_2Eneutral(A_27a),V0op))))) <=> (ap(ap(ap(c_2Eiterate_2Esupport(A_27b,A_27a),V0op),V1f),V2s) = c_2Epred__set_2EEMPTY(A_27b))))))))))))).
tff(conj_thm_2Eiterate_2ESUPPORT__SUBSET,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0op:$i] : (mem(V0op,arr(A_27a,arr(A_27a,A_27a))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27b,A_27a)) => ( ! [V2s:$i] : (mem(V2s,arr(A_27b,bool)) => p(ap(ap(c_2Epred__set_2ESUBSET(A_27b),ap(ap(ap(c_2Eiterate_2Esupport(A_27b,A_27a),V0op),V1f),V2s)),V2s)))))))))))).
tff(conj_thm_2Eiterate_2EFINITE__SUPPORT,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0op:$i] : (mem(V0op,arr(A_27a,arr(A_27a,A_27a))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27b,A_27a)) => ( ! [V2s:$i] : (mem(V2s,arr(A_27b,bool)) => (p(ap(c_2Epred__set_2EFINITE(A_27b),V2s)) => p(ap(c_2Epred__set_2EFINITE(A_27b),ap(ap(ap(c_2Eiterate_2Esupport(A_27b,A_27a),V0op),V1f),V2s)))))))))))))).
tff(conj_thm_2Eiterate_2ESUPPORT__CLAUSES,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [A_27e:del]: ( ! [A_27f:del]: ( ! [A_27g:del]: ( ! [A_27h:del]: ( ! [A_27i:del]: ( ! [V0op:$i] : (mem(V0op,arr(A_27b,arr(A_27b,A_27b))) => (( ! [V1f:$i] : (mem(V1f,arr(A_27a,A_27b)) => (ap(ap(ap(c_2Eiterate_2Esupport(A_27a,A_27b),V0op),V1f),c_2Epred__set_2EEMPTY(A_27a)) = c_2Epred__set_2EEMPTY(A_27a)))) & (( ! [V2f:$i] : (mem(V2f,arr(A_27c,A_27b)) => ( ! [V3x:$i] : (mem(V3x,A_27c) => ( ! [V4s:$i] : (mem(V4s,arr(A_27c,bool)) => (ap(ap(ap(c_2Eiterate_2Esupport(A_27c,A_27b),V0op),V2f),ap(ap(c_2Epred__set_2EINSERT(A_27c),V3x),V4s)) = ap(ap(ap(c_2Ebool_2ECOND(arr(A_27c,bool)),ap(ap(c_2Emin_2E_3D(A_27b),ap(V2f,V3x)),ap(c_2Eiterate_2Eneutral(A_27b),V0op))),ap(ap(ap(c_2Eiterate_2Esupport(A_27c,A_27b),V0op),V2f),V4s)),ap(ap(c_2Epred__set_2EINSERT(A_27c),V3x),ap(ap(ap(c_2Eiterate_2Esupport(A_27c,A_27b),V0op),V2f),V4s)))))))))) & (( ! [V5f:$i] : (mem(V5f,arr(A_27d,A_27b)) => ( ! [V6x:$i] : (mem(V6x,A_27d) => ( ! [V7s:$i] : (mem(V7s,arr(A_27d,bool)) => (ap(ap(ap(c_2Eiterate_2Esupport(A_27d,A_27b),V0op),V5f),ap(ap(c_2Epred__set_2EDELETE(A_27d),V7s),V6x)) = ap(ap(c_2Epred__set_2EDELETE(A_27d),ap(ap(ap(c_2Eiterate_2Esupport(A_27d,A_27b),V0op),V5f),V7s)),V6x)))))))) & (( ! [V8f:$i] : (mem(V8f,arr(A_27e,A_27b)) => ( ! [V9s:$i] : (mem(V9s,arr(A_27e,bool)) => ( ! [V10t:$i] : (mem(V10t,arr(A_27e,bool)) => (ap(ap(ap(c_2Eiterate_2Esupport(A_27e,A_27b),V0op),V8f),ap(ap(c_2Epred__set_2EUNION(A_27e),V9s),V10t)) = ap(ap(c_2Epred__set_2EUNION(A_27e),ap(ap(ap(c_2Eiterate_2Esupport(A_27e,A_27b),V0op),V8f),V9s)),ap(ap(ap(c_2Eiterate_2Esupport(A_27e,A_27b),V0op),V8f),V10t))))))))) & (( ! [V11f:$i] : (mem(V11f,arr(A_27f,A_27b)) => ( ! [V12s:$i] : (mem(V12s,arr(A_27f,bool)) => ( ! [V13t:$i] : (mem(V13t,arr(A_27f,bool)) => (ap(ap(ap(c_2Eiterate_2Esupport(A_27f,A_27b),V0op),V11f),ap(ap(c_2Epred__set_2EINTER(A_27f),V12s),V13t)) = ap(ap(c_2Epred__set_2EINTER(A_27f),ap(ap(ap(c_2Eiterate_2Esupport(A_27f,A_27b),V0op),V11f),V12s)),ap(ap(ap(c_2Eiterate_2Esupport(A_27f,A_27b),V0op),V11f),V13t))))))))) & (( ! [V14f:$i] : (mem(V14f,arr(A_27g,A_27b)) => ( ! [V15s:$i] : (mem(V15s,arr(A_27g,bool)) => ( ! [V16t:$i] : (mem(V16t,arr(A_27g,bool)) => (ap(ap(ap(c_2Eiterate_2Esupport(A_27g,A_27b),V0op),V14f),ap(ap(c_2Epred__set_2EDIFF(A_27g),V15s),V16t)) = ap(ap(c_2Epred__set_2EDIFF(A_27g),ap(ap(ap(c_2Eiterate_2Esupport(A_27g,A_27b),V0op),V14f),V15s)),ap(ap(ap(c_2Eiterate_2Esupport(A_27g,A_27b),V0op),V14f),V16t))))))))) & ( ! [V17f:$i] : (mem(V17f,arr(A_27h,A_27i)) => ( ! [V18g:$i] : (mem(V18g,arr(A_27i,A_27b)) => ( ! [V19s:$i] : (mem(V19s,arr(A_27h,bool)) => (ap(ap(ap(c_2Eiterate_2Esupport(A_27i,A_27b),V0op),V18g),ap(ap(c_2Epred__set_2EIMAGE(A_27h,A_27i),V17f),V19s)) = ap(ap(c_2Epred__set_2EIMAGE(A_27h,A_27i),V17f),ap(ap(ap(c_2Eiterate_2Esupport(A_27h,A_27b),V0op),ap(ap(c_2Ecombin_2Eo(A_27h,A_27b,A_27i),V18g),V17f)),V19s)))))))))))))))))))))))))))).
tff(conj_thm_2Eiterate_2ESUPPORT__DELTA,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0op:$i] : (mem(V0op,arr(A_27a,arr(A_27a,A_27a))) => ( ! [V1s:$i] : (mem(V1s,arr(A_27b,bool)) => ( ! [V2f:$i] : (mem(V2f,arr(A_27b,A_27a)) => ( ! [V3a:$i] : (mem(V3a,A_27b) => (ap(ap(ap(c_2Eiterate_2Esupport(A_27b,A_27a),V0op),f3288(A_27b,A_27a,V2f,V3a,V0op)),V1s) = ap(ap(ap(c_2Ebool_2ECOND(arr(A_27b,bool)),ap(ap(c_2Ebool_2EIN(A_27b),V3a),V1s)),ap(ap(ap(c_2Eiterate_2Esupport(A_27b,A_27a),V0op),V2f),ap(ap(c_2Epred__set_2EINSERT(A_27b),V3a),c_2Epred__set_2EEMPTY(A_27b)))),c_2Epred__set_2EEMPTY(A_27b))))))))))))))).
tff(conj_thm_2Eiterate_2EFINITE__SUPPORT__DELTA,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : (mem(V0s,arr(A_27b,bool)) => ( ! [V1op:$i] : (mem(V1op,arr(A_27a,arr(A_27a,A_27a))) => ( ! [V2f:$i] : (mem(V2f,arr(A_27b,A_27a)) => ( ! [V3a:$i] : (mem(V3a,A_27b) => p(ap(c_2Epred__set_2EFINITE(A_27b),ap(ap(ap(c_2Eiterate_2Esupport(A_27b,A_27a),V1op),f3289(A_27b,A_27a,V2f,V3a,V1op)),V0s))))))))))))))).
tff(conj_thm_2Eiterate_2EITERATE__SUPPORT,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0op:$i] : (mem(V0op,arr(A_27a,arr(A_27a,A_27a))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27b,A_27a)) => ( ! [V2s:$i] : (mem(V2s,arr(A_27b,bool)) => (ap(ap(ap(c_2Eiterate_2Eiterate(A_27b,A_27a),V0op),ap(ap(ap(c_2Eiterate_2Esupport(A_27b,A_27a),V0op),V1f),V2s)),V1f) = ap(ap(ap(c_2Eiterate_2Eiterate(A_27b,A_27a),V0op),V2s),V1f)))))))))))).
tff(conj_thm_2Eiterate_2EITERATE__EXPAND__CASES,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0op:$i] : (mem(V0op,arr(A_27a,arr(A_27a,A_27a))) => ( ! [V1f:$i] : (mem(V1f,arr(A_27b,A_27a)) => ( ! [V2s:$i] : (mem(V2s,arr(A_27b,bool)) => (ap(ap(ap(c_2Eiterate_2Eiterate(A_27b,A_27a),V0op),V2s),V1f) = ap(ap(ap(c_2Ebool_2ECOND(A_27a),ap(c_2Epred__set_2EFINITE(A_27b),ap(ap(ap(c_2Eiterate_2Esupport(A_27b,A_27a),V0op),V1f),V2s))),ap(ap(ap(c_2Eiterate_2Eiterate(A_27b,A_27a),V0op),ap(ap(ap(c_2Eiterate_2Esupport(A_27b,A_27a),V0op),V1f),V2s)),V1f)),ap(c_2Eiterate_2Eneutral(A_27a),V0op))))))))))))).
tff(conj_thm_2Eiterate_2EITERATE__CLAUSES__GEN,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0op:$i] : (mem(V0op,arr(A_27b,arr(A_27b,A_27b))) => (p(ap(c_2Eiterate_2Emonoidal(A_27b),V0op)) => (( ! [V1f:$i] : (mem(V1f,arr(A_27a,A_27b)) => (ap(ap(ap(c_2Eiterate_2Eiterate(A_27a,A_27b),V0op),c_2Epred__set_2EEMPTY(A_27a)),V1f) = ap(c_2Eiterate_2Eneutral(A_27b),V0op)))) & ( ! [V2f:$i] : (mem(V2f,arr(A_27a,A_27b)) => ( ! [V3x:$i] : (mem(V3x,A_27a) => ( ! [V4s:$i] : (mem(V4s,arr(A_27a,bool)) => ((p(ap(c_2Eiterate_2Emonoidal(A_27b),V0op)) & p(ap(c_2Epred__set_2EFINITE(A_27a),ap(ap(ap(c_2Eiterate_2Esupport(A_27a,A_27b),V0op),V2f),V4s)))) => (ap(ap(ap(c_2Eiterate_2Eiterate(A_27a,A_27b),V0op),ap(ap(c_2Epred__set_2EINSERT(A_27a),V3x),V4s)),V2f) = ap(ap(ap(c_2Ebool_2ECOND(A_27b),ap(ap(c_2Ebool_2EIN(A_27a),V3x),V4s)),ap(ap(ap(c_2Eiterate_2Eiterate(A_27a,A_27b),V0op),V4s),V2f)),ap(ap(V0op,ap(V2f,V3x)),ap(ap(ap(c_2Eiterate_2Eiterate(A_27a,A_27b),V0op),V4s),V2f))))))))))))))))))).
tff(conj_thm_2Eiterate_2EITERATE__CLAUSES,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0op:$i] : (mem(V0op,arr(A_27a,arr(A_27a,A_27a))) => (p(ap(c_2Eiterate_2Emonoidal(A_27a),V0op)) => (( ! [V1f:$i] : (mem(V1f,arr(A_27b,A_27a)) => (ap(ap(ap(c_2Eiterate_2Eiterate(A_27b,A_27a),V0op),c_2Epred__set_2EEMPTY(A_27b)),V1f) = ap(c_2Eiterate_2Eneutral(A_27a),V0op)))) & ( ! [V2f:$i] : (mem(V2f,arr(A_27b,A_27a)) => ( ! [V3x:$i] : (mem(V3x,A_27b) => ( ! [V4s:$i] : (mem(V4s,arr(A_27b,bool)) => (p(ap(c_2Epred__set_2EFINITE(A_27b),V4s)) => (ap(ap(ap(c_2Eiterate_2Eiterate(A_27b,A_27a),V0op),ap(ap(c_2Epred__set_2EINSERT(A_27b),V3x),V4s)),V2f) = ap(ap(ap(c_2Ebool_2ECOND(A_27a),ap(ap(c_2Ebool_2EIN(A_27b),V3x),V4s)),ap(ap(ap(c_2Eiterate_2Eiterate(A_27b,A_27a),V0op),V4s),V2f)),ap(ap(V0op,ap(V2f,V3x)),ap(ap(ap(c_2Eiterate_2Eiterate(A_27b,A_27a),V0op),V4s),V2f))))))))))))))))))).
tff(conj_thm_2Eiterate_2EITERATE__UNION,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0op:$i] : (mem(V0op,arr(A_27a,arr(A_27a,A_27a))) => (p(ap(c_2Eiterate_2Emonoidal(A_27a),V0op)) => ( ! [V1f:$i] : (mem(V1f,arr(A_27b,A_27a)) => ( ! [V2s:$i] : (mem(V2s,arr(A_27b,bool)) => ( ! [V3t:$i] : (mem(V3t,arr(A_27b,bool)) => ((p(ap(c_2Epred__set_2EFINITE(A_27b),V2s)) & (p(ap(c_2Epred__set_2EFINITE(A_27b),V3t)) & p(ap(ap(c_2Epred__set_2EDISJOINT(A_27b),V2s),V3t)))) => (ap(ap(ap(c_2Eiterate_2Eiterate(A_27b,A_27a),V0op),ap(ap(c_2Epred__set_2EUNION(A_27b),V2s),V3t)),V1f) = ap(ap(V0op,ap(ap(ap(c_2Eiterate_2Eiterate(A_27b,A_27a),V0op),V2s),V1f)),ap(ap(ap(c_2Eiterate_2Eiterate(A_27b,A_27a),V0op),V3t),V1f))))))))))))))))).
tff(conj_thm_2Eiterate_2EITERATE__UNION__GEN,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0op:$i] : (mem(V0op,arr(A_27b,arr(A_27b,A_27b))) => (p(ap(c_2Eiterate_2Emonoidal(A_27b),V0op)) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,A_27b)) => ( ! [V2s:$i] : (mem(V2s,arr(A_27a,bool)) => ( ! [V3t:$i] : (mem(V3t,arr(A_27a,bool)) => ((p(ap(c_2Epred__set_2EFINITE(A_27a),ap(ap(ap(c_2Eiterate_2Esupport(A_27a,A_27b),V0op),V1f),V2s))) & (p(ap(c_2Epred__set_2EFINITE(A_27a),ap(ap(ap(c_2Eiterate_2Esupport(A_27a,A_27b),V0op),V1f),V3t))) & p(ap(ap(c_2Epred__set_2EDISJOINT(A_27a),ap(ap(ap(c_2Eiterate_2Esupport(A_27a,A_27b),V0op),V1f),V2s)),ap(ap(ap(c_2Eiterate_2Esupport(A_27a,A_27b),V0op),V1f),V3t))))) => (ap(ap(ap(c_2Eiterate_2Eiterate(A_27a,A_27b),V0op),ap(ap(c_2Epred__set_2EUNION(A_27a),V2s),V3t)),V1f) = ap(ap(V0op,ap(ap(ap(c_2Eiterate_2Eiterate(A_27a,A_27b),V0op),V2s),V1f)),ap(ap(ap(c_2Eiterate_2Eiterate(A_27a,A_27b),V0op),V3t),V1f))))))))))))))))).
tff(conj_thm_2Eiterate_2EITERATE__DIFF,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0op:$i] : (mem(V0op,arr(A_27a,arr(A_27a,A_27a))) => (p(ap(c_2Eiterate_2Emonoidal(A_27a),V0op)) => ( ! [V1f:$i] : (mem(V1f,arr(A_27b,A_27a)) => ( ! [V2s:$i] : (mem(V2s,arr(A_27b,bool)) => ( ! [V3t:$i] : (mem(V3t,arr(A_27b,bool)) => ((p(ap(c_2Epred__set_2EFINITE(A_27b),V2s)) & p(ap(ap(c_2Epred__set_2ESUBSET(A_27b),V3t),V2s))) => (ap(ap(V0op,ap(ap(ap(c_2Eiterate_2Eiterate(A_27b,A_27a),V0op),ap(ap(c_2Epred__set_2EDIFF(A_27b),V2s),V3t)),V1f)),ap(ap(ap(c_2Eiterate_2Eiterate(A_27b,A_27a),V0op),V3t),V1f)) = ap(ap(ap(c_2Eiterate_2Eiterate(A_27b,A_27a),V0op),V2s),V1f)))))))))))))))).
tff(conj_thm_2Eiterate_2EITERATE__DIFF__GEN,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0op:$i] : (mem(V0op,arr(A_27b,arr(A_27b,A_27b))) => (p(ap(c_2Eiterate_2Emonoidal(A_27b),V0op)) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,A_27b)) => ( ! [V2s:$i] : (mem(V2s,arr(A_27a,bool)) => ( ! [V3t:$i] : (mem(V3t,arr(A_27a,bool)) => ((p(ap(c_2Epred__set_2EFINITE(A_27a),ap(ap(ap(c_2Eiterate_2Esupport(A_27a,A_27b),V0op),V1f),V2s))) & p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(ap(ap(c_2Eiterate_2Esupport(A_27a,A_27b),V0op),V1f),V3t)),ap(ap(ap(c_2Eiterate_2Esupport(A_27a,A_27b),V0op),V1f),V2s)))) => (ap(ap(V0op,ap(ap(ap(c_2Eiterate_2Eiterate(A_27a,A_27b),V0op),ap(ap(c_2Epred__set_2EDIFF(A_27a),V2s),V3t)),V1f)),ap(ap(ap(c_2Eiterate_2Eiterate(A_27a,A_27b),V0op),V3t),V1f)) = ap(ap(ap(c_2Eiterate_2Eiterate(A_27a,A_27b),V0op),V2s),V1f)))))))))))))))).
tff(conj_thm_2Eiterate_2EITERATE__INCL__EXCL,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0op:$i] : (mem(V0op,arr(A_27a,arr(A_27a,A_27a))) => (p(ap(c_2Eiterate_2Emonoidal(A_27a),V0op)) => ( ! [V1s:$i] : (mem(V1s,arr(A_27b,bool)) => ( ! [V2t:$i] : (mem(V2t,arr(A_27b,bool)) => ( ! [V3f:$i] : (mem(V3f,arr(A_27b,A_27a)) => ((p(ap(c_2Epred__set_2EFINITE(A_27b),V1s)) & p(ap(c_2Epred__set_2EFINITE(A_27b),V2t))) => (ap(ap(V0op,ap(ap(ap(c_2Eiterate_2Eiterate(A_27b,A_27a),V0op),V1s),V3f)),ap(ap(ap(c_2Eiterate_2Eiterate(A_27b,A_27a),V0op),V2t),V3f)) = ap(ap(V0op,ap(ap(ap(c_2Eiterate_2Eiterate(A_27b,A_27a),V0op),ap(ap(c_2Epred__set_2EUNION(A_27b),V1s),V2t)),V3f)),ap(ap(ap(c_2Eiterate_2Eiterate(A_27b,A_27a),V0op),ap(ap(c_2Epred__set_2EINTER(A_27b),V1s),V2t)),V3f))))))))))))))))).
tff(conj_thm_2Eiterate_2EITERATE__CLOSED,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0op:$i] : (mem(V0op,arr(A_27b,arr(A_27b,A_27b))) => (p(ap(c_2Eiterate_2Emonoidal(A_27b),V0op)) => ( ! [V1P:$i] : (mem(V1P,arr(A_27b,bool)) => ((p(ap(V1P,ap(c_2Eiterate_2Eneutral(A_27b),V0op))) & ( ! [V2x:$i] : (mem(V2x,A_27b) => ( ! [V3y:$i] : (mem(V3y,A_27b) => ((p(ap(V1P,V2x)) & p(ap(V1P,V3y))) => p(ap(V1P,ap(ap(V0op,V2x),V3y))))))))) => ( ! [V4f:$i] : (mem(V4f,arr(A_27a,A_27b)) => ( ! [V5s:$i] : (mem(V5s,arr(A_27a,bool)) => (( ! [V6x:$i] : (mem(V6x,A_27a) => ((p(ap(ap(c_2Ebool_2EIN(A_27a),V6x),V5s)) & (~~ (ap(V4f,V6x) = ap(c_2Eiterate_2Eneutral(A_27b),V0op)))) => p(ap(V1P,ap(V4f,V6x)))))) => p(ap(V1P,ap(ap(ap(c_2Eiterate_2Eiterate(A_27a,A_27b),V0op),V5s),V4f)))))))))))))))))).
tff(conj_thm_2Eiterate_2EITERATE__RELATED,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0op:$i] : (mem(V0op,arr(A_27b,arr(A_27b,A_27b))) => (p(ap(c_2Eiterate_2Emonoidal(A_27b),V0op)) => ( ! [V1R:$i] : (mem(V1R,arr(A_27b,arr(A_27b,bool))) => ((p(ap(ap(V1R,ap(c_2Eiterate_2Eneutral(A_27b),V0op)),ap(c_2Eiterate_2Eneutral(A_27b),V0op))) & ( ! [V2x1:$i] : (mem(V2x1,A_27b) => ( ! [V3y1:$i] : (mem(V3y1,A_27b) => ( ! [V4x2:$i] : (mem(V4x2,A_27b) => ( ! [V5y2:$i] : (mem(V5y2,A_27b) => ((p(ap(ap(V1R,V2x1),V4x2)) & p(ap(ap(V1R,V3y1),V5y2))) => p(ap(ap(V1R,ap(ap(V0op,V2x1),V3y1)),ap(ap(V0op,V4x2),V5y2))))))))))))) => ( ! [V6f:$i] : (mem(V6f,arr(A_27a,A_27b)) => ( ! [V7g:$i] : (mem(V7g,arr(A_27a,A_27b)) => ( ! [V8s:$i] : (mem(V8s,arr(A_27a,bool)) => ((p(ap(c_2Epred__set_2EFINITE(A_27a),V8s)) & ( ! [V9x:$i] : (mem(V9x,A_27a) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V9x),V8s)) => p(ap(ap(V1R,ap(V6f,V9x)),ap(V7g,V9x))))))) => p(ap(ap(V1R,ap(ap(ap(c_2Eiterate_2Eiterate(A_27a,A_27b),V0op),V8s),V6f)),ap(ap(ap(c_2Eiterate_2Eiterate(A_27a,A_27b),V0op),V8s),V7g)))))))))))))))))))).
tff(conj_thm_2Eiterate_2EITERATE__EQ__NEUTRAL,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0op:$i] : (mem(V0op,arr(A_27b,arr(A_27b,A_27b))) => (p(ap(c_2Eiterate_2Emonoidal(A_27b),V0op)) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,A_27b)) => ( ! [V2s:$i] : (mem(V2s,arr(A_27a,bool)) => (( ! [V3x:$i] : (mem(V3x,A_27a) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V3x),V2s)) => (ap(V1f,V3x) = ap(c_2Eiterate_2Eneutral(A_27b),V0op))))) => (ap(ap(ap(c_2Eiterate_2Eiterate(A_27a,A_27b),V0op),V2s),V1f) = ap(c_2Eiterate_2Eneutral(A_27b),V0op)))))))))))))).
tff(conj_thm_2Eiterate_2EITERATE__SING,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0op:$i] : (mem(V0op,arr(A_27b,arr(A_27b,A_27b))) => (p(ap(c_2Eiterate_2Emonoidal(A_27b),V0op)) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,A_27b)) => ( ! [V2x:$i] : (mem(V2x,A_27a) => (ap(ap(ap(c_2Eiterate_2Eiterate(A_27a,A_27b),V0op),ap(ap(c_2Epred__set_2EINSERT(A_27a),V2x),c_2Epred__set_2EEMPTY(A_27a))),V1f) = ap(V1f,V2x))))))))))))).
tff(conj_thm_2Eiterate_2EITERATE__DELETE,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0op:$i] : (mem(V0op,arr(A_27b,arr(A_27b,A_27b))) => (p(ap(c_2Eiterate_2Emonoidal(A_27b),V0op)) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,A_27b)) => ( ! [V2s:$i] : (mem(V2s,arr(A_27a,bool)) => ( ! [V3a:$i] : (mem(V3a,A_27a) => ((p(ap(c_2Epred__set_2EFINITE(A_27a),V2s)) & p(ap(ap(c_2Ebool_2EIN(A_27a),V3a),V2s))) => (ap(ap(V0op,ap(V1f,V3a)),ap(ap(ap(c_2Eiterate_2Eiterate(A_27a,A_27b),V0op),ap(ap(c_2Epred__set_2EDELETE(A_27a),V2s),V3a)),V1f)) = ap(ap(ap(c_2Eiterate_2Eiterate(A_27a,A_27b),V0op),V2s),V1f)))))))))))))))).
tff(conj_thm_2Eiterate_2EITERATE__DELTA,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0op:$i] : (mem(V0op,arr(A_27a,arr(A_27a,A_27a))) => (p(ap(c_2Eiterate_2Emonoidal(A_27a),V0op)) => ( ! [V1f:$i] : (mem(V1f,arr(A_27b,A_27a)) => ( ! [V2a:$i] : (mem(V2a,A_27b) => ( ! [V3s:$i] : (mem(V3s,arr(A_27b,bool)) => (ap(ap(ap(c_2Eiterate_2Eiterate(A_27b,A_27a),V0op),V3s),f3290(A_27b,A_27a,V1f,V2a,V0op)) = ap(ap(ap(c_2Ebool_2ECOND(A_27a),ap(ap(c_2Ebool_2EIN(A_27b),V2a),V3s)),ap(V1f,V2a)),ap(c_2Eiterate_2Eneutral(A_27a),V0op)))))))))))))))).
tff(conj_thm_2Eiterate_2EITERATE__IMAGE,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0op:$i] : (mem(V0op,arr(A_27c,arr(A_27c,A_27c))) => (p(ap(c_2Eiterate_2Emonoidal(A_27c),V0op)) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,A_27b)) => ( ! [V2g:$i] : (mem(V2g,arr(A_27b,A_27c)) => ( ! [V3s:$i] : (mem(V3s,arr(A_27a,bool)) => (( ! [V4x:$i] : (mem(V4x,A_27a) => ( ! [V5y:$i] : (mem(V5y,A_27a) => ((p(ap(ap(c_2Ebool_2EIN(A_27a),V4x),V3s)) & (p(ap(ap(c_2Ebool_2EIN(A_27a),V5y),V3s)) & (ap(V1f,V4x) = ap(V1f,V5y)))) => (V4x = V5y)))))) => (ap(ap(ap(c_2Eiterate_2Eiterate(A_27b,A_27c),V0op),ap(ap(c_2Epred__set_2EIMAGE(A_27a,A_27b),V1f),V3s)),V2g) = ap(ap(ap(c_2Eiterate_2Eiterate(A_27a,A_27c),V0op),V3s),ap(ap(c_2Ecombin_2Eo(A_27a,A_27c,A_27b),V2g),V1f)))))))))))))))))).
tff(conj_thm_2Eiterate_2EITERATE__BIJECTION,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0op:$i] : (mem(V0op,arr(A_27b,arr(A_27b,A_27b))) => (p(ap(c_2Eiterate_2Emonoidal(A_27b),V0op)) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,A_27b)) => ( ! [V2p:$i] : (mem(V2p,arr(A_27a,A_27a)) => ( ! [V3s:$i] : (mem(V3s,arr(A_27a,bool)) => ((( ! [V4x:$i] : (mem(V4x,A_27a) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V4x),V3s)) => p(ap(ap(c_2Ebool_2EIN(A_27a),ap(V2p,V4x)),V3s))))) & ( ! [V5y:$i] : (mem(V5y,A_27a) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V5y),V3s)) => p(ap(c_2Ebool_2E_3F_21(A_27a),f3291(A_27a,V5y,V2p,V3s))))))) => (ap(ap(ap(c_2Eiterate_2Eiterate(A_27a,A_27b),V0op),V3s),V1f) = ap(ap(ap(c_2Eiterate_2Eiterate(A_27a,A_27b),V0op),V3s),ap(ap(c_2Ecombin_2Eo(A_27a,A_27b,A_27a),V1f),V2p))))))))))))))))).
tff(conj_thm_2Eiterate_2EITERATE__ITERATE__PRODUCT,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0op:$i] : (mem(V0op,arr(A_27c,arr(A_27c,A_27c))) => (p(ap(c_2Eiterate_2Emonoidal(A_27c),V0op)) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => ( ! [V2t:$i] : (mem(V2t,arr(A_27a,arr(A_27b,bool))) => ( ! [V3x:$i] : (mem(V3x,arr(A_27a,arr(A_27b,A_27c))) => ((p(ap(c_2Epred__set_2EFINITE(A_27a),V1s)) & ( ! [V4i:$i] : (mem(V4i,A_27a) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V4i),V1s)) => p(ap(c_2Epred__set_2EFINITE(A_27b),ap(V2t,V4i))))))) => (ap(ap(ap(c_2Eiterate_2Eiterate(A_27a,A_27c),V0op),V1s),f3292(A_27b,A_27c,A_27a,V0op,V2t,V3x)) = ap(ap(ap(c_2Eiterate_2Eiterate(ty_2Epair_2Eprod(A_27a,A_27b),A_27c),V0op),ap(c_2Epred__set_2EGSPEC(ty_2Epair_2Eprod(A_27a,A_27b),ty_2Epair_2Eprod(A_27a,A_27b)),ap(c_2Epair_2EUNCURRY(A_27a,A_27b,ty_2Epair_2Eprod(ty_2Epair_2Eprod(A_27a,A_27b),bool)),f3294(A_27b,A_27a,V1s,V2t)))),ap(c_2Epair_2EUNCURRY(A_27a,A_27b,A_27c),f3296(A_27a,A_27c,A_27b,V3x))))))))))))))))))).
tff(conj_thm_2Eiterate_2EITERATE__EQ,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0op:$i] : (mem(V0op,arr(A_27b,arr(A_27b,A_27b))) => (p(ap(c_2Eiterate_2Emonoidal(A_27b),V0op)) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,A_27b)) => ( ! [V2g:$i] : (mem(V2g,arr(A_27a,A_27b)) => ( ! [V3s:$i] : (mem(V3s,arr(A_27a,bool)) => (( ! [V4x:$i] : (mem(V4x,A_27a) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V4x),V3s)) => (ap(V1f,V4x) = ap(V2g,V4x))))) => (ap(ap(ap(c_2Eiterate_2Eiterate(A_27a,A_27b),V0op),V3s),V1f) = ap(ap(ap(c_2Eiterate_2Eiterate(A_27a,A_27b),V0op),V3s),V2g)))))))))))))))).
tff(conj_thm_2Eiterate_2EITERATE__EQ__GENERAL,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0op:$i] : (mem(V0op,arr(A_27c,arr(A_27c,A_27c))) => (p(ap(c_2Eiterate_2Emonoidal(A_27c),V0op)) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => ( ! [V2t:$i] : (mem(V2t,arr(A_27b,bool)) => ( ! [V3f:$i] : (mem(V3f,arr(A_27a,A_27c)) => ( ! [V4g:$i] : (mem(V4g,arr(A_27b,A_27c)) => ( ! [V5h:$i] : (mem(V5h,arr(A_27a,A_27b)) => ((( ! [V6y:$i] : (mem(V6y,A_27b) => (p(ap(ap(c_2Ebool_2EIN(A_27b),V6y),V2t)) => p(ap(c_2Ebool_2E_3F_21(A_27a),f3297(A_27b,A_27a,V6y,V5h,V1s)))))) & ( ! [V8x:$i] : (mem(V8x,A_27a) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V8x),V1s)) => (p(ap(ap(c_2Ebool_2EIN(A_27b),ap(V5h,V8x)),V2t)) & (ap(V4g,ap(V5h,V8x)) = ap(V3f,V8x))))))) => (ap(ap(ap(c_2Eiterate_2Eiterate(A_27a,A_27c),V0op),V1s),V3f) = ap(ap(ap(c_2Eiterate_2Eiterate(A_27b,A_27c),V0op),V2t),V4g))))))))))))))))))))).
tff(conj_thm_2Eiterate_2EITERATE__EQ__GENERAL__INVERSES,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0op:$i] : (mem(V0op,arr(A_27c,arr(A_27c,A_27c))) => (p(ap(c_2Eiterate_2Emonoidal(A_27c),V0op)) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => ( ! [V2t:$i] : (mem(V2t,arr(A_27b,bool)) => ( ! [V3f:$i] : (mem(V3f,arr(A_27a,A_27c)) => ( ! [V4g:$i] : (mem(V4g,arr(A_27b,A_27c)) => ( ! [V5h:$i] : (mem(V5h,arr(A_27a,A_27b)) => ( ! [V6k:$i] : (mem(V6k,arr(A_27b,A_27a)) => ((( ! [V7y:$i] : (mem(V7y,A_27b) => (p(ap(ap(c_2Ebool_2EIN(A_27b),V7y),V2t)) => (p(ap(ap(c_2Ebool_2EIN(A_27a),ap(V6k,V7y)),V1s)) & (ap(V5h,ap(V6k,V7y)) = V7y))))) & ( ! [V8x:$i] : (mem(V8x,A_27a) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V8x),V1s)) => (p(ap(ap(c_2Ebool_2EIN(A_27b),ap(V5h,V8x)),V2t)) & ((ap(V6k,ap(V5h,V8x)) = V8x) & (ap(V4g,ap(V5h,V8x)) = ap(V3f,V8x)))))))) => (ap(ap(ap(c_2Eiterate_2Eiterate(A_27a,A_27c),V0op),V1s),V3f) = ap(ap(ap(c_2Eiterate_2Eiterate(A_27b,A_27c),V0op),V2t),V4g))))))))))))))))))))))).
tff(conj_thm_2Eiterate_2EITERATE__INJECTION,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0op:$i] : (mem(V0op,arr(A_27b,arr(A_27b,A_27b))) => (p(ap(c_2Eiterate_2Emonoidal(A_27b),V0op)) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,A_27b)) => ( ! [V2p:$i] : (mem(V2p,arr(A_27a,A_27a)) => ( ! [V3s:$i] : (mem(V3s,arr(A_27a,bool)) => ((p(ap(c_2Epred__set_2EFINITE(A_27a),V3s)) & (( ! [V4x:$i] : (mem(V4x,A_27a) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V4x),V3s)) => p(ap(ap(c_2Ebool_2EIN(A_27a),ap(V2p,V4x)),V3s))))) & ( ! [V5x:$i] : (mem(V5x,A_27a) => ( ! [V6y:$i] : (mem(V6y,A_27a) => ((p(ap(ap(c_2Ebool_2EIN(A_27a),V5x),V3s)) & (p(ap(ap(c_2Ebool_2EIN(A_27a),V6y),V3s)) & (ap(V2p,V5x) = ap(V2p,V6y)))) => (V5x = V6y)))))))) => (ap(ap(ap(c_2Eiterate_2Eiterate(A_27a,A_27b),V0op),V3s),ap(ap(c_2Ecombin_2Eo(A_27a,A_27b,A_27a),V1f),V2p)) = ap(ap(ap(c_2Eiterate_2Eiterate(A_27a,A_27b),V0op),V3s),V1f)))))))))))))))).
tff(conj_thm_2Eiterate_2EITERATE__UNION__NONZERO,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0op:$i] : (mem(V0op,arr(A_27b,arr(A_27b,A_27b))) => (p(ap(c_2Eiterate_2Emonoidal(A_27b),V0op)) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,A_27b)) => ( ! [V2s:$i] : (mem(V2s,arr(A_27a,bool)) => ( ! [V3t:$i] : (mem(V3t,arr(A_27a,bool)) => ((p(ap(c_2Epred__set_2EFINITE(A_27a),V2s)) & (p(ap(c_2Epred__set_2EFINITE(A_27a),V3t)) & ( ! [V4x:$i] : (mem(V4x,A_27a) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V4x),ap(ap(c_2Epred__set_2EINTER(A_27a),V2s),V3t))) => (ap(V1f,V4x) = ap(c_2Eiterate_2Eneutral(A_27b),V0op))))))) => (ap(ap(ap(c_2Eiterate_2Eiterate(A_27a,A_27b),V0op),ap(ap(c_2Epred__set_2EUNION(A_27a),V2s),V3t)),V1f) = ap(ap(V0op,ap(ap(ap(c_2Eiterate_2Eiterate(A_27a,A_27b),V0op),V2s),V1f)),ap(ap(ap(c_2Eiterate_2Eiterate(A_27a,A_27b),V0op),V3t),V1f))))))))))))))))).
tff(conj_thm_2Eiterate_2EITERATE__OP,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0op:$i] : (mem(V0op,arr(A_27a,arr(A_27a,A_27a))) => (p(ap(c_2Eiterate_2Emonoidal(A_27a),V0op)) => ( ! [V1f:$i] : (mem(V1f,arr(A_27b,A_27a)) => ( ! [V2g:$i] : (mem(V2g,arr(A_27b,A_27a)) => ( ! [V3s:$i] : (mem(V3s,arr(A_27b,bool)) => (p(ap(c_2Epred__set_2EFINITE(A_27b),V3s)) => (ap(ap(ap(c_2Eiterate_2Eiterate(A_27b,A_27a),V0op),V3s),f3298(A_27a,A_27b,V0op,V1f,V2g)) = ap(ap(V0op,ap(ap(ap(c_2Eiterate_2Eiterate(A_27b,A_27a),V0op),V3s),V1f)),ap(ap(ap(c_2Eiterate_2Eiterate(A_27b,A_27a),V0op),V3s),V2g))))))))))))))))).
tff(conj_thm_2Eiterate_2EITERATE__SUPERSET,conjecture,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0op:$i] : (mem(V0op,arr(A_27b,arr(A_27b,A_27b))) => (p(ap(c_2Eiterate_2Emonoidal(A_27b),V0op)) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,A_27b)) => ( ! [V2u:$i] : (mem(V2u,arr(A_27a,bool)) => ( ! [V3v:$i] : (mem(V3v,arr(A_27a,bool)) => ((p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),V2u),V3v)) & ( ! [V4x:$i] : (mem(V4x,A_27a) => ((p(ap(ap(c_2Ebool_2EIN(A_27a),V4x),V3v)) & (~~ p(ap(ap(c_2Ebool_2EIN(A_27a),V4x),V2u)))) => (ap(V1f,V4x) = ap(c_2Eiterate_2Eneutral(A_27b),V0op)))))) => (ap(ap(ap(c_2Eiterate_2Eiterate(A_27a,A_27b),V0op),V3v),V1f) = ap(ap(ap(c_2Eiterate_2Eiterate(A_27a,A_27b),V0op),V2u),V1f)))))))))))))))).
