include('Axioms/int_arith_2.ax').
tff(tp_c_2EOmega_2EMAP2,type,(c_2EOmega_2EMAP2:(del * del) > $i)).
tff(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))))))))).
tff(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)).
tff(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)).
tff(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)).
tff(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))).
tff(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)))))).
tff(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)))))).
tff(stp_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint,type,(tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint : $tType)).
tff(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)).
tff(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)).
tff(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))).
tff(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))))).
tff(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)))))).
tff(tp_c_2EOmega_2Ecalc__nightmare,type,(c_2EOmega_2Ecalc__nightmare:$i)).
tff(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))))).
tff(stp_fo_c_2EOmega_2Ecalc__nightmare,type,(fo__c_2EOmega_2Ecalc__nightmare:(tp__ty_2Einteger_2Eint * tp__ty_2Enum_2Enum * tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint) > tp__o)).
tff(stp_eq_fo_c_2EOmega_2Ecalc__nightmare,axiom,( ! [X0:tp__ty_2Einteger_2Eint] : ( ! [X1:tp__ty_2Enum_2Enum] : ( ! [X2:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : (inj__o(fo__c_2EOmega_2Ecalc__nightmare(X0,X1,X2)) = ap(ap(ap(c_2EOmega_2Ecalc__nightmare,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Enum_2Enum(X1)),inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint(X2))))))).
tff(tp_c_2EOmega_2Edark__shadow,type,(c_2EOmega_2Edark__shadow:$i)).
tff(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)))).
tff(stp_fo_c_2EOmega_2Edark__shadow,type,(fo__c_2EOmega_2Edark__shadow:(tp__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) > tp__o)).
tff(stp_eq_fo_c_2EOmega_2Edark__shadow,axiom,( ! [X0:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [X1:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : (inj__o(fo__c_2EOmega_2Edark__shadow(X0,X1)) = ap(ap(c_2EOmega_2Edark__shadow,inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint(X0)),inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint(X1)))))).
tff(tp_c_2EOmega_2Edark__shadow__cond__row,type,(c_2EOmega_2Edark__shadow__cond__row:$i)).
tff(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)))).
tff(stp_fo_c_2EOmega_2Edark__shadow__cond__row,type,(fo__c_2EOmega_2Edark__shadow__cond__row:(tp__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) > tp__o)).
tff(stp_eq_fo_c_2EOmega_2Edark__shadow__cond__row,axiom,( ! [X0:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [X1:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : (inj__o(fo__c_2EOmega_2Edark__shadow__cond__row(X0,X1)) = ap(ap(c_2EOmega_2Edark__shadow__cond__row,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint(X0)),inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint(X1)))))).
tff(tp_c_2EOmega_2Edark__shadow__condition,type,(c_2EOmega_2Edark__shadow__condition:$i)).
tff(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)))).
tff(stp_fo_c_2EOmega_2Edark__shadow__condition,type,(fo__c_2EOmega_2Edark__shadow__condition:(tp__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) > tp__o)).
tff(stp_eq_fo_c_2EOmega_2Edark__shadow__condition,axiom,( ! [X0:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [X1:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : (inj__o(fo__c_2EOmega_2Edark__shadow__condition(X0,X1)) = ap(ap(c_2EOmega_2Edark__shadow__condition,inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint(X0)),inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint(X1)))))).
tff(tp_c_2EOmega_2Edark__shadow__row,type,(c_2EOmega_2Edark__shadow__row:$i)).
tff(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))))).
tff(stp_fo_c_2EOmega_2Edark__shadow__row,type,(fo__c_2EOmega_2Edark__shadow__row:(tp__ty_2Enum_2Enum * tp__ty_2Einteger_2Eint * tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint) > tp__o)).
tff(stp_eq_fo_c_2EOmega_2Edark__shadow__row,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Einteger_2Eint] : ( ! [X2:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : (inj__o(fo__c_2EOmega_2Edark__shadow__row(X0,X1,X2)) = ap(ap(ap(c_2EOmega_2Edark__shadow__row,inj__ty_2Enum_2Enum(X0)),inj__ty_2Einteger_2Eint(X1)),inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint(X2))))))).
tff(tp_c_2EOmega_2Eevallower,type,(c_2EOmega_2Eevallower:$i)).
tff(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)))).
tff(stp_fo_c_2EOmega_2Eevallower,type,(fo__c_2EOmega_2Eevallower:(tp__ty_2Einteger_2Eint * tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint) > tp__o)).
tff(stp_eq_fo_c_2EOmega_2Eevallower,axiom,( ! [X0:tp__ty_2Einteger_2Eint] : ( ! [X1:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : (inj__o(fo__c_2EOmega_2Eevallower(X0,X1)) = ap(ap(c_2EOmega_2Eevallower,inj__ty_2Einteger_2Eint(X0)),inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint(X1)))))).
tff(tp_c_2EOmega_2Eevalupper,type,(c_2EOmega_2Eevalupper:$i)).
tff(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)))).
tff(stp_fo_c_2EOmega_2Eevalupper,type,(fo__c_2EOmega_2Eevalupper:(tp__ty_2Einteger_2Eint * tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint) > tp__o)).
tff(stp_eq_fo_c_2EOmega_2Eevalupper,axiom,( ! [X0:tp__ty_2Einteger_2Eint] : ( ! [X1:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : (inj__o(fo__c_2EOmega_2Eevalupper(X0,X1)) = ap(ap(c_2EOmega_2Eevalupper,inj__ty_2Einteger_2Eint(X0)),inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint(X1)))))).
tff(tp_c_2EOmega_2Efst1,type,(c_2EOmega_2Efst1:del > $i)).
tff(mem_c_2EOmega_2Efst1,axiom,( ! [A_27a:del] : mem(c_2EOmega_2Efst1(A_27a),arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,A_27a),bool)))).
tff(tp_c_2EOmega_2Efst__nzero,type,(c_2EOmega_2Efst__nzero:del > $i)).
tff(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)))).
tff(tp_c_2EOmega_2Emodhat,type,(c_2EOmega_2Emodhat:$i)).
tff(mem_c_2EOmega_2Emodhat,axiom,mem(c_2EOmega_2Emodhat,arr(ty_2Einteger_2Eint,arr(ty_2Einteger_2Eint,ty_2Einteger_2Eint)))).
tff(stp_fo_c_2EOmega_2Emodhat,type,(fo__c_2EOmega_2Emodhat:(tp__ty_2Einteger_2Eint * tp__ty_2Einteger_2Eint) > tp__ty_2Einteger_2Eint)).
tff(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)))))).
tff(tp_c_2EOmega_2Enightmare,type,(c_2EOmega_2Enightmare:$i)).
tff(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))))))).
tff(stp_fo_c_2EOmega_2Enightmare,type,(fo__c_2EOmega_2Enightmare:(tp__ty_2Einteger_2Eint * tp__ty_2Enum_2Enum * tp__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 * tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint) > tp__o)).
tff(stp_eq_fo_c_2EOmega_2Enightmare,axiom,( ! [X0:tp__ty_2Einteger_2Eint] : ( ! [X1:tp__ty_2Enum_2Enum] : ( ! [X2:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [X3:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [X4:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : (inj__o(fo__c_2EOmega_2Enightmare(X0,X1,X2,X3,X4)) = ap(ap(ap(ap(ap(c_2EOmega_2Enightmare,inj__ty_2Einteger_2Eint(X0)),inj__ty_2Enum_2Enum(X1)),inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint(X2)),inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint(X3)),inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint(X4))))))))).
tff(tp_c_2EOmega_2Ereal__shadow,type,(c_2EOmega_2Ereal__shadow:$i)).
tff(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)))).
tff(stp_fo_c_2EOmega_2Ereal__shadow,type,(fo__c_2EOmega_2Ereal__shadow:(tp__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) > tp__o)).
tff(stp_eq_fo_c_2EOmega_2Ereal__shadow,axiom,( ! [X0:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [X1:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : (inj__o(fo__c_2EOmega_2Ereal__shadow(X0,X1)) = ap(ap(c_2EOmega_2Ereal__shadow,inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint(X0)),inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint(X1)))))).
tff(tp_c_2EOmega_2Ershadow__row,type,(c_2EOmega_2Ershadow__row:$i)).
tff(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)))).
tff(stp_fo_c_2EOmega_2Ershadow__row,type,(fo__c_2EOmega_2Ershadow__row:(tp__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) > tp__o)).
tff(stp_eq_fo_c_2EOmega_2Ershadow__row,axiom,( ! [X0:tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : ( ! [X1:tp__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint] : (inj__o(fo__c_2EOmega_2Ershadow__row(X0,X1)) = ap(ap(c_2EOmega_2Ershadow__row,inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint(X0)),inj__c_ty_2Elist_2Elist_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Einteger_2Eint(X1)))))).
tff(stp_c_ty_2Elist_2Elist_ty_2Einteger_2Eint,type,(tp__c_ty_2Elist_2Elist_ty_2Einteger_2Eint : $tType)).
tff(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)).
tff(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)).
tff(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))).
tff(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))))).
tff(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)))))).
tff(tp_c_2EOmega_2Esumc,type,(c_2EOmega_2Esumc:$i)).
tff(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)))).
tff(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)).
tff(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)))))).
tff(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))))))))))))))))).
tff(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)))))))))))))))))))))).
tff(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))))).
tff(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)))))))))).
tff(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))))))))))))).
tff(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))))))))))))).
tff(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))))))))).
tff(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),f2513(V2f)),inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint(V0cs))),inj__c_ty_2Elist_2Elist_ty_2Einteger_2Eint(V1vs))))))))).
tff(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))))))))).
tff(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))))))))))))).
tff(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)))))))))).
tff(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),f2514(V0c)),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))))))))))))))).
tff(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)))))))))).
tff(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)))))))))))).
tff(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)))))))))).
tff(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)))))))))))).
tff(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))))))))).
tff(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))))))))).
tff(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)))))))).
tff(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)))))))))).
tff(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)))))))).
tff(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)))))))).
tff(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))))))))))).
tff(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))))))))))))).
tff(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)))))))))).
tff(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))))))))))).
tff(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))))))))))))).
tff(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)))))))))))))).
tff(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))))))))).
tff(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)))))))))).
tff(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))))))))))).
tff(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))))))))))))).
tff(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)))))))))).
tff(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)))))))))))).
tff(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)))))))))).
tff(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))))))))))).
tff(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))))))))))))).
tff(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)))))))))).
tff(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)))))))))))).
tff(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))))))))))))).
tff(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))))))))))))))).
tff(conj_thm_2EOmega_2Enightmare__implies__LHS,conjecture,(( ! [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)))))))))))).
