include('Axioms/HL4001^2.ax').
thf(tp_c_2Ebool_2EBOUNDED,type,(c_2Ebool_2EBOUNDED:$i)).
thf(mem_c_2Ebool_2EBOUNDED,axiom,(mem@c_2Ebool_2EBOUNDED@(arr@bool@bool))).
thf(tp_ty_2Elist_2Elist,type,( ty_2Elist_2Elist: del >del )).
thf(tp_c_2Elist_2ETL,type,(c_2Elist_2ETL:(del>$i))).
thf(mem_c_2Elist_2ETL,axiom,( ! [A_27a:del] : (mem@(c_2Elist_2ETL@A_27a)@(arr@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))))).
thf(tp_c_2Elist_2EAPPEND,type,(c_2Elist_2EAPPEND:(del>$i))).
thf(mem_c_2Elist_2EAPPEND,axiom,( ! [A_27a:del] : (mem@(c_2Elist_2EAPPEND@A_27a)@(arr@(ty_2Elist_2Elist@A_27a)@(arr@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a)))))).
thf(tp_c_2Elist_2EFRONT,type,(c_2Elist_2EFRONT:(del>$i))).
thf(mem_c_2Elist_2EFRONT,axiom,( ! [A_27a:del] : (mem@(c_2Elist_2EFRONT@A_27a)@(arr@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))))).
thf(tp_c_2Elist_2EREV,type,(c_2Elist_2EREV:(del>$i))).
thf(mem_c_2Elist_2EREV,axiom,( ! [A_27a:del] : (mem@(c_2Elist_2EREV@A_27a)@(arr@(ty_2Elist_2Elist@A_27a)@(arr@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a)))))).
thf(tp_ty_2Enum_2Enum,type,( ty_2Enum_2Enum:del )).
thf(stp_ty_2Enum_2Enum,type,(tp__ty_2Enum_2Enum : $tType)).
thf(stp_inj_ty_2Enum_2Enum,type,(inj__ty_2Enum_2Enum : (tp__ty_2Enum_2Enum > $i))).
thf(stp_surj_ty_2Enum_2Enum,type,(surj__ty_2Enum_2Enum : ($i > tp__ty_2Enum_2Enum))).
thf(stp_inj_surj_ty_2Enum_2Enum,axiom,( ! [X:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (inj__ty_2Enum_2Enum @ X)) = X))).
thf(stp_inj_mem_ty_2Enum_2Enum,axiom,( ! [X:tp__ty_2Enum_2Enum] : (mem @ (inj__ty_2Enum_2Enum @ X) @ ty_2Enum_2Enum))).
thf(stp_iso_mem_ty_2Enum_2Enum,axiom,( ! [X:$i] : ((mem @ X @ ty_2Enum_2Enum) => (X = (inj__ty_2Enum_2Enum @ (surj__ty_2Enum_2Enum @ X)))))).
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_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_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_2Enumeral_2EiiSUC,type,(c_2Enumeral_2EiiSUC:$i)).
thf(mem_c_2Enumeral_2EiiSUC,axiom,(mem@c_2Enumeral_2EiiSUC@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum))).
thf(stp_fo_c_2Enumeral_2EiiSUC,type,(fo__c_2Enumeral_2EiiSUC:(tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2Enumeral_2EiiSUC,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ (fo__c_2Enumeral_2EiiSUC @ X0)) = (ap @ c_2Enumeral_2EiiSUC @ (inj__ty_2Enum_2Enum @ X0))))).
thf(tp_c_2Enumeral_2EiZ,type,(c_2Enumeral_2EiZ:$i)).
thf(mem_c_2Enumeral_2EiZ,axiom,(mem@c_2Enumeral_2EiZ@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum))).
thf(stp_fo_c_2Enumeral_2EiZ,type,(fo__c_2Enumeral_2EiZ:(tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2Enumeral_2EiZ,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ (fo__c_2Enumeral_2EiZ @ X0)) = (ap @ c_2Enumeral_2EiZ @ (inj__ty_2Enum_2Enum @ X0))))).
thf(tp_c_2Ebool_2ET,type,(c_2Ebool_2ET:$i)).
thf(mem_c_2Ebool_2ET,axiom,(mem@c_2Ebool_2ET@bool)).
thf(ax_true_p,axiom,(p@c_2Ebool_2ET)).
thf(tp_c_2Enumeral_2Etexp__help,type,(c_2Enumeral_2Etexp__help:$i)).
thf(mem_c_2Enumeral_2Etexp__help,axiom,(mem@c_2Enumeral_2Etexp__help@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)))).
thf(stp_fo_c_2Enumeral_2Etexp__help,type,(fo__c_2Enumeral_2Etexp__help:(tp__ty_2Enum_2Enum > (tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum)))).
thf(stp_eq_fo_c_2Enumeral_2Etexp__help,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ ((fo__c_2Enumeral_2Etexp__help @ X0) @ X1)) = (ap @ (ap @ c_2Enumeral_2Etexp__help @ (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_2Enumeral__bit_2EiMOD__2EXP,type,(c_2Enumeral__bit_2EiMOD__2EXP:$i)).
thf(mem_c_2Enumeral__bit_2EiMOD__2EXP,axiom,(mem@c_2Enumeral__bit_2EiMOD__2EXP@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)))).
thf(stp_fo_c_2Enumeral__bit_2EiMOD__2EXP,type,(fo__c_2Enumeral__bit_2EiMOD__2EXP:(tp__ty_2Enum_2Enum > (tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum)))).
thf(stp_eq_fo_c_2Enumeral__bit_2EiMOD__2EXP,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ ((fo__c_2Enumeral__bit_2EiMOD__2EXP @ X0) @ X1)) = (ap @ (ap @ c_2Enumeral__bit_2EiMOD__2EXP @ (inj__ty_2Enum_2Enum @ X0)) @ (inj__ty_2Enum_2Enum @ X1)))))).
thf(tp_c_2Enumeral_2EiDUB,type,(c_2Enumeral_2EiDUB:$i)).
thf(mem_c_2Enumeral_2EiDUB,axiom,(mem@c_2Enumeral_2EiDUB@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum))).
thf(stp_fo_c_2Enumeral_2EiDUB,type,(fo__c_2Enumeral_2EiDUB:(tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2Enumeral_2EiDUB,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ (fo__c_2Enumeral_2EiDUB @ X0)) = (ap @ c_2Enumeral_2EiDUB @ (inj__ty_2Enum_2Enum @ X0))))).
thf(tp_c_2Ebit_2EDIV__2EXP,type,(c_2Ebit_2EDIV__2EXP:$i)).
thf(mem_c_2Ebit_2EDIV__2EXP,axiom,(mem@c_2Ebit_2EDIV__2EXP@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)))).
thf(stp_fo_c_2Ebit_2EDIV__2EXP,type,(fo__c_2Ebit_2EDIV__2EXP:(tp__ty_2Enum_2Enum > (tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum)))).
thf(stp_eq_fo_c_2Ebit_2EDIV__2EXP,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ ((fo__c_2Ebit_2EDIV__2EXP @ X0) @ X1)) = (ap @ (ap @ c_2Ebit_2EDIV__2EXP @ (inj__ty_2Enum_2Enum @ X0)) @ (inj__ty_2Enum_2Enum @ X1)))))).
thf(tp_c_2Enumeral__bit_2ESFUNPOW,type,(c_2Enumeral__bit_2ESFUNPOW:$i)).
thf(mem_c_2Enumeral__bit_2ESFUNPOW,axiom,(mem@c_2Enumeral__bit_2ESFUNPOW@(arr@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum))))).
thf(tp_c_2Enumeral__bit_2EiDIV2,type,(c_2Enumeral__bit_2EiDIV2:$i)).
thf(mem_c_2Enumeral__bit_2EiDIV2,axiom,(mem@c_2Enumeral__bit_2EiDIV2@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum))).
thf(stp_fo_c_2Enumeral__bit_2EiDIV2,type,(fo__c_2Enumeral__bit_2EiDIV2:(tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2Enumeral__bit_2EiDIV2,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ (fo__c_2Enumeral__bit_2EiDIV2 @ X0)) = (ap @ c_2Enumeral__bit_2EiDIV2 @ (inj__ty_2Enum_2Enum @ X0))))).
thf(tp_c_2Enumeral__bit_2EiSUC,type,(c_2Enumeral__bit_2EiSUC:$i)).
thf(mem_c_2Enumeral__bit_2EiSUC,axiom,(mem@c_2Enumeral__bit_2EiSUC@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum))).
thf(stp_fo_c_2Enumeral__bit_2EiSUC,type,(fo__c_2Enumeral__bit_2EiSUC:(tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2Enumeral__bit_2EiSUC,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ (fo__c_2Enumeral__bit_2EiSUC @ X0)) = (ap @ c_2Enumeral__bit_2EiSUC @ (inj__ty_2Enum_2Enum @ X0))))).
thf(tp_c_2Enumeral__bit_2EFDUB,type,(c_2Enumeral__bit_2EFDUB:$i)).
thf(mem_c_2Enumeral__bit_2EFDUB,axiom,(mem@c_2Enumeral__bit_2EFDUB@(arr@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)))).
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_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_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_2Ebit_2ETIMES__2EXP,type,(c_2Ebit_2ETIMES__2EXP:$i)).
thf(mem_c_2Ebit_2ETIMES__2EXP,axiom,(mem@c_2Ebit_2ETIMES__2EXP@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)))).
thf(stp_fo_c_2Ebit_2ETIMES__2EXP,type,(fo__c_2Ebit_2ETIMES__2EXP:(tp__ty_2Enum_2Enum > (tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum)))).
thf(stp_eq_fo_c_2Ebit_2ETIMES__2EXP,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ ((fo__c_2Ebit_2ETIMES__2EXP @ X0) @ X1)) = (ap @ (ap @ c_2Ebit_2ETIMES__2EXP @ (inj__ty_2Enum_2Enum @ X0)) @ (inj__ty_2Enum_2Enum @ X1)))))).
thf(tp_c_2Ebit_2EMOD__2EXP,type,(c_2Ebit_2EMOD__2EXP:$i)).
thf(mem_c_2Ebit_2EMOD__2EXP,axiom,(mem@c_2Ebit_2EMOD__2EXP@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)))).
thf(stp_fo_c_2Ebit_2EMOD__2EXP,type,(fo__c_2Ebit_2EMOD__2EXP:(tp__ty_2Enum_2Enum > (tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum)))).
thf(stp_eq_fo_c_2Ebit_2EMOD__2EXP,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ ((fo__c_2Ebit_2EMOD__2EXP @ X0) @ X1)) = (ap @ (ap @ c_2Ebit_2EMOD__2EXP @ (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(stp_c_ty_2Elist_2Elist_ty_2Enum_2Enum,type,(tp__c_ty_2Elist_2Elist_ty_2Enum_2Enum : $tType)).
thf(stp_inj_c_ty_2Elist_2Elist_ty_2Enum_2Enum,type,(inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum : (tp__c_ty_2Elist_2Elist_ty_2Enum_2Enum > $i))).
thf(stp_surj_c_ty_2Elist_2Elist_ty_2Enum_2Enum,type,(surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum : ($i > tp__c_ty_2Elist_2Elist_ty_2Enum_2Enum))).
thf(stp_inj_surj_c_ty_2Elist_2Elist_ty_2Enum_2Enum,axiom,( ! [X:tp__c_ty_2Elist_2Elist_ty_2Enum_2Enum] : ((surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ (inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ X)) = X))).
thf(stp_inj_mem_c_ty_2Elist_2Elist_ty_2Enum_2Enum,axiom,( ! [X:tp__c_ty_2Elist_2Elist_ty_2Enum_2Enum] : (mem @ (inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ X) @ (ty_2Elist_2Elist@ty_2Enum_2Enum)))).
thf(stp_iso_mem_c_ty_2Elist_2Elist_ty_2Enum_2Enum,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Elist_2Elist@ty_2Enum_2Enum)) => (X = (inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ (surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ X)))))).
thf(tp_c_2Enumposrep_2El2n,type,(c_2Enumposrep_2El2n:$i)).
thf(mem_c_2Enumposrep_2El2n,axiom,(mem@c_2Enumposrep_2El2n@(arr@ty_2Enum_2Enum@(arr@(ty_2Elist_2Elist@ty_2Enum_2Enum)@ty_2Enum_2Enum)))).
thf(stp_fo_c_2Enumposrep_2El2n,type,(fo__c_2Enumposrep_2El2n:(tp__ty_2Enum_2Enum > (tp__c_ty_2Elist_2Elist_ty_2Enum_2Enum > tp__ty_2Enum_2Enum)))).
thf(stp_eq_fo_c_2Enumposrep_2El2n,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__c_ty_2Elist_2Elist_ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ ((fo__c_2Enumposrep_2El2n @ X0) @ X1)) = (ap @ (ap @ c_2Enumposrep_2El2n @ (inj__ty_2Enum_2Enum @ X0)) @ (inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ X1)))))).
thf(tp_ty_2Epair_2Eprod,type,( ty_2Epair_2Eprod: del > del >del )).
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_2Ebit_2EDIVMOD__2EXP,type,(c_2Ebit_2EDIVMOD__2EXP:$i)).
thf(mem_c_2Ebit_2EDIVMOD__2EXP,axiom,(mem@c_2Ebit_2EDIVMOD__2EXP@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))))).
thf(tp_c_2Ebool_2ELET,type,(c_2Ebool_2ELET:(del>(del>$i)))).
thf(mem_c_2Ebool_2ELET,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Ebool_2ELET@A_27a@A_27b)@(arr@(arr@A_27a@A_27b)@(arr@A_27a@A_27b)))))).
thf(tp_c_2Enumposrep_2En2l,type,(c_2Enumposrep_2En2l:$i)).
thf(mem_c_2Enumposrep_2En2l,axiom,(mem@c_2Enumposrep_2En2l@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@(ty_2Elist_2Elist@ty_2Enum_2Enum))))).
thf(tp_c_2Epair_2E_2C,type,(c_2Epair_2E_2C:(del>(del>$i)))).
thf(mem_c_2Epair_2E_2C,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Epair_2E_2C@A_27a@A_27b)@(arr@A_27a@(arr@A_27b@(ty_2Epair_2Eprod@A_27a@A_27b))))))).
thf(tp_c_2Epair_2EUNCURRY,type,(c_2Epair_2EUNCURRY:(del>(del>(del>$i))))).
thf(mem_c_2Epair_2EUNCURRY,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27c:del] : (mem@(c_2Epair_2EUNCURRY@A_27a@A_27b@A_27c)@(arr@(arr@A_27a@(arr@A_27b@A_27c))@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@A_27c))))))).
thf(tp_c_2Elist_2ECONS,type,(c_2Elist_2ECONS:(del>$i))).
thf(mem_c_2Elist_2ECONS,axiom,( ! [A_27a:del] : (mem@(c_2Elist_2ECONS@A_27a)@(arr@A_27a@(arr@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a)))))).
thf(tp_ty_2Estring_2Echar,type,( ty_2Estring_2Echar:del )).
thf(stp_ty_2Estring_2Echar,type,(tp__ty_2Estring_2Echar : $tType)).
thf(stp_inj_ty_2Estring_2Echar,type,(inj__ty_2Estring_2Echar : (tp__ty_2Estring_2Echar > $i))).
thf(stp_surj_ty_2Estring_2Echar,type,(surj__ty_2Estring_2Echar : ($i > tp__ty_2Estring_2Echar))).
thf(stp_inj_surj_ty_2Estring_2Echar,axiom,( ! [X:tp__ty_2Estring_2Echar] : ((surj__ty_2Estring_2Echar @ (inj__ty_2Estring_2Echar @ X)) = X))).
thf(stp_inj_mem_ty_2Estring_2Echar,axiom,( ! [X:tp__ty_2Estring_2Echar] : (mem @ (inj__ty_2Estring_2Echar @ X) @ ty_2Estring_2Echar))).
thf(stp_iso_mem_ty_2Estring_2Echar,axiom,( ! [X:$i] : ((mem @ X @ ty_2Estring_2Echar) => (X = (inj__ty_2Estring_2Echar @ (surj__ty_2Estring_2Echar @ X)))))).
thf(stp_c_ty_2Elist_2Elist_ty_2Estring_2Echar,type,(tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar : $tType)).
thf(stp_inj_c_ty_2Elist_2Elist_ty_2Estring_2Echar,type,(inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar : (tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar > $i))).
thf(stp_surj_c_ty_2Elist_2Elist_ty_2Estring_2Echar,type,(surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar : ($i > tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar))).
thf(stp_inj_surj_c_ty_2Elist_2Elist_ty_2Estring_2Echar,axiom,( ! [X:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ((surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ (inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ X)) = X))).
thf(stp_inj_mem_c_ty_2Elist_2Elist_ty_2Estring_2Echar,axiom,( ! [X:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : (mem @ (inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ X) @ (ty_2Elist_2Elist@ty_2Estring_2Echar)))).
thf(stp_iso_mem_c_ty_2Elist_2Elist_ty_2Estring_2Echar,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Elist_2Elist@ty_2Estring_2Echar)) => (X = (inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ (surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ X)))))).
thf(tp_c_2EASCIInumbers_2Es2n,type,(c_2EASCIInumbers_2Es2n:$i)).
thf(mem_c_2EASCIInumbers_2Es2n,axiom,(mem@c_2EASCIInumbers_2Es2n@(arr@ty_2Enum_2Enum@(arr@(arr@ty_2Estring_2Echar@ty_2Enum_2Enum)@(arr@(ty_2Elist_2Elist@ty_2Estring_2Echar)@ty_2Enum_2Enum))))).
thf(tp_c_2EASCIInumbers_2En2s,type,(c_2EASCIInumbers_2En2s:$i)).
thf(mem_c_2EASCIInumbers_2En2s,axiom,(mem@c_2EASCIInumbers_2En2s@(arr@ty_2Enum_2Enum@(arr@(arr@ty_2Enum_2Enum@ty_2Estring_2Echar)@(arr@ty_2Enum_2Enum@(ty_2Elist_2Elist@ty_2Estring_2Echar)))))).
thf(tp_c_2Epatricia__casts_2ESKIP1,type,(c_2Epatricia__casts_2ESKIP1:$i)).
thf(mem_c_2Epatricia__casts_2ESKIP1,axiom,(mem@c_2Epatricia__casts_2ESKIP1@(arr@(ty_2Elist_2Elist@ty_2Estring_2Echar)@(ty_2Elist_2Elist@ty_2Estring_2Echar)))).
thf(tp_c_2Epatricia__casts_2Enum__to__string,type,(c_2Epatricia__casts_2Enum__to__string:$i)).
thf(mem_c_2Epatricia__casts_2Enum__to__string,axiom,(mem@c_2Epatricia__casts_2Enum__to__string@(arr@ty_2Enum_2Enum@(ty_2Elist_2Elist@ty_2Estring_2Echar)))).
thf(tp_c_2Epred__set_2EUNIV,type,(c_2Epred__set_2EUNIV:(del>$i))).
thf(mem_c_2Epred__set_2EUNIV,axiom,( ! [A_27a:del] : (mem@(c_2Epred__set_2EUNIV@A_27a)@(arr@A_27a@bool)))).
thf(tp_c_2Epatricia__casts_2Estring__to__num,type,(c_2Epatricia__casts_2Estring__to__num:$i)).
thf(mem_c_2Epatricia__casts_2Estring__to__num,axiom,(mem@c_2Epatricia__casts_2Estring__to__num@(arr@(ty_2Elist_2Elist@ty_2Estring_2Echar)@ty_2Enum_2Enum))).
thf(stp_fo_c_2Epatricia__casts_2Estring__to__num,type,(fo__c_2Epatricia__casts_2Estring__to__num:(tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2Epatricia__casts_2Estring__to__num,axiom,( ! [X0:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ((inj__ty_2Enum_2Enum @ (fo__c_2Epatricia__casts_2Estring__to__num @ X0)) = (ap @ c_2Epatricia__casts_2Estring__to__num @ (inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ X0))))).
thf(tp_c_2Epred__set_2EIMAGE,type,(c_2Epred__set_2EIMAGE:(del>(del>$i)))).
thf(mem_c_2Epred__set_2EIMAGE,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@(arr@(arr@A_27a@A_27b)@(arr@(arr@A_27a@bool)@(arr@A_27b@bool))))))).
thf(tp_c_2Ebool_2EIN,type,(c_2Ebool_2EIN:(del>$i))).
thf(mem_c_2Ebool_2EIN,axiom,( ! [A_27a:del] : (mem@(c_2Ebool_2EIN@A_27a)@(arr@A_27a@(arr@(arr@A_27a@bool)@bool))))).
thf(tp_c_2Elogroot_2ELOG,type,(c_2Elogroot_2ELOG:$i)).
thf(mem_c_2Elogroot_2ELOG,axiom,(mem@c_2Elogroot_2ELOG@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)))).
thf(stp_fo_c_2Elogroot_2ELOG,type,(fo__c_2Elogroot_2ELOG:(tp__ty_2Enum_2Enum > (tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum)))).
thf(stp_eq_fo_c_2Elogroot_2ELOG,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ ((fo__c_2Elogroot_2ELOG @ X0) @ X1)) = (ap @ (ap @ c_2Elogroot_2ELOG @ (inj__ty_2Enum_2Enum @ X0)) @ (inj__ty_2Enum_2Enum @ X1)))))).
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_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_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_2Enum_2ESUC,type,(c_2Enum_2ESUC:$i)).
thf(mem_c_2Enum_2ESUC,axiom,(mem@c_2Enum_2ESUC@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum))).
thf(stp_fo_c_2Enum_2ESUC,type,(fo__c_2Enum_2ESUC:(tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2Enum_2ESUC,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ (fo__c_2Enum_2ESUC @ X0)) = (ap @ c_2Enum_2ESUC @ (inj__ty_2Enum_2Enum @ X0))))).
thf(tp_c_2Enum_2E0,type,(c_2Enum_2E0:$i)).
thf(mem_c_2Enum_2E0,axiom,(mem@c_2Enum_2E0@ty_2Enum_2Enum)).
thf(stp_fo_c_2Enum_2E0,type,(fo__c_2Enum_2E0:tp__ty_2Enum_2Enum)).
thf(stp_eq_fo_c_2Enum_2E0,axiom,((inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0) = c_2Enum_2E0)).
thf(tp_c_2Elist_2EMAP,type,(c_2Elist_2EMAP:(del>(del>$i)))).
thf(mem_c_2Elist_2EMAP,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Elist_2EMAP@A_27a@A_27b)@(arr@(arr@A_27a@A_27b)@(arr@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27b))))))).
thf(tp_c_2Elist_2ELAST,type,(c_2Elist_2ELAST:(del>$i))).
thf(mem_c_2Elist_2ELAST,axiom,( ! [A_27a:del] : (mem@(c_2Elist_2ELAST@A_27a)@(arr@(ty_2Elist_2Elist@A_27a)@A_27a)))).
thf(tp_c_2Elist_2ELENGTH,type,(c_2Elist_2ELENGTH:(del>$i))).
thf(mem_c_2Elist_2ELENGTH,axiom,( ! [A_27a:del] : (mem@(c_2Elist_2ELENGTH@A_27a)@(arr@(ty_2Elist_2Elist@A_27a)@ty_2Enum_2Enum)))).
thf(tp_c_2Eprim__rec_2EPRE,type,(c_2Eprim__rec_2EPRE:$i)).
thf(mem_c_2Eprim__rec_2EPRE,axiom,(mem@c_2Eprim__rec_2EPRE@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum))).
thf(stp_fo_c_2Eprim__rec_2EPRE,type,(fo__c_2Eprim__rec_2EPRE:(tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2Eprim__rec_2EPRE,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ (fo__c_2Eprim__rec_2EPRE @ X0)) = (ap @ c_2Eprim__rec_2EPRE @ (inj__ty_2Enum_2Enum @ X0))))).
thf(tp_c_2Elist_2EEL,type,(c_2Elist_2EEL:(del>$i))).
thf(mem_c_2Elist_2EEL,axiom,( ! [A_27a:del] : (mem@(c_2Elist_2EEL@A_27a)@(arr@ty_2Enum_2Enum@(arr@(ty_2Elist_2Elist@A_27a)@A_27a))))).
thf(tp_c_2Elist_2ENIL,type,(c_2Elist_2ENIL:(del>$i))).
thf(mem_c_2Elist_2ENIL,axiom,( ! [A_27a:del] : (mem@(c_2Elist_2ENIL@A_27a)@(ty_2Elist_2Elist@A_27a)))).
thf(tp_c_2Elist_2EREVERSE,type,(c_2Elist_2EREVERSE:(del>$i))).
thf(mem_c_2Elist_2EREVERSE,axiom,( ! [A_27a:del] : (mem@(c_2Elist_2EREVERSE@A_27a)@(arr@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))))).
thf(tp_c_2Elist_2EEVERY,type,(c_2Elist_2EEVERY:(del>$i))).
thf(mem_c_2Elist_2EEVERY,axiom,( ! [A_27a:del] : (mem@(c_2Elist_2EEVERY@A_27a)@(arr@(arr@A_27a@bool)@(arr@(ty_2Elist_2Elist@A_27a)@bool))))).
thf(tp_c_2Ebool_2EF,type,(c_2Ebool_2EF:$i)).
thf(mem_c_2Ebool_2EF,axiom,(mem@c_2Ebool_2EF@bool)).
thf(ax_false_p,axiom,(~ (p@c_2Ebool_2EF))).
thf(tp_c_2Ebool_2E_5C_2F,type,(c_2Ebool_2E_5C_2F:$i)).
thf(mem_c_2Ebool_2E_5C_2F,axiom,(mem@c_2Ebool_2E_5C_2F@(arr@bool@(arr@bool@bool)))).
thf(ax_or_p,axiom,( ! [Q:$i] : ((mem@Q@bool) => ( ! [R:$i] : ((mem@R@bool) => ((p@(ap@(ap@c_2Ebool_2E_5C_2F@Q)@R)) <=> ((p@Q) | (p@R)))))))).
thf(tp_c_2Ebool_2E_7E,type,(c_2Ebool_2E_7E:$i)).
thf(mem_c_2Ebool_2E_7E,axiom,(mem@c_2Ebool_2E_7E@(arr@bool@bool))).
thf(ax_neg_p,axiom,( ! [Q:$i] : ((mem@Q@bool) => ((p@(ap@c_2Ebool_2E_7E@Q)) <=> (~ (p@Q)))))).
thf(tp_c_2Emin_2E_3D_3D_3E,type,(c_2Emin_2E_3D_3D_3E:$i)).
thf(mem_c_2Emin_2E_3D_3D_3E,axiom,(mem@c_2Emin_2E_3D_3D_3E@(arr@bool@(arr@bool@bool)))).
thf(ax_imp_p,axiom,( ! [Q:$i] : ((mem@Q@bool) => ( ! [R:$i] : ((mem@R@bool) => ((p@(ap@(ap@c_2Emin_2E_3D_3D_3E@Q)@R)) <=> ((p@Q) => (p@R)))))))).
thf(tp_c_2Ecombin_2EFAIL,type,(c_2Ecombin_2EFAIL:(del>(del>$i)))).
thf(mem_c_2Ecombin_2EFAIL,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Ecombin_2EFAIL@A_27a@A_27b)@(arr@A_27a@(arr@A_27b@A_27a)))))).
thf(tp_c_2Ebool_2ECOND,type,(c_2Ebool_2ECOND:(del>$i))).
thf(mem_c_2Ebool_2ECOND,axiom,( ! [A_27a:del] : (mem@(c_2Ebool_2ECOND@A_27a)@(arr@bool@(arr@A_27a@(arr@A_27a@A_27a)))))).
thf(tp_c_2Estring_2EORD,type,(c_2Estring_2EORD:$i)).
thf(mem_c_2Estring_2EORD,axiom,(mem@c_2Estring_2EORD@(arr@ty_2Estring_2Echar@ty_2Enum_2Enum))).
thf(stp_fo_c_2Estring_2EORD,type,(fo__c_2Estring_2EORD:(tp__ty_2Estring_2Echar > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2Estring_2EORD,axiom,( ! [X0:tp__ty_2Estring_2Echar] : ((inj__ty_2Enum_2Enum @ (fo__c_2Estring_2EORD @ X0)) = (ap @ c_2Estring_2EORD @ (inj__ty_2Estring_2Echar @ X0))))).
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_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_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_2Eprim__rec_2E_3C,type,(c_2Eprim__rec_2E_3C:$i)).
thf(mem_c_2Eprim__rec_2E_3C,axiom,(mem@c_2Eprim__rec_2E_3C@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@bool)))).
thf(tp_c_2Estring_2ECHR,type,(c_2Estring_2ECHR:$i)).
thf(mem_c_2Estring_2ECHR,axiom,(mem@c_2Estring_2ECHR@(arr@ty_2Enum_2Enum@ty_2Estring_2Echar))).
thf(stp_fo_c_2Estring_2ECHR,type,(fo__c_2Estring_2ECHR:(tp__ty_2Enum_2Enum > tp__ty_2Estring_2Echar))).
thf(stp_eq_fo_c_2Estring_2ECHR,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ((inj__ty_2Estring_2Echar @ (fo__c_2Estring_2ECHR @ X0)) = (ap @ c_2Estring_2ECHR @ (inj__ty_2Enum_2Enum @ X0))))).
thf(tp_c_2Emin_2E_3D,type,(c_2Emin_2E_3D:(del>$i))).
thf(mem_c_2Emin_2E_3D,axiom,( ! [A_27a:del] : (mem@(c_2Emin_2E_3D@A_27a)@(arr@A_27a@(arr@A_27a@bool))))).
thf(ax_eq_p,axiom,( ! [A:del] : ( ! [X:$i] : ((mem@X@A) => ( ! [Y:$i] : ((mem@Y@A) => ((p@(ap@(ap@(c_2Emin_2E_3D@A)@X)@Y)) <=> (X = Y)))))))).
thf(tp_c_2Ebool_2E_2F_5C,type,(c_2Ebool_2E_2F_5C:$i)).
thf(mem_c_2Ebool_2E_2F_5C,axiom,(mem@c_2Ebool_2E_2F_5C@(arr@bool@(arr@bool@bool)))).
thf(ax_and_p,axiom,( ! [Q:$i] : ((mem@Q@bool) => ( ! [R:$i] : ((mem@R@bool) => ((p@(ap@(ap@c_2Ebool_2E_2F_5C@Q)@R)) <=> ((p@Q) & (p@R)))))))).
thf(tp_c_2Ebool_2E_3F,type,(c_2Ebool_2E_3F:(del>$i))).
thf(mem_c_2Ebool_2E_3F,axiom,( ! [A_27a:del] : (mem@(c_2Ebool_2E_3F@A_27a)@(arr@(arr@A_27a@bool)@bool)))).
thf(ax_ex_p,axiom,( ! [A:del] : ( ! [Q:$i] : ((mem@Q@(arr@A@bool)) => ((p@(ap@(c_2Ebool_2E_3F@A)@Q)) <=> (? [X:$i] : ((mem@X@A) & (p@(ap@Q@X))))))))).
thf(tp_c_2Ebool_2E_21,type,(c_2Ebool_2E_21:(del>$i))).
thf(mem_c_2Ebool_2E_21,axiom,( ! [A_27a:del] : (mem@(c_2Ebool_2E_21@A_27a)@(arr@(arr@A_27a@bool)@bool)))).
thf(ax_all_p,axiom,( ! [A:del] : ( ! [Q:$i] : ((mem@Q@(arr@A@bool)) => ((p@(ap@(c_2Ebool_2E_21@A)@Q)) <=> ( ! [X:$i] : ((mem@X@A) => (p@(ap@Q@X))))))))).
thf(ax_thm_2EASCIInumbers_2Es2n__def,axiom,( ! [V0b:tp__ty_2Enum_2Enum] : ( ! [V1f:$i] : ((mem@V1f@(arr@ty_2Estring_2Echar@ty_2Enum_2Enum)) => ( ! [V2s:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ((surj__ty_2Enum_2Enum @ (ap@(ap@(ap@c_2EASCIInumbers_2Es2n@(inj__ty_2Enum_2Enum @ V0b))@V1f)@(inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ V2s))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Enumposrep_2El2n@(inj__ty_2Enum_2Enum @ V0b))@(ap@(ap@(c_2Elist_2EMAP@ty_2Estring_2Echar@ty_2Enum_2Enum)@V1f)@(ap@(c_2Elist_2EREVERSE@ty_2Estring_2Echar)@(inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ V2s))))))))))).
thf(ax_thm_2EASCIInumbers_2En2s__def,axiom,( ! [V0b:tp__ty_2Enum_2Enum] : ( ! [V1f:$i] : ((mem@V1f@(arr@ty_2Enum_2Enum@ty_2Estring_2Echar)) => ( ! [V2n:tp__ty_2Enum_2Enum] : ((surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ (ap@(ap@(ap@c_2EASCIInumbers_2En2s@(inj__ty_2Enum_2Enum @ V0b))@V1f)@(inj__ty_2Enum_2Enum @ V2n))) = (surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ (ap@(c_2Elist_2EREVERSE@ty_2Estring_2Echar)@(ap@(ap@(c_2Elist_2EMAP@ty_2Enum_2Enum@ty_2Estring_2Echar)@V1f)@(ap@(ap@c_2Enumposrep_2En2l@(inj__ty_2Enum_2Enum @ V0b))@(inj__ty_2Enum_2Enum @ V2n))))))))))).
thf(conj_thm_2EASCIInumbers_2Es2n__n2s,lemma,( ! [V0c2n:$i] : ((mem@V0c2n@(arr@ty_2Estring_2Echar@ty_2Enum_2Enum)) => ( ! [V1n2c:$i] : ((mem@V1n2c@(arr@ty_2Enum_2Enum@ty_2Estring_2Echar)) => ( ! [V2b:tp__ty_2Enum_2Enum] : ( ! [V3n: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 @ V2b))) & ( ! [V4x:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V4x))@(inj__ty_2Enum_2Enum @ V2b))) => ((surj__ty_2Enum_2Enum @ (ap@V0c2n@(ap@V1n2c@(inj__ty_2Enum_2Enum @ V4x)))) = V4x)))) => ((surj__ty_2Enum_2Enum @ (ap@(ap@(ap@c_2EASCIInumbers_2Es2n@(inj__ty_2Enum_2Enum @ V2b))@V0c2n)@(ap@(ap@(ap@c_2EASCIInumbers_2En2s@(inj__ty_2Enum_2Enum @ V2b))@V1n2c)@(inj__ty_2Enum_2Enum @ V3n)))) = V3n))))))))).
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(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_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_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_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_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_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__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__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_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_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_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_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_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(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(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__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_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_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_2Ebit_2EDIVMOD__2EXP,lemma,( ! [V0x:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@c_2Ebit_2EDIVMOD__2EXP@(inj__ty_2Enum_2Enum @ V0x))@(inj__ty_2Enum_2Enum @ V1n))) = (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum @ (ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Enum_2Enum)@(ap@(ap@c_2Ebit_2EDIV__2EXP@(inj__ty_2Enum_2Enum @ V0x))@(inj__ty_2Enum_2Enum @ V1n)))@(ap@(ap@c_2Ebit_2EMOD__2EXP@(inj__ty_2Enum_2Enum @ V0x))@(inj__ty_2Enum_2Enum @ V1n)))))))).
thf(conj_thm_2Ebit_2EDIV__MULT__1,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@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V1n))@(inj__ty_2Enum_2Enum @ V0r)))@(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))))))))).
thf(ax_thm_2Ebool_2ELET__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ((c_2Ebool_2ELET@A_27a@A_27b) = (lam@(arr@A_27a@A_27b)@(^ [V0f:$i] : (lam@A_27a@(^ [V1x:$i] : (ap@V0f@V1x))))))))).
thf(ax_thm_2Ebool_2EETA__AX,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0t:$i] : ((mem@V0t@(arr@A_27a@A_27b)) => ((lam@A_27a@(^ [V1x:$i] : (ap@V0t@V1x))) = V0t)))))).
thf(conj_thm_2Ebool_2ETRUTH,lemma,$true).
thf(conj_thm_2Ebool_2EIMP__ANTISYM__AX,lemma,( ! [V0t1:$i] : ((mem@V0t1@bool) => ( ! [V1t2:$i] : ((mem@V1t2@bool) => (((p@V0t1) => (p@V1t2)) => (((p@V1t2) => (p@V0t1)) => ((p@V0t1) <=> (p@V1t2))))))))).
thf(conj_thm_2Ebool_2EFALSITY,lemma,( ! [V0t:$i] : ((mem@V0t@bool) => ($false => (p@V0t))))).
thf(conj_thm_2Ebool_2EEXCLUDED__MIDDLE,lemma,( ! [V0t:$i] : ((mem@V0t@bool) => ((p@V0t) | (~ (p@V0t)))))).
thf(conj_thm_2Ebool_2EFORALL__SIMP,lemma,( ! [A_27a:del]: ( ! [V0t:$i] : ((mem@V0t@bool) => (( ! [V1x:$i] : ((mem@V1x@A_27a) => (p@V0t))) <=> (p@V0t)))))).
thf(conj_thm_2Ebool_2ECONJ__ASSOC,lemma,( ! [V0t1:$i] : ((mem@V0t1@bool) => ( ! [V1t2:$i] : ((mem@V1t2@bool) => ( ! [V2t3:$i] : ((mem@V2t3@bool) => (((p@V0t1) & ((p@V1t2) & (p@V2t3))) <=> (((p@V0t1) & (p@V1t2)) & (p@V2t3)))))))))).
thf(conj_thm_2Ebool_2EAND__CLAUSES,lemma,( ! [V0t:$i] : ((mem@V0t@bool) => ((($true & (p@V0t)) <=> (p@V0t)) & ((((p@V0t) & $true) <=> (p@V0t)) & ((($false & (p@V0t)) <=> $false) & ((((p@V0t) & $false) <=> $false) & (((p@V0t) & (p@V0t)) <=> (p@V0t))))))))).
thf(conj_thm_2Ebool_2EOR__CLAUSES,lemma,( ! [V0t:$i] : ((mem@V0t@bool) => ((($true | (p@V0t)) <=> $true) & ((((p@V0t) | $true) <=> $true) & ((($false | (p@V0t)) <=> (p@V0t)) & ((((p@V0t) | $false) <=> (p@V0t)) & (((p@V0t) | (p@V0t)) <=> (p@V0t))))))))).
thf(conj_thm_2Ebool_2EIMP__CLAUSES,lemma,( ! [V0t:$i] : ((mem@V0t@bool) => ((($true => (p@V0t)) <=> (p@V0t)) & ((((p@V0t) => $true) <=> $true) & ((($false => (p@V0t)) <=> $true) & ((((p@V0t) => (p@V0t)) <=> $true) & (((p@V0t) => $false) <=> (~ (p@V0t)))))))))).
thf(conj_thm_2Ebool_2ENOT__CLAUSES,lemma,(( ! [V0t:$i] : ((mem@V0t@bool) => ((~ (~ (p@V0t))) <=> (p@V0t)))) & (((~ ($true)) <=> $false) & ((~ ($false)) <=> $true)))).
thf(conj_thm_2Ebool_2EEQ__REFL,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => (V0x = V0x))))).
thf(conj_thm_2Ebool_2EREFL__CLAUSE,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ((V0x = V0x) <=> $true))))).
thf(conj_thm_2Ebool_2EEQ__SYM__EQ,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1y:$i] : ((mem@V1y@A_27a) => ((V0x = V1y) <=> (V1y = V0x)))))))).
thf(conj_thm_2Ebool_2EEQ__CLAUSES,lemma,( ! [V0t:$i] : ((mem@V0t@bool) => ((($true <=> (p@V0t)) <=> (p@V0t)) & ((((p@V0t) <=> $true) <=> (p@V0t)) & ((($false <=> (p@V0t)) <=> (~ (p@V0t))) & (((p@V0t) <=> $false) <=> (~ (p@V0t))))))))).
thf(conj_thm_2Ebool_2ECOND__CLAUSES,lemma,( ! [A_27a:del]: ( ! [V0t1:$i] : ((mem@V0t1@A_27a) => ( ! [V1t2:$i] : ((mem@V1t2@A_27a) => (((ap@(ap@(ap@(c_2Ebool_2ECOND@A_27a)@c_2Ebool_2ET)@V0t1)@V1t2) = V0t1) & ((ap@(ap@(ap@(c_2Ebool_2ECOND@A_27a)@c_2Ebool_2EF)@V0t1)@V1t2) = V1t2)))))))).
thf(conj_thm_2Ebool_2ELEFT__FORALL__OR__THM,lemma,( ! [A_27a:del]: ( ! [V0Q:$i] : ((mem@V0Q@bool) => ( ! [V1P:$i] : ((mem@V1P@(arr@A_27a@bool)) => (( ! [V2x:$i] : ((mem@V2x@A_27a) => ((p@(ap@V1P@V2x)) | (p@V0Q)))) <=> (( ! [V3x:$i] : ((mem@V3x@A_27a) => (p@(ap@V1P@V3x)))) | (p@V0Q))))))))).
thf(conj_thm_2Ebool_2EDISJ__ASSOC,lemma,( ! [V0A:$i] : ((mem@V0A@bool) => ( ! [V1B:$i] : ((mem@V1B@bool) => ( ! [V2C:$i] : ((mem@V2C@bool) => (((p@V0A) | ((p@V1B) | (p@V2C))) <=> (((p@V0A) | (p@V1B)) | (p@V2C)))))))))).
thf(conj_thm_2Ebool_2EDE__MORGAN__THM,lemma,( ! [V0A:$i] : ((mem@V0A@bool) => ( ! [V1B:$i] : ((mem@V1B@bool) => (((~ ((p@V0A) & (p@V1B))) <=> ((~ (p@V0A)) | (~ (p@V1B)))) & ((~ ((p@V0A) | (p@V1B))) <=> ((~ (p@V0A)) & (~ (p@V1B)))))))))).
thf(conj_thm_2Ebool_2ELEFT__OR__OVER__AND,lemma,( ! [V0A:$i] : ((mem@V0A@bool) => ( ! [V1B:$i] : ((mem@V1B@bool) => ( ! [V2C:$i] : ((mem@V2C@bool) => (((p@V0A) | ((p@V1B) & (p@V2C))) <=> (((p@V0A) | (p@V1B)) & ((p@V0A) | (p@V2C))))))))))).
thf(conj_thm_2Ebool_2ERIGHT__OR__OVER__AND,lemma,( ! [V0A:$i] : ((mem@V0A@bool) => ( ! [V1B:$i] : ((mem@V1B@bool) => ( ! [V2C:$i] : ((mem@V2C@bool) => ((((p@V1B) & (p@V2C)) | (p@V0A)) <=> (((p@V1B) | (p@V0A)) & ((p@V2C) | (p@V0A))))))))))).
thf(conj_thm_2Ebool_2EIMP__DISJ__THM,lemma,( ! [V0A:$i] : ((mem@V0A@bool) => ( ! [V1B:$i] : ((mem@V1B@bool) => (((p@V0A) => (p@V1B)) <=> ((~ (p@V0A)) | (p@V1B)))))))).
thf(conj_thm_2Ebool_2EIMP__F__EQ__F,lemma,( ! [V0t:$i] : ((mem@V0t@bool) => (((p@V0t) => $false) <=> ((p@V0t) <=> $false))))).
thf(conj_thm_2Ebool_2EAND__IMP__INTRO,lemma,( ! [V0t1:$i] : ((mem@V0t1@bool) => ( ! [V1t2:$i] : ((mem@V1t2@bool) => ( ! [V2t3:$i] : ((mem@V2t3@bool) => (((p@V0t1) => ((p@V1t2) => (p@V2t3))) <=> (((p@V0t1) & (p@V1t2)) => (p@V2t3)))))))))).
thf(conj_thm_2Ebool_2EEQ__EXPAND,lemma,( ! [V0t1:$i] : ((mem@V0t1@bool) => ( ! [V1t2:$i] : ((mem@V1t2@bool) => (((p@V0t1) <=> (p@V1t2)) <=> (((p@V0t1) & (p@V1t2)) | ((~ (p@V0t1)) & (~ (p@V1t2)))))))))).
thf(conj_thm_2Ebool_2EIMP__CONG,lemma,( ! [V0x:$i] : ((mem@V0x@bool) => ( ! [V1x_27:$i] : ((mem@V1x_27@bool) => ( ! [V2y:$i] : ((mem@V2y@bool) => ( ! [V3y_27:$i] : ((mem@V3y_27@bool) => ((((p@V0x) <=> (p@V1x_27)) & ((p@V1x_27) => ((p@V2y) <=> (p@V3y_27)))) => (((p@V0x) => (p@V2y)) <=> ((p@V1x_27) => (p@V3y_27))))))))))))).
thf(conj_thm_2Ebool_2ECOND__CONG,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@bool) => ( ! [V1Q:$i] : ((mem@V1Q@bool) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ( ! [V3x_27:$i] : ((mem@V3x_27@A_27a) => ( ! [V4y:$i] : ((mem@V4y@A_27a) => ( ! [V5y_27:$i] : ((mem@V5y_27@A_27a) => ((((p@V0P) <=> (p@V1Q)) & (((p@V1Q) => (V2x = V3x_27)) & ((~ (p@V1Q)) => (V4y = V5y_27)))) => ((ap@(ap@(ap@(c_2Ebool_2ECOND@A_27a)@V0P)@V2x)@V4y) = (ap@(ap@(ap@(c_2Ebool_2ECOND@A_27a)@V1Q)@V3x_27)@V5y_27))))))))))))))))).
thf(conj_thm_2Ebool_2Ebool__case__thm,lemma,( ! [A_27a:del]: (( ! [V0t1:$i] : ((mem@V0t1@A_27a) => ( ! [V1t2:$i] : ((mem@V1t2@A_27a) => ((ap@(ap@(ap@(c_2Ebool_2ECOND@A_27a)@c_2Ebool_2ET)@V0t1)@V1t2) = V0t1))))) & ( ! [V2t1:$i] : ((mem@V2t1@A_27a) => ( ! [V3t2:$i] : ((mem@V3t2@A_27a) => ((ap@(ap@(ap@(c_2Ebool_2ECOND@A_27a)@c_2Ebool_2EF)@V2t1)@V3t2) = V3t2)))))))).
thf(conj_thm_2Ebool_2EBOUNDED__THM,lemma,( ! [V0v:$i] : ((mem@V0v@bool) => ((p@(ap@c_2Ebool_2EBOUNDED@V0v)) <=> $true)))).
thf(ax_thm_2Elist_2ETL__DEF,axiom,( ! [A_27a:del]: (((ap@(c_2Elist_2ETL@A_27a)@(c_2Elist_2ENIL@A_27a)) = (c_2Elist_2ENIL@A_27a)) & ( ! [V0h:$i] : ((mem@V0h@A_27a) => ( ! [V1t:$i] : ((mem@V1t@(ty_2Elist_2Elist@A_27a)) => ((ap@(c_2Elist_2ETL@A_27a)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V0h)@V1t)) = V1t)))))))).
thf(ax_thm_2Elist_2EAPPEND,axiom,( ! [A_27a:del]: (( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(c_2Elist_2ENIL@A_27a))@V0l) = V0l))) & ( ! [V1l1:$i] : ((mem@V1l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V2l2:$i] : ((mem@V2l2@(ty_2Elist_2Elist@A_27a)) => ( ! [V3h:$i] : ((mem@V3h@A_27a) => ((ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V3h)@V1l1))@V2l2) = (ap@(ap@(c_2Elist_2ECONS@A_27a)@V3h)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V1l1)@V2l2)))))))))))).
thf(ax_thm_2Elist_2EMAP,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ((ap@(ap@(c_2Elist_2EMAP@A_27a@A_27b)@V0f)@(c_2Elist_2ENIL@A_27a)) = (c_2Elist_2ENIL@A_27b)))) & ( ! [V1f:$i] : ((mem@V1f@(arr@A_27a@A_27b)) => ( ! [V2h:$i] : ((mem@V2h@A_27a) => ( ! [V3t:$i] : ((mem@V3t@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Elist_2EMAP@A_27a@A_27b)@V1f)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V2h)@V3t)) = (ap@(ap@(c_2Elist_2ECONS@A_27b)@(ap@V1f@V2h))@(ap@(ap@(c_2Elist_2EMAP@A_27a@A_27b)@V1f)@V3t))))))))))))).
thf(ax_thm_2Elist_2EEVERY__DEF,axiom,( ! [A_27a:del]: (( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Elist_2EEVERY@A_27a)@V0P)@(c_2Elist_2ENIL@A_27a))) <=> $true))) & ( ! [V1P:$i] : ((mem@V1P@(arr@A_27a@bool)) => ( ! [V2h:$i] : ((mem@V2h@A_27a) => ( ! [V3t:$i] : ((mem@V3t@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Elist_2EEVERY@A_27a)@V1P)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V2h)@V3t))) <=> ((p@(ap@V1P@V2h)) & (p@(ap@(ap@(c_2Elist_2EEVERY@A_27a)@V1P)@V3t))))))))))))).
thf(conj_thm_2Elist_2Elist__induction,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@(ty_2Elist_2Elist@A_27a)@bool)) => (((p@(ap@V0P@(c_2Elist_2ENIL@A_27a))) & ( ! [V1t:$i] : ((mem@V1t@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@V0P@V1t)) => ( ! [V2h:$i] : ((mem@V2h@A_27a) => (p@(ap@V0P@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V2h)@V1t))))))))) => ( ! [V3l:$i] : ((mem@V3l@(ty_2Elist_2Elist@A_27a)) => (p@(ap@V0P@V3l))))))))).
thf(conj_thm_2Elist_2ECONS__11,lemma,( ! [A_27a:del]: ( ! [V0a0:$i] : ((mem@V0a0@A_27a) => ( ! [V1a1:$i] : ((mem@V1a1@(ty_2Elist_2Elist@A_27a)) => ( ! [V2a0_27:$i] : ((mem@V2a0_27@A_27a) => ( ! [V3a1_27:$i] : ((mem@V3a1_27@(ty_2Elist_2Elist@A_27a)) => (((ap@(ap@(c_2Elist_2ECONS@A_27a)@V0a0)@V1a1) = (ap@(ap@(c_2Elist_2ECONS@A_27a)@V2a0_27)@V3a1_27)) <=> ((V0a0 = V2a0_27) & (V1a1 = V3a1_27))))))))))))).
thf(conj_thm_2Elist_2ENOT__NIL__CONS,lemma,( ! [A_27a:del]: ( ! [V0a1:$i] : ((mem@V0a1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1a0:$i] : ((mem@V1a0@A_27a) => (~ ((c_2Elist_2ENIL@A_27a) = (ap@(ap@(c_2Elist_2ECONS@A_27a)@V1a0)@V0a1))))))))).
thf(conj_thm_2Elist_2EAPPEND__NIL,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V0l)@(c_2Elist_2ENIL@A_27a)) = V0l))))).
thf(conj_thm_2Elist_2EAPPEND__ASSOC,lemma,( ! [A_27a:del]: ( ! [V0l1:$i] : ((mem@V0l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l2:$i] : ((mem@V1l2@(ty_2Elist_2Elist@A_27a)) => ( ! [V2l3:$i] : ((mem@V2l3@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V0l1)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V1l2)@V2l3)) = (ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V0l1)@V1l2))@V2l3)))))))))).
thf(conj_thm_2Elist_2EAPPEND__11,lemma,( ! [A_27a:del]: (( ! [V0l1:$i] : ((mem@V0l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l2:$i] : ((mem@V1l2@(ty_2Elist_2Elist@A_27a)) => ( ! [V2l3:$i] : ((mem@V2l3@(ty_2Elist_2Elist@A_27a)) => (((ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V0l1)@V1l2) = (ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V0l1)@V2l3)) <=> (V1l2 = V2l3)))))))) & ( ! [V3l1:$i] : ((mem@V3l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V4l2:$i] : ((mem@V4l2@(ty_2Elist_2Elist@A_27a)) => ( ! [V5l3:$i] : ((mem@V5l3@(ty_2Elist_2Elist@A_27a)) => (((ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V4l2)@V3l1) = (ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V5l3)@V3l1)) <=> (V4l2 = V5l3))))))))))).
thf(ax_thm_2Elist_2EREVERSE__DEF,axiom,( ! [A_27a:del]: (((ap@(c_2Elist_2EREVERSE@A_27a)@(c_2Elist_2ENIL@A_27a)) = (c_2Elist_2ENIL@A_27a)) & ( ! [V0h:$i] : ((mem@V0h@A_27a) => ( ! [V1t:$i] : ((mem@V1t@(ty_2Elist_2Elist@A_27a)) => ((ap@(c_2Elist_2EREVERSE@A_27a)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V0h)@V1t)) = (ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(c_2Elist_2EREVERSE@A_27a)@V1t))@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V0h)@(c_2Elist_2ENIL@A_27a))))))))))).
thf(conj_thm_2Elist_2EREVERSE__APPEND,lemma,( ! [A_27a:del]: ( ! [V0l1:$i] : ((mem@V0l1@(ty_2Elist_2Elist@A_27a)) => ( ! [V1l2:$i] : ((mem@V1l2@(ty_2Elist_2Elist@A_27a)) => ((ap@(c_2Elist_2EREVERSE@A_27a)@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V0l1)@V1l2)) = (ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(c_2Elist_2EREVERSE@A_27a)@V1l2))@(ap@(c_2Elist_2EREVERSE@A_27a)@V0l1))))))))).
thf(conj_thm_2Elist_2EREVERSE__EQ__NIL,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => (((ap@(c_2Elist_2EREVERSE@A_27a)@V0l) = (c_2Elist_2ENIL@A_27a)) <=> (V0l = (c_2Elist_2ENIL@A_27a))))))).
thf(ax_thm_2Elist_2ELAST__DEF,axiom,( ! [A_27a:del]: ( ! [V0h:$i] : ((mem@V0h@A_27a) => ( ! [V1t:$i] : ((mem@V1t@(ty_2Elist_2Elist@A_27a)) => ((ap@(c_2Elist_2ELAST@A_27a)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V0h)@V1t)) = (ap@(ap@(ap@(c_2Ebool_2ECOND@A_27a)@(ap@(ap@(c_2Emin_2E_3D@(ty_2Elist_2Elist@A_27a))@V1t)@(c_2Elist_2ENIL@A_27a)))@V0h)@(ap@(c_2Elist_2ELAST@A_27a)@V1t))))))))).
thf(ax_thm_2Elist_2EFRONT__DEF,axiom,( ! [A_27a:del]: ( ! [V0h:$i] : ((mem@V0h@A_27a) => ( ! [V1t:$i] : ((mem@V1t@(ty_2Elist_2Elist@A_27a)) => ((ap@(c_2Elist_2EFRONT@A_27a)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V0h)@V1t)) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Elist_2Elist@A_27a))@(ap@(ap@(c_2Emin_2E_3D@(ty_2Elist_2Elist@A_27a))@V1t)@(c_2Elist_2ENIL@A_27a)))@(c_2Elist_2ENIL@A_27a))@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V0h)@(ap@(c_2Elist_2EFRONT@A_27a)@V1t)))))))))).
thf(ax_thm_2Elist_2EREV__DEF,axiom,( ! [A_27a:del]: (( ! [V0acc:$i] : ((mem@V0acc@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Elist_2EREV@A_27a)@(c_2Elist_2ENIL@A_27a))@V0acc) = V0acc))) & ( ! [V1h:$i] : ((mem@V1h@A_27a) => ( ! [V2t:$i] : ((mem@V2t@(ty_2Elist_2Elist@A_27a)) => ( ! [V3acc:$i] : ((mem@V3acc@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Elist_2EREV@A_27a)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V1h)@V2t))@V3acc) = (ap@(ap@(c_2Elist_2EREV@A_27a)@V2t)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V1h)@V3acc)))))))))))).
thf(conj_thm_2Elist_2EREVERSE__REV,lemma,( ! [A_27a:del]: ( ! [V0L:$i] : ((mem@V0L@(ty_2Elist_2Elist@A_27a)) => ((ap@(c_2Elist_2EREVERSE@A_27a)@V0L) = (ap@(ap@(c_2Elist_2EREV@A_27a)@V0L)@(c_2Elist_2ENIL@A_27a))))))).
thf(conj_thm_2Elogroot_2ELOG__ADD,lemma,( ! [V0a:tp__ty_2Enum_2Enum] : ( ! [V1b:tp__ty_2Enum_2Enum] : ( ! [V2c: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 @ V0a))) & (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V1b))@(ap@(ap@c_2Earithmetic_2EEXP@(inj__ty_2Enum_2Enum @ V0a))@(inj__ty_2Enum_2Enum @ V2c))))) => ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Elogroot_2ELOG@(inj__ty_2Enum_2Enum @ V0a))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V1b))@(ap@(ap@c_2Earithmetic_2EEXP@(inj__ty_2Enum_2Enum @ V0a))@(inj__ty_2Enum_2Enum @ V2c))))) = V2c)))))).
thf(conj_thm_2Enumeral_2Enumeral__distrib,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V0n))) = V0n)) & (( ! [V1n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V1n))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) = V1n)) & (( ! [V2n:tp__ty_2Enum_2Enum] : ( ! [V3m:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V2n)))@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V3m)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Enumeral_2EiZ@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V2n))@(inj__ty_2Enum_2Enum @ V3m)))))))) & (( ! [V4n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2A@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V4n))) = fo__c_2Enum_2E0)) & (( ! [V5n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2A@(inj__ty_2Enum_2Enum @ V5n))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) = fo__c_2Enum_2E0)) & (( ! [V6n:tp__ty_2Enum_2Enum] : ( ! [V7m:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2A@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V6n)))@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V7m)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@(ap@c_2Earithmetic_2E_2A@(inj__ty_2Enum_2Enum @ V6n))@(inj__ty_2Enum_2Enum @ V7m))))))) & (( ! [V8n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2D@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V8n))) = fo__c_2Enum_2E0)) & (( ! [V9n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2D@(inj__ty_2Enum_2Enum @ V9n))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) = V9n)) & (( ! [V10n:tp__ty_2Enum_2Enum] : ( ! [V11m:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2D@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V10n)))@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V11m)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@(ap@c_2Earithmetic_2E_2D@(inj__ty_2Enum_2Enum @ V10n))@(inj__ty_2Enum_2Enum @ V11m))))))) & (( ! [V12n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2EEXP@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V12n))))) = fo__c_2Enum_2E0)) & (( ! [V13n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2EEXP@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V13n))))) = fo__c_2Enum_2E0)) & (( ! [V14n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2EEXP@(inj__ty_2Enum_2Enum @ V14n))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) & (( ! [V15n:tp__ty_2Enum_2Enum] : ( ! [V16m:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2EEXP@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V15n)))@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V16m)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@(ap@c_2Earithmetic_2EEXP@(inj__ty_2Enum_2Enum @ V15n))@(inj__ty_2Enum_2Enum @ V16m))))))) & (((surj__ty_2Enum_2Enum @ (ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))) & (( ! [V17n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@c_2Enum_2ESUC@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V17n)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V17n)))))) & (((surj__ty_2Enum_2Enum @ (ap@c_2Eprim__rec_2EPRE@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) = fo__c_2Enum_2E0) & (( ! [V18n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@c_2Eprim__rec_2EPRE@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V18n)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Eprim__rec_2EPRE@(inj__ty_2Enum_2Enum @ V18n)))))) & (( ! [V19n:tp__ty_2Enum_2Enum] : (((surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V19n))) = fo__c_2Enum_2E0) <=> (V19n = fo__c_2Earithmetic_2EZERO))) & (( ! [V20n:tp__ty_2Enum_2Enum] : ((fo__c_2Enum_2E0 = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V20n)))) <=> (V20n = fo__c_2Earithmetic_2EZERO))) & (( ! [V21n:tp__ty_2Enum_2Enum] : ( ! [V22m:tp__ty_2Enum_2Enum] : (((surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V21n))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V22m)))) <=> (V21n = V22m)))) & (( ! [V23n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V23n))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) <=> $false)) & (( ! [V24n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V24n)))) <=> (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))@(inj__ty_2Enum_2Enum @ V24n))))) & (( ! [V25n:tp__ty_2Enum_2Enum] : ( ! [V26m:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V25n)))@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V26m)))) <=> (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V25n))@(inj__ty_2Enum_2Enum @ V26m)))))) & (( ! [V27n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3E@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V27n))) <=> $false)) & (( ! [V28n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3E@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V28n)))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) <=> (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))@(inj__ty_2Enum_2Enum @ V28n))))) & (( ! [V29n:tp__ty_2Enum_2Enum] : ( ! [V30m:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3E@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V29n)))@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V30m)))) <=> (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V30m))@(inj__ty_2Enum_2Enum @ V29n)))))) & (( ! [V31n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V31n))) <=> $true)) & (( ! [V32n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V32n)))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) <=> (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V32n))@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))) & (( ! [V33n:tp__ty_2Enum_2Enum] : ( ! [V34m:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V33n)))@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V34m)))) <=> (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V33n))@(inj__ty_2Enum_2Enum @ V34m)))))) & (( ! [V35n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3E_3D@(inj__ty_2Enum_2Enum @ V35n))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) <=> $true)) & (( ! [V36n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3E_3D@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V36n))) <=> (V36n = fo__c_2Enum_2E0))) & (( ! [V37n:tp__ty_2Enum_2Enum] : ( ! [V38m:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3E_3D@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V37n)))@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V38m)))) <=> (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V38m))@(inj__ty_2Enum_2Enum @ V37n)))))) & (( ! [V39n:tp__ty_2Enum_2Enum] : ((p@(ap@c_2Earithmetic_2EODD@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V39n)))) <=> (p@(ap@c_2Earithmetic_2EODD@(inj__ty_2Enum_2Enum @ V39n))))) & (( ! [V40n:tp__ty_2Enum_2Enum] : ((p@(ap@c_2Earithmetic_2EEVEN@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V40n)))) <=> (p@(ap@c_2Earithmetic_2EEVEN@(inj__ty_2Enum_2Enum @ V40n))))) & ((~ (p@(ap@c_2Earithmetic_2EODD@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) & (p@(ap@c_2Earithmetic_2EEVEN@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))))))))))))))))))))))))))))))))))))).
thf(conj_thm_2Enumeral_2Enumeral__add,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : (((surj__ty_2Enum_2Enum @ (ap@c_2Enumeral_2EiZ@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))@(inj__ty_2Enum_2Enum @ V0n)))) = V0n) & (((surj__ty_2Enum_2Enum @ (ap@c_2Enumeral_2EiZ@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))) = V0n) & (((surj__ty_2Enum_2Enum @ (ap@c_2Enumeral_2EiZ@(ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0n)))@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V1m))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT2@(ap@c_2Enumeral_2EiZ@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m)))))) & (((surj__ty_2Enum_2Enum @ (ap@c_2Enumeral_2EiZ@(ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0n)))@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V1m))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT1@(ap@c_2Enum_2ESUC@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m)))))) & (((surj__ty_2Enum_2Enum @ (ap@c_2Enumeral_2EiZ@(ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V0n)))@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V1m))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT1@(ap@c_2Enum_2ESUC@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m)))))) & (((surj__ty_2Enum_2Enum @ (ap@c_2Enumeral_2EiZ@(ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V0n)))@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V1m))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT2@(ap@c_2Enum_2ESUC@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m)))))) & (((surj__ty_2Enum_2Enum @ (ap@c_2Enum_2ESUC@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))@(inj__ty_2Enum_2Enum @ V0n)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V0n)))) & (((surj__ty_2Enum_2Enum @ (ap@c_2Enum_2ESUC@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V0n)))) & (((surj__ty_2Enum_2Enum @ (ap@c_2Enum_2ESUC@(ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0n)))@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V1m))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT1@(ap@c_2Enum_2ESUC@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m)))))) & (((surj__ty_2Enum_2Enum @ (ap@c_2Enum_2ESUC@(ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0n)))@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V1m))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT2@(ap@c_2Enum_2ESUC@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m)))))) & (((surj__ty_2Enum_2Enum @ (ap@c_2Enum_2ESUC@(ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V0n)))@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V1m))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT2@(ap@c_2Enum_2ESUC@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m)))))) & (((surj__ty_2Enum_2Enum @ (ap@c_2Enum_2ESUC@(ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V0n)))@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V1m))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT1@(ap@c_2Enumeral_2EiiSUC@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m)))))) & (((surj__ty_2Enum_2Enum @ (ap@c_2Enumeral_2EiiSUC@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))@(inj__ty_2Enum_2Enum @ V0n)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Enumeral_2EiiSUC@(inj__ty_2Enum_2Enum @ V0n)))) & (((surj__ty_2Enum_2Enum @ (ap@c_2Enumeral_2EiiSUC@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Enumeral_2EiiSUC@(inj__ty_2Enum_2Enum @ V0n)))) & (((surj__ty_2Enum_2Enum @ (ap@c_2Enumeral_2EiiSUC@(ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0n)))@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V1m))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT2@(ap@c_2Enum_2ESUC@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m)))))) & (((surj__ty_2Enum_2Enum @ (ap@c_2Enumeral_2EiiSUC@(ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0n)))@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V1m))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT1@(ap@c_2Enumeral_2EiiSUC@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m)))))) & (((surj__ty_2Enum_2Enum @ (ap@c_2Enumeral_2EiiSUC@(ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V0n)))@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V1m))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT1@(ap@c_2Enumeral_2EiiSUC@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m)))))) & ((surj__ty_2Enum_2Enum @ (ap@c_2Enumeral_2EiiSUC@(ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V0n)))@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V1m))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT2@(ap@c_2Enumeral_2EiiSUC@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m)))))))))))))))))))))))))).
thf(conj_thm_2Enumeral_2Enumeral__eq,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : (((fo__c_2Earithmetic_2EZERO = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0n)))) <=> $false) & ((((surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0n))) = fo__c_2Earithmetic_2EZERO) <=> $false) & (((fo__c_2Earithmetic_2EZERO = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V0n)))) <=> $false) & ((((surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V0n))) = fo__c_2Earithmetic_2EZERO) <=> $false) & ((((surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0n))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V1m)))) <=> $false) & ((((surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V0n))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V1m)))) <=> $false) & ((((surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0n))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V1m)))) <=> (V0n = V1m)) & (((surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V0n))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V1m)))) <=> (V0n = V1m)))))))))))).
thf(conj_thm_2Enumeral_2Enumeral__lt,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : (((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0n)))) <=> $true) & (((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V0n)))) <=> $true) & (((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))) <=> $false) & (((p@(ap@(ap@c_2Eprim__rec_2E_3C@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0n)))@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V1m)))) <=> (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m)))) & (((p@(ap@(ap@c_2Eprim__rec_2E_3C@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V0n)))@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V1m)))) <=> (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m)))) & (((p@(ap@(ap@c_2Eprim__rec_2E_3C@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0n)))@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V1m)))) <=> (~ (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V1m))@(inj__ty_2Enum_2Enum @ V0n))))) & ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V0n)))@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V1m)))) <=> (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m))))))))))))).
thf(conj_thm_2Enumeral_2Enumeral__lte,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : (((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))@(inj__ty_2Enum_2Enum @ V0n))) <=> $true) & (((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0n)))@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))) <=> $false) & (((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V0n)))@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))) <=> $false) & (((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0n)))@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V1m)))) <=> (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m)))) & (((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0n)))@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V1m)))) <=> (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m)))) & (((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V0n)))@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V1m)))) <=> (~ (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V1m))@(inj__ty_2Enum_2Enum @ V0n))))) & ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V0n)))@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V1m)))) <=> (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m))))))))))))).
thf(conj_thm_2Enumeral_2Enumeral__pre,lemma,(((surj__ty_2Enum_2Enum @ (ap@c_2Eprim__rec_2EPRE@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))) = fo__c_2Earithmetic_2EZERO) & (((surj__ty_2Enum_2Enum @ (ap@c_2Eprim__rec_2EPRE@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))) = fo__c_2Earithmetic_2EZERO) & (( ! [V0n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@c_2Eprim__rec_2EPRE@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0n))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT2@(ap@c_2Eprim__rec_2EPRE@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0n))))))) & (( ! [V1n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@c_2Eprim__rec_2EPRE@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V1n))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V1n)))))) & ( ! [V2n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@c_2Eprim__rec_2EPRE@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V2n)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V2n)))))))))).
thf(conj_thm_2Enumeral_2Enumeral__texp__help,lemma,( ! [V0acc:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Enumeral_2Etexp__help@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))@(inj__ty_2Enum_2Enum @ V0acc))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V0acc)))) & (((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Enumeral_2Etexp__help@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V1n)))@(inj__ty_2Enum_2Enum @ V0acc))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Enumeral_2Etexp__help@(ap@c_2Eprim__rec_2EPRE@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V1n))))@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0acc))))) & ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Enumeral_2Etexp__help@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V1n)))@(inj__ty_2Enum_2Enum @ V0acc))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Enumeral_2Etexp__help@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V1n)))@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0acc)))))))))).
thf(conj_thm_2Enumeral_2ETWO__EXP__THM,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : (((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2EEXP@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(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))))) & (((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2EEXP@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0n))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@(ap@c_2Enumeral_2Etexp__help@(ap@c_2Eprim__rec_2EPRE@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0n))))@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))) & ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2EEXP@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V0n))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@(ap@c_2Enumeral_2Etexp__help@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0n)))@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))).
thf(conj_thm_2Enumeral__bit_2Enumeral__imod__2exp,lemma,( ! [A_27a:del]: (( ! [V0n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Enumeral__bit_2EiMOD__2EXP@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V0n))) = fo__c_2Earithmetic_2EZERO)) & (( ! [V1x:tp__ty_2Enum_2Enum] : ( ! [V2n:$i] : ((mem@V2n@A_27a) => ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Enumeral__bit_2EiMOD__2EXP@(inj__ty_2Enum_2Enum @ V1x))@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))) = fo__c_2Earithmetic_2EZERO)))) & (( ! [V3x:tp__ty_2Enum_2Enum] : ( ! [V4n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Enumeral__bit_2EiMOD__2EXP@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V3x))))@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V4n)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT1@(ap@(ap@c_2Enumeral__bit_2EiMOD__2EXP@(ap@(ap@c_2Earithmetic_2E_2D@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V3x))))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(inj__ty_2Enum_2Enum @ V4n))))))) & (( ! [V5x:tp__ty_2Enum_2Enum] : ( ! [V6n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Enumeral__bit_2EiMOD__2EXP@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V5x))))@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V6n)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2EBIT1@(ap@(ap@c_2Enumeral__bit_2EiMOD__2EXP@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V5x))))@(inj__ty_2Enum_2Enum @ V6n))))))) & (( ! [V7x:tp__ty_2Enum_2Enum] : ( ! [V8n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Enumeral__bit_2EiMOD__2EXP@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V7x))))@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V8n)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Enumeral_2EiDUB@(ap@(ap@c_2Enumeral__bit_2EiMOD__2EXP@(ap@(ap@c_2Earithmetic_2E_2D@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V7x))))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V8n)))))))) & ( ! [V9x:tp__ty_2Enum_2Enum] : ( ! [V10n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Enumeral__bit_2EiMOD__2EXP@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V9x))))@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V10n)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Enumeral_2EiDUB@(ap@(ap@c_2Enumeral__bit_2EiMOD__2EXP@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V9x))))@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V10n))))))))))))))).
thf(conj_thm_2Enumeral__bit_2EMOD__2EXP,lemma,(( ! [V0x:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Ebit_2EMOD__2EXP@(inj__ty_2Enum_2Enum @ V0x))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) = fo__c_2Enum_2E0)) & ( ! [V1x:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Ebit_2EMOD__2EXP@(inj__ty_2Enum_2Enum @ V1x))@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V2n)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@(ap@c_2Enumeral__bit_2EiMOD__2EXP@(inj__ty_2Enum_2Enum @ V1x))@(inj__ty_2Enum_2Enum @ V2n))))))))).
thf(conj_thm_2Enumeral__bit_2ENUMERAL__TIMES__2EXP,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Ebit_2ETIMES__2EXP@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) = fo__c_2Enum_2E0)) & ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2x:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Ebit_2ETIMES__2EXP@(inj__ty_2Enum_2Enum @ V1n))@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V2x)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@(ap@(ap@c_2Enumeral__bit_2ESFUNPOW@c_2Enumeral_2EiDUB)@(inj__ty_2Enum_2Enum @ V1n))@(inj__ty_2Enum_2Enum @ V2x))))))))).
thf(conj_thm_2Enumeral__bit_2ENUMERAL__iDIV2,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : (((surj__ty_2Enum_2Enum @ (ap@c_2Enumeral__bit_2EiDIV2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))) = fo__c_2Earithmetic_2EZERO) & (((surj__ty_2Enum_2Enum @ (ap@c_2Enumeral__bit_2EiDIV2@(ap@c_2Enumeral__bit_2EiSUC@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))) = fo__c_2Earithmetic_2EZERO) & (((surj__ty_2Enum_2Enum @ (ap@c_2Enumeral__bit_2EiDIV2@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0n)))) = V0n) & (((surj__ty_2Enum_2Enum @ (ap@c_2Enumeral__bit_2EiDIV2@(ap@c_2Enumeral__bit_2EiSUC@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V0n))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Enumeral__bit_2EiSUC@(inj__ty_2Enum_2Enum @ V0n)))) & (((surj__ty_2Enum_2Enum @ (ap@c_2Enumeral__bit_2EiDIV2@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V0n)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Enumeral__bit_2EiSUC@(inj__ty_2Enum_2Enum @ V0n)))) & (((surj__ty_2Enum_2Enum @ (ap@c_2Enumeral__bit_2EiDIV2@(ap@c_2Enumeral__bit_2EiSUC@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V0n))))) = (surj__ty_2Enum_2Enum @ (ap@c_2Enumeral__bit_2EiSUC@(inj__ty_2Enum_2Enum @ V0n)))) & ((surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Enumeral__bit_2EiSUC@(inj__ty_2Enum_2Enum @ V0n)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V0n))))))))))))).
thf(conj_thm_2Enumeral__bit_2ENUMERAL__DIV__2EXP,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Ebit_2EDIV__2EXP@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) = fo__c_2Enum_2E0)) & ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2x:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Ebit_2EDIV__2EXP@(inj__ty_2Enum_2Enum @ V1n))@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V2x)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@(ap@(ap@c_2Enumeral__bit_2ESFUNPOW@c_2Enumeral__bit_2EiDIV2)@(inj__ty_2Enum_2Enum @ V1n))@(inj__ty_2Enum_2Enum @ V2x))))))))).
thf(conj_thm_2Enumeral__bit_2ENUMERAL__SFUNPOW__iDIV2,lemma,(( ! [V0x:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@(ap@c_2Enumeral__bit_2ESFUNPOW@c_2Enumeral__bit_2EiDIV2)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V0x))) = V0x)) & (( ! [V1y:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@(ap@c_2Enumeral__bit_2ESFUNPOW@c_2Enumeral__bit_2EiDIV2)@(inj__ty_2Enum_2Enum @ V1y))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) = fo__c_2Enum_2E0)) & (( ! [V2n:tp__ty_2Enum_2Enum] : ( ! [V3x:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@(ap@c_2Enumeral__bit_2ESFUNPOW@c_2Enumeral__bit_2EiDIV2)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V2n))))@(inj__ty_2Enum_2Enum @ V3x))) = (surj__ty_2Enum_2Enum @ (ap@(ap@(ap@c_2Enumeral__bit_2ESFUNPOW@(ap@c_2Enumeral__bit_2EFDUB@c_2Enumeral__bit_2EiDIV2))@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V2n)))@(ap@c_2Enumeral__bit_2EiDIV2@(inj__ty_2Enum_2Enum @ V3x))))))) & ( ! [V4n:tp__ty_2Enum_2Enum] : ( ! [V5x:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@(ap@c_2Enumeral__bit_2ESFUNPOW@c_2Enumeral__bit_2EiDIV2)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V4n))))@(inj__ty_2Enum_2Enum @ V5x))) = (surj__ty_2Enum_2Enum @ (ap@(ap@(ap@c_2Enumeral__bit_2ESFUNPOW@(ap@c_2Enumeral__bit_2EFDUB@c_2Enumeral__bit_2EiDIV2))@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V4n)))@(ap@c_2Enumeral__bit_2EiDIV2@(ap@c_2Enumeral__bit_2EiDIV2@(inj__ty_2Enum_2Enum @ V5x)))))))))))).
thf(conj_thm_2Enumeral__bit_2ENUMERAL__SFUNPOW__FDUB,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)) => (( ! [V1x:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@(ap@c_2Enumeral__bit_2ESFUNPOW@(ap@c_2Enumeral__bit_2EFDUB@V0f))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V1x))) = V1x)) & (( ! [V2y:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@(ap@c_2Enumeral__bit_2ESFUNPOW@(ap@c_2Enumeral__bit_2EFDUB@V0f))@(inj__ty_2Enum_2Enum @ V2y))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) = fo__c_2Enum_2E0)) & (( ! [V3n:tp__ty_2Enum_2Enum] : ( ! [V4x:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@(ap@c_2Enumeral__bit_2ESFUNPOW@(ap@c_2Enumeral__bit_2EFDUB@V0f))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V3n))))@(inj__ty_2Enum_2Enum @ V4x))) = (surj__ty_2Enum_2Enum @ (ap@(ap@(ap@c_2Enumeral__bit_2ESFUNPOW@(ap@c_2Enumeral__bit_2EFDUB@(ap@c_2Enumeral__bit_2EFDUB@V0f)))@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V3n)))@(ap@(ap@c_2Enumeral__bit_2EFDUB@V0f)@(inj__ty_2Enum_2Enum @ V4x))))))) & ( ! [V5n:tp__ty_2Enum_2Enum] : ( ! [V6x:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@(ap@c_2Enumeral__bit_2ESFUNPOW@(ap@c_2Enumeral__bit_2EFDUB@V0f))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V5n))))@(inj__ty_2Enum_2Enum @ V6x))) = (surj__ty_2Enum_2Enum @ (ap@(ap@(ap@c_2Enumeral__bit_2ESFUNPOW@(ap@c_2Enumeral__bit_2EFDUB@(ap@c_2Enumeral__bit_2EFDUB@V0f)))@(ap@c_2Earithmetic_2ENUMERAL@(inj__ty_2Enum_2Enum @ V5n)))@(ap@(ap@c_2Enumeral__bit_2EFDUB@V0f)@(ap@(ap@c_2Enumeral__bit_2EFDUB@V0f)@(inj__ty_2Enum_2Enum @ V6x)))))))))))))).
thf(conj_thm_2Enumeral__bit_2EFDUB__iDIV2,lemma,( ! [V0x:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Enumeral__bit_2EFDUB@c_2Enumeral__bit_2EiDIV2)@(inj__ty_2Enum_2Enum @ V0x))) = (surj__ty_2Enum_2Enum @ (ap@c_2Enumeral__bit_2EiDIV2@(ap@c_2Enumeral__bit_2EiDIV2@(inj__ty_2Enum_2Enum @ V0x))))))).
thf(conj_thm_2Enumeral__bit_2EFDUB__FDUB,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)) => (((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Enumeral__bit_2EFDUB@(ap@c_2Enumeral__bit_2EFDUB@V0f))@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))) = fo__c_2Earithmetic_2EZERO) & (( ! [V1x:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Enumeral__bit_2EFDUB@(ap@c_2Enumeral__bit_2EFDUB@V0f))@(ap@c_2Enumeral__bit_2EiSUC@(inj__ty_2Enum_2Enum @ V1x)))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Enumeral__bit_2EFDUB@V0f)@(ap@(ap@c_2Enumeral__bit_2EFDUB@V0f)@(ap@c_2Enumeral__bit_2EiSUC@(inj__ty_2Enum_2Enum @ V1x))))))) & (( ! [V2x:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Enumeral__bit_2EFDUB@(ap@c_2Enumeral__bit_2EFDUB@V0f))@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V2x)))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Enumeral__bit_2EFDUB@V0f)@(ap@(ap@c_2Enumeral__bit_2EFDUB@V0f)@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V2x))))))) & ( ! [V3x:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Enumeral__bit_2EFDUB@(ap@c_2Enumeral__bit_2EFDUB@V0f))@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V3x)))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Enumeral__bit_2EFDUB@V0f)@(ap@(ap@c_2Enumeral__bit_2EFDUB@V0f)@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V3x))))))))))))).
thf(ax_thm_2Enumposrep_2El2n__def,axiom,(( ! [V0b:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Enumposrep_2El2n@(inj__ty_2Enum_2Enum @ V0b))@(c_2Elist_2ENIL@ty_2Enum_2Enum))) = fo__c_2Enum_2E0)) & ( ! [V1b:tp__ty_2Enum_2Enum] : ( ! [V2h:tp__ty_2Enum_2Enum] : ( ! [V3t:tp__c_ty_2Elist_2Elist_ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Enumposrep_2El2n@(inj__ty_2Enum_2Enum @ V1b))@(ap@(ap@(c_2Elist_2ECONS@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V2h))@(inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ V3t)))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(ap@(ap@c_2Earithmetic_2EMOD@(inj__ty_2Enum_2Enum @ V2h))@(inj__ty_2Enum_2Enum @ V1b)))@(ap@(ap@c_2Earithmetic_2E_2A@(inj__ty_2Enum_2Enum @ V1b))@(ap@(ap@c_2Enumposrep_2El2n@(inj__ty_2Enum_2Enum @ V1b))@(inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ V3t))))))))))).
thf(conj_thm_2Enumposrep_2En2l__def,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1b:tp__ty_2Enum_2Enum] : ((surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ (ap@(ap@c_2Enumposrep_2En2l@(inj__ty_2Enum_2Enum @ V1b))@(inj__ty_2Enum_2Enum @ V0n))) = (surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Elist_2Elist@ty_2Enum_2Enum))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1b)))@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V1b))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))@(ap@(ap@(c_2Elist_2ECONS@ty_2Enum_2Enum)@(ap@(ap@c_2Earithmetic_2EMOD@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1b)))@(c_2Elist_2ENIL@ty_2Enum_2Enum)))@(ap@(ap@(c_2Elist_2ECONS@ty_2Enum_2Enum)@(ap@(ap@c_2Earithmetic_2EMOD@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1b)))@(ap@(ap@c_2Enumposrep_2En2l@(inj__ty_2Enum_2Enum @ V1b))@(ap@(ap@c_2Earithmetic_2EDIV@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1b)))))))))).
thf(conj_thm_2Enumposrep_2ELENGTH__n2l,lemma,( ! [V0b: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 @ V0b))) => ((surj__ty_2Enum_2Enum @ (ap@(c_2Elist_2ELENGTH@ty_2Enum_2Enum)@(ap@(ap@c_2Enumposrep_2En2l@(inj__ty_2Enum_2Enum @ V0b))@(inj__ty_2Enum_2Enum @ V1n)))) = (surj__ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V1n))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(ap@c_2Enum_2ESUC@(ap@(ap@c_2Elogroot_2ELOG@(inj__ty_2Enum_2Enum @ V0b))@(inj__ty_2Enum_2Enum @ V1n)))))))))).
thf(conj_thm_2Enumposrep_2EEL__n2l,lemma,( ! [V0b:tp__ty_2Enum_2Enum] : ( ! [V1x:tp__ty_2Enum_2Enum] : ( ! [V2n: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@(c_2Elist_2ELENGTH@ty_2Enum_2Enum)@(ap@(ap@c_2Enumposrep_2En2l@(inj__ty_2Enum_2Enum @ V0b))@(inj__ty_2Enum_2Enum @ V2n)))))) => ((surj__ty_2Enum_2Enum @ (ap@(ap@(c_2Elist_2EEL@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V1x))@(ap@(ap@c_2Enumposrep_2En2l@(inj__ty_2Enum_2Enum @ V0b))@(inj__ty_2Enum_2Enum @ V2n)))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2EMOD@(ap@(ap@c_2Earithmetic_2EDIV@(inj__ty_2Enum_2Enum @ V2n))@(ap@(ap@c_2Earithmetic_2EEXP@(inj__ty_2Enum_2Enum @ V0b))@(inj__ty_2Enum_2Enum @ V1x))))@(inj__ty_2Enum_2Enum @ V0b))))))))).
thf(conj_thm_2Enumposrep_2En2l__BOUND,lemma,( ! [V0b: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 @ V0b))) => (p@(ap@(ap@(c_2Elist_2EEVERY@ty_2Enum_2Enum)@(ap@c_2Earithmetic_2E_3E@(inj__ty_2Enum_2Enum @ V0b)))@(ap@(ap@c_2Enumposrep_2En2l@(inj__ty_2Enum_2Enum @ V0b))@(inj__ty_2Enum_2Enum @ V1n)))))))).
thf(conj_thm_2Enumposrep_2El2n__pow2__compute,lemma,(( ! [V0p:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Enumposrep_2El2n@(ap@(ap@c_2Earithmetic_2EEXP@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V0p)))@(c_2Elist_2ENIL@ty_2Enum_2Enum))) = fo__c_2Enum_2E0)) & ( ! [V1p:tp__ty_2Enum_2Enum] : ( ! [V2h:tp__ty_2Enum_2Enum] : ( ! [V3t:tp__c_ty_2Elist_2Elist_ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Enumposrep_2El2n@(ap@(ap@c_2Earithmetic_2EEXP@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V1p)))@(ap@(ap@(c_2Elist_2ECONS@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V2h))@(inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ V3t)))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(ap@(ap@c_2Ebit_2EMOD__2EXP@(inj__ty_2Enum_2Enum @ V1p))@(inj__ty_2Enum_2Enum @ V2h)))@(ap@(ap@c_2Ebit_2ETIMES__2EXP@(inj__ty_2Enum_2Enum @ V1p))@(ap@(ap@c_2Enumposrep_2El2n@(ap@(ap@c_2Earithmetic_2EEXP@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V1p)))@(inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ V3t))))))))))).
thf(conj_thm_2Enumposrep_2En2l__pow2__compute,lemma,( ! [V0p: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 @ V0p))) => ((surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ (ap@(ap@c_2Enumposrep_2En2l@(ap@(ap@c_2Earithmetic_2EEXP@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V0p)))@(inj__ty_2Enum_2Enum @ V1n))) = (surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ (ap@(ap@(c_2Ebool_2ELET@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@(ty_2Elist_2Elist@ty_2Enum_2Enum))@(ap@(c_2Epair_2EUNCURRY@ty_2Enum_2Enum@ty_2Enum_2Enum@(ty_2Elist_2Elist@ty_2Enum_2Enum))@(lam@ty_2Enum_2Enum@(^ [V2q:$i] : (lam@ty_2Enum_2Enum@(^ [V3r:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Elist_2Elist@ty_2Enum_2Enum))@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@V2q)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@(ap@(c_2Elist_2ECONS@ty_2Enum_2Enum)@V3r)@(c_2Elist_2ENIL@ty_2Enum_2Enum)))@(ap@(ap@(c_2Elist_2ECONS@ty_2Enum_2Enum)@V3r)@(ap@(ap@c_2Enumposrep_2En2l@(ap@(ap@c_2Earithmetic_2EEXP@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V0p)))@V2q)))))))))@(ap@(ap@c_2Ebit_2EDIVMOD__2EXP@(inj__ty_2Enum_2Enum @ V0p))@(inj__ty_2Enum_2Enum @ V1n))))))))).
thf(conj_thm_2Epair_2EUNCURRY__DEF,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(arr@A_27b@A_27c))) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ( ! [V2y:$i] : ((mem@V2y@A_27b) => ((ap@(ap@(c_2Epair_2EUNCURRY@A_27a@A_27b@A_27c)@V0f)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V1x)@V2y)) = (ap@(ap@V0f@V1x)@V2y)))))))))))).
thf(ax_thm_2Epatricia__casts_2ESKIP1__def,axiom,( ! [V0c:tp__ty_2Estring_2Echar] : ( ! [V1s:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ((surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ (ap@c_2Epatricia__casts_2ESKIP1@(ap@(ap@(c_2Elist_2ECONS@ty_2Estring_2Echar)@(inj__ty_2Estring_2Echar @ V0c))@(inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ V1s)))) = V1s)))).
thf(ax_thm_2Epatricia__casts_2Estring__to__num__def,axiom,( ! [V0s:tp__c_ty_2Elist_2Elist_ty_2Estring_2Echar] : ((surj__ty_2Enum_2Enum @ (ap@c_2Epatricia__casts_2Estring__to__num@(inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ V0s))) = (surj__ty_2Enum_2Enum @ (ap@(ap@(ap@c_2EASCIInumbers_2Es2n@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))@c_2Estring_2EORD)@(ap@(ap@(c_2Elist_2ECONS@ty_2Estring_2Echar)@(ap@c_2Estring_2ECHR@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(inj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ V0s))))))).
thf(ax_thm_2Epatricia__casts_2Enum__to__string__def,axiom,( ! [V0n:tp__ty_2Enum_2Enum] : ((surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ (ap@c_2Epatricia__casts_2Enum__to__string@(inj__ty_2Enum_2Enum @ V0n))) = (surj__c_ty_2Elist_2Elist_ty_2Estring_2Echar @ (ap@c_2Epatricia__casts_2ESKIP1@(ap@(ap@(ap@c_2EASCIInumbers_2En2s@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))@c_2Estring_2ECHR)@(inj__ty_2Enum_2Enum @ V0n))))))).
thf(conj_thm_2Epatricia__casts_2EIMAGE__string__to__num,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : (((V0n = (surj__ty_2Enum_2Enum @ (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@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(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_2EDIV@(inj__ty_2Enum_2Enum @ V0n))@(ap@(ap@c_2Earithmetic_2EEXP@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))@(ap@(ap@c_2Elogroot_2ELOG@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(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))))))) <=> (p@(ap@(ap@(c_2Ebool_2EIN@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(ap@(c_2Epred__set_2EIMAGE@(ty_2Elist_2Elist@ty_2Estring_2Echar)@ty_2Enum_2Enum)@c_2Epatricia__casts_2Estring__to__num)@(c_2Epred__set_2EUNIV@(ty_2Elist_2Elist@ty_2Estring_2Echar)))))))).
thf(conj_thm_2Eprim__rec_2EPRE,lemma,(((surj__ty_2Enum_2Enum @ (ap@c_2Eprim__rec_2EPRE@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) = fo__c_2Enum_2E0) & ( ! [V0m:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@c_2Eprim__rec_2EPRE@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V0m)))) = V0m)))).
thf(conj_thm_2Eprim__rec_2ELESS__0,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V0n)))))).
thf(conj_thm_2Erich__list_2EMAP__REVERSE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Elist_2EMAP@A_27a@A_27b)@V0f)@(ap@(c_2Elist_2EREVERSE@A_27a)@V1l)) = (ap@(c_2Elist_2EREVERSE@A_27b)@(ap@(ap@(c_2Elist_2EMAP@A_27a@A_27b)@V0f)@V1l)))))))))).
thf(conj_thm_2Erich__list_2EEL__PRE__LENGTH,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ((~ (V0l = (c_2Elist_2ENIL@A_27a))) => ((ap@(ap@(c_2Elist_2EEL@A_27a)@(ap@c_2Eprim__rec_2EPRE@(ap@(c_2Elist_2ELENGTH@A_27a)@V0l)))@V0l) = (ap@(c_2Elist_2ELAST@A_27a)@V0l))))))).
thf(conj_thm_2Erich__list_2EEVERY__REVERSE,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(c_2Elist_2EEVERY@A_27a)@V0P)@(ap@(c_2Elist_2EREVERSE@A_27a)@V1l))) <=> (p@(ap@(ap@(c_2Elist_2EEVERY@A_27a)@V0P)@V1l))))))))).
thf(conj_thm_2Esat_2ENOT__NOT,lemma,( ! [V0t:$i] : ((mem@V0t@bool) => ((~ (~ (p@V0t))) <=> (p@V0t))))).
thf(conj_thm_2Esat_2EAND__INV__IMP,lemma,( ! [V0A:$i] : ((mem@V0A@bool) => ((p@V0A) => ((~ (p@V0A)) => $false))))).
thf(conj_thm_2Esat_2EOR__DUAL2,lemma,( ! [V0A:$i] : ((mem@V0A@bool) => ( ! [V1B:$i] : ((mem@V1B@bool) => (((~ ((p@V0A) | (p@V1B))) => $false) <=> (((p@V0A) => $false) => ((~ (p@V1B)) => $false)))))))).
thf(conj_thm_2Esat_2EOR__DUAL3,lemma,( ! [V0A:$i] : ((mem@V0A@bool) => ( ! [V1B:$i] : ((mem@V1B@bool) => (((~ ((~ (p@V0A)) | (p@V1B))) => $false) <=> ((p@V0A) => ((~ (p@V1B)) => $false)))))))).
thf(conj_thm_2Esat_2EAND__INV2,lemma,( ! [V0A:$i] : ((mem@V0A@bool) => (((~ (p@V0A)) => $false) => (((p@V0A) => $false) => $false))))).
thf(conj_thm_2Esat_2Edc__eq,lemma,( ! [V0p:$i] : ((mem@V0p@bool) => ( ! [V1q:$i] : ((mem@V1q@bool) => ( ! [V2r:$i] : ((mem@V2r@bool) => (((p@V0p) <=> ((p@V1q) <=> (p@V2r))) <=> (((p@V0p) | ((p@V1q) | (p@V2r))) & (((p@V0p) | ((~ (p@V2r)) | (~ (p@V1q)))) & (((p@V1q) | ((~ (p@V2r)) | (~ (p@V0p)))) & ((p@V2r) | ((~ (p@V1q)) | (~ (p@V0p))))))))))))))).
thf(conj_thm_2Esat_2Edc__conj,lemma,( ! [V0p:$i] : ((mem@V0p@bool) => ( ! [V1q:$i] : ((mem@V1q@bool) => ( ! [V2r:$i] : ((mem@V2r@bool) => (((p@V0p) <=> ((p@V1q) & (p@V2r))) <=> (((p@V0p) | ((~ (p@V1q)) | (~ (p@V2r)))) & (((p@V1q) | (~ (p@V0p))) & ((p@V2r) | (~ (p@V0p))))))))))))).
thf(conj_thm_2Esat_2Edc__disj,lemma,( ! [V0p:$i] : ((mem@V0p@bool) => ( ! [V1q:$i] : ((mem@V1q@bool) => ( ! [V2r:$i] : ((mem@V2r@bool) => (((p@V0p) <=> ((p@V1q) | (p@V2r))) <=> (((p@V0p) | (~ (p@V1q))) & (((p@V0p) | (~ (p@V2r))) & ((p@V1q) | ((p@V2r) | (~ (p@V0p)))))))))))))).
thf(conj_thm_2Esat_2Edc__imp,lemma,( ! [V0p:$i] : ((mem@V0p@bool) => ( ! [V1q:$i] : ((mem@V1q@bool) => ( ! [V2r:$i] : ((mem@V2r@bool) => (((p@V0p) <=> ((p@V1q) => (p@V2r))) <=> (((p@V0p) | (p@V1q)) & (((p@V0p) | (~ (p@V2r))) & ((~ (p@V1q)) | ((p@V2r) | (~ (p@V0p)))))))))))))).
thf(conj_thm_2Esat_2Edc__neg,lemma,( ! [V0p:$i] : ((mem@V0p@bool) => ( ! [V1q:$i] : ((mem@V1q@bool) => (((p@V0p) <=> (~ (p@V1q))) <=> (((p@V0p) | (p@V1q)) & ((~ (p@V1q)) | (~ (p@V0p)))))))))).
thf(conj_thm_2Esat_2Epth__ni1,lemma,( ! [V0p:$i] : ((mem@V0p@bool) => ( ! [V1q:$i] : ((mem@V1q@bool) => ((~ ((p@V0p) => (p@V1q))) => (p@V0p))))))).
thf(conj_thm_2Esat_2Epth__ni2,lemma,( ! [V0p:$i] : ((mem@V0p@bool) => ( ! [V1q:$i] : ((mem@V1q@bool) => ((~ ((p@V0p) => (p@V1q))) => (~ (p@V1q)))))))).
thf(conj_thm_2Esat_2Epth__no1,lemma,( ! [V0p:$i] : ((mem@V0p@bool) => ( ! [V1q:$i] : ((mem@V1q@bool) => ((~ ((p@V0p) | (p@V1q))) => (~ (p@V0p)))))))).
thf(conj_thm_2Esat_2Epth__no2,lemma,( ! [V0p:$i] : ((mem@V0p@bool) => ( ! [V1q:$i] : ((mem@V1q@bool) => ((~ ((p@V0p) | (p@V1q))) => (~ (p@V1q)))))))).
thf(conj_thm_2Esat_2Epth__nn,lemma,( ! [V0p:$i] : ((mem@V0p@bool) => ((~ (~ (p@V0p))) => (p@V0p))))).
thf(conj_thm_2Estring_2ECHR__11,lemma,( ! [V0r:tp__ty_2Enum_2Enum] : ( ! [V1r_27:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0r))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))) => ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V1r_27))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))) => (((surj__ty_2Estring_2Echar @ (ap@c_2Estring_2ECHR@(inj__ty_2Enum_2Enum @ V0r))) = (surj__ty_2Estring_2Echar @ (ap@c_2Estring_2ECHR@(inj__ty_2Enum_2Enum @ V1r_27)))) <=> (V0r = V1r_27))))))).
thf(conj_thm_2Estring_2EORD__CHR__RWT,lemma,( ! [V0r:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0r))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))) => ((surj__ty_2Enum_2Enum @ (ap@c_2Estring_2EORD@(ap@c_2Estring_2ECHR@(inj__ty_2Enum_2Enum @ V0r)))) = V0r)))).
thf(conj_thm_2Estring_2EORD__CHR__COMPUTE,lemma,( ! [V0_3E_20255:$i] : ((mem@V0_3E_20255@bool) => ( ! [V1n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@c_2Estring_2EORD@(ap@c_2Estring_2ECHR@(inj__ty_2Enum_2Enum @ V1n)))) = (surj__ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V1n))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))))@(inj__ty_2Enum_2Enum @ V1n))@(ap@(ap@(ap@(c_2Ecombin_2EFAIL@(arr@ty_2Estring_2Echar@ty_2Enum_2Enum)@bool)@c_2Estring_2EORD)@V0_3E_20255)@(ap@c_2Estring_2ECHR@(inj__ty_2Enum_2Enum @ V1n)))))))))).
thf(conj_thm_2Estring_2Eranged__char__nchotomy,lemma,( ! [V0c:tp__ty_2Estring_2Echar] : (? [V1n:tp__ty_2Enum_2Enum] : ((V0c = (surj__ty_2Estring_2Echar @ (ap@c_2Estring_2ECHR@(inj__ty_2Enum_2Enum @ V1n)))) & (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V1n))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))))))).
thf(conj_thm_2Epatricia__casts_2Estring__to__num__num__to__string,conjecture,( ! [V0n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@(c_2Ebool_2EIN@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(ap@(c_2Epred__set_2EIMAGE@(ty_2Elist_2Elist@ty_2Estring_2Echar)@ty_2Enum_2Enum)@c_2Epatricia__casts_2Estring__to__num)@(c_2Epred__set_2EUNIV@(ty_2Elist_2Elist@ty_2Estring_2Echar))))) => ((surj__ty_2Enum_2Enum @ (ap@c_2Epatricia__casts_2Estring__to__num@(ap@c_2Epatricia__casts_2Enum__to__string@(inj__ty_2Enum_2Enum @ V0n)))) = V0n)))).
