include('Axioms/int_arith^2.ax').
thf(tp_c_2EOmega_2EMAP2,type,(c_2EOmega_2EMAP2:(del>(del>$i)))).
thf(mem_c_2EOmega_2EMAP2,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2EOmega_2EMAP2@A_27a@A_27b)@(arr@A_27b@(arr@(arr@A_27b@(arr@A_27b@A_27a))@(arr@(ty_2Elist_2Elist@A_27b)@(arr@(ty_2Elist_2Elist@A_27b)@(ty_2Elist_2Elist@A_27a))))))))).
thf(stp_c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint,type,(tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint : $tType)).
thf(stp_inj_c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint,type,(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint : (tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint > $i))).
thf(stp_surj_c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint,type,(surj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint : ($i > tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint))).
thf(stp_inj_surj_c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint,axiom,( ! [X:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ((surj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ (inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ X)) = X))).
thf(stp_inj_mem_c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint,axiom,( ! [X:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : (mem @ (inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ X) @ (ty_2Elist_2Elist@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))))).
thf(stp_iso_mem_c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Elist_2Elist@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))) => (X = (inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ (surj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ X)))))).
thf(stp_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint,type,(tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint : $tType)).
thf(stp_inj_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint,type,(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint : (tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint > $i))).
thf(stp_surj_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint,type,(surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint : ($i > tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint))).
thf(stp_inj_surj_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint,axiom,( ! [X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ((surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ (inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ X)) = X))).
thf(stp_inj_mem_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint,axiom,( ! [X:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : (mem @ (inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ X) @ (ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint)))).
thf(stp_iso_mem_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint)) => (X = (inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ (surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ X)))))).
thf(tp_c_2EOmega_2Ecalc__nightmare,type,(c_2EOmega_2Ecalc__nightmare:$i)).
thf(mem_c_2EOmega_2Ecalc__nightmare,axiom,(mem@c_2EOmega_2Ecalc__nightmare@(arr@ty_2Einteger_2Eint@(arr@ty_2Enum_2Enum@(arr@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@bool))))).
thf(tp_c_2EOmega_2Edark__shadow,type,(c_2EOmega_2Edark__shadow:$i)).
thf(mem_c_2EOmega_2Edark__shadow,axiom,(mem@c_2EOmega_2Edark__shadow@(arr@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(arr@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@bool)))).
thf(tp_c_2EOmega_2Edark__shadow__cond__row,type,(c_2EOmega_2Edark__shadow__cond__row:$i)).
thf(mem_c_2EOmega_2Edark__shadow__cond__row,axiom,(mem@c_2EOmega_2Edark__shadow__cond__row@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(arr@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@bool)))).
thf(tp_c_2EOmega_2Edark__shadow__condition,type,(c_2EOmega_2Edark__shadow__condition:$i)).
thf(mem_c_2EOmega_2Edark__shadow__condition,axiom,(mem@c_2EOmega_2Edark__shadow__condition@(arr@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(arr@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@bool)))).
thf(tp_c_2EOmega_2Edark__shadow__row,type,(c_2EOmega_2Edark__shadow__row:$i)).
thf(mem_c_2EOmega_2Edark__shadow__row,axiom,(mem@c_2EOmega_2Edark__shadow__row@(arr@ty_2Enum_2Enum@(arr@ty_2Einteger_2Eint@(arr@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@bool))))).
thf(tp_c_2EOmega_2Eevallower,type,(c_2EOmega_2Eevallower:$i)).
thf(mem_c_2EOmega_2Eevallower,axiom,(mem@c_2EOmega_2Eevallower@(arr@ty_2Einteger_2Eint@(arr@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@bool)))).
thf(tp_c_2EOmega_2Eevalupper,type,(c_2EOmega_2Eevalupper:$i)).
thf(mem_c_2EOmega_2Eevalupper,axiom,(mem@c_2EOmega_2Eevalupper@(arr@ty_2Einteger_2Eint@(arr@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@bool)))).
thf(tp_c_2EOmega_2Efst1,type,(c_2EOmega_2Efst1:(del>$i))).
thf(mem_c_2EOmega_2Efst1,axiom,( ! [A_27a:del] : (mem@(c_2EOmega_2Efst1@A_27a)@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@A_27a)@bool)))).
thf(tp_c_2EOmega_2Efst__nzero,type,(c_2EOmega_2Efst__nzero:(del>$i))).
thf(mem_c_2EOmega_2Efst__nzero,axiom,( ! [A_27a:del] : (mem@(c_2EOmega_2Efst__nzero@A_27a)@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@A_27a)@bool)))).
thf(tp_c_2EOmega_2Emodhat,type,(c_2EOmega_2Emodhat:$i)).
thf(mem_c_2EOmega_2Emodhat,axiom,(mem@c_2EOmega_2Emodhat@(arr@ty_2Einteger_2Eint@(arr@ty_2Einteger_2Eint@ty_2Einteger_2Eint)))).
thf(stp_fo_c_2EOmega_2Emodhat,type,(fo__c_2EOmega_2Emodhat:(tp__ty_2Einteger_2Eint > (tp__ty_2Einteger_2Eint > tp__ty_2Einteger_2Eint)))).
thf(stp_eq_fo_c_2EOmega_2Emodhat,axiom,( ! [X0:tp__ty_2Einteger_2Eint] : ( ! [X1:tp__ty_2Einteger_2Eint] : ((inj__ty_2Einteger_2Eint @ ((fo__c_2EOmega_2Emodhat @ X0) @ X1)) = (ap @ (ap @ c_2EOmega_2Emodhat @ (inj__ty_2Einteger_2Eint @ X0)) @ (inj__ty_2Einteger_2Eint @ X1)))))).
thf(tp_c_2EOmega_2Enightmare,type,(c_2EOmega_2Enightmare:$i)).
thf(mem_c_2EOmega_2Enightmare,axiom,(mem@c_2EOmega_2Enightmare@(arr@ty_2Einteger_2Eint@(arr@ty_2Enum_2Enum@(arr@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(arr@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(arr@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@bool))))))).
thf(tp_c_2EOmega_2Ereal__shadow,type,(c_2EOmega_2Ereal__shadow:$i)).
thf(mem_c_2EOmega_2Ereal__shadow,axiom,(mem@c_2EOmega_2Ereal__shadow@(arr@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(arr@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@bool)))).
thf(tp_c_2EOmega_2Ershadow__row,type,(c_2EOmega_2Ershadow__row:$i)).
thf(mem_c_2EOmega_2Ershadow__row,axiom,(mem@c_2EOmega_2Ershadow__row@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(arr@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@bool)))).
thf(stp_c_ty_2Elist_2Elist_ty_2Einteger_2Eint,type,(tp__c_ty_2Elist_2Elist_ty_2Einteger_2Eint : $tType)).
thf(stp_inj_c_ty_2Elist_2Elist_ty_2Einteger_2Eint,type,(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint : (tp__c_ty_2Elist_2Elist_ty_2Einteger_2Eint > $i))).
thf(stp_surj_c_ty_2Elist_2Elist_ty_2Einteger_2Eint,type,(surj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint : ($i > tp__c_ty_2Elist_2Elist_ty_2Einteger_2Eint))).
thf(stp_inj_surj_c_ty_2Elist_2Elist_ty_2Einteger_2Eint,axiom,( ! [X:tp__c_ty_2Elist_2Elist_ty_2Einteger_2Eint] : ((surj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ (inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ X)) = X))).
thf(stp_inj_mem_c_ty_2Elist_2Elist_ty_2Einteger_2Eint,axiom,( ! [X:tp__c_ty_2Elist_2Elist_ty_2Einteger_2Eint] : (mem @ (inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ X) @ (ty_2Elist_2Elist@ty_2Einteger_2Eint)))).
thf(stp_iso_mem_c_ty_2Elist_2Elist_ty_2Einteger_2Eint,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Elist_2Elist@ty_2Einteger_2Eint)) => (X = (inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ (surj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ X)))))).
thf(tp_c_2EOmega_2Esumc,type,(c_2EOmega_2Esumc:$i)).
thf(mem_c_2EOmega_2Esumc,axiom,(mem@c_2EOmega_2Esumc@(arr@(ty_2Elist_2Elist@ty_2Einteger_2Eint)@(arr@(ty_2Elist_2Elist@ty_2Einteger_2Eint)@ty_2Einteger_2Eint)))).
thf(stp_fo_c_2EOmega_2Esumc,type,(fo__c_2EOmega_2Esumc:(tp__c_ty_2Elist_2Elist_ty_2Einteger_2Eint > (tp__c_ty_2Elist_2Elist_ty_2Einteger_2Eint > tp__ty_2Einteger_2Eint)))).
thf(stp_eq_fo_c_2EOmega_2Esumc,axiom,( ! [X0:tp__c_ty_2Elist_2Elist_ty_2Einteger_2Eint] : ( ! [X1:tp__c_ty_2Elist_2Elist_ty_2Einteger_2Eint] : ((inj__ty_2Einteger_2Eint @ ((fo__c_2EOmega_2Esumc @ X0) @ X1)) = (ap @ (ap @ c_2EOmega_2Esumc @ (inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ X0)) @ (inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ X1)))))).
thf(conj_thm_2EOmega_2EMAP2__ind,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27b@(arr@(arr@A_27b@(arr@A_27b@A_27a))@(arr@(ty_2Elist_2Elist@A_27b)@(arr@(ty_2Elist_2Elist@A_27b)@bool))))) => ((( ! [V1pad:$i] : ((mem@V1pad@A_27b) => ( ! [V2f:$i] : ((mem@V2f@(arr@A_27b@(arr@A_27b@A_27a))) => (p@(ap@(ap@(ap@(ap@V0P@V1pad)@V2f)@(c_2Elist_2ENIL@A_27b))@(c_2Elist_2ENIL@A_27b))))))) & (( ! [V3pad:$i] : ((mem@V3pad@A_27b) => ( ! [V4f:$i] : ((mem@V4f@(arr@A_27b@(arr@A_27b@A_27a))) => ( ! [V5y:$i] : ((mem@V5y@A_27b) => ( ! [V6ys:$i] : ((mem@V6ys@(ty_2Elist_2Elist@A_27b)) => ((p@(ap@(ap@(ap@(ap@V0P@V3pad)@V4f)@(c_2Elist_2ENIL@A_27b))@V6ys)) => (p@(ap@(ap@(ap@(ap@V0P@V3pad)@V4f)@(c_2Elist_2ENIL@A_27b))@(ap@(ap@(c_2Elist_2ECONS@A_27b)@V5y)@V6ys)))))))))))) & (( ! [V7pad:$i] : ((mem@V7pad@A_27b) => ( ! [V8f:$i] : ((mem@V8f@(arr@A_27b@(arr@A_27b@A_27a))) => ( ! [V9x:$i] : ((mem@V9x@A_27b) => ( ! [V10xs:$i] : ((mem@V10xs@(ty_2Elist_2Elist@A_27b)) => ((p@(ap@(ap@(ap@(ap@V0P@V7pad)@V8f)@V10xs)@(c_2Elist_2ENIL@A_27b))) => (p@(ap@(ap@(ap@(ap@V0P@V7pad)@V8f)@(ap@(ap@(c_2Elist_2ECONS@A_27b)@V9x)@V10xs))@(c_2Elist_2ENIL@A_27b)))))))))))) & ( ! [V11pad:$i] : ((mem@V11pad@A_27b) => ( ! [V12f:$i] : ((mem@V12f@(arr@A_27b@(arr@A_27b@A_27a))) => ( ! [V13x:$i] : ((mem@V13x@A_27b) => ( ! [V14xs:$i] : ((mem@V14xs@(ty_2Elist_2Elist@A_27b)) => ( ! [V15y:$i] : ((mem@V15y@A_27b) => ( ! [V16ys:$i] : ((mem@V16ys@(ty_2Elist_2Elist@A_27b)) => ((p@(ap@(ap@(ap@(ap@V0P@V11pad)@V12f)@V14xs)@V16ys)) => (p@(ap@(ap@(ap@(ap@V0P@V11pad)@V12f)@(ap@(ap@(c_2Elist_2ECONS@A_27b)@V13x)@V14xs))@(ap@(ap@(c_2Elist_2ECONS@A_27b)@V15y)@V16ys))))))))))))))))))) => ( ! [V17v:$i] : ((mem@V17v@A_27b) => ( ! [V18v1:$i] : ((mem@V18v1@(arr@A_27b@(arr@A_27b@A_27a))) => ( ! [V19v2:$i] : ((mem@V19v2@(ty_2Elist_2Elist@A_27b)) => ( ! [V20v3:$i] : ((mem@V20v3@(ty_2Elist_2Elist@A_27b)) => (p@(ap@(ap@(ap@(ap@V0P@V17v)@V18v1)@V19v2)@V20v3)))))))))))))))).
thf(conj_thm_2EOmega_2EMAP2__def,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0pad:$i] : ((mem@V0pad@A_27b) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27b@(arr@A_27b@A_27a))) => ((ap@(ap@(ap@(ap@(c_2EOmega_2EMAP2@A_27a@A_27b)@V0pad)@V1f)@(c_2Elist_2ENIL@A_27b))@(c_2Elist_2ENIL@A_27b)) = (c_2Elist_2ENIL@A_27a)))))) & (( ! [V2ys:$i] : ((mem@V2ys@(ty_2Elist_2Elist@A_27b)) => ( ! [V3y:$i] : ((mem@V3y@A_27b) => ( ! [V4pad:$i] : ((mem@V4pad@A_27b) => ( ! [V5f:$i] : ((mem@V5f@(arr@A_27b@(arr@A_27b@A_27a))) => ((ap@(ap@(ap@(ap@(c_2EOmega_2EMAP2@A_27a@A_27b)@V4pad)@V5f)@(c_2Elist_2ENIL@A_27b))@(ap@(ap@(c_2Elist_2ECONS@A_27b)@V3y)@V2ys)) = (ap@(ap@(c_2Elist_2ECONS@A_27a)@(ap@(ap@V5f@V4pad)@V3y))@(ap@(ap@(ap@(ap@(c_2EOmega_2EMAP2@A_27a@A_27b)@V4pad)@V5f)@(c_2Elist_2ENIL@A_27b))@V2ys))))))))))) & (( ! [V6xs:$i] : ((mem@V6xs@(ty_2Elist_2Elist@A_27b)) => ( ! [V7x:$i] : ((mem@V7x@A_27b) => ( ! [V8pad:$i] : ((mem@V8pad@A_27b) => ( ! [V9f:$i] : ((mem@V9f@(arr@A_27b@(arr@A_27b@A_27a))) => ((ap@(ap@(ap@(ap@(c_2EOmega_2EMAP2@A_27a@A_27b)@V8pad)@V9f)@(ap@(ap@(c_2Elist_2ECONS@A_27b)@V7x)@V6xs))@(c_2Elist_2ENIL@A_27b)) = (ap@(ap@(c_2Elist_2ECONS@A_27a)@(ap@(ap@V9f@V7x)@V8pad))@(ap@(ap@(ap@(ap@(c_2EOmega_2EMAP2@A_27a@A_27b)@V8pad)@V9f)@V6xs)@(c_2Elist_2ENIL@A_27b)))))))))))) & ( ! [V10ys:$i] : ((mem@V10ys@(ty_2Elist_2Elist@A_27b)) => ( ! [V11y:$i] : ((mem@V11y@A_27b) => ( ! [V12xs:$i] : ((mem@V12xs@(ty_2Elist_2Elist@A_27b)) => ( ! [V13x:$i] : ((mem@V13x@A_27b) => ( ! [V14pad:$i] : ((mem@V14pad@A_27b) => ( ! [V15f:$i] : ((mem@V15f@(arr@A_27b@(arr@A_27b@A_27a))) => ((ap@(ap@(ap@(ap@(c_2EOmega_2EMAP2@A_27a@A_27b)@V14pad)@V15f)@(ap@(ap@(c_2Elist_2ECONS@A_27b)@V13x)@V12xs))@(ap@(ap@(c_2Elist_2ECONS@A_27b)@V11y)@V10ys)) = (ap@(ap@(c_2Elist_2ECONS@A_27a)@(ap@(ap@V15f@V13x)@V11y))@(ap@(ap@(ap@(ap@(c_2EOmega_2EMAP2@A_27a@A_27b)@V14pad)@V15f)@V12xs)@V10ys))))))))))))))))))))).
thf(conj_thm_2EOmega_2EMAP2__zero__ADD,lemma,( ! [V0xs:tp__c_ty_2Elist_2Elist_ty_2Einteger_2Eint] : (((surj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ (ap@(ap@(ap@(ap@(c_2EOmega_2EMAP2@ty_2Einteger_2Eint@ty_2Einteger_2Eint)@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@c_2Einteger_2Eint__add)@(c_2Elist_2ENIL@ty_2Einteger_2Eint))@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V0xs))) = V0xs) & ((surj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ (ap@(ap@(ap@(ap@(c_2EOmega_2EMAP2@ty_2Einteger_2Eint@ty_2Einteger_2Eint)@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@c_2Einteger_2Eint__add)@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V0xs))@(c_2Elist_2ENIL@ty_2Einteger_2Eint))) = V0xs)))).
thf(conj_thm_2EOmega_2Esumc__ind,lemma,( ! [V0P:$i] : ((mem@V0P@(arr@(ty_2Elist_2Elist@ty_2Einteger_2Eint)@(arr@(ty_2Elist_2Elist@ty_2Einteger_2Eint)@bool))) => ((( ! [V1v0:tp__c_ty_2Elist_2Elist_ty_2Einteger_2Eint] : (p@(ap@(ap@V0P@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V1v0))@(c_2Elist_2ENIL@ty_2Einteger_2Eint)))) & (( ! [V2v4:tp__ty_2Einteger_2Eint] : ( ! [V3v5:tp__c_ty_2Elist_2Elist_ty_2Einteger_2Eint] : (p@(ap@(ap@V0P@(c_2Elist_2ENIL@ty_2Einteger_2Eint))@(ap@(ap@(c_2Elist_2ECONS@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V2v4))@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V3v5)))))) & ( ! [V4c:tp__ty_2Einteger_2Eint] : ( ! [V5cs:tp__c_ty_2Elist_2Elist_ty_2Einteger_2Eint] : ( ! [V6v:tp__ty_2Einteger_2Eint] : ( ! [V7vs:tp__c_ty_2Elist_2Elist_ty_2Einteger_2Eint] : ((p@(ap@(ap@V0P@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V5cs))@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V7vs))) => (p@(ap@(ap@V0P@(ap@(ap@(c_2Elist_2ECONS@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V4c))@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V5cs)))@(ap@(ap@(c_2Elist_2ECONS@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V6v))@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V7vs))))))))))) => ( ! [V8v:tp__c_ty_2Elist_2Elist_ty_2Einteger_2Eint] : ( ! [V9v1:tp__c_ty_2Elist_2Elist_ty_2Einteger_2Eint] : (p@(ap@(ap@V0P@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V8v))@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V9v1))))))))).
thf(conj_thm_2EOmega_2Esumc__def,lemma,(( ! [V0v0:tp__c_ty_2Elist_2Elist_ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint @ (ap@(ap@c_2EOmega_2Esumc@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V0v0))@(c_2Elist_2ENIL@ty_2Einteger_2Eint))) = (surj__ty_2Einteger_2Eint @ (ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))) & (( ! [V1v5:tp__c_ty_2Elist_2Elist_ty_2Einteger_2Eint] : ( ! [V2v4:tp__ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint @ (ap@(ap@c_2EOmega_2Esumc@(c_2Elist_2ENIL@ty_2Einteger_2Eint))@(ap@(ap@(c_2Elist_2ECONS@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V2v4))@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V1v5)))) = (surj__ty_2Einteger_2Eint @ (ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))))) & ( ! [V3vs:tp__c_ty_2Elist_2Elist_ty_2Einteger_2Eint] : ( ! [V4v:tp__ty_2Einteger_2Eint] : ( ! [V5cs:tp__c_ty_2Elist_2Elist_ty_2Einteger_2Eint] : ( ! [V6c:tp__ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint @ (ap@(ap@c_2EOmega_2Esumc@(ap@(ap@(c_2Elist_2ECONS@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V6c))@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V5cs)))@(ap@(ap@(c_2Elist_2ECONS@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V4v))@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V3vs)))) = (surj__ty_2Einteger_2Eint @ (ap@(ap@c_2Einteger_2Eint__add@(ap@(ap@c_2Einteger_2Eint__mul@(inj__ty_2Einteger_2Eint @ V6c))@(inj__ty_2Einteger_2Eint @ V4v)))@(ap@(ap@c_2EOmega_2Esumc@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V5cs))@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V3vs)))))))))))).
thf(conj_thm_2EOmega_2Esumc__thm,lemma,( ! [V0cs:tp__c_ty_2Elist_2Elist_ty_2Einteger_2Eint] : ( ! [V1vs:tp__c_ty_2Elist_2Elist_ty_2Einteger_2Eint] : ( ! [V2c:tp__ty_2Einteger_2Eint] : ( ! [V3v:tp__ty_2Einteger_2Eint] : (((surj__ty_2Einteger_2Eint @ (ap@(ap@c_2EOmega_2Esumc@(c_2Elist_2ENIL@ty_2Einteger_2Eint))@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V1vs))) = (surj__ty_2Einteger_2Eint @ (ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) & (((surj__ty_2Einteger_2Eint @ (ap@(ap@c_2EOmega_2Esumc@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V0cs))@(c_2Elist_2ENIL@ty_2Einteger_2Eint))) = (surj__ty_2Einteger_2Eint @ (ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) & ((surj__ty_2Einteger_2Eint @ (ap@(ap@c_2EOmega_2Esumc@(ap@(ap@(c_2Elist_2ECONS@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V2c))@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V0cs)))@(ap@(ap@(c_2Elist_2ECONS@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V3v))@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V1vs)))) = (surj__ty_2Einteger_2Eint @ (ap@(ap@c_2Einteger_2Eint__add@(ap@(ap@c_2Einteger_2Eint__mul@(inj__ty_2Einteger_2Eint @ V2c))@(inj__ty_2Einteger_2Eint @ V3v)))@(ap@(ap@c_2EOmega_2Esumc@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V0cs))@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V1vs)))))))))))).
thf(conj_thm_2EOmega_2Esumc__ADD,lemma,( ! [V0cs:tp__c_ty_2Elist_2Elist_ty_2Einteger_2Eint] : ( ! [V1vs:tp__c_ty_2Elist_2Elist_ty_2Einteger_2Eint] : ( ! [V2ds:tp__c_ty_2Elist_2Elist_ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint @ (ap@(ap@c_2Einteger_2Eint__add@(ap@(ap@c_2EOmega_2Esumc@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V0cs))@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V1vs)))@(ap@(ap@c_2EOmega_2Esumc@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V2ds))@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V1vs)))) = (surj__ty_2Einteger_2Eint @ (ap@(ap@c_2EOmega_2Esumc@(ap@(ap@(ap@(ap@(c_2EOmega_2EMAP2@ty_2Einteger_2Eint@ty_2Einteger_2Eint)@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@c_2Einteger_2Eint__add)@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V0cs))@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V2ds)))@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V1vs)))))))).
thf(conj_thm_2EOmega_2Esumc__MULT,lemma,( ! [V0cs:tp__c_ty_2Elist_2Elist_ty_2Einteger_2Eint] : ( ! [V1vs:tp__c_ty_2Elist_2Elist_ty_2Einteger_2Eint] : ( ! [V2f:tp__ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint @ (ap@(ap@c_2Einteger_2Eint__mul@(inj__ty_2Einteger_2Eint @ V2f))@(ap@(ap@c_2EOmega_2Esumc@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V0cs))@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V1vs)))) = (surj__ty_2Einteger_2Eint @ (ap@(ap@c_2EOmega_2Esumc@(ap@(ap@(c_2Elist_2EMAP@ty_2Einteger_2Eint@ty_2Einteger_2Eint)@(lam@ty_2Einteger_2Eint@(^ [V3x:$i] : (ap@(ap@c_2Einteger_2Eint__mul@(inj__ty_2Einteger_2Eint @ V2f))@V3x))))@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V0cs)))@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V1vs)))))))).
thf(conj_thm_2EOmega_2Esumc__singleton,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Einteger_2Eint@ty_2Einteger_2Eint)) => ( ! [V1c:tp__ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint @ (ap@(ap@c_2EOmega_2Esumc@(ap@(ap@(c_2Elist_2EMAP@ty_2Einteger_2Eint@ty_2Einteger_2Eint)@V0f)@(ap@(ap@(c_2Elist_2ECONS@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V1c))@(c_2Elist_2ENIL@ty_2Einteger_2Eint))))@(ap@(ap@(c_2Elist_2ECONS@ty_2Einteger_2Eint)@(ap@c_2Einteger_2Eint__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(c_2Elist_2ENIL@ty_2Einteger_2Eint)))) = (surj__ty_2Einteger_2Eint @ (ap@V0f@(inj__ty_2Einteger_2Eint @ V1c)))))))).
thf(conj_thm_2EOmega_2Esumc__nonsingle,lemma,( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Einteger_2Eint@ty_2Einteger_2Eint)) => ( ! [V1cs:tp__c_ty_2Elist_2Elist_ty_2Einteger_2Eint] : ( ! [V2c:tp__ty_2Einteger_2Eint] : ( ! [V3v:tp__ty_2Einteger_2Eint] : ( ! [V4vs:tp__c_ty_2Elist_2Elist_ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint @ (ap@(ap@c_2EOmega_2Esumc@(ap@(ap@(c_2Elist_2EMAP@ty_2Einteger_2Eint@ty_2Einteger_2Eint)@V0f)@(ap@(ap@(c_2Elist_2ECONS@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V2c))@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V1cs))))@(ap@(ap@(c_2Elist_2ECONS@ty_2Einteger_2Eint)@(inj__ty_2Einteger_2Eint @ V3v))@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V4vs)))) = (surj__ty_2Einteger_2Eint @ (ap@(ap@c_2Einteger_2Eint__add@(ap@(ap@c_2Einteger_2Eint__mul@(ap@V0f@(inj__ty_2Einteger_2Eint @ V2c)))@(inj__ty_2Einteger_2Eint @ V3v)))@(ap@(ap@c_2EOmega_2Esumc@(ap@(ap@(c_2Elist_2EMAP@ty_2Einteger_2Eint@ty_2Einteger_2Eint)@V0f)@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V1cs)))@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V4vs)))))))))))).
thf(ax_thm_2EOmega_2Emodhat__def,axiom,( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1y:tp__ty_2Einteger_2Eint] : ((surj__ty_2Einteger_2Eint @ (ap@(ap@c_2EOmega_2Emodhat@(inj__ty_2Einteger_2Eint @ V0x))@(inj__ty_2Einteger_2Eint @ V1y))) = (surj__ty_2Einteger_2Eint @ (ap@(ap@c_2Einteger_2Eint__sub@(inj__ty_2Einteger_2Eint @ V0x))@(ap@(ap@c_2Einteger_2Eint__mul@(inj__ty_2Einteger_2Eint @ V1y))@(ap@(ap@c_2Einteger_2Eint__div@(ap@(ap@c_2Einteger_2Eint__add@(ap@(ap@c_2Einteger_2Eint__mul@(ap@c_2Einteger_2Eint__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(inj__ty_2Einteger_2Eint @ V0x)))@(inj__ty_2Einteger_2Eint @ V1y)))@(ap@(ap@c_2Einteger_2Eint__mul@(ap@c_2Einteger_2Eint__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(inj__ty_2Einteger_2Eint @ V1y)))))))))).
thf(conj_thm_2EOmega_2Eequality__removal,lemma,( ! [V0c:tp__ty_2Einteger_2Eint] : ( ! [V1x:tp__ty_2Einteger_2Eint] : ( ! [V2cs:tp__c_ty_2Elist_2Elist_ty_2Einteger_2Eint] : ( ! [V3vs:tp__c_ty_2Elist_2Elist_ty_2Einteger_2Eint] : ((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 @ V0c))) => (((surj__ty_2Einteger_2Eint @ (ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) = (surj__ty_2Einteger_2Eint @ (ap@(ap@c_2Einteger_2Eint__add@(ap@(ap@c_2Einteger_2Eint__mul@(inj__ty_2Einteger_2Eint @ V0c))@(inj__ty_2Einteger_2Eint @ V1x)))@(ap@(ap@c_2EOmega_2Esumc@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V2cs))@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V3vs))))) <=> (? [V4s:tp__ty_2Einteger_2Eint] : ((V1x = (surj__ty_2Einteger_2Eint @ (ap@(ap@c_2Einteger_2Eint__add@(ap@(ap@c_2Einteger_2Eint__mul@(ap@c_2Einteger_2Eint__neg@(ap@(ap@c_2Einteger_2Eint__add@(inj__ty_2Einteger_2Eint @ V0c))@(ap@c_2Einteger_2Eint__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))@(inj__ty_2Einteger_2Eint @ V4s)))@(ap@(ap@c_2EOmega_2Esumc@(ap@(ap@(c_2Elist_2EMAP@ty_2Einteger_2Eint@ty_2Einteger_2Eint)@(lam@ty_2Einteger_2Eint@(^ [V5x:$i] : (ap@(ap@c_2EOmega_2Emodhat@V5x)@(ap@(ap@c_2Einteger_2Eint__add@(inj__ty_2Einteger_2Eint @ V0c))@(ap@c_2Einteger_2Eint__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V2cs)))@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V3vs))))) & ((surj__ty_2Einteger_2Eint @ (ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) = (surj__ty_2Einteger_2Eint @ (ap@(ap@c_2Einteger_2Eint__add@(ap@(ap@c_2Einteger_2Eint__mul@(inj__ty_2Einteger_2Eint @ V0c))@(inj__ty_2Einteger_2Eint @ V1x)))@(ap@(ap@c_2EOmega_2Esumc@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V2cs))@(inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint @ V3vs)))))))))))))).
thf(conj_thm_2EOmega_2Eevalupper__ind,lemma,( ! [V0P:$i] : ((mem@V0P@(arr@ty_2Einteger_2Eint@(arr@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@bool))) => ((( ! [V1x:tp__ty_2Einteger_2Eint] : (p@(ap@(ap@V0P@(inj__ty_2Einteger_2Eint @ V1x))@(c_2Elist_2ENIL@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))))) & ( ! [V2x:tp__ty_2Einteger_2Eint] : ( ! [V3c:tp__ty_2Enum_2Enum] : ( ! [V4y:tp__ty_2Einteger_2Eint] : ( ! [V5cs:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ((p@(ap@(ap@V0P@(inj__ty_2Einteger_2Eint @ V2x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V5cs))) => (p@(ap@(ap@V0P@(inj__ty_2Einteger_2Eint @ V2x))@(ap@(ap@(c_2Elist_2ECONS@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V3c))@(inj__ty_2Einteger_2Eint @ V4y)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V5cs)))))))))) => ( ! [V6v:tp__ty_2Einteger_2Eint] : ( ! [V7v1:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : (p@(ap@(ap@V0P@(inj__ty_2Einteger_2Eint @ V6v))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V7v1))))))))).
thf(conj_thm_2EOmega_2Eevalupper__def,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2EOmega_2Eevalupper@(inj__ty_2Einteger_2Eint @ V0x))@(c_2Elist_2ENIL@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint)))) <=> $true)) & ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2x:tp__ty_2Einteger_2Eint] : ( ! [V3cs:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V4c:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2EOmega_2Eevalupper@(inj__ty_2Einteger_2Eint @ V2x))@(ap@(ap@(c_2Elist_2ECONS@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V4c))@(inj__ty_2Einteger_2Eint @ V1y)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V3cs)))) <=> ((p@(ap@(ap@c_2Einteger_2Eint__le@(ap@(ap@c_2Einteger_2Eint__mul@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V4c)))@(inj__ty_2Einteger_2Eint @ V2x)))@(inj__ty_2Einteger_2Eint @ V1y))) & (p@(ap@(ap@c_2EOmega_2Eevalupper@(inj__ty_2Einteger_2Eint @ V2x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V3cs))))))))))).
thf(conj_thm_2EOmega_2Eevallower__ind,lemma,( ! [V0P:$i] : ((mem@V0P@(arr@ty_2Einteger_2Eint@(arr@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@bool))) => ((( ! [V1x:tp__ty_2Einteger_2Eint] : (p@(ap@(ap@V0P@(inj__ty_2Einteger_2Eint @ V1x))@(c_2Elist_2ENIL@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))))) & ( ! [V2x:tp__ty_2Einteger_2Eint] : ( ! [V3c:tp__ty_2Enum_2Enum] : ( ! [V4y:tp__ty_2Einteger_2Eint] : ( ! [V5cs:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ((p@(ap@(ap@V0P@(inj__ty_2Einteger_2Eint @ V2x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V5cs))) => (p@(ap@(ap@V0P@(inj__ty_2Einteger_2Eint @ V2x))@(ap@(ap@(c_2Elist_2ECONS@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V3c))@(inj__ty_2Einteger_2Eint @ V4y)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V5cs)))))))))) => ( ! [V6v:tp__ty_2Einteger_2Eint] : ( ! [V7v1:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : (p@(ap@(ap@V0P@(inj__ty_2Einteger_2Eint @ V6v))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V7v1))))))))).
thf(conj_thm_2EOmega_2Eevallower__def,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2EOmega_2Eevallower@(inj__ty_2Einteger_2Eint @ V0x))@(c_2Elist_2ENIL@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint)))) <=> $true)) & ( ! [V1y:tp__ty_2Einteger_2Eint] : ( ! [V2x:tp__ty_2Einteger_2Eint] : ( ! [V3cs:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V4c:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2EOmega_2Eevallower@(inj__ty_2Einteger_2Eint @ V2x))@(ap@(ap@(c_2Elist_2ECONS@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V4c))@(inj__ty_2Einteger_2Eint @ V1y)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V3cs)))) <=> ((p@(ap@(ap@c_2Einteger_2Eint__le@(inj__ty_2Einteger_2Eint @ V1y))@(ap@(ap@c_2Einteger_2Eint__mul@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V4c)))@(inj__ty_2Einteger_2Eint @ V2x)))) & (p@(ap@(ap@c_2EOmega_2Eevallower@(inj__ty_2Einteger_2Eint @ V2x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V3cs))))))))))).
thf(conj_thm_2EOmega_2Esmaller__satisfies__uppers,lemma,( ! [V0uppers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V1x:tp__ty_2Einteger_2Eint] : ( ! [V2y:tp__ty_2Einteger_2Eint] : (((p@(ap@(ap@c_2EOmega_2Eevalupper@(inj__ty_2Einteger_2Eint @ V1x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers))) & (p@(ap@(ap@c_2Einteger_2Eint__lt@(inj__ty_2Einteger_2Eint @ V2y))@(inj__ty_2Einteger_2Eint @ V1x)))) => (p@(ap@(ap@c_2EOmega_2Eevalupper@(inj__ty_2Einteger_2Eint @ V2y))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers)))))))).
thf(conj_thm_2EOmega_2Ebigger__satisfies__lowers,lemma,( ! [V0lowers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V1x:tp__ty_2Einteger_2Eint] : ( ! [V2y:tp__ty_2Einteger_2Eint] : (((p@(ap@(ap@c_2EOmega_2Eevallower@(inj__ty_2Einteger_2Eint @ V1x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0lowers))) & (p@(ap@(ap@c_2Einteger_2Eint__lt@(inj__ty_2Einteger_2Eint @ V1x))@(inj__ty_2Einteger_2Eint @ V2y)))) => (p@(ap@(ap@c_2EOmega_2Eevallower@(inj__ty_2Einteger_2Eint @ V2y))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0lowers)))))))).
thf(ax_thm_2EOmega_2Efst__nzero__def,axiom,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@(ty_2Epair_2Eprod@ty_2Enum_2Enum@A_27a)) => ((p@(ap@(c_2EOmega_2Efst__nzero@A_27a)@V0x)) <=> (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@(c_2Epair_2EFST@ty_2Enum_2Enum@A_27a)@V0x)))))))).
thf(ax_thm_2EOmega_2Efst1__def,axiom,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@(ty_2Epair_2Eprod@ty_2Enum_2Enum@A_27a)) => ((p@(ap@(c_2EOmega_2Efst1@A_27a)@V0x)) <=> ((surj__ty_2Enum_2Enum @ (ap@(c_2Epair_2EFST@ty_2Enum_2Enum@A_27a)@V0x)) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))).
thf(conj_thm_2EOmega_2Eonlylowers__satisfiable,lemma,( ! [V0lowers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ((p@(ap@(ap@(c_2Elist_2EEVERY@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(c_2EOmega_2Efst__nzero@ty_2Einteger_2Eint))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0lowers))) => (? [V1x:tp__ty_2Einteger_2Eint] : (p@(ap@(ap@c_2EOmega_2Eevallower@(inj__ty_2Einteger_2Eint @ V1x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0lowers))))))).
thf(conj_thm_2EOmega_2Eonlyuppers__satisfiable,lemma,( ! [V0uppers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ((p@(ap@(ap@(c_2Elist_2EEVERY@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(c_2EOmega_2Efst__nzero@ty_2Einteger_2Eint))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers))) => (? [V1x:tp__ty_2Einteger_2Eint] : (p@(ap@(ap@c_2EOmega_2Eevalupper@(inj__ty_2Einteger_2Eint @ V1x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers))))))).
thf(conj_thm_2EOmega_2Ershadow__row__ind,lemma,( ! [V0P:$i] : ((mem@V0P@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(arr@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@bool))) => ((( ! [V1upperc:tp__ty_2Enum_2Enum] : ( ! [V2uppery:tp__ty_2Einteger_2Eint] : (p@(ap@(ap@V0P@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V1upperc))@(inj__ty_2Einteger_2Eint @ V2uppery)))@(c_2Elist_2ENIL@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint)))))) & ( ! [V3upperc:tp__ty_2Enum_2Enum] : ( ! [V4uppery:tp__ty_2Einteger_2Eint] : ( ! [V5lowerc:tp__ty_2Enum_2Enum] : ( ! [V6lowery:tp__ty_2Einteger_2Eint] : ( ! [V7rs:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ((p@(ap@(ap@V0P@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V3upperc))@(inj__ty_2Einteger_2Eint @ V4uppery)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V7rs))) => (p@(ap@(ap@V0P@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V3upperc))@(inj__ty_2Einteger_2Eint @ V4uppery)))@(ap@(ap@(c_2Elist_2ECONS@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V5lowerc))@(inj__ty_2Einteger_2Eint @ V6lowery)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V7rs))))))))))) => ( ! [V8v:tp__ty_2Enum_2Enum] : ( ! [V9v1:tp__ty_2Einteger_2Eint] : ( ! [V10v2:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : (p@(ap@(ap@V0P@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V8v))@(inj__ty_2Einteger_2Eint @ V9v1)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V10v2)))))))))).
thf(conj_thm_2EOmega_2Ershadow__row__def,lemma,(( ! [V0uppery:tp__ty_2Einteger_2Eint] : ( ! [V1upperc:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2EOmega_2Ershadow__row@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V1upperc))@(inj__ty_2Einteger_2Eint @ V0uppery)))@(c_2Elist_2ENIL@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint)))) <=> $true))) & ( ! [V2uppery:tp__ty_2Einteger_2Eint] : ( ! [V3upperc:tp__ty_2Enum_2Enum] : ( ! [V4rs:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V5lowery:tp__ty_2Einteger_2Eint] : ( ! [V6lowerc:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2EOmega_2Ershadow__row@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V3upperc))@(inj__ty_2Einteger_2Eint @ V2uppery)))@(ap@(ap@(c_2Elist_2ECONS@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V6lowerc))@(inj__ty_2Einteger_2Eint @ V5lowery)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V4rs)))) <=> ((p@(ap@(ap@c_2Einteger_2Eint__le@(ap@(ap@c_2Einteger_2Eint__mul@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V3upperc)))@(inj__ty_2Einteger_2Eint @ V5lowery)))@(ap@(ap@c_2Einteger_2Eint__mul@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V6lowerc)))@(inj__ty_2Einteger_2Eint @ V2uppery)))) & (p@(ap@(ap@c_2EOmega_2Ershadow__row@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V3upperc))@(inj__ty_2Einteger_2Eint @ V2uppery)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V4rs)))))))))))).
thf(ax_thm_2EOmega_2Ereal__shadow__def,axiom,(( ! [V0lowers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2EOmega_2Ereal__shadow@(c_2Elist_2ENIL@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0lowers))) <=> $true)) & ( ! [V1upper:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V2ls:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V3lowers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2EOmega_2Ereal__shadow@(ap@(ap@(c_2Elist_2ECONS@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1upper))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V2ls)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V3lowers))) <=> ((p@(ap@(ap@c_2EOmega_2Ershadow__row@(inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1upper))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V3lowers))) & (p@(ap@(ap@c_2EOmega_2Ereal__shadow@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V2ls))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V3lowers)))))))))).
thf(conj_thm_2EOmega_2Esingleton__real__shadow,lemma,( ! [V0c:tp__ty_2Enum_2Enum] : ( ! [V1L:tp__ty_2Einteger_2Eint] : ( ! [V2x:tp__ty_2Einteger_2Eint] : (((p@(ap@(ap@c_2Einteger_2Eint__le@(ap@(ap@c_2Einteger_2Eint__mul@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V0c)))@(inj__ty_2Einteger_2Eint @ V2x)))@(inj__ty_2Einteger_2Eint @ V1L))) & (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V0c)))) => ( ! [V3lowers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : (((p@(ap@(ap@(c_2Elist_2EEVERY@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(c_2EOmega_2Efst__nzero@ty_2Einteger_2Eint))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V3lowers))) & (p@(ap@(ap@c_2EOmega_2Eevallower@(inj__ty_2Einteger_2Eint @ V2x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V3lowers)))) => (p@(ap@(ap@c_2EOmega_2Ershadow__row@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V0c))@(inj__ty_2Einteger_2Eint @ V1L)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V3lowers)))))))))).
thf(conj_thm_2EOmega_2Ereal__shadow__revimp__uppers1,lemma,( ! [V0uppers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V1lowers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V2L:tp__ty_2Einteger_2Eint] : ( ! [V3x:tp__ty_2Einteger_2Eint] : (((p@(ap@(ap@c_2EOmega_2Ershadow__row@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Einteger_2Eint @ V2L)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1lowers))) & ((p@(ap@(ap@c_2EOmega_2Eevallower@(inj__ty_2Einteger_2Eint @ V3x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1lowers))) & ((p@(ap@(ap@c_2EOmega_2Eevalupper@(inj__ty_2Einteger_2Eint @ V3x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers))) & ((p@(ap@(ap@(c_2Elist_2EEVERY@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(c_2EOmega_2Efst__nzero@ty_2Einteger_2Eint))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1lowers))) & (p@(ap@(ap@(c_2Elist_2EEVERY@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(c_2EOmega_2Efst1@ty_2Einteger_2Eint))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers))))))) => (? [V4x:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2Einteger_2Eint__le@(inj__ty_2Einteger_2Eint @ V4x))@(inj__ty_2Einteger_2Eint @ V2L))) & ((p@(ap@(ap@c_2EOmega_2Eevalupper@(inj__ty_2Einteger_2Eint @ V4x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers))) & (p@(ap@(ap@c_2EOmega_2Eevallower@(inj__ty_2Einteger_2Eint @ V4x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1lowers)))))))))))).
thf(conj_thm_2EOmega_2Ereal__shadow__revimp__lowers1,lemma,( ! [V0uppers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V1lowers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V2c:tp__ty_2Enum_2Enum] : ( ! [V3L:tp__ty_2Einteger_2Eint] : ( ! [V4x:tp__ty_2Einteger_2Eint] : (((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V2c))) & ((p@(ap@(ap@c_2EOmega_2Ershadow__row@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V2c))@(inj__ty_2Einteger_2Eint @ V3L)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1lowers))) & ((p@(ap@(ap@c_2EOmega_2Eevalupper@(inj__ty_2Einteger_2Eint @ V4x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers))) & ((p@(ap@(ap@c_2EOmega_2Eevallower@(inj__ty_2Einteger_2Eint @ V4x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1lowers))) & ((p@(ap@(ap@(c_2Elist_2EEVERY@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(c_2EOmega_2Efst__nzero@ty_2Einteger_2Eint))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers))) & (p@(ap@(ap@(c_2Elist_2EEVERY@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(c_2EOmega_2Efst1@ty_2Einteger_2Eint))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1lowers)))))))) => (? [V5x:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2Einteger_2Eint__le@(ap@(ap@c_2Einteger_2Eint__mul@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V2c)))@(inj__ty_2Einteger_2Eint @ V5x)))@(inj__ty_2Einteger_2Eint @ V3L))) & ((p@(ap@(ap@c_2EOmega_2Eevalupper@(inj__ty_2Einteger_2Eint @ V5x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers))) & (p@(ap@(ap@c_2EOmega_2Eevallower@(inj__ty_2Einteger_2Eint @ V5x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1lowers))))))))))))).
thf(conj_thm_2EOmega_2Ereal__shadow__always__implied,lemma,( ! [V0uppers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V1lowers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V2x:tp__ty_2Einteger_2Eint] : (((p@(ap@(ap@c_2EOmega_2Eevalupper@(inj__ty_2Einteger_2Eint @ V2x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers))) & ((p@(ap@(ap@c_2EOmega_2Eevallower@(inj__ty_2Einteger_2Eint @ V2x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1lowers))) & ((p@(ap@(ap@(c_2Elist_2EEVERY@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(c_2EOmega_2Efst__nzero@ty_2Einteger_2Eint))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers))) & (p@(ap@(ap@(c_2Elist_2EEVERY@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(c_2EOmega_2Efst__nzero@ty_2Einteger_2Eint))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1lowers)))))) => (p@(ap@(ap@c_2EOmega_2Ereal__shadow@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1lowers)))))))).
thf(conj_thm_2EOmega_2Eexact__shadow__case,lemma,( ! [V0uppers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V1lowers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : (((p@(ap@(ap@(c_2Elist_2EEVERY@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(c_2EOmega_2Efst__nzero@ty_2Einteger_2Eint))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers))) & (p@(ap@(ap@(c_2Elist_2EEVERY@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(c_2EOmega_2Efst__nzero@ty_2Einteger_2Eint))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1lowers)))) => (((p@(ap@(ap@(c_2Elist_2EEVERY@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(c_2EOmega_2Efst1@ty_2Einteger_2Eint))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers))) | (p@(ap@(ap@(c_2Elist_2EEVERY@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(c_2EOmega_2Efst1@ty_2Einteger_2Eint))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1lowers)))) => ((? [V2x:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2EOmega_2Eevalupper@(inj__ty_2Einteger_2Eint @ V2x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers))) & (p@(ap@(ap@c_2EOmega_2Eevallower@(inj__ty_2Einteger_2Eint @ V2x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1lowers))))) <=> (p@(ap@(ap@c_2EOmega_2Ereal__shadow@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1lowers))))))))).
thf(conj_thm_2EOmega_2Edark__shadow__cond__row__ind,lemma,( ! [V0P:$i] : ((mem@V0P@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(arr@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@bool))) => ((( ! [V1c:tp__ty_2Enum_2Enum] : ( ! [V2L:tp__ty_2Einteger_2Eint] : (p@(ap@(ap@V0P@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V1c))@(inj__ty_2Einteger_2Eint @ V2L)))@(c_2Elist_2ENIL@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint)))))) & ( ! [V3c:tp__ty_2Enum_2Enum] : ( ! [V4L:tp__ty_2Einteger_2Eint] : ( ! [V5d:tp__ty_2Enum_2Enum] : ( ! [V6R:tp__ty_2Einteger_2Eint] : ( ! [V7t:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ((p@(ap@(ap@V0P@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V3c))@(inj__ty_2Einteger_2Eint @ V4L)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V7t))) => (p@(ap@(ap@V0P@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V3c))@(inj__ty_2Einteger_2Eint @ V4L)))@(ap@(ap@(c_2Elist_2ECONS@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V5d))@(inj__ty_2Einteger_2Eint @ V6R)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V7t))))))))))) => ( ! [V8v:tp__ty_2Enum_2Enum] : ( ! [V9v1:tp__ty_2Einteger_2Eint] : ( ! [V10v2:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : (p@(ap@(ap@V0P@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V8v))@(inj__ty_2Einteger_2Eint @ V9v1)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V10v2)))))))))).
thf(conj_thm_2EOmega_2Edark__shadow__cond__row__def,lemma,(( ! [V0c:tp__ty_2Enum_2Enum] : ( ! [V1L:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2EOmega_2Edark__shadow__cond__row@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V0c))@(inj__ty_2Einteger_2Eint @ V1L)))@(c_2Elist_2ENIL@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint)))) <=> $true))) & ( ! [V2t:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V3d:tp__ty_2Enum_2Enum] : ( ! [V4c:tp__ty_2Enum_2Enum] : ( ! [V5R:tp__ty_2Einteger_2Eint] : ( ! [V6L:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2EOmega_2Edark__shadow__cond__row@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V4c))@(inj__ty_2Einteger_2Eint @ V6L)))@(ap@(ap@(c_2Elist_2ECONS@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V3d))@(inj__ty_2Einteger_2Eint @ V5R)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V2t)))) <=> ((~~ (? [V7i:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2Einteger_2Eint__lt@(ap@(ap@c_2Einteger_2Eint__mul@(ap@(ap@c_2Einteger_2Eint__mul@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V4c)))@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V3d))))@(inj__ty_2Einteger_2Eint @ V7i)))@(ap@(ap@c_2Einteger_2Eint__mul@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V4c)))@(inj__ty_2Einteger_2Eint @ V5R)))) & ((p@(ap@(ap@c_2Einteger_2Eint__le@(ap@(ap@c_2Einteger_2Eint__mul@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V4c)))@(inj__ty_2Einteger_2Eint @ V5R)))@(ap@(ap@c_2Einteger_2Eint__mul@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V3d)))@(inj__ty_2Einteger_2Eint @ V6L)))) & (p@(ap@(ap@c_2Einteger_2Eint__lt@(ap@(ap@c_2Einteger_2Eint__mul@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V3d)))@(inj__ty_2Einteger_2Eint @ V6L)))@(ap@(ap@c_2Einteger_2Eint__mul@(ap@(ap@c_2Einteger_2Eint__mul@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V4c)))@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V3d))))@(ap@(ap@c_2Einteger_2Eint__add@(inj__ty_2Einteger_2Eint @ V7i))@(ap@c_2Einteger_2Eint__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))) & (p@(ap@(ap@c_2EOmega_2Edark__shadow__cond__row@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V4c))@(inj__ty_2Einteger_2Eint @ V6L)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V2t)))))))))))).
thf(conj_thm_2EOmega_2Edark__shadow__condition__ind,lemma,( ! [V0P:$i] : ((mem@V0P@(arr@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(arr@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@bool))) => ((( ! [V1lowers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : (p@(ap@(ap@V0P@(c_2Elist_2ENIL@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1lowers)))) & ( ! [V2c:tp__ty_2Enum_2Enum] : ( ! [V3L:tp__ty_2Einteger_2Eint] : ( ! [V4uppers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V5lowers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ((p@(ap@(ap@V0P@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V4uppers))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V5lowers))) => (p@(ap@(ap@V0P@(ap@(ap@(c_2Elist_2ECONS@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V2c))@(inj__ty_2Einteger_2Eint @ V3L)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V4uppers)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V5lowers))))))))) => ( ! [V6v:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V7v1:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : (p@(ap@(ap@V0P@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V6v))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V7v1))))))))).
thf(conj_thm_2EOmega_2Edark__shadow__condition__def,lemma,(( ! [V0lowers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2EOmega_2Edark__shadow__condition@(c_2Elist_2ENIL@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0lowers))) <=> $true)) & ( ! [V1uppers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V2lowers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V3c:tp__ty_2Enum_2Enum] : ( ! [V4L:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2EOmega_2Edark__shadow__condition@(ap@(ap@(c_2Elist_2ECONS@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V3c))@(inj__ty_2Einteger_2Eint @ V4L)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1uppers)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V2lowers))) <=> ((p@(ap@(ap@c_2EOmega_2Edark__shadow__cond__row@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V3c))@(inj__ty_2Einteger_2Eint @ V4L)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V2lowers))) & (p@(ap@(ap@c_2EOmega_2Edark__shadow__condition@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1uppers))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V2lowers))))))))))).
thf(conj_thm_2EOmega_2Ebasic__shadow__equivalence,lemma,( ! [V0uppers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V1lowers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : (((p@(ap@(ap@(c_2Elist_2EEVERY@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(c_2EOmega_2Efst__nzero@ty_2Einteger_2Eint))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers))) & (p@(ap@(ap@(c_2Elist_2EEVERY@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(c_2EOmega_2Efst__nzero@ty_2Einteger_2Eint))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1lowers)))) => ((? [V2x:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2EOmega_2Eevalupper@(inj__ty_2Einteger_2Eint @ V2x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers))) & (p@(ap@(ap@c_2EOmega_2Eevallower@(inj__ty_2Einteger_2Eint @ V2x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1lowers))))) <=> ((p@(ap@(ap@c_2EOmega_2Ereal__shadow@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1lowers))) & (p@(ap@(ap@c_2EOmega_2Edark__shadow__condition@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1lowers))))))))).
thf(conj_thm_2EOmega_2Edark__shadow__row__ind,lemma,( ! [V0P:$i] : ((mem@V0P@(arr@ty_2Enum_2Enum@(arr@ty_2Einteger_2Eint@(arr@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@bool)))) => ((( ! [V1c:tp__ty_2Enum_2Enum] : ( ! [V2L:tp__ty_2Einteger_2Eint] : (p@(ap@(ap@(ap@V0P@(inj__ty_2Enum_2Enum @ V1c))@(inj__ty_2Einteger_2Eint @ V2L))@(c_2Elist_2ENIL@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint)))))) & ( ! [V3c:tp__ty_2Enum_2Enum] : ( ! [V4L:tp__ty_2Einteger_2Eint] : ( ! [V5d:tp__ty_2Enum_2Enum] : ( ! [V6R:tp__ty_2Einteger_2Eint] : ( ! [V7rs:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ((p@(ap@(ap@(ap@V0P@(inj__ty_2Enum_2Enum @ V3c))@(inj__ty_2Einteger_2Eint @ V4L))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V7rs))) => (p@(ap@(ap@(ap@V0P@(inj__ty_2Enum_2Enum @ V3c))@(inj__ty_2Einteger_2Eint @ V4L))@(ap@(ap@(c_2Elist_2ECONS@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V5d))@(inj__ty_2Einteger_2Eint @ V6R)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V7rs))))))))))) => ( ! [V8v:tp__ty_2Enum_2Enum] : ( ! [V9v1:tp__ty_2Einteger_2Eint] : ( ! [V10v2:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : (p@(ap@(ap@(ap@V0P@(inj__ty_2Enum_2Enum @ V8v))@(inj__ty_2Einteger_2Eint @ V9v1))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V10v2)))))))))).
thf(conj_thm_2EOmega_2Edark__shadow__row__def,lemma,(( ! [V0c:tp__ty_2Enum_2Enum] : ( ! [V1L:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@(ap@c_2EOmega_2Edark__shadow__row@(inj__ty_2Enum_2Enum @ V0c))@(inj__ty_2Einteger_2Eint @ V1L))@(c_2Elist_2ENIL@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint)))) <=> $true))) & ( ! [V2rs:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V3d:tp__ty_2Enum_2Enum] : ( ! [V4c:tp__ty_2Enum_2Enum] : ( ! [V5R:tp__ty_2Einteger_2Eint] : ( ! [V6L:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@(ap@c_2EOmega_2Edark__shadow__row@(inj__ty_2Enum_2Enum @ V4c))@(inj__ty_2Einteger_2Eint @ V6L))@(ap@(ap@(c_2Elist_2ECONS@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V3d))@(inj__ty_2Einteger_2Eint @ V5R)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V2rs)))) <=> ((p@(ap@(ap@c_2Einteger_2Eint__ge@(ap@(ap@c_2Einteger_2Eint__sub@(ap@(ap@c_2Einteger_2Eint__mul@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V3d)))@(inj__ty_2Einteger_2Eint @ V6L)))@(ap@(ap@c_2Einteger_2Eint__mul@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V4c)))@(inj__ty_2Einteger_2Eint @ V5R))))@(ap@(ap@c_2Einteger_2Eint__mul@(ap@(ap@c_2Einteger_2Eint__sub@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V4c)))@(ap@c_2Einteger_2Eint__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))@(ap@(ap@c_2Einteger_2Eint__sub@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V3d)))@(ap@c_2Einteger_2Eint__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))) & (p@(ap@(ap@(ap@c_2EOmega_2Edark__shadow__row@(inj__ty_2Enum_2Enum @ V4c))@(inj__ty_2Einteger_2Eint @ V6L))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V2rs)))))))))))).
thf(conj_thm_2EOmega_2Edark__shadow__ind,lemma,( ! [V0P:$i] : ((mem@V0P@(arr@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(arr@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@bool))) => ((( ! [V1lowers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : (p@(ap@(ap@V0P@(c_2Elist_2ENIL@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1lowers)))) & ( ! [V2c:tp__ty_2Enum_2Enum] : ( ! [V3L:tp__ty_2Einteger_2Eint] : ( ! [V4uppers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V5lowers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ((p@(ap@(ap@V0P@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V4uppers))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V5lowers))) => (p@(ap@(ap@V0P@(ap@(ap@(c_2Elist_2ECONS@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V2c))@(inj__ty_2Einteger_2Eint @ V3L)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V4uppers)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V5lowers))))))))) => ( ! [V6v:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V7v1:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : (p@(ap@(ap@V0P@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V6v))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V7v1))))))))).
thf(conj_thm_2EOmega_2Edark__shadow__def,lemma,(( ! [V0lowers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2EOmega_2Edark__shadow@(c_2Elist_2ENIL@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0lowers))) <=> $true)) & ( ! [V1uppers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V2lowers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V3c:tp__ty_2Enum_2Enum] : ( ! [V4L:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2EOmega_2Edark__shadow@(ap@(ap@(c_2Elist_2ECONS@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V3c))@(inj__ty_2Einteger_2Eint @ V4L)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1uppers)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V2lowers))) <=> ((p@(ap@(ap@(ap@c_2EOmega_2Edark__shadow__row@(inj__ty_2Enum_2Enum @ V3c))@(inj__ty_2Einteger_2Eint @ V4L))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V2lowers))) & (p@(ap@(ap@c_2EOmega_2Edark__shadow@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1uppers))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V2lowers))))))))))).
thf(conj_thm_2EOmega_2Enightmare__ind,lemma,( ! [V0P:$i] : ((mem@V0P@(arr@ty_2Einteger_2Eint@(arr@ty_2Enum_2Enum@(arr@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(arr@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(arr@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@bool)))))) => ((( ! [V1x:tp__ty_2Einteger_2Eint] : ( ! [V2c:tp__ty_2Enum_2Enum] : ( ! [V3uppers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V4lowers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : (p@(ap@(ap@(ap@(ap@(ap@V0P@(inj__ty_2Einteger_2Eint @ V1x))@(inj__ty_2Enum_2Enum @ V2c))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V3uppers))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V4lowers))@(c_2Elist_2ENIL@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint)))))))) & ( ! [V5x:tp__ty_2Einteger_2Eint] : ( ! [V6c:tp__ty_2Enum_2Enum] : ( ! [V7uppers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V8lowers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V9d:tp__ty_2Enum_2Enum] : ( ! [V10R:tp__ty_2Einteger_2Eint] : ( ! [V11rs:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ((p@(ap@(ap@(ap@(ap@(ap@V0P@(inj__ty_2Einteger_2Eint @ V5x))@(inj__ty_2Enum_2Enum @ V6c))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V7uppers))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V8lowers))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V11rs))) => (p@(ap@(ap@(ap@(ap@(ap@V0P@(inj__ty_2Einteger_2Eint @ V5x))@(inj__ty_2Enum_2Enum @ V6c))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V7uppers))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V8lowers))@(ap@(ap@(c_2Elist_2ECONS@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V9d))@(inj__ty_2Einteger_2Eint @ V10R)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V11rs))))))))))))) => ( ! [V12v:tp__ty_2Einteger_2Eint] : ( ! [V13v1:tp__ty_2Enum_2Enum] : ( ! [V14v2:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V15v3:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V16v4:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : (p@(ap@(ap@(ap@(ap@(ap@V0P@(inj__ty_2Einteger_2Eint @ V12v))@(inj__ty_2Enum_2Enum @ V13v1))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V14v2))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V15v3))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V16v4)))))))))))).
thf(conj_thm_2EOmega_2Enightmare__def,lemma,(( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1uppers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V2lowers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V3c:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@(ap@(ap@(ap@c_2EOmega_2Enightmare@(inj__ty_2Einteger_2Eint @ V0x))@(inj__ty_2Enum_2Enum @ V3c))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1uppers))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V2lowers))@(c_2Elist_2ENIL@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint)))) <=> $false))))) & ( ! [V4x:tp__ty_2Einteger_2Eint] : ( ! [V5uppers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V6rs:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V7lowers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V8d:tp__ty_2Enum_2Enum] : ( ! [V9c:tp__ty_2Enum_2Enum] : ( ! [V10R:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@(ap@(ap@(ap@c_2EOmega_2Enightmare@(inj__ty_2Einteger_2Eint @ V4x))@(inj__ty_2Enum_2Enum @ V9c))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V5uppers))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V7lowers))@(ap@(ap@(c_2Elist_2ECONS@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V8d))@(inj__ty_2Einteger_2Eint @ V10R)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V6rs)))) <=> ((? [V11i:tp__ty_2Einteger_2Eint] : (((p@(ap@(ap@c_2Einteger_2Eint__le@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(inj__ty_2Einteger_2Eint @ V11i))) & (p@(ap@(ap@c_2Einteger_2Eint__le@(inj__ty_2Einteger_2Eint @ V11i))@(ap@(ap@c_2Einteger_2Eint__div@(ap@(ap@c_2Einteger_2Eint__sub@(ap@(ap@c_2Einteger_2Eint__sub@(ap@(ap@c_2Einteger_2Eint__mul@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V9c)))@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V8d))))@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V9c))))@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V8d))))@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V9c)))))) & (((surj__ty_2Einteger_2Eint @ (ap@(ap@c_2Einteger_2Eint__mul@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V8d)))@(inj__ty_2Einteger_2Eint @ V4x))) = (surj__ty_2Einteger_2Eint @ (ap@(ap@c_2Einteger_2Eint__add@(inj__ty_2Einteger_2Eint @ V10R))@(inj__ty_2Einteger_2Eint @ V11i)))) & ((p@(ap@(ap@c_2EOmega_2Eevalupper@(inj__ty_2Einteger_2Eint @ V4x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V5uppers))) & (p@(ap@(ap@c_2EOmega_2Eevallower@(inj__ty_2Einteger_2Eint @ V4x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V7lowers))))))) | (p@(ap@(ap@(ap@(ap@(ap@c_2EOmega_2Enightmare@(inj__ty_2Einteger_2Eint @ V4x))@(inj__ty_2Enum_2Enum @ V9c))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V5uppers))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V7lowers))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V6rs)))))))))))))).
thf(conj_thm_2EOmega_2Enightmare__implies__LHS,lemma,( ! [V0rs:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V1x:tp__ty_2Einteger_2Eint] : ( ! [V2uppers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V3lowers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V4c:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@(ap@(ap@(ap@c_2EOmega_2Enightmare@(inj__ty_2Einteger_2Eint @ V1x))@(inj__ty_2Enum_2Enum @ V4c))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V2uppers))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V3lowers))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0rs))) => ((p@(ap@(ap@c_2EOmega_2Eevalupper@(inj__ty_2Einteger_2Eint @ V1x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V2uppers))) & (p@(ap@(ap@c_2EOmega_2Eevallower@(inj__ty_2Einteger_2Eint @ V1x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V3lowers))))))))))).
thf(conj_thm_2EOmega_2Edark__shadow__FORALL,lemma,( ! [V0uppers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V1lowers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2EOmega_2Edark__shadow@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1lowers))) <=> ( ! [V2c:tp__ty_2Enum_2Enum] : ( ! [V3d:tp__ty_2Enum_2Enum] : ( ! [V4L:tp__ty_2Einteger_2Eint] : ( ! [V5R:tp__ty_2Einteger_2Eint] : (((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V2c))@(inj__ty_2Einteger_2Eint @ V4L)))@(ap@(c_2Elist_2ELIST__TO__SET@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers)))) & (p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V3d))@(inj__ty_2Einteger_2Eint @ V5R)))@(ap@(c_2Elist_2ELIST__TO__SET@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1lowers))))) => (p@(ap@(ap@c_2Einteger_2Eint__ge@(ap@(ap@c_2Einteger_2Eint__sub@(ap@(ap@c_2Einteger_2Eint__mul@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V3d)))@(inj__ty_2Einteger_2Eint @ V4L)))@(ap@(ap@c_2Einteger_2Eint__mul@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V2c)))@(inj__ty_2Einteger_2Eint @ V5R))))@(ap@(ap@c_2Einteger_2Eint__mul@(ap@(ap@c_2Einteger_2Eint__sub@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V2c)))@(ap@c_2Einteger_2Eint__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))@(ap@(ap@c_2Einteger_2Eint__sub@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V3d)))@(ap@c_2Einteger_2Eint__of__num@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))))))))).
thf(conj_thm_2EOmega_2Ereal__shadow__FORALL,lemma,( ! [V0uppers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V1lowers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2EOmega_2Ereal__shadow@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1lowers))) <=> ( ! [V2c:tp__ty_2Enum_2Enum] : ( ! [V3d:tp__ty_2Enum_2Enum] : ( ! [V4L:tp__ty_2Einteger_2Eint] : ( ! [V5R:tp__ty_2Einteger_2Eint] : (((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V2c))@(inj__ty_2Einteger_2Eint @ V4L)))@(ap@(c_2Elist_2ELIST__TO__SET@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers)))) & (p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V3d))@(inj__ty_2Einteger_2Eint @ V5R)))@(ap@(c_2Elist_2ELIST__TO__SET@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1lowers))))) => (p@(ap@(ap@c_2Einteger_2Eint__le@(ap@(ap@c_2Einteger_2Eint__mul@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V2c)))@(inj__ty_2Einteger_2Eint @ V5R)))@(ap@(ap@c_2Einteger_2Eint__mul@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V3d)))@(inj__ty_2Einteger_2Eint @ V4L))))))))))))).
thf(conj_thm_2EOmega_2Eevalupper__FORALL,lemma,( ! [V0uppers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V1x:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2EOmega_2Eevalupper@(inj__ty_2Einteger_2Eint @ V1x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers))) <=> ( ! [V2c:tp__ty_2Enum_2Enum] : ( ! [V3L:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V2c))@(inj__ty_2Einteger_2Eint @ V3L)))@(ap@(c_2Elist_2ELIST__TO__SET@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers)))) => (p@(ap@(ap@c_2Einteger_2Eint__le@(ap@(ap@c_2Einteger_2Eint__mul@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V2c)))@(inj__ty_2Einteger_2Eint @ V1x)))@(inj__ty_2Einteger_2Eint @ V3L)))))))))).
thf(conj_thm_2EOmega_2Eevallower__FORALL,lemma,( ! [V0lowers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V1x:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2EOmega_2Eevallower@(inj__ty_2Einteger_2Eint @ V1x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0lowers))) <=> ( ! [V2d:tp__ty_2Enum_2Enum] : ( ! [V3R:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V2d))@(inj__ty_2Einteger_2Eint @ V3R)))@(ap@(c_2Elist_2ELIST__TO__SET@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0lowers)))) => (p@(ap@(ap@c_2Einteger_2Eint__le@(inj__ty_2Einteger_2Eint @ V3R))@(ap@(ap@c_2Einteger_2Eint__mul@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V2d)))@(inj__ty_2Einteger_2Eint @ V1x))))))))))).
thf(conj_thm_2EOmega_2Enightmare__EXISTS,lemma,( ! [V0rs:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V1x:tp__ty_2Einteger_2Eint] : ( ! [V2c:tp__ty_2Enum_2Enum] : ( ! [V3uppers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V4lowers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ((p@(ap@(ap@(ap@(ap@(ap@c_2EOmega_2Enightmare@(inj__ty_2Einteger_2Eint @ V1x))@(inj__ty_2Enum_2Enum @ V2c))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V3uppers))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V4lowers))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0rs))) <=> (? [V5i:tp__ty_2Einteger_2Eint] : (? [V6d:tp__ty_2Enum_2Enum] : (? [V7R:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2Einteger_2Eint__le@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(inj__ty_2Einteger_2Eint @ V5i))) & ((p@(ap@(ap@c_2Einteger_2Eint__le@(inj__ty_2Einteger_2Eint @ V5i))@(ap@(ap@c_2Einteger_2Eint__div@(ap@(ap@c_2Einteger_2Eint__sub@(ap@(ap@c_2Einteger_2Eint__sub@(ap@(ap@c_2Einteger_2Eint__mul@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V6d)))@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V2c))))@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V2c))))@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V6d))))@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V2c))))) & ((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V6d))@(inj__ty_2Einteger_2Eint @ V7R)))@(ap@(c_2Elist_2ELIST__TO__SET@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0rs)))) & ((p@(ap@(ap@c_2EOmega_2Eevalupper@(inj__ty_2Einteger_2Eint @ V1x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V3uppers))) & ((p@(ap@(ap@c_2EOmega_2Eevallower@(inj__ty_2Einteger_2Eint @ V1x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V4lowers))) & ((surj__ty_2Einteger_2Eint @ (ap@(ap@c_2Einteger_2Eint__mul@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V6d)))@(inj__ty_2Einteger_2Eint @ V1x))) = (surj__ty_2Einteger_2Eint @ (ap@(ap@c_2Einteger_2Eint__add@(inj__ty_2Einteger_2Eint @ V7R))@(inj__ty_2Einteger_2Eint @ V5i))))))))))))))))))).
thf(conj_thm_2EOmega_2Efinal__equivalence,lemma,( ! [V0uppers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V1lowers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V2m:tp__ty_2Enum_2Enum] : (((p@(ap@(ap@(c_2Elist_2EEVERY@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(c_2EOmega_2Efst__nzero@ty_2Einteger_2Eint))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers))) & ((p@(ap@(ap@(c_2Elist_2EEVERY@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(c_2EOmega_2Efst__nzero@ty_2Einteger_2Eint))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1lowers))) & (p@(ap@(ap@(c_2Elist_2EEVERY@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(lam@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(^ [V3p:$i] : (ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(c_2Epair_2EFST@ty_2Enum_2Enum@ty_2Einteger_2Eint)@V3p))@(inj__ty_2Enum_2Enum @ V2m)))))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers))))) => ((? [V4x:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2EOmega_2Eevalupper@(inj__ty_2Einteger_2Eint @ V4x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers))) & (p@(ap@(ap@c_2EOmega_2Eevallower@(inj__ty_2Einteger_2Eint @ V4x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1lowers))))) <=> ((p@(ap@(ap@c_2EOmega_2Ereal__shadow@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1lowers))) & ((p@(ap@(ap@c_2EOmega_2Edark__shadow@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1lowers))) | (? [V5x:tp__ty_2Einteger_2Eint] : (p@(ap@(ap@(ap@(ap@(ap@c_2EOmega_2Enightmare@(inj__ty_2Einteger_2Eint @ V5x))@(inj__ty_2Enum_2Enum @ V2m))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1lowers))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1lowers)))))))))))).
thf(conj_thm_2EOmega_2Edarkrow__implies__realrow,lemma,( ! [V0lowers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V1c:tp__ty_2Enum_2Enum] : ( ! [V2L:tp__ty_2Einteger_2Eint] : (((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V1c))) & ((p@(ap@(ap@(c_2Elist_2EEVERY@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(c_2EOmega_2Efst__nzero@ty_2Einteger_2Eint))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0lowers))) & (p@(ap@(ap@(ap@c_2EOmega_2Edark__shadow__row@(inj__ty_2Enum_2Enum @ V1c))@(inj__ty_2Einteger_2Eint @ V2L))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0lowers))))) => (p@(ap@(ap@c_2EOmega_2Ershadow__row@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V1c))@(inj__ty_2Einteger_2Eint @ V2L)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0lowers)))))))).
thf(conj_thm_2EOmega_2Edark__implies__real,lemma,( ! [V0uppers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V1lowers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : (((p@(ap@(ap@(c_2Elist_2EEVERY@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(c_2EOmega_2Efst__nzero@ty_2Einteger_2Eint))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers))) & ((p@(ap@(ap@(c_2Elist_2EEVERY@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(c_2EOmega_2Efst__nzero@ty_2Einteger_2Eint))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1lowers))) & (p@(ap@(ap@c_2EOmega_2Edark__shadow@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1lowers))))) => (p@(ap@(ap@c_2EOmega_2Ereal__shadow@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1lowers))))))).
thf(conj_thm_2EOmega_2Ealternative__equivalence,lemma,( ! [V0uppers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V1lowers:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V2m:tp__ty_2Enum_2Enum] : (((p@(ap@(ap@(c_2Elist_2EEVERY@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(c_2EOmega_2Efst__nzero@ty_2Einteger_2Eint))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers))) & ((p@(ap@(ap@(c_2Elist_2EEVERY@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(c_2EOmega_2Efst__nzero@ty_2Einteger_2Eint))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1lowers))) & (p@(ap@(ap@(c_2Elist_2EEVERY@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(lam@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(^ [V3p:$i] : (ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(c_2Epair_2EFST@ty_2Enum_2Enum@ty_2Einteger_2Eint)@V3p))@(inj__ty_2Enum_2Enum @ V2m)))))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers))))) => ((? [V4x:tp__ty_2Einteger_2Eint] : ((p@(ap@(ap@c_2EOmega_2Eevalupper@(inj__ty_2Einteger_2Eint @ V4x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers))) & (p@(ap@(ap@c_2EOmega_2Eevallower@(inj__ty_2Einteger_2Eint @ V4x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1lowers))))) <=> ((p@(ap@(ap@c_2EOmega_2Edark__shadow@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1lowers))) | (? [V5x:tp__ty_2Einteger_2Eint] : (p@(ap@(ap@(ap@(ap@(ap@c_2EOmega_2Enightmare@(inj__ty_2Einteger_2Eint @ V5x))@(inj__ty_2Enum_2Enum @ V2m))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V0uppers))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1lowers))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1lowers))))))))))).
thf(conj_thm_2EOmega_2Eeval__base,lemma,( ! [V0p:$i] : ((mem@V0p@bool) => ( ! [V1x:tp__ty_2Einteger_2Eint] : ((p@V0p) <=> ((((p@(ap@(ap@c_2EOmega_2Eevalupper@(inj__ty_2Einteger_2Eint @ V1x))@(c_2Elist_2ENIL@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint)))) & (p@(ap@(ap@c_2EOmega_2Eevallower@(inj__ty_2Einteger_2Eint @ V1x))@(c_2Elist_2ENIL@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))))) & $true) & (p@V0p))))))).
thf(conj_thm_2EOmega_2Eeval__step__upper1,lemma,( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1ups:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V2lows:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V3ex:$i] : ((mem@V3ex@bool) => ( ! [V4c:tp__ty_2Enum_2Enum] : ( ! [V5r:tp__ty_2Einteger_2Eint] : (((((p@(ap@(ap@c_2EOmega_2Eevalupper@(inj__ty_2Einteger_2Eint @ V0x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1ups))) & (p@(ap@(ap@c_2EOmega_2Eevallower@(inj__ty_2Einteger_2Eint @ V0x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V2lows)))) & (p@V3ex)) & (p@(ap@(ap@c_2Einteger_2Eint__le@(ap@(ap@c_2Einteger_2Eint__mul@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V4c)))@(inj__ty_2Einteger_2Eint @ V0x)))@(inj__ty_2Einteger_2Eint @ V5r)))) <=> (((p@(ap@(ap@c_2EOmega_2Eevalupper@(inj__ty_2Einteger_2Eint @ V0x))@(ap@(ap@(c_2Elist_2ECONS@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V4c))@(inj__ty_2Einteger_2Eint @ V5r)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1ups)))) & (p@(ap@(ap@c_2EOmega_2Eevallower@(inj__ty_2Einteger_2Eint @ V0x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V2lows)))) & (p@V3ex))))))))))).
thf(conj_thm_2EOmega_2Eeval__step__upper2,lemma,( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1ups:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V2lows:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V3ex:$i] : ((mem@V3ex@bool) => ( ! [V4c:tp__ty_2Enum_2Enum] : ( ! [V5r:tp__ty_2Einteger_2Eint] : ( ! [V6p:$i] : ((mem@V6p@bool) => (((((p@(ap@(ap@c_2EOmega_2Eevalupper@(inj__ty_2Einteger_2Eint @ V0x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1ups))) & (p@(ap@(ap@c_2EOmega_2Eevallower@(inj__ty_2Einteger_2Eint @ V0x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V2lows)))) & (p@V3ex)) & ((p@(ap@(ap@c_2Einteger_2Eint__le@(ap@(ap@c_2Einteger_2Eint__mul@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V4c)))@(inj__ty_2Einteger_2Eint @ V0x)))@(inj__ty_2Einteger_2Eint @ V5r))) & (p@V6p))) <=> ((((p@(ap@(ap@c_2EOmega_2Eevalupper@(inj__ty_2Einteger_2Eint @ V0x))@(ap@(ap@(c_2Elist_2ECONS@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V4c))@(inj__ty_2Einteger_2Eint @ V5r)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1ups)))) & (p@(ap@(ap@c_2EOmega_2Eevallower@(inj__ty_2Einteger_2Eint @ V0x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V2lows)))) & (p@V3ex)) & (p@V6p))))))))))))).
thf(conj_thm_2EOmega_2Eeval__step__lower1,lemma,( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1ups:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V2lows:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V3ex:$i] : ((mem@V3ex@bool) => ( ! [V4r:tp__ty_2Einteger_2Eint] : ( ! [V5c:tp__ty_2Enum_2Enum] : (((((p@(ap@(ap@c_2EOmega_2Eevalupper@(inj__ty_2Einteger_2Eint @ V0x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1ups))) & (p@(ap@(ap@c_2EOmega_2Eevallower@(inj__ty_2Einteger_2Eint @ V0x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V2lows)))) & (p@V3ex)) & (p@(ap@(ap@c_2Einteger_2Eint__le@(inj__ty_2Einteger_2Eint @ V4r))@(ap@(ap@c_2Einteger_2Eint__mul@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V5c)))@(inj__ty_2Einteger_2Eint @ V0x))))) <=> (((p@(ap@(ap@c_2EOmega_2Eevalupper@(inj__ty_2Einteger_2Eint @ V0x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1ups))) & (p@(ap@(ap@c_2EOmega_2Eevallower@(inj__ty_2Einteger_2Eint @ V0x))@(ap@(ap@(c_2Elist_2ECONS@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V5c))@(inj__ty_2Einteger_2Eint @ V4r)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V2lows))))) & (p@V3ex))))))))))).
thf(conj_thm_2EOmega_2Eeval__step__lower2,lemma,( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1ups:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V2lows:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V3ex:$i] : ((mem@V3ex@bool) => ( ! [V4r:tp__ty_2Einteger_2Eint] : ( ! [V5c:tp__ty_2Enum_2Enum] : ( ! [V6p:$i] : ((mem@V6p@bool) => (((((p@(ap@(ap@c_2EOmega_2Eevalupper@(inj__ty_2Einteger_2Eint @ V0x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1ups))) & (p@(ap@(ap@c_2EOmega_2Eevallower@(inj__ty_2Einteger_2Eint @ V0x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V2lows)))) & (p@V3ex)) & ((p@(ap@(ap@c_2Einteger_2Eint__le@(inj__ty_2Einteger_2Eint @ V4r))@(ap@(ap@c_2Einteger_2Eint__mul@(ap@c_2Einteger_2Eint__of__num@(inj__ty_2Enum_2Enum @ V5c)))@(inj__ty_2Einteger_2Eint @ V0x)))) & (p@V6p))) <=> ((((p@(ap@(ap@c_2EOmega_2Eevalupper@(inj__ty_2Einteger_2Eint @ V0x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1ups))) & (p@(ap@(ap@c_2EOmega_2Eevallower@(inj__ty_2Einteger_2Eint @ V0x))@(ap@(ap@(c_2Elist_2ECONS@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Einteger_2Eint))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Einteger_2Eint)@(inj__ty_2Enum_2Enum @ V5c))@(inj__ty_2Einteger_2Eint @ V4r)))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V2lows))))) & (p@V3ex)) & (p@V6p))))))))))))).
thf(conj_thm_2EOmega_2Eeval__step__extra1,lemma,( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1ups:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V2lows:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V3ex_27:$i] : ((mem@V3ex_27@bool) => (((((p@(ap@(ap@c_2EOmega_2Eevalupper@(inj__ty_2Einteger_2Eint @ V0x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1ups))) & (p@(ap@(ap@c_2EOmega_2Eevallower@(inj__ty_2Einteger_2Eint @ V0x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V2lows)))) & $true) & (p@V3ex_27)) <=> (((p@(ap@(ap@c_2EOmega_2Eevalupper@(inj__ty_2Einteger_2Eint @ V0x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1ups))) & (p@(ap@(ap@c_2EOmega_2Eevallower@(inj__ty_2Einteger_2Eint @ V0x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V2lows)))) & (p@V3ex_27))))))))).
thf(conj_thm_2EOmega_2Eeval__step__extra2,lemma,( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1ups:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V2lows:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V3ex:$i] : ((mem@V3ex@bool) => ( ! [V4ex_27:$i] : ((mem@V4ex_27@bool) => (((((p@(ap@(ap@c_2EOmega_2Eevalupper@(inj__ty_2Einteger_2Eint @ V0x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1ups))) & (p@(ap@(ap@c_2EOmega_2Eevallower@(inj__ty_2Einteger_2Eint @ V0x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V2lows)))) & (p@V3ex)) & (p@V4ex_27)) <=> (((p@(ap@(ap@c_2EOmega_2Eevalupper@(inj__ty_2Einteger_2Eint @ V0x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1ups))) & (p@(ap@(ap@c_2EOmega_2Eevallower@(inj__ty_2Einteger_2Eint @ V0x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V2lows)))) & ((p@V3ex) & (p@V4ex_27)))))))))))).
thf(conj_thm_2EOmega_2Eeval__step__extra3,lemma,( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1ups:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V2lows:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V3ex_27:$i] : ((mem@V3ex_27@bool) => ( ! [V4p:$i] : ((mem@V4p@bool) => (((((p@(ap@(ap@c_2EOmega_2Eevalupper@(inj__ty_2Einteger_2Eint @ V0x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1ups))) & (p@(ap@(ap@c_2EOmega_2Eevallower@(inj__ty_2Einteger_2Eint @ V0x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V2lows)))) & $true) & ((p@V3ex_27) & (p@V4p))) <=> ((((p@(ap@(ap@c_2EOmega_2Eevalupper@(inj__ty_2Einteger_2Eint @ V0x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1ups))) & (p@(ap@(ap@c_2EOmega_2Eevallower@(inj__ty_2Einteger_2Eint @ V0x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V2lows)))) & (p@V3ex_27)) & (p@V4p))))))))))).
thf(conj_thm_2EOmega_2Eeval__step__extra4,conjecture,( ! [V0x:tp__ty_2Einteger_2Eint] : ( ! [V1ups:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V2lows:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [V3ex:$i] : ((mem@V3ex@bool) => ( ! [V4ex_27:$i] : ((mem@V4ex_27@bool) => ( ! [V5p:$i] : ((mem@V5p@bool) => (((((p@(ap@(ap@c_2EOmega_2Eevalupper@(inj__ty_2Einteger_2Eint @ V0x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1ups))) & (p@(ap@(ap@c_2EOmega_2Eevallower@(inj__ty_2Einteger_2Eint @ V0x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V2lows)))) & (p@V3ex)) & ((p@V4ex_27) & (p@V5p))) <=> ((((p@(ap@(ap@c_2EOmega_2Eevalupper@(inj__ty_2Einteger_2Eint @ V0x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V1ups))) & (p@(ap@(ap@c_2EOmega_2Eevallower@(inj__ty_2Einteger_2Eint @ V0x))@(inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint @ V2lows)))) & ((p@V3ex) & (p@V4ex_27))) & (p@V5p))))))))))))).
