include('Axioms/quote_2.ax').
tff(tp_ty_2Einteger_2Eint,type,( ty_2Einteger_2Eint: del )).
tff(stp_ty_2Einteger_2Eint,type,(tp__ty_2Einteger_2Eint : $tType)).
tff(stp_inj_ty_2Einteger_2Eint,type,(inj__ty_2Einteger_2Eint : tp__ty_2Einteger_2Eint > $i)).
tff(stp_surj_ty_2Einteger_2Eint,type,(surj__ty_2Einteger_2Eint : $i > tp__ty_2Einteger_2Eint)).
tff(stp_inj_surj_ty_2Einteger_2Eint,axiom,( ! [X:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(inj__ty_2Einteger_2Eint(X)) = X))).
tff(stp_inj_mem_ty_2Einteger_2Eint,axiom,( ! [X:tp__ty_2Einteger_2Eint] : (mem(inj__ty_2Einteger_2Eint(X),ty_2Einteger_2Eint)))).
tff(stp_iso_mem_ty_2Einteger_2Eint,axiom,( ! [X:$i] : (mem(X,ty_2Einteger_2Eint) => (X = inj__ty_2Einteger_2Eint(surj__ty_2Einteger_2Eint(X)))))).
tff(tp_c_2Einteger_2EABS,type,(c_2Einteger_2EABS:$i)).
tff(mem_c_2Einteger_2EABS,axiom,mem(c_2Einteger_2EABS,arr(ty_2Einteger_2Eint,ty_2Einteger_2Eint))).
tff(stp_fo_c_2Einteger_2EABS,type,(fo__c_2Einteger_2EABS:(tp__ty_2Einteger_2Eint) > tp__ty_2Einteger_2Eint)).
tff(stp_eq_fo_c_2Einteger_2EABS,axiom,( ! [X0:tp__ty_2Einteger_2Eint] : (inj__ty_2Einteger_2Eint(fo__c_2Einteger_2EABS(X0)) = ap(c_2Einteger_2EABS,inj__ty_2Einteger_2Eint(X0))))).
tff(tp_c_2Einteger_2ELEAST__INT,type,(c_2Einteger_2ELEAST__INT:$i)).
tff(mem_c_2Einteger_2ELEAST__INT,axiom,mem(c_2Einteger_2ELEAST__INT,arr(arr(ty_2Einteger_2Eint,bool),ty_2Einteger_2Eint))).
tff(tp_c_2Einteger_2ENum,type,(c_2Einteger_2ENum:$i)).
tff(mem_c_2Einteger_2ENum,axiom,mem(c_2Einteger_2ENum,arr(ty_2Einteger_2Eint,ty_2Enum_2Enum))).
tff(stp_fo_c_2Einteger_2ENum,type,(fo__c_2Einteger_2ENum:(tp__ty_2Einteger_2Eint) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Einteger_2ENum,axiom,( ! [X0:tp__ty_2Einteger_2Eint] : (inj__ty_2Enum_2Enum(fo__c_2Einteger_2ENum(X0)) = ap(c_2Einteger_2ENum,inj__ty_2Einteger_2Eint(X0))))).
tff(tp_c_2Einteger_2Eint__0,type,(c_2Einteger_2Eint__0:$i)).
tff(mem_c_2Einteger_2Eint__0,axiom,mem(c_2Einteger_2Eint__0,ty_2Einteger_2Eint)).
tff(stp_fo_c_2Einteger_2Eint__0,type,(fo__c_2Einteger_2Eint__0:tp__ty_2Einteger_2Eint)).
tff(stp_eq_fo_c_2Einteger_2Eint__0,axiom,(inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__0) = c_2Einteger_2Eint__0)).
tff(tp_c_2Einteger_2Eint__1,type,(c_2Einteger_2Eint__1:$i)).
tff(mem_c_2Einteger_2Eint__1,axiom,mem(c_2Einteger_2Eint__1,ty_2Einteger_2Eint)).
tff(stp_fo_c_2Einteger_2Eint__1,type,(fo__c_2Einteger_2Eint__1:tp__ty_2Einteger_2Eint)).
tff(stp_eq_fo_c_2Einteger_2Eint__1,axiom,(inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__1) = c_2Einteger_2Eint__1)).
tff(tp_c_2Einteger_2Eint__ABS,type,(c_2Einteger_2Eint__ABS:$i)).
tff(mem_c_2Einteger_2Eint__ABS,axiom,mem(c_2Einteger_2Eint__ABS,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Einteger_2Eint))).
tff(stp_fo_c_2Einteger_2Eint__ABS,type,(fo__c_2Einteger_2Eint__ABS:(tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum) > tp__ty_2Einteger_2Eint)).
tff(stp_eq_fo_c_2Einteger_2Eint__ABS,axiom,( ! [X0:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : (inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__ABS(X0)) = ap(c_2Einteger_2Eint__ABS,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(X0))))).
tff(tp_c_2Einteger_2Eint__ABS__CLASS,type,(c_2Einteger_2Eint__ABS__CLASS:$i)).
tff(mem_c_2Einteger_2Eint__ABS__CLASS,axiom,mem(c_2Einteger_2Eint__ABS__CLASS,arr(arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),bool),ty_2Einteger_2Eint))).
tff(tp_c_2Einteger_2Eint__REP,type,(c_2Einteger_2Eint__REP:$i)).
tff(mem_c_2Einteger_2Eint__REP,axiom,mem(c_2Einteger_2Eint__REP,arr(ty_2Einteger_2Eint,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)))).
tff(tp_c_2Einteger_2Eint__REP__CLASS,type,(c_2Einteger_2Eint__REP__CLASS:$i)).
tff(mem_c_2Einteger_2Eint__REP__CLASS,axiom,mem(c_2Einteger_2Eint__REP__CLASS,arr(ty_2Einteger_2Eint,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),bool)))).
tff(stp_fo_c_2Einteger_2Eint__REP__CLASS,type,(fo__c_2Einteger_2Eint__REP__CLASS:(tp__ty_2Einteger_2Eint * tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum) > tp__o)).
tff(stp_eq_fo_c_2Einteger_2Eint__REP__CLASS,axiom,( ! [X0:tp__ty_2Einteger_2Eint] : ( ! [X1:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : (inj__o(fo__c_2Einteger_2Eint__REP__CLASS(X0,X1)) = ap(ap(c_2Einteger_2Eint__REP__CLASS,inj__ty_2Einteger_2Eint(X0)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Einteger_2Eint__add,type,(c_2Einteger_2Eint__add:$i)).
tff(mem_c_2Einteger_2Eint__add,axiom,mem(c_2Einteger_2Eint__add,arr(ty_2Einteger_2Eint,arr(ty_2Einteger_2Eint,ty_2Einteger_2Eint)))).
tff(stp_fo_c_2Einteger_2Eint__add,type,(fo__c_2Einteger_2Eint__add:(tp__ty_2Einteger_2Eint * tp__ty_2Einteger_2Eint) > tp__ty_2Einteger_2Eint)).
tff(stp_eq_fo_c_2Einteger_2Eint__add,axiom,( ! [X0:tp__ty_2Einteger_2Eint] : ( ! [X1:tp__ty_2Einteger_2Eint] : (inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__add(X0,X1)) = ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X1)))))).
tff(tp_c_2Einteger_2Eint__div,type,(c_2Einteger_2Eint__div:$i)).
tff(mem_c_2Einteger_2Eint__div,axiom,mem(c_2Einteger_2Eint__div,arr(ty_2Einteger_2Eint,arr(ty_2Einteger_2Eint,ty_2Einteger_2Eint)))).
tff(stp_fo_c_2Einteger_2Eint__div,type,(fo__c_2Einteger_2Eint__div:(tp__ty_2Einteger_2Eint * tp__ty_2Einteger_2Eint) > tp__ty_2Einteger_2Eint)).
tff(stp_eq_fo_c_2Einteger_2Eint__div,axiom,( ! [X0:tp__ty_2Einteger_2Eint] : ( ! [X1:tp__ty_2Einteger_2Eint] : (inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__div(X0,X1)) = ap(ap(c_2Einteger_2Eint__div,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X1)))))).
tff(tp_c_2Einteger_2Eint__divides,type,(c_2Einteger_2Eint__divides:$i)).
tff(mem_c_2Einteger_2Eint__divides,axiom,mem(c_2Einteger_2Eint__divides,arr(ty_2Einteger_2Eint,arr(ty_2Einteger_2Eint,bool)))).
tff(stp_fo_c_2Einteger_2Eint__divides,type,(fo__c_2Einteger_2Eint__divides:(tp__ty_2Einteger_2Eint * tp__ty_2Einteger_2Eint) > tp__o)).
tff(stp_eq_fo_c_2Einteger_2Eint__divides,axiom,( ! [X0:tp__ty_2Einteger_2Eint] : ( ! [X1:tp__ty_2Einteger_2Eint] : (inj__o(fo__c_2Einteger_2Eint__divides(X0,X1)) = ap(ap(c_2Einteger_2Eint__divides,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X1)))))).
tff(tp_c_2Einteger_2Eint__exp,type,(c_2Einteger_2Eint__exp:$i)).
tff(mem_c_2Einteger_2Eint__exp,axiom,mem(c_2Einteger_2Eint__exp,arr(ty_2Einteger_2Eint,arr(ty_2Enum_2Enum,ty_2Einteger_2Eint)))).
tff(stp_fo_c_2Einteger_2Eint__exp,type,(fo__c_2Einteger_2Eint__exp:(tp__ty_2Einteger_2Eint * tp__ty_2Enum_2Enum) > tp__ty_2Einteger_2Eint)).
tff(stp_eq_fo_c_2Einteger_2Eint__exp,axiom,( ! [X0:tp__ty_2Einteger_2Eint] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__exp(X0,X1)) = ap(ap(c_2Einteger_2Eint__exp,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Einteger_2Eint__ge,type,(c_2Einteger_2Eint__ge:$i)).
tff(mem_c_2Einteger_2Eint__ge,axiom,mem(c_2Einteger_2Eint__ge,arr(ty_2Einteger_2Eint,arr(ty_2Einteger_2Eint,bool)))).
tff(stp_fo_c_2Einteger_2Eint__ge,type,(fo__c_2Einteger_2Eint__ge:(tp__ty_2Einteger_2Eint * tp__ty_2Einteger_2Eint) > tp__o)).
tff(stp_eq_fo_c_2Einteger_2Eint__ge,axiom,( ! [X0:tp__ty_2Einteger_2Eint] : ( ! [X1:tp__ty_2Einteger_2Eint] : (inj__o(fo__c_2Einteger_2Eint__ge(X0,X1)) = ap(ap(c_2Einteger_2Eint__ge,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X1)))))).
tff(tp_c_2Einteger_2Eint__gt,type,(c_2Einteger_2Eint__gt:$i)).
tff(mem_c_2Einteger_2Eint__gt,axiom,mem(c_2Einteger_2Eint__gt,arr(ty_2Einteger_2Eint,arr(ty_2Einteger_2Eint,bool)))).
tff(stp_fo_c_2Einteger_2Eint__gt,type,(fo__c_2Einteger_2Eint__gt:(tp__ty_2Einteger_2Eint * tp__ty_2Einteger_2Eint) > tp__o)).
tff(stp_eq_fo_c_2Einteger_2Eint__gt,axiom,( ! [X0:tp__ty_2Einteger_2Eint] : ( ! [X1:tp__ty_2Einteger_2Eint] : (inj__o(fo__c_2Einteger_2Eint__gt(X0,X1)) = ap(ap(c_2Einteger_2Eint__gt,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X1)))))).
tff(tp_c_2Einteger_2Eint__le,type,(c_2Einteger_2Eint__le:$i)).
tff(mem_c_2Einteger_2Eint__le,axiom,mem(c_2Einteger_2Eint__le,arr(ty_2Einteger_2Eint,arr(ty_2Einteger_2Eint,bool)))).
tff(stp_fo_c_2Einteger_2Eint__le,type,(fo__c_2Einteger_2Eint__le:(tp__ty_2Einteger_2Eint * tp__ty_2Einteger_2Eint) > tp__o)).
tff(stp_eq_fo_c_2Einteger_2Eint__le,axiom,( ! [X0:tp__ty_2Einteger_2Eint] : ( ! [X1:tp__ty_2Einteger_2Eint] : (inj__o(fo__c_2Einteger_2Eint__le(X0,X1)) = ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X1)))))).
tff(tp_c_2Einteger_2Eint__lt,type,(c_2Einteger_2Eint__lt:$i)).
tff(mem_c_2Einteger_2Eint__lt,axiom,mem(c_2Einteger_2Eint__lt,arr(ty_2Einteger_2Eint,arr(ty_2Einteger_2Eint,bool)))).
tff(stp_fo_c_2Einteger_2Eint__lt,type,(fo__c_2Einteger_2Eint__lt:(tp__ty_2Einteger_2Eint * tp__ty_2Einteger_2Eint) > tp__o)).
tff(stp_eq_fo_c_2Einteger_2Eint__lt,axiom,( ! [X0:tp__ty_2Einteger_2Eint] : ( ! [X1:tp__ty_2Einteger_2Eint] : (inj__o(fo__c_2Einteger_2Eint__lt(X0,X1)) = ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X1)))))).
tff(tp_c_2Einteger_2Eint__max,type,(c_2Einteger_2Eint__max:$i)).
tff(mem_c_2Einteger_2Eint__max,axiom,mem(c_2Einteger_2Eint__max,arr(ty_2Einteger_2Eint,arr(ty_2Einteger_2Eint,ty_2Einteger_2Eint)))).
tff(stp_fo_c_2Einteger_2Eint__max,type,(fo__c_2Einteger_2Eint__max:(tp__ty_2Einteger_2Eint * tp__ty_2Einteger_2Eint) > tp__ty_2Einteger_2Eint)).
tff(stp_eq_fo_c_2Einteger_2Eint__max,axiom,( ! [X0:tp__ty_2Einteger_2Eint] : ( ! [X1:tp__ty_2Einteger_2Eint] : (inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__max(X0,X1)) = ap(ap(c_2Einteger_2Eint__max,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X1)))))).
tff(tp_c_2Einteger_2Eint__min,type,(c_2Einteger_2Eint__min:$i)).
tff(mem_c_2Einteger_2Eint__min,axiom,mem(c_2Einteger_2Eint__min,arr(ty_2Einteger_2Eint,arr(ty_2Einteger_2Eint,ty_2Einteger_2Eint)))).
tff(stp_fo_c_2Einteger_2Eint__min,type,(fo__c_2Einteger_2Eint__min:(tp__ty_2Einteger_2Eint * tp__ty_2Einteger_2Eint) > tp__ty_2Einteger_2Eint)).
tff(stp_eq_fo_c_2Einteger_2Eint__min,axiom,( ! [X0:tp__ty_2Einteger_2Eint] : ( ! [X1:tp__ty_2Einteger_2Eint] : (inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__min(X0,X1)) = ap(ap(c_2Einteger_2Eint__min,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X1)))))).
tff(tp_c_2Einteger_2Eint__mod,type,(c_2Einteger_2Eint__mod:$i)).
tff(mem_c_2Einteger_2Eint__mod,axiom,mem(c_2Einteger_2Eint__mod,arr(ty_2Einteger_2Eint,arr(ty_2Einteger_2Eint,ty_2Einteger_2Eint)))).
tff(stp_fo_c_2Einteger_2Eint__mod,type,(fo__c_2Einteger_2Eint__mod:(tp__ty_2Einteger_2Eint * tp__ty_2Einteger_2Eint) > tp__ty_2Einteger_2Eint)).
tff(stp_eq_fo_c_2Einteger_2Eint__mod,axiom,( ! [X0:tp__ty_2Einteger_2Eint] : ( ! [X1:tp__ty_2Einteger_2Eint] : (inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__mod(X0,X1)) = ap(ap(c_2Einteger_2Eint__mod,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X1)))))).
tff(tp_c_2Einteger_2Eint__mul,type,(c_2Einteger_2Eint__mul:$i)).
tff(mem_c_2Einteger_2Eint__mul,axiom,mem(c_2Einteger_2Eint__mul,arr(ty_2Einteger_2Eint,arr(ty_2Einteger_2Eint,ty_2Einteger_2Eint)))).
tff(stp_fo_c_2Einteger_2Eint__mul,type,(fo__c_2Einteger_2Eint__mul:(tp__ty_2Einteger_2Eint * tp__ty_2Einteger_2Eint) > tp__ty_2Einteger_2Eint)).
tff(stp_eq_fo_c_2Einteger_2Eint__mul,axiom,( ! [X0:tp__ty_2Einteger_2Eint] : ( ! [X1:tp__ty_2Einteger_2Eint] : (inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__mul(X0,X1)) = ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X1)))))).
tff(tp_c_2Einteger_2Eint__neg,type,(c_2Einteger_2Eint__neg:$i)).
tff(mem_c_2Einteger_2Eint__neg,axiom,mem(c_2Einteger_2Eint__neg,arr(ty_2Einteger_2Eint,ty_2Einteger_2Eint))).
tff(stp_fo_c_2Einteger_2Eint__neg,type,(fo__c_2Einteger_2Eint__neg:(tp__ty_2Einteger_2Eint) > tp__ty_2Einteger_2Eint)).
tff(stp_eq_fo_c_2Einteger_2Eint__neg,axiom,( ! [X0:tp__ty_2Einteger_2Eint] : (inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__neg(X0)) = ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(X0))))).
tff(tp_c_2Einteger_2Eint__of__num,type,(c_2Einteger_2Eint__of__num:$i)).
tff(mem_c_2Einteger_2Eint__of__num,axiom,mem(c_2Einteger_2Eint__of__num,arr(ty_2Enum_2Enum,ty_2Einteger_2Eint))).
tff(stp_fo_c_2Einteger_2Eint__of__num,type,(fo__c_2Einteger_2Eint__of__num:(tp__ty_2Enum_2Enum) > tp__ty_2Einteger_2Eint)).
tff(stp_eq_fo_c_2Einteger_2Eint__of__num,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__of__num(X0)) = ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Einteger_2Eint__quot,type,(c_2Einteger_2Eint__quot:$i)).
tff(mem_c_2Einteger_2Eint__quot,axiom,mem(c_2Einteger_2Eint__quot,arr(ty_2Einteger_2Eint,arr(ty_2Einteger_2Eint,ty_2Einteger_2Eint)))).
tff(stp_fo_c_2Einteger_2Eint__quot,type,(fo__c_2Einteger_2Eint__quot:(tp__ty_2Einteger_2Eint * tp__ty_2Einteger_2Eint) > tp__ty_2Einteger_2Eint)).
tff(stp_eq_fo_c_2Einteger_2Eint__quot,axiom,( ! [X0:tp__ty_2Einteger_2Eint] : ( ! [X1:tp__ty_2Einteger_2Eint] : (inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__quot(X0,X1)) = ap(ap(c_2Einteger_2Eint__quot,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X1)))))).
tff(tp_c_2Einteger_2Eint__rem,type,(c_2Einteger_2Eint__rem:$i)).
tff(mem_c_2Einteger_2Eint__rem,axiom,mem(c_2Einteger_2Eint__rem,arr(ty_2Einteger_2Eint,arr(ty_2Einteger_2Eint,ty_2Einteger_2Eint)))).
tff(stp_fo_c_2Einteger_2Eint__rem,type,(fo__c_2Einteger_2Eint__rem:(tp__ty_2Einteger_2Eint * tp__ty_2Einteger_2Eint) > tp__ty_2Einteger_2Eint)).
tff(stp_eq_fo_c_2Einteger_2Eint__rem,axiom,( ! [X0:tp__ty_2Einteger_2Eint] : ( ! [X1:tp__ty_2Einteger_2Eint] : (inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__rem(X0,X1)) = ap(ap(c_2Einteger_2Eint__rem,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X1)))))).
tff(tp_c_2Einteger_2Eint__sub,type,(c_2Einteger_2Eint__sub:$i)).
tff(mem_c_2Einteger_2Eint__sub,axiom,mem(c_2Einteger_2Eint__sub,arr(ty_2Einteger_2Eint,arr(ty_2Einteger_2Eint,ty_2Einteger_2Eint)))).
tff(stp_fo_c_2Einteger_2Eint__sub,type,(fo__c_2Einteger_2Eint__sub:(tp__ty_2Einteger_2Eint * tp__ty_2Einteger_2Eint) > tp__ty_2Einteger_2Eint)).
tff(stp_eq_fo_c_2Einteger_2Eint__sub,axiom,( ! [X0:tp__ty_2Einteger_2Eint] : ( ! [X1:tp__ty_2Einteger_2Eint] : (inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__sub(X0,X1)) = ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Einteger_2Eint(X1)))))).
tff(tp_c_2Einteger_2Etint__0,type,(c_2Einteger_2Etint__0:$i)).
tff(mem_c_2Einteger_2Etint__0,axiom,mem(c_2Einteger_2Etint__0,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))).
tff(tp_c_2Einteger_2Etint__1,type,(c_2Einteger_2Etint__1:$i)).
tff(mem_c_2Einteger_2Etint__1,axiom,mem(c_2Einteger_2Etint__1,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))).
tff(tp_c_2Einteger_2Etint__add,type,(c_2Einteger_2Etint__add:$i)).
tff(mem_c_2Einteger_2Etint__add,axiom,mem(c_2Einteger_2Etint__add,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))))).
tff(tp_c_2Einteger_2Etint__eq,type,(c_2Einteger_2Etint__eq:$i)).
tff(mem_c_2Einteger_2Etint__eq,axiom,mem(c_2Einteger_2Etint__eq,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),bool)))).
tff(stp_fo_c_2Einteger_2Etint__eq,type,(fo__c_2Einteger_2Etint__eq:(tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum * tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum) > tp__o)).
tff(stp_eq_fo_c_2Einteger_2Etint__eq,axiom,( ! [X0:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [X1:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : (inj__o(fo__c_2Einteger_2Etint__eq(X0,X1)) = ap(ap(c_2Einteger_2Etint__eq,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(X0)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Einteger_2Etint__lt,type,(c_2Einteger_2Etint__lt:$i)).
tff(mem_c_2Einteger_2Etint__lt,axiom,mem(c_2Einteger_2Etint__lt,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),bool)))).
tff(stp_fo_c_2Einteger_2Etint__lt,type,(fo__c_2Einteger_2Etint__lt:(tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum * tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum) > tp__o)).
tff(stp_eq_fo_c_2Einteger_2Etint__lt,axiom,( ! [X0:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [X1:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : (inj__o(fo__c_2Einteger_2Etint__lt(X0,X1)) = ap(ap(c_2Einteger_2Etint__lt,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(X0)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Einteger_2Etint__mul,type,(c_2Einteger_2Etint__mul:$i)).
tff(mem_c_2Einteger_2Etint__mul,axiom,mem(c_2Einteger_2Etint__mul,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))))).
tff(tp_c_2Einteger_2Etint__neg,type,(c_2Einteger_2Etint__neg:$i)).
tff(mem_c_2Einteger_2Etint__neg,axiom,mem(c_2Einteger_2Etint__neg,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)))).
tff(tp_c_2Einteger_2Etint__of__num,type,(c_2Einteger_2Etint__of__num:$i)).
tff(mem_c_2Einteger_2Etint__of__num,axiom,mem(c_2Einteger_2Etint__of__num,arr(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)))).
tff(conj_thm_2Einteger_2EEQ__LADD,lemma,(( ! [V0x:tp__ty_2Enum_2Enum] : ( ! [V1y:tp__ty_2Enum_2Enum] : ( ! [V2z:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V1y))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V2z)))) <=> (V1y = V2z))))))).
tff(conj_thm_2Einteger_2EEQ__ADDL,lemma,(( ! [V0x:tp__ty_2Enum_2Enum] : ( ! [V1y:tp__ty_2Enum_2Enum] : ((V0x = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V1y)))) <=> (V1y = fo__c_2Enum_2E0)))))).
tff(conj_thm_2Einteger_2ELT__LADD,lemma,(( ! [V0x:tp__ty_2Enum_2Enum] : ( ! [V1y:tp__ty_2Enum_2Enum] : ( ! [V2z:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V1y))),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V2z)))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1y)),inj__ty_2Enum_2Enum(V2z))))))))).
tff(conj_thm_2Einteger_2ELT__ADDL,lemma,(( ! [V0x:tp__ty_2Enum_2Enum] : ( ! [V1y:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0x)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V1y)))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V1y)))))))).
tff(conj_thm_2Einteger_2ELT__ADDR,lemma,(( ! [V0x:tp__ty_2Enum_2Enum] : ( ! [V1y:tp__ty_2Enum_2Enum] : (~~ p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V1y))),inj__ty_2Enum_2Enum(V0x)))))))).
tff(conj_thm_2Einteger_2ELT__ADD2,lemma,(( ! [V0x1:tp__ty_2Enum_2Enum] : ( ! [V1x2:tp__ty_2Enum_2Enum] : ( ! [V2y1:tp__ty_2Enum_2Enum] : ( ! [V3y2:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0x1)),inj__ty_2Enum_2Enum(V2y1))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1x2)),inj__ty_2Enum_2Enum(V3y2)))) => p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0x1)),inj__ty_2Enum_2Enum(V1x2))),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V2y1)),inj__ty_2Enum_2Enum(V3y2))))))))))).
tff(ax_thm_2Einteger_2Etint__0,axiom,(surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(c_2Einteger_2Etint__0) = surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))).
tff(ax_thm_2Einteger_2Etint__1,axiom,(surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(c_2Einteger_2Etint__1) = surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,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)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))).
tff(ax_thm_2Einteger_2Etint__neg,axiom,( ! [V0x:tp__ty_2Enum_2Enum] : ( ! [V1y:tp__ty_2Enum_2Enum] : (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(ap(c_2Einteger_2Etint__neg,ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V1y)))) = surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V1y)),inj__ty_2Enum_2Enum(V0x))))))).
tff(ax_thm_2Einteger_2Etint__add,axiom,( ! [V0x1:tp__ty_2Enum_2Enum] : ( ! [V1y1:tp__ty_2Enum_2Enum] : ( ! [V2x2:tp__ty_2Enum_2Enum] : ( ! [V3y2:tp__ty_2Enum_2Enum] : (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(ap(ap(c_2Einteger_2Etint__add,ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V0x1)),inj__ty_2Enum_2Enum(V1y1))),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V2x2)),inj__ty_2Enum_2Enum(V3y2)))) = surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0x1)),inj__ty_2Enum_2Enum(V2x2))),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1y1)),inj__ty_2Enum_2Enum(V3y2)))))))))).
tff(ax_thm_2Einteger_2Etint__mul,axiom,( ! [V0x1:tp__ty_2Enum_2Enum] : ( ! [V1y1:tp__ty_2Enum_2Enum] : ( ! [V2x2:tp__ty_2Enum_2Enum] : ( ! [V3y2:tp__ty_2Enum_2Enum] : (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(ap(ap(c_2Einteger_2Etint__mul,ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V0x1)),inj__ty_2Enum_2Enum(V1y1))),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V2x2)),inj__ty_2Enum_2Enum(V3y2)))) = surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0x1)),inj__ty_2Enum_2Enum(V2x2))),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V1y1)),inj__ty_2Enum_2Enum(V3y2)))),ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0x1)),inj__ty_2Enum_2Enum(V3y2))),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V1y1)),inj__ty_2Enum_2Enum(V2x2))))))))))).
tff(ax_thm_2Einteger_2Etint__lt,axiom,( ! [V0x1:tp__ty_2Enum_2Enum] : ( ! [V1y1:tp__ty_2Enum_2Enum] : ( ! [V2x2:tp__ty_2Enum_2Enum] : ( ! [V3y2:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Einteger_2Etint__lt,ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V0x1)),inj__ty_2Enum_2Enum(V1y1))),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V2x2)),inj__ty_2Enum_2Enum(V3y2)))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0x1)),inj__ty_2Enum_2Enum(V3y2))),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V2x2)),inj__ty_2Enum_2Enum(V1y1)))))))))).
tff(ax_thm_2Einteger_2Etint__eq,axiom,( ! [V0x1:tp__ty_2Enum_2Enum] : ( ! [V1y1:tp__ty_2Enum_2Enum] : ( ! [V2x2:tp__ty_2Enum_2Enum] : ( ! [V3y2:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Einteger_2Etint__eq,ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V0x1)),inj__ty_2Enum_2Enum(V1y1))),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V2x2)),inj__ty_2Enum_2Enum(V3y2)))) <=> (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0x1)),inj__ty_2Enum_2Enum(V3y2))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V2x2)),inj__ty_2Enum_2Enum(V1y1)))))))))).
tff(conj_thm_2Einteger_2ETINT__EQ__REFL,lemma,(( ! [V0x:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : p(ap(ap(c_2Einteger_2Etint__eq,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x)))))).
tff(conj_thm_2Einteger_2ETINT__EQ__SYM,lemma,(( ! [V0x:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1y:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : (p(ap(ap(c_2Einteger_2Etint__eq,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1y))) <=> p(ap(ap(c_2Einteger_2Etint__eq,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1y)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x)))))))).
tff(conj_thm_2Einteger_2ETINT__EQ__TRANS,lemma,(( ! [V0x:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1y:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V2z:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((p(ap(ap(c_2Einteger_2Etint__eq,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1y))) & p(ap(ap(c_2Einteger_2Etint__eq,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1y)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V2z)))) => p(ap(ap(c_2Einteger_2Etint__eq,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V2z))))))))).
tff(conj_thm_2Einteger_2ETINT__EQ__EQUIV,lemma,(( ! [V0p:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1q:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : (p(ap(ap(c_2Einteger_2Etint__eq,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0p)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1q))) <=> (ap(c_2Einteger_2Etint__eq,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0p)) = ap(c_2Einteger_2Etint__eq,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1q)))))))).
tff(conj_thm_2Einteger_2ETINT__EQ__AP,lemma,(( ! [V0p:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1q:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((V0p = V1q) => p(ap(ap(c_2Einteger_2Etint__eq,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0p)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1q)))))))).
tff(conj_thm_2Einteger_2ETINT__10,lemma,((~~ p(ap(ap(c_2Einteger_2Etint__eq,c_2Einteger_2Etint__1),c_2Einteger_2Etint__0))))).
tff(conj_thm_2Einteger_2ETINT__ADD__SYM,lemma,(( ! [V0x:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1y:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(ap(ap(c_2Einteger_2Etint__add,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1y))) = surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(ap(ap(c_2Einteger_2Etint__add,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1y)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x)))))))).
tff(conj_thm_2Einteger_2ETINT__MUL__SYM,lemma,(( ! [V0x:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1y:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(ap(ap(c_2Einteger_2Etint__mul,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1y))) = surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(ap(ap(c_2Einteger_2Etint__mul,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1y)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x)))))))).
tff(conj_thm_2Einteger_2ETINT__ADD__ASSOC,lemma,(( ! [V0x:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1y:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V2z:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(ap(ap(c_2Einteger_2Etint__add,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x)),ap(ap(c_2Einteger_2Etint__add,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1y)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V2z)))) = surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(ap(ap(c_2Einteger_2Etint__add,ap(ap(c_2Einteger_2Etint__add,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1y))),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V2z))))))))).
tff(conj_thm_2Einteger_2ETINT__MUL__ASSOC,lemma,(( ! [V0x:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1y:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V2z:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(ap(ap(c_2Einteger_2Etint__mul,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x)),ap(ap(c_2Einteger_2Etint__mul,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1y)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V2z)))) = surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(ap(ap(c_2Einteger_2Etint__mul,ap(ap(c_2Einteger_2Etint__mul,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1y))),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V2z))))))))).
tff(conj_thm_2Einteger_2ETINT__LDISTRIB,lemma,(( ! [V0x:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1y:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V2z:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(ap(ap(c_2Einteger_2Etint__mul,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x)),ap(ap(c_2Einteger_2Etint__add,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1y)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V2z)))) = surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(ap(ap(c_2Einteger_2Etint__add,ap(ap(c_2Einteger_2Etint__mul,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1y))),ap(ap(c_2Einteger_2Etint__mul,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V2z)))))))))).
tff(conj_thm_2Einteger_2ETINT__ADD__LID,lemma,(( ! [V0x:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : p(ap(ap(c_2Einteger_2Etint__eq,ap(ap(c_2Einteger_2Etint__add,c_2Einteger_2Etint__0),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x))),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x)))))).
tff(conj_thm_2Einteger_2ETINT__MUL__LID,lemma,(( ! [V0x:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : p(ap(ap(c_2Einteger_2Etint__eq,ap(ap(c_2Einteger_2Etint__mul,c_2Einteger_2Etint__1),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x))),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x)))))).
tff(conj_thm_2Einteger_2ETINT__ADD__LINV,lemma,(( ! [V0x:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : p(ap(ap(c_2Einteger_2Etint__eq,ap(ap(c_2Einteger_2Etint__add,ap(c_2Einteger_2Etint__neg,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x))),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x))),c_2Einteger_2Etint__0))))).
tff(conj_thm_2Einteger_2ETINT__LT__TOTAL,lemma,(( ! [V0x:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1y:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : (p(ap(ap(c_2Einteger_2Etint__eq,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1y))) | (p(ap(ap(c_2Einteger_2Etint__lt,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1y))) | p(ap(ap(c_2Einteger_2Etint__lt,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1y)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x))))))))).
tff(conj_thm_2Einteger_2ETINT__LT__REFL,lemma,(( ! [V0x:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : (~~ p(ap(ap(c_2Einteger_2Etint__lt,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x))))))).
tff(conj_thm_2Einteger_2ETINT__LT__TRANS,lemma,(( ! [V0x:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1y:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V2z:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((p(ap(ap(c_2Einteger_2Etint__lt,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1y))) & p(ap(ap(c_2Einteger_2Etint__lt,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1y)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V2z)))) => p(ap(ap(c_2Einteger_2Etint__lt,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V2z))))))))).
tff(conj_thm_2Einteger_2ETINT__LT__ADD,lemma,(( ! [V0x:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1y:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V2z:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : (p(ap(ap(c_2Einteger_2Etint__lt,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1y)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V2z))) => p(ap(ap(c_2Einteger_2Etint__lt,ap(ap(c_2Einteger_2Etint__add,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1y))),ap(ap(c_2Einteger_2Etint__add,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V2z)))))))))).
tff(conj_thm_2Einteger_2ETINT__LT__MUL,lemma,(( ! [V0x:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1y:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((p(ap(ap(c_2Einteger_2Etint__lt,c_2Einteger_2Etint__0),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x))) & p(ap(ap(c_2Einteger_2Etint__lt,c_2Einteger_2Etint__0),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1y)))) => p(ap(ap(c_2Einteger_2Etint__lt,c_2Einteger_2Etint__0),ap(ap(c_2Einteger_2Etint__mul,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1y))))))))).
tff(conj_thm_2Einteger_2ETINT__NEG__WELLDEF,lemma,(( ! [V0x1:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1x2:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : (p(ap(ap(c_2Einteger_2Etint__eq,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x1)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1x2))) => p(ap(ap(c_2Einteger_2Etint__eq,ap(c_2Einteger_2Etint__neg,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x1))),ap(c_2Einteger_2Etint__neg,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1x2))))))))).
tff(conj_thm_2Einteger_2ETINT__ADD__WELLDEFR,lemma,(( ! [V0x1:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1x2:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V2y:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : (p(ap(ap(c_2Einteger_2Etint__eq,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x1)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1x2))) => p(ap(ap(c_2Einteger_2Etint__eq,ap(ap(c_2Einteger_2Etint__add,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x1)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V2y))),ap(ap(c_2Einteger_2Etint__add,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1x2)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V2y)))))))))).
tff(conj_thm_2Einteger_2ETINT__ADD__WELLDEF,lemma,(( ! [V0x1:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1x2:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V2y1:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V3y2:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((p(ap(ap(c_2Einteger_2Etint__eq,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x1)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1x2))) & p(ap(ap(c_2Einteger_2Etint__eq,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V2y1)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V3y2)))) => p(ap(ap(c_2Einteger_2Etint__eq,ap(ap(c_2Einteger_2Etint__add,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x1)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V2y1))),ap(ap(c_2Einteger_2Etint__add,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1x2)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V3y2))))))))))).
tff(conj_thm_2Einteger_2ETINT__MUL__WELLDEFR,lemma,(( ! [V0x1:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1x2:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V2y:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : (p(ap(ap(c_2Einteger_2Etint__eq,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x1)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1x2))) => p(ap(ap(c_2Einteger_2Etint__eq,ap(ap(c_2Einteger_2Etint__mul,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x1)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V2y))),ap(ap(c_2Einteger_2Etint__mul,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1x2)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V2y)))))))))).
tff(conj_thm_2Einteger_2ETINT__MUL__WELLDEF,lemma,(( ! [V0x1:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1x2:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V2y1:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V3y2:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((p(ap(ap(c_2Einteger_2Etint__eq,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x1)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1x2))) & p(ap(ap(c_2Einteger_2Etint__eq,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V2y1)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V3y2)))) => p(ap(ap(c_2Einteger_2Etint__eq,ap(ap(c_2Einteger_2Etint__mul,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x1)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V2y1))),ap(ap(c_2Einteger_2Etint__mul,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1x2)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V3y2))))))))))).
tff(conj_thm_2Einteger_2ETINT__LT__WELLDEFR,lemma,(( ! [V0x1:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1x2:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V2y:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : (p(ap(ap(c_2Einteger_2Etint__eq,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x1)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1x2))) => (p(ap(ap(c_2Einteger_2Etint__lt,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x1)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V2y))) <=> p(ap(ap(c_2Einteger_2Etint__lt,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1x2)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V2y)))))))))).
tff(conj_thm_2Einteger_2ETINT__LT__WELLDEFL,lemma,(( ! [V0x:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1y1:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V2y2:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : (p(ap(ap(c_2Einteger_2Etint__eq,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1y1)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V2y2))) => (p(ap(ap(c_2Einteger_2Etint__lt,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1y1))) <=> p(ap(ap(c_2Einteger_2Etint__lt,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V2y2)))))))))).
tff(conj_thm_2Einteger_2ETINT__LT__WELLDEF,lemma,(( ! [V0x1:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V1x2:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V2y1:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ( ! [V3y2:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((p(ap(ap(c_2Einteger_2Etint__eq,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x1)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1x2))) & p(ap(ap(c_2Einteger_2Etint__eq,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V2y1)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V3y2)))) => (p(ap(ap(c_2Einteger_2Etint__lt,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0x1)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V2y1))) <=> p(ap(ap(c_2Einteger_2Etint__lt,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V1x2)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V3y2))))))))))).
tff(ax_thm_2Einteger_2Etint__of__num,axiom,((surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(ap(c_2Einteger_2Etint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(c_2Einteger_2Etint__0)) & ( ! [V0n:tp__ty_2Enum_2Enum] : (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(ap(c_2Einteger_2Etint__of__num,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n)))) = surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(ap(ap(c_2Einteger_2Etint__add,ap(c_2Einteger_2Etint__of__num,inj__ty_2Enum_2Enum(V0n))),c_2Einteger_2Etint__1)))))).
tff(conj_thm_2Einteger_2Etint__of__num__eq,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Epair_2EFST(ty_2Enum_2Enum,ty_2Enum_2Enum),ap(c_2Einteger_2Etint__of__num,inj__ty_2Enum_2Enum(V0n)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(c_2Epair_2ESND(ty_2Enum_2Enum,ty_2Enum_2Enum),ap(c_2Einteger_2Etint__of__num,inj__ty_2Enum_2Enum(V0n)))),inj__ty_2Enum_2Enum(V0n))))))).
tff(conj_thm_2Einteger_2ETINT__INJ,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Einteger_2Etint__eq,ap(c_2Einteger_2Etint__of__num,inj__ty_2Enum_2Enum(V0m))),ap(c_2Einteger_2Etint__of__num,inj__ty_2Enum_2Enum(V1n)))) <=> (V0m = V1n)))))).
tff(conj_thm_2Einteger_2ENUM__POSTINT__EX,lemma,(( ! [V0t:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : ((~~ p(ap(ap(c_2Einteger_2Etint__lt,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0t)),c_2Einteger_2Etint__0))) => (? [V1n:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Einteger_2Etint__eq,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0t)),ap(c_2Einteger_2Etint__of__num,inj__ty_2Enum_2Enum(V1n))))))))).
tff(ax_thm_2Einteger_2Eint__TY__DEF,axiom,(? [V0rep:$i] : (mem(V0rep,arr(ty_2Einteger_2Eint,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),bool))) & p(ap(ap(c_2Ebool_2ETYPE__DEFINITION(arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),bool),ty_2Einteger_2Eint),f2135),V0rep))))).
tff(ax_thm_2Einteger_2Eint__bijections,axiom,(( ! [V0a:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__ABS__CLASS,ap(c_2Einteger_2Eint__REP__CLASS,inj__ty_2Einteger_2Eint(V0a)))) = V0a)) & ( ! [V1r:$i] : (mem(V1r,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),bool)) => (p(ap(f2137,V1r)) <=> (ap(c_2Einteger_2Eint__REP__CLASS,ap(c_2Einteger_2Eint__ABS__CLASS,V1r)) = V1r)))))).
tff(conj_thm_2Einteger_2Eint__ABS__REP__CLASS,lemma,((( ! [V0a:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__ABS__CLASS,ap(c_2Einteger_2Eint__REP__CLASS,inj__ty_2Einteger_2Eint(V0a)))) = V0a)) & ( ! [V1c:$i] : (mem(V1c,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),bool)) => ((? [V2r:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : (p(ap(ap(c_2Einteger_2Etint__eq,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V2r)),inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V2r))) & (V1c = ap(c_2Einteger_2Etint__eq,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V2r))))) <=> (ap(c_2Einteger_2Eint__REP__CLASS,ap(c_2Einteger_2Eint__ABS__CLASS,V1c)) = V1c))))))).
tff(ax_thm_2Einteger_2Eint__REP__def,axiom,( ! [V0a:tp__ty_2Einteger_2Eint] : (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(ap(c_2Einteger_2Eint__REP,inj__ty_2Einteger_2Eint(V0a))) = surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(ap(c_2Emin_2E_40(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),ap(c_2Einteger_2Eint__REP__CLASS,inj__ty_2Einteger_2Eint(V0a))))))).
tff(ax_thm_2Einteger_2Eint__ABS__def,axiom,( ! [V0r:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : (surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__ABS,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0r))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__ABS__CLASS,ap(c_2Einteger_2Etint__eq,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(V0r))))))).
tff(conj_thm_2Einteger_2Eint__QUOTIENT,lemma,(p(ap(ap(ap(c_2Equotient_2EQUOTIENT(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Einteger_2Eint),c_2Einteger_2Etint__eq),c_2Einteger_2Eint__ABS),c_2Einteger_2Eint__REP)))).
tff(ax_thm_2Einteger_2Eint__0,axiom,(fo__c_2Einteger_2Eint__0 = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__ABS,c_2Einteger_2Etint__0)))).
tff(ax_thm_2Einteger_2Eint__1,axiom,(fo__c_2Einteger_2Eint__1 = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__ABS,c_2Einteger_2Etint__1)))).
tff(ax_thm_2Einteger_2Eint__neg,axiom,( ! [V0T1:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V0T1))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__ABS,ap(c_2Einteger_2Etint__neg,ap(c_2Einteger_2Eint__REP,inj__ty_2Einteger_2Eint(V0T1)))))))).
tff(ax_thm_2Einteger_2Eint__add,axiom,( ! [V0T1:tp__ty_2Einteger_2Eint] : ( ! [V1T2:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0T1)),inj__ty_2Einteger_2Eint(V1T2))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__ABS,ap(ap(c_2Einteger_2Etint__add,ap(c_2Einteger_2Eint__REP,inj__ty_2Einteger_2Eint(V0T1))),ap(c_2Einteger_2Eint__REP,inj__ty_2Einteger_2Eint(V1T2))))))))).
tff(ax_thm_2Einteger_2Eint__mul,axiom,( ! [V0T1:tp__ty_2Einteger_2Eint] : ( ! [V1T2:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V0T1)),inj__ty_2Einteger_2Eint(V1T2))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__ABS,ap(ap(c_2Einteger_2Etint__mul,ap(c_2Einteger_2Eint__REP,inj__ty_2Einteger_2Eint(V0T1))),ap(c_2Einteger_2Eint__REP,inj__ty_2Einteger_2Eint(V1T2))))))))).
tff(ax_thm_2Einteger_2Eint__lt,axiom,( ! [V0T1:tp__ty_2Einteger_2Eint] : ( ! [V1T2:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0T1)),inj__ty_2Einteger_2Eint(V1T2))) <=> p(ap(ap(c_2Einteger_2Etint__lt,ap(c_2Einteger_2Eint__REP,inj__ty_2Einteger_2Eint(V0T1))),ap(c_2Einteger_2Eint__REP,inj__ty_2Einteger_2Eint(V1T2)))))))).
tff(conj_thm_2Einteger_2EINT__10,lemma,((~~ (fo__c_2Einteger_2Eint__1 = fo__c_2Einteger_2Eint__0)))).
tff(conj_thm_2Einteger_2EINT__ADD__SYM,lemma,(( ! [V0y:tp__ty_2Einteger_2Eint] : ( ! [V1x:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1x)),inj__ty_2Einteger_2Eint(V0y))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0y)),inj__ty_2Einteger_2Eint(V1x)))))))).
tff(conj_thm_2Einteger_2EINT__ADD__COMM,lemma,(( ! [V0y:tp__ty_2Einteger_2Eint] : ( ! [V1x:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1x)),inj__ty_2Einteger_2Eint(V0y))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0y)),inj__ty_2Einteger_2Eint(V1x)))))))).
tff(conj_thm_2Einteger_2EINT__MUL__SYM,lemma,(( ! [V0y:tp__ty_2Einteger_2Eint] : ( ! [V1x:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V1x)),inj__ty_2Einteger_2Eint(V0y))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V0y)),inj__ty_2Einteger_2Eint(V1x)))))))).
tff(conj_thm_2Einteger_2EINT__MUL__COMM,lemma,(( ! [V0y:tp__ty_2Einteger_2Eint] : ( ! [V1x:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V1x)),inj__ty_2Einteger_2Eint(V0y))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V0y)),inj__ty_2Einteger_2Eint(V1x)))))))).
tff(conj_thm_2Einteger_2EINT__ADD__ASSOC,lemma,(( ! [V0z:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2x:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V2x)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V0z)))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V2x)),inj__ty_2Einteger_2Eint(V1y))),inj__ty_2Einteger_2Eint(V0z))))))))).
tff(conj_thm_2Einteger_2EINT__MUL__ASSOC,lemma,(( ! [V0z:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2x:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V2x)),ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V0z)))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V2x)),inj__ty_2Einteger_2Eint(V1y))),inj__ty_2Einteger_2Eint(V0z))))))))).
tff(conj_thm_2Einteger_2EINT__LDISTRIB,lemma,(( ! [V0z:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2x:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V2x)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V0z)))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V2x)),inj__ty_2Einteger_2Eint(V1y))),ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V2x)),inj__ty_2Einteger_2Eint(V0z)))))))))).
tff(conj_thm_2Einteger_2EINT__LT__TOTAL,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ((V0x = V1y) | (p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) | p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V0x))))))))).
tff(conj_thm_2Einteger_2EINT__LT__REFL,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : (~~ p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V0x))))))).
tff(conj_thm_2Einteger_2EINT__LT__TRANS,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : ((p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) & p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V2z)))) => p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V2z))))))))).
tff(conj_thm_2Einteger_2EINT__LT__LADD__IMP,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V2z))) => p(ap(ap(c_2Einteger_2Eint__lt,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V2z)))))))))).
tff(conj_thm_2Einteger_2EINT__LT__MUL,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ((p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__0)),inj__ty_2Einteger_2Eint(V0x))) & p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__0)),inj__ty_2Einteger_2Eint(V1y)))) => p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__0)),ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))))))))).
tff(conj_thm_2Einteger_2Eint__of__num,lemma,(((surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = fo__c_2Einteger_2Eint__0) & ( ! [V0n:tp__ty_2Enum_2Enum] : (surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n)))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(V0n))),inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__1)))))))).
tff(conj_thm_2Einteger_2ENUM__POSINT__EX,lemma,(( ! [V0t:tp__ty_2Einteger_2Eint] : ((~~ p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0t)),inj__ty_2Einteger_2Eint(fo__c_2Einteger_2Eint__0)))) => (? [V1n:tp__ty_2Enum_2Enum] : (V0t = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(V1n))))))))).
tff(ax_thm_2Einteger_2Eint__sub,axiom,( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V1y)))))))).
tff(ax_thm_2Einteger_2Eint__le,axiom,( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) <=> (~~ p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V0x)))))))).
tff(ax_thm_2Einteger_2Eint__gt,axiom,( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__gt,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) <=> p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V0x))))))).
tff(ax_thm_2Einteger_2Eint__ge,axiom,( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__ge,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) <=> p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V0x))))))).
tff(conj_thm_2Einteger_2EINT__0,lemma,((fo__c_2Einteger_2Eint__0 = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))).
tff(conj_thm_2Einteger_2EINT__1,lemma,((fo__c_2Einteger_2Eint__1 = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))).
tff(conj_thm_2Einteger_2EINT__ADD__LID,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Einteger_2Eint(V0x))) = V0x)))).
tff(conj_thm_2Einteger_2EINT__ADD__RID,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) = V0x)))).
tff(conj_thm_2Einteger_2EINT__ADD__LINV,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V0x))),inj__ty_2Einteger_2Eint(V0x))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))).
tff(conj_thm_2Einteger_2EINT__ADD__RINV,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V0x)))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))).
tff(conj_thm_2Einteger_2EINT__MUL__LID,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),inj__ty_2Einteger_2Eint(V0x))) = V0x)))).
tff(conj_thm_2Einteger_2EINT__MUL__RID,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V0x)),ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))) = V0x)))).
tff(conj_thm_2Einteger_2EINT__RDISTRIB,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))),inj__ty_2Einteger_2Eint(V2z))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V2z))),ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V2z)))))))))).
tff(conj_thm_2Einteger_2EINT__EQ__LADD,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V2z)))) <=> (V1y = V2z))))))).
tff(conj_thm_2Einteger_2EINT__EQ__RADD,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V2z))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V2z)))) <=> (V0x = V1y))))))).
tff(conj_thm_2Einteger_2EINT__ADD__LID__UNIQ,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) = V1y) <=> (V0x = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))))).
tff(conj_thm_2Einteger_2EINT__ADD__RID__UNIQ,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) = V0x) <=> (V1y = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))))).
tff(conj_thm_2Einteger_2EINT__LNEG__UNIQ,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) <=> (V0x = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V1y))))))))).
tff(conj_thm_2Einteger_2EINT__RNEG__UNIQ,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) <=> (V1y = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V0x))))))))).
tff(conj_thm_2Einteger_2EINT__NEG__ADD,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__neg,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y)))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V0x))),ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V1y))))))))).
tff(conj_thm_2Einteger_2EINT__MUL__LZERO,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Einteger_2Eint(V0x))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))).
tff(conj_thm_2Einteger_2EINT__MUL__RZERO,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V0x)),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))).
tff(conj_thm_2Einteger_2EINT__NEG__LMUL,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__neg,ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y)))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V0x))),inj__ty_2Einteger_2Eint(V1y)))))))).
tff(conj_thm_2Einteger_2EINT__NEG__RMUL,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__neg,ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y)))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V0x)),ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V1y))))))))).
tff(conj_thm_2Einteger_2EINT__NEGNEG,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V0x)))) = V0x)))).
tff(conj_thm_2Einteger_2EINT__NEG__MUL2,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V0x))),ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V1y)))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y)))))))).
tff(conj_thm_2Einteger_2EINT__LT__LADD,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__lt,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V2z)))) <=> p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V2z))))))))).
tff(conj_thm_2Einteger_2EINT__LT__RADD,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__lt,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V2z))),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V2z)))) <=> p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))))))))).
tff(conj_thm_2Einteger_2EINT__NOT__LT,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ((~~ p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y)))) <=> p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V0x)))))))).
tff(conj_thm_2Einteger_2EINT__LT__ANTISYM,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (~~ (p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) & p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V0x))))))))).
tff(conj_thm_2Einteger_2EINT__LT__GT,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) => (~~ p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V0x))))))))).
tff(conj_thm_2Einteger_2EINT__NOT__LE,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ((~~ p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y)))) <=> p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V0x)))))))).
tff(conj_thm_2Einteger_2EINT__LE__TOTAL,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) | p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V0x)))))))).
tff(conj_thm_2Einteger_2EINT__LET__TOTAL,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) | p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V0x)))))))).
tff(conj_thm_2Einteger_2EINT__LTE__TOTAL,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) | p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V0x)))))))).
tff(conj_thm_2Einteger_2EINT__LE__REFL,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V0x)))))).
tff(conj_thm_2Einteger_2EINT__LE__LT,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) <=> (p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) | (V0x = V1y))))))).
tff(conj_thm_2Einteger_2EINT__LT__LE,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) <=> (p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) & (~~ (V0x = V1y)))))))).
tff(conj_thm_2Einteger_2EINT__LT__IMP__LE,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) => p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y)))))))).
tff(conj_thm_2Einteger_2EINT__LTE__TRANS,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : ((p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) & p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V2z)))) => p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V2z))))))))).
tff(conj_thm_2Einteger_2EINT__LET__TRANS,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : ((p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) & p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V2z)))) => p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V2z))))))))).
tff(conj_thm_2Einteger_2EINT__LE__TRANS,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : ((p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) & p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V2z)))) => p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V2z))))))))).
tff(conj_thm_2Einteger_2EINT__LE__ANTISYM,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ((p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) & p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V0x)))) <=> (V0x = V1y)))))).
tff(conj_thm_2Einteger_2EINT__LET__ANTISYM,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (~~ (p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) & p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V0x))))))))).
tff(conj_thm_2Einteger_2EINT__LTE__ANTSYM,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (~~ (p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) & p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V0x))))))))).
tff(conj_thm_2Einteger_2EINT__NEG__LT0,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V0x))),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) <=> p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Einteger_2Eint(V0x))))))).
tff(conj_thm_2Einteger_2EINT__NEG__GT0,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V0x)))) <=> p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0x)),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))).
tff(conj_thm_2Einteger_2EINT__NEG__LE0,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V0x))),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) <=> p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Einteger_2Eint(V0x))))))).
tff(conj_thm_2Einteger_2EINT__NEG__GE0,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V0x)))) <=> p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V0x)),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))).
tff(conj_thm_2Einteger_2EINT__LT__NEGTOTAL,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ((V0x = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) | (p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Einteger_2Eint(V0x))) | p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V0x))))))))).
tff(conj_thm_2Einteger_2EINT__LE__NEGTOTAL,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Einteger_2Eint(V0x))) | p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V0x)))))))).
tff(conj_thm_2Einteger_2EINT__LE__MUL,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ((p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Einteger_2Eint(V0x))) & p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Einteger_2Eint(V1y)))) => p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))))))))).
tff(conj_thm_2Einteger_2EINT__LE__SQUARE,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V0x))))))).
tff(conj_thm_2Einteger_2EINT__LE__01,lemma,(p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))).
tff(conj_thm_2Einteger_2EINT__LT__01,lemma,(p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))).
tff(conj_thm_2Einteger_2EINT__LE__LADD,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V2z)))) <=> p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V2z))))))))).
tff(conj_thm_2Einteger_2EINT__LE__RADD,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V2z))),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V2z)))) <=> p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))))))))).
tff(conj_thm_2Einteger_2EINT__LT__ADD2,lemma,(( ! [V0w:tp__ty_2Einteger_2Eint] : ( ! [V1x:tp__ty_2Einteger_2Eint] : ( ! [V2y:tp__ty_2Einteger_2Eint] : ( ! [V3z:tp__ty_2Einteger_2Eint] : ((p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0w)),inj__ty_2Einteger_2Eint(V1x))) & p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V2y)),inj__ty_2Einteger_2Eint(V3z)))) => p(ap(ap(c_2Einteger_2Eint__lt,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0w)),inj__ty_2Einteger_2Eint(V2y))),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1x)),inj__ty_2Einteger_2Eint(V3z))))))))))).
tff(conj_thm_2Einteger_2EINT__LE__ADD2,lemma,(( ! [V0w:tp__ty_2Einteger_2Eint] : ( ! [V1x:tp__ty_2Einteger_2Eint] : ( ! [V2y:tp__ty_2Einteger_2Eint] : ( ! [V3z:tp__ty_2Einteger_2Eint] : ((p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V0w)),inj__ty_2Einteger_2Eint(V1x))) & p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V2y)),inj__ty_2Einteger_2Eint(V3z)))) => p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0w)),inj__ty_2Einteger_2Eint(V2y))),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1x)),inj__ty_2Einteger_2Eint(V3z))))))))))).
tff(conj_thm_2Einteger_2EINT__LE__ADD,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ((p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Einteger_2Eint(V0x))) & p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Einteger_2Eint(V1y)))) => p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))))))))).
tff(conj_thm_2Einteger_2EINT__LT__ADD,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ((p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Einteger_2Eint(V0x))) & p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Einteger_2Eint(V1y)))) => p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))))))))).
tff(conj_thm_2Einteger_2EINT__LT__ADDNEG,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V1y)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V2z))))) <=> p(ap(ap(c_2Einteger_2Eint__lt,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V2z))),inj__ty_2Einteger_2Eint(V0x))))))))).
tff(conj_thm_2Einteger_2EINT__LT__ADDNEG2,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__lt,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V1y)))),inj__ty_2Einteger_2Eint(V2z))) <=> p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V2z)),inj__ty_2Einteger_2Eint(V1y)))))))))).
tff(conj_thm_2Einteger_2EINT__LT__ADD1,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) => p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))).
tff(conj_thm_2Einteger_2EINT__SUB__ADD,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))),inj__ty_2Einteger_2Eint(V1y))) = V0x))))).
tff(conj_thm_2Einteger_2EINT__SUB__ADD2,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y)))) = V0x))))).
tff(conj_thm_2Einteger_2EINT__SUB__REFL,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V0x))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))).
tff(conj_thm_2Einteger_2EINT__SUB__0,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) <=> (V0x = V1y)))))).
tff(conj_thm_2Einteger_2EINT__LE__DOUBLE,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V0x)))) <=> p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Einteger_2Eint(V0x))))))).
tff(conj_thm_2Einteger_2EINT__LE__NEGL,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V0x))),inj__ty_2Einteger_2Eint(V0x))) <=> p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Einteger_2Eint(V0x))))))).
tff(conj_thm_2Einteger_2EINT__LE__NEGR,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V0x)),ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V0x)))) <=> p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V0x)),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))).
tff(conj_thm_2Einteger_2EINT__NEG__EQ0,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V0x))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) <=> (V0x = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))).
tff(conj_thm_2Einteger_2EINT__NEG__0,lemma,((surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))).
tff(conj_thm_2Einteger_2EINT__NEG__SUB,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__neg,ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y)))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V0x)))))))).
tff(conj_thm_2Einteger_2EINT__SUB__LT,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y)))) <=> p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V0x)))))))).
tff(conj_thm_2Einteger_2EINT__SUB__LE,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y)))) <=> p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V0x)))))))).
tff(conj_thm_2Einteger_2EINT__ADD__SUB,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__sub,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))),inj__ty_2Einteger_2Eint(V0x))) = V1y))))).
tff(conj_thm_2Einteger_2EINT__SUB__LDISTRIB,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V2z)))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__sub,ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))),ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V2z)))))))))).
tff(conj_thm_2Einteger_2EINT__SUB__RDISTRIB,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))),inj__ty_2Einteger_2Eint(V2z))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__sub,ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V2z))),ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V2z)))))))))).
tff(conj_thm_2Einteger_2EINT__NEG__EQ,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V0x))) = V1y) <=> (V0x = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V1y))))))))).
tff(conj_thm_2Einteger_2EINT__NEG__MINUS1,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V0x))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V0x))))))).
tff(conj_thm_2Einteger_2EINT__LT__IMP__NE,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) => (~~ (V0x = V1y))))))).
tff(conj_thm_2Einteger_2EINT__LE__ADDR,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y)))) <=> p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Einteger_2Eint(V1y)))))))).
tff(conj_thm_2Einteger_2EINT__LE__ADDL,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V1y)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y)))) <=> p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Einteger_2Eint(V0x)))))))).
tff(conj_thm_2Einteger_2EINT__LT__ADDR,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y)))) <=> p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Einteger_2Eint(V1y)))))))).
tff(conj_thm_2Einteger_2EINT__LT__ADDL,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V1y)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y)))) <=> p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Einteger_2Eint(V0x)))))))).
tff(conj_thm_2Einteger_2EINT__ENTIRE,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) <=> ((V0x = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) | (V1y = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))))).
tff(conj_thm_2Einteger_2EINT__EQ__LMUL,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V2z)))) <=> ((V0x = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) | (V1y = V2z)))))))).
tff(conj_thm_2Einteger_2EINT__EQ__RMUL,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V2z))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V2z)))) <=> ((V2z = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) | (V0x = V1y)))))))).
tff(conj_thm_2Einteger_2EINT,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n)))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(V0n))),ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))).
tff(conj_thm_2Einteger_2EINT__POS,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(V0n))))))).
tff(conj_thm_2Einteger_2EINT__LE,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(V0m))),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(V1n)))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))))))).
tff(conj_thm_2Einteger_2EINT__LT,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(V0m))),ap(c_2Einteger_2Eint__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_2Einteger_2EINT__INJ,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(V0m))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(V1n)))) <=> (V0m = V1n)))))).
tff(conj_thm_2Einteger_2EINT__ADD,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(V0m))),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(V1n)))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))))))))).
tff(conj_thm_2Einteger_2EINT__MUL,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(V0m))),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(V1n)))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))))))))).
tff(conj_thm_2Einteger_2EINT__LT__NZ,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ((~~ (surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))) <=> p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(V0n)))))))).
tff(conj_thm_2Einteger_2EINT__NZ__IMP__LT,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ((~~ (V0n = fo__c_2Enum_2E0)) => p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(V0n)))))))).
tff(conj_thm_2Einteger_2EINT__DOUBLE,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V0x))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),inj__ty_2Einteger_2Eint(V0x))))))).
tff(conj_thm_2Einteger_2EINT__SUB__SUB,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__sub,ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))),inj__ty_2Einteger_2Eint(V0x))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V1y)))))))).
tff(conj_thm_2Einteger_2EINT__LT__ADD__SUB,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__lt,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))),inj__ty_2Einteger_2Eint(V2z))) <=> p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(V2z)),inj__ty_2Einteger_2Eint(V1y)))))))))).
tff(conj_thm_2Einteger_2EINT__LT__SUB__RADD,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__lt,ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))),inj__ty_2Einteger_2Eint(V2z))) <=> p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V2z)),inj__ty_2Einteger_2Eint(V1y)))))))))).
tff(conj_thm_2Einteger_2EINT__LT__SUB__LADD,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V2z)))) <=> p(ap(ap(c_2Einteger_2Eint__lt,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V2z))),inj__ty_2Einteger_2Eint(V1y))))))))).
tff(conj_thm_2Einteger_2EINT__LE__SUB__LADD,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V2z)))) <=> p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V2z))),inj__ty_2Einteger_2Eint(V1y))))))))).
tff(conj_thm_2Einteger_2EINT__LE__SUB__RADD,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))),inj__ty_2Einteger_2Eint(V2z))) <=> p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V2z)),inj__ty_2Einteger_2Eint(V1y)))))))))).
tff(conj_thm_2Einteger_2EINT__LT__NEG,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V0x))),ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V1y)))) <=> p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V0x)))))))).
tff(conj_thm_2Einteger_2EINT__LE__NEG,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V0x))),ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V1y)))) <=> p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V0x)))))))).
tff(conj_thm_2Einteger_2EINT__ADD2__SUB2,lemma,(( ! [V0a:tp__ty_2Einteger_2Eint] : ( ! [V1b:tp__ty_2Einteger_2Eint] : ( ! [V2c:tp__ty_2Einteger_2Eint] : ( ! [V3d:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__sub,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0a)),inj__ty_2Einteger_2Eint(V1b))),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V2c)),inj__ty_2Einteger_2Eint(V3d)))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(V0a)),inj__ty_2Einteger_2Eint(V2c))),ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(V1b)),inj__ty_2Einteger_2Eint(V3d))))))))))).
tff(conj_thm_2Einteger_2EINT__SUB__LZERO,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__sub,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Einteger_2Eint(V0x))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V0x))))))).
tff(conj_thm_2Einteger_2EINT__SUB__RZERO,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(V0x)),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) = V0x)))).
tff(conj_thm_2Einteger_2EINT__LET__ADD2,lemma,(( ! [V0w:tp__ty_2Einteger_2Eint] : ( ! [V1x:tp__ty_2Einteger_2Eint] : ( ! [V2y:tp__ty_2Einteger_2Eint] : ( ! [V3z:tp__ty_2Einteger_2Eint] : ((p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V0w)),inj__ty_2Einteger_2Eint(V1x))) & p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V2y)),inj__ty_2Einteger_2Eint(V3z)))) => p(ap(ap(c_2Einteger_2Eint__lt,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0w)),inj__ty_2Einteger_2Eint(V2y))),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1x)),inj__ty_2Einteger_2Eint(V3z))))))))))).
tff(conj_thm_2Einteger_2EINT__LTE__ADD2,lemma,(( ! [V0w:tp__ty_2Einteger_2Eint] : ( ! [V1x:tp__ty_2Einteger_2Eint] : ( ! [V2y:tp__ty_2Einteger_2Eint] : ( ! [V3z:tp__ty_2Einteger_2Eint] : ((p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0w)),inj__ty_2Einteger_2Eint(V1x))) & p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V2y)),inj__ty_2Einteger_2Eint(V3z)))) => p(ap(ap(c_2Einteger_2Eint__lt,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0w)),inj__ty_2Einteger_2Eint(V2y))),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1x)),inj__ty_2Einteger_2Eint(V3z))))))))))).
tff(conj_thm_2Einteger_2EINT__LET__ADD,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ((p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Einteger_2Eint(V0x))) & p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Einteger_2Eint(V1y)))) => p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))))))))).
tff(conj_thm_2Einteger_2EINT__LTE__ADD,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ((p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Einteger_2Eint(V0x))) & p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Einteger_2Eint(V1y)))) => p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))))))))).
tff(conj_thm_2Einteger_2EINT__LT__MUL2,lemma,(( ! [V0x1:tp__ty_2Einteger_2Eint] : ( ! [V1x2:tp__ty_2Einteger_2Eint] : ( ! [V2y1:tp__ty_2Einteger_2Eint] : ( ! [V3y2:tp__ty_2Einteger_2Eint] : ((p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Einteger_2Eint(V0x1))) & (p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Einteger_2Eint(V2y1))) & (p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0x1)),inj__ty_2Einteger_2Eint(V1x2))) & p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V2y1)),inj__ty_2Einteger_2Eint(V3y2)))))) => p(ap(ap(c_2Einteger_2Eint__lt,ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V0x1)),inj__ty_2Einteger_2Eint(V2y1))),ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V1x2)),inj__ty_2Einteger_2Eint(V3y2))))))))))).
tff(conj_thm_2Einteger_2EINT__SUB__LNEG,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__sub,ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V0x))),inj__ty_2Einteger_2Eint(V1y))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__neg,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))))))))).
tff(conj_thm_2Einteger_2EINT__SUB__RNEG,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(V0x)),ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V1y)))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y)))))))).
tff(conj_thm_2Einteger_2EINT__SUB__NEG2,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__sub,ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V0x))),ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V1y)))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V0x)))))))).
tff(conj_thm_2Einteger_2EINT__SUB__TRIANGLE,lemma,(( ! [V0a:tp__ty_2Einteger_2Eint] : ( ! [V1b:tp__ty_2Einteger_2Eint] : ( ! [V2c:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(V0a)),inj__ty_2Einteger_2Eint(V1b))),ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(V1b)),inj__ty_2Einteger_2Eint(V2c)))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(V0a)),inj__ty_2Einteger_2Eint(V2c))))))))).
tff(conj_thm_2Einteger_2EINT__EQ__SUB__LADD,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : ((V0x = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V2z)))) <=> (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V2z))) = V1y))))))).
tff(conj_thm_2Einteger_2EINT__EQ__SUB__RADD,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) = V2z) <=> (V0x = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V2z)),inj__ty_2Einteger_2Eint(V1y)))))))))).
tff(conj_thm_2Einteger_2EINT__SUB,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1m)),inj__ty_2Enum_2Enum(V0n))) => (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__sub,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(V0n))),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(V1m)))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))))))))).
tff(conj_thm_2Einteger_2EINT__SUB__SUB2,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y)))) = V1y))))).
tff(conj_thm_2Einteger_2EINT__ADD__SUB2,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y)))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V1y)))))))).
tff(conj_thm_2Einteger_2EINT__EQ__LMUL2,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : ((~~ (V0x = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))) => ((V1y = V2z) <=> (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V2z))))))))))).
tff(conj_thm_2Einteger_2EINT__EQ__IMP__LE,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ((V0x = V1y) => p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y)))))))).
tff(conj_thm_2Einteger_2EINT__POS__NZ,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Einteger_2Eint(V0x))) => (~~ (V0x = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))))).
tff(conj_thm_2Einteger_2EINT__EQ__RMUL__IMP,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : (((~~ (V2z = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))) & (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V2z))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V2z))))) => (V0x = V1y))))))).
tff(conj_thm_2Einteger_2EINT__EQ__LMUL__IMP,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2z:tp__ty_2Einteger_2Eint] : (((~~ (V0x = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))) & (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V2z))))) => (V1y = V2z))))))).
tff(conj_thm_2Einteger_2EINT__DIFFSQ,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))),ap(ap(c_2Einteger_2Eint__sub,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y)))) = surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__sub,ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V0x))),ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V1y))))))))).
tff(conj_thm_2Einteger_2EINT__POASQ,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V0x)))) <=> (~~ (V0x = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))))).
tff(conj_thm_2Einteger_2EINT__SUMSQ,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__add,ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V0x))),ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V1y)),inj__ty_2Einteger_2Eint(V1y)))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) <=> ((V0x = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) & (V1y = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))))).
tff(conj_thm_2Einteger_2EINT__EQ__NEG,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V0x))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__neg,inj__ty_2Einteger_2Eint(V1y)))) <=> (V0x = V1y)))))).
tff(conj_thm_2Einteger_2EINT__LT__CALCULATE,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(V0n))),ap(c_2Einteger_2Eint__of__num,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_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(V0n)))),ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,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_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(V0n)))),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(V1m)))) <=> ((~~ (V0n = fo__c_2Enum_2E0)) | (~~ (V1m = fo__c_2Enum_2E0)))) & (p(ap(ap(c_2Einteger_2Eint__lt,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(V0n))),ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(V1m))))) <=> $false)))))))).
tff(conj_thm_2Einteger_2ENUM__POSINT,lemma,(( ! [V0i:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Einteger_2Eint(V0i))) => p(ap(c_2Ebool_2E_3F_21(ty_2Enum_2Enum),f2138(V0i))))))).
tff(conj_thm_2Einteger_2ENUM__POSINT__EXISTS,lemma,(( ! [V0i:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Einteger_2Eint(V0i))) => (? [V1n:tp__ty_2Enum_2Enum] : (V0i = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(V1n))))))))).
tff(conj_thm_2Einteger_2ENUM__NEGINT__EXISTS,lemma,(( ! [V0i:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V0i)),ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) => (? [V1n:tp__ty_2Enum_2Enum] : (V0i = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(V1n)))))))))).
tff(conj_thm_2Einteger_2EINT__NUM__CASES,lemma,(( ! [V0p:tp__ty_2Einteger_2Eint] : ((? [V1n:tp__ty_2Enum_2Enum] : ((V0p = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(V1n)))) & (~~ (V1n = fo__c_2Enum_2E0)))) | ((? [V2n:tp__ty_2Enum_2Enum] : ((V0p = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(V2n))))) & (~~ (V2n = fo__c_2Enum_2E0)))) | (V0p = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))))).
tff(conj_thm_2Einteger_2EINT__DISCRETE,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (~~ (p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) & p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V1y)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))))))).
tff(conj_thm_2Einteger_2EINT__LE__LT1,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__le,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) <=> p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0x)),ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V1y)),ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))).
tff(conj_thm_2Einteger_2EINT__LT__LE1,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) <=> p(ap(ap(c_2Einteger_2Eint__le,ap(ap(c_2Einteger_2Eint__add,inj__ty_2Einteger_2Eint(V0x)),ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),inj__ty_2Einteger_2Eint(V1y)))))))).
tff(conj_thm_2Einteger_2EINT__MUL__EQ__1,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint(ap(ap(c_2Einteger_2Eint__mul,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))) = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))) <=> (((V0x = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))) & (V1y = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) | ((V0x = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) & (V1y = surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__neg,ap(c_2Einteger_2Eint__of__num,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))))).
tff(ax_thm_2Einteger_2ENum,axiom,( ! [V0i:tp__ty_2Einteger_2Eint] : (surj__ty_2Enum_2Enum(ap(c_2Einteger_2ENum,inj__ty_2Einteger_2Eint(V0i))) = surj__ty_2Enum_2Enum(ap(c_2Emin_2E_40(ty_2Enum_2Enum),f2138(V0i)))))).
tff(conj_thm_2Einteger_2ENUM__OF__INT,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Einteger_2ENum,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(V0n)))) = V0n)))).
tff(conj_thm_2Einteger_2EINT__OF__NUM,lemma,(( ! [V0i:tp__ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint(ap(c_2Einteger_2Eint__of__num,ap(c_2Einteger_2ENum,inj__ty_2Einteger_2Eint(V0i)))) = V0i) <=> p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Einteger_2Eint(V0i))))))).
tff(conj_thm_2Einteger_2ELE__NUM__OF__INT,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1i:tp__ty_2Einteger_2Eint] : (p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(V0n))),inj__ty_2Einteger_2Eint(V1i))) => p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0n)),ap(c_2Einteger_2ENum,inj__ty_2Einteger_2Eint(V1i))))))))).
tff(conj_thm_2Einteger_2ENUM__LT,conjecture,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ((p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Einteger_2Eint(V0x))) & p(ap(ap(c_2Einteger_2Eint__le,ap(c_2Einteger_2Eint__of__num,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Einteger_2Eint(V1y)))) => (p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Einteger_2ENum,inj__ty_2Einteger_2Eint(V0x))),ap(c_2Einteger_2ENum,inj__ty_2Einteger_2Eint(V1y)))) <=> p(ap(ap(c_2Einteger_2Eint__lt,inj__ty_2Einteger_2Eint(V0x)),inj__ty_2Einteger_2Eint(V1y))))))))).
