include('Axioms/HL4001_2.ax').
tff(stp_o,type,(tp__o : $tType)).
tff(stp_inj_o,type,(inj__o : tp__o > $i)).
tff(stp_surj_o,type,(surj__o : $i > tp__o)).
tff(stp_inj_surj_o,axiom,( ! [X:tp__o] : (surj__o(inj__o(X)) = X))).
tff(stp_inj_mem_o,axiom,( ! [X:tp__o] : (mem(inj__o(X),bool)))).
tff(stp_iso_mem_o,axiom,( ! [X:$i] : (mem(X,bool) => (X = inj__o(surj__o(X)))))).
tff(tp_c_2Emin_2E_40,type,(c_2Emin_2E_40:del > $i)).
tff(mem_c_2Emin_2E_40,axiom,( ! [A_27a:del] : mem(c_2Emin_2E_40(A_27a),arr(arr(A_27a,bool),A_27a)))).
tff(tp_c_2Ecombin_2EK,type,(c_2Ecombin_2EK:(del * del) > $i)).
tff(mem_c_2Ecombin_2EK,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Ecombin_2EK(A_27a,A_27b),arr(A_27a,arr(A_27b,A_27a)))))).
tff(tp_c_2Ecombin_2ES,type,(c_2Ecombin_2ES:(del * del * del) > $i)).
tff(mem_c_2Ecombin_2ES,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27c:del] : mem(c_2Ecombin_2ES(A_27a,A_27b,A_27c),arr(arr(A_27a,arr(A_27b,A_27c)),arr(arr(A_27a,A_27b),arr(A_27a,A_27c)))))))).
tff(tp_c_2Ecombin_2EC,type,(c_2Ecombin_2EC:(del * del * del) > $i)).
tff(mem_c_2Ecombin_2EC,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27c:del] : mem(c_2Ecombin_2EC(A_27a,A_27b,A_27c),arr(arr(A_27a,arr(A_27b,A_27c)),arr(A_27b,arr(A_27a,A_27c)))))))).
tff(tp_c_2Ecombin_2EI,type,(c_2Ecombin_2EI:del > $i)).
tff(mem_c_2Ecombin_2EI,axiom,( ! [A_27a:del] : mem(c_2Ecombin_2EI(A_27a),arr(A_27a,A_27a)))).
tff(tp_c_2Ecombin_2Eo,type,(c_2Ecombin_2Eo:(del * del * del) > $i)).
tff(mem_c_2Ecombin_2Eo,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27c:del] : mem(c_2Ecombin_2Eo(A_27a,A_27b,A_27c),arr(arr(A_27c,A_27b),arr(arr(A_27a,A_27c),arr(A_27a,A_27b)))))))).
tff(tp_ty_2Eextreal_2Eextreal,type,( ty_2Eextreal_2Eextreal: del )).
tff(stp_ty_2Eextreal_2Eextreal,type,(tp__ty_2Eextreal_2Eextreal : $tType)).
tff(stp_inj_ty_2Eextreal_2Eextreal,type,(inj__ty_2Eextreal_2Eextreal : tp__ty_2Eextreal_2Eextreal > $i)).
tff(stp_surj_ty_2Eextreal_2Eextreal,type,(surj__ty_2Eextreal_2Eextreal : $i > tp__ty_2Eextreal_2Eextreal)).
tff(stp_inj_surj_ty_2Eextreal_2Eextreal,axiom,( ! [X:tp__ty_2Eextreal_2Eextreal] : (surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(X)) = X))).
tff(stp_inj_mem_ty_2Eextreal_2Eextreal,axiom,( ! [X:tp__ty_2Eextreal_2Eextreal] : (mem(inj__ty_2Eextreal_2Eextreal(X),ty_2Eextreal_2Eextreal)))).
tff(stp_iso_mem_ty_2Eextreal_2Eextreal,axiom,( ! [X:$i] : (mem(X,ty_2Eextreal_2Eextreal) => (X = inj__ty_2Eextreal_2Eextreal(surj__ty_2Eextreal_2Eextreal(X)))))).
tff(tp_ty_2Erealax_2Ereal,type,( ty_2Erealax_2Ereal: del )).
tff(stp_ty_2Erealax_2Ereal,type,(tp__ty_2Erealax_2Ereal : $tType)).
tff(stp_inj_ty_2Erealax_2Ereal,type,(inj__ty_2Erealax_2Ereal : tp__ty_2Erealax_2Ereal > $i)).
tff(stp_surj_ty_2Erealax_2Ereal,type,(surj__ty_2Erealax_2Ereal : $i > tp__ty_2Erealax_2Ereal)).
tff(stp_inj_surj_ty_2Erealax_2Ereal,axiom,( ! [X:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(inj__ty_2Erealax_2Ereal(X)) = X))).
tff(stp_inj_mem_ty_2Erealax_2Ereal,axiom,( ! [X:tp__ty_2Erealax_2Ereal] : (mem(inj__ty_2Erealax_2Ereal(X),ty_2Erealax_2Ereal)))).
tff(stp_iso_mem_ty_2Erealax_2Ereal,axiom,( ! [X:$i] : (mem(X,ty_2Erealax_2Ereal) => (X = inj__ty_2Erealax_2Ereal(surj__ty_2Erealax_2Ereal(X)))))).
tff(tp_c_2Eextreal_2ENormal,type,(c_2Eextreal_2ENormal:$i)).
tff(mem_c_2Eextreal_2ENormal,axiom,mem(c_2Eextreal_2ENormal,arr(ty_2Erealax_2Ereal,ty_2Eextreal_2Eextreal))).
tff(stp_fo_c_2Eextreal_2ENormal,type,(fo__c_2Eextreal_2ENormal:(tp__ty_2Erealax_2Ereal) > tp__ty_2Eextreal_2Eextreal)).
tff(stp_eq_fo_c_2Eextreal_2ENormal,axiom,( ! [X0:tp__ty_2Erealax_2Ereal] : (inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2ENormal(X0)) = ap(c_2Eextreal_2ENormal,inj__ty_2Erealax_2Ereal(X0))))).
tff(tp_c_2Eextreal_2Eextreal__add,type,(c_2Eextreal_2Eextreal__add:$i)).
tff(mem_c_2Eextreal_2Eextreal__add,axiom,mem(c_2Eextreal_2Eextreal__add,arr(ty_2Eextreal_2Eextreal,arr(ty_2Eextreal_2Eextreal,ty_2Eextreal_2Eextreal)))).
tff(stp_fo_c_2Eextreal_2Eextreal__add,type,(fo__c_2Eextreal_2Eextreal__add:(tp__ty_2Eextreal_2Eextreal * tp__ty_2Eextreal_2Eextreal) > tp__ty_2Eextreal_2Eextreal)).
tff(stp_eq_fo_c_2Eextreal_2Eextreal__add,axiom,( ! [X0:tp__ty_2Eextreal_2Eextreal] : ( ! [X1:tp__ty_2Eextreal_2Eextreal] : (inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__add(X0,X1)) = ap(ap(c_2Eextreal_2Eextreal__add,inj__ty_2Eextreal_2Eextreal(X0)),inj__ty_2Eextreal_2Eextreal(X1)))))).
tff(tp_ty_2Enum_2Enum,type,( ty_2Enum_2Enum: del )).
tff(stp_ty_2Enum_2Enum,type,(tp__ty_2Enum_2Enum : $tType)).
tff(stp_inj_ty_2Enum_2Enum,type,(inj__ty_2Enum_2Enum : tp__ty_2Enum_2Enum > $i)).
tff(stp_surj_ty_2Enum_2Enum,type,(surj__ty_2Enum_2Enum : $i > tp__ty_2Enum_2Enum)).
tff(stp_inj_surj_ty_2Enum_2Enum,axiom,( ! [X:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(inj__ty_2Enum_2Enum(X)) = X))).
tff(stp_inj_mem_ty_2Enum_2Enum,axiom,( ! [X:tp__ty_2Enum_2Enum] : (mem(inj__ty_2Enum_2Enum(X),ty_2Enum_2Enum)))).
tff(stp_iso_mem_ty_2Enum_2Enum,axiom,( ! [X:$i] : (mem(X,ty_2Enum_2Enum) => (X = inj__ty_2Enum_2Enum(surj__ty_2Enum_2Enum(X)))))).
tff(tp_c_2Eextreal_2Eextreal__of__num,type,(c_2Eextreal_2Eextreal__of__num:$i)).
tff(mem_c_2Eextreal_2Eextreal__of__num,axiom,mem(c_2Eextreal_2Eextreal__of__num,arr(ty_2Enum_2Enum,ty_2Eextreal_2Eextreal))).
tff(stp_fo_c_2Eextreal_2Eextreal__of__num,type,(fo__c_2Eextreal_2Eextreal__of__num:(tp__ty_2Enum_2Enum) > tp__ty_2Eextreal_2Eextreal)).
tff(stp_eq_fo_c_2Eextreal_2Eextreal__of__num,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__of__num(X0)) = ap(c_2Eextreal_2Eextreal__of__num,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Eextreal_2Eextreal__le,type,(c_2Eextreal_2Eextreal__le:$i)).
tff(mem_c_2Eextreal_2Eextreal__le,axiom,mem(c_2Eextreal_2Eextreal__le,arr(ty_2Eextreal_2Eextreal,arr(ty_2Eextreal_2Eextreal,bool)))).
tff(stp_fo_c_2Eextreal_2Eextreal__le,type,(fo__c_2Eextreal_2Eextreal__le:(tp__ty_2Eextreal_2Eextreal * tp__ty_2Eextreal_2Eextreal) > tp__o)).
tff(stp_eq_fo_c_2Eextreal_2Eextreal__le,axiom,( ! [X0:tp__ty_2Eextreal_2Eextreal] : ( ! [X1:tp__ty_2Eextreal_2Eextreal] : (inj__o(fo__c_2Eextreal_2Eextreal__le(X0,X1)) = ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0)),inj__ty_2Eextreal_2Eextreal(X1)))))).
tff(tp_c_2Eextreal_2EPosInf,type,(c_2Eextreal_2EPosInf:$i)).
tff(mem_c_2Eextreal_2EPosInf,axiom,mem(c_2Eextreal_2EPosInf,ty_2Eextreal_2Eextreal)).
tff(stp_fo_c_2Eextreal_2EPosInf,type,(fo__c_2Eextreal_2EPosInf:tp__ty_2Eextreal_2Eextreal)).
tff(stp_eq_fo_c_2Eextreal_2EPosInf,axiom,(inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2EPosInf) = c_2Eextreal_2EPosInf)).
tff(tp_c_2Epred__set_2EUNION,type,(c_2Epred__set_2EUNION:del > $i)).
tff(mem_c_2Epred__set_2EUNION,axiom,( ! [A_27a:del] : mem(c_2Epred__set_2EUNION(A_27a),arr(arr(A_27a,bool),arr(arr(A_27a,bool),arr(A_27a,bool)))))).
tff(tp_c_2Epred__set_2ESUBSET,type,(c_2Epred__set_2ESUBSET:del > $i)).
tff(mem_c_2Epred__set_2ESUBSET,axiom,( ! [A_27a:del] : mem(c_2Epred__set_2ESUBSET(A_27a),arr(arr(A_27a,bool),arr(arr(A_27a,bool),bool))))).
tff(tp_c_2Epred__set_2Ecountable,type,(c_2Epred__set_2Ecountable:del > $i)).
tff(mem_c_2Epred__set_2Ecountable,axiom,( ! [A_27a:del] : mem(c_2Epred__set_2Ecountable(A_27a),arr(arr(A_27a,bool),bool)))).
tff(tp_ty_2Epair_2Eprod,type,( ty_2Epair_2Eprod: ( del * del ) > del )).
tff(tp_c_2Emeasure_2Ealgebra,type,(c_2Emeasure_2Ealgebra:del > $i)).
tff(mem_c_2Emeasure_2Ealgebra,axiom,( ! [A_27a:del] : mem(c_2Emeasure_2Ealgebra(A_27a),arr(ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),bool)))).
tff(tp_c_2Emeasure_2Esubset__class,type,(c_2Emeasure_2Esubset__class:del > $i)).
tff(mem_c_2Emeasure_2Esubset__class,axiom,( ! [A_27a:del] : mem(c_2Emeasure_2Esubset__class(A_27a),arr(arr(A_27a,bool),arr(arr(arr(A_27a,bool),bool),bool))))).
tff(tp_c_2Eextreal_2Eextreal__lt,type,(c_2Eextreal_2Eextreal__lt:$i)).
tff(mem_c_2Eextreal_2Eextreal__lt,axiom,mem(c_2Eextreal_2Eextreal__lt,arr(ty_2Eextreal_2Eextreal,arr(ty_2Eextreal_2Eextreal,bool)))).
tff(stp_fo_c_2Eextreal_2Eextreal__lt,type,(fo__c_2Eextreal_2Eextreal__lt:(tp__ty_2Eextreal_2Eextreal * tp__ty_2Eextreal_2Eextreal) > tp__o)).
tff(stp_eq_fo_c_2Eextreal_2Eextreal__lt,axiom,( ! [X0:tp__ty_2Eextreal_2Eextreal] : ( ! [X1:tp__ty_2Eextreal_2Eextreal] : (inj__o(fo__c_2Eextreal_2Eextreal__lt(X0,X1)) = ap(ap(c_2Eextreal_2Eextreal__lt,inj__ty_2Eextreal_2Eextreal(X0)),inj__ty_2Eextreal_2Eextreal(X1)))))).
tff(tp_c_2Emeasure_2Esigma__algebra,type,(c_2Emeasure_2Esigma__algebra:del > $i)).
tff(mem_c_2Emeasure_2Esigma__algebra,axiom,( ! [A_27a:del] : mem(c_2Emeasure_2Esigma__algebra(A_27a),arr(ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),bool)))).
tff(tp_c_2Emeasure_2Esubsets,type,(c_2Emeasure_2Esubsets:del > $i)).
tff(mem_c_2Emeasure_2Esubsets,axiom,( ! [A_27a:del] : mem(c_2Emeasure_2Esubsets(A_27a),arr(ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),arr(arr(A_27a,bool),bool))))).
tff(tp_c_2Emeasure_2Espace,type,(c_2Emeasure_2Espace:del > $i)).
tff(mem_c_2Emeasure_2Espace,axiom,( ! [A_27a:del] : mem(c_2Emeasure_2Espace(A_27a),arr(ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),arr(A_27a,bool))))).
tff(tp_c_2Eextreal_2ENegInf,type,(c_2Eextreal_2ENegInf:$i)).
tff(mem_c_2Eextreal_2ENegInf,axiom,mem(c_2Eextreal_2ENegInf,ty_2Eextreal_2Eextreal)).
tff(stp_fo_c_2Eextreal_2ENegInf,type,(fo__c_2Eextreal_2ENegInf:tp__ty_2Eextreal_2Eextreal)).
tff(stp_eq_fo_c_2Eextreal_2ENegInf,axiom,(inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2ENegInf) = c_2Eextreal_2ENegInf)).
tff(tp_c_2Emeasure_2EBorel,type,(c_2Emeasure_2EBorel:$i)).
tff(mem_c_2Emeasure_2EBorel,axiom,mem(c_2Emeasure_2EBorel,ty_2Epair_2Eprod(arr(ty_2Eextreal_2Eextreal,bool),arr(arr(ty_2Eextreal_2Eextreal,bool),bool)))).
tff(tp_c_2Emeasure_2Emeasurable,type,(c_2Emeasure_2Emeasurable:(del * del) > $i)).
tff(mem_c_2Emeasure_2Emeasurable,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Emeasure_2Emeasurable(A_27a,A_27b),arr(ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool)),arr(ty_2Epair_2Eprod(arr(A_27b,bool),arr(arr(A_27b,bool),bool)),arr(arr(A_27a,A_27b),bool))))))).
tff(tp_c_2Earithmetic_2EEVEN,type,(c_2Earithmetic_2EEVEN:$i)).
tff(mem_c_2Earithmetic_2EEVEN,axiom,mem(c_2Earithmetic_2EEVEN,arr(ty_2Enum_2Enum,bool))).
tff(stp_fo_c_2Earithmetic_2EEVEN,type,(fo__c_2Earithmetic_2EEVEN:(tp__ty_2Enum_2Enum) > tp__o)).
tff(stp_eq_fo_c_2Earithmetic_2EEVEN,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__o(fo__c_2Earithmetic_2EEVEN(X0)) = ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Earithmetic_2E_3E,type,(c_2Earithmetic_2E_3E:$i)).
tff(mem_c_2Earithmetic_2E_3E,axiom,mem(c_2Earithmetic_2E_3E,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool)))).
tff(stp_fo_c_2Earithmetic_2E_3E,type,(fo__c_2Earithmetic_2E_3E:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__o)).
tff(stp_eq_fo_c_2Earithmetic_2E_3E,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__o(fo__c_2Earithmetic_2E_3E(X0,X1)) = ap(ap(c_2Earithmetic_2E_3E,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Eprim__rec_2EPRE,type,(c_2Eprim__rec_2EPRE:$i)).
tff(mem_c_2Eprim__rec_2EPRE,axiom,mem(c_2Eprim__rec_2EPRE,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))).
tff(stp_fo_c_2Eprim__rec_2EPRE,type,(fo__c_2Eprim__rec_2EPRE:(tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Eprim__rec_2EPRE,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Eprim__rec_2EPRE(X0)) = ap(c_2Eprim__rec_2EPRE,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Enum_2ESUC,type,(c_2Enum_2ESUC:$i)).
tff(mem_c_2Enum_2ESUC,axiom,mem(c_2Enum_2ESUC,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))).
tff(stp_fo_c_2Enum_2ESUC,type,(fo__c_2Enum_2ESUC:(tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Enum_2ESUC,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Enum_2ESUC(X0)) = ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Earithmetic_2E_2D,type,(c_2Earithmetic_2E_2D:$i)).
tff(mem_c_2Earithmetic_2E_2D,axiom,mem(c_2Earithmetic_2E_2D,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)))).
tff(stp_fo_c_2Earithmetic_2E_2D,type,(fo__c_2Earithmetic_2E_2D:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2E_2D,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2E_2D(X0,X1)) = ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Earithmetic_2E_2A,type,(c_2Earithmetic_2E_2A:$i)).
tff(mem_c_2Earithmetic_2E_2A,axiom,mem(c_2Earithmetic_2E_2A,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)))).
tff(stp_fo_c_2Earithmetic_2E_2A,type,(fo__c_2Earithmetic_2E_2A:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2E_2A,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2E_2A(X0,X1)) = ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Enumeral_2EiZ,type,(c_2Enumeral_2EiZ:$i)).
tff(mem_c_2Enumeral_2EiZ,axiom,mem(c_2Enumeral_2EiZ,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))).
tff(stp_fo_c_2Enumeral_2EiZ,type,(fo__c_2Enumeral_2EiZ:(tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Enumeral_2EiZ,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Enumeral_2EiZ(X0)) = ap(c_2Enumeral_2EiZ,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Earithmetic_2E_2B,type,(c_2Earithmetic_2E_2B:$i)).
tff(mem_c_2Earithmetic_2E_2B,axiom,mem(c_2Earithmetic_2E_2B,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)))).
tff(stp_fo_c_2Earithmetic_2E_2B,type,(fo__c_2Earithmetic_2E_2B:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2E_2B,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2E_2B(X0,X1)) = ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Earithmetic_2E_3C_3D,type,(c_2Earithmetic_2E_3C_3D:$i)).
tff(mem_c_2Earithmetic_2E_3C_3D,axiom,mem(c_2Earithmetic_2E_3C_3D,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool)))).
tff(stp_fo_c_2Earithmetic_2E_3C_3D,type,(fo__c_2Earithmetic_2E_3C_3D:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__o)).
tff(stp_eq_fo_c_2Earithmetic_2E_3C_3D,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__o(fo__c_2Earithmetic_2E_3C_3D(X0,X1)) = ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Epred__set_2EINTER,type,(c_2Epred__set_2EINTER:del > $i)).
tff(mem_c_2Epred__set_2EINTER,axiom,( ! [A_27a:del] : mem(c_2Epred__set_2EINTER(A_27a),arr(arr(A_27a,bool),arr(arr(A_27a,bool),arr(A_27a,bool)))))).
tff(tp_c_2Epred__set_2EDIFF,type,(c_2Epred__set_2EDIFF:del > $i)).
tff(mem_c_2Epred__set_2EDIFF,axiom,( ! [A_27a:del] : mem(c_2Epred__set_2EDIFF(A_27a),arr(arr(A_27a,bool),arr(arr(A_27a,bool),arr(A_27a,bool)))))).
tff(tp_c_2Epred__set_2EFUNSET,type,(c_2Epred__set_2EFUNSET:(del * del) > $i)).
tff(mem_c_2Epred__set_2EFUNSET,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Epred__set_2EFUNSET(A_27a,A_27b),arr(arr(A_27a,bool),arr(arr(A_27b,bool),arr(arr(A_27a,A_27b),bool))))))).
tff(tp_c_2Epred__set_2EBIGUNION,type,(c_2Epred__set_2EBIGUNION:del > $i)).
tff(mem_c_2Epred__set_2EBIGUNION,axiom,( ! [A_27a:del] : mem(c_2Epred__set_2EBIGUNION(A_27a),arr(arr(arr(A_27a,bool),bool),arr(A_27a,bool))))).
tff(tp_c_2Epred__set_2EIMAGE,type,(c_2Epred__set_2EIMAGE:(del * del) > $i)).
tff(mem_c_2Epred__set_2EIMAGE,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Epred__set_2EIMAGE(A_27a,A_27b),arr(arr(A_27a,A_27b),arr(arr(A_27a,bool),arr(A_27b,bool))))))).
tff(tp_c_2Epred__set_2EBIGINTER,type,(c_2Epred__set_2EBIGINTER:del > $i)).
tff(mem_c_2Epred__set_2EBIGINTER,axiom,( ! [A_27a:del] : mem(c_2Epred__set_2EBIGINTER(A_27a),arr(arr(arr(A_27a,bool),bool),arr(A_27a,bool))))).
tff(tp_c_2Ebool_2EIN,type,(c_2Ebool_2EIN:del > $i)).
tff(mem_c_2Ebool_2EIN,axiom,( ! [A_27a:del] : mem(c_2Ebool_2EIN(A_27a),arr(A_27a,arr(arr(A_27a,bool),bool))))).
tff(tp_c_2Epred__set_2EEMPTY,type,(c_2Epred__set_2EEMPTY:del > $i)).
tff(mem_c_2Epred__set_2EEMPTY,axiom,( ! [A_27a:del] : mem(c_2Epred__set_2EEMPTY(A_27a),arr(A_27a,bool)))).
tff(tp_c_2Epred__set_2EUNIV,type,(c_2Epred__set_2EUNIV:del > $i)).
tff(mem_c_2Epred__set_2EUNIV,axiom,( ! [A_27a:del] : mem(c_2Epred__set_2EUNIV(A_27a),arr(A_27a,bool)))).
tff(tp_c_2Ebool_2ET,type,(c_2Ebool_2ET:$i)).
tff(mem_c_2Ebool_2ET,axiom,mem(c_2Ebool_2ET,bool)).
tff(stp_fo_c_2Ebool_2ET,type,(fo__c_2Ebool_2ET:tp__o)).
tff(stp_eq_fo_c_2Ebool_2ET,axiom,(inj__o(fo__c_2Ebool_2ET) = c_2Ebool_2ET)).
tff(ax_true_p,axiom,p(c_2Ebool_2ET)).
tff(tp_c_2Epair_2E_2C,type,(c_2Epair_2E_2C:(del * del) > $i)).
tff(mem_c_2Epair_2E_2C,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Epair_2E_2C(A_27a,A_27b),arr(A_27a,arr(A_27b,ty_2Epair_2Eprod(A_27a,A_27b))))))).
tff(tp_c_2Epred__set_2EGSPEC,type,(c_2Epred__set_2EGSPEC:(del * del) > $i)).
tff(mem_c_2Epred__set_2EGSPEC,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Epred__set_2EGSPEC(A_27a,A_27b),arr(arr(A_27b,ty_2Epair_2Eprod(A_27a,bool)),arr(A_27a,bool)))))).
tff(tp_c_2Eprim__rec_2E_3C,type,(c_2Eprim__rec_2E_3C:$i)).
tff(mem_c_2Eprim__rec_2E_3C,axiom,mem(c_2Eprim__rec_2E_3C,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool)))).
tff(stp_fo_c_2Eprim__rec_2E_3C,type,(fo__c_2Eprim__rec_2E_3C:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__o)).
tff(stp_eq_fo_c_2Eprim__rec_2E_3C,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__o(fo__c_2Eprim__rec_2E_3C(X0,X1)) = ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Earithmetic_2EODD,type,(c_2Earithmetic_2EODD:$i)).
tff(mem_c_2Earithmetic_2EODD,axiom,mem(c_2Earithmetic_2EODD,arr(ty_2Enum_2Enum,bool))).
tff(stp_fo_c_2Earithmetic_2EODD,type,(fo__c_2Earithmetic_2EODD:(tp__ty_2Enum_2Enum) > tp__o)).
tff(stp_eq_fo_c_2Earithmetic_2EODD,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__o(fo__c_2Earithmetic_2EODD(X0)) = ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Earithmetic_2EEXP,type,(c_2Earithmetic_2EEXP:$i)).
tff(mem_c_2Earithmetic_2EEXP,axiom,mem(c_2Earithmetic_2EEXP,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)))).
tff(stp_fo_c_2Earithmetic_2EEXP,type,(fo__c_2Earithmetic_2EEXP:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2EEXP,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EEXP(X0,X1)) = ap(ap(c_2Earithmetic_2EEXP,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Earithmetic_2EBIT2,type,(c_2Earithmetic_2EBIT2:$i)).
tff(mem_c_2Earithmetic_2EBIT2,axiom,mem(c_2Earithmetic_2EBIT2,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))).
tff(stp_fo_c_2Earithmetic_2EBIT2,type,(fo__c_2Earithmetic_2EBIT2:(tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2EBIT2,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EBIT2(X0)) = ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Erealax_2Ereal__neg,type,(c_2Erealax_2Ereal__neg:$i)).
tff(mem_c_2Erealax_2Ereal__neg,axiom,mem(c_2Erealax_2Ereal__neg,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))).
tff(stp_fo_c_2Erealax_2Ereal__neg,type,(fo__c_2Erealax_2Ereal__neg:(tp__ty_2Erealax_2Ereal) > tp__ty_2Erealax_2Ereal)).
tff(stp_eq_fo_c_2Erealax_2Ereal__neg,axiom,( ! [X0:tp__ty_2Erealax_2Ereal] : (inj__ty_2Erealax_2Ereal(fo__c_2Erealax_2Ereal__neg(X0)) = ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(X0))))).
tff(tp_c_2Erealax_2Ereal__mul,type,(c_2Erealax_2Ereal__mul:$i)).
tff(mem_c_2Erealax_2Ereal__mul,axiom,mem(c_2Erealax_2Ereal__mul,arr(ty_2Erealax_2Ereal,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)))).
tff(stp_fo_c_2Erealax_2Ereal__mul,type,(fo__c_2Erealax_2Ereal__mul:(tp__ty_2Erealax_2Ereal * tp__ty_2Erealax_2Ereal) > tp__ty_2Erealax_2Ereal)).
tff(stp_eq_fo_c_2Erealax_2Ereal__mul,axiom,( ! [X0:tp__ty_2Erealax_2Ereal] : ( ! [X1:tp__ty_2Erealax_2Ereal] : (inj__ty_2Erealax_2Ereal(fo__c_2Erealax_2Ereal__mul(X0,X1)) = ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(X0)),inj__ty_2Erealax_2Ereal(X1)))))).
tff(tp_c_2Emarker_2Eunint,type,(c_2Emarker_2Eunint:del > $i)).
tff(mem_c_2Emarker_2Eunint,axiom,( ! [A_27a:del] : mem(c_2Emarker_2Eunint(A_27a),arr(A_27a,A_27a)))).
tff(tp_c_2Ebool_2ECOND,type,(c_2Ebool_2ECOND:del > $i)).
tff(mem_c_2Ebool_2ECOND,axiom,( ! [A_27a:del] : mem(c_2Ebool_2ECOND(A_27a),arr(bool,arr(A_27a,arr(A_27a,A_27a)))))).
tff(tp_c_2Ereal_2E_2F,type,(c_2Ereal_2E_2F:$i)).
tff(mem_c_2Ereal_2E_2F,axiom,mem(c_2Ereal_2E_2F,arr(ty_2Erealax_2Ereal,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)))).
tff(stp_fo_c_2Ereal_2E_2F,type,(fo__c_2Ereal_2E_2F:(tp__ty_2Erealax_2Ereal * tp__ty_2Erealax_2Ereal) > tp__ty_2Erealax_2Ereal)).
tff(stp_eq_fo_c_2Ereal_2E_2F,axiom,( ! [X0:tp__ty_2Erealax_2Ereal] : ( ! [X1:tp__ty_2Erealax_2Ereal] : (inj__ty_2Erealax_2Ereal(fo__c_2Ereal_2E_2F(X0,X1)) = ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(X0)),inj__ty_2Erealax_2Ereal(X1)))))).
tff(tp_c_2Ebool_2EF,type,(c_2Ebool_2EF:$i)).
tff(mem_c_2Ebool_2EF,axiom,mem(c_2Ebool_2EF,bool)).
tff(stp_fo_c_2Ebool_2EF,type,(fo__c_2Ebool_2EF:tp__o)).
tff(stp_eq_fo_c_2Ebool_2EF,axiom,(inj__o(fo__c_2Ebool_2EF) = c_2Ebool_2EF)).
tff(ax_false_p,axiom,(~ p(c_2Ebool_2EF))).
tff(tp_c_2Ebool_2E_5C_2F,type,(c_2Ebool_2E_5C_2F:$i)).
tff(mem_c_2Ebool_2E_5C_2F,axiom,mem(c_2Ebool_2E_5C_2F,arr(bool,arr(bool,bool)))).
tff(stp_fo_c_2Ebool_2E_5C_2F,type,(fo__c_2Ebool_2E_5C_2F:(tp__o * tp__o) > tp__o)).
tff(stp_eq_fo_c_2Ebool_2E_5C_2F,axiom,( ! [X0:tp__o] : ( ! [X1:tp__o] : (inj__o(fo__c_2Ebool_2E_5C_2F(X0,X1)) = ap(ap(c_2Ebool_2E_5C_2F,inj__o(X0)),inj__o(X1)))))).
tff(ax_or_p,axiom,( ! [Q:$i] : (mem(Q,bool) => ( ! [R:$i] : (mem(R,bool) => (p(ap(ap(c_2Ebool_2E_5C_2F,Q),R)) <=> (p(Q) | p(R)))))))).
tff(tp_c_2Ebool_2E_7E,type,(c_2Ebool_2E_7E:$i)).
tff(mem_c_2Ebool_2E_7E,axiom,mem(c_2Ebool_2E_7E,arr(bool,bool))).
tff(stp_fo_c_2Ebool_2E_7E,type,(fo__c_2Ebool_2E_7E:(tp__o) > tp__o)).
tff(stp_eq_fo_c_2Ebool_2E_7E,axiom,( ! [X0:tp__o] : (inj__o(fo__c_2Ebool_2E_7E(X0)) = ap(c_2Ebool_2E_7E,inj__o(X0))))).
tff(ax_neg_p,axiom,( ! [Q:$i] : (mem(Q,bool) => (p(ap(c_2Ebool_2E_7E,Q)) <=> (~ p(Q)))))).
tff(tp_c_2Earithmetic_2E_3E_3D,type,(c_2Earithmetic_2E_3E_3D:$i)).
tff(mem_c_2Earithmetic_2E_3E_3D,axiom,mem(c_2Earithmetic_2E_3E_3D,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool)))).
tff(stp_fo_c_2Earithmetic_2E_3E_3D,type,(fo__c_2Earithmetic_2E_3E_3D:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__o)).
tff(stp_eq_fo_c_2Earithmetic_2E_3E_3D,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__o(fo__c_2Earithmetic_2E_3E_3D(X0,X1)) = ap(ap(c_2Earithmetic_2E_3E_3D,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Ebool_2E_3F,type,(c_2Ebool_2E_3F:del > $i)).
tff(mem_c_2Ebool_2E_3F,axiom,( ! [A_27a:del] : mem(c_2Ebool_2E_3F(A_27a),arr(arr(A_27a,bool),bool)))).
tff(ax_ex_p,axiom,( ! [A:del] : ( ! [Q:$i] : (mem(Q,arr(A,bool)) => (p(ap(c_2Ebool_2E_3F(A),Q)) <=> (? [X:$i] : (mem(X,A) & p(ap(Q,X))))))))).
tff(tp_c_2Emin_2E_3D,type,(c_2Emin_2E_3D:del > $i)).
tff(mem_c_2Emin_2E_3D,axiom,( ! [A_27a:del] : mem(c_2Emin_2E_3D(A_27a),arr(A_27a,arr(A_27a,bool))))).
tff(ax_eq_p,axiom,( ! [A:del] : ( ! [X:$i] : (mem(X,A) => ( ! [Y:$i] : (mem(Y,A) => (p(ap(ap(c_2Emin_2E_3D(A),X),Y)) <=> (X = Y)))))))).
tff(tp_c_2Erealax_2Ereal__add,type,(c_2Erealax_2Ereal__add:$i)).
tff(mem_c_2Erealax_2Ereal__add,axiom,mem(c_2Erealax_2Ereal__add,arr(ty_2Erealax_2Ereal,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)))).
tff(stp_fo_c_2Erealax_2Ereal__add,type,(fo__c_2Erealax_2Ereal__add:(tp__ty_2Erealax_2Ereal * tp__ty_2Erealax_2Ereal) > tp__ty_2Erealax_2Ereal)).
tff(stp_eq_fo_c_2Erealax_2Ereal__add,axiom,( ! [X0:tp__ty_2Erealax_2Ereal] : ( ! [X1:tp__ty_2Erealax_2Ereal] : (inj__ty_2Erealax_2Ereal(fo__c_2Erealax_2Ereal__add(X0,X1)) = ap(ap(c_2Erealax_2Ereal__add,inj__ty_2Erealax_2Ereal(X0)),inj__ty_2Erealax_2Ereal(X1)))))).
tff(tp_c_2Ereal_2Ereal__sub,type,(c_2Ereal_2Ereal__sub:$i)).
tff(mem_c_2Ereal_2Ereal__sub,axiom,mem(c_2Ereal_2Ereal__sub,arr(ty_2Erealax_2Ereal,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)))).
tff(stp_fo_c_2Ereal_2Ereal__sub,type,(fo__c_2Ereal_2Ereal__sub:(tp__ty_2Erealax_2Ereal * tp__ty_2Erealax_2Ereal) > tp__ty_2Erealax_2Ereal)).
tff(stp_eq_fo_c_2Ereal_2Ereal__sub,axiom,( ! [X0:tp__ty_2Erealax_2Ereal] : ( ! [X1:tp__ty_2Erealax_2Ereal] : (inj__ty_2Erealax_2Ereal(fo__c_2Ereal_2Ereal__sub(X0,X1)) = ap(ap(c_2Ereal_2Ereal__sub,inj__ty_2Erealax_2Ereal(X0)),inj__ty_2Erealax_2Ereal(X1)))))).
tff(tp_c_2Enum_2E0,type,(c_2Enum_2E0:$i)).
tff(mem_c_2Enum_2E0,axiom,mem(c_2Enum_2E0,ty_2Enum_2Enum)).
tff(stp_fo_c_2Enum_2E0,type,(fo__c_2Enum_2E0:tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Enum_2E0,axiom,(inj__ty_2Enum_2Enum(fo__c_2Enum_2E0) = c_2Enum_2E0)).
tff(tp_c_2Ereal_2Epow,type,(c_2Ereal_2Epow:$i)).
tff(mem_c_2Ereal_2Epow,axiom,mem(c_2Ereal_2Epow,arr(ty_2Erealax_2Ereal,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)))).
tff(stp_fo_c_2Ereal_2Epow,type,(fo__c_2Ereal_2Epow:(tp__ty_2Erealax_2Ereal * tp__ty_2Enum_2Enum) > tp__ty_2Erealax_2Ereal)).
tff(stp_eq_fo_c_2Ereal_2Epow,axiom,( ! [X0:tp__ty_2Erealax_2Ereal] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__ty_2Erealax_2Ereal(fo__c_2Ereal_2Epow(X0,X1)) = ap(ap(c_2Ereal_2Epow,inj__ty_2Erealax_2Ereal(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Earithmetic_2EZERO,type,(c_2Earithmetic_2EZERO:$i)).
tff(mem_c_2Earithmetic_2EZERO,axiom,mem(c_2Earithmetic_2EZERO,ty_2Enum_2Enum)).
tff(stp_fo_c_2Earithmetic_2EZERO,type,(fo__c_2Earithmetic_2EZERO:tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2EZERO,axiom,(inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO) = c_2Earithmetic_2EZERO)).
tff(tp_c_2Earithmetic_2EBIT1,type,(c_2Earithmetic_2EBIT1:$i)).
tff(mem_c_2Earithmetic_2EBIT1,axiom,mem(c_2Earithmetic_2EBIT1,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))).
tff(stp_fo_c_2Earithmetic_2EBIT1,type,(fo__c_2Earithmetic_2EBIT1:(tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2EBIT1,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EBIT1(X0)) = ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Earithmetic_2ENUMERAL,type,(c_2Earithmetic_2ENUMERAL:$i)).
tff(mem_c_2Earithmetic_2ENUMERAL,axiom,mem(c_2Earithmetic_2ENUMERAL,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))).
tff(stp_fo_c_2Earithmetic_2ENUMERAL,type,(fo__c_2Earithmetic_2ENUMERAL:(tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2ENUMERAL,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2ENUMERAL(X0)) = ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Ereal_2Ereal__of__num,type,(c_2Ereal_2Ereal__of__num:$i)).
tff(mem_c_2Ereal_2Ereal__of__num,axiom,mem(c_2Ereal_2Ereal__of__num,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal))).
tff(stp_fo_c_2Ereal_2Ereal__of__num,type,(fo__c_2Ereal_2Ereal__of__num:(tp__ty_2Enum_2Enum) > tp__ty_2Erealax_2Ereal)).
tff(stp_eq_fo_c_2Ereal_2Ereal__of__num,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2Erealax_2Ereal(fo__c_2Ereal_2Ereal__of__num(X0)) = ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Ereal_2Eabs,type,(c_2Ereal_2Eabs:$i)).
tff(mem_c_2Ereal_2Eabs,axiom,mem(c_2Ereal_2Eabs,arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal))).
tff(stp_fo_c_2Ereal_2Eabs,type,(fo__c_2Ereal_2Eabs:(tp__ty_2Erealax_2Ereal) > tp__ty_2Erealax_2Ereal)).
tff(stp_eq_fo_c_2Ereal_2Eabs,axiom,( ! [X0:tp__ty_2Erealax_2Ereal] : (inj__ty_2Erealax_2Ereal(fo__c_2Ereal_2Eabs(X0)) = ap(c_2Ereal_2Eabs,inj__ty_2Erealax_2Ereal(X0))))).
tff(tp_c_2Erealax_2Ereal__lt,type,(c_2Erealax_2Ereal__lt:$i)).
tff(mem_c_2Erealax_2Ereal__lt,axiom,mem(c_2Erealax_2Ereal__lt,arr(ty_2Erealax_2Ereal,arr(ty_2Erealax_2Ereal,bool)))).
tff(stp_fo_c_2Erealax_2Ereal__lt,type,(fo__c_2Erealax_2Ereal__lt:(tp__ty_2Erealax_2Ereal * tp__ty_2Erealax_2Ereal) > tp__o)).
tff(stp_eq_fo_c_2Erealax_2Ereal__lt,axiom,( ! [X0:tp__ty_2Erealax_2Ereal] : ( ! [X1:tp__ty_2Erealax_2Ereal] : (inj__o(fo__c_2Erealax_2Ereal__lt(X0,X1)) = ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(X0)),inj__ty_2Erealax_2Ereal(X1)))))).
tff(tp_c_2Eseq_2E_2D_2D_3E,type,(c_2Eseq_2E_2D_2D_3E:$i)).
tff(mem_c_2Eseq_2E_2D_2D_3E,axiom,mem(c_2Eseq_2E_2D_2D_3E,arr(arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal),arr(ty_2Erealax_2Ereal,bool)))).
tff(tp_c_2Ereal_2Ereal__lte,type,(c_2Ereal_2Ereal__lte:$i)).
tff(mem_c_2Ereal_2Ereal__lte,axiom,mem(c_2Ereal_2Ereal__lte,arr(ty_2Erealax_2Ereal,arr(ty_2Erealax_2Ereal,bool)))).
tff(stp_fo_c_2Ereal_2Ereal__lte,type,(fo__c_2Ereal_2Ereal__lte:(tp__ty_2Erealax_2Ereal * tp__ty_2Erealax_2Ereal) > tp__o)).
tff(stp_eq_fo_c_2Ereal_2Ereal__lte,axiom,( ! [X0:tp__ty_2Erealax_2Ereal] : ( ! [X1:tp__ty_2Erealax_2Ereal] : (inj__o(fo__c_2Ereal_2Ereal__lte(X0,X1)) = ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(X0)),inj__ty_2Erealax_2Ereal(X1)))))).
tff(tp_c_2Ebool_2E_2F_5C,type,(c_2Ebool_2E_2F_5C:$i)).
tff(mem_c_2Ebool_2E_2F_5C,axiom,mem(c_2Ebool_2E_2F_5C,arr(bool,arr(bool,bool)))).
tff(stp_fo_c_2Ebool_2E_2F_5C,type,(fo__c_2Ebool_2E_2F_5C:(tp__o * tp__o) > tp__o)).
tff(stp_eq_fo_c_2Ebool_2E_2F_5C,axiom,( ! [X0:tp__o] : ( ! [X1:tp__o] : (inj__o(fo__c_2Ebool_2E_2F_5C(X0,X1)) = ap(ap(c_2Ebool_2E_2F_5C,inj__o(X0)),inj__o(X1)))))).
tff(ax_and_p,axiom,( ! [Q:$i] : (mem(Q,bool) => ( ! [R:$i] : (mem(R,bool) => (p(ap(ap(c_2Ebool_2E_2F_5C,Q),R)) <=> (p(Q) & p(R)))))))).
tff(tp_c_2Emin_2E_3D_3D_3E,type,(c_2Emin_2E_3D_3D_3E:$i)).
tff(mem_c_2Emin_2E_3D_3D_3E,axiom,mem(c_2Emin_2E_3D_3D_3E,arr(bool,arr(bool,bool)))).
tff(stp_fo_c_2Emin_2E_3D_3D_3E,type,(fo__c_2Emin_2E_3D_3D_3E:(tp__o * tp__o) > tp__o)).
tff(stp_eq_fo_c_2Emin_2E_3D_3D_3E,axiom,( ! [X0:tp__o] : ( ! [X1:tp__o] : (inj__o(fo__c_2Emin_2E_3D_3D_3E(X0,X1)) = ap(ap(c_2Emin_2E_3D_3D_3E,inj__o(X0)),inj__o(X1)))))).
tff(ax_imp_p,axiom,( ! [Q:$i] : (mem(Q,bool) => ( ! [R:$i] : (mem(R,bool) => (p(ap(ap(c_2Emin_2E_3D_3D_3E,Q),R)) <=> (p(Q) => p(R)))))))).
tff(tp_c_2Ebool_2E_21,type,(c_2Ebool_2E_21:del > $i)).
tff(mem_c_2Ebool_2E_21,axiom,( ! [A_27a:del] : mem(c_2Ebool_2E_21(A_27a),arr(arr(A_27a,bool),bool)))).
tff(ax_all_p,axiom,( ! [A:del] : ( ! [Q:$i] : (mem(Q,arr(A,bool)) => (p(ap(c_2Ebool_2E_21(A),Q)) <=> ( ! [X:$i] : (mem(X,A) => p(ap(Q,X))))))))).
tff(conj_thm_2Earithmetic_2EADD__CLAUSES,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0m))) = V0m) & ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = V0m) & ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0m))),inj__ty_2Enum_2Enum(V1n))) = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))))) & (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1n)))) = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))))))))))).
tff(conj_thm_2Earithmetic_2EADD__SYM,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V0m)))))))).
tff(conj_thm_2Earithmetic_2EMULT__CLAUSES,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0m))) = fo__c_2Enum_2E0) & ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = fo__c_2Enum_2E0) & ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(V0m))) = V0m) & ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) = V0m) & ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0m))),inj__ty_2Enum_2Enum(V1n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(V1n)))) & (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1n)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))))))))))))).
tff(conj_thm_2Earithmetic_2EGREATER__EQ,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3E_3D,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1m)),inj__ty_2Enum_2Enum(V0n)))))))).
tff(conj_thm_2Earithmetic_2EADD__MONO__LESS__EQ,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2p)))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p))))))))).
tff(conj_thm_2Earithmetic_2ENOT__LEQ,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)))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(V0m)))))))).
tff(conj_thm_2Earithmetic_2ESUC__ONE__ADD,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(V0n))))))).
tff(ax_thm_2Ebool_2EEXISTS__DEF,axiom,( ! [A_27a:del]: (c_2Ebool_2E_3F(A_27a) = f2(A_27a)))).
tff(ax_thm_2Ebool_2EETA__AX,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0t:$i] : (mem(V0t,arr(A_27a,A_27b)) => (f31(A_27b,A_27a,V0t) = V0t)))))).
tff(ax_thm_2Ebool_2ESELECT__AX,axiom,( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1x:$i] : (mem(V1x,A_27a) => (p(ap(V0P,V1x)) => p(ap(V0P,ap(c_2Emin_2E_40(A_27a),V0P)))))))))).
tff(conj_thm_2Ebool_2ETRUTH,lemma,($true)).
tff(conj_thm_2Ebool_2EIMP__ANTISYM__AX,lemma,(( ! [V0t1:tp__o] : ( ! [V1t2:tp__o] : ((p(inj__o(V0t1)) => p(inj__o(V1t2))) => ((p(inj__o(V1t2)) => p(inj__o(V0t1))) => (p(inj__o(V0t1)) <=> p(inj__o(V1t2))))))))).
tff(conj_thm_2Ebool_2EFALSITY,lemma,(( ! [V0t:tp__o] : ($false => p(inj__o(V0t)))))).
tff(conj_thm_2Ebool_2EEXCLUDED__MIDDLE,lemma,(( ! [V0t:tp__o] : (p(inj__o(V0t)) | (~~ p(inj__o(V0t))))))).
tff(conj_thm_2Ebool_2EFORALL__SIMP,lemma,(( ! [A_27a:del]: ( ! [V0t:tp__o] : (( ! [V1x:$i] : (mem(V1x,A_27a) => p(inj__o(V0t)))) <=> p(inj__o(V0t))))))).
tff(conj_thm_2Ebool_2EF__IMP,lemma,(( ! [V0t:tp__o] : ((~~ p(inj__o(V0t))) => (p(inj__o(V0t)) => $false))))).
tff(conj_thm_2Ebool_2EAND__CLAUSES,lemma,(( ! [V0t:tp__o] : ((($true & p(inj__o(V0t))) <=> p(inj__o(V0t))) & (((p(inj__o(V0t)) & $true) <=> p(inj__o(V0t))) & ((($false & p(inj__o(V0t))) <=> $false) & (((p(inj__o(V0t)) & $false) <=> $false) & ((p(inj__o(V0t)) & p(inj__o(V0t))) <=> p(inj__o(V0t)))))))))).
tff(conj_thm_2Ebool_2EOR__CLAUSES,lemma,(( ! [V0t:tp__o] : ((($true | p(inj__o(V0t))) <=> $true) & (((p(inj__o(V0t)) | $true) <=> $true) & ((($false | p(inj__o(V0t))) <=> p(inj__o(V0t))) & (((p(inj__o(V0t)) | $false) <=> p(inj__o(V0t))) & ((p(inj__o(V0t)) | p(inj__o(V0t))) <=> p(inj__o(V0t)))))))))).
tff(conj_thm_2Ebool_2EIMP__CLAUSES,lemma,(( ! [V0t:tp__o] : ((($true => p(inj__o(V0t))) <=> p(inj__o(V0t))) & (((p(inj__o(V0t)) => $true) <=> $true) & ((($false => p(inj__o(V0t))) <=> $true) & (((p(inj__o(V0t)) => p(inj__o(V0t))) <=> $true) & ((p(inj__o(V0t)) => $false) <=> (~~ p(inj__o(V0t))))))))))).
tff(conj_thm_2Ebool_2ENOT__CLAUSES,lemma,((( ! [V0t:tp__o] : ((~~ (~~ p(inj__o(V0t)))) <=> p(inj__o(V0t)))) & (((~~ ($true)) <=> $false) & ((~~ ($false)) <=> $true))))).
tff(conj_thm_2Ebool_2EEQ__REFL,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => (V0x = V0x)))))).
tff(conj_thm_2Ebool_2EREFL__CLAUSE,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ((V0x = V0x) <=> $true)))))).
tff(conj_thm_2Ebool_2EEQ__SYM__EQ,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1y:$i] : (mem(V1y,A_27a) => ((V0x = V1y) <=> (V1y = V0x))))))))).
tff(conj_thm_2Ebool_2EFUN__EQ__THM,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27b)) => ( ! [V1g:$i] : (mem(V1g,arr(A_27a,A_27b)) => ((V0f = V1g) <=> ( ! [V2x:$i] : (mem(V2x,A_27a) => (ap(V0f,V2x) = ap(V1g,V2x))))))))))))).
tff(conj_thm_2Ebool_2EEQ__CLAUSES,lemma,(( ! [V0t:tp__o] : ((($true <=> p(inj__o(V0t))) <=> p(inj__o(V0t))) & (((p(inj__o(V0t)) <=> $true) <=> p(inj__o(V0t))) & ((($false <=> p(inj__o(V0t))) <=> (~~ p(inj__o(V0t)))) & ((p(inj__o(V0t)) <=> $false) <=> (~~ p(inj__o(V0t)))))))))).
tff(conj_thm_2Ebool_2ECOND__CLAUSES,lemma,(( ! [A_27a:del]: ( ! [V0t1:$i] : (mem(V0t1,A_27a) => ( ! [V1t2:$i] : (mem(V1t2,A_27a) => ((ap(ap(ap(c_2Ebool_2ECOND(A_27a),inj__o(fo__c_2Ebool_2ET)),V0t1),V1t2) = V0t1) & (ap(ap(ap(c_2Ebool_2ECOND(A_27a),inj__o(fo__c_2Ebool_2EF)),V0t1),V1t2) = V1t2))))))))).
tff(conj_thm_2Ebool_2EFORALL__AND__THM,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1Q:$i] : (mem(V1Q,arr(A_27a,bool)) => (( ! [V2x:$i] : (mem(V2x,A_27a) => (p(ap(V0P,V2x)) & p(ap(V1Q,V2x))))) <=> (( ! [V3x:$i] : (mem(V3x,A_27a) => p(ap(V0P,V3x)))) & ( ! [V4x:$i] : (mem(V4x,A_27a) => p(ap(V1Q,V4x))))))))))))).
tff(conj_thm_2Ebool_2ERIGHT__AND__FORALL__THM,lemma,(( ! [A_27a:del]: ( ! [V0P:tp__o] : ( ! [V1Q:$i] : (mem(V1Q,arr(A_27a,bool)) => ((p(inj__o(V0P)) & ( ! [V2x:$i] : (mem(V2x,A_27a) => p(ap(V1Q,V2x))))) <=> ( ! [V3x:$i] : (mem(V3x,A_27a) => (p(inj__o(V0P)) & p(ap(V1Q,V3x)))))))))))).
tff(conj_thm_2Ebool_2ELEFT__FORALL__OR__THM,lemma,(( ! [A_27a:del]: ( ! [V0Q:tp__o] : ( ! [V1P:$i] : (mem(V1P,arr(A_27a,bool)) => (( ! [V2x:$i] : (mem(V2x,A_27a) => (p(ap(V1P,V2x)) | p(inj__o(V0Q))))) <=> (( ! [V3x:$i] : (mem(V3x,A_27a) => p(ap(V1P,V3x)))) | p(inj__o(V0Q)))))))))).
tff(conj_thm_2Ebool_2ERIGHT__FORALL__OR__THM,lemma,(( ! [A_27a:del]: ( ! [V0P:tp__o] : ( ! [V1Q:$i] : (mem(V1Q,arr(A_27a,bool)) => (( ! [V2x:$i] : (mem(V2x,A_27a) => (p(inj__o(V0P)) | p(ap(V1Q,V2x))))) <=> (p(inj__o(V0P)) | ( ! [V3x:$i] : (mem(V3x,A_27a) => p(ap(V1Q,V3x)))))))))))).
tff(conj_thm_2Ebool_2EDE__MORGAN__THM,lemma,(( ! [V0A:tp__o] : ( ! [V1B:tp__o] : (((~~ (p(inj__o(V0A)) & p(inj__o(V1B)))) <=> ((~~ p(inj__o(V0A))) | (~~ p(inj__o(V1B))))) & ((~~ (p(inj__o(V0A)) | p(inj__o(V1B)))) <=> ((~~ p(inj__o(V0A))) & (~~ p(inj__o(V1B)))))))))).
tff(conj_thm_2Ebool_2ELEFT__OR__OVER__AND,lemma,(( ! [V0A:tp__o] : ( ! [V1B:tp__o] : ( ! [V2C:tp__o] : ((p(inj__o(V0A)) | (p(inj__o(V1B)) & p(inj__o(V2C)))) <=> ((p(inj__o(V0A)) | p(inj__o(V1B))) & (p(inj__o(V0A)) | p(inj__o(V2C)))))))))).
tff(conj_thm_2Ebool_2ERIGHT__OR__OVER__AND,lemma,(( ! [V0A:tp__o] : ( ! [V1B:tp__o] : ( ! [V2C:tp__o] : (((p(inj__o(V1B)) & p(inj__o(V2C))) | p(inj__o(V0A))) <=> ((p(inj__o(V1B)) | p(inj__o(V0A))) & (p(inj__o(V2C)) | p(inj__o(V0A)))))))))).
tff(conj_thm_2Ebool_2EIMP__F__EQ__F,lemma,(( ! [V0t:tp__o] : ((p(inj__o(V0t)) => $false) <=> (p(inj__o(V0t)) <=> $false))))).
tff(conj_thm_2Ebool_2EAND__IMP__INTRO,lemma,(( ! [V0t1:tp__o] : ( ! [V1t2:tp__o] : ( ! [V2t3:tp__o] : ((p(inj__o(V0t1)) => (p(inj__o(V1t2)) => p(inj__o(V2t3)))) <=> ((p(inj__o(V0t1)) & p(inj__o(V1t2))) => p(inj__o(V2t3))))))))).
tff(conj_thm_2Ebool_2EIMP__CONG,lemma,(( ! [V0x:tp__o] : ( ! [V1x_27:tp__o] : ( ! [V2y:tp__o] : ( ! [V3y_27:tp__o] : (((p(inj__o(V0x)) <=> p(inj__o(V1x_27))) & (p(inj__o(V1x_27)) => (p(inj__o(V2y)) <=> p(inj__o(V3y_27))))) => ((p(inj__o(V0x)) => p(inj__o(V2y))) <=> (p(inj__o(V1x_27)) => p(inj__o(V3y_27))))))))))).
tff(conj_thm_2Ebool_2ECOND__CONG,lemma,(( ! [A_27a:del]: ( ! [V0P:tp__o] : ( ! [V1Q:tp__o] : ( ! [V2x:$i] : (mem(V2x,A_27a) => ( ! [V3x_27:$i] : (mem(V3x_27,A_27a) => ( ! [V4y:$i] : (mem(V4y,A_27a) => ( ! [V5y_27:$i] : (mem(V5y_27,A_27a) => (((p(inj__o(V0P)) <=> p(inj__o(V1Q))) & ((p(inj__o(V1Q)) => (V2x = V3x_27)) & ((~~ p(inj__o(V1Q))) => (V4y = V5y_27)))) => (ap(ap(ap(c_2Ebool_2ECOND(A_27a),inj__o(V0P)),V2x),V4y) = ap(ap(ap(c_2Ebool_2ECOND(A_27a),inj__o(V1Q)),V3x_27),V5y_27)))))))))))))))).
tff(conj_thm_2Ebool_2EUNWIND__THM2,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1a:$i] : (mem(V1a,A_27a) => ((? [V2x:$i] : (mem(V2x,A_27a) & ((V2x = V1a) & p(ap(V0P,V2x))))) <=> p(ap(V0P,V1a)))))))))).
tff(conj_thm_2Ebool_2Ebool__case__thm,lemma,(( ! [A_27a:del]: (( ! [V0t1:$i] : (mem(V0t1,A_27a) => ( ! [V1t2:$i] : (mem(V1t2,A_27a) => (ap(ap(ap(c_2Ebool_2ECOND(A_27a),inj__o(fo__c_2Ebool_2ET)),V0t1),V1t2) = V0t1))))) & ( ! [V2t1:$i] : (mem(V2t1,A_27a) => ( ! [V3t2:$i] : (mem(V3t2,A_27a) => (ap(ap(ap(c_2Ebool_2ECOND(A_27a),inj__o(fo__c_2Ebool_2EF)),V2t1),V3t2) = V3t2))))))))).
tff(ax_thm_2Ecombin_2EK__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (c_2Ecombin_2EK(A_27a,A_27b) = f68(A_27a))))).
tff(ax_thm_2Ecombin_2ES__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: (c_2Ecombin_2ES(A_27a,A_27b,A_27c) = f71(A_27c,A_27b,A_27a)))))).
tff(ax_thm_2Ecombin_2EC__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: (c_2Ecombin_2EC(A_27a,A_27b,A_27c) = f74(A_27a,A_27c,A_27b)))))).
tff(ax_thm_2Ecombin_2Eo__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27c,A_27b)) => ( ! [V1g:$i] : (mem(V1g,arr(A_27a,A_27c)) => (ap(ap(c_2Ecombin_2Eo(A_27a,A_27b,A_27c),V0f),V1g) = f77(A_27b,A_27c,A_27a,V1g,V0f)))))))))).
tff(conj_thm_2Ecombin_2EI__THM,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => (ap(c_2Ecombin_2EI(A_27a),V0x) = V0x)))))).
tff(conj_thm_2Ecombin_2EI__o__ID,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27b)) => ((ap(ap(c_2Ecombin_2Eo(A_27a,A_27b,A_27b),c_2Ecombin_2EI(A_27b)),V0f) = V0f) & (ap(ap(c_2Ecombin_2Eo(A_27a,A_27b,A_27a),V0f),c_2Ecombin_2EI(A_27a)) = V0f)))))))).
tff(ax_thm_2Eextreal_2Eextreal__of__num__def,axiom,( ! [V0n:tp__ty_2Enum_2Enum] : (surj__ty_2Eextreal_2Eextreal(ap(c_2Eextreal_2Eextreal__of__num,inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Eextreal_2Eextreal(ap(c_2Eextreal_2ENormal,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(V0n))))))).
tff(conj_thm_2Eextreal_2Eextreal__add__def,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : ( ! [V2a:tp__ty_2Eextreal_2Eextreal] : ( ! [V3v2:tp__ty_2Erealax_2Ereal] : ( ! [V4v5:tp__ty_2Erealax_2Ereal] : ( ! [V5v3:tp__ty_2Erealax_2Ereal] : ((surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Eextreal_2Eextreal__add,ap(c_2Eextreal_2ENormal,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Eextreal_2ENormal,inj__ty_2Erealax_2Ereal(V1y)))) = surj__ty_2Eextreal_2Eextreal(ap(c_2Eextreal_2ENormal,ap(ap(c_2Erealax_2Ereal__add,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Erealax_2Ereal(V1y))))) & ((surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Eextreal_2Eextreal__add,inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2EPosInf)),inj__ty_2Eextreal_2Eextreal(V2a))) = fo__c_2Eextreal_2EPosInf) & ((surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Eextreal_2Eextreal__add,inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2ENegInf)),inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2EPosInf))) = fo__c_2Eextreal_2EPosInf) & ((surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Eextreal_2Eextreal__add,ap(c_2Eextreal_2ENormal,inj__ty_2Erealax_2Ereal(V3v2))),inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2EPosInf))) = fo__c_2Eextreal_2EPosInf) & ((surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Eextreal_2Eextreal__add,inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2ENegInf)),inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2ENegInf))) = fo__c_2Eextreal_2ENegInf) & ((surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Eextreal_2Eextreal__add,inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2ENegInf)),ap(c_2Eextreal_2ENormal,inj__ty_2Erealax_2Ereal(V4v5)))) = fo__c_2Eextreal_2ENegInf) & (surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Eextreal_2Eextreal__add,ap(c_2Eextreal_2ENormal,inj__ty_2Erealax_2Ereal(V5v3))),inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2ENegInf))) = fo__c_2Eextreal_2ENegInf))))))))))))))).
tff(conj_thm_2Eextreal_2Eextreal__le__def,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : ( ! [V2a:tp__ty_2Eextreal_2Eextreal] : ( ! [V3v2:tp__ty_2Erealax_2Ereal] : ( ! [V4v3:tp__ty_2Erealax_2Ereal] : ( ! [V5v5:tp__ty_2Erealax_2Ereal] : ((p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2ENormal,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Eextreal_2ENormal,inj__ty_2Erealax_2Ereal(V1y)))) <=> p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Erealax_2Ereal(V1y)))) & ((p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2ENegInf)),inj__ty_2Eextreal_2Eextreal(V2a))) <=> $true) & ((p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2EPosInf)),inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2EPosInf))) <=> $true) & ((p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2ENormal,inj__ty_2Erealax_2Ereal(V3v2))),inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2EPosInf))) <=> $true) & ((p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2EPosInf)),inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2ENegInf))) <=> $false) & ((p(ap(ap(c_2Eextreal_2Eextreal__le,ap(c_2Eextreal_2ENormal,inj__ty_2Erealax_2Ereal(V4v3))),inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2ENegInf))) <=> $false) & (p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2EPosInf)),ap(c_2Eextreal_2ENormal,inj__ty_2Erealax_2Ereal(V5v5)))) <=> $false))))))))))))))).
tff(ax_thm_2Eextreal_2Eextreal__lt__def,axiom,( ! [V0x:tp__ty_2Eextreal_2Eextreal] : ( ! [V1y:tp__ty_2Eextreal_2Eextreal] : (p(ap(ap(c_2Eextreal_2Eextreal__lt,inj__ty_2Eextreal_2Eextreal(V0x)),inj__ty_2Eextreal_2Eextreal(V1y))) <=> (~~ p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(V1y)),inj__ty_2Eextreal_2Eextreal(V0x)))))))).
tff(conj_thm_2Eextreal_2Eextreal__cases,lemma,(( ! [V0x:tp__ty_2Eextreal_2Eextreal] : ((V0x = fo__c_2Eextreal_2ENegInf) | ((V0x = fo__c_2Eextreal_2EPosInf) | (? [V1r:tp__ty_2Erealax_2Ereal] : (V0x = surj__ty_2Eextreal_2Eextreal(ap(c_2Eextreal_2ENormal,inj__ty_2Erealax_2Ereal(V1r)))))))))).
tff(conj_thm_2Eextreal_2Eextreal__not__infty,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ((~~ (surj__ty_2Eextreal_2Eextreal(ap(c_2Eextreal_2ENormal,inj__ty_2Erealax_2Ereal(V0x))) = fo__c_2Eextreal_2ENegInf)) & (~~ (surj__ty_2Eextreal_2Eextreal(ap(c_2Eextreal_2ENormal,inj__ty_2Erealax_2Ereal(V0x))) = fo__c_2Eextreal_2EPosInf)))))).
tff(conj_thm_2Eextreal_2Enum__not__infty,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ((~~ (surj__ty_2Eextreal_2Eextreal(ap(c_2Eextreal_2Eextreal__of__num,inj__ty_2Enum_2Enum(V0n))) = fo__c_2Eextreal_2ENegInf)) & (~~ (surj__ty_2Eextreal_2Eextreal(ap(c_2Eextreal_2Eextreal__of__num,inj__ty_2Enum_2Enum(V0n))) = fo__c_2Eextreal_2EPosInf)))))).
tff(conj_thm_2Eextreal_2Eextreal__lt__eq,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2ENormal,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Eextreal_2ENormal,inj__ty_2Erealax_2Ereal(V1y)))) <=> p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Erealax_2Ereal(V1y)))))))).
tff(conj_thm_2Eextreal_2Ele__infty,lemma,((( ! [V0x:tp__ty_2Eextreal_2Eextreal] : (p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2ENegInf)),inj__ty_2Eextreal_2Eextreal(V0x))) & p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(V0x)),inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2EPosInf))))) & (( ! [V1x:tp__ty_2Eextreal_2Eextreal] : (p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(V1x)),inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2ENegInf))) <=> (V1x = fo__c_2Eextreal_2ENegInf))) & ( ! [V2x:tp__ty_2Eextreal_2Eextreal] : (p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2EPosInf)),inj__ty_2Eextreal_2Eextreal(V2x))) <=> (V2x = fo__c_2Eextreal_2EPosInf))))))).
tff(conj_thm_2Eextreal_2Elt__infty,lemma,(( ! [V0x:tp__ty_2Eextreal_2Eextreal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Eextreal_2Eextreal__lt,inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2ENegInf)),ap(c_2Eextreal_2ENormal,inj__ty_2Erealax_2Ereal(V1y)))) & (p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(c_2Eextreal_2ENormal,inj__ty_2Erealax_2Ereal(V1y))),inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2EPosInf))) & (p(ap(ap(c_2Eextreal_2Eextreal__lt,inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2ENegInf)),inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2EPosInf))) & ((~~ p(ap(ap(c_2Eextreal_2Eextreal__lt,inj__ty_2Eextreal_2Eextreal(V0x)),inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2ENegInf)))) & ((~~ p(ap(ap(c_2Eextreal_2Eextreal__lt,inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2EPosInf)),inj__ty_2Eextreal_2Eextreal(V0x)))) & (((~~ (V0x = fo__c_2Eextreal_2EPosInf)) <=> p(ap(ap(c_2Eextreal_2Eextreal__lt,inj__ty_2Eextreal_2Eextreal(V0x)),inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2EPosInf)))) & ((~~ (V0x = fo__c_2Eextreal_2ENegInf)) <=> p(ap(ap(c_2Eextreal_2Eextreal__lt,inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2ENegInf)),inj__ty_2Eextreal_2Eextreal(V0x)))))))))))))).
tff(conj_thm_2Eextreal_2Elet__add2,lemma,(( ! [V0w:tp__ty_2Eextreal_2Eextreal] : ( ! [V1x:tp__ty_2Eextreal_2Eextreal] : ( ! [V2y:tp__ty_2Eextreal_2Eextreal] : ( ! [V3z:tp__ty_2Eextreal_2Eextreal] : (((~~ (V0w = fo__c_2Eextreal_2ENegInf)) & ((~~ (V0w = fo__c_2Eextreal_2EPosInf)) & (p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(V0w)),inj__ty_2Eextreal_2Eextreal(V1x))) & p(ap(ap(c_2Eextreal_2Eextreal__lt,inj__ty_2Eextreal_2Eextreal(V2y)),inj__ty_2Eextreal_2Eextreal(V3z)))))) => p(ap(ap(c_2Eextreal_2Eextreal__lt,ap(ap(c_2Eextreal_2Eextreal__add,inj__ty_2Eextreal_2Eextreal(V0w)),inj__ty_2Eextreal_2Eextreal(V2y))),ap(ap(c_2Eextreal_2Eextreal__add,inj__ty_2Eextreal_2Eextreal(V1x)),inj__ty_2Eextreal_2Eextreal(V3z))))))))))).
tff(conj_thm_2Eextreal_2Eadd__rzero,lemma,(( ! [V0x:tp__ty_2Eextreal_2Eextreal] : (surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Eextreal_2Eextreal__add,inj__ty_2Eextreal_2Eextreal(V0x)),ap(c_2Eextreal_2Eextreal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) = V0x)))).
tff(conj_thm_2Eextreal_2ESIMP__EXTREAL__ARCH,lemma,(( ! [V0x:tp__ty_2Eextreal_2Eextreal] : ((~~ (V0x = fo__c_2Eextreal_2EPosInf)) => (? [V1n:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(V0x)),ap(c_2Eextreal_2Eextreal__of__num,inj__ty_2Enum_2Enum(V1n))))))))).
tff(ax_thm_2Emeasure_2Ealgebra__def,axiom,( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => (p(ap(c_2Emeasure_2Ealgebra(A_27a),V0a)) <=> (p(ap(ap(c_2Emeasure_2Esubset__class(A_27a),ap(c_2Emeasure_2Espace(A_27a),V0a)),ap(c_2Emeasure_2Esubsets(A_27a),V0a))) & (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),c_2Epred__set_2EEMPTY(A_27a)),ap(c_2Emeasure_2Esubsets(A_27a),V0a))) & (( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V1s),ap(c_2Emeasure_2Esubsets(A_27a),V0a))) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(ap(c_2Epred__set_2EDIFF(A_27a),ap(c_2Emeasure_2Espace(A_27a),V0a)),V1s)),ap(c_2Emeasure_2Esubsets(A_27a),V0a)))))) & ( ! [V2s:$i] : (mem(V2s,arr(A_27a,bool)) => ( ! [V3t:$i] : (mem(V3t,arr(A_27a,bool)) => ((p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V2s),ap(c_2Emeasure_2Esubsets(A_27a),V0a))) & p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V3t),ap(c_2Emeasure_2Esubsets(A_27a),V0a)))) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(ap(c_2Epred__set_2EUNION(A_27a),V2s),V3t)),ap(c_2Emeasure_2Esubsets(A_27a),V0a)))))))))))))))).
tff(ax_thm_2Emeasure_2Esigma__algebra__def,axiom,( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => (p(ap(c_2Emeasure_2Esigma__algebra(A_27a),V0a)) <=> (p(ap(c_2Emeasure_2Ealgebra(A_27a),V0a)) & ( ! [V1c:$i] : (mem(V1c,arr(arr(A_27a,bool),bool)) => ((p(ap(c_2Epred__set_2Ecountable(arr(A_27a,bool)),V1c)) & p(ap(ap(c_2Epred__set_2ESUBSET(arr(A_27a,bool)),V1c),ap(c_2Emeasure_2Esubsets(A_27a),V0a)))) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(c_2Epred__set_2EBIGUNION(A_27a),V1c)),ap(c_2Emeasure_2Esubsets(A_27a),V0a)))))))))))).
tff(conj_thm_2Emeasure_2EALGEBRA__SPACE,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => (p(ap(c_2Emeasure_2Ealgebra(A_27a),V0a)) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(c_2Emeasure_2Espace(A_27a),V0a)),ap(c_2Emeasure_2Esubsets(A_27a),V0a))))))))).
tff(conj_thm_2Emeasure_2ESIGMA__ALGEBRA__ENUM,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => ( ! [V1f:$i] : (mem(V1f,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => ((p(ap(c_2Emeasure_2Esigma__algebra(A_27a),V0a)) & p(ap(ap(c_2Ebool_2EIN(arr(ty_2Enum_2Enum,arr(A_27a,bool))),V1f),ap(ap(c_2Epred__set_2EFUNSET(ty_2Enum_2Enum,arr(A_27a,bool)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),ap(c_2Emeasure_2Esubsets(A_27a),V0a))))) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(c_2Epred__set_2EBIGUNION(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,arr(A_27a,bool)),V1f),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)))),ap(c_2Emeasure_2Esubsets(A_27a),V0a))))))))))).
tff(conj_thm_2Emeasure_2ESIGMA__ALGEBRA__FN__BIGINTER,lemma,(( ! [A_27a:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => (p(ap(c_2Emeasure_2Esigma__algebra(A_27a),V0a)) => (p(ap(ap(c_2Emeasure_2Esubset__class(A_27a),ap(c_2Emeasure_2Espace(A_27a),V0a)),ap(c_2Emeasure_2Esubsets(A_27a),V0a))) & (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),c_2Epred__set_2EEMPTY(A_27a)),ap(c_2Emeasure_2Esubsets(A_27a),V0a))) & (( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),V1s),ap(c_2Emeasure_2Esubsets(A_27a),V0a))) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(ap(c_2Epred__set_2EDIFF(A_27a),ap(c_2Emeasure_2Espace(A_27a),V0a)),V1s)),ap(c_2Emeasure_2Esubsets(A_27a),V0a)))))) & ( ! [V2f:$i] : (mem(V2f,arr(ty_2Enum_2Enum,arr(A_27a,bool))) => (p(ap(ap(c_2Ebool_2EIN(arr(ty_2Enum_2Enum,arr(A_27a,bool))),V2f),ap(ap(c_2Epred__set_2EFUNSET(ty_2Enum_2Enum,arr(A_27a,bool)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),ap(c_2Emeasure_2Esubsets(A_27a),V0a)))) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(c_2Epred__set_2EBIGINTER(A_27a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,arr(A_27a,bool)),V2f),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)))),ap(c_2Emeasure_2Esubsets(A_27a),V0a))))))))))))))).
tff(conj_thm_2Emeasure_2EIN__MEASURABLE__BOREL,lemma,(( ! [A_27a:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V1a:$i] : (mem(V1a,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,ty_2Eextreal_2Eextreal)),V0f),ap(ap(c_2Emeasure_2Emeasurable(A_27a,ty_2Eextreal_2Eextreal),V1a),c_2Emeasure_2EBorel))) <=> (p(ap(c_2Emeasure_2Esigma__algebra(A_27a),V1a)) & (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,ty_2Eextreal_2Eextreal)),V0f),ap(ap(c_2Epred__set_2EFUNSET(A_27a,ty_2Eextreal_2Eextreal),ap(c_2Emeasure_2Espace(A_27a),V1a)),c_2Epred__set_2EUNIV(ty_2Eextreal_2Eextreal)))) & ( ! [V2c:tp__ty_2Eextreal_2Eextreal] : p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(ap(c_2Epred__set_2EINTER(A_27a),ap(c_2Epred__set_2EGSPEC(A_27a,A_27a),f3530(A_27a,V2c,V0f))),ap(c_2Emeasure_2Espace(A_27a),V1a))),ap(c_2Emeasure_2Esubsets(A_27a),V1a)))))))))))))).
tff(conj_thm_2Emeasure_2EIN__MEASURABLE__BOREL__NEGINF,lemma,(( ! [A_27a:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V1a:$i] : (mem(V1a,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,ty_2Eextreal_2Eextreal)),V0f),ap(ap(c_2Emeasure_2Emeasurable(A_27a,ty_2Eextreal_2Eextreal),V1a),c_2Emeasure_2EBorel))) => p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(ap(c_2Epred__set_2EINTER(A_27a),ap(c_2Epred__set_2EGSPEC(A_27a,A_27a),f3531(A_27a,V0f))),ap(c_2Emeasure_2Espace(A_27a),V1a))),ap(c_2Emeasure_2Esubsets(A_27a),V1a))))))))))).
tff(conj_thm_2Enumeral_2Enumeral__distrib,lemma,((( ! [V0n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n))) = V0n)) & (( ! [V1n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = V1n)) & (( ! [V2n:tp__ty_2Enum_2Enum] : ( ! [V3m:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V2n))),ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V3m)))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Enumeral_2EiZ,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V2n)),inj__ty_2Enum_2Enum(V3m)))))))) & (( ! [V4n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V4n))) = fo__c_2Enum_2E0)) & (( ! [V5n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V5n)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = fo__c_2Enum_2E0)) & (( ! [V6n:tp__ty_2Enum_2Enum] : ( ! [V7m:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V6n))),ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V7m)))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V6n)),inj__ty_2Enum_2Enum(V7m))))))) & (( ! [V8n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V8n))) = fo__c_2Enum_2E0)) & (( ! [V9n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V9n)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = V9n)) & (( ! [V10n:tp__ty_2Enum_2Enum] : ( ! [V11m:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V10n))),ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V11m)))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V10n)),inj__ty_2Enum_2Enum(V11m))))))) & (( ! [V12n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EEXP,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V12n))))) = fo__c_2Enum_2E0)) & (( ! [V13n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EEXP,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V13n))))) = fo__c_2Enum_2E0)) & (( ! [V14n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EEXP,inj__ty_2Enum_2Enum(V14n)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))) & (( ! [V15n:tp__ty_2Enum_2Enum] : ( ! [V16m:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EEXP,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V15n))),ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V16m)))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(ap(c_2Earithmetic_2EEXP,inj__ty_2Enum_2Enum(V15n)),inj__ty_2Enum_2Enum(V16m))))))) & ((surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) & (( ! [V17n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V17n)))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V17n)))))) & ((surj__ty_2Enum_2Enum(ap(c_2Eprim__rec_2EPRE,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = fo__c_2Enum_2E0) & (( ! [V18n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Eprim__rec_2EPRE,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V18n)))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Eprim__rec_2EPRE,inj__ty_2Enum_2Enum(V18n)))))) & (( ! [V19n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V19n))) = fo__c_2Enum_2E0) <=> (V19n = fo__c_2Earithmetic_2EZERO))) & (( ! [V20n:tp__ty_2Enum_2Enum] : ((fo__c_2Enum_2E0 = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V20n)))) <=> (V20n = fo__c_2Earithmetic_2EZERO))) & (( ! [V21n:tp__ty_2Enum_2Enum] : ( ! [V22m:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V21n))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V22m)))) <=> (V21n = V22m)))) & (( ! [V23n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V23n)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) <=> $false)) & (( ! [V24n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V24n)))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)),inj__ty_2Enum_2Enum(V24n))))) & (( ! [V25n:tp__ty_2Enum_2Enum] : ( ! [V26m:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V25n))),ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V26m)))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V25n)),inj__ty_2Enum_2Enum(V26m)))))) & (( ! [V27n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3E,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V27n))) <=> $false)) & (( ! [V28n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3E,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V28n))),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)),inj__ty_2Enum_2Enum(V28n))))) & (( ! [V29n:tp__ty_2Enum_2Enum] : ( ! [V30m:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3E,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V29n))),ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V30m)))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V30m)),inj__ty_2Enum_2Enum(V29n)))))) & (( ! [V31n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V31n))) <=> $true)) & (( ! [V32n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V32n))),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V32n)),inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) & (( ! [V33n:tp__ty_2Enum_2Enum] : ( ! [V34m:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V33n))),ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V34m)))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V33n)),inj__ty_2Enum_2Enum(V34m)))))) & (( ! [V35n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3E_3D,inj__ty_2Enum_2Enum(V35n)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) <=> $true)) & (( ! [V36n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3E_3D,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V36n))) <=> (V36n = fo__c_2Enum_2E0))) & (( ! [V37n:tp__ty_2Enum_2Enum] : ( ! [V38m:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3E_3D,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V37n))),ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V38m)))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V38m)),inj__ty_2Enum_2Enum(V37n)))))) & (( ! [V39n:tp__ty_2Enum_2Enum] : (p(ap(c_2Earithmetic_2EODD,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V39n)))) <=> p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(V39n))))) & (( ! [V40n:tp__ty_2Enum_2Enum] : (p(ap(c_2Earithmetic_2EEVEN,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V40n)))) <=> p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V40n))))) & ((~~ p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) & p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))))))))))))))))))))))))))))))))))).
tff(conj_thm_2Enumeral_2Enumeral__eq,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : (((fo__c_2Earithmetic_2EZERO = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n)))) <=> $false) & (((surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))) = fo__c_2Earithmetic_2EZERO) <=> $false) & (((fo__c_2Earithmetic_2EZERO = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n)))) <=> $false) & (((surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n))) = fo__c_2Earithmetic_2EZERO) <=> $false) & (((surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1m)))) <=> $false) & (((surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1m)))) <=> $false) & (((surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1m)))) <=> (V0n = V1m)) & ((surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1m)))) <=> (V0n = V1m))))))))))))).
tff(conj_thm_2Enumeral_2Enumeral__lt,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)),ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n)))) <=> $true) & ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)),ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n)))) <=> $true) & ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))) <=> $false) & ((p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1m)))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))) & ((p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1m)))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))) & ((p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1m)))) <=> (~~ p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1m)),inj__ty_2Enum_2Enum(V0n))))) & (p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1m)))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))))))))))))).
tff(conj_thm_2Enumeral_2Enumeral__lte,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)),inj__ty_2Enum_2Enum(V0n))) <=> $true) & ((p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))),inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))) <=> $false) & ((p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n))),inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))) <=> $false) & ((p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1m)))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))) & ((p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1m)))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))) & ((p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1m)))) <=> (~~ p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1m)),inj__ty_2Enum_2Enum(V0n))))) & (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1m)))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))))))))))))).
tff(conj_thm_2Epair_2ECLOSED__PAIR__EQ,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1y:$i] : (mem(V1y,A_27b) => ( ! [V2a:$i] : (mem(V2a,A_27a) => ( ! [V3b:$i] : (mem(V3b,A_27b) => ((ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V0x),V1y) = ap(ap(c_2Epair_2E_2C(A_27a,A_27b),V2a),V3b)) <=> ((V0x = V2a) & (V1y = V3b))))))))))))))).
tff(conj_thm_2Epred__set_2EEXTENSION,lemma,(( ! [A_27a:del]: ( ! [V0s:$i] : (mem(V0s,arr(A_27a,bool)) => ( ! [V1t:$i] : (mem(V1t,arr(A_27a,bool)) => ((V0s = V1t) <=> ( ! [V2x:$i] : (mem(V2x,A_27a) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V0s)) <=> p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V1t))))))))))))).
tff(ax_thm_2Epred__set_2EGSPECIFICATION,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27b,ty_2Epair_2Eprod(A_27a,bool))) => ( ! [V1v:$i] : (mem(V1v,A_27a) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V1v),ap(c_2Epred__set_2EGSPEC(A_27a,A_27b),V0f))) <=> (? [V2x:$i] : (mem(V2x,A_27b) & (ap(ap(c_2Epair_2E_2C(A_27a,bool),V1v),inj__o(fo__c_2Ebool_2ET)) = ap(V0f,V2x)))))))))))).
tff(conj_thm_2Epred__set_2EIN__UNIV,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => p(ap(ap(c_2Ebool_2EIN(A_27a),V0x),c_2Epred__set_2EUNIV(A_27a)))))))).
tff(conj_thm_2Epred__set_2EIN__INTER,lemma,(( ! [A_27a:del]: ( ! [V0s:$i] : (mem(V0s,arr(A_27a,bool)) => ( ! [V1t:$i] : (mem(V1t,arr(A_27a,bool)) => ( ! [V2x:$i] : (mem(V2x,A_27a) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),ap(ap(c_2Epred__set_2EINTER(A_27a),V0s),V1t))) <=> (p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V0s)) & p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V1t))))))))))))).
tff(conj_thm_2Epred__set_2EINTER__EMPTY,lemma,(( ! [A_27a:del]: (( ! [V0s:$i] : (mem(V0s,arr(A_27a,bool)) => (ap(ap(c_2Epred__set_2EINTER(A_27a),c_2Epred__set_2EEMPTY(A_27a)),V0s) = c_2Epred__set_2EEMPTY(A_27a)))) & ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => (ap(ap(c_2Epred__set_2EINTER(A_27a),V1s),c_2Epred__set_2EEMPTY(A_27a)) = c_2Epred__set_2EEMPTY(A_27a)))))))).
tff(conj_thm_2Epred__set_2EINTER__UNIV,lemma,(( ! [A_27a:del]: (( ! [V0s:$i] : (mem(V0s,arr(A_27a,bool)) => (ap(ap(c_2Epred__set_2EINTER(A_27a),c_2Epred__set_2EUNIV(A_27a)),V0s) = V0s))) & ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => (ap(ap(c_2Epred__set_2EINTER(A_27a),V1s),c_2Epred__set_2EUNIV(A_27a)) = V1s))))))).
tff(conj_thm_2Epred__set_2EIN__DIFF,lemma,(( ! [A_27a:del]: ( ! [V0s:$i] : (mem(V0s,arr(A_27a,bool)) => ( ! [V1t:$i] : (mem(V1t,arr(A_27a,bool)) => ( ! [V2x:$i] : (mem(V2x,A_27a) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),ap(ap(c_2Epred__set_2EDIFF(A_27a),V0s),V1t))) <=> (p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V0s)) & (~~ p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V1t)))))))))))))).
tff(conj_thm_2Epred__set_2EIN__FUNSET,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27b)) => ( ! [V1P:$i] : (mem(V1P,arr(A_27a,bool)) => ( ! [V2Q:$i] : (mem(V2Q,arr(A_27b,bool)) => (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,A_27b)),V0f),ap(ap(c_2Epred__set_2EFUNSET(A_27a,A_27b),V1P),V2Q))) <=> ( ! [V3x:$i] : (mem(V3x,A_27a) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V3x),V1P)) => p(ap(ap(c_2Ebool_2EIN(A_27b),ap(V0f,V3x)),V2Q)))))))))))))))).
tff(conj_thm_2Epred__set_2EIN__BIGUNION__IMAGE,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,arr(A_27b,bool))) => ( ! [V1s:$i] : (mem(V1s,arr(A_27a,bool)) => ( ! [V2y:$i] : (mem(V2y,A_27b) => (p(ap(ap(c_2Ebool_2EIN(A_27b),V2y),ap(c_2Epred__set_2EBIGUNION(A_27b),ap(ap(c_2Epred__set_2EIMAGE(A_27a,arr(A_27b,bool)),V0f),V1s)))) <=> (? [V3x:$i] : (mem(V3x,A_27a) & (p(ap(ap(c_2Ebool_2EIN(A_27a),V3x),V1s)) & p(ap(ap(c_2Ebool_2EIN(A_27b),V2y),ap(V0f,V3x))))))))))))))))).
tff(conj_thm_2Epred__set_2EIN__BIGINTER__IMAGE,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1f:$i] : (mem(V1f,arr(A_27b,arr(A_27a,bool))) => ( ! [V2s:$i] : (mem(V2s,arr(A_27b,bool)) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V0x),ap(c_2Epred__set_2EBIGINTER(A_27a),ap(ap(c_2Epred__set_2EIMAGE(A_27b,arr(A_27a,bool)),V1f),V2s)))) <=> ( ! [V3y:$i] : (mem(V3y,A_27b) => (p(ap(ap(c_2Ebool_2EIN(A_27b),V3y),V2s)) => p(ap(ap(c_2Ebool_2EIN(A_27a),V0x),ap(V1f,V3y))))))))))))))))).
tff(conj_thm_2Epred__set_2EGSPEC__F,lemma,(( ! [A_27a:del]: (ap(c_2Epred__set_2EGSPEC(A_27a,A_27a),f291(A_27a)) = c_2Epred__set_2EEMPTY(A_27a))))).
tff(conj_thm_2Epred__set_2EGSPEC__T,lemma,(( ! [A_27a:del]: (ap(c_2Epred__set_2EGSPEC(A_27a,A_27a),f292(A_27a)) = c_2Epred__set_2EUNIV(A_27a))))).
tff(conj_thm_2Ereal_2EREAL__ADD__COMM,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Erealax_2Ereal(V1y))) = surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,inj__ty_2Erealax_2Ereal(V1y)),inj__ty_2Erealax_2Ereal(V0x)))))))).
tff(conj_thm_2Ereal_2EREAL__LT__IADD,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : ( ! [V2z:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V1y)),inj__ty_2Erealax_2Ereal(V2z))) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Erealax_2Ereal__add,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Erealax_2Ereal(V1y))),ap(ap(c_2Erealax_2Ereal__add,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Erealax_2Ereal(V2z)))))))))).
tff(ax_thm_2Ereal_2Ereal__sub,axiom,( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(ap(c_2Ereal_2Ereal__sub,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Erealax_2Ereal(V1y))) = surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,inj__ty_2Erealax_2Ereal(V0x)),ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V1y)))))))).
tff(conj_thm_2Ereal_2EREAL__ADD__RID,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__add,inj__ty_2Erealax_2Ereal(V0x)),ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) = V0x)))).
tff(conj_thm_2Ereal_2EREAL__MUL__RZERO,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(ap(c_2Erealax_2Ereal__mul,inj__ty_2Erealax_2Ereal(V0x)),ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))).
tff(conj_thm_2Ereal_2EREAL__LT__IMP__LE,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Erealax_2Ereal(V1y))) => p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Erealax_2Ereal(V1y)))))))).
tff(conj_thm_2Ereal_2EREAL__LET__TRANS,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : ( ! [V2z:tp__ty_2Erealax_2Ereal] : ((p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Erealax_2Ereal(V1y))) & p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V1y)),inj__ty_2Erealax_2Ereal(V2z)))) => p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Erealax_2Ereal(V2z))))))))).
tff(conj_thm_2Ereal_2EREAL__NEG__0,lemma,((surj__ty_2Erealax_2Ereal(ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))).
tff(conj_thm_2Ereal_2EREAL__SUB__LT,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(ap(c_2Ereal_2Ereal__sub,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Erealax_2Ereal(V1y)))) <=> p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V1y)),inj__ty_2Erealax_2Ereal(V0x)))))))).
tff(conj_thm_2Ereal_2EREAL__LT,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(V0m))),ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(V1n)))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))))))).
tff(conj_thm_2Ereal_2EREAL__INJ,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(V0m))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(V1n)))) <=> (V0m = V1n)))))).
tff(conj_thm_2Ereal_2EREAL__LT__ADD__SUB,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : ( ! [V2z:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Erealax_2Ereal__add,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Erealax_2Ereal(V1y))),inj__ty_2Erealax_2Ereal(V2z))) <=> p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V0x)),ap(ap(c_2Ereal_2Ereal__sub,inj__ty_2Erealax_2Ereal(V2z)),inj__ty_2Erealax_2Ereal(V1y)))))))))).
tff(conj_thm_2Ereal_2EREAL__LT__NEG,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V0x))),ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V1y)))) <=> p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V1y)),inj__ty_2Erealax_2Ereal(V0x)))))))).
tff(conj_thm_2Ereal_2EREAL__SUB__RZERO,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(ap(c_2Ereal_2Ereal__sub,inj__ty_2Erealax_2Ereal(V0x)),ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) = V0x)))).
tff(ax_thm_2Ereal_2Eabs,axiom,( ! [V0x:tp__ty_2Erealax_2Ereal] : (surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Eabs,inj__ty_2Erealax_2Ereal(V0x))) = surj__ty_2Erealax_2Ereal(ap(ap(ap(c_2Ebool_2ECOND(ty_2Erealax_2Ereal),ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Erealax_2Ereal(V0x))),inj__ty_2Erealax_2Ereal(V0x)),ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V0x))))))).
tff(conj_thm_2Ereal_2EABS__REFL,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Eabs,inj__ty_2Erealax_2Ereal(V0x))) = V0x) <=> p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Erealax_2Ereal(V0x))))))).
tff(conj_thm_2Ereal_2EPOW__POS,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Erealax_2Ereal(V0x))) => ( ! [V1n:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(ap(c_2Ereal_2Epow,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Enum_2Enum(V1n))))))))).
tff(conj_thm_2Ereal_2EREAL__POW__LT,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Erealax_2Ereal(V0x))) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(ap(c_2Ereal_2Epow,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Enum_2Enum(V1n))))))))).
tff(conj_thm_2Ereal_2EREAL__HALF__BETWEEN,lemma,(((p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(ap(c_2Ereal_2E_2F,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) & p(ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Ereal_2E_2F,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) & (p(ap(ap(c_2Ereal_2Ereal__lte,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(ap(c_2Ereal_2E_2F,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) & p(ap(ap(c_2Ereal_2Ereal__lte,ap(ap(c_2Ereal_2E_2F,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))).
tff(conj_thm_2Ereal_2Epow__rat,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2a:tp__ty_2Enum_2Enum] : ( ! [V3y:tp__ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal(ap(ap(c_2Ereal_2Epow,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))) & ((surj__ty_2Erealax_2Ereal(ap(ap(c_2Ereal_2Epow,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1n))))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) & ((surj__ty_2Erealax_2Ereal(ap(ap(c_2Ereal_2Epow,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1n))))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) & ((surj__ty_2Erealax_2Ereal(ap(ap(c_2Ereal_2Epow,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V2a)))),ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V1n)))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,ap(ap(c_2Earithmetic_2EEXP,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V2a))),ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V1n)))))) & ((surj__ty_2Erealax_2Ereal(ap(ap(c_2Ereal_2Epow,ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V2a))))),ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V1n)))) = surj__ty_2Erealax_2Ereal(ap(ap(ap(ap(c_2Ebool_2ECOND(arr(ty_2Erealax_2Ereal,ty_2Erealax_2Ereal)),ap(c_2Earithmetic_2EODD,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V1n)))),c_2Erealax_2Ereal__neg),i(ty_2Erealax_2Ereal)),ap(c_2Ereal_2Ereal__of__num,ap(ap(c_2Earithmetic_2EEXP,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V2a))),ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V1n))))))) & (surj__ty_2Erealax_2Ereal(ap(ap(c_2Ereal_2Epow,ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Erealax_2Ereal(V3y))),inj__ty_2Enum_2Enum(V1n))) = surj__ty_2Erealax_2Ereal(ap(ap(c_2Ereal_2E_2F,ap(ap(c_2Ereal_2Epow,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Enum_2Enum(V1n))),ap(ap(c_2Ereal_2Epow,inj__ty_2Erealax_2Ereal(V3y)),inj__ty_2Enum_2Enum(V1n)))))))))))))))).
tff(conj_thm_2Ereal_2Eneg__rat,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : ((surj__ty_2Erealax_2Ereal(ap(c_2Erealax_2Ereal__neg,ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Erealax_2Ereal(V1y)))) = surj__ty_2Erealax_2Ereal(ap(ap(ap(c_2Ebool_2ECOND(ty_2Erealax_2Ereal),ap(ap(c_2Emin_2E_3D(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V1y)),ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))),ap(c_2Erealax_2Ereal__neg,ap(c_2Emarker_2Eunint(ty_2Erealax_2Ereal),ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Erealax_2Ereal(V1y))))),ap(ap(c_2Ereal_2E_2F,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V0x))),inj__ty_2Erealax_2Ereal(V1y))))) & (surj__ty_2Erealax_2Ereal(ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(V0x)),ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V1y)))) = surj__ty_2Erealax_2Ereal(ap(ap(ap(c_2Ebool_2ECOND(ty_2Erealax_2Ereal),ap(ap(c_2Emin_2E_3D(ty_2Erealax_2Ereal),inj__ty_2Erealax_2Ereal(V1y)),ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))),ap(c_2Emarker_2Eunint(ty_2Erealax_2Ereal),ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Erealax_2Ereal(V1y)))),ap(ap(c_2Ereal_2E_2F,ap(c_2Erealax_2Ereal__neg,inj__ty_2Erealax_2Ereal(V0x))),inj__ty_2Erealax_2Ereal(V1y)))))))))).
tff(conj_thm_2Ereal_2Eeq__ints,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : (((surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(V1m)))) <=> (V0n = V1m)) & (((surj__ty_2Erealax_2Ereal(ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(V0n)))) = surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(V1m)))) <=> ((V0n = fo__c_2Enum_2E0) & (V1m = fo__c_2Enum_2E0))) & (((surj__ty_2Erealax_2Ereal(ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Erealax_2Ereal(ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(V1m))))) <=> ((V0n = fo__c_2Enum_2E0) & (V1m = fo__c_2Enum_2E0))) & ((surj__ty_2Erealax_2Ereal(ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(V0n)))) = surj__ty_2Erealax_2Ereal(ap(c_2Erealax_2Ereal__neg,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(V1m))))) <=> (V0n = V1m))))))))).
tff(conj_thm_2Ereal_2Elt__ratr,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1u:tp__ty_2Erealax_2Ereal] : ( ! [V2m:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V0x)),ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(V1u)),ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(V2m))))) <=> p(ap(ap(ap(c_2Ebool_2ECOND(bool),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V2m)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(ap(c_2Erealax_2Ereal__lt,inj__ty_2Erealax_2Ereal(V0x)),ap(c_2Emarker_2Eunint(ty_2Erealax_2Ereal),ap(ap(c_2Ereal_2E_2F,inj__ty_2Erealax_2Ereal(V1u)),ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))),ap(ap(c_2Erealax_2Ereal__lt,ap(ap(c_2Erealax_2Ereal__mul,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(V2m))),inj__ty_2Erealax_2Ereal(V0x))),inj__ty_2Erealax_2Ereal(V1u)))))))))).
tff(conj_thm_2Esat_2ENOT__NOT,lemma,(( ! [V0t:tp__o] : ((~~ (~~ p(inj__o(V0t)))) <=> p(inj__o(V0t)))))).
tff(conj_thm_2Esat_2EAND__INV__IMP,lemma,(( ! [V0A:tp__o] : (p(inj__o(V0A)) => ((~~ p(inj__o(V0A))) => $false))))).
tff(conj_thm_2Esat_2EOR__DUAL2,lemma,(( ! [V0A:tp__o] : ( ! [V1B:tp__o] : (((~~ (p(inj__o(V0A)) | p(inj__o(V1B)))) => $false) <=> ((p(inj__o(V0A)) => $false) => ((~~ p(inj__o(V1B))) => $false))))))).
tff(conj_thm_2Esat_2EOR__DUAL3,lemma,(( ! [V0A:tp__o] : ( ! [V1B:tp__o] : (((~~ ((~~ p(inj__o(V0A))) | p(inj__o(V1B)))) => $false) <=> (p(inj__o(V0A)) => ((~~ p(inj__o(V1B))) => $false))))))).
tff(conj_thm_2Esat_2EAND__INV2,lemma,(( ! [V0A:tp__o] : (((~~ p(inj__o(V0A))) => $false) => ((p(inj__o(V0A)) => $false) => $false))))).
tff(conj_thm_2Esat_2Edc__eq,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ( ! [V2r:tp__o] : ((p(inj__o(V0p)) <=> (p(inj__o(V1q)) <=> p(inj__o(V2r)))) <=> ((p(inj__o(V0p)) | (p(inj__o(V1q)) | p(inj__o(V2r)))) & ((p(inj__o(V0p)) | ((~~ p(inj__o(V2r))) | (~~ p(inj__o(V1q))))) & ((p(inj__o(V1q)) | ((~~ p(inj__o(V2r))) | (~~ p(inj__o(V0p))))) & (p(inj__o(V2r)) | ((~~ p(inj__o(V1q))) | (~~ p(inj__o(V0p)))))))))))))).
tff(conj_thm_2Esat_2Edc__conj,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ( ! [V2r:tp__o] : ((p(inj__o(V0p)) <=> (p(inj__o(V1q)) & p(inj__o(V2r)))) <=> ((p(inj__o(V0p)) | ((~~ p(inj__o(V1q))) | (~~ p(inj__o(V2r))))) & ((p(inj__o(V1q)) | (~~ p(inj__o(V0p)))) & (p(inj__o(V2r)) | (~~ p(inj__o(V0p)))))))))))).
tff(conj_thm_2Esat_2Edc__disj,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ( ! [V2r:tp__o] : ((p(inj__o(V0p)) <=> (p(inj__o(V1q)) | p(inj__o(V2r)))) <=> ((p(inj__o(V0p)) | (~~ p(inj__o(V1q)))) & ((p(inj__o(V0p)) | (~~ p(inj__o(V2r)))) & (p(inj__o(V1q)) | (p(inj__o(V2r)) | (~~ p(inj__o(V0p))))))))))))).
tff(conj_thm_2Esat_2Edc__imp,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ( ! [V2r:tp__o] : ((p(inj__o(V0p)) <=> (p(inj__o(V1q)) => p(inj__o(V2r)))) <=> ((p(inj__o(V0p)) | p(inj__o(V1q))) & ((p(inj__o(V0p)) | (~~ p(inj__o(V2r)))) & ((~~ p(inj__o(V1q))) | (p(inj__o(V2r)) | (~~ p(inj__o(V0p))))))))))))).
tff(conj_thm_2Esat_2Edc__neg,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ((p(inj__o(V0p)) <=> (~~ p(inj__o(V1q)))) <=> ((p(inj__o(V0p)) | p(inj__o(V1q))) & ((~~ p(inj__o(V1q))) | (~~ p(inj__o(V0p)))))))))).
tff(conj_thm_2Esat_2Epth__ni1,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ((~~ (p(inj__o(V0p)) => p(inj__o(V1q)))) => p(inj__o(V0p))))))).
tff(conj_thm_2Esat_2Epth__ni2,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ((~~ (p(inj__o(V0p)) => p(inj__o(V1q)))) => (~~ p(inj__o(V1q)))))))).
tff(conj_thm_2Esat_2Epth__no1,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ((~~ (p(inj__o(V0p)) | p(inj__o(V1q)))) => (~~ p(inj__o(V0p)))))))).
tff(conj_thm_2Esat_2Epth__no2,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ((~~ (p(inj__o(V0p)) | p(inj__o(V1q)))) => (~~ p(inj__o(V1q)))))))).
tff(conj_thm_2Esat_2Epth__nn,lemma,(( ! [V0p:tp__o] : ((~~ (~~ p(inj__o(V0p)))) => p(inj__o(V0p)))))).
tff(conj_thm_2Eseq_2ESEQ,lemma,(( ! [V0x:$i] : (mem(V0x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ( ! [V1x0:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Eseq_2E_2D_2D_3E,V0x),inj__ty_2Erealax_2Ereal(V1x0))) <=> ( ! [V2e:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Erealax_2Ereal(V2e))) => (? [V3N:tp__ty_2Enum_2Enum] : ( ! [V4n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3E_3D,inj__ty_2Enum_2Enum(V4n)),inj__ty_2Enum_2Enum(V3N))) => p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Eabs,ap(ap(c_2Ereal_2Ereal__sub,ap(V0x,inj__ty_2Enum_2Enum(V4n))),inj__ty_2Erealax_2Ereal(V1x0)))),inj__ty_2Erealax_2Ereal(V2e)))))))))))))).
tff(conj_thm_2Eseq_2ESEQ__CONST,lemma,(( ! [V0k:tp__ty_2Erealax_2Ereal] : p(ap(ap(c_2Eseq_2E_2D_2D_3E,k(ty_2Enum_2Enum,inj__ty_2Erealax_2Ereal(V0k))),inj__ty_2Erealax_2Ereal(V0k)))))).
tff(conj_thm_2Eseq_2ESEQ__ADD,lemma,(( ! [V0x:$i] : (mem(V0x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ( ! [V1x0:tp__ty_2Erealax_2Ereal] : ( ! [V2y:$i] : (mem(V2y,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ( ! [V3y0:tp__ty_2Erealax_2Ereal] : ((p(ap(ap(c_2Eseq_2E_2D_2D_3E,V0x),inj__ty_2Erealax_2Ereal(V1x0))) & p(ap(ap(c_2Eseq_2E_2D_2D_3E,V2y),inj__ty_2Erealax_2Ereal(V3y0)))) => p(ap(ap(c_2Eseq_2E_2D_2D_3E,f2864(V0x,V2y)),ap(ap(c_2Erealax_2Ereal__add,inj__ty_2Erealax_2Ereal(V1x0)),inj__ty_2Erealax_2Ereal(V3y0))))))))))))).
tff(conj_thm_2Eseq_2ESEQ__SUB,lemma,(( ! [V0x:$i] : (mem(V0x,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ( ! [V1x0:tp__ty_2Erealax_2Ereal] : ( ! [V2y:$i] : (mem(V2y,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ( ! [V3y0:tp__ty_2Erealax_2Ereal] : ((p(ap(ap(c_2Eseq_2E_2D_2D_3E,V0x),inj__ty_2Erealax_2Ereal(V1x0))) & p(ap(ap(c_2Eseq_2E_2D_2D_3E,V2y),inj__ty_2Erealax_2Ereal(V3y0)))) => p(ap(ap(c_2Eseq_2E_2D_2D_3E,f2868(V0x,V2y)),ap(ap(c_2Ereal_2Ereal__sub,inj__ty_2Erealax_2Ereal(V1x0)),inj__ty_2Erealax_2Ereal(V3y0))))))))))))).
tff(conj_thm_2Eseq_2ESEQ__POWER,lemma,(( ! [V0c:tp__ty_2Erealax_2Ereal] : (p(ap(ap(c_2Erealax_2Ereal__lt,ap(c_2Ereal_2Eabs,inj__ty_2Erealax_2Ereal(V0c))),ap(c_2Ereal_2Ereal__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))) => p(ap(ap(c_2Eseq_2E_2D_2D_3E,f2878(V0c)),ap(c_2Ereal_2Ereal__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))).
tff(conj_thm_2Eseq_2ELE__SEQ__IMP__LE__LIM,lemma,(( ! [V0x:tp__ty_2Erealax_2Ereal] : ( ! [V1y:tp__ty_2Erealax_2Ereal] : ( ! [V2f:$i] : (mem(V2f,arr(ty_2Enum_2Enum,ty_2Erealax_2Ereal)) => ((( ! [V3n:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V0x)),ap(V2f,inj__ty_2Enum_2Enum(V3n))))) & p(ap(ap(c_2Eseq_2E_2D_2D_3E,V2f),inj__ty_2Erealax_2Ereal(V1y)))) => p(ap(ap(c_2Ereal_2Ereal__lte,inj__ty_2Erealax_2Ereal(V0x)),inj__ty_2Erealax_2Ereal(V1y)))))))))).
tff(conj_thm_2Emeasure_2EIN__MEASURABLE__BOREL__ALT2,conjecture,(( ! [A_27a:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,ty_2Eextreal_2Eextreal)) => ( ! [V1a:$i] : (mem(V1a,ty_2Epair_2Eprod(arr(A_27a,bool),arr(arr(A_27a,bool),bool))) => (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,ty_2Eextreal_2Eextreal)),V0f),ap(ap(c_2Emeasure_2Emeasurable(A_27a,ty_2Eextreal_2Eextreal),V1a),c_2Emeasure_2EBorel))) <=> (p(ap(c_2Emeasure_2Esigma__algebra(A_27a),V1a)) & (p(ap(ap(c_2Ebool_2EIN(arr(A_27a,ty_2Eextreal_2Eextreal)),V0f),ap(ap(c_2Epred__set_2EFUNSET(A_27a,ty_2Eextreal_2Eextreal),ap(c_2Emeasure_2Espace(A_27a),V1a)),c_2Epred__set_2EUNIV(ty_2Eextreal_2Eextreal)))) & ( ! [V2c:tp__ty_2Eextreal_2Eextreal] : p(ap(ap(c_2Ebool_2EIN(arr(A_27a,bool)),ap(ap(c_2Epred__set_2EINTER(A_27a),ap(c_2Epred__set_2EGSPEC(A_27a,A_27a),f3533(A_27a,V2c,V0f))),ap(c_2Emeasure_2Espace(A_27a),V1a))),ap(c_2Emeasure_2Esubsets(A_27a),V1a)))))))))))))).
