include('Axioms/fmsp^2.ax').
thf(tp_ty_2EDeepSyntax_2Edeep__form,type,( ty_2EDeepSyntax_2Edeep__form:del )).
thf(stp_ty_2EDeepSyntax_2Edeep__form,type,(tp__ty_2EDeepSyntax_2Edeep__form : $tType)).
thf(stp_inj_ty_2EDeepSyntax_2Edeep__form,type,(inj__ty_2EDeepSyntax_2Edeep__form : (tp__ty_2EDeepSyntax_2Edeep__form > $i))).
thf(stp_surj_ty_2EDeepSyntax_2Edeep__form,type,(surj__ty_2EDeepSyntax_2Edeep__form : ($i > tp__ty_2EDeepSyntax_2Edeep__form))).
thf(stp_inj_surj_ty_2EDeepSyntax_2Edeep__form,axiom,( ! [X:tp__ty_2EDeepSyntax_2Edeep__form] : ((surj__ty_2EDeepSyntax_2Edeep__form @ (inj__ty_2EDeepSyntax_2Edeep__form @ X)) = X))).
thf(stp_inj_mem_ty_2EDeepSyntax_2Edeep__form,axiom,( ! [X:tp__ty_2EDeepSyntax_2Edeep__form] : (mem @ (inj__ty_2EDeepSyntax_2Edeep__form @ X) @ ty_2EDeepSyntax_2Edeep__form))).
thf(stp_iso_mem_ty_2EDeepSyntax_2Edeep__form,axiom,( ! [X:$i] : ((mem @ X @ ty_2EDeepSyntax_2Edeep__form) => (X = (inj__ty_2EDeepSyntax_2Edeep__form @ (surj__ty_2EDeepSyntax_2Edeep__form @ X)))))).
thf(tp_c_2EDeepSyntax_2EAset,type,(c_2EDeepSyntax_2EAset:$i)).
thf(mem_c_2EDeepSyntax_2EAset,axiom,(mem@c_2EDeepSyntax_2EAset@(arr@bool@(arr@ty_2EDeepSyntax_2Edeep__form@(arr@ty_2Einteger_2Eint@bool))))).
thf(tp_c_2EDeepSyntax_2EBset,type,(c_2EDeepSyntax_2EBset:$i)).
thf(mem_c_2EDeepSyntax_2EBset,axiom,(mem@c_2EDeepSyntax_2EBset@(arr@bool@(arr@ty_2EDeepSyntax_2Edeep__form@(arr@ty_2Einteger_2Eint@bool))))).
thf(tp_c_2EDeepSyntax_2EConjn,type,(c_2EDeepSyntax_2EConjn:$i)).
thf(mem_c_2EDeepSyntax_2EConjn,axiom,(mem@c_2EDeepSyntax_2EConjn@(arr@ty_2EDeepSyntax_2Edeep__form@(arr@ty_2EDeepSyntax_2Edeep__form@ty_2EDeepSyntax_2Edeep__form)))).
thf(stp_fo_c_2EDeepSyntax_2EConjn,type,(fo__c_2EDeepSyntax_2EConjn:(tp__ty_2EDeepSyntax_2Edeep__form > (tp__ty_2EDeepSyntax_2Edeep__form > tp__ty_2EDeepSyntax_2Edeep__form)))).
thf(stp_eq_fo_c_2EDeepSyntax_2EConjn,axiom,( ! [X0:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [X1:tp__ty_2EDeepSyntax_2Edeep__form] : ((inj__ty_2EDeepSyntax_2Edeep__form @ ((fo__c_2EDeepSyntax_2EConjn @ X0) @ X1)) = (ap @ (ap @ c_2EDeepSyntax_2EConjn @ (inj__ty_2EDeepSyntax_2Edeep__form @ X0)) @ (inj__ty_2EDeepSyntax_2Edeep__form @ X1)))))).
thf(tp_c_2EDeepSyntax_2EDisjn,type,(c_2EDeepSyntax_2EDisjn:$i)).
thf(mem_c_2EDeepSyntax_2EDisjn,axiom,(mem@c_2EDeepSyntax_2EDisjn@(arr@ty_2EDeepSyntax_2Edeep__form@(arr@ty_2EDeepSyntax_2Edeep__form@ty_2EDeepSyntax_2Edeep__form)))).
thf(stp_fo_c_2EDeepSyntax_2EDisjn,type,(fo__c_2EDeepSyntax_2EDisjn:(tp__ty_2EDeepSyntax_2Edeep__form > (tp__ty_2EDeepSyntax_2Edeep__form > tp__ty_2EDeepSyntax_2Edeep__form)))).
thf(stp_eq_fo_c_2EDeepSyntax_2EDisjn,axiom,( ! [X0:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [X1:tp__ty_2EDeepSyntax_2Edeep__form] : ((inj__ty_2EDeepSyntax_2Edeep__form @ ((fo__c_2EDeepSyntax_2EDisjn @ X0) @ X1)) = (ap @ (ap @ c_2EDeepSyntax_2EDisjn @ (inj__ty_2EDeepSyntax_2Edeep__form @ X0)) @ (inj__ty_2EDeepSyntax_2Edeep__form @ X1)))))).
thf(tp_c_2EDeepSyntax_2ELTx,type,(c_2EDeepSyntax_2ELTx:$i)).
thf(mem_c_2EDeepSyntax_2ELTx,axiom,(mem@c_2EDeepSyntax_2ELTx@(arr@ty_2Einteger_2Eint@ty_2EDeepSyntax_2Edeep__form))).
thf(stp_fo_c_2EDeepSyntax_2ELTx,type,(fo__c_2EDeepSyntax_2ELTx:(tp__ty_2Einteger_2Eint > tp__ty_2EDeepSyntax_2Edeep__form))).
thf(stp_eq_fo_c_2EDeepSyntax_2ELTx,axiom,( ! [X0:tp__ty_2Einteger_2Eint] : ((inj__ty_2EDeepSyntax_2Edeep__form @ (fo__c_2EDeepSyntax_2ELTx @ X0)) = (ap @ c_2EDeepSyntax_2ELTx @ (inj__ty_2Einteger_2Eint @ X0))))).
thf(tp_c_2EDeepSyntax_2ENegn,type,(c_2EDeepSyntax_2ENegn:$i)).
thf(mem_c_2EDeepSyntax_2ENegn,axiom,(mem@c_2EDeepSyntax_2ENegn@(arr@ty_2EDeepSyntax_2Edeep__form@ty_2EDeepSyntax_2Edeep__form))).
thf(stp_fo_c_2EDeepSyntax_2ENegn,type,(fo__c_2EDeepSyntax_2ENegn:(tp__ty_2EDeepSyntax_2Edeep__form > tp__ty_2EDeepSyntax_2Edeep__form))).
thf(stp_eq_fo_c_2EDeepSyntax_2ENegn,axiom,( ! [X0:tp__ty_2EDeepSyntax_2Edeep__form] : ((inj__ty_2EDeepSyntax_2Edeep__form @ (fo__c_2EDeepSyntax_2ENegn @ X0)) = (ap @ c_2EDeepSyntax_2ENegn @ (inj__ty_2EDeepSyntax_2Edeep__form @ X0))))).
thf(tp_c_2EDeepSyntax_2EUnrelatedBool,type,(c_2EDeepSyntax_2EUnrelatedBool:$i)).
thf(mem_c_2EDeepSyntax_2EUnrelatedBool,axiom,(mem@c_2EDeepSyntax_2EUnrelatedBool@(arr@bool@ty_2EDeepSyntax_2Edeep__form))).
thf(tp_c_2EDeepSyntax_2Ealldivide,type,(c_2EDeepSyntax_2Ealldivide:$i)).
thf(mem_c_2EDeepSyntax_2Ealldivide,axiom,(mem@c_2EDeepSyntax_2Ealldivide@(arr@ty_2EDeepSyntax_2Edeep__form@(arr@ty_2Einteger_2Eint@bool)))).
thf(tp_c_2EDeepSyntax_2Edeep__form__CASE,type,(c_2EDeepSyntax_2Edeep__form__CASE:(del>$i))).
thf(mem_c_2EDeepSyntax_2Edeep__form__CASE,axiom,( ! [A_27a:del] : (mem@(c_2EDeepSyntax_2Edeep__form__CASE@A_27a)@(arr@ty_2EDeepSyntax_2Edeep__form@(arr@(arr@ty_2EDeepSyntax_2Edeep__form@(arr@ty_2EDeepSyntax_2Edeep__form@A_27a))@(arr@(arr@ty_2EDeepSyntax_2Edeep__form@(arr@ty_2EDeepSyntax_2Edeep__form@A_27a))@(arr@(arr@ty_2EDeepSyntax_2Edeep__form@A_27a)@(arr@(arr@bool@A_27a)@(arr@(arr@ty_2Einteger_2Eint@A_27a)@(arr@(arr@ty_2Einteger_2Eint@A_27a)@(arr@(arr@ty_2Einteger_2Eint@A_27a)@(arr@(arr@ty_2Einteger_2Eint@(arr@ty_2Einteger_2Eint@A_27a))@A_27a)))))))))))).
thf(tp_c_2EDeepSyntax_2Edeep__form__size,type,(c_2EDeepSyntax_2Edeep__form__size:$i)).
thf(mem_c_2EDeepSyntax_2Edeep__form__size,axiom,(mem@c_2EDeepSyntax_2Edeep__form__size@(arr@ty_2EDeepSyntax_2Edeep__form@ty_2Enum_2Enum))).
thf(stp_fo_c_2EDeepSyntax_2Edeep__form__size,type,(fo__c_2EDeepSyntax_2Edeep__form__size:(tp__ty_2EDeepSyntax_2Edeep__form > tp__ty_2Enum_2Enum))).
thf(stp_eq_fo_c_2EDeepSyntax_2Edeep__form__size,axiom,( ! [X0:tp__ty_2EDeepSyntax_2Edeep__form] : ((inj__ty_2Enum_2Enum @ (fo__c_2EDeepSyntax_2Edeep__form__size @ X0)) = (ap @ c_2EDeepSyntax_2Edeep__form__size @ (inj__ty_2EDeepSyntax_2Edeep__form @ X0))))).
thf(tp_c_2EDeepSyntax_2Eeval__form,type,(c_2EDeepSyntax_2Eeval__form:$i)).
thf(mem_c_2EDeepSyntax_2Eeval__form,axiom,(mem@c_2EDeepSyntax_2Eeval__form@(arr@ty_2EDeepSyntax_2Edeep__form@(arr@ty_2Einteger_2Eint@bool)))).
thf(tp_c_2EDeepSyntax_2Eneginf,type,(c_2EDeepSyntax_2Eneginf:$i)).
thf(mem_c_2EDeepSyntax_2Eneginf,axiom,(mem@c_2EDeepSyntax_2Eneginf@(arr@ty_2EDeepSyntax_2Edeep__form@ty_2EDeepSyntax_2Edeep__form))).
thf(stp_fo_c_2EDeepSyntax_2Eneginf,type,(fo__c_2EDeepSyntax_2Eneginf:(tp__ty_2EDeepSyntax_2Edeep__form > tp__ty_2EDeepSyntax_2Edeep__form))).
thf(stp_eq_fo_c_2EDeepSyntax_2Eneginf,axiom,( ! [X0:tp__ty_2EDeepSyntax_2Edeep__form] : ((inj__ty_2EDeepSyntax_2Edeep__form @ (fo__c_2EDeepSyntax_2Eneginf @ X0)) = (ap @ c_2EDeepSyntax_2Eneginf @ (inj__ty_2EDeepSyntax_2Edeep__form @ X0))))).
thf(tp_c_2EDeepSyntax_2Eposinf,type,(c_2EDeepSyntax_2Eposinf:$i)).
thf(mem_c_2EDeepSyntax_2Eposinf,axiom,(mem@c_2EDeepSyntax_2Eposinf@(arr@ty_2EDeepSyntax_2Edeep__form@ty_2EDeepSyntax_2Edeep__form))).
thf(stp_fo_c_2EDeepSyntax_2Eposinf,type,(fo__c_2EDeepSyntax_2Eposinf:(tp__ty_2EDeepSyntax_2Edeep__form > tp__ty_2EDeepSyntax_2Edeep__form))).
thf(stp_eq_fo_c_2EDeepSyntax_2Eposinf,axiom,( ! [X0:tp__ty_2EDeepSyntax_2Edeep__form] : ((inj__ty_2EDeepSyntax_2Edeep__form @ (fo__c_2EDeepSyntax_2Eposinf @ X0)) = (ap @ c_2EDeepSyntax_2Eposinf @ (inj__ty_2EDeepSyntax_2Edeep__form @ X0))))).
thf(tp_c_2EDeepSyntax_2ExDivided,type,(c_2EDeepSyntax_2ExDivided:$i)).
thf(mem_c_2EDeepSyntax_2ExDivided,axiom,(mem@c_2EDeepSyntax_2ExDivided@(arr@ty_2Einteger_2Eint@(arr@ty_2Einteger_2Eint@ty_2EDeepSyntax_2Edeep__form)))).
thf(stp_fo_c_2EDeepSyntax_2ExDivided,type,(fo__c_2EDeepSyntax_2ExDivided:(tp__ty_2Einteger_2Eint > (tp__ty_2Einteger_2Eint > tp__ty_2EDeepSyntax_2Edeep__form)))).
thf(stp_eq_fo_c_2EDeepSyntax_2ExDivided,axiom,( ! [X0:tp__ty_2Einteger_2Eint] : ( ! [X1:tp__ty_2Einteger_2Eint] : ((inj__ty_2EDeepSyntax_2Edeep__form @ ((fo__c_2EDeepSyntax_2ExDivided @ X0) @ X1)) = (ap @ (ap @ c_2EDeepSyntax_2ExDivided @ (inj__ty_2Einteger_2Eint @ X0)) @ (inj__ty_2Einteger_2Eint @ X1)))))).
thf(tp_c_2EDeepSyntax_2ExEQ,type,(c_2EDeepSyntax_2ExEQ:$i)).
thf(mem_c_2EDeepSyntax_2ExEQ,axiom,(mem@c_2EDeepSyntax_2ExEQ@(arr@ty_2Einteger_2Eint@ty_2EDeepSyntax_2Edeep__form))).
thf(stp_fo_c_2EDeepSyntax_2ExEQ,type,(fo__c_2EDeepSyntax_2ExEQ:(tp__ty_2Einteger_2Eint > tp__ty_2EDeepSyntax_2Edeep__form))).
thf(stp_eq_fo_c_2EDeepSyntax_2ExEQ,axiom,( ! [X0:tp__ty_2Einteger_2Eint] : ((inj__ty_2EDeepSyntax_2Edeep__form @ (fo__c_2EDeepSyntax_2ExEQ @ X0)) = (ap @ c_2EDeepSyntax_2ExEQ @ (inj__ty_2Einteger_2Eint @ X0))))).
thf(tp_c_2EDeepSyntax_2ExLT,type,(c_2EDeepSyntax_2ExLT:$i)).
thf(mem_c_2EDeepSyntax_2ExLT,axiom,(mem@c_2EDeepSyntax_2ExLT@(arr@ty_2Einteger_2Eint@ty_2EDeepSyntax_2Edeep__form))).
thf(stp_fo_c_2EDeepSyntax_2ExLT,type,(fo__c_2EDeepSyntax_2ExLT:(tp__ty_2Einteger_2Eint > tp__ty_2EDeepSyntax_2Edeep__form))).
thf(stp_eq_fo_c_2EDeepSyntax_2ExLT,axiom,( ! [X0:tp__ty_2Einteger_2Eint] : ((inj__ty_2EDeepSyntax_2Edeep__form @ (fo__c_2EDeepSyntax_2ExLT @ X0)) = (ap @ c_2EDeepSyntax_2ExLT @ (inj__ty_2Einteger_2Eint @ X0))))).
thf(stp_c_ty_2Eind__type_2Erecspace_c_ty_2Epair_2Eprod_o_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint,type,(tp__c_ty_2Eind__type_2Erecspace_c_ty_2Epair_2Eprod_o_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint : $tType)).
thf(stp_inj_c_ty_2Eind__type_2Erecspace_c_ty_2Epair_2Eprod_o_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint,type,(inj__c_ty_2Eind__type_2Erecspace_c_ty_2Epair_2Eprod_o_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint : (tp__c_ty_2Eind__type_2Erecspace_c_ty_2Epair_2Eprod_o_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint > $i))).
thf(stp_surj_c_ty_2Eind__type_2Erecspace_c_ty_2Epair_2Eprod_o_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint,type,(surj__c_ty_2Eind__type_2Erecspace_c_ty_2Epair_2Eprod_o_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint : ($i > tp__c_ty_2Eind__type_2Erecspace_c_ty_2Epair_2Eprod_o_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint))).
thf(stp_inj_surj_c_ty_2Eind__type_2Erecspace_c_ty_2Epair_2Eprod_o_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint,axiom,( ! [X:tp__c_ty_2Eind__type_2Erecspace_c_ty_2Epair_2Eprod_o_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint] : ((surj__c_ty_2Eind__type_2Erecspace_c_ty_2Epair_2Eprod_o_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint @ (inj__c_ty_2Eind__type_2Erecspace_c_ty_2Epair_2Eprod_o_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint @ X)) = X))).
thf(stp_inj_mem_c_ty_2Eind__type_2Erecspace_c_ty_2Epair_2Eprod_o_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint,axiom,( ! [X:tp__c_ty_2Eind__type_2Erecspace_c_ty_2Epair_2Eprod_o_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint] : (mem @ (inj__c_ty_2Eind__type_2Erecspace_c_ty_2Epair_2Eprod_o_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint @ X) @ (ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint)))))).
thf(stp_iso_mem_c_ty_2Eind__type_2Erecspace_c_ty_2Epair_2Eprod_o_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint)))) => (X = (inj__c_ty_2Eind__type_2Erecspace_c_ty_2Epair_2Eprod_o_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint @ (surj__c_ty_2Eind__type_2Erecspace_c_ty_2Epair_2Eprod_o_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint @ X)))))).
thf(stp_c_ty_2Epair_2Eprod_o_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint,type,(tp__c_ty_2Epair_2Eprod_o_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint : $tType)).
thf(stp_inj_c_ty_2Epair_2Eprod_o_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint,type,(inj__c_ty_2Epair_2Eprod_o_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint : (tp__c_ty_2Epair_2Eprod_o_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint > $i))).
thf(stp_surj_c_ty_2Epair_2Eprod_o_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint,type,(surj__c_ty_2Epair_2Eprod_o_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint : ($i > tp__c_ty_2Epair_2Eprod_o_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint))).
thf(stp_inj_surj_c_ty_2Epair_2Eprod_o_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint,axiom,( ! [X:tp__c_ty_2Epair_2Eprod_o_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint] : ((surj__c_ty_2Epair_2Eprod_o_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint @ (inj__c_ty_2Epair_2Eprod_o_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint @ X)) = X))).
thf(stp_inj_mem_c_ty_2Epair_2Eprod_o_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint,axiom,( ! [X:tp__c_ty_2Epair_2Eprod_o_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint] : (mem @ (inj__c_ty_2Epair_2Eprod_o_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint @ X) @ (ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint))))).
thf(stp_iso_mem_c_ty_2Epair_2Eprod_o_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint))) => (X = (inj__c_ty_2Epair_2Eprod_o_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint @ (surj__c_ty_2Epair_2Eprod_o_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint @ X)))))).
thf(stp_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint,type,(tp__c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint : $tType)).
thf(stp_inj_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint,type,(inj__c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint : (tp__c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint > $i))).
thf(stp_surj_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint,type,(surj__c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint : ($i > tp__c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint))).
thf(stp_inj_surj_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint,axiom,( ! [X:tp__c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint] : ((surj__c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint @ (inj__c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint @ X)) = X))).
thf(stp_inj_mem_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint,axiom,( ! [X:tp__c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint] : (mem @ (inj__c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint @ X) @ (ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint)))).
thf(stp_iso_mem_c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint)) => (X = (inj__c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint @ (surj__c_ty_2Epair_2Eprod_ty_2Einteger_2Eint_ty_2Einteger_2Eint @ X)))))).
thf(ax_thm_2EDeepSyntax_2Edeep__form__TY__DEF,axiom,(? [V0rep:$i] : ((mem@V0rep@(arr@ty_2EDeepSyntax_2Edeep__form@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint))))) & (p@(ap@(ap@(c_2Ebool_2ETYPE__DEFINITION@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint)))@ty_2EDeepSyntax_2Edeep__form)@(lam@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint)))@(^ [V1a0_27:$i] : (ap@(c_2Ebool_2E_21@(arr@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint)))@bool))@(lam@(arr@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint)))@bool)@(^ [V2_27deep__form_27:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@(c_2Ebool_2E_21@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint))))@(lam@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint)))@(^ [V3a0_27:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(c_2Ebool_2E_3F@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint))))@(lam@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint)))@(^ [V4a0:$i] : (ap@(c_2Ebool_2E_3F@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint))))@(lam@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint)))@(^ [V5a1:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Emin_2E_3D@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint))))@V3a0_27)@(ap@(ap@(lam@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint)))@(^ [V6a0:$i] : (lam@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint)))@(^ [V7a1:$i] : (ap@(ap@(ap@(c_2Eind__type_2ECONSTR@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint)))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@(ap@(c_2Epair_2E_2C@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint))@(c_2Ebool_2EARB@bool))@(ap@(ap@(c_2Epair_2E_2C@ty_2Einteger_2Eint@ty_2Einteger_2Eint)@(c_2Ebool_2EARB@ty_2Einteger_2Eint))@(c_2Ebool_2EARB@ty_2Einteger_2Eint))))@(ap@(ap@(c_2Eind__type_2EFCONS@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint))))@V6a0)@(ap@(ap@(c_2Eind__type_2EFCONS@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint))))@V7a1)@(lam@ty_2Enum_2Enum@(^ [V8n:$i] : (c_2Eind__type_2EBOTTOM@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint))))))))))))@V4a0)@V5a1)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@V2_27deep__form_27@V4a0))@(ap@V2_27deep__form_27@V5a1))))))))))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(c_2Ebool_2E_3F@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint))))@(lam@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint)))@(^ [V9a0:$i] : (ap@(c_2Ebool_2E_3F@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint))))@(lam@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint)))@(^ [V10a1:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Emin_2E_3D@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint))))@V3a0_27)@(ap@(ap@(lam@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint)))@(^ [V11a0:$i] : (lam@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint)))@(^ [V12a1:$i] : (ap@(ap@(ap@(c_2Eind__type_2ECONSTR@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint)))@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@(ap@(c_2Epair_2E_2C@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint))@(c_2Ebool_2EARB@bool))@(ap@(ap@(c_2Epair_2E_2C@ty_2Einteger_2Eint@ty_2Einteger_2Eint)@(c_2Ebool_2EARB@ty_2Einteger_2Eint))@(c_2Ebool_2EARB@ty_2Einteger_2Eint))))@(ap@(ap@(c_2Eind__type_2EFCONS@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint))))@V11a0)@(ap@(ap@(c_2Eind__type_2EFCONS@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint))))@V12a1)@(lam@ty_2Enum_2Enum@(^ [V13n:$i] : (c_2Eind__type_2EBOTTOM@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint))))))))))))@V9a0)@V10a1)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@V2_27deep__form_27@V9a0))@(ap@V2_27deep__form_27@V10a1))))))))))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(c_2Ebool_2E_3F@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint))))@(lam@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint)))@(^ [V14a:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Emin_2E_3D@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint))))@V3a0_27)@(ap@(lam@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint)))@(^ [V15a:$i] : (ap@(ap@(ap@(c_2Eind__type_2ECONSTR@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint)))@(ap@c_2Enum_2ESUC@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))@(ap@(ap@(c_2Epair_2E_2C@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint))@(c_2Ebool_2EARB@bool))@(ap@(ap@(c_2Epair_2E_2C@ty_2Einteger_2Eint@ty_2Einteger_2Eint)@(c_2Ebool_2EARB@ty_2Einteger_2Eint))@(c_2Ebool_2EARB@ty_2Einteger_2Eint))))@(ap@(ap@(c_2Eind__type_2EFCONS@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint))))@V15a)@(lam@ty_2Enum_2Enum@(^ [V16n:$i] : (c_2Eind__type_2EBOTTOM@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint)))))))))@V14a)))@(ap@V2_27deep__form_27@V14a))))))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(c_2Ebool_2E_3F@bool)@(lam@bool@(^ [V17a:$i] : (ap@(ap@(c_2Emin_2E_3D@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint))))@V3a0_27)@(ap@(lam@bool@(^ [V18a:$i] : (ap@(ap@(ap@(c_2Eind__type_2ECONSTR@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint)))@(ap@c_2Enum_2ESUC@(ap@c_2Enum_2ESUC@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))@(ap@(ap@(c_2Epair_2E_2C@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint))@V18a)@(ap@(ap@(c_2Epair_2E_2C@ty_2Einteger_2Eint@ty_2Einteger_2Eint)@(c_2Ebool_2EARB@ty_2Einteger_2Eint))@(c_2Ebool_2EARB@ty_2Einteger_2Eint))))@(lam@ty_2Enum_2Enum@(^ [V19n:$i] : (c_2Eind__type_2EBOTTOM@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint))))))))@V17a))))))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(c_2Ebool_2E_3F@ty_2Einteger_2Eint)@(lam@ty_2Einteger_2Eint@(^ [V20a:$i] : (ap@(ap@(c_2Emin_2E_3D@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint))))@V3a0_27)@(ap@(lam@ty_2Einteger_2Eint@(^ [V21a:$i] : (ap@(ap@(ap@(c_2Eind__type_2ECONSTR@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint)))@(ap@c_2Enum_2ESUC@(ap@c_2Enum_2ESUC@(ap@c_2Enum_2ESUC@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))))@(ap@(ap@(c_2Epair_2E_2C@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint))@(c_2Ebool_2EARB@bool))@(ap@(ap@(c_2Epair_2E_2C@ty_2Einteger_2Eint@ty_2Einteger_2Eint)@V21a)@(c_2Ebool_2EARB@ty_2Einteger_2Eint))))@(lam@ty_2Enum_2Enum@(^ [V22n:$i] : (c_2Eind__type_2EBOTTOM@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint))))))))@V20a))))))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(c_2Ebool_2E_3F@ty_2Einteger_2Eint)@(lam@ty_2Einteger_2Eint@(^ [V23a:$i] : (ap@(ap@(c_2Emin_2E_3D@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint))))@V3a0_27)@(ap@(lam@ty_2Einteger_2Eint@(^ [V24a:$i] : (ap@(ap@(ap@(c_2Eind__type_2ECONSTR@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint)))@(ap@c_2Enum_2ESUC@(ap@c_2Enum_2ESUC@(ap@c_2Enum_2ESUC@(ap@c_2Enum_2ESUC@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))))@(ap@(ap@(c_2Epair_2E_2C@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint))@(c_2Ebool_2EARB@bool))@(ap@(ap@(c_2Epair_2E_2C@ty_2Einteger_2Eint@ty_2Einteger_2Eint)@V24a)@(c_2Ebool_2EARB@ty_2Einteger_2Eint))))@(lam@ty_2Enum_2Enum@(^ [V25n:$i] : (c_2Eind__type_2EBOTTOM@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint))))))))@V23a))))))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(c_2Ebool_2E_3F@ty_2Einteger_2Eint)@(lam@ty_2Einteger_2Eint@(^ [V26a:$i] : (ap@(ap@(c_2Emin_2E_3D@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint))))@V3a0_27)@(ap@(lam@ty_2Einteger_2Eint@(^ [V27a:$i] : (ap@(ap@(ap@(c_2Eind__type_2ECONSTR@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint)))@(ap@c_2Enum_2ESUC@(ap@c_2Enum_2ESUC@(ap@c_2Enum_2ESUC@(ap@c_2Enum_2ESUC@(ap@c_2Enum_2ESUC@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))))))@(ap@(ap@(c_2Epair_2E_2C@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint))@(c_2Ebool_2EARB@bool))@(ap@(ap@(c_2Epair_2E_2C@ty_2Einteger_2Eint@ty_2Einteger_2Eint)@V27a)@(c_2Ebool_2EARB@ty_2Einteger_2Eint))))@(lam@ty_2Enum_2Enum@(^ [V28n:$i] : (c_2Eind__type_2EBOTTOM@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint))))))))@V26a))))))@(ap@(c_2Ebool_2E_3F@ty_2Einteger_2Eint)@(lam@ty_2Einteger_2Eint@(^ [V29a0:$i] : (ap@(c_2Ebool_2E_3F@ty_2Einteger_2Eint)@(lam@ty_2Einteger_2Eint@(^ [V30a1:$i] : (ap@(ap@(c_2Emin_2E_3D@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint))))@V3a0_27)@(ap@(ap@(lam@ty_2Einteger_2Eint@(^ [V31a0:$i] : (lam@ty_2Einteger_2Eint@(^ [V32a1:$i] : (ap@(ap@(ap@(c_2Eind__type_2ECONSTR@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint)))@(ap@c_2Enum_2ESUC@(ap@c_2Enum_2ESUC@(ap@c_2Enum_2ESUC@(ap@c_2Enum_2ESUC@(ap@c_2Enum_2ESUC@(ap@c_2Enum_2ESUC@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))))))@(ap@(ap@(c_2Epair_2E_2C@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint))@(c_2Ebool_2EARB@bool))@(ap@(ap@(c_2Epair_2E_2C@ty_2Einteger_2Eint@ty_2Einteger_2Eint)@V31a0)@V32a1)))@(lam@ty_2Enum_2Enum@(^ [V33n:$i] : (c_2Eind__type_2EBOTTOM@(ty_2Epair_2Eprod@bool@(ty_2Epair_2Eprod@ty_2Einteger_2Eint@ty_2Einteger_2Eint))))))))))@V29a0)@V30a1))))))))))))))))@(ap@V2_27deep__form_27@V3a0_27))))))@(ap@V2_27deep__form_27@V1a0_27))))))))@V0rep))))).
thf(ax_thm_2EDeepSyntax_2Edeep__form__case__def,axiom,( ! [A_27a:del]: (( ! [V0a0:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V1a1:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V2f:$i] : ((mem@V2f@(arr@ty_2EDeepSyntax_2Edeep__form@(arr@ty_2EDeepSyntax_2Edeep__form@A_27a))) => ( ! [V3f1:$i] : ((mem@V3f1@(arr@ty_2EDeepSyntax_2Edeep__form@(arr@ty_2EDeepSyntax_2Edeep__form@A_27a))) => ( ! [V4f2:$i] : ((mem@V4f2@(arr@ty_2EDeepSyntax_2Edeep__form@A_27a)) => ( ! [V5f3:$i] : ((mem@V5f3@(arr@bool@A_27a)) => ( ! [V6f4:$i] : ((mem@V6f4@(arr@ty_2Einteger_2Eint@A_27a)) => ( ! [V7f5:$i] : ((mem@V7f5@(arr@ty_2Einteger_2Eint@A_27a)) => ( ! [V8f6:$i] : ((mem@V8f6@(arr@ty_2Einteger_2Eint@A_27a)) => ( ! [V9f7:$i] : ((mem@V9f7@(arr@ty_2Einteger_2Eint@(arr@ty_2Einteger_2Eint@A_27a))) => ((ap@(ap@(ap@(ap@(ap@(ap@(ap@(ap@(ap@(c_2EDeepSyntax_2Edeep__form__CASE@A_27a)@(ap@(ap@c_2EDeepSyntax_2EConjn@(inj__ty_2EDeepSyntax_2Edeep__form @ V0a0))@(inj__ty_2EDeepSyntax_2Edeep__form @ V1a1)))@V2f)@V3f1)@V4f2)@V5f3)@V6f4)@V7f5)@V8f6)@V9f7) = (ap@(ap@V2f@(inj__ty_2EDeepSyntax_2Edeep__form @ V0a0))@(inj__ty_2EDeepSyntax_2Edeep__form @ V1a1))))))))))))))))))))) & (( ! [V10a0:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V11a1:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V12f:$i] : ((mem@V12f@(arr@ty_2EDeepSyntax_2Edeep__form@(arr@ty_2EDeepSyntax_2Edeep__form@A_27a))) => ( ! [V13f1:$i] : ((mem@V13f1@(arr@ty_2EDeepSyntax_2Edeep__form@(arr@ty_2EDeepSyntax_2Edeep__form@A_27a))) => ( ! [V14f2:$i] : ((mem@V14f2@(arr@ty_2EDeepSyntax_2Edeep__form@A_27a)) => ( ! [V15f3:$i] : ((mem@V15f3@(arr@bool@A_27a)) => ( ! [V16f4:$i] : ((mem@V16f4@(arr@ty_2Einteger_2Eint@A_27a)) => ( ! [V17f5:$i] : ((mem@V17f5@(arr@ty_2Einteger_2Eint@A_27a)) => ( ! [V18f6:$i] : ((mem@V18f6@(arr@ty_2Einteger_2Eint@A_27a)) => ( ! [V19f7:$i] : ((mem@V19f7@(arr@ty_2Einteger_2Eint@(arr@ty_2Einteger_2Eint@A_27a))) => ((ap@(ap@(ap@(ap@(ap@(ap@(ap@(ap@(ap@(c_2EDeepSyntax_2Edeep__form__CASE@A_27a)@(ap@(ap@c_2EDeepSyntax_2EDisjn@(inj__ty_2EDeepSyntax_2Edeep__form @ V10a0))@(inj__ty_2EDeepSyntax_2Edeep__form @ V11a1)))@V12f)@V13f1)@V14f2)@V15f3)@V16f4)@V17f5)@V18f6)@V19f7) = (ap@(ap@V13f1@(inj__ty_2EDeepSyntax_2Edeep__form @ V10a0))@(inj__ty_2EDeepSyntax_2Edeep__form @ V11a1))))))))))))))))))))) & (( ! [V20a:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V21f:$i] : ((mem@V21f@(arr@ty_2EDeepSyntax_2Edeep__form@(arr@ty_2EDeepSyntax_2Edeep__form@A_27a))) => ( ! [V22f1:$i] : ((mem@V22f1@(arr@ty_2EDeepSyntax_2Edeep__form@(arr@ty_2EDeepSyntax_2Edeep__form@A_27a))) => ( ! [V23f2:$i] : ((mem@V23f2@(arr@ty_2EDeepSyntax_2Edeep__form@A_27a)) => ( ! [V24f3:$i] : ((mem@V24f3@(arr@bool@A_27a)) => ( ! [V25f4:$i] : ((mem@V25f4@(arr@ty_2Einteger_2Eint@A_27a)) => ( ! [V26f5:$i] : ((mem@V26f5@(arr@ty_2Einteger_2Eint@A_27a)) => ( ! [V27f6:$i] : ((mem@V27f6@(arr@ty_2Einteger_2Eint@A_27a)) => ( ! [V28f7:$i] : ((mem@V28f7@(arr@ty_2Einteger_2Eint@(arr@ty_2Einteger_2Eint@A_27a))) => ((ap@(ap@(ap@(ap@(ap@(ap@(ap@(ap@(ap@(c_2EDeepSyntax_2Edeep__form__CASE@A_27a)@(ap@c_2EDeepSyntax_2ENegn@(inj__ty_2EDeepSyntax_2Edeep__form @ V20a)))@V21f)@V22f1)@V23f2)@V24f3)@V25f4)@V26f5)@V27f6)@V28f7) = (ap@V23f2@(inj__ty_2EDeepSyntax_2Edeep__form @ V20a)))))))))))))))))))) & (( ! [V29a:$i] : ((mem@V29a@bool) => ( ! [V30f:$i] : ((mem@V30f@(arr@ty_2EDeepSyntax_2Edeep__form@(arr@ty_2EDeepSyntax_2Edeep__form@A_27a))) => ( ! [V31f1:$i] : ((mem@V31f1@(arr@ty_2EDeepSyntax_2Edeep__form@(arr@ty_2EDeepSyntax_2Edeep__form@A_27a))) => ( ! [V32f2:$i] : ((mem@V32f2@(arr@ty_2EDeepSyntax_2Edeep__form@A_27a)) => ( ! [V33f3:$i] : ((mem@V33f3@(arr@bool@A_27a)) => ( ! [V34f4:$i] : ((mem@V34f4@(arr@ty_2Einteger_2Eint@A_27a)) => ( ! [V35f5:$i] : ((mem@V35f5@(arr@ty_2Einteger_2Eint@A_27a)) => ( ! [V36f6:$i] : ((mem@V36f6@(arr@ty_2Einteger_2Eint@A_27a)) => ( ! [V37f7:$i] : ((mem@V37f7@(arr@ty_2Einteger_2Eint@(arr@ty_2Einteger_2Eint@A_27a))) => ((ap@(ap@(ap@(ap@(ap@(ap@(ap@(ap@(ap@(c_2EDeepSyntax_2Edeep__form__CASE@A_27a)@(ap@c_2EDeepSyntax_2EUnrelatedBool@V29a))@V30f)@V31f1)@V32f2)@V33f3)@V34f4)@V35f5)@V36f6)@V37f7) = (ap@V33f3@V29a)))))))))))))))))))) & (( ! [V38a:tp__ty_2Einteger_2Eint] : ( ! [V39f:$i] : ((mem@V39f@(arr@ty_2EDeepSyntax_2Edeep__form@(arr@ty_2EDeepSyntax_2Edeep__form@A_27a))) => ( ! [V40f1:$i] : ((mem@V40f1@(arr@ty_2EDeepSyntax_2Edeep__form@(arr@ty_2EDeepSyntax_2Edeep__form@A_27a))) => ( ! [V41f2:$i] : ((mem@V41f2@(arr@ty_2EDeepSyntax_2Edeep__form@A_27a)) => ( ! [V42f3:$i] : ((mem@V42f3@(arr@bool@A_27a)) => ( ! [V43f4:$i] : ((mem@V43f4@(arr@ty_2Einteger_2Eint@A_27a)) => ( ! [V44f5:$i] : ((mem@V44f5@(arr@ty_2Einteger_2Eint@A_27a)) => ( ! [V45f6:$i] : ((mem@V45f6@(arr@ty_2Einteger_2Eint@A_27a)) => ( ! [V46f7:$i] : ((mem@V46f7@(arr@ty_2Einteger_2Eint@(arr@ty_2Einteger_2Eint@A_27a))) => ((ap@(ap@(ap@(ap@(ap@(ap@(ap@(ap@(ap@(c_2EDeepSyntax_2Edeep__form__CASE@A_27a)@(ap@c_2EDeepSyntax_2ExLT@(inj__ty_2Einteger_2Eint @ V38a)))@V39f)@V40f1)@V41f2)@V42f3)@V43f4)@V44f5)@V45f6)@V46f7) = (ap@V43f4@(inj__ty_2Einteger_2Eint @ V38a)))))))))))))))))))) & (( ! [V47a:tp__ty_2Einteger_2Eint] : ( ! [V48f:$i] : ((mem@V48f@(arr@ty_2EDeepSyntax_2Edeep__form@(arr@ty_2EDeepSyntax_2Edeep__form@A_27a))) => ( ! [V49f1:$i] : ((mem@V49f1@(arr@ty_2EDeepSyntax_2Edeep__form@(arr@ty_2EDeepSyntax_2Edeep__form@A_27a))) => ( ! [V50f2:$i] : ((mem@V50f2@(arr@ty_2EDeepSyntax_2Edeep__form@A_27a)) => ( ! [V51f3:$i] : ((mem@V51f3@(arr@bool@A_27a)) => ( ! [V52f4:$i] : ((mem@V52f4@(arr@ty_2Einteger_2Eint@A_27a)) => ( ! [V53f5:$i] : ((mem@V53f5@(arr@ty_2Einteger_2Eint@A_27a)) => ( ! [V54f6:$i] : ((mem@V54f6@(arr@ty_2Einteger_2Eint@A_27a)) => ( ! [V55f7:$i] : ((mem@V55f7@(arr@ty_2Einteger_2Eint@(arr@ty_2Einteger_2Eint@A_27a))) => ((ap@(ap@(ap@(ap@(ap@(ap@(ap@(ap@(ap@(c_2EDeepSyntax_2Edeep__form__CASE@A_27a)@(ap@c_2EDeepSyntax_2ELTx@(inj__ty_2Einteger_2Eint @ V47a)))@V48f)@V49f1)@V50f2)@V51f3)@V52f4)@V53f5)@V54f6)@V55f7) = (ap@V53f5@(inj__ty_2Einteger_2Eint @ V47a)))))))))))))))))))) & (( ! [V56a:tp__ty_2Einteger_2Eint] : ( ! [V57f:$i] : ((mem@V57f@(arr@ty_2EDeepSyntax_2Edeep__form@(arr@ty_2EDeepSyntax_2Edeep__form@A_27a))) => ( ! [V58f1:$i] : ((mem@V58f1@(arr@ty_2EDeepSyntax_2Edeep__form@(arr@ty_2EDeepSyntax_2Edeep__form@A_27a))) => ( ! [V59f2:$i] : ((mem@V59f2@(arr@ty_2EDeepSyntax_2Edeep__form@A_27a)) => ( ! [V60f3:$i] : ((mem@V60f3@(arr@bool@A_27a)) => ( ! [V61f4:$i] : ((mem@V61f4@(arr@ty_2Einteger_2Eint@A_27a)) => ( ! [V62f5:$i] : ((mem@V62f5@(arr@ty_2Einteger_2Eint@A_27a)) => ( ! [V63f6:$i] : ((mem@V63f6@(arr@ty_2Einteger_2Eint@A_27a)) => ( ! [V64f7:$i] : ((mem@V64f7@(arr@ty_2Einteger_2Eint@(arr@ty_2Einteger_2Eint@A_27a))) => ((ap@(ap@(ap@(ap@(ap@(ap@(ap@(ap@(ap@(c_2EDeepSyntax_2Edeep__form__CASE@A_27a)@(ap@c_2EDeepSyntax_2ExEQ@(inj__ty_2Einteger_2Eint @ V56a)))@V57f)@V58f1)@V59f2)@V60f3)@V61f4)@V62f5)@V63f6)@V64f7) = (ap@V63f6@(inj__ty_2Einteger_2Eint @ V56a)))))))))))))))))))) & ( ! [V65a0:tp__ty_2Einteger_2Eint] : ( ! [V66a1:tp__ty_2Einteger_2Eint] : ( ! [V67f:$i] : ((mem@V67f@(arr@ty_2EDeepSyntax_2Edeep__form@(arr@ty_2EDeepSyntax_2Edeep__form@A_27a))) => ( ! [V68f1:$i] : ((mem@V68f1@(arr@ty_2EDeepSyntax_2Edeep__form@(arr@ty_2EDeepSyntax_2Edeep__form@A_27a))) => ( ! [V69f2:$i] : ((mem@V69f2@(arr@ty_2EDeepSyntax_2Edeep__form@A_27a)) => ( ! [V70f3:$i] : ((mem@V70f3@(arr@bool@A_27a)) => ( ! [V71f4:$i] : ((mem@V71f4@(arr@ty_2Einteger_2Eint@A_27a)) => ( ! [V72f5:$i] : ((mem@V72f5@(arr@ty_2Einteger_2Eint@A_27a)) => ( ! [V73f6:$i] : ((mem@V73f6@(arr@ty_2Einteger_2Eint@A_27a)) => ( ! [V74f7:$i] : ((mem@V74f7@(arr@ty_2Einteger_2Eint@(arr@ty_2Einteger_2Eint@A_27a))) => ((ap@(ap@(ap@(ap@(ap@(ap@(ap@(ap@(ap@(c_2EDeepSyntax_2Edeep__form__CASE@A_27a)@(ap@(ap@c_2EDeepSyntax_2ExDivided@(inj__ty_2Einteger_2Eint @ V65a0))@(inj__ty_2Einteger_2Eint @ V66a1)))@V67f)@V68f1)@V69f2)@V70f3)@V71f4)@V72f5)@V73f6)@V74f7) = (ap@(ap@V74f7@(inj__ty_2Einteger_2Eint @ V65a0))@(inj__ty_2Einteger_2Eint @ V66a1)))))))))))))))))))))))))))))).
thf(ax_thm_2EDeepSyntax_2Edeep__form__size__def,axiom,(( ! [V0a0:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V1a1:tp__ty_2EDeepSyntax_2Edeep__form] : ((surj__ty_2Enum_2Enum @ (ap@c_2EDeepSyntax_2Edeep__form__size@(ap@(ap@c_2EDeepSyntax_2EConjn@(inj__ty_2EDeepSyntax_2Edeep__form @ V0a0))@(inj__ty_2EDeepSyntax_2Edeep__form @ V1a1)))) = (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_2EDeepSyntax_2Edeep__form__size@(inj__ty_2EDeepSyntax_2Edeep__form @ V0a0)))@(ap@c_2EDeepSyntax_2Edeep__form__size@(inj__ty_2EDeepSyntax_2Edeep__form @ V1a1)))))))) & (( ! [V2a0:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V3a1:tp__ty_2EDeepSyntax_2Edeep__form] : ((surj__ty_2Enum_2Enum @ (ap@c_2EDeepSyntax_2Edeep__form__size@(ap@(ap@c_2EDeepSyntax_2EDisjn@(inj__ty_2EDeepSyntax_2Edeep__form @ V2a0))@(inj__ty_2EDeepSyntax_2Edeep__form @ V3a1)))) = (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_2EDeepSyntax_2Edeep__form__size@(inj__ty_2EDeepSyntax_2Edeep__form @ V2a0)))@(ap@c_2EDeepSyntax_2Edeep__form__size@(inj__ty_2EDeepSyntax_2Edeep__form @ V3a1)))))))) & (( ! [V4a:tp__ty_2EDeepSyntax_2Edeep__form] : ((surj__ty_2Enum_2Enum @ (ap@c_2EDeepSyntax_2Edeep__form__size@(ap@c_2EDeepSyntax_2ENegn@(inj__ty_2EDeepSyntax_2Edeep__form @ V4a)))) = (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_2EDeepSyntax_2Edeep__form__size@(inj__ty_2EDeepSyntax_2Edeep__form @ V4a)))))) & (( ! [V5a:$i] : ((mem@V5a@bool) => ((surj__ty_2Enum_2Enum @ (ap@c_2EDeepSyntax_2Edeep__form__size@(ap@c_2EDeepSyntax_2EUnrelatedBool@V5a))) = (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_2EbasicSize_2Ebool__size@V5a)))))) & (( ! [V6a:tp__ty_2Einteger_2Eint] : ((surj__ty_2Enum_2Enum @ (ap@c_2EDeepSyntax_2Edeep__form__size@(ap@c_2EDeepSyntax_2ExLT@(inj__ty_2Einteger_2Eint @ V6a)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) & (( ! [V7a:tp__ty_2Einteger_2Eint] : ((surj__ty_2Enum_2Enum @ (ap@c_2EDeepSyntax_2Edeep__form__size@(ap@c_2EDeepSyntax_2ELTx@(inj__ty_2Einteger_2Eint @ V7a)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) & (( ! [V8a:tp__ty_2Einteger_2Eint] : ((surj__ty_2Enum_2Enum @ (ap@c_2EDeepSyntax_2Edeep__form__size@(ap@c_2EDeepSyntax_2ExEQ@(inj__ty_2Einteger_2Eint @ V8a)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) & ( ! [V9a0:tp__ty_2Einteger_2Eint] : ( ! [V10a1:tp__ty_2Einteger_2Eint] : ((surj__ty_2Enum_2Enum @ (ap@c_2EDeepSyntax_2Edeep__form__size@(ap@(ap@c_2EDeepSyntax_2ExDivided@(inj__ty_2Einteger_2Eint @ V9a0))@(inj__ty_2Einteger_2Eint @ V10a1)))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))))))).
thf(conj_thm_2EDeepSyntax_2Edatatype__deep__form,lemma,( ! [V0deep__form:$i] : ((mem@V0deep__form@(arr@(arr@ty_2EDeepSyntax_2Edeep__form@(arr@ty_2EDeepSyntax_2Edeep__form@ty_2EDeepSyntax_2Edeep__form))@(arr@(arr@ty_2EDeepSyntax_2Edeep__form@(arr@ty_2EDeepSyntax_2Edeep__form@ty_2EDeepSyntax_2Edeep__form))@(arr@(arr@ty_2EDeepSyntax_2Edeep__form@ty_2EDeepSyntax_2Edeep__form)@(arr@(arr@bool@ty_2EDeepSyntax_2Edeep__form)@(arr@(arr@ty_2Einteger_2Eint@ty_2EDeepSyntax_2Edeep__form)@(arr@(arr@ty_2Einteger_2Eint@ty_2EDeepSyntax_2Edeep__form)@(arr@(arr@ty_2Einteger_2Eint@ty_2EDeepSyntax_2Edeep__form)@(arr@(arr@ty_2Einteger_2Eint@(arr@ty_2Einteger_2Eint@ty_2EDeepSyntax_2Edeep__form))@bool))))))))) => (p@(ap@(c_2Ebool_2EDATATYPE@bool)@(ap@(ap@(ap@(ap@(ap@(ap@(ap@(ap@V0deep__form@c_2EDeepSyntax_2EConjn)@c_2EDeepSyntax_2EDisjn)@c_2EDeepSyntax_2ENegn)@c_2EDeepSyntax_2EUnrelatedBool)@c_2EDeepSyntax_2ExLT)@c_2EDeepSyntax_2ELTx)@c_2EDeepSyntax_2ExEQ)@c_2EDeepSyntax_2ExDivided)))))).
thf(conj_thm_2EDeepSyntax_2Edeep__form__11,lemma,(( ! [V0a0:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V1a1:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V2a0_27:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V3a1_27:tp__ty_2EDeepSyntax_2Edeep__form] : (((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2EConjn@(inj__ty_2EDeepSyntax_2Edeep__form @ V0a0))@(inj__ty_2EDeepSyntax_2Edeep__form @ V1a1))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2EConjn@(inj__ty_2EDeepSyntax_2Edeep__form @ V2a0_27))@(inj__ty_2EDeepSyntax_2Edeep__form @ V3a1_27)))) <=> ((V0a0 = V2a0_27) & (V1a1 = V3a1_27))))))) & (( ! [V4a0:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V5a1:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V6a0_27:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V7a1_27:tp__ty_2EDeepSyntax_2Edeep__form] : (((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2EDisjn@(inj__ty_2EDeepSyntax_2Edeep__form @ V4a0))@(inj__ty_2EDeepSyntax_2Edeep__form @ V5a1))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2EDisjn@(inj__ty_2EDeepSyntax_2Edeep__form @ V6a0_27))@(inj__ty_2EDeepSyntax_2Edeep__form @ V7a1_27)))) <=> ((V4a0 = V6a0_27) & (V5a1 = V7a1_27))))))) & (( ! [V8a:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V9a_27:tp__ty_2EDeepSyntax_2Edeep__form] : (((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ENegn@(inj__ty_2EDeepSyntax_2Edeep__form @ V8a))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ENegn@(inj__ty_2EDeepSyntax_2Edeep__form @ V9a_27)))) <=> (V8a = V9a_27)))) & (( ! [V10a:$i] : ((mem@V10a@bool) => ( ! [V11a_27:$i] : ((mem@V11a_27@bool) => (((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2EUnrelatedBool@V10a)) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2EUnrelatedBool@V11a_27))) <=> ((p@V10a) <=> (p@V11a_27))))))) & (( ! [V12a:tp__ty_2Einteger_2Eint] : ( ! [V13a_27:tp__ty_2Einteger_2Eint] : (((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ExLT@(inj__ty_2Einteger_2Eint @ V12a))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ExLT@(inj__ty_2Einteger_2Eint @ V13a_27)))) <=> (V12a = V13a_27)))) & (( ! [V14a:tp__ty_2Einteger_2Eint] : ( ! [V15a_27:tp__ty_2Einteger_2Eint] : (((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ELTx@(inj__ty_2Einteger_2Eint @ V14a))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ELTx@(inj__ty_2Einteger_2Eint @ V15a_27)))) <=> (V14a = V15a_27)))) & (( ! [V16a:tp__ty_2Einteger_2Eint] : ( ! [V17a_27:tp__ty_2Einteger_2Eint] : (((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ExEQ@(inj__ty_2Einteger_2Eint @ V16a))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ExEQ@(inj__ty_2Einteger_2Eint @ V17a_27)))) <=> (V16a = V17a_27)))) & ( ! [V18a0:tp__ty_2Einteger_2Eint] : ( ! [V19a1:tp__ty_2Einteger_2Eint] : ( ! [V20a0_27:tp__ty_2Einteger_2Eint] : ( ! [V21a1_27:tp__ty_2Einteger_2Eint] : (((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2ExDivided@(inj__ty_2Einteger_2Eint @ V18a0))@(inj__ty_2Einteger_2Eint @ V19a1))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2ExDivided@(inj__ty_2Einteger_2Eint @ V20a0_27))@(inj__ty_2Einteger_2Eint @ V21a1_27)))) <=> ((V18a0 = V20a0_27) & (V19a1 = V21a1_27))))))))))))))).
thf(conj_thm_2EDeepSyntax_2Edeep__form__distinct,lemma,(( ! [V0a1_27:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V1a1:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V2a0_27:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V3a0:tp__ty_2EDeepSyntax_2Edeep__form] : (~~ ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2EConjn@(inj__ty_2EDeepSyntax_2Edeep__form @ V3a0))@(inj__ty_2EDeepSyntax_2Edeep__form @ V1a1))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2EDisjn@(inj__ty_2EDeepSyntax_2Edeep__form @ V2a0_27))@(inj__ty_2EDeepSyntax_2Edeep__form @ V0a1_27))))))))) & (( ! [V4a1:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V5a0:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V6a:tp__ty_2EDeepSyntax_2Edeep__form] : (~~ ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2EConjn@(inj__ty_2EDeepSyntax_2Edeep__form @ V5a0))@(inj__ty_2EDeepSyntax_2Edeep__form @ V4a1))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ENegn@(inj__ty_2EDeepSyntax_2Edeep__form @ V6a)))))))) & (( ! [V7a1:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V8a0:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V9a:$i] : ((mem@V9a@bool) => (~~ ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2EConjn@(inj__ty_2EDeepSyntax_2Edeep__form @ V8a0))@(inj__ty_2EDeepSyntax_2Edeep__form @ V7a1))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2EUnrelatedBool@V9a)))))))) & (( ! [V10a1:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V11a0:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V12a:tp__ty_2Einteger_2Eint] : (~~ ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2EConjn@(inj__ty_2EDeepSyntax_2Edeep__form @ V11a0))@(inj__ty_2EDeepSyntax_2Edeep__form @ V10a1))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ExLT@(inj__ty_2Einteger_2Eint @ V12a)))))))) & (( ! [V13a1:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V14a0:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V15a:tp__ty_2Einteger_2Eint] : (~~ ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2EConjn@(inj__ty_2EDeepSyntax_2Edeep__form @ V14a0))@(inj__ty_2EDeepSyntax_2Edeep__form @ V13a1))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ELTx@(inj__ty_2Einteger_2Eint @ V15a)))))))) & (( ! [V16a1:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V17a0:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V18a:tp__ty_2Einteger_2Eint] : (~~ ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2EConjn@(inj__ty_2EDeepSyntax_2Edeep__form @ V17a0))@(inj__ty_2EDeepSyntax_2Edeep__form @ V16a1))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ExEQ@(inj__ty_2Einteger_2Eint @ V18a)))))))) & (( ! [V19a1_27:tp__ty_2Einteger_2Eint] : ( ! [V20a1:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V21a0_27:tp__ty_2Einteger_2Eint] : ( ! [V22a0:tp__ty_2EDeepSyntax_2Edeep__form] : (~~ ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2EConjn@(inj__ty_2EDeepSyntax_2Edeep__form @ V22a0))@(inj__ty_2EDeepSyntax_2Edeep__form @ V20a1))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2ExDivided@(inj__ty_2Einteger_2Eint @ V21a0_27))@(inj__ty_2Einteger_2Eint @ V19a1_27))))))))) & (( ! [V23a1:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V24a0:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V25a:tp__ty_2EDeepSyntax_2Edeep__form] : (~~ ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2EDisjn@(inj__ty_2EDeepSyntax_2Edeep__form @ V24a0))@(inj__ty_2EDeepSyntax_2Edeep__form @ V23a1))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ENegn@(inj__ty_2EDeepSyntax_2Edeep__form @ V25a)))))))) & (( ! [V26a1:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V27a0:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V28a:$i] : ((mem@V28a@bool) => (~~ ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2EDisjn@(inj__ty_2EDeepSyntax_2Edeep__form @ V27a0))@(inj__ty_2EDeepSyntax_2Edeep__form @ V26a1))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2EUnrelatedBool@V28a)))))))) & (( ! [V29a1:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V30a0:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V31a:tp__ty_2Einteger_2Eint] : (~~ ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2EDisjn@(inj__ty_2EDeepSyntax_2Edeep__form @ V30a0))@(inj__ty_2EDeepSyntax_2Edeep__form @ V29a1))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ExLT@(inj__ty_2Einteger_2Eint @ V31a)))))))) & (( ! [V32a1:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V33a0:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V34a:tp__ty_2Einteger_2Eint] : (~~ ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2EDisjn@(inj__ty_2EDeepSyntax_2Edeep__form @ V33a0))@(inj__ty_2EDeepSyntax_2Edeep__form @ V32a1))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ELTx@(inj__ty_2Einteger_2Eint @ V34a)))))))) & (( ! [V35a1:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V36a0:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V37a:tp__ty_2Einteger_2Eint] : (~~ ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2EDisjn@(inj__ty_2EDeepSyntax_2Edeep__form @ V36a0))@(inj__ty_2EDeepSyntax_2Edeep__form @ V35a1))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ExEQ@(inj__ty_2Einteger_2Eint @ V37a)))))))) & (( ! [V38a1_27:tp__ty_2Einteger_2Eint] : ( ! [V39a1:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V40a0_27:tp__ty_2Einteger_2Eint] : ( ! [V41a0:tp__ty_2EDeepSyntax_2Edeep__form] : (~~ ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2EDisjn@(inj__ty_2EDeepSyntax_2Edeep__form @ V41a0))@(inj__ty_2EDeepSyntax_2Edeep__form @ V39a1))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2ExDivided@(inj__ty_2Einteger_2Eint @ V40a0_27))@(inj__ty_2Einteger_2Eint @ V38a1_27))))))))) & (( ! [V42a_27:$i] : ((mem@V42a_27@bool) => ( ! [V43a:tp__ty_2EDeepSyntax_2Edeep__form] : (~~ ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ENegn@(inj__ty_2EDeepSyntax_2Edeep__form @ V43a))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2EUnrelatedBool@V42a_27))))))) & (( ! [V44a_27:tp__ty_2Einteger_2Eint] : ( ! [V45a:tp__ty_2EDeepSyntax_2Edeep__form] : (~~ ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ENegn@(inj__ty_2EDeepSyntax_2Edeep__form @ V45a))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ExLT@(inj__ty_2Einteger_2Eint @ V44a_27))))))) & (( ! [V46a_27:tp__ty_2Einteger_2Eint] : ( ! [V47a:tp__ty_2EDeepSyntax_2Edeep__form] : (~~ ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ENegn@(inj__ty_2EDeepSyntax_2Edeep__form @ V47a))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ELTx@(inj__ty_2Einteger_2Eint @ V46a_27))))))) & (( ! [V48a_27:tp__ty_2Einteger_2Eint] : ( ! [V49a:tp__ty_2EDeepSyntax_2Edeep__form] : (~~ ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ENegn@(inj__ty_2EDeepSyntax_2Edeep__form @ V49a))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ExEQ@(inj__ty_2Einteger_2Eint @ V48a_27))))))) & (( ! [V50a1:tp__ty_2Einteger_2Eint] : ( ! [V51a0:tp__ty_2Einteger_2Eint] : ( ! [V52a:tp__ty_2EDeepSyntax_2Edeep__form] : (~~ ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ENegn@(inj__ty_2EDeepSyntax_2Edeep__form @ V52a))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2ExDivided@(inj__ty_2Einteger_2Eint @ V51a0))@(inj__ty_2Einteger_2Eint @ V50a1)))))))) & (( ! [V53a_27:tp__ty_2Einteger_2Eint] : ( ! [V54a:$i] : ((mem@V54a@bool) => (~~ ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2EUnrelatedBool@V54a)) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ExLT@(inj__ty_2Einteger_2Eint @ V53a_27)))))))) & (( ! [V55a_27:tp__ty_2Einteger_2Eint] : ( ! [V56a:$i] : ((mem@V56a@bool) => (~~ ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2EUnrelatedBool@V56a)) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ELTx@(inj__ty_2Einteger_2Eint @ V55a_27)))))))) & (( ! [V57a_27:tp__ty_2Einteger_2Eint] : ( ! [V58a:$i] : ((mem@V58a@bool) => (~~ ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2EUnrelatedBool@V58a)) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ExEQ@(inj__ty_2Einteger_2Eint @ V57a_27)))))))) & (( ! [V59a1:tp__ty_2Einteger_2Eint] : ( ! [V60a0:tp__ty_2Einteger_2Eint] : ( ! [V61a:$i] : ((mem@V61a@bool) => (~~ ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2EUnrelatedBool@V61a)) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2ExDivided@(inj__ty_2Einteger_2Eint @ V60a0))@(inj__ty_2Einteger_2Eint @ V59a1))))))))) & (( ! [V62a_27:tp__ty_2Einteger_2Eint] : ( ! [V63a:tp__ty_2Einteger_2Eint] : (~~ ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ExLT@(inj__ty_2Einteger_2Eint @ V63a))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ELTx@(inj__ty_2Einteger_2Eint @ V62a_27))))))) & (( ! [V64a_27:tp__ty_2Einteger_2Eint] : ( ! [V65a:tp__ty_2Einteger_2Eint] : (~~ ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ExLT@(inj__ty_2Einteger_2Eint @ V65a))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ExEQ@(inj__ty_2Einteger_2Eint @ V64a_27))))))) & (( ! [V66a1:tp__ty_2Einteger_2Eint] : ( ! [V67a0:tp__ty_2Einteger_2Eint] : ( ! [V68a:tp__ty_2Einteger_2Eint] : (~~ ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ExLT@(inj__ty_2Einteger_2Eint @ V68a))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2ExDivided@(inj__ty_2Einteger_2Eint @ V67a0))@(inj__ty_2Einteger_2Eint @ V66a1)))))))) & (( ! [V69a_27:tp__ty_2Einteger_2Eint] : ( ! [V70a:tp__ty_2Einteger_2Eint] : (~~ ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ELTx@(inj__ty_2Einteger_2Eint @ V70a))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ExEQ@(inj__ty_2Einteger_2Eint @ V69a_27))))))) & (( ! [V71a1:tp__ty_2Einteger_2Eint] : ( ! [V72a0:tp__ty_2Einteger_2Eint] : ( ! [V73a:tp__ty_2Einteger_2Eint] : (~~ ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ELTx@(inj__ty_2Einteger_2Eint @ V73a))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2ExDivided@(inj__ty_2Einteger_2Eint @ V72a0))@(inj__ty_2Einteger_2Eint @ V71a1)))))))) & ( ! [V74a1:tp__ty_2Einteger_2Eint] : ( ! [V75a0:tp__ty_2Einteger_2Eint] : ( ! [V76a:tp__ty_2Einteger_2Eint] : (~~ ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ExEQ@(inj__ty_2Einteger_2Eint @ V76a))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2ExDivided@(inj__ty_2Einteger_2Eint @ V75a0))@(inj__ty_2Einteger_2Eint @ V74a1)))))))))))))))))))))))))))))))))))).
thf(conj_thm_2EDeepSyntax_2Edeep__form__nchotomy,lemma,( ! [V0dd:tp__ty_2EDeepSyntax_2Edeep__form] : ((? [V1d:tp__ty_2EDeepSyntax_2Edeep__form] : (? [V2d0:tp__ty_2EDeepSyntax_2Edeep__form] : (V0dd = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2EConjn@(inj__ty_2EDeepSyntax_2Edeep__form @ V1d))@(inj__ty_2EDeepSyntax_2Edeep__form @ V2d0)))))) | ((? [V3d:tp__ty_2EDeepSyntax_2Edeep__form] : (? [V4d0:tp__ty_2EDeepSyntax_2Edeep__form] : (V0dd = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2EDisjn@(inj__ty_2EDeepSyntax_2Edeep__form @ V3d))@(inj__ty_2EDeepSyntax_2Edeep__form @ V4d0)))))) | ((? [V5d:tp__ty_2EDeepSyntax_2Edeep__form] : (V0dd = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ENegn@(inj__ty_2EDeepSyntax_2Edeep__form @ V5d))))) | ((? [V6b:$i] : ((mem@V6b@bool) & (V0dd = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2EUnrelatedBool@V6b))))) | ((? [V7i:tp__ty_2Einteger_2Eint] : (V0dd = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ExLT@(inj__ty_2Einteger_2Eint @ V7i))))) | ((? [V8i:tp__ty_2Einteger_2Eint] : (V0dd = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ELTx@(inj__ty_2Einteger_2Eint @ V8i))))) | ((? [V9i:tp__ty_2Einteger_2Eint] : (V0dd = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ExEQ@(inj__ty_2Einteger_2Eint @ V9i))))) | (? [V10i:tp__ty_2Einteger_2Eint] : (? [V11i0:tp__ty_2Einteger_2Eint] : (V0dd = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2ExDivided@(inj__ty_2Einteger_2Eint @ V10i))@(inj__ty_2Einteger_2Eint @ V11i0))))))))))))))).
thf(conj_thm_2EDeepSyntax_2Edeep__form__Axiom,lemma,( ! [A_27a:del]: ( ! [V0f0:$i] : ((mem@V0f0@(arr@ty_2EDeepSyntax_2Edeep__form@(arr@ty_2EDeepSyntax_2Edeep__form@(arr@A_27a@(arr@A_27a@A_27a))))) => ( ! [V1f1:$i] : ((mem@V1f1@(arr@ty_2EDeepSyntax_2Edeep__form@(arr@ty_2EDeepSyntax_2Edeep__form@(arr@A_27a@(arr@A_27a@A_27a))))) => ( ! [V2f2:$i] : ((mem@V2f2@(arr@ty_2EDeepSyntax_2Edeep__form@(arr@A_27a@A_27a))) => ( ! [V3f3:$i] : ((mem@V3f3@(arr@bool@A_27a)) => ( ! [V4f4:$i] : ((mem@V4f4@(arr@ty_2Einteger_2Eint@A_27a)) => ( ! [V5f5:$i] : ((mem@V5f5@(arr@ty_2Einteger_2Eint@A_27a)) => ( ! [V6f6:$i] : ((mem@V6f6@(arr@ty_2Einteger_2Eint@A_27a)) => ( ! [V7f7:$i] : ((mem@V7f7@(arr@ty_2Einteger_2Eint@(arr@ty_2Einteger_2Eint@A_27a))) => (? [V8fn:$i] : ((mem@V8fn@(arr@ty_2EDeepSyntax_2Edeep__form@A_27a)) & (( ! [V9a0:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V10a1:tp__ty_2EDeepSyntax_2Edeep__form] : ((ap@V8fn@(ap@(ap@c_2EDeepSyntax_2EConjn@(inj__ty_2EDeepSyntax_2Edeep__form @ V9a0))@(inj__ty_2EDeepSyntax_2Edeep__form @ V10a1))) = (ap@(ap@(ap@(ap@V0f0@(inj__ty_2EDeepSyntax_2Edeep__form @ V9a0))@(inj__ty_2EDeepSyntax_2Edeep__form @ V10a1))@(ap@V8fn@(inj__ty_2EDeepSyntax_2Edeep__form @ V9a0)))@(ap@V8fn@(inj__ty_2EDeepSyntax_2Edeep__form @ V10a1)))))) & (( ! [V11a0:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V12a1:tp__ty_2EDeepSyntax_2Edeep__form] : ((ap@V8fn@(ap@(ap@c_2EDeepSyntax_2EDisjn@(inj__ty_2EDeepSyntax_2Edeep__form @ V11a0))@(inj__ty_2EDeepSyntax_2Edeep__form @ V12a1))) = (ap@(ap@(ap@(ap@V1f1@(inj__ty_2EDeepSyntax_2Edeep__form @ V11a0))@(inj__ty_2EDeepSyntax_2Edeep__form @ V12a1))@(ap@V8fn@(inj__ty_2EDeepSyntax_2Edeep__form @ V11a0)))@(ap@V8fn@(inj__ty_2EDeepSyntax_2Edeep__form @ V12a1)))))) & (( ! [V13a:tp__ty_2EDeepSyntax_2Edeep__form] : ((ap@V8fn@(ap@c_2EDeepSyntax_2ENegn@(inj__ty_2EDeepSyntax_2Edeep__form @ V13a))) = (ap@(ap@V2f2@(inj__ty_2EDeepSyntax_2Edeep__form @ V13a))@(ap@V8fn@(inj__ty_2EDeepSyntax_2Edeep__form @ V13a))))) & (( ! [V14a:$i] : ((mem@V14a@bool) => ((ap@V8fn@(ap@c_2EDeepSyntax_2EUnrelatedBool@V14a)) = (ap@V3f3@V14a)))) & (( ! [V15a:tp__ty_2Einteger_2Eint] : ((ap@V8fn@(ap@c_2EDeepSyntax_2ExLT@(inj__ty_2Einteger_2Eint @ V15a))) = (ap@V4f4@(inj__ty_2Einteger_2Eint @ V15a)))) & (( ! [V16a:tp__ty_2Einteger_2Eint] : ((ap@V8fn@(ap@c_2EDeepSyntax_2ELTx@(inj__ty_2Einteger_2Eint @ V16a))) = (ap@V5f5@(inj__ty_2Einteger_2Eint @ V16a)))) & (( ! [V17a:tp__ty_2Einteger_2Eint] : ((ap@V8fn@(ap@c_2EDeepSyntax_2ExEQ@(inj__ty_2Einteger_2Eint @ V17a))) = (ap@V6f6@(inj__ty_2Einteger_2Eint @ V17a)))) & ( ! [V18a0:tp__ty_2Einteger_2Eint] : ( ! [V19a1:tp__ty_2Einteger_2Eint] : ((ap@V8fn@(ap@(ap@c_2EDeepSyntax_2ExDivided@(inj__ty_2Einteger_2Eint @ V18a0))@(inj__ty_2Einteger_2Eint @ V19a1))) = (ap@(ap@V7f7@(inj__ty_2Einteger_2Eint @ V18a0))@(inj__ty_2Einteger_2Eint @ V19a1)))))))))))))))))))))))))))))))).
thf(conj_thm_2EDeepSyntax_2Edeep__form__induction,lemma,( ! [V0P:$i] : ((mem@V0P@(arr@ty_2EDeepSyntax_2Edeep__form@bool)) => ((( ! [V1d:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V2d0:tp__ty_2EDeepSyntax_2Edeep__form] : (((p@(ap@V0P@(inj__ty_2EDeepSyntax_2Edeep__form @ V1d))) & (p@(ap@V0P@(inj__ty_2EDeepSyntax_2Edeep__form @ V2d0)))) => (p@(ap@V0P@(ap@(ap@c_2EDeepSyntax_2EConjn@(inj__ty_2EDeepSyntax_2Edeep__form @ V1d))@(inj__ty_2EDeepSyntax_2Edeep__form @ V2d0))))))) & (( ! [V3d:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V4d0:tp__ty_2EDeepSyntax_2Edeep__form] : (((p@(ap@V0P@(inj__ty_2EDeepSyntax_2Edeep__form @ V3d))) & (p@(ap@V0P@(inj__ty_2EDeepSyntax_2Edeep__form @ V4d0)))) => (p@(ap@V0P@(ap@(ap@c_2EDeepSyntax_2EDisjn@(inj__ty_2EDeepSyntax_2Edeep__form @ V3d))@(inj__ty_2EDeepSyntax_2Edeep__form @ V4d0))))))) & (( ! [V5d:tp__ty_2EDeepSyntax_2Edeep__form] : ((p@(ap@V0P@(inj__ty_2EDeepSyntax_2Edeep__form @ V5d))) => (p@(ap@V0P@(ap@c_2EDeepSyntax_2ENegn@(inj__ty_2EDeepSyntax_2Edeep__form @ V5d)))))) & (( ! [V6b:$i] : ((mem@V6b@bool) => (p@(ap@V0P@(ap@c_2EDeepSyntax_2EUnrelatedBool@V6b))))) & (( ! [V7i:tp__ty_2Einteger_2Eint] : (p@(ap@V0P@(ap@c_2EDeepSyntax_2ExLT@(inj__ty_2Einteger_2Eint @ V7i))))) & (( ! [V8i:tp__ty_2Einteger_2Eint] : (p@(ap@V0P@(ap@c_2EDeepSyntax_2ELTx@(inj__ty_2Einteger_2Eint @ V8i))))) & (( ! [V9i:tp__ty_2Einteger_2Eint] : (p@(ap@V0P@(ap@c_2EDeepSyntax_2ExEQ@(inj__ty_2Einteger_2Eint @ V9i))))) & ( ! [V10i:tp__ty_2Einteger_2Eint] : ( ! [V11i0:tp__ty_2Einteger_2Eint] : (p@(ap@V0P@(ap@(ap@c_2EDeepSyntax_2ExDivided@(inj__ty_2Einteger_2Eint @ V10i))@(inj__ty_2Einteger_2Eint @ V11i0))))))))))))) => ( ! [V12d:tp__ty_2EDeepSyntax_2Edeep__form] : (p@(ap@V0P@(inj__ty_2EDeepSyntax_2Edeep__form @ V12d)))))))).
thf(conj_thm_2EDeepSyntax_2Edeep__form__case__cong,lemma,( ! [A_27a:del]: ( ! [V0f_27:$i] : ((mem@V0f_27@(arr@ty_2EDeepSyntax_2Edeep__form@(arr@ty_2EDeepSyntax_2Edeep__form@A_27a))) => ( ! [V1f1_27:$i] : ((mem@V1f1_27@(arr@ty_2EDeepSyntax_2Edeep__form@(arr@ty_2EDeepSyntax_2Edeep__form@A_27a))) => ( ! [V2f2_27:$i] : ((mem@V2f2_27@(arr@ty_2EDeepSyntax_2Edeep__form@A_27a)) => ( ! [V3f3_27:$i] : ((mem@V3f3_27@(arr@bool@A_27a)) => ( ! [V4f4_27:$i] : ((mem@V4f4_27@(arr@ty_2Einteger_2Eint@A_27a)) => ( ! [V5f5_27:$i] : ((mem@V5f5_27@(arr@ty_2Einteger_2Eint@A_27a)) => ( ! [V6f6_27:$i] : ((mem@V6f6_27@(arr@ty_2Einteger_2Eint@A_27a)) => ( ! [V7f7_27:$i] : ((mem@V7f7_27@(arr@ty_2Einteger_2Eint@(arr@ty_2Einteger_2Eint@A_27a))) => ( ! [V8M:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V9M_27:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V10f:$i] : ((mem@V10f@(arr@ty_2EDeepSyntax_2Edeep__form@(arr@ty_2EDeepSyntax_2Edeep__form@A_27a))) => ( ! [V11f1:$i] : ((mem@V11f1@(arr@ty_2EDeepSyntax_2Edeep__form@(arr@ty_2EDeepSyntax_2Edeep__form@A_27a))) => ( ! [V12f2:$i] : ((mem@V12f2@(arr@ty_2EDeepSyntax_2Edeep__form@A_27a)) => ( ! [V13f3:$i] : ((mem@V13f3@(arr@bool@A_27a)) => ( ! [V14f4:$i] : ((mem@V14f4@(arr@ty_2Einteger_2Eint@A_27a)) => ( ! [V15f5:$i] : ((mem@V15f5@(arr@ty_2Einteger_2Eint@A_27a)) => ( ! [V16f6:$i] : ((mem@V16f6@(arr@ty_2Einteger_2Eint@A_27a)) => ( ! [V17f7:$i] : ((mem@V17f7@(arr@ty_2Einteger_2Eint@(arr@ty_2Einteger_2Eint@A_27a))) => (((V8M = V9M_27) & (( ! [V18a0:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V19a1:tp__ty_2EDeepSyntax_2Edeep__form] : ((V9M_27 = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2EConjn@(inj__ty_2EDeepSyntax_2Edeep__form @ V18a0))@(inj__ty_2EDeepSyntax_2Edeep__form @ V19a1)))) => ((ap@(ap@V10f@(inj__ty_2EDeepSyntax_2Edeep__form @ V18a0))@(inj__ty_2EDeepSyntax_2Edeep__form @ V19a1)) = (ap@(ap@V0f_27@(inj__ty_2EDeepSyntax_2Edeep__form @ V18a0))@(inj__ty_2EDeepSyntax_2Edeep__form @ V19a1)))))) & (( ! [V20a0:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V21a1:tp__ty_2EDeepSyntax_2Edeep__form] : ((V9M_27 = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2EDisjn@(inj__ty_2EDeepSyntax_2Edeep__form @ V20a0))@(inj__ty_2EDeepSyntax_2Edeep__form @ V21a1)))) => ((ap@(ap@V11f1@(inj__ty_2EDeepSyntax_2Edeep__form @ V20a0))@(inj__ty_2EDeepSyntax_2Edeep__form @ V21a1)) = (ap@(ap@V1f1_27@(inj__ty_2EDeepSyntax_2Edeep__form @ V20a0))@(inj__ty_2EDeepSyntax_2Edeep__form @ V21a1)))))) & (( ! [V22a:tp__ty_2EDeepSyntax_2Edeep__form] : ((V9M_27 = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ENegn@(inj__ty_2EDeepSyntax_2Edeep__form @ V22a)))) => ((ap@V12f2@(inj__ty_2EDeepSyntax_2Edeep__form @ V22a)) = (ap@V2f2_27@(inj__ty_2EDeepSyntax_2Edeep__form @ V22a))))) & (( ! [V23a:$i] : ((mem@V23a@bool) => ((V9M_27 = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2EUnrelatedBool@V23a))) => ((ap@V13f3@V23a) = (ap@V3f3_27@V23a))))) & (( ! [V24a:tp__ty_2Einteger_2Eint] : ((V9M_27 = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ExLT@(inj__ty_2Einteger_2Eint @ V24a)))) => ((ap@V14f4@(inj__ty_2Einteger_2Eint @ V24a)) = (ap@V4f4_27@(inj__ty_2Einteger_2Eint @ V24a))))) & (( ! [V25a:tp__ty_2Einteger_2Eint] : ((V9M_27 = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ELTx@(inj__ty_2Einteger_2Eint @ V25a)))) => ((ap@V15f5@(inj__ty_2Einteger_2Eint @ V25a)) = (ap@V5f5_27@(inj__ty_2Einteger_2Eint @ V25a))))) & (( ! [V26a:tp__ty_2Einteger_2Eint] : ((V9M_27 = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ExEQ@(inj__ty_2Einteger_2Eint @ V26a)))) => ((ap@V16f6@(inj__ty_2Einteger_2Eint @ V26a)) = (ap@V6f6_27@(inj__ty_2Einteger_2Eint @ V26a))))) & ( ! [V27a0:tp__ty_2Einteger_2Eint] : ( ! [V28a1:tp__ty_2Einteger_2Eint] : ((V9M_27 = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2ExDivided@(inj__ty_2Einteger_2Eint @ V27a0))@(inj__ty_2Einteger_2Eint @ V28a1)))) => ((ap@(ap@V17f7@(inj__ty_2Einteger_2Eint @ V27a0))@(inj__ty_2Einteger_2Eint @ V28a1)) = (ap@(ap@V7f7_27@(inj__ty_2Einteger_2Eint @ V27a0))@(inj__ty_2Einteger_2Eint @ V28a1)))))))))))))) => ((ap@(ap@(ap@(ap@(ap@(ap@(ap@(ap@(ap@(c_2EDeepSyntax_2Edeep__form__CASE@A_27a)@(inj__ty_2EDeepSyntax_2Edeep__form @ V8M))@V10f)@V11f1)@V12f2)@V13f3)@V14f4)@V15f5)@V16f6)@V17f7) = (ap@(ap@(ap@(ap@(ap@(ap@(ap@(ap@(ap@(c_2EDeepSyntax_2Edeep__form__CASE@A_27a)@(inj__ty_2EDeepSyntax_2Edeep__form @ V9M_27))@V0f_27)@V1f1_27)@V2f2_27)@V3f3_27)@V4f4_27)@V5f5_27)@V6f6_27)@V7f7_27))))))))))))))))))))))))))))))))))))))).
thf(conj_thm_2EDeepSyntax_2Edeep__form__case__eq,lemma,( ! [A_27a:del]: ( ! [V0x:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V1f:$i] : ((mem@V1f@(arr@ty_2EDeepSyntax_2Edeep__form@(arr@ty_2EDeepSyntax_2Edeep__form@A_27a))) => ( ! [V2f1:$i] : ((mem@V2f1@(arr@ty_2EDeepSyntax_2Edeep__form@(arr@ty_2EDeepSyntax_2Edeep__form@A_27a))) => ( ! [V3f2:$i] : ((mem@V3f2@(arr@ty_2EDeepSyntax_2Edeep__form@A_27a)) => ( ! [V4f3:$i] : ((mem@V4f3@(arr@bool@A_27a)) => ( ! [V5f4:$i] : ((mem@V5f4@(arr@ty_2Einteger_2Eint@A_27a)) => ( ! [V6f5:$i] : ((mem@V6f5@(arr@ty_2Einteger_2Eint@A_27a)) => ( ! [V7f6:$i] : ((mem@V7f6@(arr@ty_2Einteger_2Eint@A_27a)) => ( ! [V8f7:$i] : ((mem@V8f7@(arr@ty_2Einteger_2Eint@(arr@ty_2Einteger_2Eint@A_27a))) => ( ! [V9v:$i] : ((mem@V9v@A_27a) => (((ap@(ap@(ap@(ap@(ap@(ap@(ap@(ap@(ap@(c_2EDeepSyntax_2Edeep__form__CASE@A_27a)@(inj__ty_2EDeepSyntax_2Edeep__form @ V0x))@V1f)@V2f1)@V3f2)@V4f3)@V5f4)@V6f5)@V7f6)@V8f7) = V9v) <=> ((? [V10d:tp__ty_2EDeepSyntax_2Edeep__form] : (? [V11d0:tp__ty_2EDeepSyntax_2Edeep__form] : ((V0x = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2EConjn@(inj__ty_2EDeepSyntax_2Edeep__form @ V10d))@(inj__ty_2EDeepSyntax_2Edeep__form @ V11d0)))) & ((ap@(ap@V1f@(inj__ty_2EDeepSyntax_2Edeep__form @ V10d))@(inj__ty_2EDeepSyntax_2Edeep__form @ V11d0)) = V9v)))) | ((? [V12d:tp__ty_2EDeepSyntax_2Edeep__form] : (? [V13d0:tp__ty_2EDeepSyntax_2Edeep__form] : ((V0x = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2EDisjn@(inj__ty_2EDeepSyntax_2Edeep__form @ V12d))@(inj__ty_2EDeepSyntax_2Edeep__form @ V13d0)))) & ((ap@(ap@V2f1@(inj__ty_2EDeepSyntax_2Edeep__form @ V12d))@(inj__ty_2EDeepSyntax_2Edeep__form @ V13d0)) = V9v)))) | ((? [V14d:tp__ty_2EDeepSyntax_2Edeep__form] : ((V0x = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ENegn@(inj__ty_2EDeepSyntax_2Edeep__form @ V14d)))) & ((ap@V3f2@(inj__ty_2EDeepSyntax_2Edeep__form @ V14d)) = V9v))) | ((? [V15b:$i] : ((mem@V15b@bool) & ((V0x = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2EUnrelatedBool@V15b))) & ((ap@V4f3@V15b) = V9v)))) | ((? [V16i:tp__ty_2Einteger_2Eint] : ((V0x = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ExLT@(inj__ty_2Einteger_2Eint @ V16i)))) & ((ap@V5f4@(inj__ty_2Einteger_2Eint @ V16i)) = V9v))) | ((? [V17i:tp__ty_2Einteger_2Eint] : ((V0x = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ELTx@(inj__ty_2Einteger_2Eint @ V17i)))) & ((ap@V6f5@(inj__ty_2Einteger_2Eint @ V17i)) = V9v))) | ((? [V18i:tp__ty_2Einteger_2Eint] : ((V0x = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ExEQ@(inj__ty_2Einteger_2Eint @ V18i)))) & ((ap@V7f6@(inj__ty_2Einteger_2Eint @ V18i)) = V9v))) | (? [V19i:tp__ty_2Einteger_2Eint] : (? [V20i0:tp__ty_2Einteger_2Eint] : ((V0x = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2ExDivided@(inj__ty_2Einteger_2Eint @ V19i))@(inj__ty_2Einteger_2Eint @ V20i0)))) & ((ap@(ap@V8f7@(inj__ty_2Einteger_2Eint @ V19i))@(inj__ty_2Einteger_2Eint @ V20i0)) = V9v))))))))))))))))))))))))))))))))).
thf(ax_thm_2EDeepSyntax_2Eeval__form__def,axiom,(( ! [V0f1:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V1f2:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V2x:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2EDeepSyntax_2Eeval__form@(ap@(ap@c_2EDeepSyntax_2EConjn@(inj__ty_2EDeepSyntax_2Edeep__form @ V0f1))@(inj__ty_2EDeepSyntax_2Edeep__form @ V1f2)))@(inj__ty_2Einteger_2Eint @ V2x))) <=> ((p@(ap@(ap@c_2EDeepSyntax_2Eeval__form@(inj__ty_2EDeepSyntax_2Edeep__form @ V0f1))@(inj__ty_2Einteger_2Eint @ V2x))) & (p@(ap@(ap@c_2EDeepSyntax_2Eeval__form@(inj__ty_2EDeepSyntax_2Edeep__form @ V1f2))@(inj__ty_2Einteger_2Eint @ V2x)))))))) & (( ! [V3f1:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V4f2:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V5x:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2EDeepSyntax_2Eeval__form@(ap@(ap@c_2EDeepSyntax_2EDisjn@(inj__ty_2EDeepSyntax_2Edeep__form @ V3f1))@(inj__ty_2EDeepSyntax_2Edeep__form @ V4f2)))@(inj__ty_2Einteger_2Eint @ V5x))) <=> ((p@(ap@(ap@c_2EDeepSyntax_2Eeval__form@(inj__ty_2EDeepSyntax_2Edeep__form @ V3f1))@(inj__ty_2Einteger_2Eint @ V5x))) | (p@(ap@(ap@c_2EDeepSyntax_2Eeval__form@(inj__ty_2EDeepSyntax_2Edeep__form @ V4f2))@(inj__ty_2Einteger_2Eint @ V5x)))))))) & (( ! [V6f:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V7x:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2EDeepSyntax_2Eeval__form@(ap@c_2EDeepSyntax_2ENegn@(inj__ty_2EDeepSyntax_2Edeep__form @ V6f)))@(inj__ty_2Einteger_2Eint @ V7x))) <=> (~ (p@(ap@(ap@c_2EDeepSyntax_2Eeval__form@(inj__ty_2EDeepSyntax_2Edeep__form @ V6f))@(inj__ty_2Einteger_2Eint @ V7x))))))) & (( ! [V8b:$i] : ((mem@V8b@bool) => ( ! [V9x:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2EDeepSyntax_2Eeval__form@(ap@c_2EDeepSyntax_2EUnrelatedBool@V8b))@(inj__ty_2Einteger_2Eint @ V9x))) <=> (p@V8b))))) & (( ! [V10i:tp__ty_2Einteger_2Eint] : ( ! [V11x:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2EDeepSyntax_2Eeval__form@(ap@c_2EDeepSyntax_2ExLT@(inj__ty_2Einteger_2Eint @ V10i)))@(inj__ty_2Einteger_2Eint @ V11x))) <=> (p@(ap@(ap@c_2Einteger_2Eint__lt@(inj__ty_2Einteger_2Eint @ V11x))@(inj__ty_2Einteger_2Eint @ V10i)))))) & (( ! [V12i:tp__ty_2Einteger_2Eint] : ( ! [V13x:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2EDeepSyntax_2Eeval__form@(ap@c_2EDeepSyntax_2ELTx@(inj__ty_2Einteger_2Eint @ V12i)))@(inj__ty_2Einteger_2Eint @ V13x))) <=> (p@(ap@(ap@c_2Einteger_2Eint__lt@(inj__ty_2Einteger_2Eint @ V12i))@(inj__ty_2Einteger_2Eint @ V13x)))))) & (( ! [V14i:tp__ty_2Einteger_2Eint] : ( ! [V15x:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2EDeepSyntax_2Eeval__form@(ap@c_2EDeepSyntax_2ExEQ@(inj__ty_2Einteger_2Eint @ V14i)))@(inj__ty_2Einteger_2Eint @ V15x))) <=> (V15x = V14i)))) & ( ! [V16i1:tp__ty_2Einteger_2Eint] : ( ! [V17i2:tp__ty_2Einteger_2Eint] : ( ! [V18x:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2EDeepSyntax_2Eeval__form@(ap@(ap@c_2EDeepSyntax_2ExDivided@(inj__ty_2Einteger_2Eint @ V16i1))@(inj__ty_2Einteger_2Eint @ V17i2)))@(inj__ty_2Einteger_2Eint @ V18x))) <=> (p@(ap@(ap@c_2Einteger_2Eint__divides@(inj__ty_2Einteger_2Eint @ V16i1))@(ap@(ap@c_2Einteger_2Eint__add@(inj__ty_2Einteger_2Eint @ V18x))@(inj__ty_2Einteger_2Eint @ V17i2)))))))))))))))).
thf(ax_thm_2EDeepSyntax_2Eneginf__def,axiom,(( ! [V0f1:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V1f2:tp__ty_2EDeepSyntax_2Edeep__form] : ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2Eneginf@(ap@(ap@c_2EDeepSyntax_2EConjn@(inj__ty_2EDeepSyntax_2Edeep__form @ V0f1))@(inj__ty_2EDeepSyntax_2Edeep__form @ V1f2)))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2EConjn@(ap@c_2EDeepSyntax_2Eneginf@(inj__ty_2EDeepSyntax_2Edeep__form @ V0f1)))@(ap@c_2EDeepSyntax_2Eneginf@(inj__ty_2EDeepSyntax_2Edeep__form @ V1f2))))))) & (( ! [V2f1:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V3f2:tp__ty_2EDeepSyntax_2Edeep__form] : ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2Eneginf@(ap@(ap@c_2EDeepSyntax_2EDisjn@(inj__ty_2EDeepSyntax_2Edeep__form @ V2f1))@(inj__ty_2EDeepSyntax_2Edeep__form @ V3f2)))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2EDisjn@(ap@c_2EDeepSyntax_2Eneginf@(inj__ty_2EDeepSyntax_2Edeep__form @ V2f1)))@(ap@c_2EDeepSyntax_2Eneginf@(inj__ty_2EDeepSyntax_2Edeep__form @ V3f2))))))) & (( ! [V4f:tp__ty_2EDeepSyntax_2Edeep__form] : ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2Eneginf@(ap@c_2EDeepSyntax_2ENegn@(inj__ty_2EDeepSyntax_2Edeep__form @ V4f)))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ENegn@(ap@c_2EDeepSyntax_2Eneginf@(inj__ty_2EDeepSyntax_2Edeep__form @ V4f)))))) & (( ! [V5b:$i] : ((mem@V5b@bool) => ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2Eneginf@(ap@c_2EDeepSyntax_2EUnrelatedBool@V5b))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2EUnrelatedBool@V5b))))) & (( ! [V6i:tp__ty_2Einteger_2Eint] : ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2Eneginf@(ap@c_2EDeepSyntax_2ExLT@(inj__ty_2Einteger_2Eint @ V6i)))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2EUnrelatedBool@c_2Ebool_2ET)))) & (( ! [V7i:tp__ty_2Einteger_2Eint] : ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2Eneginf@(ap@c_2EDeepSyntax_2ELTx@(inj__ty_2Einteger_2Eint @ V7i)))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2EUnrelatedBool@c_2Ebool_2EF)))) & (( ! [V8i:tp__ty_2Einteger_2Eint] : ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2Eneginf@(ap@c_2EDeepSyntax_2ExEQ@(inj__ty_2Einteger_2Eint @ V8i)))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2EUnrelatedBool@c_2Ebool_2EF)))) & ( ! [V9i1:tp__ty_2Einteger_2Eint] : ( ! [V10i2:tp__ty_2Einteger_2Eint] : ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2Eneginf@(ap@(ap@c_2EDeepSyntax_2ExDivided@(inj__ty_2Einteger_2Eint @ V9i1))@(inj__ty_2Einteger_2Eint @ V10i2)))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2ExDivided@(inj__ty_2Einteger_2Eint @ V9i1))@(inj__ty_2Einteger_2Eint @ V10i2)))))))))))))).
thf(ax_thm_2EDeepSyntax_2Eposinf__def,axiom,(( ! [V0f1:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V1f2:tp__ty_2EDeepSyntax_2Edeep__form] : ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2Eposinf@(ap@(ap@c_2EDeepSyntax_2EConjn@(inj__ty_2EDeepSyntax_2Edeep__form @ V0f1))@(inj__ty_2EDeepSyntax_2Edeep__form @ V1f2)))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2EConjn@(ap@c_2EDeepSyntax_2Eposinf@(inj__ty_2EDeepSyntax_2Edeep__form @ V0f1)))@(ap@c_2EDeepSyntax_2Eposinf@(inj__ty_2EDeepSyntax_2Edeep__form @ V1f2))))))) & (( ! [V2f1:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V3f2:tp__ty_2EDeepSyntax_2Edeep__form] : ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2Eposinf@(ap@(ap@c_2EDeepSyntax_2EDisjn@(inj__ty_2EDeepSyntax_2Edeep__form @ V2f1))@(inj__ty_2EDeepSyntax_2Edeep__form @ V3f2)))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2EDisjn@(ap@c_2EDeepSyntax_2Eposinf@(inj__ty_2EDeepSyntax_2Edeep__form @ V2f1)))@(ap@c_2EDeepSyntax_2Eposinf@(inj__ty_2EDeepSyntax_2Edeep__form @ V3f2))))))) & (( ! [V4f:tp__ty_2EDeepSyntax_2Edeep__form] : ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2Eposinf@(ap@c_2EDeepSyntax_2ENegn@(inj__ty_2EDeepSyntax_2Edeep__form @ V4f)))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2ENegn@(ap@c_2EDeepSyntax_2Eposinf@(inj__ty_2EDeepSyntax_2Edeep__form @ V4f)))))) & (( ! [V5b:$i] : ((mem@V5b@bool) => ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2Eposinf@(ap@c_2EDeepSyntax_2EUnrelatedBool@V5b))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2EUnrelatedBool@V5b))))) & (( ! [V6i:tp__ty_2Einteger_2Eint] : ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2Eposinf@(ap@c_2EDeepSyntax_2ExLT@(inj__ty_2Einteger_2Eint @ V6i)))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2EUnrelatedBool@c_2Ebool_2EF)))) & (( ! [V7i:tp__ty_2Einteger_2Eint] : ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2Eposinf@(ap@c_2EDeepSyntax_2ELTx@(inj__ty_2Einteger_2Eint @ V7i)))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2EUnrelatedBool@c_2Ebool_2ET)))) & (( ! [V8i:tp__ty_2Einteger_2Eint] : ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2Eposinf@(ap@c_2EDeepSyntax_2ExEQ@(inj__ty_2Einteger_2Eint @ V8i)))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2EUnrelatedBool@c_2Ebool_2EF)))) & ( ! [V9i1:tp__ty_2Einteger_2Eint] : ( ! [V10i2:tp__ty_2Einteger_2Eint] : ((surj__ty_2EDeepSyntax_2Edeep__form @ (ap@c_2EDeepSyntax_2Eposinf@(ap@(ap@c_2EDeepSyntax_2ExDivided@(inj__ty_2Einteger_2Eint @ V9i1))@(inj__ty_2Einteger_2Eint @ V10i2)))) = (surj__ty_2EDeepSyntax_2Edeep__form @ (ap@(ap@c_2EDeepSyntax_2ExDivided@(inj__ty_2Einteger_2Eint @ V9i1))@(inj__ty_2Einteger_2Eint @ V10i2)))))))))))))).
thf(conj_thm_2EDeepSyntax_2Eneginf__ok,lemma,( ! [V0f:tp__ty_2EDeepSyntax_2Edeep__form] : (? [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2x:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2Einteger_2Eint__lt@(inj__ty_2Einteger_2Eint @ V2x))@(inj__ty_2Einteger_2Eint @ V1y))) => ((p@(ap@(ap@c_2EDeepSyntax_2Eeval__form@(inj__ty_2EDeepSyntax_2Edeep__form @ V0f))@(inj__ty_2Einteger_2Eint @ V2x))) <=> (p@(ap@(ap@c_2EDeepSyntax_2Eeval__form@(ap@c_2EDeepSyntax_2Eneginf@(inj__ty_2EDeepSyntax_2Edeep__form @ V0f)))@(inj__ty_2Einteger_2Eint @ V2x))))))))).
thf(conj_thm_2EDeepSyntax_2Eposinf__ok,lemma,( ! [V0f:tp__ty_2EDeepSyntax_2Edeep__form] : (? [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2x:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2Einteger_2Eint__lt@(inj__ty_2Einteger_2Eint @ V1y))@(inj__ty_2Einteger_2Eint @ V2x))) => ((p@(ap@(ap@c_2EDeepSyntax_2Eeval__form@(inj__ty_2EDeepSyntax_2Edeep__form @ V0f))@(inj__ty_2Einteger_2Eint @ V2x))) <=> (p@(ap@(ap@c_2EDeepSyntax_2Eeval__form@(ap@c_2EDeepSyntax_2Eposinf@(inj__ty_2EDeepSyntax_2Edeep__form @ V0f)))@(inj__ty_2Einteger_2Eint @ V2x))))))))).
thf(ax_thm_2EDeepSyntax_2Ealldivide__def,axiom,(( ! [V0f1:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V1f2:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V2d:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2EDeepSyntax_2Ealldivide@(ap@(ap@c_2EDeepSyntax_2EConjn@(inj__ty_2EDeepSyntax_2Edeep__form @ V0f1))@(inj__ty_2EDeepSyntax_2Edeep__form @ V1f2)))@(inj__ty_2Einteger_2Eint @ V2d))) <=> ((p@(ap@(ap@c_2EDeepSyntax_2Ealldivide@(inj__ty_2EDeepSyntax_2Edeep__form @ V0f1))@(inj__ty_2Einteger_2Eint @ V2d))) & (p@(ap@(ap@c_2EDeepSyntax_2Ealldivide@(inj__ty_2EDeepSyntax_2Edeep__form @ V1f2))@(inj__ty_2Einteger_2Eint @ V2d)))))))) & (( ! [V3f1:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V4f2:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V5d:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2EDeepSyntax_2Ealldivide@(ap@(ap@c_2EDeepSyntax_2EDisjn@(inj__ty_2EDeepSyntax_2Edeep__form @ V3f1))@(inj__ty_2EDeepSyntax_2Edeep__form @ V4f2)))@(inj__ty_2Einteger_2Eint @ V5d))) <=> ((p@(ap@(ap@c_2EDeepSyntax_2Ealldivide@(inj__ty_2EDeepSyntax_2Edeep__form @ V3f1))@(inj__ty_2Einteger_2Eint @ V5d))) & (p@(ap@(ap@c_2EDeepSyntax_2Ealldivide@(inj__ty_2EDeepSyntax_2Edeep__form @ V4f2))@(inj__ty_2Einteger_2Eint @ V5d)))))))) & (( ! [V6f:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V7d:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2EDeepSyntax_2Ealldivide@(ap@c_2EDeepSyntax_2ENegn@(inj__ty_2EDeepSyntax_2Edeep__form @ V6f)))@(inj__ty_2Einteger_2Eint @ V7d))) <=> (p@(ap@(ap@c_2EDeepSyntax_2Ealldivide@(inj__ty_2EDeepSyntax_2Edeep__form @ V6f))@(inj__ty_2Einteger_2Eint @ V7d)))))) & (( ! [V8b:$i] : ((mem@V8b@bool) => ( ! [V9d:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2EDeepSyntax_2Ealldivide@(ap@c_2EDeepSyntax_2EUnrelatedBool@V8b))@(inj__ty_2Einteger_2Eint @ V9d))) <=> $true)))) & (( ! [V10i:tp__ty_2Einteger_2Eint] : ( ! [V11d:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2EDeepSyntax_2Ealldivide@(ap@c_2EDeepSyntax_2ExLT@(inj__ty_2Einteger_2Eint @ V10i)))@(inj__ty_2Einteger_2Eint @ V11d))) <=> $true))) & (( ! [V12i:tp__ty_2Einteger_2Eint] : ( ! [V13d:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2EDeepSyntax_2Ealldivide@(ap@c_2EDeepSyntax_2ELTx@(inj__ty_2Einteger_2Eint @ V12i)))@(inj__ty_2Einteger_2Eint @ V13d))) <=> $true))) & (( ! [V14i:tp__ty_2Einteger_2Eint] : ( ! [V15d:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2EDeepSyntax_2Ealldivide@(ap@c_2EDeepSyntax_2ExEQ@(inj__ty_2Einteger_2Eint @ V14i)))@(inj__ty_2Einteger_2Eint @ V15d))) <=> $true))) & ( ! [V16i1:tp__ty_2Einteger_2Eint] : ( ! [V17i2:tp__ty_2Einteger_2Eint] : ( ! [V18d:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2EDeepSyntax_2Ealldivide@(ap@(ap@c_2EDeepSyntax_2ExDivided@(inj__ty_2Einteger_2Eint @ V16i1))@(inj__ty_2Einteger_2Eint @ V17i2)))@(inj__ty_2Einteger_2Eint @ V18d))) <=> (p@(ap@(ap@c_2Einteger_2Eint__divides@(inj__ty_2Einteger_2Eint @ V16i1))@(inj__ty_2Einteger_2Eint @ V18d))))))))))))))).
thf(conj_thm_2EDeepSyntax_2Eadd__d__neginf,lemma,( ! [V0f:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V1x:tp__ty_2Einteger_2Eint] : ( ! [V2y:tp__ty_2Einteger_2Eint] : ( ! [V3d:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2EDeepSyntax_2Ealldivide@(inj__ty_2EDeepSyntax_2Edeep__form @ V0f))@(inj__ty_2Einteger_2Eint @ V3d))) => ((p@(ap@(ap@c_2EDeepSyntax_2Eeval__form@(ap@c_2EDeepSyntax_2Eneginf@(inj__ty_2EDeepSyntax_2Edeep__form @ V0f)))@(inj__ty_2Einteger_2Eint @ V1x))) <=> (p@(ap@(ap@c_2EDeepSyntax_2Eeval__form@(ap@c_2EDeepSyntax_2Eneginf@(inj__ty_2EDeepSyntax_2Edeep__form @ V0f)))@(ap@(ap@c_2Einteger_2Eint__add@(inj__ty_2Einteger_2Eint @ V1x))@(ap@(ap@c_2Einteger_2Eint__mul@(inj__ty_2Einteger_2Eint @ V2y))@(inj__ty_2Einteger_2Eint @ V3d)))))))))))).
thf(conj_thm_2EDeepSyntax_2Eadd__d__posinf,lemma,( ! [V0f:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V1x:tp__ty_2Einteger_2Eint] : ( ! [V2y:tp__ty_2Einteger_2Eint] : ( ! [V3d:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2EDeepSyntax_2Ealldivide@(inj__ty_2EDeepSyntax_2Edeep__form @ V0f))@(inj__ty_2Einteger_2Eint @ V3d))) => ((p@(ap@(ap@c_2EDeepSyntax_2Eeval__form@(ap@c_2EDeepSyntax_2Eposinf@(inj__ty_2EDeepSyntax_2Edeep__form @ V0f)))@(inj__ty_2Einteger_2Eint @ V1x))) <=> (p@(ap@(ap@c_2EDeepSyntax_2Eeval__form@(ap@c_2EDeepSyntax_2Eposinf@(inj__ty_2EDeepSyntax_2Edeep__form @ V0f)))@(ap@(ap@c_2Einteger_2Eint__add@(inj__ty_2Einteger_2Eint @ V1x))@(ap@(ap@c_2Einteger_2Eint__mul@(inj__ty_2Einteger_2Eint @ V2y))@(inj__ty_2Einteger_2Eint @ V3d)))))))))))).
thf(conj_thm_2EDeepSyntax_2Eneginf__disj1__implies__exoriginal,conjecture,( ! [V0f:tp__ty_2EDeepSyntax_2Edeep__form] : ( ! [V1d:tp__ty_2Einteger_2Eint] : ( ! [V2i:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2EDeepSyntax_2Ealldivide@(inj__ty_2EDeepSyntax_2Edeep__form @ V0f))@(inj__ty_2Einteger_2Eint @ V1d))) => (((p@(ap@(ap@c_2Einteger_2Eint__lt@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(inj__ty_2Einteger_2Eint @ V2i))) & ((p@(ap@(ap@c_2Einteger_2Eint__le@(inj__ty_2Einteger_2Eint @ V2i))@(inj__ty_2Einteger_2Eint @ V1d))) & (p@(ap@(ap@c_2EDeepSyntax_2Eeval__form@(ap@c_2EDeepSyntax_2Eneginf@(inj__ty_2EDeepSyntax_2Edeep__form @ V0f)))@(inj__ty_2Einteger_2Eint @ V2i))))) => (? [V3x:tp__ty_2Einteger_2Eint] : (p@(ap@(ap@c_2EDeepSyntax_2Eeval__form@(inj__ty_2EDeepSyntax_2Edeep__form @ V0f))@(inj__ty_2Einteger_2Eint @ V3x)))))))))).
