include('Axioms/intExtension^2.ax').
thf(tp_ty_2EordinalNotation_2Eosyntax,type,( ty_2EordinalNotation_2Eosyntax:del )).
thf(stp_ty_2EordinalNotation_2Eosyntax,type,(tp__ty_2EordinalNotation_2Eosyntax : $tType)).
thf(stp_inj_ty_2EordinalNotation_2Eosyntax,type,(inj__ty_2EordinalNotation_2Eosyntax : (tp__ty_2EordinalNotation_2Eosyntax > $i))).
thf(stp_surj_ty_2EordinalNotation_2Eosyntax,type,(surj__ty_2EordinalNotation_2Eosyntax : ($i > tp__ty_2EordinalNotation_2Eosyntax))).
thf(stp_inj_surj_ty_2EordinalNotation_2Eosyntax,axiom,( ! [X:tp__ty_2EordinalNotation_2Eosyntax] : ((surj__ty_2EordinalNotation_2Eosyntax @ (inj__ty_2EordinalNotation_2Eosyntax @ X)) = X))).
thf(stp_inj_mem_ty_2EordinalNotation_2Eosyntax,axiom,( ! [X:tp__ty_2EordinalNotation_2Eosyntax] : (mem @ (inj__ty_2EordinalNotation_2Eosyntax @ X) @ ty_2EordinalNotation_2Eosyntax))).
thf(stp_iso_mem_ty_2EordinalNotation_2Eosyntax,axiom,( ! [X:$i] : ((mem @ X @ ty_2EordinalNotation_2Eosyntax) => (X = (inj__ty_2EordinalNotation_2Eosyntax @ (surj__ty_2EordinalNotation_2Eosyntax @ X)))))).
thf(tp_c_2EordinalNotation_2EEnd,type,(c_2EordinalNotation_2EEnd:$i)).
thf(mem_c_2EordinalNotation_2EEnd,axiom,(mem@c_2EordinalNotation_2EEnd@(arr@ty_2Enum_2Enum@ty_2EordinalNotation_2Eosyntax))).
thf(stp_fo_c_2EordinalNotation_2EEnd,type,(fo__c_2EordinalNotation_2EEnd:(tp__ty_2Enum_2Enum > tp__ty_2EordinalNotation_2Eosyntax))).
thf(stp_eq_fo_c_2EordinalNotation_2EEnd,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ((inj__ty_2EordinalNotation_2Eosyntax @ (fo__c_2EordinalNotation_2EEnd @ X0)) = (ap @ c_2EordinalNotation_2EEnd @ (inj__ty_2Enum_2Enum @ X0))))).
thf(tp_c_2EordinalNotation_2EPlus,type,(c_2EordinalNotation_2EPlus:$i)).
thf(mem_c_2EordinalNotation_2EPlus,axiom,(mem@c_2EordinalNotation_2EPlus@(arr@ty_2EordinalNotation_2Eosyntax@(arr@ty_2Enum_2Enum@(arr@ty_2EordinalNotation_2Eosyntax@ty_2EordinalNotation_2Eosyntax))))).
thf(stp_fo_c_2EordinalNotation_2EPlus,type,(fo__c_2EordinalNotation_2EPlus:(tp__ty_2EordinalNotation_2Eosyntax > (tp__ty_2Enum_2Enum > (tp__ty_2EordinalNotation_2Eosyntax > tp__ty_2EordinalNotation_2Eosyntax))))).
thf(stp_eq_fo_c_2EordinalNotation_2EPlus,axiom,( ! [X0:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [X1:tp__ty_2Enum_2Enum] : ( ! [X2:tp__ty_2EordinalNotation_2Eosyntax] : ((inj__ty_2EordinalNotation_2Eosyntax @ (((fo__c_2EordinalNotation_2EPlus @ X0) @ X1) @ X2)) = (ap @ (ap @ (ap @ c_2EordinalNotation_2EPlus @ (inj__ty_2EordinalNotation_2Eosyntax @ X0)) @ (inj__ty_2Enum_2Enum @ X1)) @ (inj__ty_2EordinalNotation_2Eosyntax @ X2))))))).
thf(tp_c_2EordinalNotation_2Ecf1,type,(c_2EordinalNotation_2Ecf1:$i)).
thf(mem_c_2EordinalNotation_2Ecf1,axiom,(mem@c_2EordinalNotation_2Ecf1@(arr@ty_2EordinalNotation_2Eosyntax@(arr@ty_2EordinalNotation_2Eosyntax@ty_2Enum_2Enum)))).
thf(stp_fo_c_2EordinalNotation_2Ecf1,type,(fo__c_2EordinalNotation_2Ecf1:(tp__ty_2EordinalNotation_2Eosyntax > (tp__ty_2EordinalNotation_2Eosyntax > tp__ty_2Enum_2Enum)))).
thf(stp_eq_fo_c_2EordinalNotation_2Ecf1,axiom,( ! [X0:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [X1:tp__ty_2EordinalNotation_2Eosyntax] : ((inj__ty_2Enum_2Enum @ ((fo__c_2EordinalNotation_2Ecf1 @ X0) @ X1)) = (ap @ (ap @ c_2EordinalNotation_2Ecf1 @ (inj__ty_2EordinalNotation_2Eosyntax @ X0)) @ (inj__ty_2EordinalNotation_2Eosyntax @ X1)))))).
thf(tp_c_2EordinalNotation_2Ecf2,type,(c_2EordinalNotation_2Ecf2:$i)).
thf(mem_c_2EordinalNotation_2Ecf2,axiom,(mem@c_2EordinalNotation_2Ecf2@(arr@ty_2EordinalNotation_2Eosyntax@(arr@ty_2EordinalNotation_2Eosyntax@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum))))).
thf(stp_fo_c_2EordinalNotation_2Ecf2,type,(fo__c_2EordinalNotation_2Ecf2:(tp__ty_2EordinalNotation_2Eosyntax > (tp__ty_2EordinalNotation_2Eosyntax > (tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum))))).
thf(stp_eq_fo_c_2EordinalNotation_2Ecf2,axiom,( ! [X0:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [X1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [X2:tp__ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ (((fo__c_2EordinalNotation_2Ecf2 @ X0) @ X1) @ X2)) = (ap @ (ap @ (ap @ c_2EordinalNotation_2Ecf2 @ (inj__ty_2EordinalNotation_2Eosyntax @ X0)) @ (inj__ty_2EordinalNotation_2Eosyntax @ X1)) @ (inj__ty_2Enum_2Enum @ X2))))))).
thf(tp_c_2EordinalNotation_2Ecoeff,type,(c_2EordinalNotation_2Ecoeff:$i)).
thf(mem_c_2EordinalNotation_2Ecoeff,axiom,(mem@c_2EordinalNotation_2Ecoeff@(arr@ty_2EordinalNotation_2Eosyntax@ty_2Enum_2Enum))).
thf(stp_fo_c_2EordinalNotation_2Ecoeff,type,(fo__c_2EordinalNotation_2Ecoeff:(tp__ty_2EordinalNotation_2Eosyntax > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2EordinalNotation_2Ecoeff,axiom,( ! [X0:tp__ty_2EordinalNotation_2Eosyntax] : ((inj__ty_2Enum_2Enum @ (fo__c_2EordinalNotation_2Ecoeff @ X0)) = (ap @ c_2EordinalNotation_2Ecoeff @ (inj__ty_2EordinalNotation_2Eosyntax @ X0))))).
thf(tp_c_2EordinalNotation_2Eexpt,type,(c_2EordinalNotation_2Eexpt:$i)).
thf(mem_c_2EordinalNotation_2Eexpt,axiom,(mem@c_2EordinalNotation_2Eexpt@(arr@ty_2EordinalNotation_2Eosyntax@ty_2EordinalNotation_2Eosyntax))).
thf(stp_fo_c_2EordinalNotation_2Eexpt,type,(fo__c_2EordinalNotation_2Eexpt:(tp__ty_2EordinalNotation_2Eosyntax > tp__ty_2EordinalNotation_2Eosyntax))).
thf(stp_eq_fo_c_2EordinalNotation_2Eexpt,axiom,( ! [X0:tp__ty_2EordinalNotation_2Eosyntax] : ((inj__ty_2EordinalNotation_2Eosyntax @ (fo__c_2EordinalNotation_2Eexpt @ X0)) = (ap @ c_2EordinalNotation_2Eexpt @ (inj__ty_2EordinalNotation_2Eosyntax @ X0))))).
thf(tp_c_2EordinalNotation_2Efinp,type,(c_2EordinalNotation_2Efinp:$i)).
thf(mem_c_2EordinalNotation_2Efinp,axiom,(mem@c_2EordinalNotation_2Efinp@(arr@ty_2EordinalNotation_2Eosyntax@bool))).
thf(tp_c_2EordinalNotation_2Eis__ord,type,(c_2EordinalNotation_2Eis__ord:$i)).
thf(mem_c_2EordinalNotation_2Eis__ord,axiom,(mem@c_2EordinalNotation_2Eis__ord@(arr@ty_2EordinalNotation_2Eosyntax@bool))).
thf(tp_c_2EordinalNotation_2Eoless,type,(c_2EordinalNotation_2Eoless:$i)).
thf(mem_c_2EordinalNotation_2Eoless,axiom,(mem@c_2EordinalNotation_2Eoless@(arr@ty_2EordinalNotation_2Eosyntax@(arr@ty_2EordinalNotation_2Eosyntax@bool)))).
thf(tp_c_2EordinalNotation_2Eord__add,type,(c_2EordinalNotation_2Eord__add:$i)).
thf(mem_c_2EordinalNotation_2Eord__add,axiom,(mem@c_2EordinalNotation_2Eord__add@(arr@ty_2EordinalNotation_2Eosyntax@(arr@ty_2EordinalNotation_2Eosyntax@ty_2EordinalNotation_2Eosyntax)))).
thf(stp_fo_c_2EordinalNotation_2Eord__add,type,(fo__c_2EordinalNotation_2Eord__add:(tp__ty_2EordinalNotation_2Eosyntax > (tp__ty_2EordinalNotation_2Eosyntax > tp__ty_2EordinalNotation_2Eosyntax)))).
thf(stp_eq_fo_c_2EordinalNotation_2Eord__add,axiom,( ! [X0:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [X1:tp__ty_2EordinalNotation_2Eosyntax] : ((inj__ty_2EordinalNotation_2Eosyntax @ ((fo__c_2EordinalNotation_2Eord__add @ X0) @ X1)) = (ap @ (ap @ c_2EordinalNotation_2Eord__add @ (inj__ty_2EordinalNotation_2Eosyntax @ X0)) @ (inj__ty_2EordinalNotation_2Eosyntax @ X1)))))).
thf(tp_c_2EordinalNotation_2Eord__less,type,(c_2EordinalNotation_2Eord__less:$i)).
thf(mem_c_2EordinalNotation_2Eord__less,axiom,(mem@c_2EordinalNotation_2Eord__less@(arr@ty_2EordinalNotation_2Eosyntax@(arr@ty_2EordinalNotation_2Eosyntax@bool)))).
thf(tp_c_2EordinalNotation_2Eord__mult,type,(c_2EordinalNotation_2Eord__mult:$i)).
thf(mem_c_2EordinalNotation_2Eord__mult,axiom,(mem@c_2EordinalNotation_2Eord__mult@(arr@ty_2EordinalNotation_2Eosyntax@(arr@ty_2EordinalNotation_2Eosyntax@ty_2EordinalNotation_2Eosyntax)))).
thf(stp_fo_c_2EordinalNotation_2Eord__mult,type,(fo__c_2EordinalNotation_2Eord__mult:(tp__ty_2EordinalNotation_2Eosyntax > (tp__ty_2EordinalNotation_2Eosyntax > tp__ty_2EordinalNotation_2Eosyntax)))).
thf(stp_eq_fo_c_2EordinalNotation_2Eord__mult,axiom,( ! [X0:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [X1:tp__ty_2EordinalNotation_2Eosyntax] : ((inj__ty_2EordinalNotation_2Eosyntax @ ((fo__c_2EordinalNotation_2Eord__mult @ X0) @ X1)) = (ap @ (ap @ c_2EordinalNotation_2Eord__mult @ (inj__ty_2EordinalNotation_2Eosyntax @ X0)) @ (inj__ty_2EordinalNotation_2Eosyntax @ X1)))))).
thf(tp_c_2EordinalNotation_2Eord__sub,type,(c_2EordinalNotation_2Eord__sub:$i)).
thf(mem_c_2EordinalNotation_2Eord__sub,axiom,(mem@c_2EordinalNotation_2Eord__sub@(arr@ty_2EordinalNotation_2Eosyntax@(arr@ty_2EordinalNotation_2Eosyntax@ty_2EordinalNotation_2Eosyntax)))).
thf(stp_fo_c_2EordinalNotation_2Eord__sub,type,(fo__c_2EordinalNotation_2Eord__sub:(tp__ty_2EordinalNotation_2Eosyntax > (tp__ty_2EordinalNotation_2Eosyntax > tp__ty_2EordinalNotation_2Eosyntax)))).
thf(stp_eq_fo_c_2EordinalNotation_2Eord__sub,axiom,( ! [X0:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [X1:tp__ty_2EordinalNotation_2Eosyntax] : ((inj__ty_2EordinalNotation_2Eosyntax @ ((fo__c_2EordinalNotation_2Eord__sub @ X0) @ X1)) = (ap @ (ap @ c_2EordinalNotation_2Eord__sub @ (inj__ty_2EordinalNotation_2Eosyntax @ X0)) @ (inj__ty_2EordinalNotation_2Eosyntax @ X1)))))).
thf(tp_c_2EordinalNotation_2Eosyntax__CASE,type,(c_2EordinalNotation_2Eosyntax__CASE:(del>$i))).
thf(mem_c_2EordinalNotation_2Eosyntax__CASE,axiom,( ! [A_27a:del] : (mem@(c_2EordinalNotation_2Eosyntax__CASE@A_27a)@(arr@ty_2EordinalNotation_2Eosyntax@(arr@(arr@ty_2Enum_2Enum@A_27a)@(arr@(arr@ty_2EordinalNotation_2Eosyntax@(arr@ty_2Enum_2Enum@(arr@ty_2EordinalNotation_2Eosyntax@A_27a)))@A_27a)))))).
thf(tp_c_2EordinalNotation_2Eosyntax__size,type,(c_2EordinalNotation_2Eosyntax__size:$i)).
thf(mem_c_2EordinalNotation_2Eosyntax__size,axiom,(mem@c_2EordinalNotation_2Eosyntax__size@(arr@ty_2EordinalNotation_2Eosyntax@ty_2Enum_2Enum))).
thf(stp_fo_c_2EordinalNotation_2Eosyntax__size,type,(fo__c_2EordinalNotation_2Eosyntax__size:(tp__ty_2EordinalNotation_2Eosyntax > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2EordinalNotation_2Eosyntax__size,axiom,( ! [X0:tp__ty_2EordinalNotation_2Eosyntax] : ((inj__ty_2Enum_2Enum @ (fo__c_2EordinalNotation_2Eosyntax__size @ X0)) = (ap @ c_2EordinalNotation_2Eosyntax__size @ (inj__ty_2EordinalNotation_2Eosyntax @ X0))))).
thf(tp_c_2EordinalNotation_2Epadd,type,(c_2EordinalNotation_2Epadd:$i)).
thf(mem_c_2EordinalNotation_2Epadd,axiom,(mem@c_2EordinalNotation_2Epadd@(arr@ty_2EordinalNotation_2Eosyntax@(arr@ty_2EordinalNotation_2Eosyntax@(arr@ty_2Enum_2Enum@ty_2EordinalNotation_2Eosyntax))))).
thf(stp_fo_c_2EordinalNotation_2Epadd,type,(fo__c_2EordinalNotation_2Epadd:(tp__ty_2EordinalNotation_2Eosyntax > (tp__ty_2EordinalNotation_2Eosyntax > (tp__ty_2Enum_2Enum > tp__ty_2EordinalNotation_2Eosyntax))))).
thf(stp_eq_fo_c_2EordinalNotation_2Epadd,axiom,( ! [X0:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [X1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [X2:tp__ty_2Enum_2Enum] : ((inj__ty_2EordinalNotation_2Eosyntax @ (((fo__c_2EordinalNotation_2Epadd @ X0) @ X1) @ X2)) = (ap @ (ap @ (ap @ c_2EordinalNotation_2Epadd @ (inj__ty_2EordinalNotation_2Eosyntax @ X0)) @ (inj__ty_2EordinalNotation_2Eosyntax @ X1)) @ (inj__ty_2Enum_2Enum @ X2))))))).
thf(tp_c_2EordinalNotation_2Epmult,type,(c_2EordinalNotation_2Epmult:$i)).
thf(mem_c_2EordinalNotation_2Epmult,axiom,(mem@c_2EordinalNotation_2Epmult@(arr@ty_2EordinalNotation_2Eosyntax@(arr@ty_2EordinalNotation_2Eosyntax@(arr@ty_2Enum_2Enum@ty_2EordinalNotation_2Eosyntax))))).
thf(stp_fo_c_2EordinalNotation_2Epmult,type,(fo__c_2EordinalNotation_2Epmult:(tp__ty_2EordinalNotation_2Eosyntax > (tp__ty_2EordinalNotation_2Eosyntax > (tp__ty_2Enum_2Enum > tp__ty_2EordinalNotation_2Eosyntax))))).
thf(stp_eq_fo_c_2EordinalNotation_2Epmult,axiom,( ! [X0:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [X1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [X2:tp__ty_2Enum_2Enum] : ((inj__ty_2EordinalNotation_2Eosyntax @ (((fo__c_2EordinalNotation_2Epmult @ X0) @ X1) @ X2)) = (ap @ (ap @ (ap @ c_2EordinalNotation_2Epmult @ (inj__ty_2EordinalNotation_2Eosyntax @ X0)) @ (inj__ty_2EordinalNotation_2Eosyntax @ X1)) @ (inj__ty_2Enum_2Enum @ X2))))))).
thf(tp_c_2EordinalNotation_2Erank,type,(c_2EordinalNotation_2Erank:$i)).
thf(mem_c_2EordinalNotation_2Erank,axiom,(mem@c_2EordinalNotation_2Erank@(arr@ty_2EordinalNotation_2Eosyntax@ty_2Enum_2Enum))).
thf(stp_fo_c_2EordinalNotation_2Erank,type,(fo__c_2EordinalNotation_2Erank:(tp__ty_2EordinalNotation_2Eosyntax > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2EordinalNotation_2Erank,axiom,( ! [X0:tp__ty_2EordinalNotation_2Eosyntax] : ((inj__ty_2Enum_2Enum @ (fo__c_2EordinalNotation_2Erank @ X0)) = (ap @ c_2EordinalNotation_2Erank @ (inj__ty_2EordinalNotation_2Eosyntax @ X0))))).
thf(tp_c_2EordinalNotation_2Erestn,type,(c_2EordinalNotation_2Erestn:$i)).
thf(mem_c_2EordinalNotation_2Erestn,axiom,(mem@c_2EordinalNotation_2Erestn@(arr@ty_2EordinalNotation_2Eosyntax@(arr@ty_2Enum_2Enum@ty_2EordinalNotation_2Eosyntax)))).
thf(stp_fo_c_2EordinalNotation_2Erestn,type,(fo__c_2EordinalNotation_2Erestn:(tp__ty_2EordinalNotation_2Eosyntax > (tp__ty_2Enum_2Enum > tp__ty_2EordinalNotation_2Eosyntax)))).
thf(stp_eq_fo_c_2EordinalNotation_2Erestn,axiom,( ! [X0:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [X1:tp__ty_2Enum_2Enum] : ((inj__ty_2EordinalNotation_2Eosyntax @ ((fo__c_2EordinalNotation_2Erestn @ X0) @ X1)) = (ap @ (ap @ c_2EordinalNotation_2Erestn @ (inj__ty_2EordinalNotation_2Eosyntax @ X0)) @ (inj__ty_2Enum_2Enum @ X1)))))).
thf(tp_c_2EordinalNotation_2Etail,type,(c_2EordinalNotation_2Etail:$i)).
thf(mem_c_2EordinalNotation_2Etail,axiom,(mem@c_2EordinalNotation_2Etail@(arr@ty_2EordinalNotation_2Eosyntax@ty_2EordinalNotation_2Eosyntax))).
thf(stp_fo_c_2EordinalNotation_2Etail,type,(fo__c_2EordinalNotation_2Etail:(tp__ty_2EordinalNotation_2Eosyntax > tp__ty_2EordinalNotation_2Eosyntax))).
thf(stp_eq_fo_c_2EordinalNotation_2Etail,axiom,( ! [X0:tp__ty_2EordinalNotation_2Eosyntax] : ((inj__ty_2EordinalNotation_2Eosyntax @ (fo__c_2EordinalNotation_2Etail @ X0)) = (ap @ c_2EordinalNotation_2Etail @ (inj__ty_2EordinalNotation_2Eosyntax @ X0))))).
thf(stp_c_ty_2Eind__type_2Erecspace_ty_2Enum_2Enum,type,(tp__c_ty_2Eind__type_2Erecspace_ty_2Enum_2Enum : $tType)).
thf(stp_inj_c_ty_2Eind__type_2Erecspace_ty_2Enum_2Enum,type,(inj__c_ty_2Eind__type_2Erecspace_ty_2Enum_2Enum : (tp__c_ty_2Eind__type_2Erecspace_ty_2Enum_2Enum > $i))).
thf(stp_surj_c_ty_2Eind__type_2Erecspace_ty_2Enum_2Enum,type,(surj__c_ty_2Eind__type_2Erecspace_ty_2Enum_2Enum : ($i > tp__c_ty_2Eind__type_2Erecspace_ty_2Enum_2Enum))).
thf(stp_inj_surj_c_ty_2Eind__type_2Erecspace_ty_2Enum_2Enum,axiom,( ! [X:tp__c_ty_2Eind__type_2Erecspace_ty_2Enum_2Enum] : ((surj__c_ty_2Eind__type_2Erecspace_ty_2Enum_2Enum @ (inj__c_ty_2Eind__type_2Erecspace_ty_2Enum_2Enum @ X)) = X))).
thf(stp_inj_mem_c_ty_2Eind__type_2Erecspace_ty_2Enum_2Enum,axiom,( ! [X:tp__c_ty_2Eind__type_2Erecspace_ty_2Enum_2Enum] : (mem @ (inj__c_ty_2Eind__type_2Erecspace_ty_2Enum_2Enum @ X) @ (ty_2Eind__type_2Erecspace@ty_2Enum_2Enum)))).
thf(stp_iso_mem_c_ty_2Eind__type_2Erecspace_ty_2Enum_2Enum,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Eind__type_2Erecspace@ty_2Enum_2Enum)) => (X = (inj__c_ty_2Eind__type_2Erecspace_ty_2Enum_2Enum @ (surj__c_ty_2Eind__type_2Erecspace_ty_2Enum_2Enum @ X)))))).
thf(ax_thm_2EordinalNotation_2Eosyntax__TY__DEF,axiom,(? [V0rep:$i] : ((mem@V0rep@(arr@ty_2EordinalNotation_2Eosyntax@(ty_2Eind__type_2Erecspace@ty_2Enum_2Enum))) & (p@(ap@(ap@(c_2Ebool_2ETYPE__DEFINITION@(ty_2Eind__type_2Erecspace@ty_2Enum_2Enum)@ty_2EordinalNotation_2Eosyntax)@(lam@(ty_2Eind__type_2Erecspace@ty_2Enum_2Enum)@(^ [V1a0_27:$i] : (ap@(c_2Ebool_2E_21@(arr@(ty_2Eind__type_2Erecspace@ty_2Enum_2Enum)@bool))@(lam@(arr@(ty_2Eind__type_2Erecspace@ty_2Enum_2Enum)@bool)@(^ [V2_27osyntax_27:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@(c_2Ebool_2E_21@(ty_2Eind__type_2Erecspace@ty_2Enum_2Enum))@(lam@(ty_2Eind__type_2Erecspace@ty_2Enum_2Enum)@(^ [V3a0_27:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(c_2Ebool_2E_3F@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V4a:$i] : (ap@(ap@(c_2Emin_2E_3D@(ty_2Eind__type_2Erecspace@ty_2Enum_2Enum))@V3a0_27)@(ap@(lam@ty_2Enum_2Enum@(^ [V5a:$i] : (ap@(ap@(ap@(c_2Eind__type_2ECONSTR@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@V5a)@(lam@ty_2Enum_2Enum@(^ [V6n:$i] : (c_2Eind__type_2EBOTTOM@ty_2Enum_2Enum))))))@V4a))))))@(ap@(c_2Ebool_2E_3F@(ty_2Eind__type_2Erecspace@ty_2Enum_2Enum))@(lam@(ty_2Eind__type_2Erecspace@ty_2Enum_2Enum)@(^ [V7a0:$i] : (ap@(c_2Ebool_2E_3F@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V8a1:$i] : (ap@(c_2Ebool_2E_3F@(ty_2Eind__type_2Erecspace@ty_2Enum_2Enum))@(lam@(ty_2Eind__type_2Erecspace@ty_2Enum_2Enum)@(^ [V9a2:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Emin_2E_3D@(ty_2Eind__type_2Erecspace@ty_2Enum_2Enum))@V3a0_27)@(ap@(ap@(ap@(lam@(ty_2Eind__type_2Erecspace@ty_2Enum_2Enum)@(^ [V10a0:$i] : (lam@ty_2Enum_2Enum@(^ [V11a1:$i] : (lam@(ty_2Eind__type_2Erecspace@ty_2Enum_2Enum)@(^ [V12a2:$i] : (ap@(ap@(ap@(c_2Eind__type_2ECONSTR@ty_2Enum_2Enum)@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@V11a1)@(ap@(ap@(c_2Eind__type_2EFCONS@(ty_2Eind__type_2Erecspace@ty_2Enum_2Enum))@V10a0)@(ap@(ap@(c_2Eind__type_2EFCONS@(ty_2Eind__type_2Erecspace@ty_2Enum_2Enum))@V12a2)@(lam@ty_2Enum_2Enum@(^ [V13n:$i] : (c_2Eind__type_2EBOTTOM@ty_2Enum_2Enum))))))))))))@V7a0)@V8a1)@V9a2)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@V2_27osyntax_27@V7a0))@(ap@V2_27osyntax_27@V9a2))))))))))))))@(ap@V2_27osyntax_27@V3a0_27))))))@(ap@V2_27osyntax_27@V1a0_27))))))))@V0rep))))).
thf(ax_thm_2EordinalNotation_2Eosyntax__case__def,axiom,( ! [A_27a:del]: (( ! [V0a:tp__ty_2Enum_2Enum] : ( ! [V1f:$i] : ((mem@V1f@(arr@ty_2Enum_2Enum@A_27a)) => ( ! [V2f1:$i] : ((mem@V2f1@(arr@ty_2EordinalNotation_2Eosyntax@(arr@ty_2Enum_2Enum@(arr@ty_2EordinalNotation_2Eosyntax@A_27a)))) => ((ap@(ap@(ap@(c_2EordinalNotation_2Eosyntax__CASE@A_27a)@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V0a)))@V1f)@V2f1) = (ap@V1f@(inj__ty_2Enum_2Enum @ V0a)))))))) & ( ! [V3a0:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V4a1:tp__ty_2Enum_2Enum] : ( ! [V5a2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V6f:$i] : ((mem@V6f@(arr@ty_2Enum_2Enum@A_27a)) => ( ! [V7f1:$i] : ((mem@V7f1@(arr@ty_2EordinalNotation_2Eosyntax@(arr@ty_2Enum_2Enum@(arr@ty_2EordinalNotation_2Eosyntax@A_27a)))) => ((ap@(ap@(ap@(c_2EordinalNotation_2Eosyntax__CASE@A_27a)@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V3a0))@(inj__ty_2Enum_2Enum @ V4a1))@(inj__ty_2EordinalNotation_2Eosyntax @ V5a2)))@V6f)@V7f1) = (ap@(ap@(ap@V7f1@(inj__ty_2EordinalNotation_2Eosyntax @ V3a0))@(inj__ty_2Enum_2Enum @ V4a1))@(inj__ty_2EordinalNotation_2Eosyntax @ V5a2))))))))))))).
thf(ax_thm_2EordinalNotation_2Eosyntax__size__def,axiom,(( ! [V0a:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@c_2EordinalNotation_2Eosyntax__size@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V0a)))) = (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 @ V0a))))) & ( ! [V1a0:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V2a1:tp__ty_2Enum_2Enum] : ( ! [V3a2:tp__ty_2EordinalNotation_2Eosyntax] : ((surj__ty_2Enum_2Enum @ (ap@c_2EordinalNotation_2Eosyntax__size@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V1a0))@(inj__ty_2Enum_2Enum @ V2a1))@(inj__ty_2EordinalNotation_2Eosyntax @ V3a2)))) = (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))))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2EordinalNotation_2Eosyntax__size@(inj__ty_2EordinalNotation_2Eosyntax @ V1a0)))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V2a1))@(ap@c_2EordinalNotation_2Eosyntax__size@(inj__ty_2EordinalNotation_2Eosyntax @ V3a2)))))))))))).
thf(conj_thm_2EordinalNotation_2Edatatype__osyntax,lemma,( ! [V0osyntax:$i] : ((mem@V0osyntax@(arr@(arr@ty_2Enum_2Enum@ty_2EordinalNotation_2Eosyntax)@(arr@(arr@ty_2EordinalNotation_2Eosyntax@(arr@ty_2Enum_2Enum@(arr@ty_2EordinalNotation_2Eosyntax@ty_2EordinalNotation_2Eosyntax)))@bool))) => (p@(ap@(c_2Ebool_2EDATATYPE@bool)@(ap@(ap@V0osyntax@c_2EordinalNotation_2EEnd)@c_2EordinalNotation_2EPlus)))))).
thf(conj_thm_2EordinalNotation_2Eosyntax__11,lemma,(( ! [V0a:tp__ty_2Enum_2Enum] : ( ! [V1a_27:tp__ty_2Enum_2Enum] : (((surj__ty_2EordinalNotation_2Eosyntax @ (ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V0a))) = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V1a_27)))) <=> (V0a = V1a_27)))) & ( ! [V2a0:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V3a1:tp__ty_2Enum_2Enum] : ( ! [V4a2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V5a0_27:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V6a1_27:tp__ty_2Enum_2Enum] : ( ! [V7a2_27:tp__ty_2EordinalNotation_2Eosyntax] : (((surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V2a0))@(inj__ty_2Enum_2Enum @ V3a1))@(inj__ty_2EordinalNotation_2Eosyntax @ V4a2))) = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V5a0_27))@(inj__ty_2Enum_2Enum @ V6a1_27))@(inj__ty_2EordinalNotation_2Eosyntax @ V7a2_27)))) <=> ((V2a0 = V5a0_27) & ((V3a1 = V6a1_27) & (V4a2 = V7a2_27)))))))))))).
thf(conj_thm_2EordinalNotation_2Eosyntax__distinct,lemma,( ! [V0a2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V1a1:tp__ty_2Enum_2Enum] : ( ! [V2a0:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V3a:tp__ty_2Enum_2Enum] : (~~ ((surj__ty_2EordinalNotation_2Eosyntax @ (ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V3a))) = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V2a0))@(inj__ty_2Enum_2Enum @ V1a1))@(inj__ty_2EordinalNotation_2Eosyntax @ V0a2)))))))))).
thf(conj_thm_2EordinalNotation_2Eosyntax__nchotomy,lemma,( ! [V0oo:tp__ty_2EordinalNotation_2Eosyntax] : ((? [V1n:tp__ty_2Enum_2Enum] : (V0oo = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V1n))))) | (? [V2o:tp__ty_2EordinalNotation_2Eosyntax] : (? [V3n:tp__ty_2Enum_2Enum] : (? [V4o0:tp__ty_2EordinalNotation_2Eosyntax] : (V0oo = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V2o))@(inj__ty_2Enum_2Enum @ V3n))@(inj__ty_2EordinalNotation_2Eosyntax @ V4o0)))))))))).
thf(conj_thm_2EordinalNotation_2Eosyntax__Axiom,lemma,( ! [A_27a:del]: ( ! [V0f0:$i] : ((mem@V0f0@(arr@ty_2Enum_2Enum@A_27a)) => ( ! [V1f1:$i] : ((mem@V1f1@(arr@ty_2Enum_2Enum@(arr@ty_2EordinalNotation_2Eosyntax@(arr@ty_2EordinalNotation_2Eosyntax@(arr@A_27a@(arr@A_27a@A_27a)))))) => (? [V2fn:$i] : ((mem@V2fn@(arr@ty_2EordinalNotation_2Eosyntax@A_27a)) & (( ! [V3a:tp__ty_2Enum_2Enum] : ((ap@V2fn@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V3a))) = (ap@V0f0@(inj__ty_2Enum_2Enum @ V3a)))) & ( ! [V4a0:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V5a1:tp__ty_2Enum_2Enum] : ( ! [V6a2:tp__ty_2EordinalNotation_2Eosyntax] : ((ap@V2fn@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V4a0))@(inj__ty_2Enum_2Enum @ V5a1))@(inj__ty_2EordinalNotation_2Eosyntax @ V6a2))) = (ap@(ap@(ap@(ap@(ap@V1f1@(inj__ty_2Enum_2Enum @ V5a1))@(inj__ty_2EordinalNotation_2Eosyntax @ V4a0))@(inj__ty_2EordinalNotation_2Eosyntax @ V6a2))@(ap@V2fn@(inj__ty_2EordinalNotation_2Eosyntax @ V4a0)))@(ap@V2fn@(inj__ty_2EordinalNotation_2Eosyntax @ V6a2)))))))))))))))).
thf(conj_thm_2EordinalNotation_2Eosyntax__induction,lemma,( ! [V0P:$i] : ((mem@V0P@(arr@ty_2EordinalNotation_2Eosyntax@bool)) => ((( ! [V1n:tp__ty_2Enum_2Enum] : (p@(ap@V0P@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V1n))))) & ( ! [V2o:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V3o0:tp__ty_2EordinalNotation_2Eosyntax] : (((p@(ap@V0P@(inj__ty_2EordinalNotation_2Eosyntax @ V2o))) & (p@(ap@V0P@(inj__ty_2EordinalNotation_2Eosyntax @ V3o0)))) => ( ! [V4n:tp__ty_2Enum_2Enum] : (p@(ap@V0P@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V2o))@(inj__ty_2Enum_2Enum @ V4n))@(inj__ty_2EordinalNotation_2Eosyntax @ V3o0))))))))) => ( ! [V5o:tp__ty_2EordinalNotation_2Eosyntax] : (p@(ap@V0P@(inj__ty_2EordinalNotation_2Eosyntax @ V5o)))))))).
thf(conj_thm_2EordinalNotation_2Eosyntax__case__cong,lemma,( ! [A_27a:del]: ( ! [V0f_27:$i] : ((mem@V0f_27@(arr@ty_2Enum_2Enum@A_27a)) => ( ! [V1f1_27:$i] : ((mem@V1f1_27@(arr@ty_2EordinalNotation_2Eosyntax@(arr@ty_2Enum_2Enum@(arr@ty_2EordinalNotation_2Eosyntax@A_27a)))) => ( ! [V2M:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V3M_27:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V4f:$i] : ((mem@V4f@(arr@ty_2Enum_2Enum@A_27a)) => ( ! [V5f1:$i] : ((mem@V5f1@(arr@ty_2EordinalNotation_2Eosyntax@(arr@ty_2Enum_2Enum@(arr@ty_2EordinalNotation_2Eosyntax@A_27a)))) => (((V2M = V3M_27) & (( ! [V6a:tp__ty_2Enum_2Enum] : ((V3M_27 = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V6a)))) => ((ap@V4f@(inj__ty_2Enum_2Enum @ V6a)) = (ap@V0f_27@(inj__ty_2Enum_2Enum @ V6a))))) & ( ! [V7a0:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V8a1:tp__ty_2Enum_2Enum] : ( ! [V9a2:tp__ty_2EordinalNotation_2Eosyntax] : ((V3M_27 = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V7a0))@(inj__ty_2Enum_2Enum @ V8a1))@(inj__ty_2EordinalNotation_2Eosyntax @ V9a2)))) => ((ap@(ap@(ap@V5f1@(inj__ty_2EordinalNotation_2Eosyntax @ V7a0))@(inj__ty_2Enum_2Enum @ V8a1))@(inj__ty_2EordinalNotation_2Eosyntax @ V9a2)) = (ap@(ap@(ap@V1f1_27@(inj__ty_2EordinalNotation_2Eosyntax @ V7a0))@(inj__ty_2Enum_2Enum @ V8a1))@(inj__ty_2EordinalNotation_2Eosyntax @ V9a2))))))))) => ((ap@(ap@(ap@(c_2EordinalNotation_2Eosyntax__CASE@A_27a)@(inj__ty_2EordinalNotation_2Eosyntax @ V2M))@V4f)@V5f1) = (ap@(ap@(ap@(c_2EordinalNotation_2Eosyntax__CASE@A_27a)@(inj__ty_2EordinalNotation_2Eosyntax @ V3M_27))@V0f_27)@V1f1_27))))))))))))))).
thf(conj_thm_2EordinalNotation_2Eosyntax__case__eq,lemma,( ! [A_27a:del]: ( ! [V0x:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V1f:$i] : ((mem@V1f@(arr@ty_2Enum_2Enum@A_27a)) => ( ! [V2f1:$i] : ((mem@V2f1@(arr@ty_2EordinalNotation_2Eosyntax@(arr@ty_2Enum_2Enum@(arr@ty_2EordinalNotation_2Eosyntax@A_27a)))) => ( ! [V3v:$i] : ((mem@V3v@A_27a) => (((ap@(ap@(ap@(c_2EordinalNotation_2Eosyntax__CASE@A_27a)@(inj__ty_2EordinalNotation_2Eosyntax @ V0x))@V1f)@V2f1) = V3v) <=> ((? [V4n:tp__ty_2Enum_2Enum] : ((V0x = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V4n)))) & ((ap@V1f@(inj__ty_2Enum_2Enum @ V4n)) = V3v))) | (? [V5o_27:tp__ty_2EordinalNotation_2Eosyntax] : (? [V6n:tp__ty_2Enum_2Enum] : (? [V7o0:tp__ty_2EordinalNotation_2Eosyntax] : ((V0x = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V5o_27))@(inj__ty_2Enum_2Enum @ V6n))@(inj__ty_2EordinalNotation_2Eosyntax @ V7o0)))) & ((ap@(ap@(ap@V2f1@(inj__ty_2EordinalNotation_2Eosyntax @ V5o_27))@(inj__ty_2Enum_2Enum @ V6n))@(inj__ty_2EordinalNotation_2Eosyntax @ V7o0)) = V3v)))))))))))))))).
thf(ax_thm_2EordinalNotation_2Eexpt__def,axiom,(( ! [V0v0:tp__ty_2Enum_2Enum] : ((surj__ty_2EordinalNotation_2Eosyntax @ (ap@c_2EordinalNotation_2Eexpt@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V0v0)))) = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) & ( ! [V1e:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V2k:tp__ty_2Enum_2Enum] : ( ! [V3t:tp__ty_2EordinalNotation_2Eosyntax] : ((surj__ty_2EordinalNotation_2Eosyntax @ (ap@c_2EordinalNotation_2Eexpt@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V1e))@(inj__ty_2Enum_2Enum @ V2k))@(inj__ty_2EordinalNotation_2Eosyntax @ V3t)))) = V1e)))))).
thf(ax_thm_2EordinalNotation_2Ecoeff__def,axiom,(( ! [V0x:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@c_2EordinalNotation_2Ecoeff@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V0x)))) = V0x)) & ( ! [V1e:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V2k:tp__ty_2Enum_2Enum] : ( ! [V3t:tp__ty_2EordinalNotation_2Eosyntax] : ((surj__ty_2Enum_2Enum @ (ap@c_2EordinalNotation_2Ecoeff@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V1e))@(inj__ty_2Enum_2Enum @ V2k))@(inj__ty_2EordinalNotation_2Eosyntax @ V3t)))) = V2k)))))).
thf(ax_thm_2EordinalNotation_2Efinp__def,axiom,(( ! [V0v0:tp__ty_2Enum_2Enum] : ((p@(ap@c_2EordinalNotation_2Efinp@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V0v0)))) <=> $true)) & ( ! [V1v1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V2v2:tp__ty_2Enum_2Enum] : ( ! [V3v3:tp__ty_2EordinalNotation_2Eosyntax] : ((p@(ap@c_2EordinalNotation_2Efinp@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V1v1))@(inj__ty_2Enum_2Enum @ V2v2))@(inj__ty_2EordinalNotation_2Eosyntax @ V3v3)))) <=> $false)))))).
thf(ax_thm_2EordinalNotation_2Etail__def,axiom,( ! [V0e:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2t:tp__ty_2EordinalNotation_2Eosyntax] : ((surj__ty_2EordinalNotation_2Eosyntax @ (ap@c_2EordinalNotation_2Etail@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V0e))@(inj__ty_2Enum_2Enum @ V1k))@(inj__ty_2EordinalNotation_2Eosyntax @ V2t)))) = V2t))))).
thf(ax_thm_2EordinalNotation_2Erank__def,axiom,(( ! [V0v0:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@c_2EordinalNotation_2Erank@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V0v0)))) = fo__c_2Enum_2E0)) & ( ! [V1e:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V2k:tp__ty_2Enum_2Enum] : ( ! [V3t:tp__ty_2EordinalNotation_2Eosyntax] : ((surj__ty_2Enum_2Enum @ (ap@c_2EordinalNotation_2Erank@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V1e))@(inj__ty_2Enum_2Enum @ V2k))@(inj__ty_2EordinalNotation_2Eosyntax @ V3t)))) = (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))))@(ap@c_2EordinalNotation_2Erank@(inj__ty_2EordinalNotation_2Eosyntax @ V1e)))))))))).
thf(ax_thm_2EordinalNotation_2Eoless__def,axiom,(c_2EordinalNotation_2Eoless = (lam@ty_2EordinalNotation_2Eosyntax@(^ [V0a0:$i] : (lam@ty_2EordinalNotation_2Eosyntax@(^ [V1a1:$i] : (ap@(c_2Ebool_2E_21@(arr@ty_2EordinalNotation_2Eosyntax@(arr@ty_2EordinalNotation_2Eosyntax@bool)))@(lam@(arr@ty_2EordinalNotation_2Eosyntax@(arr@ty_2EordinalNotation_2Eosyntax@bool))@(^ [V2oless_27:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@(c_2Ebool_2E_21@ty_2EordinalNotation_2Eosyntax)@(lam@ty_2EordinalNotation_2Eosyntax@(^ [V3a0:$i] : (ap@(c_2Ebool_2E_21@ty_2EordinalNotation_2Eosyntax)@(lam@ty_2EordinalNotation_2Eosyntax@(^ [V4a1:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(c_2Ebool_2E_3F@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V5k1:$i] : (ap@(c_2Ebool_2E_3F@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V6k2:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Emin_2E_3D@ty_2EordinalNotation_2Eosyntax)@V3a0)@(ap@c_2EordinalNotation_2EEnd@V5k1)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Emin_2E_3D@ty_2EordinalNotation_2Eosyntax)@V4a1)@(ap@c_2EordinalNotation_2EEnd@V6k2)))@(ap@(ap@c_2Eprim__rec_2E_3C@V5k1)@V6k2))))))))))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(c_2Ebool_2E_3F@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V7k1:$i] : (ap@(c_2Ebool_2E_3F@ty_2EordinalNotation_2Eosyntax)@(lam@ty_2EordinalNotation_2Eosyntax@(^ [V8e2:$i] : (ap@(c_2Ebool_2E_3F@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V9k2:$i] : (ap@(c_2Ebool_2E_3F@ty_2EordinalNotation_2Eosyntax)@(lam@ty_2EordinalNotation_2Eosyntax@(^ [V10t2:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Emin_2E_3D@ty_2EordinalNotation_2Eosyntax)@V3a0)@(ap@c_2EordinalNotation_2EEnd@V7k1)))@(ap@(ap@(c_2Emin_2E_3D@ty_2EordinalNotation_2Eosyntax)@V4a1)@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@V8e2)@V9k2)@V10t2))))))))))))))))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(c_2Ebool_2E_3F@ty_2EordinalNotation_2Eosyntax)@(lam@ty_2EordinalNotation_2Eosyntax@(^ [V11e1:$i] : (ap@(c_2Ebool_2E_3F@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V12k1:$i] : (ap@(c_2Ebool_2E_3F@ty_2EordinalNotation_2Eosyntax)@(lam@ty_2EordinalNotation_2Eosyntax@(^ [V13t1:$i] : (ap@(c_2Ebool_2E_3F@ty_2EordinalNotation_2Eosyntax)@(lam@ty_2EordinalNotation_2Eosyntax@(^ [V14e2:$i] : (ap@(c_2Ebool_2E_3F@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V15k2:$i] : (ap@(c_2Ebool_2E_3F@ty_2EordinalNotation_2Eosyntax)@(lam@ty_2EordinalNotation_2Eosyntax@(^ [V16t2:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Emin_2E_3D@ty_2EordinalNotation_2Eosyntax)@V3a0)@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@V11e1)@V12k1)@V13t1)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Emin_2E_3D@ty_2EordinalNotation_2Eosyntax)@V4a1)@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@V14e2)@V15k2)@V16t2)))@(ap@(ap@V2oless_27@V11e1)@V14e2))))))))))))))))))))))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(c_2Ebool_2E_3F@ty_2EordinalNotation_2Eosyntax)@(lam@ty_2EordinalNotation_2Eosyntax@(^ [V17e1:$i] : (ap@(c_2Ebool_2E_3F@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V18k1:$i] : (ap@(c_2Ebool_2E_3F@ty_2EordinalNotation_2Eosyntax)@(lam@ty_2EordinalNotation_2Eosyntax@(^ [V19t1:$i] : (ap@(c_2Ebool_2E_3F@ty_2EordinalNotation_2Eosyntax)@(lam@ty_2EordinalNotation_2Eosyntax@(^ [V20e2:$i] : (ap@(c_2Ebool_2E_3F@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V21k2:$i] : (ap@(c_2Ebool_2E_3F@ty_2EordinalNotation_2Eosyntax)@(lam@ty_2EordinalNotation_2Eosyntax@(^ [V22t2:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Emin_2E_3D@ty_2EordinalNotation_2Eosyntax)@V3a0)@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@V17e1)@V18k1)@V19t1)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Emin_2E_3D@ty_2EordinalNotation_2Eosyntax)@V4a1)@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@V20e2)@V21k2)@V22t2)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Emin_2E_3D@ty_2EordinalNotation_2Eosyntax)@V17e1)@V20e2))@(ap@(ap@c_2Eprim__rec_2E_3C@V18k1)@V21k2)))))))))))))))))))))))@(ap@(c_2Ebool_2E_3F@ty_2EordinalNotation_2Eosyntax)@(lam@ty_2EordinalNotation_2Eosyntax@(^ [V23e1:$i] : (ap@(c_2Ebool_2E_3F@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V24k1:$i] : (ap@(c_2Ebool_2E_3F@ty_2EordinalNotation_2Eosyntax)@(lam@ty_2EordinalNotation_2Eosyntax@(^ [V25t1:$i] : (ap@(c_2Ebool_2E_3F@ty_2EordinalNotation_2Eosyntax)@(lam@ty_2EordinalNotation_2Eosyntax@(^ [V26e2:$i] : (ap@(c_2Ebool_2E_3F@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V27k2:$i] : (ap@(c_2Ebool_2E_3F@ty_2EordinalNotation_2Eosyntax)@(lam@ty_2EordinalNotation_2Eosyntax@(^ [V28t2:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Emin_2E_3D@ty_2EordinalNotation_2Eosyntax)@V3a0)@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@V23e1)@V24k1)@V25t1)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Emin_2E_3D@ty_2EordinalNotation_2Eosyntax)@V4a1)@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@V26e2)@V27k2)@V28t2)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Emin_2E_3D@ty_2EordinalNotation_2Eosyntax)@V23e1)@V26e2))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@V24k1)@V27k2))@(ap@(ap@V2oless_27@V25t1)@V28t2))))))))))))))))))))))))))))@(ap@(ap@V2oless_27@V3a0)@V4a1)))))))))@(ap@(ap@V2oless_27@V0a0)@V1a1))))))))))).
thf(conj_thm_2EordinalNotation_2Eoless__rules,lemma,(( ! [V0k1:tp__ty_2Enum_2Enum] : ( ! [V1k2:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0k1))@(inj__ty_2Enum_2Enum @ V1k2))) => (p@(ap@(ap@c_2EordinalNotation_2Eoless@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V0k1)))@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V1k2))))))) & (( ! [V2k1:tp__ty_2Enum_2Enum] : ( ! [V3e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V4k2:tp__ty_2Enum_2Enum] : ( ! [V5t2:tp__ty_2EordinalNotation_2Eosyntax] : (p@(ap@(ap@c_2EordinalNotation_2Eoless@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V2k1)))@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V3e2))@(inj__ty_2Enum_2Enum @ V4k2))@(inj__ty_2EordinalNotation_2Eosyntax @ V5t2)))))))) & (( ! [V6e1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V7k1:tp__ty_2Enum_2Enum] : ( ! [V8t1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V9e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V10k2:tp__ty_2Enum_2Enum] : ( ! [V11t2:tp__ty_2EordinalNotation_2Eosyntax] : ((p@(ap@(ap@c_2EordinalNotation_2Eoless@(inj__ty_2EordinalNotation_2Eosyntax @ V6e1))@(inj__ty_2EordinalNotation_2Eosyntax @ V9e2))) => (p@(ap@(ap@c_2EordinalNotation_2Eoless@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V6e1))@(inj__ty_2Enum_2Enum @ V7k1))@(inj__ty_2EordinalNotation_2Eosyntax @ V8t1)))@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V9e2))@(inj__ty_2Enum_2Enum @ V10k2))@(inj__ty_2EordinalNotation_2Eosyntax @ V11t2))))))))))) & (( ! [V12e1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V13k1:tp__ty_2Enum_2Enum] : ( ! [V14t1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V15e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V16k2:tp__ty_2Enum_2Enum] : ( ! [V17t2:tp__ty_2EordinalNotation_2Eosyntax] : (((V12e1 = V15e2) & (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V13k1))@(inj__ty_2Enum_2Enum @ V16k2)))) => (p@(ap@(ap@c_2EordinalNotation_2Eoless@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V12e1))@(inj__ty_2Enum_2Enum @ V13k1))@(inj__ty_2EordinalNotation_2Eosyntax @ V14t1)))@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V15e2))@(inj__ty_2Enum_2Enum @ V16k2))@(inj__ty_2EordinalNotation_2Eosyntax @ V17t2))))))))))) & ( ! [V18e1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V19k1:tp__ty_2Enum_2Enum] : ( ! [V20t1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V21e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V22k2:tp__ty_2Enum_2Enum] : ( ! [V23t2:tp__ty_2EordinalNotation_2Eosyntax] : (((V18e1 = V21e2) & ((V19k1 = V22k2) & (p@(ap@(ap@c_2EordinalNotation_2Eoless@(inj__ty_2EordinalNotation_2Eosyntax @ V20t1))@(inj__ty_2EordinalNotation_2Eosyntax @ V23t2))))) => (p@(ap@(ap@c_2EordinalNotation_2Eoless@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V18e1))@(inj__ty_2Enum_2Enum @ V19k1))@(inj__ty_2EordinalNotation_2Eosyntax @ V20t1)))@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V21e2))@(inj__ty_2Enum_2Enum @ V22k2))@(inj__ty_2EordinalNotation_2Eosyntax @ V23t2)))))))))))))))).
thf(conj_thm_2EordinalNotation_2Eoless__ind,lemma,( ! [V0oless_27:$i] : ((mem@V0oless_27@(arr@ty_2EordinalNotation_2Eosyntax@(arr@ty_2EordinalNotation_2Eosyntax@bool))) => ((( ! [V1k1:tp__ty_2Enum_2Enum] : ( ! [V2k2:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V1k1))@(inj__ty_2Enum_2Enum @ V2k2))) => (p@(ap@(ap@V0oless_27@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V1k1)))@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V2k2))))))) & (( ! [V3k1:tp__ty_2Enum_2Enum] : ( ! [V4e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V5k2:tp__ty_2Enum_2Enum] : ( ! [V6t2:tp__ty_2EordinalNotation_2Eosyntax] : (p@(ap@(ap@V0oless_27@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V3k1)))@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V4e2))@(inj__ty_2Enum_2Enum @ V5k2))@(inj__ty_2EordinalNotation_2Eosyntax @ V6t2)))))))) & (( ! [V7e1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V8k1:tp__ty_2Enum_2Enum] : ( ! [V9t1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V10e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V11k2:tp__ty_2Enum_2Enum] : ( ! [V12t2:tp__ty_2EordinalNotation_2Eosyntax] : ((p@(ap@(ap@V0oless_27@(inj__ty_2EordinalNotation_2Eosyntax @ V7e1))@(inj__ty_2EordinalNotation_2Eosyntax @ V10e2))) => (p@(ap@(ap@V0oless_27@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V7e1))@(inj__ty_2Enum_2Enum @ V8k1))@(inj__ty_2EordinalNotation_2Eosyntax @ V9t1)))@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V10e2))@(inj__ty_2Enum_2Enum @ V11k2))@(inj__ty_2EordinalNotation_2Eosyntax @ V12t2))))))))))) & (( ! [V13e1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V14k1:tp__ty_2Enum_2Enum] : ( ! [V15t1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V16e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V17k2:tp__ty_2Enum_2Enum] : ( ! [V18t2:tp__ty_2EordinalNotation_2Eosyntax] : (((V13e1 = V16e2) & (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V14k1))@(inj__ty_2Enum_2Enum @ V17k2)))) => (p@(ap@(ap@V0oless_27@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V13e1))@(inj__ty_2Enum_2Enum @ V14k1))@(inj__ty_2EordinalNotation_2Eosyntax @ V15t1)))@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V16e2))@(inj__ty_2Enum_2Enum @ V17k2))@(inj__ty_2EordinalNotation_2Eosyntax @ V18t2))))))))))) & ( ! [V19e1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V20k1:tp__ty_2Enum_2Enum] : ( ! [V21t1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V22e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V23k2:tp__ty_2Enum_2Enum] : ( ! [V24t2:tp__ty_2EordinalNotation_2Eosyntax] : (((V19e1 = V22e2) & ((V20k1 = V23k2) & (p@(ap@(ap@V0oless_27@(inj__ty_2EordinalNotation_2Eosyntax @ V21t1))@(inj__ty_2EordinalNotation_2Eosyntax @ V24t2))))) => (p@(ap@(ap@V0oless_27@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V19e1))@(inj__ty_2Enum_2Enum @ V20k1))@(inj__ty_2EordinalNotation_2Eosyntax @ V21t1)))@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V22e2))@(inj__ty_2Enum_2Enum @ V23k2))@(inj__ty_2EordinalNotation_2Eosyntax @ V24t2))))))))))))))) => ( ! [V25a0:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V26a1:tp__ty_2EordinalNotation_2Eosyntax] : ((p@(ap@(ap@c_2EordinalNotation_2Eoless@(inj__ty_2EordinalNotation_2Eosyntax @ V25a0))@(inj__ty_2EordinalNotation_2Eosyntax @ V26a1))) => (p@(ap@(ap@V0oless_27@(inj__ty_2EordinalNotation_2Eosyntax @ V25a0))@(inj__ty_2EordinalNotation_2Eosyntax @ V26a1)))))))))).
thf(conj_thm_2EordinalNotation_2Eoless__strongind,lemma,( ! [V0oless_27:$i] : ((mem@V0oless_27@(arr@ty_2EordinalNotation_2Eosyntax@(arr@ty_2EordinalNotation_2Eosyntax@bool))) => ((( ! [V1k1:tp__ty_2Enum_2Enum] : ( ! [V2k2:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V1k1))@(inj__ty_2Enum_2Enum @ V2k2))) => (p@(ap@(ap@V0oless_27@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V1k1)))@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V2k2))))))) & (( ! [V3k1:tp__ty_2Enum_2Enum] : ( ! [V4e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V5k2:tp__ty_2Enum_2Enum] : ( ! [V6t2:tp__ty_2EordinalNotation_2Eosyntax] : (p@(ap@(ap@V0oless_27@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V3k1)))@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V4e2))@(inj__ty_2Enum_2Enum @ V5k2))@(inj__ty_2EordinalNotation_2Eosyntax @ V6t2)))))))) & (( ! [V7e1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V8k1:tp__ty_2Enum_2Enum] : ( ! [V9t1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V10e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V11k2:tp__ty_2Enum_2Enum] : ( ! [V12t2:tp__ty_2EordinalNotation_2Eosyntax] : (((p@(ap@(ap@c_2EordinalNotation_2Eoless@(inj__ty_2EordinalNotation_2Eosyntax @ V7e1))@(inj__ty_2EordinalNotation_2Eosyntax @ V10e2))) & (p@(ap@(ap@V0oless_27@(inj__ty_2EordinalNotation_2Eosyntax @ V7e1))@(inj__ty_2EordinalNotation_2Eosyntax @ V10e2)))) => (p@(ap@(ap@V0oless_27@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V7e1))@(inj__ty_2Enum_2Enum @ V8k1))@(inj__ty_2EordinalNotation_2Eosyntax @ V9t1)))@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V10e2))@(inj__ty_2Enum_2Enum @ V11k2))@(inj__ty_2EordinalNotation_2Eosyntax @ V12t2))))))))))) & (( ! [V13e1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V14k1:tp__ty_2Enum_2Enum] : ( ! [V15t1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V16e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V17k2:tp__ty_2Enum_2Enum] : ( ! [V18t2:tp__ty_2EordinalNotation_2Eosyntax] : (((V13e1 = V16e2) & (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V14k1))@(inj__ty_2Enum_2Enum @ V17k2)))) => (p@(ap@(ap@V0oless_27@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V13e1))@(inj__ty_2Enum_2Enum @ V14k1))@(inj__ty_2EordinalNotation_2Eosyntax @ V15t1)))@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V16e2))@(inj__ty_2Enum_2Enum @ V17k2))@(inj__ty_2EordinalNotation_2Eosyntax @ V18t2))))))))))) & ( ! [V19e1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V20k1:tp__ty_2Enum_2Enum] : ( ! [V21t1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V22e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V23k2:tp__ty_2Enum_2Enum] : ( ! [V24t2:tp__ty_2EordinalNotation_2Eosyntax] : (((V19e1 = V22e2) & ((V20k1 = V23k2) & ((p@(ap@(ap@c_2EordinalNotation_2Eoless@(inj__ty_2EordinalNotation_2Eosyntax @ V21t1))@(inj__ty_2EordinalNotation_2Eosyntax @ V24t2))) & (p@(ap@(ap@V0oless_27@(inj__ty_2EordinalNotation_2Eosyntax @ V21t1))@(inj__ty_2EordinalNotation_2Eosyntax @ V24t2)))))) => (p@(ap@(ap@V0oless_27@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V19e1))@(inj__ty_2Enum_2Enum @ V20k1))@(inj__ty_2EordinalNotation_2Eosyntax @ V21t1)))@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V22e2))@(inj__ty_2Enum_2Enum @ V23k2))@(inj__ty_2EordinalNotation_2Eosyntax @ V24t2))))))))))))))) => ( ! [V25a0:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V26a1:tp__ty_2EordinalNotation_2Eosyntax] : ((p@(ap@(ap@c_2EordinalNotation_2Eoless@(inj__ty_2EordinalNotation_2Eosyntax @ V25a0))@(inj__ty_2EordinalNotation_2Eosyntax @ V26a1))) => (p@(ap@(ap@V0oless_27@(inj__ty_2EordinalNotation_2Eosyntax @ V25a0))@(inj__ty_2EordinalNotation_2Eosyntax @ V26a1)))))))))).
thf(conj_thm_2EordinalNotation_2Eoless__cases,lemma,( ! [V0a0:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V1a1:tp__ty_2EordinalNotation_2Eosyntax] : ((p@(ap@(ap@c_2EordinalNotation_2Eoless@(inj__ty_2EordinalNotation_2Eosyntax @ V0a0))@(inj__ty_2EordinalNotation_2Eosyntax @ V1a1))) <=> ((? [V2k1:tp__ty_2Enum_2Enum] : (? [V3k2:tp__ty_2Enum_2Enum] : ((V0a0 = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V2k1)))) & ((V1a1 = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V3k2)))) & (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V2k1))@(inj__ty_2Enum_2Enum @ V3k2))))))) | ((? [V4k1:tp__ty_2Enum_2Enum] : (? [V5e2:tp__ty_2EordinalNotation_2Eosyntax] : (? [V6k2:tp__ty_2Enum_2Enum] : (? [V7t2:tp__ty_2EordinalNotation_2Eosyntax] : ((V0a0 = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V4k1)))) & (V1a1 = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V5e2))@(inj__ty_2Enum_2Enum @ V6k2))@(inj__ty_2EordinalNotation_2Eosyntax @ V7t2))))))))) | ((? [V8e1:tp__ty_2EordinalNotation_2Eosyntax] : (? [V9k1:tp__ty_2Enum_2Enum] : (? [V10t1:tp__ty_2EordinalNotation_2Eosyntax] : (? [V11e2:tp__ty_2EordinalNotation_2Eosyntax] : (? [V12k2:tp__ty_2Enum_2Enum] : (? [V13t2:tp__ty_2EordinalNotation_2Eosyntax] : ((V0a0 = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V8e1))@(inj__ty_2Enum_2Enum @ V9k1))@(inj__ty_2EordinalNotation_2Eosyntax @ V10t1)))) & ((V1a1 = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V11e2))@(inj__ty_2Enum_2Enum @ V12k2))@(inj__ty_2EordinalNotation_2Eosyntax @ V13t2)))) & (p@(ap@(ap@c_2EordinalNotation_2Eoless@(inj__ty_2EordinalNotation_2Eosyntax @ V8e1))@(inj__ty_2EordinalNotation_2Eosyntax @ V11e2))))))))))) | ((? [V14e1:tp__ty_2EordinalNotation_2Eosyntax] : (? [V15k1:tp__ty_2Enum_2Enum] : (? [V16t1:tp__ty_2EordinalNotation_2Eosyntax] : (? [V17e2:tp__ty_2EordinalNotation_2Eosyntax] : (? [V18k2:tp__ty_2Enum_2Enum] : (? [V19t2:tp__ty_2EordinalNotation_2Eosyntax] : ((V0a0 = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V14e1))@(inj__ty_2Enum_2Enum @ V15k1))@(inj__ty_2EordinalNotation_2Eosyntax @ V16t1)))) & ((V1a1 = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V17e2))@(inj__ty_2Enum_2Enum @ V18k2))@(inj__ty_2EordinalNotation_2Eosyntax @ V19t2)))) & ((V14e1 = V17e2) & (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V15k1))@(inj__ty_2Enum_2Enum @ V18k2)))))))))))) | (? [V20e1:tp__ty_2EordinalNotation_2Eosyntax] : (? [V21k1:tp__ty_2Enum_2Enum] : (? [V22t1:tp__ty_2EordinalNotation_2Eosyntax] : (? [V23e2:tp__ty_2EordinalNotation_2Eosyntax] : (? [V24k2:tp__ty_2Enum_2Enum] : (? [V25t2:tp__ty_2EordinalNotation_2Eosyntax] : ((V0a0 = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V20e1))@(inj__ty_2Enum_2Enum @ V21k1))@(inj__ty_2EordinalNotation_2Eosyntax @ V22t1)))) & ((V1a1 = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V23e2))@(inj__ty_2Enum_2Enum @ V24k2))@(inj__ty_2EordinalNotation_2Eosyntax @ V25t2)))) & ((V20e1 = V23e2) & ((V21k1 = V24k2) & (p@(ap@(ap@c_2EordinalNotation_2Eoless@(inj__ty_2EordinalNotation_2Eosyntax @ V22t1))@(inj__ty_2EordinalNotation_2Eosyntax @ V25t2))))))))))))))))))))).
thf(conj_thm_2EordinalNotation_2Eoless__strong__ind,lemma,( ! [V0oless_27:$i] : ((mem@V0oless_27@(arr@ty_2EordinalNotation_2Eosyntax@(arr@ty_2EordinalNotation_2Eosyntax@bool))) => ((( ! [V1k1:tp__ty_2Enum_2Enum] : ( ! [V2k2:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V1k1))@(inj__ty_2Enum_2Enum @ V2k2))) => (p@(ap@(ap@V0oless_27@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V1k1)))@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V2k2))))))) & (( ! [V3k1:tp__ty_2Enum_2Enum] : ( ! [V4e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V5k2:tp__ty_2Enum_2Enum] : ( ! [V6t2:tp__ty_2EordinalNotation_2Eosyntax] : (p@(ap@(ap@V0oless_27@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V3k1)))@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V4e2))@(inj__ty_2Enum_2Enum @ V5k2))@(inj__ty_2EordinalNotation_2Eosyntax @ V6t2)))))))) & (( ! [V7e1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V8k1:tp__ty_2Enum_2Enum] : ( ! [V9t1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V10e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V11k2:tp__ty_2Enum_2Enum] : ( ! [V12t2:tp__ty_2EordinalNotation_2Eosyntax] : (((p@(ap@(ap@c_2EordinalNotation_2Eoless@(inj__ty_2EordinalNotation_2Eosyntax @ V7e1))@(inj__ty_2EordinalNotation_2Eosyntax @ V10e2))) & (p@(ap@(ap@V0oless_27@(inj__ty_2EordinalNotation_2Eosyntax @ V7e1))@(inj__ty_2EordinalNotation_2Eosyntax @ V10e2)))) => (p@(ap@(ap@V0oless_27@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V7e1))@(inj__ty_2Enum_2Enum @ V8k1))@(inj__ty_2EordinalNotation_2Eosyntax @ V9t1)))@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V10e2))@(inj__ty_2Enum_2Enum @ V11k2))@(inj__ty_2EordinalNotation_2Eosyntax @ V12t2))))))))))) & (( ! [V13e1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V14k1:tp__ty_2Enum_2Enum] : ( ! [V15t1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V16e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V17k2:tp__ty_2Enum_2Enum] : ( ! [V18t2:tp__ty_2EordinalNotation_2Eosyntax] : (((V13e1 = V16e2) & (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V14k1))@(inj__ty_2Enum_2Enum @ V17k2)))) => (p@(ap@(ap@V0oless_27@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V13e1))@(inj__ty_2Enum_2Enum @ V14k1))@(inj__ty_2EordinalNotation_2Eosyntax @ V15t1)))@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V16e2))@(inj__ty_2Enum_2Enum @ V17k2))@(inj__ty_2EordinalNotation_2Eosyntax @ V18t2))))))))))) & ( ! [V19e1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V20k1:tp__ty_2Enum_2Enum] : ( ! [V21t1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V22e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V23k2:tp__ty_2Enum_2Enum] : ( ! [V24t2:tp__ty_2EordinalNotation_2Eosyntax] : (((V19e1 = V22e2) & ((V20k1 = V23k2) & ((p@(ap@(ap@c_2EordinalNotation_2Eoless@(inj__ty_2EordinalNotation_2Eosyntax @ V21t1))@(inj__ty_2EordinalNotation_2Eosyntax @ V24t2))) & (p@(ap@(ap@V0oless_27@(inj__ty_2EordinalNotation_2Eosyntax @ V21t1))@(inj__ty_2EordinalNotation_2Eosyntax @ V24t2)))))) => (p@(ap@(ap@V0oless_27@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V19e1))@(inj__ty_2Enum_2Enum @ V20k1))@(inj__ty_2EordinalNotation_2Eosyntax @ V21t1)))@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V22e2))@(inj__ty_2Enum_2Enum @ V23k2))@(inj__ty_2EordinalNotation_2Eosyntax @ V24t2))))))))))))))) => ( ! [V25a0:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V26a1:tp__ty_2EordinalNotation_2Eosyntax] : ((p@(ap@(ap@c_2EordinalNotation_2Eoless@(inj__ty_2EordinalNotation_2Eosyntax @ V25a0))@(inj__ty_2EordinalNotation_2Eosyntax @ V26a1))) => (p@(ap@(ap@V0oless_27@(inj__ty_2EordinalNotation_2Eosyntax @ V25a0))@(inj__ty_2EordinalNotation_2Eosyntax @ V26a1)))))))))).
thf(conj_thm_2EordinalNotation_2Eoless__End__End,lemma,( ! [V0k1:tp__ty_2Enum_2Enum] : ( ! [V1k2:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2EordinalNotation_2Eoless@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V0k1)))@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V1k2)))) => (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0k1))@(inj__ty_2Enum_2Enum @ V1k2))))))).
thf(conj_thm_2EordinalNotation_2Eoless__equations,lemma,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2e:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V3k:tp__ty_2Enum_2Enum] : ( ! [V4t:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V5e1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V6k1:tp__ty_2Enum_2Enum] : ( ! [V7t1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V8e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V9k2:tp__ty_2Enum_2Enum] : ( ! [V10t2:tp__ty_2EordinalNotation_2Eosyntax] : (((p@(ap@(ap@c_2EordinalNotation_2Eoless@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V0m)))@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V1n)))) <=> (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V1n)))) & (((p@(ap@(ap@c_2EordinalNotation_2Eoless@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V0m)))@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V2e))@(inj__ty_2Enum_2Enum @ V3k))@(inj__ty_2EordinalNotation_2Eosyntax @ V4t)))) <=> $true) & (((p@(ap@(ap@c_2EordinalNotation_2Eoless@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V2e))@(inj__ty_2Enum_2Enum @ V3k))@(inj__ty_2EordinalNotation_2Eosyntax @ V4t)))@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V0m)))) <=> $false) & ((p@(ap@(ap@c_2EordinalNotation_2Eoless@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V5e1))@(inj__ty_2Enum_2Enum @ V6k1))@(inj__ty_2EordinalNotation_2Eosyntax @ V7t1)))@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V8e2))@(inj__ty_2Enum_2Enum @ V9k2))@(inj__ty_2EordinalNotation_2Eosyntax @ V10t2)))) <=> (p@(ap@(ap@(ap@(c_2Ebool_2ECOND@bool)@(ap@(ap@c_2EordinalNotation_2Eoless@(inj__ty_2EordinalNotation_2Eosyntax @ V5e1))@(inj__ty_2EordinalNotation_2Eosyntax @ V8e2)))@c_2Ebool_2ET)@(ap@(ap@(ap@(c_2Ebool_2ECOND@bool)@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Emin_2E_3D@ty_2EordinalNotation_2Eosyntax)@(inj__ty_2EordinalNotation_2Eosyntax @ V5e1))@(inj__ty_2EordinalNotation_2Eosyntax @ V8e2)))@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V6k1))@(inj__ty_2Enum_2Enum @ V9k2))))@c_2Ebool_2ET)@(ap@(ap@(ap@(c_2Ebool_2ECOND@bool)@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Emin_2E_3D@ty_2EordinalNotation_2Eosyntax)@(inj__ty_2EordinalNotation_2Eosyntax @ V5e1))@(inj__ty_2EordinalNotation_2Eosyntax @ V8e2)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V6k1))@(inj__ty_2Enum_2Enum @ V9k2)))@(ap@(ap@c_2EordinalNotation_2Eoless@(inj__ty_2EordinalNotation_2Eosyntax @ V7t1))@(inj__ty_2EordinalNotation_2Eosyntax @ V10t2)))))@c_2Ebool_2ET)@c_2Ebool_2EF)))))))))))))))))))).
thf(ax_thm_2EordinalNotation_2Eis__ord__def,axiom,(c_2EordinalNotation_2Eis__ord = (lam@ty_2EordinalNotation_2Eosyntax@(^ [V0a0:$i] : (ap@(c_2Ebool_2E_21@(arr@ty_2EordinalNotation_2Eosyntax@bool))@(lam@(arr@ty_2EordinalNotation_2Eosyntax@bool)@(^ [V1is__ord_27:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@(c_2Ebool_2E_21@ty_2EordinalNotation_2Eosyntax)@(lam@ty_2EordinalNotation_2Eosyntax@(^ [V2a0:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(c_2Ebool_2E_3F@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V3k:$i] : (ap@(ap@(c_2Emin_2E_3D@ty_2EordinalNotation_2Eosyntax)@V2a0)@(ap@c_2EordinalNotation_2EEnd@V3k))))))@(ap@(c_2Ebool_2E_3F@ty_2EordinalNotation_2Eosyntax)@(lam@ty_2EordinalNotation_2Eosyntax@(^ [V4e:$i] : (ap@(c_2Ebool_2E_3F@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V5k:$i] : (ap@(c_2Ebool_2E_3F@ty_2EordinalNotation_2Eosyntax)@(lam@ty_2EordinalNotation_2Eosyntax@(^ [V6t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Emin_2E_3D@ty_2EordinalNotation_2Eosyntax)@V2a0)@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@V4e)@V5k)@V6t)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@V1is__ord_27@V4e))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@(ap@(c_2Emin_2E_3D@ty_2EordinalNotation_2Eosyntax)@V4e)@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@V5k))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@V1is__ord_27@V6t))@(ap@(ap@c_2EordinalNotation_2Eoless@(ap@c_2EordinalNotation_2Eexpt@V6t))@V4e)))))))))))))))))@(ap@V1is__ord_27@V2a0))))))@(ap@V1is__ord_27@V0a0))))))))).
thf(conj_thm_2EordinalNotation_2Eis__ord__rules,lemma,(( ! [V0k:tp__ty_2Enum_2Enum] : (p@(ap@c_2EordinalNotation_2Eis__ord@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V0k))))) & ( ! [V1e:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V2k:tp__ty_2Enum_2Enum] : ( ! [V3t:tp__ty_2EordinalNotation_2Eosyntax] : (((p@(ap@c_2EordinalNotation_2Eis__ord@(inj__ty_2EordinalNotation_2Eosyntax @ V1e))) & ((~~ (V1e = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) & ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V2k))) & ((p@(ap@c_2EordinalNotation_2Eis__ord@(inj__ty_2EordinalNotation_2Eosyntax @ V3t))) & (p@(ap@(ap@c_2EordinalNotation_2Eoless@(ap@c_2EordinalNotation_2Eexpt@(inj__ty_2EordinalNotation_2Eosyntax @ V3t)))@(inj__ty_2EordinalNotation_2Eosyntax @ V1e))))))) => (p@(ap@c_2EordinalNotation_2Eis__ord@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V1e))@(inj__ty_2Enum_2Enum @ V2k))@(inj__ty_2EordinalNotation_2Eosyntax @ V3t)))))))))).
thf(conj_thm_2EordinalNotation_2Eis__ord__ind,lemma,( ! [V0is__ord_27:$i] : ((mem@V0is__ord_27@(arr@ty_2EordinalNotation_2Eosyntax@bool)) => ((( ! [V1k:tp__ty_2Enum_2Enum] : (p@(ap@V0is__ord_27@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V1k))))) & ( ! [V2e:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V3k:tp__ty_2Enum_2Enum] : ( ! [V4t:tp__ty_2EordinalNotation_2Eosyntax] : (((p@(ap@V0is__ord_27@(inj__ty_2EordinalNotation_2Eosyntax @ V2e))) & ((~~ (V2e = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) & ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V3k))) & ((p@(ap@V0is__ord_27@(inj__ty_2EordinalNotation_2Eosyntax @ V4t))) & (p@(ap@(ap@c_2EordinalNotation_2Eoless@(ap@c_2EordinalNotation_2Eexpt@(inj__ty_2EordinalNotation_2Eosyntax @ V4t)))@(inj__ty_2EordinalNotation_2Eosyntax @ V2e))))))) => (p@(ap@V0is__ord_27@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V2e))@(inj__ty_2Enum_2Enum @ V3k))@(inj__ty_2EordinalNotation_2Eosyntax @ V4t))))))))) => ( ! [V5a0:tp__ty_2EordinalNotation_2Eosyntax] : ((p@(ap@c_2EordinalNotation_2Eis__ord@(inj__ty_2EordinalNotation_2Eosyntax @ V5a0))) => (p@(ap@V0is__ord_27@(inj__ty_2EordinalNotation_2Eosyntax @ V5a0))))))))).
thf(conj_thm_2EordinalNotation_2Eis__ord__strongind,lemma,( ! [V0is__ord_27:$i] : ((mem@V0is__ord_27@(arr@ty_2EordinalNotation_2Eosyntax@bool)) => ((( ! [V1k:tp__ty_2Enum_2Enum] : (p@(ap@V0is__ord_27@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V1k))))) & ( ! [V2e:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V3k:tp__ty_2Enum_2Enum] : ( ! [V4t:tp__ty_2EordinalNotation_2Eosyntax] : (((p@(ap@c_2EordinalNotation_2Eis__ord@(inj__ty_2EordinalNotation_2Eosyntax @ V2e))) & ((p@(ap@V0is__ord_27@(inj__ty_2EordinalNotation_2Eosyntax @ V2e))) & ((~~ (V2e = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) & ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V3k))) & ((p@(ap@c_2EordinalNotation_2Eis__ord@(inj__ty_2EordinalNotation_2Eosyntax @ V4t))) & ((p@(ap@V0is__ord_27@(inj__ty_2EordinalNotation_2Eosyntax @ V4t))) & (p@(ap@(ap@c_2EordinalNotation_2Eoless@(ap@c_2EordinalNotation_2Eexpt@(inj__ty_2EordinalNotation_2Eosyntax @ V4t)))@(inj__ty_2EordinalNotation_2Eosyntax @ V2e))))))))) => (p@(ap@V0is__ord_27@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V2e))@(inj__ty_2Enum_2Enum @ V3k))@(inj__ty_2EordinalNotation_2Eosyntax @ V4t))))))))) => ( ! [V5a0:tp__ty_2EordinalNotation_2Eosyntax] : ((p@(ap@c_2EordinalNotation_2Eis__ord@(inj__ty_2EordinalNotation_2Eosyntax @ V5a0))) => (p@(ap@V0is__ord_27@(inj__ty_2EordinalNotation_2Eosyntax @ V5a0))))))))).
thf(conj_thm_2EordinalNotation_2Eis__ord__cases,lemma,( ! [V0a0:tp__ty_2EordinalNotation_2Eosyntax] : ((p@(ap@c_2EordinalNotation_2Eis__ord@(inj__ty_2EordinalNotation_2Eosyntax @ V0a0))) <=> ((? [V1k:tp__ty_2Enum_2Enum] : (V0a0 = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V1k))))) | (? [V2e:tp__ty_2EordinalNotation_2Eosyntax] : (? [V3k:tp__ty_2Enum_2Enum] : (? [V4t:tp__ty_2EordinalNotation_2Eosyntax] : ((V0a0 = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V2e))@(inj__ty_2Enum_2Enum @ V3k))@(inj__ty_2EordinalNotation_2Eosyntax @ V4t)))) & ((p@(ap@c_2EordinalNotation_2Eis__ord@(inj__ty_2EordinalNotation_2Eosyntax @ V2e))) & ((~~ (V2e = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) & ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V3k))) & ((p@(ap@c_2EordinalNotation_2Eis__ord@(inj__ty_2EordinalNotation_2Eosyntax @ V4t))) & (p@(ap@(ap@c_2EordinalNotation_2Eoless@(ap@c_2EordinalNotation_2Eexpt@(inj__ty_2EordinalNotation_2Eosyntax @ V4t)))@(inj__ty_2EordinalNotation_2Eosyntax @ V2e))))))))))))))).
thf(conj_thm_2EordinalNotation_2Eis__ord__strong__ind,lemma,( ! [V0is__ord_27:$i] : ((mem@V0is__ord_27@(arr@ty_2EordinalNotation_2Eosyntax@bool)) => ((( ! [V1k:tp__ty_2Enum_2Enum] : (p@(ap@V0is__ord_27@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V1k))))) & ( ! [V2e:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V3k:tp__ty_2Enum_2Enum] : ( ! [V4t:tp__ty_2EordinalNotation_2Eosyntax] : (((p@(ap@c_2EordinalNotation_2Eis__ord@(inj__ty_2EordinalNotation_2Eosyntax @ V2e))) & ((p@(ap@V0is__ord_27@(inj__ty_2EordinalNotation_2Eosyntax @ V2e))) & ((~~ (V2e = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) & ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V3k))) & ((p@(ap@c_2EordinalNotation_2Eis__ord@(inj__ty_2EordinalNotation_2Eosyntax @ V4t))) & ((p@(ap@V0is__ord_27@(inj__ty_2EordinalNotation_2Eosyntax @ V4t))) & (p@(ap@(ap@c_2EordinalNotation_2Eoless@(ap@c_2EordinalNotation_2Eexpt@(inj__ty_2EordinalNotation_2Eosyntax @ V4t)))@(inj__ty_2EordinalNotation_2Eosyntax @ V2e))))))))) => (p@(ap@V0is__ord_27@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V2e))@(inj__ty_2Enum_2Enum @ V3k))@(inj__ty_2EordinalNotation_2Eosyntax @ V4t))))))))) => ( ! [V5a0:tp__ty_2EordinalNotation_2Eosyntax] : ((p@(ap@c_2EordinalNotation_2Eis__ord@(inj__ty_2EordinalNotation_2Eosyntax @ V5a0))) => (p@(ap@V0is__ord_27@(inj__ty_2EordinalNotation_2Eosyntax @ V5a0))))))))).
thf(conj_thm_2EordinalNotation_2Edecompose__plus,lemma,( ! [V0e:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2t:tp__ty_2EordinalNotation_2Eosyntax] : ((p@(ap@c_2EordinalNotation_2Eis__ord@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V0e))@(inj__ty_2Enum_2Enum @ V1k))@(inj__ty_2EordinalNotation_2Eosyntax @ V2t)))) => ((p@(ap@c_2EordinalNotation_2Eis__ord@(inj__ty_2EordinalNotation_2Eosyntax @ V0e))) & ((~~ (V0e = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) & ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V1k))) & ((p@(ap@c_2EordinalNotation_2Eis__ord@(inj__ty_2EordinalNotation_2Eosyntax @ V2t))) & (p@(ap@(ap@c_2EordinalNotation_2Eoless@(ap@c_2EordinalNotation_2Eexpt@(inj__ty_2EordinalNotation_2Eosyntax @ V2t)))@(inj__ty_2EordinalNotation_2Eosyntax @ V0e)))))))))))).
thf(conj_thm_2EordinalNotation_2Eis__ord__equations,lemma,( ! [V0k:tp__ty_2Enum_2Enum] : ( ! [V1e:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V2t:tp__ty_2EordinalNotation_2Eosyntax] : (((p@(ap@c_2EordinalNotation_2Eis__ord@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V0k)))) <=> $true) & ((p@(ap@c_2EordinalNotation_2Eis__ord@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V1e))@(inj__ty_2Enum_2Enum @ V0k))@(inj__ty_2EordinalNotation_2Eosyntax @ V2t)))) <=> ((p@(ap@c_2EordinalNotation_2Eis__ord@(inj__ty_2EordinalNotation_2Eosyntax @ V1e))) & ((~~ (V1e = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) & ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V0k))) & ((p@(ap@c_2EordinalNotation_2Eis__ord@(inj__ty_2EordinalNotation_2Eosyntax @ V2t))) & (p@(ap@(ap@c_2EordinalNotation_2Eoless@(ap@c_2EordinalNotation_2Eexpt@(inj__ty_2EordinalNotation_2Eosyntax @ V2t)))@(inj__ty_2EordinalNotation_2Eosyntax @ V1e))))))))))))).
thf(conj_thm_2EordinalNotation_2Eis__ord__expt__closed,lemma,( ! [V0x:tp__ty_2EordinalNotation_2Eosyntax] : ((p@(ap@c_2EordinalNotation_2Eis__ord@(inj__ty_2EordinalNotation_2Eosyntax @ V0x))) => (p@(ap@c_2EordinalNotation_2Eis__ord@(ap@c_2EordinalNotation_2Eexpt@(inj__ty_2EordinalNotation_2Eosyntax @ V0x))))))).
thf(conj_thm_2EordinalNotation_2Eis__ord__tail__closed,lemma,( ! [V0x:tp__ty_2EordinalNotation_2Eosyntax] : (((~~ (p@(ap@c_2EordinalNotation_2Efinp@(inj__ty_2EordinalNotation_2Eosyntax @ V0x)))) & (p@(ap@c_2EordinalNotation_2Eis__ord@(inj__ty_2EordinalNotation_2Eosyntax @ V0x)))) => (p@(ap@c_2EordinalNotation_2Eis__ord@(ap@c_2EordinalNotation_2Etail@(inj__ty_2EordinalNotation_2Eosyntax @ V0x))))))).
thf(conj_thm_2EordinalNotation_2Eis__ord__downclosed,lemma,( ! [V0w:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2t:tp__ty_2EordinalNotation_2Eosyntax] : ((p@(ap@c_2EordinalNotation_2Eis__ord@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V0w))@(inj__ty_2Enum_2Enum @ V1k))@(inj__ty_2EordinalNotation_2Eosyntax @ V2t)))) => ((p@(ap@c_2EordinalNotation_2Eis__ord@(inj__ty_2EordinalNotation_2Eosyntax @ V0w))) & (p@(ap@c_2EordinalNotation_2Eis__ord@(inj__ty_2EordinalNotation_2Eosyntax @ V2t))))))))).
thf(conj_thm_2EordinalNotation_2Eis__ord__coeff__pos,lemma,( ! [V0x:tp__ty_2EordinalNotation_2Eosyntax] : (((~~ (p@(ap@c_2EordinalNotation_2Efinp@(inj__ty_2EordinalNotation_2Eosyntax @ V0x)))) & (p@(ap@c_2EordinalNotation_2Eis__ord@(inj__ty_2EordinalNotation_2Eosyntax @ V0x)))) => (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@c_2EordinalNotation_2Ecoeff@(inj__ty_2EordinalNotation_2Eosyntax @ V0x))))))).
thf(conj_thm_2EordinalNotation_2Erank__expt,lemma,( ! [V0x:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V1n:tp__ty_2Enum_2Enum] : (((p@(ap@c_2EordinalNotation_2Eis__ord@(inj__ty_2EordinalNotation_2Eosyntax @ V0x))) & ((surj__ty_2Enum_2Enum @ (ap@c_2EordinalNotation_2Erank@(inj__ty_2EordinalNotation_2Eosyntax @ V0x))) = (surj__ty_2Enum_2Enum @ (ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n))))) => ((surj__ty_2Enum_2Enum @ (ap@c_2EordinalNotation_2Erank@(ap@c_2EordinalNotation_2Eexpt@(inj__ty_2EordinalNotation_2Eosyntax @ V0x)))) = V1n))))).
thf(conj_thm_2EordinalNotation_2Eoless__antirefl,lemma,( ! [V0x:tp__ty_2EordinalNotation_2Eosyntax] : ((p@(ap@c_2EordinalNotation_2Eis__ord@(inj__ty_2EordinalNotation_2Eosyntax @ V0x))) => (~~ (p@(ap@(ap@c_2EordinalNotation_2Eoless@(inj__ty_2EordinalNotation_2Eosyntax @ V0x))@(inj__ty_2EordinalNotation_2Eosyntax @ V0x))))))).
thf(conj_thm_2EordinalNotation_2Eoless__antisym,lemma,( ! [V0x:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V1y:tp__ty_2EordinalNotation_2Eosyntax] : (((p@(ap@c_2EordinalNotation_2Eis__ord@(inj__ty_2EordinalNotation_2Eosyntax @ V0x))) & ((p@(ap@c_2EordinalNotation_2Eis__ord@(inj__ty_2EordinalNotation_2Eosyntax @ V1y))) & (p@(ap@(ap@c_2EordinalNotation_2Eoless@(inj__ty_2EordinalNotation_2Eosyntax @ V0x))@(inj__ty_2EordinalNotation_2Eosyntax @ V1y))))) => (~~ (p@(ap@(ap@c_2EordinalNotation_2Eoless@(inj__ty_2EordinalNotation_2Eosyntax @ V1y))@(inj__ty_2EordinalNotation_2Eosyntax @ V0x)))))))).
thf(conj_thm_2EordinalNotation_2Erank__less__imp__oless,lemma,( ! [V0x:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V1y:tp__ty_2EordinalNotation_2Eosyntax] : (((p@(ap@c_2EordinalNotation_2Eis__ord@(inj__ty_2EordinalNotation_2Eosyntax @ V0x))) & ((p@(ap@c_2EordinalNotation_2Eis__ord@(inj__ty_2EordinalNotation_2Eosyntax @ V1y))) & (p@(ap@(ap@c_2Eprim__rec_2E_3C@(ap@c_2EordinalNotation_2Erank@(inj__ty_2EordinalNotation_2Eosyntax @ V0x)))@(ap@c_2EordinalNotation_2Erank@(inj__ty_2EordinalNotation_2Eosyntax @ V1y)))))) => (p@(ap@(ap@c_2EordinalNotation_2Eoless@(inj__ty_2EordinalNotation_2Eosyntax @ V0x))@(inj__ty_2EordinalNotation_2Eosyntax @ V1y))))))).
thf(conj_thm_2EordinalNotation_2Eoless__imp__rank__leq,lemma,( ! [V0x:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V1y:tp__ty_2EordinalNotation_2Eosyntax] : (((p@(ap@c_2EordinalNotation_2Eis__ord@(inj__ty_2EordinalNotation_2Eosyntax @ V0x))) & ((p@(ap@c_2EordinalNotation_2Eis__ord@(inj__ty_2EordinalNotation_2Eosyntax @ V1y))) & (p@(ap@(ap@c_2EordinalNotation_2Eoless@(inj__ty_2EordinalNotation_2Eosyntax @ V0x))@(inj__ty_2EordinalNotation_2Eosyntax @ V1y))))) => (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@c_2EordinalNotation_2Erank@(inj__ty_2EordinalNotation_2Eosyntax @ V0x)))@(ap@c_2EordinalNotation_2Erank@(inj__ty_2EordinalNotation_2Eosyntax @ V1y)))))))).
thf(conj_thm_2EordinalNotation_2Erank__0__End,lemma,( ! [V0x:tp__ty_2EordinalNotation_2Eosyntax] : (((surj__ty_2Enum_2Enum @ (ap@c_2EordinalNotation_2Erank@(inj__ty_2EordinalNotation_2Eosyntax @ V0x))) = fo__c_2Enum_2E0) <=> (? [V1n:tp__ty_2Enum_2Enum] : (V0x = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V1n)))))))).
thf(conj_thm_2EordinalNotation_2Erank__finp,lemma,( ! [V0x:tp__ty_2EordinalNotation_2Eosyntax] : (((surj__ty_2Enum_2Enum @ (ap@c_2EordinalNotation_2Erank@(inj__ty_2EordinalNotation_2Eosyntax @ V0x))) = fo__c_2Enum_2E0) <=> (p@(ap@c_2EordinalNotation_2Efinp@(inj__ty_2EordinalNotation_2Eosyntax @ V0x)))))).
thf(conj_thm_2EordinalNotation_2Erank__positive__exists,lemma,( ! [V0x:tp__ty_2EordinalNotation_2Eosyntax] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@c_2EordinalNotation_2Erank@(inj__ty_2EordinalNotation_2Eosyntax @ V0x)))) <=> (? [V1e:tp__ty_2EordinalNotation_2Eosyntax] : (? [V2c:tp__ty_2Enum_2Enum] : (? [V3t:tp__ty_2EordinalNotation_2Eosyntax] : (V0x = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V1e))@(inj__ty_2Enum_2Enum @ V2c))@(inj__ty_2EordinalNotation_2Eosyntax @ V3t)))))))))).
thf(conj_thm_2EordinalNotation_2Erank__positive,lemma,( ! [V0x:tp__ty_2EordinalNotation_2Eosyntax] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@c_2EordinalNotation_2Erank@(inj__ty_2EordinalNotation_2Eosyntax @ V0x)))) <=> (V0x = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@(ap@c_2EordinalNotation_2EPlus@(ap@c_2EordinalNotation_2Eexpt@(inj__ty_2EordinalNotation_2Eosyntax @ V0x)))@(ap@c_2EordinalNotation_2Ecoeff@(inj__ty_2EordinalNotation_2Eosyntax @ V0x)))@(ap@c_2EordinalNotation_2Etail@(inj__ty_2EordinalNotation_2Eosyntax @ V0x)))))))).
thf(conj_thm_2EordinalNotation_2Erank__positive__expt,lemma,( ! [V0x:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V1n:tp__ty_2Enum_2Enum] : (((surj__ty_2Enum_2Enum @ (ap@c_2EordinalNotation_2Erank@(inj__ty_2EordinalNotation_2Eosyntax @ V0x))) = (surj__ty_2Enum_2Enum @ (ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n)))) => ((surj__ty_2Enum_2Enum @ (ap@c_2EordinalNotation_2Erank@(ap@c_2EordinalNotation_2Eexpt@(inj__ty_2EordinalNotation_2Eosyntax @ V0x)))) = V1n))))).
thf(conj_thm_2EordinalNotation_2Eoless__expt,lemma,( ! [V0e:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2t:tp__ty_2EordinalNotation_2Eosyntax] : ((p@(ap@c_2EordinalNotation_2Eis__ord@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V0e))@(inj__ty_2Enum_2Enum @ V1k))@(inj__ty_2EordinalNotation_2Eosyntax @ V2t)))) => (p@(ap@(ap@c_2EordinalNotation_2Eoless@(inj__ty_2EordinalNotation_2Eosyntax @ V0e))@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V0e))@(inj__ty_2Enum_2Enum @ V1k))@(inj__ty_2EordinalNotation_2Eosyntax @ V2t))))))))).
thf(conj_thm_2EordinalNotation_2Eoless__tail,lemma,( ! [V0x:tp__ty_2EordinalNotation_2Eosyntax] : (((p@(ap@c_2EordinalNotation_2Eis__ord@(inj__ty_2EordinalNotation_2Eosyntax @ V0x))) & (~~ (p@(ap@c_2EordinalNotation_2Efinp@(inj__ty_2EordinalNotation_2Eosyntax @ V0x))))) => (p@(ap@(ap@c_2EordinalNotation_2Eoless@(ap@c_2EordinalNotation_2Etail@(inj__ty_2EordinalNotation_2Eosyntax @ V0x)))@(inj__ty_2EordinalNotation_2Eosyntax @ V0x)))))).
thf(conj_thm_2EordinalNotation_2Elemma,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1P:$i] : ((mem@V1P@(arr@ty_2EordinalNotation_2Eosyntax@bool)) => ((? [V2x:tp__ty_2EordinalNotation_2Eosyntax] : ((p@(ap@c_2EordinalNotation_2Eis__ord@(inj__ty_2EordinalNotation_2Eosyntax @ V2x))) & ((p@(ap@V1P@(inj__ty_2EordinalNotation_2Eosyntax @ V2x))) & (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@c_2EordinalNotation_2Erank@(inj__ty_2EordinalNotation_2Eosyntax @ V2x)))@(inj__ty_2Enum_2Enum @ V0n)))))) => (? [V3m:tp__ty_2EordinalNotation_2Eosyntax] : ((p@(ap@c_2EordinalNotation_2Eis__ord@(inj__ty_2EordinalNotation_2Eosyntax @ V3m))) & ((p@(ap@V1P@(inj__ty_2EordinalNotation_2Eosyntax @ V3m))) & ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@c_2EordinalNotation_2Erank@(inj__ty_2EordinalNotation_2Eosyntax @ V3m)))@(inj__ty_2Enum_2Enum @ V0n))) & ( ! [V4y:tp__ty_2EordinalNotation_2Eosyntax] : (((p@(ap@c_2EordinalNotation_2Eis__ord@(inj__ty_2EordinalNotation_2Eosyntax @ V4y))) & ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@c_2EordinalNotation_2Erank@(inj__ty_2EordinalNotation_2Eosyntax @ V4y)))@(inj__ty_2Enum_2Enum @ V0n))) & (p@(ap@(ap@c_2EordinalNotation_2Eoless@(inj__ty_2EordinalNotation_2Eosyntax @ V4y))@(inj__ty_2EordinalNotation_2Eosyntax @ V3m))))) => (~~ (p@(ap@V1P@(inj__ty_2EordinalNotation_2Eosyntax @ V4y))))))))))))))).
thf(conj_thm_2EordinalNotation_2Emain__lemma,lemma,( ! [V0P:$i] : ((mem@V0P@(arr@ty_2EordinalNotation_2Eosyntax@bool)) => ((? [V1x:tp__ty_2EordinalNotation_2Eosyntax] : ((p@(ap@V0P@(inj__ty_2EordinalNotation_2Eosyntax @ V1x))) & (p@(ap@c_2EordinalNotation_2Eis__ord@(inj__ty_2EordinalNotation_2Eosyntax @ V1x))))) => (? [V2x:tp__ty_2EordinalNotation_2Eosyntax] : ((p@(ap@V0P@(inj__ty_2EordinalNotation_2Eosyntax @ V2x))) & ((p@(ap@c_2EordinalNotation_2Eis__ord@(inj__ty_2EordinalNotation_2Eosyntax @ V2x))) & ( ! [V3y:tp__ty_2EordinalNotation_2Eosyntax] : (((p@(ap@c_2EordinalNotation_2Eis__ord@(inj__ty_2EordinalNotation_2Eosyntax @ V3y))) & (p@(ap@(ap@c_2EordinalNotation_2Eoless@(inj__ty_2EordinalNotation_2Eosyntax @ V3y))@(inj__ty_2EordinalNotation_2Eosyntax @ V2x)))) => (~~ (p@(ap@V0P@(inj__ty_2EordinalNotation_2Eosyntax @ V3y))))))))))))).
thf(ax_thm_2EordinalNotation_2Eord__less__def,axiom,( ! [V0x:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V1y:tp__ty_2EordinalNotation_2Eosyntax] : ((p@(ap@(ap@c_2EordinalNotation_2Eord__less@(inj__ty_2EordinalNotation_2Eosyntax @ V0x))@(inj__ty_2EordinalNotation_2Eosyntax @ V1y))) <=> ((p@(ap@c_2EordinalNotation_2Eis__ord@(inj__ty_2EordinalNotation_2Eosyntax @ V0x))) & ((p@(ap@c_2EordinalNotation_2Eis__ord@(inj__ty_2EordinalNotation_2Eosyntax @ V1y))) & (p@(ap@(ap@c_2EordinalNotation_2Eoless@(inj__ty_2EordinalNotation_2Eosyntax @ V0x))@(inj__ty_2EordinalNotation_2Eosyntax @ V1y))))))))).
thf(conj_thm_2EordinalNotation_2EWF__ord__less,lemma,(p@(ap@(c_2Erelation_2EWF@ty_2EordinalNotation_2Eosyntax)@c_2EordinalNotation_2Eord__less))).
thf(conj_thm_2EordinalNotation_2Ee0__INDUCTION,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27a@ty_2EordinalNotation_2Eosyntax)) => (( ! [V2x:$i] : ((mem@V2x@A_27a) => (( ! [V3y:$i] : ((mem@V3y@A_27a) => ((p@(ap@(ap@c_2EordinalNotation_2Eord__less@(ap@V1f@V3y))@(ap@V1f@V2x))) => (p@(ap@V0P@V3y))))) => (p@(ap@V0P@V2x))))) => ( ! [V4x:$i] : ((mem@V4x@A_27a) => (p@(ap@V0P@V4x))))))))))).
thf(conj_thm_2EordinalNotation_2Ee0__RECURSION,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0M:$i] : ((mem@V0M@(arr@(arr@A_27a@A_27b)@(arr@A_27a@A_27b))) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27a@ty_2EordinalNotation_2Eosyntax)) => (p@(ap@(c_2Ebool_2E_3F_21@(arr@A_27a@A_27b))@(lam@(arr@A_27a@A_27b)@(^ [V2g:$i] : (ap@(c_2Ebool_2E_21@A_27a)@(lam@A_27a@(^ [V3x:$i] : (ap@(ap@(c_2Emin_2E_3D@A_27b)@(ap@V2g@V3x))@(ap@(ap@V0M@(ap@(ap@(ap@(c_2Erelation_2ERESTRICT@A_27a@A_27b)@V2g)@(lam@A_27a@(^ [V4x:$i] : (lam@A_27a@(^ [V5y:$i] : (ap@(ap@c_2EordinalNotation_2Eord__less@(ap@V1f@V4x))@(ap@V1f@V5y)))))))@V3x))@V3x)))))))))))))))).
thf(conj_thm_2EordinalNotation_2Eord__add__ind,lemma,( ! [V0P:$i] : ((mem@V0P@(arr@ty_2EordinalNotation_2Eosyntax@(arr@ty_2EordinalNotation_2Eosyntax@bool))) => ((( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@V0P@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V1m)))@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V2n)))))) & (( ! [V3m:tp__ty_2Enum_2Enum] : ( ! [V4p:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V5k:tp__ty_2Enum_2Enum] : ( ! [V6t:tp__ty_2EordinalNotation_2Eosyntax] : (p@(ap@(ap@V0P@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V3m)))@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V4p))@(inj__ty_2Enum_2Enum @ V5k))@(inj__ty_2EordinalNotation_2Eosyntax @ V6t)))))))) & (( ! [V7e:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V8k:tp__ty_2Enum_2Enum] : ( ! [V9t:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V10m:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@V0P@(inj__ty_2EordinalNotation_2Eosyntax @ V9t))@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V10m)))) => (p@(ap@(ap@V0P@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V7e))@(inj__ty_2Enum_2Enum @ V8k))@(inj__ty_2EordinalNotation_2Eosyntax @ V9t)))@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V10m))))))))) & ( ! [V11e1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V12k1:tp__ty_2Enum_2Enum] : ( ! [V13t1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V14e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V15k2:tp__ty_2Enum_2Enum] : ( ! [V16t2:tp__ty_2EordinalNotation_2Eosyntax] : ((((~~ (p@(ap@(ap@c_2EordinalNotation_2Eoless@(inj__ty_2EordinalNotation_2Eosyntax @ V11e1))@(inj__ty_2EordinalNotation_2Eosyntax @ V14e2)))) & (~~ (V11e1 = V14e2))) => (p@(ap@(ap@V0P@(inj__ty_2EordinalNotation_2Eosyntax @ V13t1))@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V14e2))@(inj__ty_2Enum_2Enum @ V15k2))@(inj__ty_2EordinalNotation_2Eosyntax @ V16t2))))) => (p@(ap@(ap@V0P@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V11e1))@(inj__ty_2Enum_2Enum @ V12k1))@(inj__ty_2EordinalNotation_2Eosyntax @ V13t1)))@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V14e2))@(inj__ty_2Enum_2Enum @ V15k2))@(inj__ty_2EordinalNotation_2Eosyntax @ V16t2)))))))))))))) => ( ! [V17v:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V18v1:tp__ty_2EordinalNotation_2Eosyntax] : (p@(ap@(ap@V0P@(inj__ty_2EordinalNotation_2Eosyntax @ V17v))@(inj__ty_2EordinalNotation_2Eosyntax @ V18v1))))))))).
thf(conj_thm_2EordinalNotation_2Eord__add__def,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ((surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@c_2EordinalNotation_2Eord__add@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V1m)))@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V0n)))) = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@c_2EordinalNotation_2EEnd@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V1m))@(inj__ty_2Enum_2Enum @ V0n))))))) & (( ! [V2t:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V3p:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V4m:tp__ty_2Enum_2Enum] : ( ! [V5k:tp__ty_2Enum_2Enum] : ((surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@c_2EordinalNotation_2Eord__add@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V4m)))@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V3p))@(inj__ty_2Enum_2Enum @ V5k))@(inj__ty_2EordinalNotation_2Eosyntax @ V2t)))) = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V3p))@(inj__ty_2Enum_2Enum @ V5k))@(inj__ty_2EordinalNotation_2Eosyntax @ V2t)))))))) & (( ! [V6t:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V7m:tp__ty_2Enum_2Enum] : ( ! [V8k:tp__ty_2Enum_2Enum] : ( ! [V9e:tp__ty_2EordinalNotation_2Eosyntax] : ((surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@c_2EordinalNotation_2Eord__add@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V9e))@(inj__ty_2Enum_2Enum @ V8k))@(inj__ty_2EordinalNotation_2Eosyntax @ V6t)))@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V7m)))) = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V9e))@(inj__ty_2Enum_2Enum @ V8k))@(ap@(ap@c_2EordinalNotation_2Eord__add@(inj__ty_2EordinalNotation_2Eosyntax @ V6t))@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V7m)))))))))) & ( ! [V10t2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V11t1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V12k2:tp__ty_2Enum_2Enum] : ( ! [V13k1:tp__ty_2Enum_2Enum] : ( ! [V14e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V15e1:tp__ty_2EordinalNotation_2Eosyntax] : ((surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@c_2EordinalNotation_2Eord__add@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V15e1))@(inj__ty_2Enum_2Enum @ V13k1))@(inj__ty_2EordinalNotation_2Eosyntax @ V11t1)))@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V14e2))@(inj__ty_2Enum_2Enum @ V12k2))@(inj__ty_2EordinalNotation_2Eosyntax @ V10t2)))) = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2EordinalNotation_2Eosyntax)@(ap@(ap@c_2EordinalNotation_2Eoless@(inj__ty_2EordinalNotation_2Eosyntax @ V15e1))@(inj__ty_2EordinalNotation_2Eosyntax @ V14e2)))@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V14e2))@(inj__ty_2Enum_2Enum @ V12k2))@(inj__ty_2EordinalNotation_2Eosyntax @ V10t2)))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2EordinalNotation_2Eosyntax)@(ap@(ap@(c_2Emin_2E_3D@ty_2EordinalNotation_2Eosyntax)@(inj__ty_2EordinalNotation_2Eosyntax @ V15e1))@(inj__ty_2EordinalNotation_2Eosyntax @ V14e2)))@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V14e2))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V13k1))@(inj__ty_2Enum_2Enum @ V12k2)))@(inj__ty_2EordinalNotation_2Eosyntax @ V10t2)))@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V15e1))@(inj__ty_2Enum_2Enum @ V13k1))@(ap@(ap@c_2EordinalNotation_2Eord__add@(inj__ty_2EordinalNotation_2Eosyntax @ V11t1))@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V14e2))@(inj__ty_2Enum_2Enum @ V12k2))@(inj__ty_2EordinalNotation_2Eosyntax @ V10t2)))))))))))))))))).
thf(conj_thm_2EordinalNotation_2Eord__sub__ind,lemma,( ! [V0P:$i] : ((mem@V0P@(arr@ty_2EordinalNotation_2Eosyntax@(arr@ty_2EordinalNotation_2Eosyntax@bool))) => ((( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@V0P@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V1m)))@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V2n)))))) & (( ! [V3m:tp__ty_2Enum_2Enum] : ( ! [V4p:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V5k:tp__ty_2Enum_2Enum] : ( ! [V6t:tp__ty_2EordinalNotation_2Eosyntax] : (p@(ap@(ap@V0P@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V3m)))@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V4p))@(inj__ty_2Enum_2Enum @ V5k))@(inj__ty_2EordinalNotation_2Eosyntax @ V6t)))))))) & (( ! [V7e:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V8k:tp__ty_2Enum_2Enum] : ( ! [V9t:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V10m:tp__ty_2Enum_2Enum] : (p@(ap@(ap@V0P@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V7e))@(inj__ty_2Enum_2Enum @ V8k))@(inj__ty_2EordinalNotation_2Eosyntax @ V9t)))@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V10m)))))))) & ( ! [V11e1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V12k1:tp__ty_2Enum_2Enum] : ( ! [V13t1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V14e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V15k2:tp__ty_2Enum_2Enum] : ( ! [V16t2:tp__ty_2EordinalNotation_2Eosyntax] : ((((~~ (p@(ap@(ap@c_2EordinalNotation_2Eoless@(inj__ty_2EordinalNotation_2Eosyntax @ V11e1))@(inj__ty_2EordinalNotation_2Eosyntax @ V14e2)))) & ((V11e1 = V14e2) & ((~~ (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V12k1))@(inj__ty_2Enum_2Enum @ V15k2)))) & (~~ (p@(ap@(ap@c_2Earithmetic_2E_3E@(inj__ty_2Enum_2Enum @ V12k1))@(inj__ty_2Enum_2Enum @ V15k2))))))) => (p@(ap@(ap@V0P@(inj__ty_2EordinalNotation_2Eosyntax @ V13t1))@(inj__ty_2EordinalNotation_2Eosyntax @ V16t2)))) => (p@(ap@(ap@V0P@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V11e1))@(inj__ty_2Enum_2Enum @ V12k1))@(inj__ty_2EordinalNotation_2Eosyntax @ V13t1)))@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V14e2))@(inj__ty_2Enum_2Enum @ V15k2))@(inj__ty_2EordinalNotation_2Eosyntax @ V16t2)))))))))))))) => ( ! [V17v:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V18v1:tp__ty_2EordinalNotation_2Eosyntax] : (p@(ap@(ap@V0P@(inj__ty_2EordinalNotation_2Eosyntax @ V17v))@(inj__ty_2EordinalNotation_2Eosyntax @ V18v1))))))))).
thf(conj_thm_2EordinalNotation_2Eord__sub__def,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ((surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@c_2EordinalNotation_2Eord__sub@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V1m)))@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V0n)))) = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@c_2EordinalNotation_2EEnd@(ap@(ap@c_2Earithmetic_2E_2D@(inj__ty_2Enum_2Enum @ V1m))@(inj__ty_2Enum_2Enum @ V0n))))))) & (( ! [V2t:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V3p:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V4m:tp__ty_2Enum_2Enum] : ( ! [V5k:tp__ty_2Enum_2Enum] : ((surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@c_2EordinalNotation_2Eord__sub@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V4m)))@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V3p))@(inj__ty_2Enum_2Enum @ V5k))@(inj__ty_2EordinalNotation_2Eosyntax @ V2t)))) = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))))) & (( ! [V6t:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V7m:tp__ty_2Enum_2Enum] : ( ! [V8k:tp__ty_2Enum_2Enum] : ( ! [V9e:tp__ty_2EordinalNotation_2Eosyntax] : ((surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@c_2EordinalNotation_2Eord__sub@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V9e))@(inj__ty_2Enum_2Enum @ V8k))@(inj__ty_2EordinalNotation_2Eosyntax @ V6t)))@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V7m)))) = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V9e))@(inj__ty_2Enum_2Enum @ V8k))@(inj__ty_2EordinalNotation_2Eosyntax @ V6t)))))))) & ( ! [V10t2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V11t1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V12k2:tp__ty_2Enum_2Enum] : ( ! [V13k1:tp__ty_2Enum_2Enum] : ( ! [V14e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V15e1:tp__ty_2EordinalNotation_2Eosyntax] : ((surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@c_2EordinalNotation_2Eord__sub@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V15e1))@(inj__ty_2Enum_2Enum @ V13k1))@(inj__ty_2EordinalNotation_2Eosyntax @ V11t1)))@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V14e2))@(inj__ty_2Enum_2Enum @ V12k2))@(inj__ty_2EordinalNotation_2Eosyntax @ V10t2)))) = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2EordinalNotation_2Eosyntax)@(ap@(ap@c_2EordinalNotation_2Eoless@(inj__ty_2EordinalNotation_2Eosyntax @ V15e1))@(inj__ty_2EordinalNotation_2Eosyntax @ V14e2)))@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2EordinalNotation_2Eosyntax)@(ap@(ap@(c_2Emin_2E_3D@ty_2EordinalNotation_2Eosyntax)@(inj__ty_2EordinalNotation_2Eosyntax @ V15e1))@(inj__ty_2EordinalNotation_2Eosyntax @ V14e2)))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2EordinalNotation_2Eosyntax)@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V13k1))@(inj__ty_2Enum_2Enum @ V12k2)))@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2EordinalNotation_2Eosyntax)@(ap@(ap@c_2Earithmetic_2E_3E@(inj__ty_2Enum_2Enum @ V13k1))@(inj__ty_2Enum_2Enum @ V12k2)))@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V15e1))@(ap@(ap@c_2Earithmetic_2E_2D@(inj__ty_2Enum_2Enum @ V13k1))@(inj__ty_2Enum_2Enum @ V12k2)))@(inj__ty_2EordinalNotation_2Eosyntax @ V11t1)))@(ap@(ap@c_2EordinalNotation_2Eord__sub@(inj__ty_2EordinalNotation_2Eosyntax @ V11t1))@(inj__ty_2EordinalNotation_2Eosyntax @ V10t2)))))@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V15e1))@(inj__ty_2Enum_2Enum @ V13k1))@(inj__ty_2EordinalNotation_2Eosyntax @ V11t1)))))))))))))))).
thf(stp_c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax,type,(tp__c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax : $tType)).
thf(stp_inj_c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax,type,(inj__c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax : (tp__c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax > $i))).
thf(stp_surj_c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax,type,(surj__c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax : ($i > tp__c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax))).
thf(stp_inj_surj_c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax,axiom,( ! [X:tp__c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax] : ((surj__c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax @ (inj__c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax @ X)) = X))).
thf(stp_inj_mem_c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax,axiom,( ! [X:tp__c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax] : (mem @ (inj__c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax @ X) @ (ty_2Epair_2Eprod@ty_2EordinalNotation_2Eosyntax@ty_2EordinalNotation_2Eosyntax)))).
thf(stp_iso_mem_c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Epair_2Eprod@ty_2EordinalNotation_2Eosyntax@ty_2EordinalNotation_2Eosyntax)) => (X = (inj__c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax @ (surj__c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax @ X)))))).
thf(conj_thm_2EordinalNotation_2Eord__mult__ind,lemma,( ! [V0P:$i] : ((mem@V0P@(arr@ty_2EordinalNotation_2Eosyntax@(arr@ty_2EordinalNotation_2Eosyntax@bool))) => (( ! [V1x:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V2y:tp__ty_2EordinalNotation_2Eosyntax] : ((( ! [V3v:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V4v1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V5m:tp__ty_2Enum_2Enum] : ( ! [V6e:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V7k:tp__ty_2Enum_2Enum] : ( ! [V8t:tp__ty_2EordinalNotation_2Eosyntax] : (((~~ ((V1x = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) | (V2y = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))) & (((surj__c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax @ (ap@(ap@(c_2Epair_2E_2C@ty_2EordinalNotation_2Eosyntax@ty_2EordinalNotation_2Eosyntax)@(inj__ty_2EordinalNotation_2Eosyntax @ V1x))@(inj__ty_2EordinalNotation_2Eosyntax @ V2y))) = (surj__c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax @ (ap@(ap@(c_2Epair_2E_2C@ty_2EordinalNotation_2Eosyntax@ty_2EordinalNotation_2Eosyntax)@(inj__ty_2EordinalNotation_2Eosyntax @ V3v))@(inj__ty_2EordinalNotation_2Eosyntax @ V4v1)))) & ((V3v = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V5m)))) & (V4v1 = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V6e))@(inj__ty_2Enum_2Enum @ V7k))@(inj__ty_2EordinalNotation_2Eosyntax @ V8t))))))) => (p@(ap@(ap@V0P@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ V5m)))@(inj__ty_2EordinalNotation_2Eosyntax @ V8t)))))))))) & ( ! [V9v:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V10v1:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V11e_27:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V12k_27:tp__ty_2Enum_2Enum] : ( ! [V13t_27:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V14e2:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V15k2:tp__ty_2Enum_2Enum] : ( ! [V16t2:tp__ty_2EordinalNotation_2Eosyntax] : (((~~ ((V1x = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) | (V2y = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))) & (((surj__c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax @ (ap@(ap@(c_2Epair_2E_2C@ty_2EordinalNotation_2Eosyntax@ty_2EordinalNotation_2Eosyntax)@(inj__ty_2EordinalNotation_2Eosyntax @ V1x))@(inj__ty_2EordinalNotation_2Eosyntax @ V2y))) = (surj__c_ty_2Epair_2Eprod_ty_2EordinalNotation_2Eosyntax_ty_2EordinalNotation_2Eosyntax @ (ap@(ap@(c_2Epair_2E_2C@ty_2EordinalNotation_2Eosyntax@ty_2EordinalNotation_2Eosyntax)@(inj__ty_2EordinalNotation_2Eosyntax @ V9v))@(inj__ty_2EordinalNotation_2Eosyntax @ V10v1)))) & ((V9v = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V11e_27))@(inj__ty_2Enum_2Enum @ V12k_27))@(inj__ty_2EordinalNotation_2Eosyntax @ V13t_27)))) & (V10v1 = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V14e2))@(inj__ty_2Enum_2Enum @ V15k2))@(inj__ty_2EordinalNotation_2Eosyntax @ V16t2))))))) => (p@(ap@(ap@V0P@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@(inj__ty_2EordinalNotation_2Eosyntax @ V11e_27))@(inj__ty_2Enum_2Enum @ V12k_27))@(inj__ty_2EordinalNotation_2Eosyntax @ V13t_27)))@(inj__ty_2EordinalNotation_2Eosyntax @ V16t2))))))))))))) => (p@(ap@(ap@V0P@(inj__ty_2EordinalNotation_2Eosyntax @ V1x))@(inj__ty_2EordinalNotation_2Eosyntax @ V2y)))))) => ( ! [V17v:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V18v1:tp__ty_2EordinalNotation_2Eosyntax] : (p@(ap@(ap@V0P@(inj__ty_2EordinalNotation_2Eosyntax @ V17v))@(inj__ty_2EordinalNotation_2Eosyntax @ V18v1))))))))).
thf(conj_thm_2EordinalNotation_2Eord__mult__def,lemma,( ! [V0y:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V1x:tp__ty_2EordinalNotation_2Eosyntax] : ((surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@c_2EordinalNotation_2Eord__mult@(inj__ty_2EordinalNotation_2Eosyntax @ V1x))@(inj__ty_2EordinalNotation_2Eosyntax @ V0y))) = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2EordinalNotation_2Eosyntax)@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@(c_2Emin_2E_3D@ty_2EordinalNotation_2Eosyntax)@(inj__ty_2EordinalNotation_2Eosyntax @ V1x))@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))@(ap@(ap@(c_2Emin_2E_3D@ty_2EordinalNotation_2Eosyntax)@(inj__ty_2EordinalNotation_2Eosyntax @ V0y))@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@(ap@(c_2Epair_2Epair__CASE@ty_2EordinalNotation_2Eosyntax@ty_2EordinalNotation_2Eosyntax@ty_2EordinalNotation_2Eosyntax)@(ap@(ap@(c_2Epair_2E_2C@ty_2EordinalNotation_2Eosyntax@ty_2EordinalNotation_2Eosyntax)@(inj__ty_2EordinalNotation_2Eosyntax @ V1x))@(inj__ty_2EordinalNotation_2Eosyntax @ V0y)))@(lam@ty_2EordinalNotation_2Eosyntax@(^ [V2v:$i] : (lam@ty_2EordinalNotation_2Eosyntax@(^ [V3v1:$i] : (ap@(ap@(ap@(c_2EordinalNotation_2Eosyntax__CASE@ty_2EordinalNotation_2Eosyntax)@V2v)@(lam@ty_2Enum_2Enum@(^ [V4m:$i] : (ap@(ap@(ap@(c_2EordinalNotation_2Eosyntax__CASE@ty_2EordinalNotation_2Eosyntax)@V3v1)@(lam@ty_2Enum_2Enum@(^ [V5n:$i] : (ap@c_2EordinalNotation_2EEnd@(ap@(ap@c_2Earithmetic_2E_2A@V4m)@V5n)))))@(lam@ty_2EordinalNotation_2Eosyntax@(^ [V6e:$i] : (lam@ty_2Enum_2Enum@(^ [V7k:$i] : (lam@ty_2EordinalNotation_2Eosyntax@(^ [V8t:$i] : (ap@(ap@(ap@c_2EordinalNotation_2EPlus@(ap@(ap@c_2EordinalNotation_2Eord__add@(ap@c_2EordinalNotation_2EEnd@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@V6e))@V7k)@(ap@(ap@c_2EordinalNotation_2Eord__mult@(ap@c_2EordinalNotation_2EEnd@V4m))@V8t))))))))))))@(lam@ty_2EordinalNotation_2Eosyntax@(^ [V9e_27:$i] : (lam@ty_2Enum_2Enum@(^ [V10k_27:$i] : (lam@ty_2EordinalNotation_2Eosyntax@(^ [V11t_27:$i] : (ap@(ap@(ap@(c_2EordinalNotation_2Eosyntax__CASE@ty_2EordinalNotation_2Eosyntax)@V3v1)@(lam@ty_2Enum_2Enum@(^ [V12n_27:$i] : (ap@(ap@(ap@c_2EordinalNotation_2EPlus@V9e_27)@(ap@(ap@c_2Earithmetic_2E_2A@V10k_27)@V12n_27))@V11t_27))))@(lam@ty_2EordinalNotation_2Eosyntax@(^ [V13e2:$i] : (lam@ty_2Enum_2Enum@(^ [V14k2:$i] : (lam@ty_2EordinalNotation_2Eosyntax@(^ [V15t2:$i] : (ap@(ap@(ap@c_2EordinalNotation_2EPlus@(ap@(ap@c_2EordinalNotation_2Eord__add@V9e_27)@V13e2))@V14k2)@(ap@(ap@c_2EordinalNotation_2Eord__mult@(ap@(ap@(ap@c_2EordinalNotation_2EPlus@V9e_27)@V10k_27)@V11t_27))@V15t2))))))))))))))))))))))))))).
thf(ax_thm_2EordinalNotation_2Erestn__def,axiom,(( ! [V0a:tp__ty_2EordinalNotation_2Eosyntax] : ((surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@c_2EordinalNotation_2Erestn@(inj__ty_2EordinalNotation_2Eosyntax @ V0a))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) = V0a)) & ( ! [V1a:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V2n:tp__ty_2Enum_2Enum] : ((surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@c_2EordinalNotation_2Erestn@(inj__ty_2EordinalNotation_2Eosyntax @ V1a))@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V2n)))) = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@c_2EordinalNotation_2Erestn@(ap@c_2EordinalNotation_2Etail@(inj__ty_2EordinalNotation_2Eosyntax @ V1a)))@(inj__ty_2Enum_2Enum @ V2n)))))))).
thf(conj_thm_2EordinalNotation_2Erestn__def__compute,conjecture,(( ! [V0a:tp__ty_2EordinalNotation_2Eosyntax] : ((surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@c_2EordinalNotation_2Erestn@(inj__ty_2EordinalNotation_2Eosyntax @ V0a))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) = V0a)) & (( ! [V1a:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V2n:tp__ty_2Enum_2Enum] : ((surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@c_2EordinalNotation_2Erestn@(inj__ty_2EordinalNotation_2Eosyntax @ V1a))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V2n))))) = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@c_2EordinalNotation_2Erestn@(ap@c_2EordinalNotation_2Etail@(inj__ty_2EordinalNotation_2Eosyntax @ V1a)))@(ap@(ap@c_2Earithmetic_2E_2D@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V2n))))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))) & ( ! [V3a:tp__ty_2EordinalNotation_2Eosyntax] : ( ! [V4n:tp__ty_2Enum_2Enum] : ((surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@c_2EordinalNotation_2Erestn@(inj__ty_2EordinalNotation_2Eosyntax @ V3a))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V4n))))) = (surj__ty_2EordinalNotation_2Eosyntax @ (ap@(ap@c_2EordinalNotation_2Erestn@(ap@c_2EordinalNotation_2Etail@(inj__ty_2EordinalNotation_2Eosyntax @ V3a)))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V4n))))))))))).
