include('Axioms/poset^2.ax').
thf(tp_c_2Earithmetic_2E_2A,type,(c_2Earithmetic_2E_2A:$i)).
thf(mem_c_2Earithmetic_2E_2A,axiom,(mem@c_2Earithmetic_2E_2A@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)))).
thf(stp_fo_c_2Earithmetic_2E_2A,type,(fo__c_2Earithmetic_2E_2A:(tp__ty_2Enum_2Enum > (tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum)))).
thf(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)))))).
thf(tp_c_2Earithmetic_2E_2B,type,(c_2Earithmetic_2E_2B:$i)).
thf(mem_c_2Earithmetic_2E_2B,axiom,(mem@c_2Earithmetic_2E_2B@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)))).
thf(stp_fo_c_2Earithmetic_2E_2B,type,(fo__c_2Earithmetic_2E_2B:(tp__ty_2Enum_2Enum > (tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum)))).
thf(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)))))).
thf(tp_c_2Earithmetic_2E_2D,type,(c_2Earithmetic_2E_2D:$i)).
thf(mem_c_2Earithmetic_2E_2D,axiom,(mem@c_2Earithmetic_2E_2D@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)))).
thf(stp_fo_c_2Earithmetic_2E_2D,type,(fo__c_2Earithmetic_2E_2D:(tp__ty_2Enum_2Enum > (tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum)))).
thf(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)))))).
thf(tp_c_2Earithmetic_2E_3C_3D,type,(c_2Earithmetic_2E_3C_3D:$i)).
thf(mem_c_2Earithmetic_2E_3C_3D,axiom,(mem@c_2Earithmetic_2E_3C_3D@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@bool)))).
thf(tp_c_2Earithmetic_2E_3E,type,(c_2Earithmetic_2E_3E:$i)).
thf(mem_c_2Earithmetic_2E_3E,axiom,(mem@c_2Earithmetic_2E_3E@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@bool)))).
thf(tp_c_2Earithmetic_2E_3E_3D,type,(c_2Earithmetic_2E_3E_3D:$i)).
thf(mem_c_2Earithmetic_2E_3E_3D,axiom,(mem@c_2Earithmetic_2E_3E_3D@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@bool)))).
thf(tp_c_2Earithmetic_2EABS__DIFF,type,(c_2Earithmetic_2EABS__DIFF:$i)).
thf(mem_c_2Earithmetic_2EABS__DIFF,axiom,(mem@c_2Earithmetic_2EABS__DIFF@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)))).
thf(stp_fo_c_2Earithmetic_2EABS__DIFF,type,(fo__c_2Earithmetic_2EABS__DIFF:(tp__ty_2Enum_2Enum > (tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum)))).
thf(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)))))).
thf(tp_c_2Earithmetic_2EBIT1,type,(c_2Earithmetic_2EBIT1:$i)).
thf(mem_c_2Earithmetic_2EBIT1,axiom,(mem@c_2Earithmetic_2EBIT1@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum))).
thf(stp_fo_c_2Earithmetic_2EBIT1,type,(fo__c_2Earithmetic_2EBIT1:(tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(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))))).
thf(tp_c_2Earithmetic_2EBIT2,type,(c_2Earithmetic_2EBIT2:$i)).
thf(mem_c_2Earithmetic_2EBIT2,axiom,(mem@c_2Earithmetic_2EBIT2@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum))).
thf(stp_fo_c_2Earithmetic_2EBIT2,type,(fo__c_2Earithmetic_2EBIT2:(tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(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))))).
thf(tp_c_2Earithmetic_2EDIV,type,(c_2Earithmetic_2EDIV:$i)).
thf(mem_c_2Earithmetic_2EDIV,axiom,(mem@c_2Earithmetic_2EDIV@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)))).
thf(stp_fo_c_2Earithmetic_2EDIV,type,(fo__c_2Earithmetic_2EDIV:(tp__ty_2Enum_2Enum > (tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum)))).
thf(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)))))).
thf(tp_c_2Earithmetic_2EDIV2,type,(c_2Earithmetic_2EDIV2:$i)).
thf(mem_c_2Earithmetic_2EDIV2,axiom,(mem@c_2Earithmetic_2EDIV2@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum))).
thf(stp_fo_c_2Earithmetic_2EDIV2,type,(fo__c_2Earithmetic_2EDIV2:(tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(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))))).
thf(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)).
thf(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))).
thf(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))).
thf(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))).
thf(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))))).
thf(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)))))).
thf(stp_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum,type,(tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum : $tType)).
thf(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))).
thf(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))).
thf(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))).
thf(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)))).
thf(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)))))).
thf(tp_c_2Earithmetic_2EDIVMOD,type,(c_2Earithmetic_2EDIVMOD:$i)).
thf(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)))).
thf(tp_c_2Earithmetic_2EEVEN,type,(c_2Earithmetic_2EEVEN:$i)).
thf(mem_c_2Earithmetic_2EEVEN,axiom,(mem@c_2Earithmetic_2EEVEN@(arr@ty_2Enum_2Enum@bool))).
thf(tp_c_2Earithmetic_2EEXP,type,(c_2Earithmetic_2EEXP:$i)).
thf(mem_c_2Earithmetic_2EEXP,axiom,(mem@c_2Earithmetic_2EEXP@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)))).
thf(stp_fo_c_2Earithmetic_2EEXP,type,(fo__c_2Earithmetic_2EEXP:(tp__ty_2Enum_2Enum > (tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum)))).
thf(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)))))).
thf(tp_c_2Earithmetic_2EFACT,type,(c_2Earithmetic_2EFACT:$i)).
thf(mem_c_2Earithmetic_2EFACT,axiom,(mem@c_2Earithmetic_2EFACT@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum))).
thf(stp_fo_c_2Earithmetic_2EFACT,type,(fo__c_2Earithmetic_2EFACT:(tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(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))))).
thf(tp_c_2Earithmetic_2EFUNPOW,type,(c_2Earithmetic_2EFUNPOW:(del>$i))).
thf(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)))))).
thf(tp_c_2Earithmetic_2EMAX,type,(c_2Earithmetic_2EMAX:$i)).
thf(mem_c_2Earithmetic_2EMAX,axiom,(mem@c_2Earithmetic_2EMAX@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)))).
thf(stp_fo_c_2Earithmetic_2EMAX,type,(fo__c_2Earithmetic_2EMAX:(tp__ty_2Enum_2Enum > (tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum)))).
thf(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)))))).
thf(tp_c_2Earithmetic_2EMIN,type,(c_2Earithmetic_2EMIN:$i)).
thf(mem_c_2Earithmetic_2EMIN,axiom,(mem@c_2Earithmetic_2EMIN@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)))).
thf(stp_fo_c_2Earithmetic_2EMIN,type,(fo__c_2Earithmetic_2EMIN:(tp__ty_2Enum_2Enum > (tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum)))).
thf(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)))))).
thf(tp_c_2Earithmetic_2EMOD,type,(c_2Earithmetic_2EMOD:$i)).
thf(mem_c_2Earithmetic_2EMOD,axiom,(mem@c_2Earithmetic_2EMOD@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)))).
thf(stp_fo_c_2Earithmetic_2EMOD,type,(fo__c_2Earithmetic_2EMOD:(tp__ty_2Enum_2Enum > (tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum)))).
thf(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)))))).
thf(tp_c_2Earithmetic_2EMODEQ,type,(c_2Earithmetic_2EMODEQ:$i)).
thf(mem_c_2Earithmetic_2EMODEQ,axiom,(mem@c_2Earithmetic_2EMODEQ@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@bool))))).
thf(tp_c_2Earithmetic_2ENRC,type,(c_2Earithmetic_2ENRC:(del>$i))).
thf(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))))))).
thf(tp_c_2Earithmetic_2ENUMERAL,type,(c_2Earithmetic_2ENUMERAL:$i)).
thf(mem_c_2Earithmetic_2ENUMERAL,axiom,(mem@c_2Earithmetic_2ENUMERAL@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum))).
thf(stp_fo_c_2Earithmetic_2ENUMERAL,type,(fo__c_2Earithmetic_2ENUMERAL:(tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(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))))).
thf(tp_c_2Earithmetic_2EODD,type,(c_2Earithmetic_2EODD:$i)).
thf(mem_c_2Earithmetic_2EODD,axiom,(mem@c_2Earithmetic_2EODD@(arr@ty_2Enum_2Enum@bool))).
thf(tp_c_2Earithmetic_2EZERO,type,(c_2Earithmetic_2EZERO:$i)).
thf(mem_c_2Earithmetic_2EZERO,axiom,(mem@c_2Earithmetic_2EZERO@ty_2Enum_2Enum)).
thf(stp_fo_c_2Earithmetic_2EZERO,type,(fo__c_2Earithmetic_2EZERO:tp__ty_2Enum_2Enum)).
thf(stp_eq_fo_c_2Earithmetic_2EZERO,axiom,((inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO) = c_2Earithmetic_2EZERO)).
thf(tp_c_2Earithmetic_2Efindq,type,(c_2Earithmetic_2Efindq:$i)).
thf(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))).
thf(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))).
thf(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))))).
thf(tp_c_2Earithmetic_2Enat__elim____magic,type,(c_2Earithmetic_2Enat__elim____magic:$i)).
thf(mem_c_2Earithmetic_2Enat__elim____magic,axiom,(mem@c_2Earithmetic_2Enat__elim____magic@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum))).
thf(stp_fo_c_2Earithmetic_2Enat__elim____magic,type,(fo__c_2Earithmetic_2Enat__elim____magic:(tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(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))))).
thf(tp_c_2Earithmetic_2Enum__CASE,type,(c_2Earithmetic_2Enum__CASE:(del>$i))).
thf(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)))))).
thf(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))))))))).
thf(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))).
thf(ax_thm_2Earithmetic_2EALT__ZERO,axiom,(fo__c_2Earithmetic_2EZERO = fo__c_2Enum_2E0)).
thf(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)))))))).
thf(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))))))))).
thf(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))).
thf(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)))))))))).
thf(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)))))))).
thf(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))))))))).
thf(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))))))).
thf(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)))))).
thf(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)))))).
thf(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)))))))).
thf(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)))))))).
thf(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))))))))))).
thf(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))))))))))).
thf(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)))))))))))))))).
thf(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))))).
thf(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))))))).
thf(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)).
thf(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)))))))))))).
thf(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))))))).
thf(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))).
thf(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)))))))).
thf(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))))))))))).
thf(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))))))).
thf(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))))))).
thf(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)))))))).
thf(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)))))))).
thf(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)))))).
thf(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)))).
thf(conj_thm_2Earithmetic_2ELESS__OR__EQ__ALT,lemma,(c_2Earithmetic_2E_3C_3D = (ap@(c_2Erelation_2ERTC@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V0x:$i] : (lam@ty_2Enum_2Enum@(^ [V1y:$i] : (ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@V1y)@(ap@c_2Enum_2ESUC@V0x))))))))).
thf(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)))))).
thf(conj_thm_2Earithmetic_2Etransitive__LESS,lemma,(p@(ap@(c_2Erelation_2Etransitive@ty_2Enum_2Enum)@c_2Eprim__rec_2E_3C))).
thf(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)))))))).
thf(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)))))))).
thf(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))))))).
thf(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))))))).
thf(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))))))).
thf(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))))))))).
thf(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))))))).
thf(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))))))).
thf(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))))))).
thf(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))))))).
thf(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)))))))).
thf(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)))))))).
thf(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))))).
thf(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))))))).
thf(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))))))).
thf(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)))))).
thf(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))))))).
thf(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))))))).
thf(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))))).
thf(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))))))).
thf(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)))))).
thf(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)))))).
thf(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)))))).
thf(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)))))))).
thf(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)))))).
thf(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))))))).
thf(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))))))).
thf(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)))))))).
thf(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)))).
thf(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)))).
thf(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))))))).
thf(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))))))).
thf(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)))))))).
thf(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))).
thf(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)))))))).
thf(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))).
thf(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)))))))).
thf(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))).
thf(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))).
thf(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))))))))))))).
thf(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))))))).
thf(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))))))).
thf(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))))))))).
thf(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))))))))).
thf(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)))))))).
thf(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))))).
thf(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))))))).
thf(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)))))).
thf(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))))))))))).
thf(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))))).
thf(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)))))).
thf(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)))))).
thf(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))))))))).
thf(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)))))))))).
thf(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))))))))).
thf(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)))))))).
thf(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)))))))).
thf(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)))))))).
thf(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)))))))).
thf(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)))))).
thf(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)))))))).
thf(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)))))))).
thf(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)))))))).
thf(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)))))))).
thf(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)))))))))).
thf(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))))).
thf(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))))))).
thf(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))))))))).
thf(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)))))))))).
thf(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))))))))).
thf(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))))))))).
thf(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)))))))))))).
thf(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))))))))).
thf(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)))))))).
thf(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))))).
thf(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)))))))).
thf(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))))))))).
thf(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)))))))))))).
thf(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)))))))).
thf(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))))))))))).
thf(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))))))).
thf(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)))))))).
thf(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)))))))).
thf(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)))))))).
thf(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)))))))).
thf(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)))))).
thf(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)))))).
thf(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)))))))).
thf(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)))))))))).
thf(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)))))))).
thf(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)))))).
thf(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)))))))).
thf(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)))))).
thf(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)))))).
thf(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))))))).
thf(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)))))).
thf(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)))))).
thf(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))))))).
thf(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))))))).
thf(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)))).
thf(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)))))))))).
thf(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))).
thf(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)))))))))).
thf(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))))))).
thf(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))))))))).
thf(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))))))))).
thf(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)))))))))).
thf(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))))))).
thf(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))))))).
thf(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))))))).
thf(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))))).
thf(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))))))).
thf(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)))))))))).
thf(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)))))))).
thf(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)))))))).
thf(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))))))).
thf(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))))))).
thf(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))))))))).
thf(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))))))))).
thf(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)))))).
thf(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)))))))))).
thf(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)))))).
thf(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)))))))).
thf(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)))))))).
thf(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)))))))).
thf(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)))))))).
thf(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)))))).
thf(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))))))).
thf(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))))))).
thf(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)))))).
thf(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))))))).
thf(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)))))))).
thf(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)))))))).
thf(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))))))))).
thf(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)))))))).
thf(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)))))).
thf(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))))))).
thf(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)))))))))).
thf(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)))))))).
thf(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))))))))).
thf(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)))))))).
thf(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)))))))).
thf(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)))))))).
thf(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)))))))).
thf(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)))))))).
thf(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)))))))).
thf(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)))))))).
thf(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)))))))).
thf(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))))))).
thf(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)))))))).
thf(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))))))).
thf(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))))))).
thf(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)))))).
thf(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))))))).
thf(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))))))).
thf(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))))))))).
thf(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))))))))).
thf(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))))))))).
thf(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))))))))).
thf(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))))))))).
thf(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))))))))).
thf(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))))))).
thf(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))))))))).
thf(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))))))))))).
thf(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))))))))).
thf(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))))))))).
thf(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))))))))).
thf(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))))))))).
thf(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)))))))).
thf(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))))))))).
thf(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))))))))).
thf(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)))))))).
thf(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))))))))).
thf(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)))))))).
thf(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))))))))).
thf(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))))))))).
thf(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))))))))).
thf(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)))))))))).
thf(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)))))))))).
thf(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))))))))).
thf(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)))))))))).
thf(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)))))))).
thf(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)))))))).
thf(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))).
thf(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))).
thf(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))))))).
thf(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)))))).
thf(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)))))).
thf(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)))))).
thf(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))))).
thf(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))))).
thf(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)))).
thf(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)))).
thf(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)))))).
thf(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))))))))).
thf(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))))))))).
thf(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))))))))).
thf(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)))))))).
thf(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))))).
thf(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))))).
thf(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)))))))))).
thf(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))))))))))).
thf(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))))))))).
thf(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))).
thf(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))).
thf(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))))).
thf(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)))))))))).
thf(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)))).
thf(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))))))).
thf(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))))))).
thf(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))))))))).
thf(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)))))))).
thf(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)))))))).
thf(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)))))))))))))).
thf(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))))))))))))).
thf(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)))))))))))))).
thf(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))))))))))))).
thf(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))))))))).
thf(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)))))))))).
thf(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)))))))).
thf(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))))))))).
thf(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)))))))))).
thf(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))))))))).
thf(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))))))))).
thf(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)))))))))).
thf(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)))))))))).
thf(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))))))))))).
thf(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))))))))).
thf(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)))))))).
thf(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)))))))).
thf(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)))))))))).
thf(conj_thm_2Earithmetic_2EMOD__SUC,lemma,( ! [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))))))))).
thf(conj_thm_2Earithmetic_2EMOD__SUC__IFF,lemma,( ! [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@(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))))) <=> (~~ ((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)))))))))).
thf(conj_thm_2Earithmetic_2EONE__MOD,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ((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 @ V0n))) => ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2EMOD@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(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)))))))).
thf(conj_thm_2Earithmetic_2EONE__MOD__IFF,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ((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 @ V0n))) <=> ((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@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(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))))))))).
thf(conj_thm_2Earithmetic_2EMOD__LESS__EQ,lemma,( ! [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))) => (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(ap@c_2Earithmetic_2EMOD@(inj__ty_2Enum_2Enum @ V1x))@(inj__ty_2Enum_2Enum @ V0y)))@(inj__ty_2Enum_2Enum @ V1x))))))).
thf(conj_thm_2Earithmetic_2EMOD__LIFT__PLUS,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2x: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 @ V1k))@(ap@(ap@c_2Earithmetic_2E_2D@(inj__ty_2Enum_2Enum @ V0n))@(ap@(ap@c_2Earithmetic_2EMOD@(inj__ty_2Enum_2Enum @ V2x))@(inj__ty_2Enum_2Enum @ V0n)))))) => ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2EMOD@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V2x))@(inj__ty_2Enum_2Enum @ V1k)))@(inj__ty_2Enum_2Enum @ V0n))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(ap@(ap@c_2Earithmetic_2EMOD@(inj__ty_2Enum_2Enum @ V2x))@(inj__ty_2Enum_2Enum @ V0n)))@(inj__ty_2Enum_2Enum @ V1k))))))))).
thf(conj_thm_2Earithmetic_2EMOD__LIFT__PLUS__IFF,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1x: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 @ 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 @ V2k)))@(inj__ty_2Enum_2Enum @ V0n))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(ap@(ap@c_2Earithmetic_2EMOD@(inj__ty_2Enum_2Enum @ V1x))@(inj__ty_2Enum_2Enum @ V0n)))@(inj__ty_2Enum_2Enum @ V2k)))) <=> (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V2k))@(ap@(ap@c_2Earithmetic_2E_2D@(inj__ty_2Enum_2Enum @ V0n))@(ap@(ap@c_2Earithmetic_2EMOD@(inj__ty_2Enum_2Enum @ V1x))@(inj__ty_2Enum_2Enum @ V0n))))))))))).
thf(conj_thm_2Earithmetic_2Enum__case__cong,lemma,( ! [A_27a:del]: ( ! [V0v_27:$i] : ((mem@V0v_27@A_27a) => ( ! [V1f_27:$i] : ((mem@V1f_27@(arr@ty_2Enum_2Enum@A_27a)) => ( ! [V2M:tp__ty_2Enum_2Enum] : ( ! [V3M_27:tp__ty_2Enum_2Enum] : ( ! [V4v:$i] : ((mem@V4v@A_27a) => ( ! [V5f:$i] : ((mem@V5f@(arr@ty_2Enum_2Enum@A_27a)) => (((V2M = V3M_27) & (((V3M_27 = fo__c_2Enum_2E0) => (V4v = V0v_27)) & ( ! [V6n:tp__ty_2Enum_2Enum] : ((V3M_27 = (surj__ty_2Enum_2Enum @ (ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V6n)))) => ((ap@V5f@(inj__ty_2Enum_2Enum @ V6n)) = (ap@V1f_27@(inj__ty_2Enum_2Enum @ V6n))))))) => ((ap@(ap@(ap@(c_2Earithmetic_2Enum__CASE@A_27a)@(inj__ty_2Enum_2Enum @ V2M))@V4v)@V5f) = (ap@(ap@(ap@(c_2Earithmetic_2Enum__CASE@A_27a)@(inj__ty_2Enum_2Enum @ V3M_27))@V0v_27)@V1f_27))))))))))))))).
thf(conj_thm_2Earithmetic_2ESUC__ELIM__THM,lemma,( ! [V0P:$i] : ((mem@V0P@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@bool))) => (( ! [V1n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@V0P@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n)))@(inj__ty_2Enum_2Enum @ V1n)))) <=> ( ! [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@(ap@V0P@(inj__ty_2Enum_2Enum @ V2n))@(ap@(ap@c_2Earithmetic_2E_2D@(inj__ty_2Enum_2Enum @ V2n))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))).
thf(conj_thm_2Earithmetic_2ESUC__ELIM__NUMERALS,lemma,( ! [A_27a:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@A_27a))) => ( ! [V1g:$i] : ((mem@V1g@(arr@ty_2Enum_2Enum@A_27a)) => (( ! [V2n:tp__ty_2Enum_2Enum] : ((ap@V1g@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V2n))) = (ap@(ap@V0f@(inj__ty_2Enum_2Enum @ V2n))@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V2n))))) <=> (( ! [V3n:tp__ty_2Enum_2Enum] : ((ap@V1g@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V3n)))) = (ap@(ap@V0f@(ap@(ap@c_2Earithmetic_2E_2D@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V3n))))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V3n)))))) & ( ! [V4n:tp__ty_2Enum_2Enum] : ((ap@V1g@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V4n)))) = (ap@(ap@V0f@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V4n))))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V4n)))))))))))))).
thf(conj_thm_2Earithmetic_2ESUB__ELIM__THM,lemma,( ! [V0P:$i] : ((mem@V0P@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1a:tp__ty_2Enum_2Enum] : ( ! [V2b:tp__ty_2Enum_2Enum] : ((p@(ap@V0P@(ap@(ap@c_2Earithmetic_2E_2D@(inj__ty_2Enum_2Enum @ V1a))@(inj__ty_2Enum_2Enum @ V2b)))) <=> ( ! [V3d:tp__ty_2Enum_2Enum] : (((V2b = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V1a))@(inj__ty_2Enum_2Enum @ V3d)))) => (p@(ap@V0P@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) & ((V1a = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V2b))@(inj__ty_2Enum_2Enum @ V3d)))) => (p@(ap@V0P@(inj__ty_2Enum_2Enum @ V3d)))))))))))).
thf(conj_thm_2Earithmetic_2EPRE__ELIM__THM,lemma,( ! [V0P:$i] : ((mem@V0P@(arr@ty_2Enum_2Enum@bool)) => ( ! [V1n:tp__ty_2Enum_2Enum] : ((p@(ap@V0P@(ap@c_2Eprim__rec_2EPRE@(inj__ty_2Enum_2Enum @ V1n)))) <=> ( ! [V2m:tp__ty_2Enum_2Enum] : (((V1n = fo__c_2Enum_2E0) => (p@(ap@V0P@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) & ((V1n = (surj__ty_2Enum_2Enum @ (ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V2m)))) => (p@(ap@V0P@(inj__ty_2Enum_2Enum @ V2m))))))))))).
thf(conj_thm_2Earithmetic_2EMULT__INCREASES,lemma,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (((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 @ 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_2Earithmetic_2E_3C_3D@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n)))@(ap@(ap@c_2Earithmetic_2E_2A@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V1n)))))))).
thf(conj_thm_2Earithmetic_2EEXP__ALWAYS__BIG__ENOUGH,lemma,( ! [V0b:tp__ty_2Enum_2Enum] : ((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 @ V0b))) => ( ! [V1n:tp__ty_2Enum_2Enum] : (? [V2m:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V1n))@(ap@(ap@c_2Earithmetic_2EEXP@(inj__ty_2Enum_2Enum @ V0b))@(inj__ty_2Enum_2Enum @ V2m))))))))).
thf(conj_thm_2Earithmetic_2EEXP__EQ__0,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : (((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2EEXP@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m))) = fo__c_2Enum_2E0) <=> ((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 @ V1m)))))))).
thf(conj_thm_2Earithmetic_2EZERO__LT__EXP,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))@(ap@(ap@c_2Earithmetic_2EEXP@(inj__ty_2Enum_2Enum @ V0x))@(inj__ty_2Enum_2Enum @ V1y)))) <=> ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V0x))) | (V1y = fo__c_2Enum_2E0)))))).
thf(conj_thm_2Earithmetic_2EEXP__1,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : (((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2EEXP@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(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_2EEXP@(inj__ty_2Enum_2Enum @ V0n))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))) = V0n)))).
thf(conj_thm_2Earithmetic_2EEXP__EQ__1,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : (((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2EEXP@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))) <=> ((V0n = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))) | (V1m = fo__c_2Enum_2E0)))))).
thf(conj_thm_2Earithmetic_2EEXP__BASE__LE__MONO,lemma,( ! [V0b:tp__ty_2Enum_2Enum] : ((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 @ V0b))) => ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2m:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(ap@c_2Earithmetic_2EEXP@(inj__ty_2Enum_2Enum @ V0b))@(inj__ty_2Enum_2Enum @ V2m)))@(ap@(ap@c_2Earithmetic_2EEXP@(inj__ty_2Enum_2Enum @ V0b))@(inj__ty_2Enum_2Enum @ V1n)))) <=> (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V2m))@(inj__ty_2Enum_2Enum @ V1n))))))))).
thf(conj_thm_2Earithmetic_2EEXP__BASE__LT__MONO,lemma,( ! [V0b:tp__ty_2Enum_2Enum] : ((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 @ V0b))) => ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2m:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(ap@(ap@c_2Earithmetic_2EEXP@(inj__ty_2Enum_2Enum @ V0b))@(inj__ty_2Enum_2Enum @ V2m)))@(ap@(ap@c_2Earithmetic_2EEXP@(inj__ty_2Enum_2Enum @ V0b))@(inj__ty_2Enum_2Enum @ V1n)))) <=> (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V2m))@(inj__ty_2Enum_2Enum @ V1n))))))))).
thf(conj_thm_2Earithmetic_2EEXP__BASE__INJECTIVE,lemma,( ! [V0b:tp__ty_2Enum_2Enum] : ((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 @ V0b))) => ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2m:tp__ty_2Enum_2Enum] : (((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2EEXP@(inj__ty_2Enum_2Enum @ V0b))@(inj__ty_2Enum_2Enum @ V1n))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2EEXP@(inj__ty_2Enum_2Enum @ V0b))@(inj__ty_2Enum_2Enum @ V2m)))) <=> (V1n = V2m))))))).
thf(conj_thm_2Earithmetic_2EEXP__BASE__LEQ__MONO__IMP,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2b:tp__ty_2Enum_2Enum] : (((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V2b))) & (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V1m))@(inj__ty_2Enum_2Enum @ V0n)))) => (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(ap@c_2Earithmetic_2EEXP@(inj__ty_2Enum_2Enum @ V2b))@(inj__ty_2Enum_2Enum @ V1m)))@(ap@(ap@c_2Earithmetic_2EEXP@(inj__ty_2Enum_2Enum @ V2b))@(inj__ty_2Enum_2Enum @ V0n))))))))).
thf(conj_thm_2Earithmetic_2EEXP__BASE__LEQ__MONO__SUC__IMP,lemma,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2b: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_2EEXP@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V2b)))@(inj__ty_2Enum_2Enum @ V0m)))@(ap@(ap@c_2Earithmetic_2EEXP@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V2b)))@(inj__ty_2Enum_2Enum @ V1n))))))))).
thf(conj_thm_2Earithmetic_2EEXP__BASE__LE__IFF,lemma,( ! [V0b:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(ap@c_2Earithmetic_2EEXP@(inj__ty_2Enum_2Enum @ V0b))@(inj__ty_2Enum_2Enum @ V1m)))@(ap@(ap@c_2Earithmetic_2EEXP@(inj__ty_2Enum_2Enum @ V0b))@(inj__ty_2Enum_2Enum @ V2n)))) <=> (((V0b = fo__c_2Enum_2E0) & (V2n = fo__c_2Enum_2E0)) | (((V0b = fo__c_2Enum_2E0) & (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V1m)))) | ((V0b = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))) | ((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 @ V0b))) & (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V1m))@(inj__ty_2Enum_2Enum @ V2n)))))))))))).
thf(conj_thm_2Earithmetic_2EX__LE__X__EXP,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))) => (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V1x))@(ap@(ap@c_2Earithmetic_2EEXP@(inj__ty_2Enum_2Enum @ V1x))@(inj__ty_2Enum_2Enum @ V0n)))))))).
thf(conj_thm_2Earithmetic_2EX__LT__EXP__X,conjecture,( ! [V0b:tp__ty_2Enum_2Enum] : ( ! [V1x:tp__ty_2Enum_2Enum] : ((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 @ V0b))) => (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V1x))@(ap@(ap@c_2Earithmetic_2EEXP@(inj__ty_2Enum_2Enum @ V0b))@(inj__ty_2Enum_2Enum @ V1x)))))))).
