include('Axioms/poset_2.ax').
tff(tp_c_2Earithmetic_2E_2A,type,(c_2Earithmetic_2E_2A:$i)).
tff(mem_c_2Earithmetic_2E_2A,axiom,mem(c_2Earithmetic_2E_2A,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)))).
tff(stp_fo_c_2Earithmetic_2E_2A,type,(fo__c_2Earithmetic_2E_2A:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2E_2A,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2E_2A(X0,X1)) = ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Earithmetic_2E_2B,type,(c_2Earithmetic_2E_2B:$i)).
tff(mem_c_2Earithmetic_2E_2B,axiom,mem(c_2Earithmetic_2E_2B,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)))).
tff(stp_fo_c_2Earithmetic_2E_2B,type,(fo__c_2Earithmetic_2E_2B:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2E_2B,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2E_2B(X0,X1)) = ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Earithmetic_2E_2D,type,(c_2Earithmetic_2E_2D:$i)).
tff(mem_c_2Earithmetic_2E_2D,axiom,mem(c_2Earithmetic_2E_2D,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)))).
tff(stp_fo_c_2Earithmetic_2E_2D,type,(fo__c_2Earithmetic_2E_2D:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2E_2D,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2E_2D(X0,X1)) = ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Earithmetic_2E_3C_3D,type,(c_2Earithmetic_2E_3C_3D:$i)).
tff(mem_c_2Earithmetic_2E_3C_3D,axiom,mem(c_2Earithmetic_2E_3C_3D,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool)))).
tff(stp_fo_c_2Earithmetic_2E_3C_3D,type,(fo__c_2Earithmetic_2E_3C_3D:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__o)).
tff(stp_eq_fo_c_2Earithmetic_2E_3C_3D,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__o(fo__c_2Earithmetic_2E_3C_3D(X0,X1)) = ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Earithmetic_2E_3E,type,(c_2Earithmetic_2E_3E:$i)).
tff(mem_c_2Earithmetic_2E_3E,axiom,mem(c_2Earithmetic_2E_3E,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool)))).
tff(stp_fo_c_2Earithmetic_2E_3E,type,(fo__c_2Earithmetic_2E_3E:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__o)).
tff(stp_eq_fo_c_2Earithmetic_2E_3E,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__o(fo__c_2Earithmetic_2E_3E(X0,X1)) = ap(ap(c_2Earithmetic_2E_3E,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Earithmetic_2E_3E_3D,type,(c_2Earithmetic_2E_3E_3D:$i)).
tff(mem_c_2Earithmetic_2E_3E_3D,axiom,mem(c_2Earithmetic_2E_3E_3D,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool)))).
tff(stp_fo_c_2Earithmetic_2E_3E_3D,type,(fo__c_2Earithmetic_2E_3E_3D:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__o)).
tff(stp_eq_fo_c_2Earithmetic_2E_3E_3D,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__o(fo__c_2Earithmetic_2E_3E_3D(X0,X1)) = ap(ap(c_2Earithmetic_2E_3E_3D,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Earithmetic_2EABS__DIFF,type,(c_2Earithmetic_2EABS__DIFF:$i)).
tff(mem_c_2Earithmetic_2EABS__DIFF,axiom,mem(c_2Earithmetic_2EABS__DIFF,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)))).
tff(stp_fo_c_2Earithmetic_2EABS__DIFF,type,(fo__c_2Earithmetic_2EABS__DIFF:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2EABS__DIFF,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EABS__DIFF(X0,X1)) = ap(ap(c_2Earithmetic_2EABS__DIFF,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Earithmetic_2EBIT1,type,(c_2Earithmetic_2EBIT1:$i)).
tff(mem_c_2Earithmetic_2EBIT1,axiom,mem(c_2Earithmetic_2EBIT1,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))).
tff(stp_fo_c_2Earithmetic_2EBIT1,type,(fo__c_2Earithmetic_2EBIT1:(tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2EBIT1,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EBIT1(X0)) = ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Earithmetic_2EBIT2,type,(c_2Earithmetic_2EBIT2:$i)).
tff(mem_c_2Earithmetic_2EBIT2,axiom,mem(c_2Earithmetic_2EBIT2,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))).
tff(stp_fo_c_2Earithmetic_2EBIT2,type,(fo__c_2Earithmetic_2EBIT2:(tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2EBIT2,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EBIT2(X0)) = ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Earithmetic_2EDIV,type,(c_2Earithmetic_2EDIV:$i)).
tff(mem_c_2Earithmetic_2EDIV,axiom,mem(c_2Earithmetic_2EDIV,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)))).
tff(stp_fo_c_2Earithmetic_2EDIV,type,(fo__c_2Earithmetic_2EDIV:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2EDIV,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EDIV(X0,X1)) = ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Earithmetic_2EDIV2,type,(c_2Earithmetic_2EDIV2:$i)).
tff(mem_c_2Earithmetic_2EDIV2,axiom,mem(c_2Earithmetic_2EDIV2,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))).
tff(stp_fo_c_2Earithmetic_2EDIV2,type,(fo__c_2Earithmetic_2EDIV2:(tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2EDIV2,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EDIV2(X0)) = ap(c_2Earithmetic_2EDIV2,inj__ty_2Enum_2Enum(X0))))).
tff(stp_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum,type,(tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum : $tType)).
tff(stp_inj_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum,type,(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum : tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum > $i)).
tff(stp_surj_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum,type,(surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum : $i > tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum)).
tff(stp_inj_surj_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum,axiom,( ! [X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(X)) = X))).
tff(stp_inj_mem_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum,axiom,( ! [X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : (mem(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(X),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)))))).
tff(stp_iso_mem_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum,axiom,( ! [X:$i] : (mem(X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))) => (X = inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(X)))))).
tff(stp_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum,type,(tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum : $tType)).
tff(stp_inj_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum,type,(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum : tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum > $i)).
tff(stp_surj_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum,type,(surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum : $i > tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum)).
tff(stp_inj_surj_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum,axiom,( ! [X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(X)) = X))).
tff(stp_inj_mem_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum,axiom,( ! [X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : (mem(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(X),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))))).
tff(stp_iso_mem_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum,axiom,( ! [X:$i] : (mem(X,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)) => (X = inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(X)))))).
tff(tp_c_2Earithmetic_2EDIVMOD,type,(c_2Earithmetic_2EDIVMOD:$i)).
tff(mem_c_2Earithmetic_2EDIVMOD,axiom,mem(c_2Earithmetic_2EDIVMOD,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)))).
tff(tp_c_2Earithmetic_2EEVEN,type,(c_2Earithmetic_2EEVEN:$i)).
tff(mem_c_2Earithmetic_2EEVEN,axiom,mem(c_2Earithmetic_2EEVEN,arr(ty_2Enum_2Enum,bool))).
tff(stp_fo_c_2Earithmetic_2EEVEN,type,(fo__c_2Earithmetic_2EEVEN:(tp__ty_2Enum_2Enum) > tp__o)).
tff(stp_eq_fo_c_2Earithmetic_2EEVEN,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__o(fo__c_2Earithmetic_2EEVEN(X0)) = ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Earithmetic_2EEXP,type,(c_2Earithmetic_2EEXP:$i)).
tff(mem_c_2Earithmetic_2EEXP,axiom,mem(c_2Earithmetic_2EEXP,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)))).
tff(stp_fo_c_2Earithmetic_2EEXP,type,(fo__c_2Earithmetic_2EEXP:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2EEXP,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EEXP(X0,X1)) = ap(ap(c_2Earithmetic_2EEXP,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Earithmetic_2EFACT,type,(c_2Earithmetic_2EFACT:$i)).
tff(mem_c_2Earithmetic_2EFACT,axiom,mem(c_2Earithmetic_2EFACT,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))).
tff(stp_fo_c_2Earithmetic_2EFACT,type,(fo__c_2Earithmetic_2EFACT:(tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2EFACT,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EFACT(X0)) = ap(c_2Earithmetic_2EFACT,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Earithmetic_2EFUNPOW,type,(c_2Earithmetic_2EFUNPOW:del > $i)).
tff(mem_c_2Earithmetic_2EFUNPOW,axiom,( ! [A_27a:del] : mem(c_2Earithmetic_2EFUNPOW(A_27a),arr(arr(A_27a,A_27a),arr(ty_2Enum_2Enum,arr(A_27a,A_27a)))))).
tff(tp_c_2Earithmetic_2EMAX,type,(c_2Earithmetic_2EMAX:$i)).
tff(mem_c_2Earithmetic_2EMAX,axiom,mem(c_2Earithmetic_2EMAX,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)))).
tff(stp_fo_c_2Earithmetic_2EMAX,type,(fo__c_2Earithmetic_2EMAX:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2EMAX,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EMAX(X0,X1)) = ap(ap(c_2Earithmetic_2EMAX,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Earithmetic_2EMIN,type,(c_2Earithmetic_2EMIN:$i)).
tff(mem_c_2Earithmetic_2EMIN,axiom,mem(c_2Earithmetic_2EMIN,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)))).
tff(stp_fo_c_2Earithmetic_2EMIN,type,(fo__c_2Earithmetic_2EMIN:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2EMIN,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EMIN(X0,X1)) = ap(ap(c_2Earithmetic_2EMIN,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Earithmetic_2EMOD,type,(c_2Earithmetic_2EMOD:$i)).
tff(mem_c_2Earithmetic_2EMOD,axiom,mem(c_2Earithmetic_2EMOD,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)))).
tff(stp_fo_c_2Earithmetic_2EMOD,type,(fo__c_2Earithmetic_2EMOD:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2EMOD,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EMOD(X0,X1)) = ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Earithmetic_2EMODEQ,type,(c_2Earithmetic_2EMODEQ:$i)).
tff(mem_c_2Earithmetic_2EMODEQ,axiom,mem(c_2Earithmetic_2EMODEQ,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool))))).
tff(stp_fo_c_2Earithmetic_2EMODEQ,type,(fo__c_2Earithmetic_2EMODEQ:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__o)).
tff(stp_eq_fo_c_2Earithmetic_2EMODEQ,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : ( ! [X2:tp__ty_2Enum_2Enum] : (inj__o(fo__c_2Earithmetic_2EMODEQ(X0,X1,X2)) = ap(ap(ap(c_2Earithmetic_2EMODEQ,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)),inj__ty_2Enum_2Enum(X2))))))).
tff(tp_c_2Earithmetic_2ENRC,type,(c_2Earithmetic_2ENRC:del > $i)).
tff(mem_c_2Earithmetic_2ENRC,axiom,( ! [A_27a:del] : mem(c_2Earithmetic_2ENRC(A_27a),arr(arr(A_27a,arr(A_27a,bool)),arr(ty_2Enum_2Enum,arr(A_27a,arr(A_27a,bool))))))).
tff(tp_c_2Earithmetic_2ENUMERAL,type,(c_2Earithmetic_2ENUMERAL:$i)).
tff(mem_c_2Earithmetic_2ENUMERAL,axiom,mem(c_2Earithmetic_2ENUMERAL,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))).
tff(stp_fo_c_2Earithmetic_2ENUMERAL,type,(fo__c_2Earithmetic_2ENUMERAL:(tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2ENUMERAL,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2ENUMERAL(X0)) = ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Earithmetic_2EODD,type,(c_2Earithmetic_2EODD:$i)).
tff(mem_c_2Earithmetic_2EODD,axiom,mem(c_2Earithmetic_2EODD,arr(ty_2Enum_2Enum,bool))).
tff(stp_fo_c_2Earithmetic_2EODD,type,(fo__c_2Earithmetic_2EODD:(tp__ty_2Enum_2Enum) > tp__o)).
tff(stp_eq_fo_c_2Earithmetic_2EODD,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__o(fo__c_2Earithmetic_2EODD(X0)) = ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Earithmetic_2EZERO,type,(c_2Earithmetic_2EZERO:$i)).
tff(mem_c_2Earithmetic_2EZERO,axiom,mem(c_2Earithmetic_2EZERO,ty_2Enum_2Enum)).
tff(stp_fo_c_2Earithmetic_2EZERO,type,(fo__c_2Earithmetic_2EZERO:tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2EZERO,axiom,(inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO) = c_2Earithmetic_2EZERO)).
tff(tp_c_2Earithmetic_2Efindq,type,(c_2Earithmetic_2Efindq:$i)).
tff(mem_c_2Earithmetic_2Efindq,axiom,mem(c_2Earithmetic_2Efindq,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),ty_2Enum_2Enum))).
tff(stp_fo_c_2Earithmetic_2Efindq,type,(fo__c_2Earithmetic_2Efindq:(tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2Efindq,axiom,( ! [X0:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2Efindq(X0)) = ap(c_2Earithmetic_2Efindq,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum(X0))))).
tff(tp_c_2Earithmetic_2Enat__elim____magic,type,(c_2Earithmetic_2Enat__elim____magic:$i)).
tff(mem_c_2Earithmetic_2Enat__elim____magic,axiom,mem(c_2Earithmetic_2Enat__elim____magic,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))).
tff(stp_fo_c_2Earithmetic_2Enat__elim____magic,type,(fo__c_2Earithmetic_2Enat__elim____magic:(tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2Enat__elim____magic,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2Enat__elim____magic(X0)) = ap(c_2Earithmetic_2Enat__elim____magic,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Earithmetic_2Enum__CASE,type,(c_2Earithmetic_2Enum__CASE:del > $i)).
tff(mem_c_2Earithmetic_2Enum__CASE,axiom,( ! [A_27a:del] : mem(c_2Earithmetic_2Enum__CASE(A_27a),arr(ty_2Enum_2Enum,arr(A_27a,arr(arr(ty_2Enum_2Enum,A_27a),A_27a)))))).
tff(ax_thm_2Earithmetic_2EADD,axiom,(( ! [V0n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n))) = V0n)) & ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1m))),inj__ty_2Enum_2Enum(V2n))) = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1m)),inj__ty_2Enum_2Enum(V2n))))))))).
tff(ax_thm_2Earithmetic_2ENUMERAL__DEF,axiom,( ! [V0x:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V0x))) = V0x))).
tff(ax_thm_2Earithmetic_2EALT__ZERO,axiom,(fo__c_2Earithmetic_2EZERO = fo__c_2Enum_2E0)).
tff(ax_thm_2Earithmetic_2EBIT1,axiom,( ! [V0n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))).
tff(ax_thm_2Earithmetic_2EBIT2,axiom,( ! [V0n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),ap(c_2Enum_2ESUC,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))))).
tff(ax_thm_2Earithmetic_2Enat__elim____magic,axiom,( ! [V0n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2Enat__elim____magic,inj__ty_2Enum_2Enum(V0n))) = V0n))).
tff(ax_thm_2Earithmetic_2ESUB,axiom,(( ! [V0m:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0m))) = fo__c_2Enum_2E0)) & ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1m))),inj__ty_2Enum_2Enum(V2n))) = surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1m)),inj__ty_2Enum_2Enum(V2n))),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V1m)),inj__ty_2Enum_2Enum(V2n)))))))))).
tff(ax_thm_2Earithmetic_2EMULT,axiom,(( ! [V0n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n))) = fo__c_2Enum_2E0)) & ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1m))),inj__ty_2Enum_2Enum(V2n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V1m)),inj__ty_2Enum_2Enum(V2n))),inj__ty_2Enum_2Enum(V2n)))))))).
tff(ax_thm_2Earithmetic_2EEXP,axiom,(( ! [V0m:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EEXP,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))) & ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EEXP,inj__ty_2Enum_2Enum(V1m)),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V2n)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V1m)),ap(ap(c_2Earithmetic_2EEXP,inj__ty_2Enum_2Enum(V1m)),inj__ty_2Enum_2Enum(V2n))))))))).
tff(ax_thm_2Earithmetic_2EGREATER__DEF,axiom,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3E,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V0m))))))).
tff(ax_thm_2Earithmetic_2ELESS__OR__EQ,axiom,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) <=> (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) | (V0m = V1n)))))).
tff(ax_thm_2Earithmetic_2EGREATER__OR__EQ,axiom,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3E_3D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) <=> (p(ap(ap(c_2Earithmetic_2E_3E,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) | (V0m = V1n)))))).
tff(ax_thm_2Earithmetic_2EEVEN,axiom,((p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) <=> $true) & ( ! [V0n:tp__ty_2Enum_2Enum] : (p(ap(c_2Earithmetic_2EEVEN,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n)))) <=> (~~ p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V0n)))))))).
tff(ax_thm_2Earithmetic_2EODD,axiom,((p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) <=> $false) & ( ! [V0n:tp__ty_2Enum_2Enum] : (p(ap(c_2Earithmetic_2EODD,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n)))) <=> (~~ p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(V0n)))))))).
tff(ax_thm_2Earithmetic_2Enum__case__def,axiom,( ! [A_27a:del]: (( ! [V0v:$i] : (mem(V0v,A_27a) => ( ! [V1f:$i] : (mem(V1f,arr(ty_2Enum_2Enum,A_27a)) => (ap(ap(ap(c_2Earithmetic_2Enum__CASE(A_27a),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),V0v),V1f) = V0v))))) & ( ! [V2n:tp__ty_2Enum_2Enum] : ( ! [V3v:$i] : (mem(V3v,A_27a) => ( ! [V4f:$i] : (mem(V4f,arr(ty_2Enum_2Enum,A_27a)) => (ap(ap(ap(c_2Earithmetic_2Enum__CASE(A_27a),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V2n))),V3v),V4f) = ap(V4f,inj__ty_2Enum_2Enum(V2n))))))))))).
tff(ax_thm_2Earithmetic_2EFUNPOW,axiom,( ! [A_27a:del]: (( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27a)) => ( ! [V1x:$i] : (mem(V1x,A_27a) => (ap(ap(ap(c_2Earithmetic_2EFUNPOW(A_27a),V0f),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),V1x) = V1x))))) & ( ! [V2f:$i] : (mem(V2f,arr(A_27a,A_27a)) => ( ! [V3n:tp__ty_2Enum_2Enum] : ( ! [V4x:$i] : (mem(V4x,A_27a) => (ap(ap(ap(c_2Earithmetic_2EFUNPOW(A_27a),V2f),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V3n))),V4x) = ap(ap(ap(c_2Earithmetic_2EFUNPOW(A_27a),V2f),inj__ty_2Enum_2Enum(V3n)),ap(V2f,V4x))))))))))).
tff(ax_thm_2Earithmetic_2ENRC,axiom,( ! [A_27a:del]: (( ! [V0R:$i] : (mem(V0R,arr(A_27a,arr(A_27a,bool))) => ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2y:$i] : (mem(V2y,A_27a) => (p(ap(ap(ap(ap(c_2Earithmetic_2ENRC(A_27a),V0R),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),V1x),V2y)) <=> (V1x = V2y)))))))) & ( ! [V3R:$i] : (mem(V3R,arr(A_27a,arr(A_27a,bool))) => ( ! [V4n:tp__ty_2Enum_2Enum] : ( ! [V5x:$i] : (mem(V5x,A_27a) => ( ! [V6y:$i] : (mem(V6y,A_27a) => (p(ap(ap(ap(ap(c_2Earithmetic_2ENRC(A_27a),V3R),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V4n))),V5x),V6y)) <=> (? [V7z:$i] : (mem(V7z,A_27a) & (p(ap(ap(V3R,V5x),V7z)) & p(ap(ap(ap(ap(c_2Earithmetic_2ENRC(A_27a),V3R),inj__ty_2Enum_2Enum(V4n)),V7z),V6y)))))))))))))))).
tff(conj_thm_2Earithmetic_2EONE,lemma,((surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))) = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))).
tff(conj_thm_2Earithmetic_2ETWO,lemma,((surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))) = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))).
tff(conj_thm_2Earithmetic_2ENORM__0,lemma,((surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))) = fo__c_2Enum_2E0))).
tff(conj_thm_2Earithmetic_2Enum__case__compute,lemma,(( ! [A_27a:del]: ( ! [V0f:$i] : (mem(V0f,A_27a) => ( ! [V1g:$i] : (mem(V1g,arr(ty_2Enum_2Enum,A_27a)) => ( ! [V2n:tp__ty_2Enum_2Enum] : (ap(ap(ap(c_2Earithmetic_2Enum__CASE(A_27a),inj__ty_2Enum_2Enum(V2n)),V0f),V1g) = ap(ap(ap(c_2Ebool_2ECOND(A_27a),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V2n)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),V0f),ap(V1g,ap(c_2Eprim__rec_2EPRE,inj__ty_2Enum_2Enum(V2n))))))))))))).
tff(conj_thm_2Earithmetic_2ESUC__NOT,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (~~ (fo__c_2Enum_2E0 = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n)))))))).
tff(conj_thm_2Earithmetic_2EADD__0,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = V0m)))).
tff(conj_thm_2Earithmetic_2EADD__SUC,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1n))))))))).
tff(conj_thm_2Earithmetic_2EADD__CLAUSES,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0m))) = V0m) & ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = V0m) & ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0m))),inj__ty_2Enum_2Enum(V1n))) = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))))) & (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1n)))) = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))))))))))).
tff(conj_thm_2Earithmetic_2EADD__SYM,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V0m)))))))).
tff(conj_thm_2Earithmetic_2EADD__COMM,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V0m)))))))).
tff(conj_thm_2Earithmetic_2EADD__ASSOC,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(V2p))))))))).
tff(conj_thm_2Earithmetic_2Enum__CASES,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ((V0m = fo__c_2Enum_2E0) | (? [V1n:tp__ty_2Enum_2Enum] : (V0m = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1n))))))))).
tff(conj_thm_2Earithmetic_2ENOT__ZERO__LT__ZERO,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ((~~ (V0n = fo__c_2Enum_2E0)) <=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n))))))).
tff(conj_thm_2Earithmetic_2ENOT__LT__ZERO__EQ__ZERO,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ((~~ p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n)))) <=> (V0n = fo__c_2Enum_2E0))))).
tff(conj_thm_2Earithmetic_2ELESS__OR__EQ__ALT,lemma,((c_2Earithmetic_2E_3C_3D = ap(c_2Erelation_2ERTC(ty_2Enum_2Enum),f159)))).
tff(conj_thm_2Earithmetic_2ELESS__ADD,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V0m))) => (? [V2p:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V2p)),inj__ty_2Enum_2Enum(V1n))) = V0m))))))).
tff(conj_thm_2Earithmetic_2Etransitive__LESS,lemma,(p(ap(c_2Erelation_2Etransitive(ty_2Enum_2Enum),c_2Eprim__rec_2E_3C)))).
tff(conj_thm_2Earithmetic_2ELESS__TRANS,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p)))) => p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2p))))))))).
tff(conj_thm_2Earithmetic_2ELESS__ANTISYM,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (~~ (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V0m))))))))).
tff(conj_thm_2Earithmetic_2ELESS__MONO__REV,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0m))),ap(c_2Enum_2ESUC,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_2Earithmetic_2ELESS__MONO__EQ,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0m))),ap(c_2Enum_2ESUC,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_2Earithmetic_2ELESS__EQ__MONO,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1m)))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))))))).
tff(conj_thm_2Earithmetic_2ELESS__LESS__SUC,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (~~ (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1n)),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0m)))))))))).
tff(conj_thm_2Earithmetic_2Etransitive__measure,lemma,(( ! [A_27a:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,ty_2Enum_2Enum)) => p(ap(c_2Erelation_2Etransitive(A_27a),ap(c_2Eprim__rec_2Emeasure(A_27a),V0f)))))))).
tff(conj_thm_2Earithmetic_2ELESS__EQ,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0m))),inj__ty_2Enum_2Enum(V1n)))))))).
tff(conj_thm_2Earithmetic_2ELESS__OR,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) => p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0m))),inj__ty_2Enum_2Enum(V1n)))))))).
tff(conj_thm_2Earithmetic_2EOR__LESS,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0m))),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_2Earithmetic_2ELESS__EQ__IFF__LESS__SUC,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0n)),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1m))))))))).
tff(conj_thm_2Earithmetic_2ELESS__EQ__IMP__LESS__SUC,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m))) => p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0n)),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1m))))))))).
tff(conj_thm_2Earithmetic_2EZERO__LESS__EQ,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n)))))).
tff(conj_thm_2Earithmetic_2ELESS__SUC__EQ__COR,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) & (~~ (surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0m))) = V1n))) => p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0m))),inj__ty_2Enum_2Enum(V1n)))))))).
tff(conj_thm_2Earithmetic_2ELESS__NOT__SUC,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) & (~~ (V1n = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0m)))))) => p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0m))),inj__ty_2Enum_2Enum(V1n)))))))).
tff(conj_thm_2Earithmetic_2ELESS__0__CASES,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ((fo__c_2Enum_2E0 = V0m) | p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0m))))))).
tff(conj_thm_2Earithmetic_2ELESS__CASES__IMP,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (((~~ p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))) & (~~ (V0m = V1n))) => p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V0m)))))))).
tff(conj_thm_2Earithmetic_2ELESS__CASES,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) | p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V0m)))))))).
tff(conj_thm_2Earithmetic_2EADD__INV__0,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) = V0m) => (V1n = fo__c_2Enum_2E0)))))).
tff(conj_thm_2Earithmetic_2ELESS__EQ__ADD,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))))))).
tff(conj_thm_2Earithmetic_2ELESS__EQ__ADD__EXISTS,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V0m))) => (? [V2p:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V2p)),inj__ty_2Enum_2Enum(V1n))) = V0m))))))).
tff(conj_thm_2Earithmetic_2ELESS__STRONG__ADD,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V0m))) => (? [V2p:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V2p))),inj__ty_2Enum_2Enum(V1n))) = V0m))))))).
tff(conj_thm_2Earithmetic_2ELESS__EQ__SUC__REFL,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0m))))))).
tff(conj_thm_2Earithmetic_2ELESS__ADD__NONZERO,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((~~ (V1n = fo__c_2Enum_2E0)) => p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0m)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))))))))).
tff(conj_thm_2Earithmetic_2ENOT__SUC__LESS__EQ__0,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (~~ p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))).
tff(conj_thm_2Earithmetic_2ENOT__LESS,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((~~ p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V0m)))))))).
tff(conj_thm_2Earithmetic_2ENOT__LESS__EQUAL,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((~~ p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V0m)))))))).
tff(conj_thm_2Earithmetic_2ELESS__EQ__ANTISYM,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (~~ (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) & p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V0m))))))))).
tff(conj_thm_2Earithmetic_2ELESS__EQ__0,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) <=> (V0n = fo__c_2Enum_2E0))))).
tff(conj_thm_2Earithmetic_2ESUB__0,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0m))) = fo__c_2Enum_2E0) & (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = V0m))))).
tff(conj_thm_2Earithmetic_2ESUB__MONO__EQ,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1m)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))))))).
tff(conj_thm_2Earithmetic_2ESUB__EQ__0,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) = fo__c_2Enum_2E0) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))))))).
tff(conj_thm_2Earithmetic_2EADD1,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0m))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))).
tff(conj_thm_2Earithmetic_2ESUC__SUB1,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0m))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) = V0m)))).
tff(conj_thm_2Earithmetic_2EPRE__SUB1,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Eprim__rec_2EPRE,inj__ty_2Enum_2Enum(V0m))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0m)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))).
tff(conj_thm_2Earithmetic_2EMULT__0,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = fo__c_2Enum_2E0)))).
tff(conj_thm_2Earithmetic_2EMULT__SUC,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1n)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))))))))).
tff(conj_thm_2Earithmetic_2EMULT__LEFT__1,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(V0m))) = V0m)))).
tff(conj_thm_2Earithmetic_2EMULT__RIGHT__1,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) = V0m)))).
tff(conj_thm_2Earithmetic_2EMULT__CLAUSES,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0m))) = fo__c_2Enum_2E0) & ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = fo__c_2Enum_2E0) & ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(V0m))) = V0m) & ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) = V0m) & ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0m))),inj__ty_2Enum_2Enum(V1n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(V1n)))) & (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1n)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))))))))))))).
tff(conj_thm_2Earithmetic_2EMULT__SYM,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V0m)))))))).
tff(conj_thm_2Earithmetic_2EMULT__COMM,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V0m)))))))).
tff(conj_thm_2Earithmetic_2ERIGHT__ADD__DISTRIB,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(V2p))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2p))),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p)))))))))).
tff(conj_thm_2Earithmetic_2ELEFT__ADD__DISTRIB,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V2p)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V2p)),inj__ty_2Enum_2Enum(V0m))),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V2p)),inj__ty_2Enum_2Enum(V1n)))))))))).
tff(conj_thm_2Earithmetic_2EMULT__ASSOC,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(V2p))))))))).
tff(conj_thm_2Earithmetic_2ESUB__ADD,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V0m))) => (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(V1n))) = V0m)))))).
tff(conj_thm_2Earithmetic_2EPRE__SUB,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Eprim__rec_2EPRE,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,ap(c_2Eprim__rec_2EPRE,inj__ty_2Enum_2Enum(V0m))),inj__ty_2Enum_2Enum(V1n)))))))).
tff(conj_thm_2Earithmetic_2EADD__EQ__0,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) = fo__c_2Enum_2E0) <=> ((V0m = fo__c_2Enum_2E0) & (V1n = fo__c_2Enum_2E0))))))).
tff(conj_thm_2Earithmetic_2EADD__EQ__1,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) <=> (((V0m = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) & (V1n = fo__c_2Enum_2E0)) | ((V0m = fo__c_2Enum_2E0) & (V1n = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))).
tff(conj_thm_2Earithmetic_2EADD__INV__0__EQ,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) = V0m) <=> (V1n = fo__c_2Enum_2E0)))))).
tff(conj_thm_2Earithmetic_2EPRE__SUC__EQ,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V1n))) => ((V0m = surj__ty_2Enum_2Enum(ap(c_2Eprim__rec_2EPRE,inj__ty_2Enum_2Enum(V1n)))) <=> (surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0m))) = V1n))))))).
tff(conj_thm_2Earithmetic_2EINV__PRE__EQ,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0m))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V1n)))) => ((surj__ty_2Enum_2Enum(ap(c_2Eprim__rec_2EPRE,inj__ty_2Enum_2Enum(V0m))) = surj__ty_2Enum_2Enum(ap(c_2Eprim__rec_2EPRE,inj__ty_2Enum_2Enum(V1n)))) <=> (V0m = V1n))))))).
tff(conj_thm_2Earithmetic_2ELESS__SUC__NOT,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) => (~~ p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1n)),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0m)))))))))).
tff(conj_thm_2Earithmetic_2EADD__EQ__SUB,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p))) => ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) = V2p) <=> (V0m = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V2p)),inj__ty_2Enum_2Enum(V1n))))))))))).
tff(conj_thm_2Earithmetic_2ELESS__MONO__ADD,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) => p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2p))),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p)))))))))).
tff(conj_thm_2Earithmetic_2ELESS__MONO__ADD__INV,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2p))),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p)))) => p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))))))))).
tff(conj_thm_2Earithmetic_2ELESS__MONO__ADD__EQ,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2p))),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p)))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))))))))).
tff(conj_thm_2Earithmetic_2ELT__ADD__RCANCEL,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2p))),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p)))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))))))))).
tff(conj_thm_2Earithmetic_2ELT__ADD__LCANCEL,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V2p)),inj__ty_2Enum_2Enum(V0m))),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V2p)),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_2Earithmetic_2EEQ__MONO__ADD__EQ,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2p))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p)))) <=> (V0m = V1n))))))).
tff(conj_thm_2Earithmetic_2ELESS__EQ__MONO__ADD__EQ,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2p))),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p)))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))))))))).
tff(conj_thm_2Earithmetic_2ELESS__EQ__TRANS,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) & p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p)))) => p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2p))))))))).
tff(conj_thm_2Earithmetic_2ELESS__EQ__LESS__TRANS,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p)))) => p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2p))))))))).
tff(conj_thm_2Earithmetic_2ELESS__LESS__EQ__TRANS,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) & p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p)))) => p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2p))))))))).
tff(conj_thm_2Earithmetic_2ELESS__EQ__LESS__EQ__MONO,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : ( ! [V3q:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2p))) & p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V3q)))) => p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V2p)),inj__ty_2Enum_2Enum(V3q))))))))))).
tff(conj_thm_2Earithmetic_2ELESS__EQ__REFL,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V0m)))))).
tff(conj_thm_2Earithmetic_2ELESS__IMP__LESS__OR__EQ,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) => p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))))))).
tff(conj_thm_2Earithmetic_2ELESS__MONO__MULT,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) => p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2p))),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p)))))))))).
tff(conj_thm_2Earithmetic_2ELESS__MONO__MULT2,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2i:tp__ty_2Enum_2Enum] : ( ! [V3j:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2i))) & p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V3j)))) => p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V2i)),inj__ty_2Enum_2Enum(V3j))))))))))).
tff(conj_thm_2Earithmetic_2ERIGHT__SUB__DISTRIB,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(V2p))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2p))),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p)))))))))).
tff(conj_thm_2Earithmetic_2ELEFT__SUB__DISTRIB,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V2p)),ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V2p)),inj__ty_2Enum_2Enum(V0m))),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V2p)),inj__ty_2Enum_2Enum(V1n)))))))))).
tff(conj_thm_2Earithmetic_2ELESS__ADD__1,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V0m))) => (? [V2p:tp__ty_2Enum_2Enum] : (V0m = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1n)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V2p)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))))))).
tff(conj_thm_2Earithmetic_2EEXP__ADD,lemma,(( ! [V0p:tp__ty_2Enum_2Enum] : ( ! [V1q:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EEXP,inj__ty_2Enum_2Enum(V2n)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0p)),inj__ty_2Enum_2Enum(V1q)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(ap(c_2Earithmetic_2EEXP,inj__ty_2Enum_2Enum(V2n)),inj__ty_2Enum_2Enum(V0p))),ap(ap(c_2Earithmetic_2EEXP,inj__ty_2Enum_2Enum(V2n)),inj__ty_2Enum_2Enum(V1q)))))))))).
tff(conj_thm_2Earithmetic_2ENOT__ODD__EQ__EVEN,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : (~~ (surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V0n)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1m)),inj__ty_2Enum_2Enum(V1m))))))))).
tff(conj_thm_2Earithmetic_2ELESS__EQUAL__ANTISYM,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m))) & p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1m)),inj__ty_2Enum_2Enum(V0n)))) => (V0n = V1m)))))).
tff(conj_thm_2Earithmetic_2ELESS__ADD__SUC,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0m)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1n))))))))).
tff(conj_thm_2Earithmetic_2ELESS__OR__EQ__ADD,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m))) | (? [V2p:tp__ty_2Enum_2Enum] : (V0n = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V2p)),inj__ty_2Enum_2Enum(V1m)))))))))).
tff(conj_thm_2Earithmetic_2EWOP,lemma,(( ! [V0P:$i] : (mem(V0P,arr(ty_2Enum_2Enum,bool)) => ((? [V1n:tp__ty_2Enum_2Enum] : p(ap(V0P,inj__ty_2Enum_2Enum(V1n)))) => (? [V2n:tp__ty_2Enum_2Enum] : (p(ap(V0P,inj__ty_2Enum_2Enum(V2n))) & ( ! [V3m:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V3m)),inj__ty_2Enum_2Enum(V2n))) => (~~ p(ap(V0P,inj__ty_2Enum_2Enum(V3m))))))))))))).
tff(conj_thm_2Earithmetic_2ECOMPLETE__INDUCTION,lemma,(( ! [V0P:$i] : (mem(V0P,arr(ty_2Enum_2Enum,bool)) => (( ! [V1n:tp__ty_2Enum_2Enum] : (( ! [V2m:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V2m)),inj__ty_2Enum_2Enum(V1n))) => p(ap(V0P,inj__ty_2Enum_2Enum(V2m))))) => p(ap(V0P,inj__ty_2Enum_2Enum(V1n))))) => ( ! [V3n:tp__ty_2Enum_2Enum] : p(ap(V0P,inj__ty_2Enum_2Enum(V3n))))))))).
tff(conj_thm_2Earithmetic_2EFORALL__NUM__THM,lemma,(( ! [V0P:$i] : (mem(V0P,arr(ty_2Enum_2Enum,bool)) => (( ! [V1n:tp__ty_2Enum_2Enum] : p(ap(V0P,inj__ty_2Enum_2Enum(V1n)))) <=> (p(ap(V0P,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) & ( ! [V2n:tp__ty_2Enum_2Enum] : (p(ap(V0P,inj__ty_2Enum_2Enum(V2n))) => p(ap(V0P,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V2n)))))))))))).
tff(conj_thm_2Earithmetic_2ESUC__SUB,lemma,(( ! [V0a:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0a))),inj__ty_2Enum_2Enum(V0a))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))).
tff(conj_thm_2Earithmetic_2ESUB__PLUS,lemma,(( ! [V0a:tp__ty_2Enum_2Enum] : ( ! [V1b:tp__ty_2Enum_2Enum] : ( ! [V2c:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0a)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1b)),inj__ty_2Enum_2Enum(V2c)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0a)),inj__ty_2Enum_2Enum(V1b))),inj__ty_2Enum_2Enum(V2c))))))))).
tff(conj_thm_2Earithmetic_2EINV__PRE__LESS,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0m))) => ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Eprim__rec_2EPRE,inj__ty_2Enum_2Enum(V0m))),ap(c_2Eprim__rec_2EPRE,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_2Earithmetic_2EINV__PRE__LESS__EQ,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n))) => ( ! [V1m:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Eprim__rec_2EPRE,inj__ty_2Enum_2Enum(V1m))),ap(c_2Eprim__rec_2EPRE,inj__ty_2Enum_2Enum(V0n)))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1m)),inj__ty_2Enum_2Enum(V0n))))))))).
tff(conj_thm_2Earithmetic_2EPRE__LESS__EQ,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) => p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Eprim__rec_2EPRE,inj__ty_2Enum_2Enum(V0m))),ap(c_2Eprim__rec_2EPRE,inj__ty_2Enum_2Enum(V1n))))))))).
tff(conj_thm_2Earithmetic_2ESUB__LESS__EQ,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m))),inj__ty_2Enum_2Enum(V0n))))))).
tff(conj_thm_2Earithmetic_2ESUB__EQ__EQ__0,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) = V0m) <=> ((V0m = fo__c_2Enum_2E0) | (V1n = fo__c_2Enum_2E0))))))).
tff(conj_thm_2Earithmetic_2ESUB__LESS__0,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1m)),inj__ty_2Enum_2Enum(V0n))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m))))))))).
tff(conj_thm_2Earithmetic_2ESUB__LESS__OR,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V0m))) => p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1n)),ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0m)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))))).
tff(conj_thm_2Earithmetic_2ELESS__SUB__ADD__LESS,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2i:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V2i)),ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))) => p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V2i)),inj__ty_2Enum_2Enum(V1m))),inj__ty_2Enum_2Enum(V0n))))))))).
tff(conj_thm_2Earithmetic_2ETIMES2,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V0n))))))).
tff(conj_thm_2Earithmetic_2ELESS__MULT__MONO,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1i:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2A,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V2n))),inj__ty_2Enum_2Enum(V0m))),ap(ap(c_2Earithmetic_2E_2A,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V2n))),inj__ty_2Enum_2Enum(V1i)))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1i))))))))).
tff(conj_thm_2Earithmetic_2EMULT__MONO__EQ,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1i:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V2n))),inj__ty_2Enum_2Enum(V0m))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V2n))),inj__ty_2Enum_2Enum(V1i)))) <=> (V0m = V1i))))))).
tff(conj_thm_2Earithmetic_2EMULT__SUC__EQ,lemma,(( ! [V0p:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V2n)),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0p)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V1m)),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0p))))) <=> (V2n = V1m))))))).
tff(conj_thm_2Earithmetic_2EMULT__EXP__MONO,lemma,(( ! [V0p:tp__ty_2Enum_2Enum] : ( ! [V1q:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : ( ! [V3m:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V2n)),ap(ap(c_2Earithmetic_2EEXP,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1q))),inj__ty_2Enum_2Enum(V0p)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V3m)),ap(ap(c_2Earithmetic_2EEXP,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1q))),inj__ty_2Enum_2Enum(V0p))))) <=> (V2n = V3m)))))))).
tff(conj_thm_2Earithmetic_2EEQ__ADD__LCANCEL,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2p)))) <=> (V1n = V2p))))))).
tff(conj_thm_2Earithmetic_2EEQ__ADD__RCANCEL,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2p))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p)))) <=> (V0m = V1n))))))).
tff(conj_thm_2Earithmetic_2EEQ__MULT__LCANCEL,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2p)))) <=> ((V0m = fo__c_2Enum_2E0) | (V1n = V2p)))))))).
tff(conj_thm_2Earithmetic_2EEQ__MULT__RCANCEL,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V0m))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V2p)),inj__ty_2Enum_2Enum(V0m)))) <=> ((V0m = fo__c_2Enum_2E0) | (V1n = V2p)))))))).
tff(conj_thm_2Earithmetic_2EADD__SUB,lemma,(( ! [V0a:tp__ty_2Enum_2Enum] : ( ! [V1c:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0a)),inj__ty_2Enum_2Enum(V1c))),inj__ty_2Enum_2Enum(V1c))) = V0a))))).
tff(conj_thm_2Earithmetic_2ELESS__EQ__ADD__SUB,lemma,(( ! [V0c:tp__ty_2Enum_2Enum] : ( ! [V1b:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0c)),inj__ty_2Enum_2Enum(V1b))) => ( ! [V2a:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V2a)),inj__ty_2Enum_2Enum(V1b))),inj__ty_2Enum_2Enum(V0c))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V2a)),ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V1b)),inj__ty_2Enum_2Enum(V0c))))))))))).
tff(conj_thm_2Earithmetic_2ESUB__EQUAL__0,lemma,(( ! [V0c:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0c)),inj__ty_2Enum_2Enum(V0c))) = fo__c_2Enum_2E0)))).
tff(conj_thm_2Earithmetic_2ELESS__EQ__SUB__LESS,lemma,(( ! [V0a:tp__ty_2Enum_2Enum] : ( ! [V1b:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1b)),inj__ty_2Enum_2Enum(V0a))) => ( ! [V2c:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0a)),inj__ty_2Enum_2Enum(V1b))),inj__ty_2Enum_2Enum(V2c))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0a)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1b)),inj__ty_2Enum_2Enum(V2c))))))))))).
tff(conj_thm_2Earithmetic_2ENOT__SUC__LESS__EQ,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ((~~ p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),inj__ty_2Enum_2Enum(V1m)))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1m)),inj__ty_2Enum_2Enum(V0n)))))))).
tff(conj_thm_2Earithmetic_2ESUB__SUB,lemma,(( ! [V0b:tp__ty_2Enum_2Enum] : ( ! [V1c:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1c)),inj__ty_2Enum_2Enum(V0b))) => ( ! [V2a:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V2a)),ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0b)),inj__ty_2Enum_2Enum(V1c)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V2a)),inj__ty_2Enum_2Enum(V1c))),inj__ty_2Enum_2Enum(V0b)))))))))).
tff(conj_thm_2Earithmetic_2ELESS__IMP__LESS__ADD,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m))) => ( ! [V2p:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0n)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1m)),inj__ty_2Enum_2Enum(V2p)))))))))).
tff(conj_thm_2Earithmetic_2ESUB__LESS__EQ__ADD,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1p:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1p))) => ( ! [V2n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V1p)),inj__ty_2Enum_2Enum(V0m))),inj__ty_2Enum_2Enum(V2n))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1p)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2n))))))))))).
tff(conj_thm_2Earithmetic_2ESUB__LESS__SUC,lemma,(( ! [V0p:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0p)),inj__ty_2Enum_2Enum(V1m))),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0p)))))))).
tff(conj_thm_2Earithmetic_2ESUB__CANCEL,lemma,(( ! [V0p:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2m:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V0p))) & p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V2m)),inj__ty_2Enum_2Enum(V0p)))) => ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0p)),inj__ty_2Enum_2Enum(V1n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0p)),inj__ty_2Enum_2Enum(V2m)))) <=> (V1n = V2m)))))))).
tff(conj_thm_2Earithmetic_2ECANCEL__SUB,lemma,(( ! [V0p:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2m:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0p)),inj__ty_2Enum_2Enum(V1n))) & p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0p)),inj__ty_2Enum_2Enum(V2m)))) => ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V0p))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V2m)),inj__ty_2Enum_2Enum(V0p)))) <=> (V1n = V2m)))))))).
tff(conj_thm_2Earithmetic_2ENOT__EXP__0,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (~~ (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EEXP,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(V0m))) = fo__c_2Enum_2E0)))))).
tff(conj_thm_2Earithmetic_2EZERO__LESS__EXP,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(ap(c_2Earithmetic_2EEXP,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(V0m)))))))).
tff(conj_thm_2Earithmetic_2EODD__OR__EVEN,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (? [V1m:tp__ty_2Enum_2Enum] : ((V0n = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(c_2Enum_2ESUC,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))),inj__ty_2Enum_2Enum(V1m)))) | (V0n = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,ap(c_2Enum_2ESUC,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))),inj__ty_2Enum_2Enum(V1m))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))))).
tff(conj_thm_2Earithmetic_2ELESS__EXP__SUC__MONO,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2EEXP,ap(c_2Enum_2ESUC,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1m)))),inj__ty_2Enum_2Enum(V0n))),ap(ap(c_2Earithmetic_2EEXP,ap(c_2Enum_2ESUC,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1m)))),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))))))))).
tff(conj_thm_2Earithmetic_2ELESS__LESS__CASES,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((V0m = V1n) | (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) | p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V0m))))))))).
tff(conj_thm_2Earithmetic_2EGREATER__EQ,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3E_3D,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1m)),inj__ty_2Enum_2Enum(V0n)))))))).
tff(conj_thm_2Earithmetic_2ELESS__EQ__CASES,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) | p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V0m)))))))).
tff(conj_thm_2Earithmetic_2ELESS__EQUAL__ADD,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) => (? [V2p:tp__ty_2Enum_2Enum] : (V1n = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2p)))))))))).
tff(conj_thm_2Earithmetic_2ELESS__EQ__EXISTS,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) <=> (? [V2p:tp__ty_2Enum_2Enum] : (V1n = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2p)))))))))).
tff(conj_thm_2Earithmetic_2EMULT__EQ__0,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) = fo__c_2Enum_2E0) <=> ((V0m = fo__c_2Enum_2E0) | (V1n = fo__c_2Enum_2E0))))))).
tff(conj_thm_2Earithmetic_2EMULT__EQ__1,lemma,(( ! [V0x:tp__ty_2Enum_2Enum] : ( ! [V1y:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V1y))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) <=> ((V0x = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) & (V1y = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))))).
tff(conj_thm_2Earithmetic_2EMULT__EQ__ID,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) = V1n) <=> ((V0m = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) | (V1n = fo__c_2Enum_2E0))))))).
tff(conj_thm_2Earithmetic_2ELESS__MULT2,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0m))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V1n)))) => p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))))))))).
tff(conj_thm_2Earithmetic_2EZERO__LESS__MULT,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))) <=> (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0m))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V1n))))))))).
tff(conj_thm_2Earithmetic_2EZERO__LESS__ADD,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))) <=> (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0m))) | p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V1n))))))))).
tff(ax_thm_2Earithmetic_2EFACT,axiom,((surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EFACT,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) & ( ! [V0n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EFACT,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EFACT,inj__ty_2Enum_2Enum(V0n)))))))).
tff(conj_thm_2Earithmetic_2EFACT__LESS,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(c_2Earithmetic_2EFACT,inj__ty_2Enum_2Enum(V0n))))))).
tff(conj_thm_2Earithmetic_2EEVEN__ODD,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V0n))) <=> (~~ p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(V0n)))))))).
tff(conj_thm_2Earithmetic_2EODD__EVEN,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(V0n))) <=> (~~ p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V0n)))))))).
tff(conj_thm_2Earithmetic_2EEVEN__OR__ODD,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V0n))) | p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(V0n))))))).
tff(conj_thm_2Earithmetic_2EEVEN__AND__ODD,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (~~ (p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V0n))) & p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(V0n)))))))).
tff(conj_thm_2Earithmetic_2EEVEN__ADD,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(c_2Earithmetic_2EEVEN,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))) <=> (p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V0m))) <=> p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V1n))))))))).
tff(conj_thm_2Earithmetic_2EEVEN__MULT,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(c_2Earithmetic_2EEVEN,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))) <=> (p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V0m))) | p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V1n))))))))).
tff(conj_thm_2Earithmetic_2EODD__ADD,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(c_2Earithmetic_2EODD,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))) <=> (~~ (p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(V0m))) <=> p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(V1n)))))))))).
tff(conj_thm_2Earithmetic_2EODD__MULT,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(c_2Earithmetic_2EODD,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))) <=> (p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(V0m))) & p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(V1n))))))))).
tff(conj_thm_2Earithmetic_2EEVEN__DOUBLE,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : p(ap(c_2Earithmetic_2EEVEN,ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(V0n))))))).
tff(conj_thm_2Earithmetic_2EODD__DOUBLE,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : p(ap(c_2Earithmetic_2EODD,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(V0n)))))))).
tff(conj_thm_2Earithmetic_2EEVEN__ODD__EXISTS,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ((p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V0n))) => (? [V1m:tp__ty_2Enum_2Enum] : (V0n = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(V1m)))))) & (p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(V0n))) => (? [V2m:tp__ty_2Enum_2Enum] : (V0n = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(V2m))))))))))).
tff(conj_thm_2Earithmetic_2EEVEN__EXISTS,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V0n))) <=> (? [V1m:tp__ty_2Enum_2Enum] : (V0n = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(V1m))))))))).
tff(conj_thm_2Earithmetic_2EODD__EXISTS,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(V0n))) <=> (? [V1m:tp__ty_2Enum_2Enum] : (V0n = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(V1m)))))))))).
tff(conj_thm_2Earithmetic_2EEVEN__EXP__IFF,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : (p(ap(c_2Earithmetic_2EEVEN,ap(ap(c_2Earithmetic_2EEXP,inj__ty_2Enum_2Enum(V1m)),inj__ty_2Enum_2Enum(V0n)))) <=> (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n))) & p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V1m))))))))).
tff(conj_thm_2Earithmetic_2EEVEN__EXP,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V1n))) & p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V0m)))) => p(ap(c_2Earithmetic_2EEVEN,ap(ap(c_2Earithmetic_2EEXP,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))))))))).
tff(conj_thm_2Earithmetic_2EODD__EXP__IFF,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : (p(ap(c_2Earithmetic_2EODD,ap(ap(c_2Earithmetic_2EEXP,inj__ty_2Enum_2Enum(V1m)),inj__ty_2Enum_2Enum(V0n)))) <=> ((V0n = fo__c_2Enum_2E0) | p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(V1m))))))))).
tff(conj_thm_2Earithmetic_2EODD__EXP,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V1n))) & p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(V0m)))) => p(ap(c_2Earithmetic_2EODD,ap(ap(c_2Earithmetic_2EEXP,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))))))))).
tff(conj_thm_2Earithmetic_2EEQ__LESS__EQ,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((V0m = V1n) <=> (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) & p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V0m))))))))).
tff(conj_thm_2Earithmetic_2EADD__MONO__LESS__EQ,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2p)))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p))))))))).
tff(conj_thm_2Earithmetic_2ELE__ADD__LCANCEL,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2p)))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p))))))))).
tff(conj_thm_2Earithmetic_2ELE__ADD__RCANCEL,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V0m))),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V2p)),inj__ty_2Enum_2Enum(V0m)))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p))))))))).
tff(conj_thm_2Earithmetic_2ENOT__LEQ,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((~~ p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(V0m)))))))).
tff(conj_thm_2Earithmetic_2ENOT__NUM__EQ,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((~~ (V0m = V1n)) <=> (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0m))),inj__ty_2Enum_2Enum(V1n))) | p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(V0m))))))))).
tff(conj_thm_2Earithmetic_2ENOT__GREATER,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((~~ p(ap(ap(c_2Earithmetic_2E_3E,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))))))).
tff(conj_thm_2Earithmetic_2ENOT__GREATER__EQ,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((~~ p(ap(ap(c_2Earithmetic_2E_3E_3D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0m))),inj__ty_2Enum_2Enum(V1n)))))))).
tff(conj_thm_2Earithmetic_2ESUC__ONE__ADD,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(V0n))))))).
tff(conj_thm_2Earithmetic_2ESUC__ADD__SYM,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(V0m)))))))).
tff(conj_thm_2Earithmetic_2ENOT__SUC__ADD__LESS__EQ,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (~~ p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))),inj__ty_2Enum_2Enum(V0m)))))))).
tff(conj_thm_2Earithmetic_2EMULT__LESS__EQ__SUC,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2A,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V2p))),inj__ty_2Enum_2Enum(V0m))),ap(ap(c_2Earithmetic_2E_2A,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V2p))),inj__ty_2Enum_2Enum(V1n)))))))))).
tff(conj_thm_2Earithmetic_2ELE__MULT__LCANCEL,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2p)))) <=> ((V0m = fo__c_2Enum_2E0) | p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p)))))))))).
tff(conj_thm_2Earithmetic_2ELE__MULT__RCANCEL,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V2p)),inj__ty_2Enum_2Enum(V1n)))) <=> ((V1n = fo__c_2Enum_2E0) | p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2p)))))))))).
tff(conj_thm_2Earithmetic_2ELT__MULT__LCANCEL,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2p)))) <=> (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0m))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p)))))))))).
tff(conj_thm_2Earithmetic_2ELT__MULT__RCANCEL,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V2p)),inj__ty_2Enum_2Enum(V1n)))) <=> (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V1n))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2p)))))))))).
tff(conj_thm_2Earithmetic_2ELT__MULT__CANCEL__LBARE,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0m)),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))) <=> (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0m))) & p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(V1n))))) & (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0m)),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V0m)))) <=> (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0m))) & p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(V1n)))))))))).
tff(conj_thm_2Earithmetic_2ELT__MULT__CANCEL__RBARE,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(V0m))) <=> (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0m))) & (V1n = fo__c_2Enum_2E0))) & (p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(V1n))) <=> (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V1n))) & (V0m = fo__c_2Enum_2E0)))))))).
tff(conj_thm_2Earithmetic_2ELE__MULT__CANCEL__LBARE,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))) <=> ((V0m = fo__c_2Enum_2E0) | p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V1n))))) & (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V0m)))) <=> ((V0m = fo__c_2Enum_2E0) | p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V1n)))))))))).
tff(conj_thm_2Earithmetic_2ELE__MULT__CANCEL__RBARE,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(V0m))) <=> ((V0m = fo__c_2Enum_2E0) | p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1n)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) & (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(V1n))) <=> ((V1n = fo__c_2Enum_2E0) | p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))).
tff(conj_thm_2Earithmetic_2ESUB__LEFT__ADD,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p)))) = surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p))),inj__ty_2Enum_2Enum(V0m)),ap(ap(c_2Earithmetic_2E_2D,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(V2p)))))))))).
tff(conj_thm_2Earithmetic_2ESUB__RIGHT__ADD,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(V2p))) = surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(V2p)),ap(ap(c_2Earithmetic_2E_2D,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2p))),inj__ty_2Enum_2Enum(V1n)))))))))).
tff(conj_thm_2Earithmetic_2ESUB__LEFT__SUB,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0m)),ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p)))) = surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p))),inj__ty_2Enum_2Enum(V0m)),ap(ap(c_2Earithmetic_2E_2D,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2p))),inj__ty_2Enum_2Enum(V1n)))))))))).
tff(conj_thm_2Earithmetic_2ESUB__RIGHT__SUB,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(V2p))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0m)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p)))))))))).
tff(conj_thm_2Earithmetic_2ESUB__LEFT__SUC,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))) = surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(ap(c_2Earithmetic_2E_2D,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0m))),inj__ty_2Enum_2Enum(V1n))))))))).
tff(conj_thm_2Earithmetic_2ESUB__LEFT__LESS__EQ,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p)))) <=> (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2p))),inj__ty_2Enum_2Enum(V1n))) | p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))))).
tff(conj_thm_2Earithmetic_2ESUB__RIGHT__LESS__EQ,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(V2p))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p)))))))))).
tff(conj_thm_2Earithmetic_2ESUB__LEFT__LESS,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0m)),ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p)))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2p))),inj__ty_2Enum_2Enum(V1n))))))))).
tff(conj_thm_2Earithmetic_2ESUB__RIGHT__LESS,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(V2p))) <=> (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0m)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p)))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V2p)))))))))).
tff(conj_thm_2Earithmetic_2ESUB__LEFT__GREATER__EQ,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3E_3D,inj__ty_2Enum_2Enum(V0m)),ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p)))) <=> p(ap(ap(c_2Earithmetic_2E_3E_3D,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2p))),inj__ty_2Enum_2Enum(V1n))))))))).
tff(conj_thm_2Earithmetic_2ESUB__RIGHT__GREATER__EQ,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3E_3D,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(V2p))) <=> (p(ap(ap(c_2Earithmetic_2E_3E_3D,inj__ty_2Enum_2Enum(V0m)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p)))) | p(ap(ap(c_2Earithmetic_2E_3E_3D,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V2p)))))))))).
tff(conj_thm_2Earithmetic_2ESUB__LEFT__GREATER,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3E,inj__ty_2Enum_2Enum(V0m)),ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p)))) <=> (p(ap(ap(c_2Earithmetic_2E_3E,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2p))),inj__ty_2Enum_2Enum(V1n))) & p(ap(ap(c_2Earithmetic_2E_3E,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))))).
tff(conj_thm_2Earithmetic_2ESUB__RIGHT__GREATER,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3E,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(V2p))) <=> p(ap(ap(c_2Earithmetic_2E_3E,inj__ty_2Enum_2Enum(V0m)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p)))))))))).
tff(conj_thm_2Earithmetic_2ESUB__LEFT__EQ,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : ((V0m = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p)))) <=> ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2p))) = V1n) | (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) & p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p))))))))))).
tff(conj_thm_2Earithmetic_2ESUB__RIGHT__EQ,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) = V2p) <=> ((V0m = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p)))) | (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) & p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V2p)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))))))).
tff(conj_thm_2Earithmetic_2ELE,lemma,((( ! [V0n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) <=> (V0n = fo__c_2Enum_2E0))) & ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1m)),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V2n)))) <=> ((V1m = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V2n)))) | p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1m)),inj__ty_2Enum_2Enum(V2n)))))))))).
tff(conj_thm_2Earithmetic_2EDA,lemma,(( ! [V0k:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V1n))) => (? [V2r:tp__ty_2Enum_2Enum] : (? [V3q:tp__ty_2Enum_2Enum] : ((V0k = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V3q)),inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(V2r)))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V2r)),inj__ty_2Enum_2Enum(V1n))))))))))).
tff(ax_thm_2Earithmetic_2EDIVISION,axiom,( ! [V0n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n))) => ( ! [V1k:tp__ty_2Enum_2Enum] : ((V1k = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V1k)),inj__ty_2Enum_2Enum(V0n))),inj__ty_2Enum_2Enum(V0n))),ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V1k)),inj__ty_2Enum_2Enum(V0n))))) & p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V1k)),inj__ty_2Enum_2Enum(V0n))),inj__ty_2Enum_2Enum(V0n)))))))).
tff(ax_thm_2Earithmetic_2EDIV2__def,axiom,( ! [V0n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EDIV2,inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V0n)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))).
tff(conj_thm_2Earithmetic_2EMOD__ONE,lemma,(( ! [V0k:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V0k)),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) = fo__c_2Enum_2E0)))).
tff(conj_thm_2Earithmetic_2EMOD__1,lemma,(( ! [V0k:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V0k)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) = fo__c_2Enum_2E0)))).
tff(conj_thm_2Earithmetic_2EDIV__LESS__EQ,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n))) => ( ! [V1k:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V1k)),inj__ty_2Enum_2Enum(V0n))),inj__ty_2Enum_2Enum(V1k)))))))).
tff(conj_thm_2Earithmetic_2EDIV__UNIQUE,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2q:tp__ty_2Enum_2Enum] : ((? [V3r:tp__ty_2Enum_2Enum] : ((V1k = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V2q)),inj__ty_2Enum_2Enum(V0n))),inj__ty_2Enum_2Enum(V3r)))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V3r)),inj__ty_2Enum_2Enum(V0n))))) => (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V1k)),inj__ty_2Enum_2Enum(V0n))) = V2q))))))).
tff(conj_thm_2Earithmetic_2EMOD__UNIQUE,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2r:tp__ty_2Enum_2Enum] : ((? [V3q:tp__ty_2Enum_2Enum] : ((V1k = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V3q)),inj__ty_2Enum_2Enum(V0n))),inj__ty_2Enum_2Enum(V2r)))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V2r)),inj__ty_2Enum_2Enum(V0n))))) => (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V1k)),inj__ty_2Enum_2Enum(V0n))) = V2r))))))).
tff(conj_thm_2Earithmetic_2EDIV__MULT,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1r:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1r)),inj__ty_2Enum_2Enum(V0n))) => ( ! [V2q:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V2q)),inj__ty_2Enum_2Enum(V0n))),inj__ty_2Enum_2Enum(V1r))),inj__ty_2Enum_2Enum(V0n))) = V2q))))))).
tff(conj_thm_2Earithmetic_2ELESS__MOD,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1k:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1k)),inj__ty_2Enum_2Enum(V0n))) => (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V1k)),inj__ty_2Enum_2Enum(V0n))) = V1k)))))).
tff(conj_thm_2Earithmetic_2EMOD__EQ__0,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n))) => ( ! [V1k:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V1k)),inj__ty_2Enum_2Enum(V0n))),inj__ty_2Enum_2Enum(V0n))) = fo__c_2Enum_2E0)))))).
tff(conj_thm_2Earithmetic_2EZERO__MOD,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n))) => (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n))) = fo__c_2Enum_2E0))))).
tff(conj_thm_2Earithmetic_2EZERO__DIV,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n))) => (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n))) = fo__c_2Enum_2E0))))).
tff(conj_thm_2Earithmetic_2EMOD__MULT,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1r:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1r)),inj__ty_2Enum_2Enum(V0n))) => ( ! [V2q:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V2q)),inj__ty_2Enum_2Enum(V0n))),inj__ty_2Enum_2Enum(V1r))),inj__ty_2Enum_2Enum(V0n))) = V1r))))))).
tff(conj_thm_2Earithmetic_2EMOD__TIMES,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n))) => ( ! [V1q:tp__ty_2Enum_2Enum] : ( ! [V2r:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V1q)),inj__ty_2Enum_2Enum(V0n))),inj__ty_2Enum_2Enum(V2r))),inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V2r)),inj__ty_2Enum_2Enum(V0n)))))))))).
tff(conj_thm_2Earithmetic_2EMOD__TIMES__SUB,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1q:tp__ty_2Enum_2Enum] : ( ! [V2r:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n))) & (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V1q))) & p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V2r)),inj__ty_2Enum_2Enum(V0n))))) => (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,ap(ap(c_2Earithmetic_2E_2D,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V1q)),inj__ty_2Enum_2Enum(V0n))),inj__ty_2Enum_2Enum(V2r))),inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V2r))),inj__ty_2Enum_2Enum(V0n)))))))))).
tff(conj_thm_2Earithmetic_2EMOD__PLUS,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n))) => ( ! [V1j:tp__ty_2Enum_2Enum] : ( ! [V2k:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V1j)),inj__ty_2Enum_2Enum(V0n))),ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V2k)),inj__ty_2Enum_2Enum(V0n)))),inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1j)),inj__ty_2Enum_2Enum(V2k))),inj__ty_2Enum_2Enum(V0n)))))))))).
tff(conj_thm_2Earithmetic_2EMOD__MOD,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n))) => ( ! [V1k:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V1k)),inj__ty_2Enum_2Enum(V0n))),inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V1k)),inj__ty_2Enum_2Enum(V0n))))))))).
tff(conj_thm_2Earithmetic_2ELESS__DIV__EQ__ZERO,lemma,(( ! [V0r:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0r)),inj__ty_2Enum_2Enum(V1n))) => (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V0r)),inj__ty_2Enum_2Enum(V1n))) = fo__c_2Enum_2E0)))))).
tff(conj_thm_2Earithmetic_2EMULT__DIV,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1q:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n))) => (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V1q)),inj__ty_2Enum_2Enum(V0n))),inj__ty_2Enum_2Enum(V0n))) = V1q)))))).
tff(conj_thm_2Earithmetic_2EADD__DIV__ADD__DIV,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n))) => ( ! [V1x:tp__ty_2Enum_2Enum] : ( ! [V2r:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V1x)),inj__ty_2Enum_2Enum(V0n))),inj__ty_2Enum_2Enum(V2r))),inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1x)),ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V2r)),inj__ty_2Enum_2Enum(V0n))))))))))).
tff(conj_thm_2Earithmetic_2EADD__DIV__RWT,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n))) => ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V1m)),inj__ty_2Enum_2Enum(V0n))) = fo__c_2Enum_2E0) | (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V2p)),inj__ty_2Enum_2Enum(V0n))) = fo__c_2Enum_2E0)) => (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1m)),inj__ty_2Enum_2Enum(V2p))),inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V1m)),inj__ty_2Enum_2Enum(V0n))),ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V2p)),inj__ty_2Enum_2Enum(V0n)))))))))))).
tff(conj_thm_2Earithmetic_2EMOD__MULT__MOD,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V1n))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0m)))) => ( ! [V2x:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V2x)),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V0m)))),inj__ty_2Enum_2Enum(V1n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V2x)),inj__ty_2Enum_2Enum(V1n)))))))))).
tff(conj_thm_2Earithmetic_2EDIV__ONE,lemma,(( ! [V0q:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V0q)),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) = V0q)))).
tff(conj_thm_2Earithmetic_2EDIV__1,lemma,(( ! [V0q:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V0q)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) = V0q)))).
tff(conj_thm_2Earithmetic_2EDIVMOD__ID,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n))) => ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) & (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V0n))) = fo__c_2Enum_2E0)))))).
tff(conj_thm_2Earithmetic_2EDIV__DIV__DIV__MULT,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0m))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V1n)))) => ( ! [V2x:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V2x)),inj__ty_2Enum_2Enum(V0m))),inj__ty_2Enum_2Enum(V1n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V2x)),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))))))))))).
tff(conj_thm_2Earithmetic_2ESUC__PRE,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0m))) <=> (surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(c_2Eprim__rec_2EPRE,inj__ty_2Enum_2Enum(V0m)))) = V0m))))).
tff(conj_thm_2Earithmetic_2EDIV__LESS,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1d:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n))) & p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(V1d)))) => p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1d))),inj__ty_2Enum_2Enum(V0n)))))))).
tff(conj_thm_2Earithmetic_2EMOD__LESS,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V1n))) => p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(V1n)))))))).
tff(conj_thm_2Earithmetic_2EADD__MODULUS,lemma,((( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1x:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n))) => (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1x)),inj__ty_2Enum_2Enum(V0n))),inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V1x)),inj__ty_2Enum_2Enum(V0n))))))) & ( ! [V2n:tp__ty_2Enum_2Enum] : ( ! [V3x:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V2n))) => (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V2n)),inj__ty_2Enum_2Enum(V3x))),inj__ty_2Enum_2Enum(V2n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V3x)),inj__ty_2Enum_2Enum(V2n)))))))))).
tff(conj_thm_2Earithmetic_2EADD__MODULUS__LEFT,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1x:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n))) => (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1x)),inj__ty_2Enum_2Enum(V0n))),inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V1x)),inj__ty_2Enum_2Enum(V0n))))))))).
tff(conj_thm_2Earithmetic_2EADD__MODULUS__RIGHT,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1x:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n))) => (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1x))),inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V1x)),inj__ty_2Enum_2Enum(V0n))))))))).
tff(conj_thm_2Earithmetic_2EDIV__P,lemma,(( ! [V0P:$i] : (mem(V0P,arr(ty_2Enum_2Enum,bool)) => ( ! [V1p:tp__ty_2Enum_2Enum] : ( ! [V2q:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V2q))) => (p(ap(V0P,ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V1p)),inj__ty_2Enum_2Enum(V2q)))) <=> (? [V3k:tp__ty_2Enum_2Enum] : (? [V4r:tp__ty_2Enum_2Enum] : ((V1p = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V3k)),inj__ty_2Enum_2Enum(V2q))),inj__ty_2Enum_2Enum(V4r)))) & (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V4r)),inj__ty_2Enum_2Enum(V2q))) & p(ap(V0P,inj__ty_2Enum_2Enum(V3k))))))))))))))).
tff(conj_thm_2Earithmetic_2EDIV__P__UNIV,lemma,(( ! [V0P:$i] : (mem(V0P,arr(ty_2Enum_2Enum,bool)) => ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V2n))) => (p(ap(V0P,ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V1m)),inj__ty_2Enum_2Enum(V2n)))) <=> ( ! [V3q:tp__ty_2Enum_2Enum] : ( ! [V4r:tp__ty_2Enum_2Enum] : (((V1m = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V3q)),inj__ty_2Enum_2Enum(V2n))),inj__ty_2Enum_2Enum(V4r)))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V4r)),inj__ty_2Enum_2Enum(V2n)))) => p(ap(V0P,inj__ty_2Enum_2Enum(V3q)))))))))))))).
tff(conj_thm_2Earithmetic_2EMOD__P,lemma,(( ! [V0P:$i] : (mem(V0P,arr(ty_2Enum_2Enum,bool)) => ( ! [V1p:tp__ty_2Enum_2Enum] : ( ! [V2q:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V2q))) => (p(ap(V0P,ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V1p)),inj__ty_2Enum_2Enum(V2q)))) <=> (? [V3k:tp__ty_2Enum_2Enum] : (? [V4r:tp__ty_2Enum_2Enum] : ((V1p = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V3k)),inj__ty_2Enum_2Enum(V2q))),inj__ty_2Enum_2Enum(V4r)))) & (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V4r)),inj__ty_2Enum_2Enum(V2q))) & p(ap(V0P,inj__ty_2Enum_2Enum(V4r))))))))))))))).
tff(conj_thm_2Earithmetic_2EMOD__P__UNIV,lemma,(( ! [V0P:$i] : (mem(V0P,arr(ty_2Enum_2Enum,bool)) => ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V2n))) => (p(ap(V0P,ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V1m)),inj__ty_2Enum_2Enum(V2n)))) <=> ( ! [V3q:tp__ty_2Enum_2Enum] : ( ! [V4r:tp__ty_2Enum_2Enum] : (((V1m = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V3q)),inj__ty_2Enum_2Enum(V2n))),inj__ty_2Enum_2Enum(V4r)))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V4r)),inj__ty_2Enum_2Enum(V2n)))) => p(ap(V0P,inj__ty_2Enum_2Enum(V4r)))))))))))))).
tff(conj_thm_2Earithmetic_2EMOD__TIMES2,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n))) => ( ! [V1j:tp__ty_2Enum_2Enum] : ( ! [V2k:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,ap(ap(c_2Earithmetic_2E_2A,ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V1j)),inj__ty_2Enum_2Enum(V0n))),ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V2k)),inj__ty_2Enum_2Enum(V0n)))),inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V1j)),inj__ty_2Enum_2Enum(V2k))),inj__ty_2Enum_2Enum(V0n)))))))))).
tff(conj_thm_2Earithmetic_2EMOD__COMMON__FACTOR,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1p:tp__ty_2Enum_2Enum] : ( ! [V2q:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V2q)))) => (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0n)),ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V1p)),inj__ty_2Enum_2Enum(V2q)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1p))),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V2q))))))))))).
tff(conj_thm_2Earithmetic_2EX__MOD__Y__EQ__X,lemma,(( ! [V0x:tp__ty_2Enum_2Enum] : ( ! [V1y:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V1y))) => ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V1y))) = V0x) <=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V1y))))))))).
tff(conj_thm_2Earithmetic_2EDIV__LE__MONOTONE,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1x:tp__ty_2Enum_2Enum] : ( ! [V2y:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n))) & p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1x)),inj__ty_2Enum_2Enum(V2y)))) => p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V1x)),inj__ty_2Enum_2Enum(V0n))),ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V2y)),inj__ty_2Enum_2Enum(V0n)))))))))).
tff(conj_thm_2Earithmetic_2ELE__LT1,lemma,(( ! [V0x:tp__ty_2Enum_2Enum] : ( ! [V1y:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V1y))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0x)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1y)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))))).
tff(conj_thm_2Earithmetic_2EX__LE__DIV,lemma,(( ! [V0x:tp__ty_2Enum_2Enum] : ( ! [V1y:tp__ty_2Enum_2Enum] : ( ! [V2z:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V2z))) => (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0x)),ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V1y)),inj__ty_2Enum_2Enum(V2z)))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V2z))),inj__ty_2Enum_2Enum(V1y)))))))))).
tff(conj_thm_2Earithmetic_2EX__LT__DIV,lemma,(( ! [V0x:tp__ty_2Enum_2Enum] : ( ! [V1y:tp__ty_2Enum_2Enum] : ( ! [V2z:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V2z))) => (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0x)),ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V1y)),inj__ty_2Enum_2Enum(V2z)))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2A,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0x)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),inj__ty_2Enum_2Enum(V2z))),inj__ty_2Enum_2Enum(V1y)))))))))).
tff(conj_thm_2Earithmetic_2EDIV__LT__X,lemma,(( ! [V0x:tp__ty_2Enum_2Enum] : ( ! [V1y:tp__ty_2Enum_2Enum] : ( ! [V2z:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V2z))) => (p(ap(ap(c_2Eprim__rec_2E_3C,ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V1y)),inj__ty_2Enum_2Enum(V2z))),inj__ty_2Enum_2Enum(V0x))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1y)),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V2z))))))))))).
tff(conj_thm_2Earithmetic_2EDIV__LE__X,lemma,(( ! [V0x:tp__ty_2Enum_2Enum] : ( ! [V1y:tp__ty_2Enum_2Enum] : ( ! [V2z:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V2z))) => (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V1y)),inj__ty_2Enum_2Enum(V2z))),inj__ty_2Enum_2Enum(V0x))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1y)),ap(ap(c_2Earithmetic_2E_2A,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0x)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),inj__ty_2Enum_2Enum(V2z))))))))))).
tff(conj_thm_2Earithmetic_2EDIV__EQ__X,lemma,(( ! [V0x:tp__ty_2Enum_2Enum] : ( ! [V1y:tp__ty_2Enum_2Enum] : ( ! [V2z:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V2z))) => ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V1y)),inj__ty_2Enum_2Enum(V2z))) = V0x) <=> (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V2z))),inj__ty_2Enum_2Enum(V1y))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1y)),ap(ap(c_2Earithmetic_2E_2A,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0x))),inj__ty_2Enum_2Enum(V2z)))))))))))).
tff(conj_thm_2Earithmetic_2EDIV__MOD__MOD__DIV,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2k:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V1n))) & p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V2k)))) => (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(V2k))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V0m)),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2k)))),inj__ty_2Enum_2Enum(V1n)))))))))).
tff(conj_thm_2Earithmetic_2EMULT__EQ__DIV,lemma,(( ! [V0x:tp__ty_2Enum_2Enum] : ( ! [V1y:tp__ty_2Enum_2Enum] : ( ! [V2z:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0x))) => ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0x)),inj__ty_2Enum_2Enum(V1y))) = V2z) <=> ((V1y = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V2z)),inj__ty_2Enum_2Enum(V0x)))) & (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V2z)),inj__ty_2Enum_2Enum(V0x))) = fo__c_2Enum_2E0))))))))).
tff(conj_thm_2Earithmetic_2ENUMERAL__MULT__EQ__DIV,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_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0x)))),inj__ty_2Enum_2Enum(V1y))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V2z)))) <=> ((V1y = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EDIV,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V2z))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0x)))))) & (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V2z))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0x))))) = fo__c_2Enum_2E0))) & ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0x)))),inj__ty_2Enum_2Enum(V1y))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V2z)))) <=> ((V1y = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EDIV,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V2z))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0x)))))) & (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V2z))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0x))))) = fo__c_2Enum_2E0))))))))).
tff(conj_thm_2Earithmetic_2EMOD__EQ__0__DIVISOR,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1k:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n))) => ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V1k)),inj__ty_2Enum_2Enum(V0n))) = fo__c_2Enum_2E0) <=> (? [V2d:tp__ty_2Enum_2Enum] : (V1k = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V2d)),inj__ty_2Enum_2Enum(V0n))))))))))).
tff(conj_thm_2Earithmetic_2EMOD__SUC,conjecture,(( ! [V0y:tp__ty_2Enum_2Enum] : ( ! [V1x:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0y))) & (~~ (surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1x))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V1x)),inj__ty_2Enum_2Enum(V0y)))),inj__ty_2Enum_2Enum(V0y)))))) => (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1x))),inj__ty_2Enum_2Enum(V0y))) = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(V1x)),inj__ty_2Enum_2Enum(V0y)))))))))).
