include('Axioms/HL4001_2.ax').
tff(tp_ty_2Elist_2Elist,type,( ty_2Elist_2Elist: del > del )).
tff(tp_c_2Elist_2EHD,type,(c_2Elist_2EHD:del > $i)).
tff(mem_c_2Elist_2EHD,axiom,( ! [A_27a:del] : mem(c_2Elist_2EHD(A_27a),arr(ty_2Elist_2Elist(A_27a),A_27a)))).
tff(tp_c_2Elist_2ETL,type,(c_2Elist_2ETL:del > $i)).
tff(mem_c_2Elist_2ETL,axiom,( ! [A_27a:del] : mem(c_2Elist_2ETL(A_27a),arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a))))).
tff(stp_o,type,(tp__o : $tType)).
tff(stp_inj_o,type,(inj__o : tp__o > $i)).
tff(stp_surj_o,type,(surj__o : $i > tp__o)).
tff(stp_inj_surj_o,axiom,( ! [X:tp__o] : (surj__o(inj__o(X)) = X))).
tff(stp_inj_mem_o,axiom,( ! [X:tp__o] : (mem(inj__o(X),bool)))).
tff(stp_iso_mem_o,axiom,( ! [X:$i] : (mem(X,bool) => (X = inj__o(surj__o(X)))))).
tff(tp_c_2Ebool_2E_3F,type,(c_2Ebool_2E_3F:del > $i)).
tff(mem_c_2Ebool_2E_3F,axiom,( ! [A_27a:del] : mem(c_2Ebool_2E_3F(A_27a),arr(arr(A_27a,bool),bool)))).
tff(ax_ex_p,axiom,( ! [A:del] : ( ! [Q:$i] : (mem(Q,arr(A,bool)) => (p(ap(c_2Ebool_2E_3F(A),Q)) <=> (? [X:$i] : (mem(X,A) & p(ap(Q,X))))))))).
tff(tp_c_2Elist_2ECONS,type,(c_2Elist_2ECONS:del > $i)).
tff(mem_c_2Elist_2ECONS,axiom,( ! [A_27a:del] : mem(c_2Elist_2ECONS(A_27a),arr(A_27a,arr(ty_2Elist_2Elist(A_27a),ty_2Elist_2Elist(A_27a)))))).
tff(tp_c_2Elist_2ENIL,type,(c_2Elist_2ENIL:del > $i)).
tff(mem_c_2Elist_2ENIL,axiom,( ! [A_27a:del] : mem(c_2Elist_2ENIL(A_27a),ty_2Elist_2Elist(A_27a)))).
tff(tp_ty_2Enum_2Enum,type,( ty_2Enum_2Enum: del )).
tff(stp_ty_2Enum_2Enum,type,(tp__ty_2Enum_2Enum : $tType)).
tff(stp_inj_ty_2Enum_2Enum,type,(inj__ty_2Enum_2Enum : tp__ty_2Enum_2Enum > $i)).
tff(stp_surj_ty_2Enum_2Enum,type,(surj__ty_2Enum_2Enum : $i > tp__ty_2Enum_2Enum)).
tff(stp_inj_surj_ty_2Enum_2Enum,axiom,( ! [X:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(inj__ty_2Enum_2Enum(X)) = X))).
tff(stp_inj_mem_ty_2Enum_2Enum,axiom,( ! [X:tp__ty_2Enum_2Enum] : (mem(inj__ty_2Enum_2Enum(X),ty_2Enum_2Enum)))).
tff(stp_iso_mem_ty_2Enum_2Enum,axiom,( ! [X:$i] : (mem(X,ty_2Enum_2Enum) => (X = inj__ty_2Enum_2Enum(surj__ty_2Enum_2Enum(X)))))).
tff(tp_c_2Elist_2ELENGTH,type,(c_2Elist_2ELENGTH:del > $i)).
tff(mem_c_2Elist_2ELENGTH,axiom,( ! [A_27a:del] : mem(c_2Elist_2ELENGTH(A_27a),arr(ty_2Elist_2Elist(A_27a),ty_2Enum_2Enum)))).
tff(tp_c_2Earithmetic_2EEVEN,type,(c_2Earithmetic_2EEVEN:$i)).
tff(mem_c_2Earithmetic_2EEVEN,axiom,mem(c_2Earithmetic_2EEVEN,arr(ty_2Enum_2Enum,bool))).
tff(stp_fo_c_2Earithmetic_2EEVEN,type,(fo__c_2Earithmetic_2EEVEN:(tp__ty_2Enum_2Enum) > tp__o)).
tff(stp_eq_fo_c_2Earithmetic_2EEVEN,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__o(fo__c_2Earithmetic_2EEVEN(X0)) = ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Earithmetic_2EODD,type,(c_2Earithmetic_2EODD:$i)).
tff(mem_c_2Earithmetic_2EODD,axiom,mem(c_2Earithmetic_2EODD,arr(ty_2Enum_2Enum,bool))).
tff(stp_fo_c_2Earithmetic_2EODD,type,(fo__c_2Earithmetic_2EODD:(tp__ty_2Enum_2Enum) > tp__o)).
tff(stp_eq_fo_c_2Earithmetic_2EODD,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__o(fo__c_2Earithmetic_2EODD(X0)) = ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Earithmetic_2E_3E_3D,type,(c_2Earithmetic_2E_3E_3D:$i)).
tff(mem_c_2Earithmetic_2E_3E_3D,axiom,mem(c_2Earithmetic_2E_3E_3D,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool)))).
tff(stp_fo_c_2Earithmetic_2E_3E_3D,type,(fo__c_2Earithmetic_2E_3E_3D:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__o)).
tff(stp_eq_fo_c_2Earithmetic_2E_3E_3D,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__o(fo__c_2Earithmetic_2E_3E_3D(X0,X1)) = ap(ap(c_2Earithmetic_2E_3E_3D,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Earithmetic_2E_3E,type,(c_2Earithmetic_2E_3E:$i)).
tff(mem_c_2Earithmetic_2E_3E,axiom,mem(c_2Earithmetic_2E_3E,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool)))).
tff(stp_fo_c_2Earithmetic_2E_3E,type,(fo__c_2Earithmetic_2E_3E:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__o)).
tff(stp_eq_fo_c_2Earithmetic_2E_3E,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__o(fo__c_2Earithmetic_2E_3E(X0,X1)) = ap(ap(c_2Earithmetic_2E_3E,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Earithmetic_2EEXP,type,(c_2Earithmetic_2EEXP:$i)).
tff(mem_c_2Earithmetic_2EEXP,axiom,mem(c_2Earithmetic_2EEXP,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)))).
tff(stp_fo_c_2Earithmetic_2EEXP,type,(fo__c_2Earithmetic_2EEXP:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2EEXP,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EEXP(X0,X1)) = ap(ap(c_2Earithmetic_2EEXP,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Earithmetic_2E_2D,type,(c_2Earithmetic_2E_2D:$i)).
tff(mem_c_2Earithmetic_2E_2D,axiom,mem(c_2Earithmetic_2E_2D,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)))).
tff(stp_fo_c_2Earithmetic_2E_2D,type,(fo__c_2Earithmetic_2E_2D:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2E_2D,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2E_2D(X0,X1)) = ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Earithmetic_2E_2A,type,(c_2Earithmetic_2E_2A:$i)).
tff(mem_c_2Earithmetic_2E_2A,axiom,mem(c_2Earithmetic_2E_2A,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)))).
tff(stp_fo_c_2Earithmetic_2E_2A,type,(fo__c_2Earithmetic_2E_2A:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2E_2A,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2E_2A(X0,X1)) = ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Earithmetic_2ENUMERAL,type,(c_2Earithmetic_2ENUMERAL:$i)).
tff(mem_c_2Earithmetic_2ENUMERAL,axiom,mem(c_2Earithmetic_2ENUMERAL,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))).
tff(stp_fo_c_2Earithmetic_2ENUMERAL,type,(fo__c_2Earithmetic_2ENUMERAL:(tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2ENUMERAL,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2ENUMERAL(X0)) = ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Enum_2E0,type,(c_2Enum_2E0:$i)).
tff(mem_c_2Enum_2E0,axiom,mem(c_2Enum_2E0,ty_2Enum_2Enum)).
tff(stp_fo_c_2Enum_2E0,type,(fo__c_2Enum_2E0:tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Enum_2E0,axiom,(inj__ty_2Enum_2Enum(fo__c_2Enum_2E0) = c_2Enum_2E0)).
tff(tp_c_2Enumeral_2EiiSUC,type,(c_2Enumeral_2EiiSUC:$i)).
tff(mem_c_2Enumeral_2EiiSUC,axiom,mem(c_2Enumeral_2EiiSUC,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))).
tff(stp_fo_c_2Enumeral_2EiiSUC,type,(fo__c_2Enumeral_2EiiSUC:(tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Enumeral_2EiiSUC,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Enumeral_2EiiSUC(X0)) = ap(c_2Enumeral_2EiiSUC,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Enum_2ESUC,type,(c_2Enum_2ESUC:$i)).
tff(mem_c_2Enum_2ESUC,axiom,mem(c_2Enum_2ESUC,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))).
tff(stp_fo_c_2Enum_2ESUC,type,(fo__c_2Enum_2ESUC:(tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Enum_2ESUC,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Enum_2ESUC(X0)) = ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Earithmetic_2E_2B,type,(c_2Earithmetic_2E_2B:$i)).
tff(mem_c_2Earithmetic_2E_2B,axiom,mem(c_2Earithmetic_2E_2B,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)))).
tff(stp_fo_c_2Earithmetic_2E_2B,type,(fo__c_2Earithmetic_2E_2B:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2E_2B,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2E_2B(X0,X1)) = ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Enumeral_2EiZ,type,(c_2Enumeral_2EiZ:$i)).
tff(mem_c_2Enumeral_2EiZ,axiom,mem(c_2Enumeral_2EiZ,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))).
tff(stp_fo_c_2Enumeral_2EiZ,type,(fo__c_2Enumeral_2EiZ:(tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Enumeral_2EiZ,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Enumeral_2EiZ(X0)) = ap(c_2Enumeral_2EiZ,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Eprim__rec_2E_3C,type,(c_2Eprim__rec_2E_3C:$i)).
tff(mem_c_2Eprim__rec_2E_3C,axiom,mem(c_2Eprim__rec_2E_3C,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool)))).
tff(stp_fo_c_2Eprim__rec_2E_3C,type,(fo__c_2Eprim__rec_2E_3C:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__o)).
tff(stp_eq_fo_c_2Eprim__rec_2E_3C,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__o(fo__c_2Eprim__rec_2E_3C(X0,X1)) = ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Ebool_2ET,type,(c_2Ebool_2ET:$i)).
tff(mem_c_2Ebool_2ET,axiom,mem(c_2Ebool_2ET,bool)).
tff(stp_fo_c_2Ebool_2ET,type,(fo__c_2Ebool_2ET:tp__o)).
tff(stp_eq_fo_c_2Ebool_2ET,axiom,(inj__o(fo__c_2Ebool_2ET) = c_2Ebool_2ET)).
tff(ax_true_p,axiom,p(c_2Ebool_2ET)).
tff(tp_c_2Earithmetic_2E_3C_3D,type,(c_2Earithmetic_2E_3C_3D:$i)).
tff(mem_c_2Earithmetic_2E_3C_3D,axiom,mem(c_2Earithmetic_2E_3C_3D,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool)))).
tff(stp_fo_c_2Earithmetic_2E_3C_3D,type,(fo__c_2Earithmetic_2E_3C_3D:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__o)).
tff(stp_eq_fo_c_2Earithmetic_2E_3C_3D,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__o(fo__c_2Earithmetic_2E_3C_3D(X0,X1)) = ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Earithmetic_2EBIT2,type,(c_2Earithmetic_2EBIT2:$i)).
tff(mem_c_2Earithmetic_2EBIT2,axiom,mem(c_2Earithmetic_2EBIT2,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))).
tff(stp_fo_c_2Earithmetic_2EBIT2,type,(fo__c_2Earithmetic_2EBIT2:(tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2EBIT2,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EBIT2(X0)) = ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Earithmetic_2EBIT1,type,(c_2Earithmetic_2EBIT1:$i)).
tff(mem_c_2Earithmetic_2EBIT1,axiom,mem(c_2Earithmetic_2EBIT1,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))).
tff(stp_fo_c_2Earithmetic_2EBIT1,type,(fo__c_2Earithmetic_2EBIT1:(tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2EBIT1,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EBIT1(X0)) = ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Earithmetic_2EZERO,type,(c_2Earithmetic_2EZERO:$i)).
tff(mem_c_2Earithmetic_2EZERO,axiom,mem(c_2Earithmetic_2EZERO,ty_2Enum_2Enum)).
tff(stp_fo_c_2Earithmetic_2EZERO,type,(fo__c_2Earithmetic_2EZERO:tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Earithmetic_2EZERO,axiom,(inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO) = c_2Earithmetic_2EZERO)).
tff(tp_c_2Eprim__rec_2EPRE,type,(c_2Eprim__rec_2EPRE:$i)).
tff(mem_c_2Eprim__rec_2EPRE,axiom,mem(c_2Eprim__rec_2EPRE,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))).
tff(stp_fo_c_2Eprim__rec_2EPRE,type,(fo__c_2Eprim__rec_2EPRE:(tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Eprim__rec_2EPRE,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Eprim__rec_2EPRE(X0)) = ap(c_2Eprim__rec_2EPRE,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Ebool_2EF,type,(c_2Ebool_2EF:$i)).
tff(mem_c_2Ebool_2EF,axiom,mem(c_2Ebool_2EF,bool)).
tff(stp_fo_c_2Ebool_2EF,type,(fo__c_2Ebool_2EF:tp__o)).
tff(stp_eq_fo_c_2Ebool_2EF,axiom,(inj__o(fo__c_2Ebool_2EF) = c_2Ebool_2EF)).
tff(ax_false_p,axiom,(~ p(c_2Ebool_2EF))).
tff(tp_c_2Emin_2E_3D_3D_3E,type,(c_2Emin_2E_3D_3D_3E:$i)).
tff(mem_c_2Emin_2E_3D_3D_3E,axiom,mem(c_2Emin_2E_3D_3D_3E,arr(bool,arr(bool,bool)))).
tff(stp_fo_c_2Emin_2E_3D_3D_3E,type,(fo__c_2Emin_2E_3D_3D_3E:(tp__o * tp__o) > tp__o)).
tff(stp_eq_fo_c_2Emin_2E_3D_3D_3E,axiom,( ! [X0:tp__o] : ( ! [X1:tp__o] : (inj__o(fo__c_2Emin_2E_3D_3D_3E(X0,X1)) = ap(ap(c_2Emin_2E_3D_3D_3E,inj__o(X0)),inj__o(X1)))))).
tff(ax_imp_p,axiom,( ! [Q:$i] : (mem(Q,bool) => ( ! [R:$i] : (mem(R,bool) => (p(ap(ap(c_2Emin_2E_3D_3D_3E,Q),R)) <=> (p(Q) => p(R)))))))).
tff(tp_c_2Ebool_2E_5C_2F,type,(c_2Ebool_2E_5C_2F:$i)).
tff(mem_c_2Ebool_2E_5C_2F,axiom,mem(c_2Ebool_2E_5C_2F,arr(bool,arr(bool,bool)))).
tff(stp_fo_c_2Ebool_2E_5C_2F,type,(fo__c_2Ebool_2E_5C_2F:(tp__o * tp__o) > tp__o)).
tff(stp_eq_fo_c_2Ebool_2E_5C_2F,axiom,( ! [X0:tp__o] : ( ! [X1:tp__o] : (inj__o(fo__c_2Ebool_2E_5C_2F(X0,X1)) = ap(ap(c_2Ebool_2E_5C_2F,inj__o(X0)),inj__o(X1)))))).
tff(ax_or_p,axiom,( ! [Q:$i] : (mem(Q,bool) => ( ! [R:$i] : (mem(R,bool) => (p(ap(ap(c_2Ebool_2E_5C_2F,Q),R)) <=> (p(Q) | p(R)))))))).
tff(tp_c_2Ebool_2E_2F_5C,type,(c_2Ebool_2E_2F_5C:$i)).
tff(mem_c_2Ebool_2E_2F_5C,axiom,mem(c_2Ebool_2E_2F_5C,arr(bool,arr(bool,bool)))).
tff(stp_fo_c_2Ebool_2E_2F_5C,type,(fo__c_2Ebool_2E_2F_5C:(tp__o * tp__o) > tp__o)).
tff(stp_eq_fo_c_2Ebool_2E_2F_5C,axiom,( ! [X0:tp__o] : ( ! [X1:tp__o] : (inj__o(fo__c_2Ebool_2E_2F_5C(X0,X1)) = ap(ap(c_2Ebool_2E_2F_5C,inj__o(X0)),inj__o(X1)))))).
tff(ax_and_p,axiom,( ! [Q:$i] : (mem(Q,bool) => ( ! [R:$i] : (mem(R,bool) => (p(ap(ap(c_2Ebool_2E_2F_5C,Q),R)) <=> (p(Q) & p(R)))))))).
tff(tp_c_2Ebool_2E_7E,type,(c_2Ebool_2E_7E:$i)).
tff(mem_c_2Ebool_2E_7E,axiom,mem(c_2Ebool_2E_7E,arr(bool,bool))).
tff(stp_fo_c_2Ebool_2E_7E,type,(fo__c_2Ebool_2E_7E:(tp__o) > tp__o)).
tff(stp_eq_fo_c_2Ebool_2E_7E,axiom,( ! [X0:tp__o] : (inj__o(fo__c_2Ebool_2E_7E(X0)) = ap(c_2Ebool_2E_7E,inj__o(X0))))).
tff(ax_neg_p,axiom,( ! [Q:$i] : (mem(Q,bool) => (p(ap(c_2Ebool_2E_7E,Q)) <=> (~ p(Q)))))).
tff(tp_c_2Emin_2E_3D,type,(c_2Emin_2E_3D:del > $i)).
tff(mem_c_2Emin_2E_3D,axiom,( ! [A_27a:del] : mem(c_2Emin_2E_3D(A_27a),arr(A_27a,arr(A_27a,bool))))).
tff(ax_eq_p,axiom,( ! [A:del] : ( ! [X:$i] : (mem(X,A) => ( ! [Y:$i] : (mem(Y,A) => (p(ap(ap(c_2Emin_2E_3D(A),X),Y)) <=> (X = Y)))))))).
tff(tp_c_2Ebool_2E_21,type,(c_2Ebool_2E_21:del > $i)).
tff(mem_c_2Ebool_2E_21,axiom,( ! [A_27a:del] : mem(c_2Ebool_2E_21(A_27a),arr(arr(A_27a,bool),bool)))).
tff(ax_all_p,axiom,( ! [A:del] : ( ! [Q:$i] : (mem(Q,arr(A,bool)) => (p(ap(c_2Ebool_2E_21(A),Q)) <=> ( ! [X:$i] : (mem(X,A) => p(ap(Q,X))))))))).
tff(ax_thm_2Earithmetic_2EGREATER__DEF,axiom,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3E,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V0m))))))).
tff(conj_thm_2Earithmetic_2ETWO,lemma,((surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))) = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))).
tff(conj_thm_2Earithmetic_2EADD__CLAUSES,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0m))) = V0m) & ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = V0m) & ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0m))),inj__ty_2Enum_2Enum(V1n))) = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))))) & (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1n)))) = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))))))))))).
tff(conj_thm_2Earithmetic_2EADD__SYM,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V0m)))))))).
tff(conj_thm_2Earithmetic_2EADD__ASSOC,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(V2p))))))))).
tff(conj_thm_2Earithmetic_2ELESS__EQ,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0m))),inj__ty_2Enum_2Enum(V1n)))))))).
tff(conj_thm_2Earithmetic_2EZERO__LESS__EQ,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n)))))).
tff(conj_thm_2Earithmetic_2ENOT__LESS,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((~~ p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V0m)))))))).
tff(conj_thm_2Earithmetic_2EMULT__CLAUSES,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0m))) = fo__c_2Enum_2E0) & ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = fo__c_2Enum_2E0) & ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(V0m))) = V0m) & ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) = V0m) & ((surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0m))),inj__ty_2Enum_2Enum(V1n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(V1n)))) & (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1n)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n)))))))))))))).
tff(conj_thm_2Earithmetic_2EPRE__SUC__EQ,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V1n))) => ((V0m = surj__ty_2Enum_2Enum(ap(c_2Eprim__rec_2EPRE,inj__ty_2Enum_2Enum(V1n)))) <=> (surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0m))) = V1n))))))).
tff(conj_thm_2Earithmetic_2ELESS__EQ__TRANS,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) & p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p)))) => p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2p))))))))).
tff(conj_thm_2Earithmetic_2EEQ__LESS__EQ,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((V0m = V1n) <=> (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))) & p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V0m))))))))).
tff(conj_thm_2Earithmetic_2EADD__MONO__LESS__EQ,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V1n))),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0m)),inj__ty_2Enum_2Enum(V2p)))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(V2p))))))))).
tff(conj_thm_2Earithmetic_2ENOT__NUM__EQ,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((~~ (V0m = V1n)) <=> (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0m))),inj__ty_2Enum_2Enum(V1n))) | p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1n))),inj__ty_2Enum_2Enum(V0m))))))))).
tff(conj_thm_2Earithmetic_2ESUC__ONE__ADD,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(V0n))))))).
tff(conj_thm_2Ebool_2ETRUTH,lemma,($true)).
tff(conj_thm_2Ebool_2EIMP__ANTISYM__AX,lemma,(( ! [V0t1:tp__o] : ( ! [V1t2:tp__o] : ((p(inj__o(V0t1)) => p(inj__o(V1t2))) => ((p(inj__o(V1t2)) => p(inj__o(V0t1))) => (p(inj__o(V0t1)) <=> p(inj__o(V1t2))))))))).
tff(conj_thm_2Ebool_2EFALSITY,lemma,(( ! [V0t:tp__o] : ($false => p(inj__o(V0t)))))).
tff(conj_thm_2Ebool_2EFORALL__SIMP,lemma,(( ! [A_27a:del]: ( ! [V0t:tp__o] : (( ! [V1x:$i] : (mem(V1x,A_27a) => p(inj__o(V0t)))) <=> p(inj__o(V0t))))))).
tff(conj_thm_2Ebool_2EAND__CLAUSES,lemma,(( ! [V0t:tp__o] : ((($true & p(inj__o(V0t))) <=> p(inj__o(V0t))) & (((p(inj__o(V0t)) & $true) <=> p(inj__o(V0t))) & ((($false & p(inj__o(V0t))) <=> $false) & (((p(inj__o(V0t)) & $false) <=> $false) & ((p(inj__o(V0t)) & p(inj__o(V0t))) <=> p(inj__o(V0t)))))))))).
tff(conj_thm_2Ebool_2EOR__CLAUSES,lemma,(( ! [V0t:tp__o] : ((($true | p(inj__o(V0t))) <=> $true) & (((p(inj__o(V0t)) | $true) <=> $true) & ((($false | p(inj__o(V0t))) <=> p(inj__o(V0t))) & (((p(inj__o(V0t)) | $false) <=> p(inj__o(V0t))) & ((p(inj__o(V0t)) | p(inj__o(V0t))) <=> p(inj__o(V0t)))))))))).
tff(conj_thm_2Ebool_2ENOT__CLAUSES,lemma,((( ! [V0t:tp__o] : ((~~ (~~ p(inj__o(V0t)))) <=> p(inj__o(V0t)))) & (((~~ ($true)) <=> $false) & ((~~ ($false)) <=> $true))))).
tff(conj_thm_2Ebool_2EREFL__CLAUSE,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ((V0x = V0x) <=> $true)))))).
tff(conj_thm_2Ebool_2EEQ__SYM__EQ,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1y:$i] : (mem(V1y,A_27a) => ((V0x = V1y) <=> (V1y = V0x))))))))).
tff(conj_thm_2Ebool_2EEQ__CLAUSES,lemma,(( ! [V0t:tp__o] : ((($true <=> p(inj__o(V0t))) <=> p(inj__o(V0t))) & (((p(inj__o(V0t)) <=> $true) <=> p(inj__o(V0t))) & ((($false <=> p(inj__o(V0t))) <=> (~~ p(inj__o(V0t)))) & ((p(inj__o(V0t)) <=> $false) <=> (~~ p(inj__o(V0t)))))))))).
tff(conj_thm_2Ebool_2EDISJ__ASSOC,lemma,(( ! [V0A:tp__o] : ( ! [V1B:tp__o] : ( ! [V2C:tp__o] : ((p(inj__o(V0A)) | (p(inj__o(V1B)) | p(inj__o(V2C)))) <=> ((p(inj__o(V0A)) | p(inj__o(V1B))) | p(inj__o(V2C))))))))).
tff(conj_thm_2Ebool_2EDE__MORGAN__THM,lemma,(( ! [V0A:tp__o] : ( ! [V1B:tp__o] : (((~~ (p(inj__o(V0A)) & p(inj__o(V1B)))) <=> ((~~ p(inj__o(V0A))) | (~~ p(inj__o(V1B))))) & ((~~ (p(inj__o(V0A)) | p(inj__o(V1B)))) <=> ((~~ p(inj__o(V0A))) & (~~ p(inj__o(V1B)))))))))).
tff(conj_thm_2Ebool_2EIMP__F__EQ__F,lemma,(( ! [V0t:tp__o] : ((p(inj__o(V0t)) => $false) <=> (p(inj__o(V0t)) <=> $false))))).
tff(conj_thm_2Ebool_2EAND__IMP__INTRO,lemma,(( ! [V0t1:tp__o] : ( ! [V1t2:tp__o] : ( ! [V2t3:tp__o] : ((p(inj__o(V0t1)) => (p(inj__o(V1t2)) => p(inj__o(V2t3)))) <=> ((p(inj__o(V0t1)) & p(inj__o(V1t2))) => p(inj__o(V2t3))))))))).
tff(conj_thm_2Ebool_2EEQ__EXPAND,lemma,(( ! [V0t1:tp__o] : ( ! [V1t2:tp__o] : ((p(inj__o(V0t1)) <=> p(inj__o(V1t2))) <=> ((p(inj__o(V0t1)) & p(inj__o(V1t2))) | ((~~ p(inj__o(V0t1))) & (~~ p(inj__o(V1t2)))))))))).
tff(ax_thm_2Elist_2EHD,axiom,( ! [A_27a:del]: ( ! [V0h:$i] : (mem(V0h,A_27a) => ( ! [V1t:$i] : (mem(V1t,ty_2Elist_2Elist(A_27a)) => (ap(c_2Elist_2EHD(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V0h),V1t)) = V0h))))))).
tff(ax_thm_2Elist_2ETL__DEF,axiom,( ! [A_27a:del]: ((ap(c_2Elist_2ETL(A_27a),c_2Elist_2ENIL(A_27a)) = c_2Elist_2ENIL(A_27a)) & ( ! [V0h:$i] : (mem(V0h,A_27a) => ( ! [V1t:$i] : (mem(V1t,ty_2Elist_2Elist(A_27a)) => (ap(c_2Elist_2ETL(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V0h),V1t)) = V1t)))))))).
tff(ax_thm_2Elist_2ELENGTH,axiom,( ! [A_27a:del]: ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),c_2Elist_2ENIL(A_27a))) = fo__c_2Enum_2E0) & ( ! [V0h:$i] : (mem(V0h,A_27a) => ( ! [V1t:$i] : (mem(V1t,ty_2Elist_2Elist(A_27a)) => (surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V0h),V1t))) = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(c_2Elist_2ELENGTH(A_27a),V1t))))))))))).
tff(conj_thm_2Elist_2Elist__nchotomy,lemma,(( ! [A_27a:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => ((V0l = c_2Elist_2ENIL(A_27a)) | (? [V1h:$i] : (mem(V1h,A_27a) & (? [V2t:$i] : (mem(V2t,ty_2Elist_2Elist(A_27a)) & (V0l = ap(ap(c_2Elist_2ECONS(A_27a),V1h),V2t)))))))))))).
tff(conj_thm_2Elist_2ECONS__11,lemma,(( ! [A_27a:del]: ( ! [V0a0:$i] : (mem(V0a0,A_27a) => ( ! [V1a1:$i] : (mem(V1a1,ty_2Elist_2Elist(A_27a)) => ( ! [V2a0_27:$i] : (mem(V2a0_27,A_27a) => ( ! [V3a1_27:$i] : (mem(V3a1_27,ty_2Elist_2Elist(A_27a)) => ((ap(ap(c_2Elist_2ECONS(A_27a),V0a0),V1a1) = ap(ap(c_2Elist_2ECONS(A_27a),V2a0_27),V3a1_27)) <=> ((V0a0 = V2a0_27) & (V1a1 = V3a1_27)))))))))))))).
tff(conj_thm_2Elist_2ENOT__NIL__CONS,lemma,(( ! [A_27a:del]: ( ! [V0a1:$i] : (mem(V0a1,ty_2Elist_2Elist(A_27a)) => ( ! [V1a0:$i] : (mem(V1a0,A_27a) => (~~ (c_2Elist_2ENIL(A_27a) = ap(ap(c_2Elist_2ECONS(A_27a),V1a0),V0a1)))))))))).
tff(conj_thm_2Elist_2ELENGTH__NIL,lemma,(( ! [A_27a:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => ((surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V0l)) = fo__c_2Enum_2E0) <=> (V0l = c_2Elist_2ENIL(A_27a)))))))).
tff(conj_thm_2Enumeral_2Enumeral__suc,lemma,(((surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))) & (( ! [V0n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n)))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n))))) & ( ! [V1n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1n)))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT1,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1n)))))))))).
tff(conj_thm_2Enumeral_2Enumeral__distrib,lemma,((( ! [V0n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0n))) = V0n)) & (( ! [V1n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1n)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = V1n)) & (( ! [V2n:tp__ty_2Enum_2Enum] : ( ! [V3m:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V2n))),ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V3m)))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Enumeral_2EiZ,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V2n)),inj__ty_2Enum_2Enum(V3m)))))))) & (( ! [V4n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V4n))) = fo__c_2Enum_2E0)) & (( ! [V5n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V5n)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = fo__c_2Enum_2E0)) & (( ! [V6n:tp__ty_2Enum_2Enum] : ( ! [V7m:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V6n))),ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V7m)))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V6n)),inj__ty_2Enum_2Enum(V7m))))))) & (( ! [V8n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V8n))) = fo__c_2Enum_2E0)) & (( ! [V9n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V9n)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = V9n)) & (( ! [V10n:tp__ty_2Enum_2Enum] : ( ! [V11m:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2D,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V10n))),ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V11m)))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V10n)),inj__ty_2Enum_2Enum(V11m))))))) & (( ! [V12n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EEXP,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V12n))))) = fo__c_2Enum_2E0)) & (( ! [V13n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EEXP,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V13n))))) = fo__c_2Enum_2E0)) & (( ! [V14n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EEXP,inj__ty_2Enum_2Enum(V14n)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))) & (( ! [V15n:tp__ty_2Enum_2Enum] : ( ! [V16m:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EEXP,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V15n))),ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V16m)))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(ap(c_2Earithmetic_2EEXP,inj__ty_2Enum_2Enum(V15n)),inj__ty_2Enum_2Enum(V16m))))))) & ((surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) & (( ! [V17n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V17n)))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V17n)))))) & ((surj__ty_2Enum_2Enum(ap(c_2Eprim__rec_2EPRE,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = fo__c_2Enum_2E0) & (( ! [V18n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Eprim__rec_2EPRE,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V18n)))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Eprim__rec_2EPRE,inj__ty_2Enum_2Enum(V18n)))))) & (( ! [V19n:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V19n))) = fo__c_2Enum_2E0) <=> (V19n = fo__c_2Earithmetic_2EZERO))) & (( ! [V20n:tp__ty_2Enum_2Enum] : ((fo__c_2Enum_2E0 = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V20n)))) <=> (V20n = fo__c_2Earithmetic_2EZERO))) & (( ! [V21n:tp__ty_2Enum_2Enum] : ( ! [V22m:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V21n))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V22m)))) <=> (V21n = V22m)))) & (( ! [V23n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V23n)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) <=> $false)) & (( ! [V24n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V24n)))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)),inj__ty_2Enum_2Enum(V24n))))) & (( ! [V25n:tp__ty_2Enum_2Enum] : ( ! [V26m:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V25n))),ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V26m)))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V25n)),inj__ty_2Enum_2Enum(V26m)))))) & (( ! [V27n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3E,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V27n))) <=> $false)) & (( ! [V28n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3E,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V28n))),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)),inj__ty_2Enum_2Enum(V28n))))) & (( ! [V29n:tp__ty_2Enum_2Enum] : ( ! [V30m:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3E,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V29n))),ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V30m)))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V30m)),inj__ty_2Enum_2Enum(V29n)))))) & (( ! [V31n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V31n))) <=> $true)) & (( ! [V32n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V32n))),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V32n)),inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) & (( ! [V33n:tp__ty_2Enum_2Enum] : ( ! [V34m:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V33n))),ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V34m)))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V33n)),inj__ty_2Enum_2Enum(V34m)))))) & (( ! [V35n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3E_3D,inj__ty_2Enum_2Enum(V35n)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) <=> $true)) & (( ! [V36n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3E_3D,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V36n))) <=> (V36n = fo__c_2Enum_2E0))) & (( ! [V37n:tp__ty_2Enum_2Enum] : ( ! [V38m:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Earithmetic_2E_3E_3D,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V37n))),ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V38m)))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V38m)),inj__ty_2Enum_2Enum(V37n)))))) & (( ! [V39n:tp__ty_2Enum_2Enum] : (p(ap(c_2Earithmetic_2EODD,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V39n)))) <=> p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(V39n))))) & (( ! [V40n:tp__ty_2Enum_2Enum] : (p(ap(c_2Earithmetic_2EEVEN,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V40n)))) <=> p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V40n))))) & ((~~ p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) & p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))))))))))))))))))))))))))))))))))))))).
tff(conj_thm_2Enumeral_2Enumeral__add,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum(ap(c_2Enumeral_2EiZ,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)),inj__ty_2Enum_2Enum(V0n)))) = V0n) & ((surj__ty_2Enum_2Enum(ap(c_2Enumeral_2EiZ,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))) = V0n) & ((surj__ty_2Enum_2Enum(ap(c_2Enumeral_2EiZ,ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1m))))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,ap(c_2Enumeral_2EiZ,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))))) & ((surj__ty_2Enum_2Enum(ap(c_2Enumeral_2EiZ,ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1m))))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT1,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))))) & ((surj__ty_2Enum_2Enum(ap(c_2Enumeral_2EiZ,ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1m))))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT1,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))))) & ((surj__ty_2Enum_2Enum(ap(c_2Enumeral_2EiZ,ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1m))))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))))) & ((surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)),inj__ty_2Enum_2Enum(V0n)))) = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n)))) & ((surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))) = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V0n)))) & ((surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1m))))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT1,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))))) & ((surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1m))))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))))) & ((surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1m))))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))))) & ((surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1m))))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT1,ap(c_2Enumeral_2EiiSUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))))) & ((surj__ty_2Enum_2Enum(ap(c_2Enumeral_2EiiSUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)),inj__ty_2Enum_2Enum(V0n)))) = surj__ty_2Enum_2Enum(ap(c_2Enumeral_2EiiSUC,inj__ty_2Enum_2Enum(V0n)))) & ((surj__ty_2Enum_2Enum(ap(c_2Enumeral_2EiiSUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))) = surj__ty_2Enum_2Enum(ap(c_2Enumeral_2EiiSUC,inj__ty_2Enum_2Enum(V0n)))) & ((surj__ty_2Enum_2Enum(ap(c_2Enumeral_2EiiSUC,ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1m))))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))))) & ((surj__ty_2Enum_2Enum(ap(c_2Enumeral_2EiiSUC,ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1m))))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT1,ap(c_2Enumeral_2EiiSUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))))) & ((surj__ty_2Enum_2Enum(ap(c_2Enumeral_2EiiSUC,ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1m))))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT1,ap(c_2Enumeral_2EiiSUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))))) & (surj__ty_2Enum_2Enum(ap(c_2Enumeral_2EiiSUC,ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1m))))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,ap(c_2Enumeral_2EiiSUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m))))))))))))))))))))))))))).
tff(conj_thm_2Enumeral_2Enumeral__eq,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : (((fo__c_2Earithmetic_2EZERO = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n)))) <=> $false) & (((surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))) = fo__c_2Earithmetic_2EZERO) <=> $false) & (((fo__c_2Earithmetic_2EZERO = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n)))) <=> $false) & (((surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n))) = fo__c_2Earithmetic_2EZERO) <=> $false) & (((surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1m)))) <=> $false) & (((surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1m)))) <=> $false) & (((surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1m)))) <=> (V0n = V1m)) & ((surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1m)))) <=> (V0n = V1m))))))))))))).
tff(conj_thm_2Enumeral_2Enumeral__lt,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)),ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n)))) <=> $true) & ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)),ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n)))) <=> $true) & ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))) <=> $false) & ((p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1m)))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))) & ((p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1m)))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))) & ((p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1m)))) <=> (~~ p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V1m)),inj__ty_2Enum_2Enum(V0n))))) & (p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1m)))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))))))))))))).
tff(conj_thm_2Enumeral_2Enumeral__lte,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)),inj__ty_2Enum_2Enum(V0n))) <=> $true) & ((p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))),inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))) <=> $false) & ((p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n))),inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))) <=> $false) & ((p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1m)))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))) & ((p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1m)))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))) & ((p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1m)))) <=> (~~ p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1m)),inj__ty_2Enum_2Enum(V0n))))) & (p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V0n))),ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1m)))) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(V1m)))))))))))))).
tff(conj_thm_2Enumeral_2Enumeral__pre,lemma,(((surj__ty_2Enum_2Enum(ap(c_2Eprim__rec_2EPRE,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))) = fo__c_2Earithmetic_2EZERO) & ((surj__ty_2Enum_2Enum(ap(c_2Eprim__rec_2EPRE,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))) = fo__c_2Earithmetic_2EZERO) & (( ! [V0n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Eprim__rec_2EPRE,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,ap(c_2Eprim__rec_2EPRE,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n))))))) & (( ! [V1n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Eprim__rec_2EPRE,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V1n))))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1n)))))) & ( ! [V2n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Eprim__rec_2EPRE,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V2n)))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V2n))))))))))).
tff(conj_thm_2Esat_2ENOT__NOT,lemma,(( ! [V0t:tp__o] : ((~~ (~~ p(inj__o(V0t)))) <=> p(inj__o(V0t)))))).
tff(conj_thm_2Esat_2EAND__INV__IMP,lemma,(( ! [V0A:tp__o] : (p(inj__o(V0A)) => ((~~ p(inj__o(V0A))) => $false))))).
tff(conj_thm_2Esat_2EOR__DUAL2,lemma,(( ! [V0A:tp__o] : ( ! [V1B:tp__o] : (((~~ (p(inj__o(V0A)) | p(inj__o(V1B)))) => $false) <=> ((p(inj__o(V0A)) => $false) => ((~~ p(inj__o(V1B))) => $false))))))).
tff(conj_thm_2Esat_2EOR__DUAL3,lemma,(( ! [V0A:tp__o] : ( ! [V1B:tp__o] : (((~~ ((~~ p(inj__o(V0A))) | p(inj__o(V1B)))) => $false) <=> (p(inj__o(V0A)) => ((~~ p(inj__o(V1B))) => $false))))))).
tff(conj_thm_2Esat_2EAND__INV2,lemma,(( ! [V0A:tp__o] : (((~~ p(inj__o(V0A))) => $false) => ((p(inj__o(V0A)) => $false) => $false))))).
tff(conj_thm_2Esat_2Edc__eq,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ( ! [V2r:tp__o] : ((p(inj__o(V0p)) <=> (p(inj__o(V1q)) <=> p(inj__o(V2r)))) <=> ((p(inj__o(V0p)) | (p(inj__o(V1q)) | p(inj__o(V2r)))) & ((p(inj__o(V0p)) | ((~~ p(inj__o(V2r))) | (~~ p(inj__o(V1q))))) & ((p(inj__o(V1q)) | ((~~ p(inj__o(V2r))) | (~~ p(inj__o(V0p))))) & (p(inj__o(V2r)) | ((~~ p(inj__o(V1q))) | (~~ p(inj__o(V0p)))))))))))))).
tff(conj_thm_2Esat_2Edc__conj,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ( ! [V2r:tp__o] : ((p(inj__o(V0p)) <=> (p(inj__o(V1q)) & p(inj__o(V2r)))) <=> ((p(inj__o(V0p)) | ((~~ p(inj__o(V1q))) | (~~ p(inj__o(V2r))))) & ((p(inj__o(V1q)) | (~~ p(inj__o(V0p)))) & (p(inj__o(V2r)) | (~~ p(inj__o(V0p)))))))))))).
tff(conj_thm_2Esat_2Edc__disj,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ( ! [V2r:tp__o] : ((p(inj__o(V0p)) <=> (p(inj__o(V1q)) | p(inj__o(V2r)))) <=> ((p(inj__o(V0p)) | (~~ p(inj__o(V1q)))) & ((p(inj__o(V0p)) | (~~ p(inj__o(V2r)))) & (p(inj__o(V1q)) | (p(inj__o(V2r)) | (~~ p(inj__o(V0p))))))))))))).
tff(conj_thm_2Esat_2Edc__neg,lemma,(( ! [V0p:tp__o] : ( ! [V1q:tp__o] : ((p(inj__o(V0p)) <=> (~~ p(inj__o(V1q)))) <=> ((p(inj__o(V0p)) | p(inj__o(V1q))) & ((~~ p(inj__o(V1q))) | (~~ p(inj__o(V0p)))))))))).
tff(conj_thm_2EquantHeuristics_2EHD__TL__EQ__THMS,conjecture,(( ! [A_27a:del]: (( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => ((ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),V0l)),ap(c_2Elist_2ETL(A_27a),V0l)) = V0l) <=> (~~ (V0l = c_2Elist_2ENIL(A_27a)))))) & (( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(A_27a)) => ((ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),V1l)),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),V1l))),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V1l)))) = V1l) <=> p(ap(ap(c_2Earithmetic_2E_3E,ap(c_2Elist_2ELENGTH(A_27a),V1l)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))) & (( ! [V2l:$i] : (mem(V2l,ty_2Elist_2Elist(A_27a)) => ((ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),V2l)),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),V2l))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V2l)))),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V2l)))))) = V2l) <=> p(ap(ap(c_2Earithmetic_2E_3E,ap(c_2Elist_2ELENGTH(A_27a),V2l)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))) & (( ! [V3l:$i] : (mem(V3l,ty_2Elist_2Elist(A_27a)) => ((ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),V3l)),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),V3l))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V3l)))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V3l))))),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V3l)))))))) = V3l) <=> p(ap(ap(c_2Earithmetic_2E_3E,ap(c_2Elist_2ELENGTH(A_27a),V3l)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))) & (( ! [V4l:$i] : (mem(V4l,ty_2Elist_2Elist(A_27a)) => ((ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),V4l)),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),V4l))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V4l)))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V4l))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V4l)))))),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V4l)))))))))) = V4l) <=> p(ap(ap(c_2Earithmetic_2E_3E,ap(c_2Elist_2ELENGTH(A_27a),V4l)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))) & (( ! [V5l:$i] : (mem(V5l,ty_2Elist_2Elist(A_27a)) => ((ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),V5l)),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),V5l))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V5l)))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V5l))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V5l)))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V5l))))))),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V5l)))))))))))) = V5l) <=> p(ap(ap(c_2Earithmetic_2E_3E,ap(c_2Elist_2ELENGTH(A_27a),V5l)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))) & (( ! [V6l:$i] : (mem(V6l,ty_2Elist_2Elist(A_27a)) => ((ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),V6l)),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),V6l))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V6l)))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V6l))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V6l)))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V6l))))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V6l)))))))),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V6l)))))))))))))) = V6l) <=> p(ap(ap(c_2Earithmetic_2E_3E,ap(c_2Elist_2ELENGTH(A_27a),V6l)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))) & (( ! [V7l:$i] : (mem(V7l,ty_2Elist_2Elist(A_27a)) => ((ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),V7l)),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),V7l))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V7l)))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V7l))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V7l)))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V7l))))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V7l)))))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V7l))))))))),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V7l)))))))))))))))) = V7l) <=> p(ap(ap(c_2Earithmetic_2E_3E,ap(c_2Elist_2ELENGTH(A_27a),V7l)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))) & (( ! [V8l:$i] : (mem(V8l,ty_2Elist_2Elist(A_27a)) => ((ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),V8l)),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),V8l))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V8l)))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V8l))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V8l)))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V8l))))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V8l)))))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V8l))))))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V8l)))))))))),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V8l)))))))))))))))))) = V8l) <=> p(ap(ap(c_2Earithmetic_2E_3E,ap(c_2Elist_2ELENGTH(A_27a),V8l)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))) & (( ! [V9l:$i] : (mem(V9l,ty_2Elist_2Elist(A_27a)) => ((ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),V9l)),c_2Elist_2ENIL(A_27a)) = V9l) <=> (surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V9l)) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))) & (( ! [V10l:$i] : (mem(V10l,ty_2Elist_2Elist(A_27a)) => ((ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),V10l)),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),V10l))),c_2Elist_2ENIL(A_27a))) = V10l) <=> (surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V10l)) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))) & (( ! [V11l:$i] : (mem(V11l,ty_2Elist_2Elist(A_27a)) => ((ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),V11l)),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),V11l))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V11l)))),c_2Elist_2ENIL(A_27a)))) = V11l) <=> (surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V11l)) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))) & (( ! [V12l:$i] : (mem(V12l,ty_2Elist_2Elist(A_27a)) => ((ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),V12l)),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),V12l))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V12l)))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V12l))))),c_2Elist_2ENIL(A_27a))))) = V12l) <=> (surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V12l)) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))) & (( ! [V13l:$i] : (mem(V13l,ty_2Elist_2Elist(A_27a)) => ((ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),V13l)),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),V13l))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V13l)))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V13l))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V13l)))))),c_2Elist_2ENIL(A_27a)))))) = V13l) <=> (surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V13l)) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))) & (( ! [V14l:$i] : (mem(V14l,ty_2Elist_2Elist(A_27a)) => ((ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),V14l)),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),V14l))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V14l)))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V14l))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V14l)))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V14l))))))),c_2Elist_2ENIL(A_27a))))))) = V14l) <=> (surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V14l)) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))) & (( ! [V15l:$i] : (mem(V15l,ty_2Elist_2Elist(A_27a)) => ((ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),V15l)),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),V15l))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V15l)))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V15l))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V15l)))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V15l))))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V15l)))))))),c_2Elist_2ENIL(A_27a)))))))) = V15l) <=> (surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V15l)) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))) & (( ! [V16l:$i] : (mem(V16l,ty_2Elist_2Elist(A_27a)) => ((ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),V16l)),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),V16l))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V16l)))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V16l))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V16l)))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V16l))))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V16l)))))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V16l))))))))),c_2Elist_2ENIL(A_27a))))))))) = V16l) <=> (surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V16l)) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))) & (( ! [V17l:$i] : (mem(V17l,ty_2Elist_2Elist(A_27a)) => ((ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),V17l)),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),V17l))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V17l)))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V17l))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V17l)))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V17l))))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V17l)))))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V17l))))))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V17l)))))))))),c_2Elist_2ENIL(A_27a)))))))))) = V17l) <=> (surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V17l)) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))) & (( ! [V18l:$i] : (mem(V18l,ty_2Elist_2Elist(A_27a)) => ((V18l = ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),V18l)),ap(c_2Elist_2ETL(A_27a),V18l))) <=> (~~ (V18l = c_2Elist_2ENIL(A_27a)))))) & (( ! [V19l:$i] : (mem(V19l,ty_2Elist_2Elist(A_27a)) => ((V19l = ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),V19l)),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),V19l))),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V19l))))) <=> p(ap(ap(c_2Earithmetic_2E_3E,ap(c_2Elist_2ELENGTH(A_27a),V19l)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))) & (( ! [V20l:$i] : (mem(V20l,ty_2Elist_2Elist(A_27a)) => ((V20l = ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),V20l)),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),V20l))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V20l)))),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V20l))))))) <=> p(ap(ap(c_2Earithmetic_2E_3E,ap(c_2Elist_2ELENGTH(A_27a),V20l)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))) & (( ! [V21l:$i] : (mem(V21l,ty_2Elist_2Elist(A_27a)) => ((V21l = ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),V21l)),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),V21l))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V21l)))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V21l))))),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V21l))))))))) <=> p(ap(ap(c_2Earithmetic_2E_3E,ap(c_2Elist_2ELENGTH(A_27a),V21l)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))) & (( ! [V22l:$i] : (mem(V22l,ty_2Elist_2Elist(A_27a)) => ((V22l = ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),V22l)),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),V22l))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V22l)))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V22l))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V22l)))))),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V22l))))))))))) <=> p(ap(ap(c_2Earithmetic_2E_3E,ap(c_2Elist_2ELENGTH(A_27a),V22l)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))) & (( ! [V23l:$i] : (mem(V23l,ty_2Elist_2Elist(A_27a)) => ((V23l = ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),V23l)),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),V23l))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V23l)))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V23l))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V23l)))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V23l))))))),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V23l))))))))))))) <=> p(ap(ap(c_2Earithmetic_2E_3E,ap(c_2Elist_2ELENGTH(A_27a),V23l)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))) & (( ! [V24l:$i] : (mem(V24l,ty_2Elist_2Elist(A_27a)) => ((V24l = ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),V24l)),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),V24l))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V24l)))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V24l))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V24l)))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V24l))))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V24l)))))))),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V24l))))))))))))))) <=> p(ap(ap(c_2Earithmetic_2E_3E,ap(c_2Elist_2ELENGTH(A_27a),V24l)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))) & (( ! [V25l:$i] : (mem(V25l,ty_2Elist_2Elist(A_27a)) => ((V25l = ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),V25l)),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),V25l))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V25l)))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V25l))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V25l)))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V25l))))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V25l)))))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V25l))))))))),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V25l))))))))))))))))) <=> p(ap(ap(c_2Earithmetic_2E_3E,ap(c_2Elist_2ELENGTH(A_27a),V25l)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))) & (( ! [V26l:$i] : (mem(V26l,ty_2Elist_2Elist(A_27a)) => ((V26l = ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),V26l)),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),V26l))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V26l)))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V26l))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V26l)))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V26l))))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V26l)))))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V26l))))))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V26l)))))))))),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V26l))))))))))))))))))) <=> p(ap(ap(c_2Earithmetic_2E_3E,ap(c_2Elist_2ELENGTH(A_27a),V26l)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))) & (( ! [V27l:$i] : (mem(V27l,ty_2Elist_2Elist(A_27a)) => ((V27l = ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),V27l)),c_2Elist_2ENIL(A_27a))) <=> (surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V27l)) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))) & (( ! [V28l:$i] : (mem(V28l,ty_2Elist_2Elist(A_27a)) => ((V28l = ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),V28l)),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),V28l))),c_2Elist_2ENIL(A_27a)))) <=> (surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V28l)) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))) & (( ! [V29l:$i] : (mem(V29l,ty_2Elist_2Elist(A_27a)) => ((V29l = ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),V29l)),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),V29l))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V29l)))),c_2Elist_2ENIL(A_27a))))) <=> (surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V29l)) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))) & (( ! [V30l:$i] : (mem(V30l,ty_2Elist_2Elist(A_27a)) => ((V30l = ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),V30l)),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),V30l))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V30l)))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V30l))))),c_2Elist_2ENIL(A_27a)))))) <=> (surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V30l)) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))) & (( ! [V31l:$i] : (mem(V31l,ty_2Elist_2Elist(A_27a)) => ((V31l = ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),V31l)),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),V31l))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V31l)))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V31l))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V31l)))))),c_2Elist_2ENIL(A_27a))))))) <=> (surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V31l)) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))) & (( ! [V32l:$i] : (mem(V32l,ty_2Elist_2Elist(A_27a)) => ((V32l = ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),V32l)),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),V32l))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V32l)))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V32l))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V32l)))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V32l))))))),c_2Elist_2ENIL(A_27a)))))))) <=> (surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V32l)) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))) & (( ! [V33l:$i] : (mem(V33l,ty_2Elist_2Elist(A_27a)) => ((V33l = ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),V33l)),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),V33l))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V33l)))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V33l))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V33l)))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V33l))))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V33l)))))))),c_2Elist_2ENIL(A_27a))))))))) <=> (surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V33l)) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))) & (( ! [V34l:$i] : (mem(V34l,ty_2Elist_2Elist(A_27a)) => ((V34l = ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),V34l)),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),V34l))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V34l)))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V34l))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V34l)))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V34l))))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V34l)))))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V34l))))))))),c_2Elist_2ENIL(A_27a)))))))))) <=> (surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V34l)) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))) & ( ! [V35l:$i] : (mem(V35l,ty_2Elist_2Elist(A_27a)) => ((V35l = ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),V35l)),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),V35l))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V35l)))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V35l))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V35l)))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V35l))))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V35l)))))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V35l))))))))),ap(ap(c_2Elist_2ECONS(A_27a),ap(c_2Elist_2EHD(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),ap(c_2Elist_2ETL(A_27a),V35l)))))))))),c_2Elist_2ENIL(A_27a))))))))))) <=> (surj__ty_2Enum_2Enum(ap(c_2Elist_2ELENGTH(A_27a),V35l)) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,ap(c_2Earithmetic_2EBIT2,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))))))))))))))))))))))))))))))))))))))).
