include('Axioms/veblen^2.ax').
thf(tp_ty_2Epatricia_2Eptree,type,( ty_2Epatricia_2Eptree: del >del )).
thf(tp_c_2Epatricia_2EADD,type,(c_2Epatricia_2EADD:(del>$i))).
thf(mem_c_2Epatricia_2EADD,axiom,( ! [A_27a:del] : (mem@(c_2Epatricia_2EADD@A_27a)@(arr@(ty_2Epatricia_2Eptree@A_27a)@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@A_27a)@(ty_2Epatricia_2Eptree@A_27a)))))).
thf(tp_c_2Epatricia_2EADD__LIST,type,(c_2Epatricia_2EADD__LIST:(del>$i))).
thf(mem_c_2Epatricia_2EADD__LIST,axiom,( ! [A_27a:del] : (mem@(c_2Epatricia_2EADD__LIST@A_27a)@(arr@(ty_2Epatricia_2Eptree@A_27a)@(arr@(ty_2Elist_2Elist@(ty_2Epair_2Eprod@ty_2Enum_2Enum@A_27a))@(ty_2Epatricia_2Eptree@A_27a)))))).
thf(tp_c_2Epatricia_2EBRANCH,type,(c_2Epatricia_2EBRANCH:(del>$i))).
thf(mem_c_2Epatricia_2EBRANCH,axiom,( ! [A_27a:del] : (mem@(c_2Epatricia_2EBRANCH@A_27a)@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))))@(ty_2Epatricia_2Eptree@A_27a))))).
thf(tp_c_2Epatricia_2EBRANCHING__BIT,type,(c_2Epatricia_2EBRANCHING__BIT:$i)).
thf(mem_c_2Epatricia_2EBRANCHING__BIT,axiom,(mem@c_2Epatricia_2EBRANCHING__BIT@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@ty_2Enum_2Enum)))).
thf(stp_fo_c_2Epatricia_2EBRANCHING__BIT,type,(fo__c_2Epatricia_2EBRANCHING__BIT:(tp__ty_2Enum_2Enum > (tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum)))).
thf(stp_eq_fo_c_2Epatricia_2EBRANCHING__BIT,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : ((inj__ty_2Enum_2Enum @ ((fo__c_2Epatricia_2EBRANCHING__BIT @ X0) @ X1)) = (ap @ (ap @ c_2Epatricia_2EBRANCHING__BIT @ (inj__ty_2Enum_2Enum @ X0)) @ (inj__ty_2Enum_2Enum @ X1)))))).
thf(tp_c_2Epatricia_2EBranch,type,(c_2Epatricia_2EBranch:(del>$i))).
thf(mem_c_2Epatricia_2EBranch,axiom,( ! [A_27a:del] : (mem@(c_2Epatricia_2EBranch@A_27a)@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@(arr@(ty_2Epatricia_2Eptree@A_27a)@(arr@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a)))))))).
thf(tp_c_2Epatricia_2EDEPTH,type,(c_2Epatricia_2EDEPTH:(del>$i))).
thf(mem_c_2Epatricia_2EDEPTH,axiom,( ! [A_27a:del] : (mem@(c_2Epatricia_2EDEPTH@A_27a)@(arr@(ty_2Epatricia_2Eptree@A_27a)@ty_2Enum_2Enum)))).
thf(tp_c_2Epatricia_2EEVERY__LEAF,type,(c_2Epatricia_2EEVERY__LEAF:(del>$i))).
thf(mem_c_2Epatricia_2EEVERY__LEAF,axiom,( ! [A_27a:del] : (mem@(c_2Epatricia_2EEVERY__LEAF@A_27a)@(arr@(arr@ty_2Enum_2Enum@(arr@A_27a@bool))@(arr@(ty_2Epatricia_2Eptree@A_27a)@bool))))).
thf(tp_c_2Epatricia_2EEXISTS__LEAF,type,(c_2Epatricia_2EEXISTS__LEAF:(del>$i))).
thf(mem_c_2Epatricia_2EEXISTS__LEAF,axiom,( ! [A_27a:del] : (mem@(c_2Epatricia_2EEXISTS__LEAF@A_27a)@(arr@(arr@ty_2Enum_2Enum@(arr@A_27a@bool))@(arr@(ty_2Epatricia_2Eptree@A_27a)@bool))))).
thf(tp_c_2Epatricia_2EEmpty,type,(c_2Epatricia_2EEmpty:(del>$i))).
thf(mem_c_2Epatricia_2EEmpty,axiom,( ! [A_27a:del] : (mem@(c_2Epatricia_2EEmpty@A_27a)@(ty_2Epatricia_2Eptree@A_27a)))).
thf(tp_c_2Epatricia_2EFIND,type,(c_2Epatricia_2EFIND:(del>$i))).
thf(mem_c_2Epatricia_2EFIND,axiom,( ! [A_27a:del] : (mem@(c_2Epatricia_2EFIND@A_27a)@(arr@(ty_2Epatricia_2Eptree@A_27a)@(arr@ty_2Enum_2Enum@A_27a))))).
thf(stp_c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone,type,(tp__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone : $tType)).
thf(stp_inj_c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone,type,(inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone : (tp__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone > $i))).
thf(stp_surj_c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone,type,(surj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone : ($i > tp__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone))).
thf(stp_inj_surj_c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone] : ((surj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone @ (inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone @ X)) = X))).
thf(stp_inj_mem_c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone] : (mem @ (inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone @ X) @ (ty_2Epatricia_2Eptree@ty_2Eone_2Eone)))).
thf(stp_iso_mem_c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Epatricia_2Eptree@ty_2Eone_2Eone)) => (X = (inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone @ (surj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone @ X)))))).
thf(tp_c_2Epatricia_2EINSERT__PTREE,type,(c_2Epatricia_2EINSERT__PTREE:$i)).
thf(mem_c_2Epatricia_2EINSERT__PTREE,axiom,(mem@c_2Epatricia_2EINSERT__PTREE@(arr@ty_2Enum_2Enum@(arr@(ty_2Epatricia_2Eptree@ty_2Eone_2Eone)@(ty_2Epatricia_2Eptree@ty_2Eone_2Eone))))).
thf(tp_c_2Epatricia_2EIN__PTREE,type,(c_2Epatricia_2EIN__PTREE:$i)).
thf(mem_c_2Epatricia_2EIN__PTREE,axiom,(mem@c_2Epatricia_2EIN__PTREE@(arr@ty_2Enum_2Enum@(arr@(ty_2Epatricia_2Eptree@ty_2Eone_2Eone)@bool)))).
thf(tp_c_2Epatricia_2EIS__EMPTY,type,(c_2Epatricia_2EIS__EMPTY:(del>$i))).
thf(mem_c_2Epatricia_2EIS__EMPTY,axiom,( ! [A_27a:del] : (mem@(c_2Epatricia_2EIS__EMPTY@A_27a)@(arr@(ty_2Epatricia_2Eptree@A_27a)@bool)))).
thf(tp_c_2Epatricia_2EIS__PTREE,type,(c_2Epatricia_2EIS__PTREE:(del>$i))).
thf(mem_c_2Epatricia_2EIS__PTREE,axiom,( ! [A_27a:del] : (mem@(c_2Epatricia_2EIS__PTREE@A_27a)@(arr@(ty_2Epatricia_2Eptree@A_27a)@bool)))).
thf(tp_c_2Epatricia_2EJOIN,type,(c_2Epatricia_2EJOIN:(del>$i))).
thf(mem_c_2Epatricia_2EJOIN,axiom,( ! [A_27a:del] : (mem@(c_2Epatricia_2EJOIN@A_27a)@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epatricia_2Eptree@A_27a))))@(ty_2Epatricia_2Eptree@A_27a))))).
thf(tp_c_2Epatricia_2EKEYS,type,(c_2Epatricia_2EKEYS:(del>$i))).
thf(mem_c_2Epatricia_2EKEYS,axiom,( ! [A_27a:del] : (mem@(c_2Epatricia_2EKEYS@A_27a)@(arr@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Elist_2Elist@ty_2Enum_2Enum))))).
thf(tp_c_2Epatricia_2ELeaf,type,(c_2Epatricia_2ELeaf:(del>$i))).
thf(mem_c_2Epatricia_2ELeaf,axiom,( ! [A_27a:del] : (mem@(c_2Epatricia_2ELeaf@A_27a)@(arr@ty_2Enum_2Enum@(arr@A_27a@(ty_2Epatricia_2Eptree@A_27a)))))).
thf(tp_c_2Epatricia_2ENUMSET__OF__PTREE,type,(c_2Epatricia_2ENUMSET__OF__PTREE:$i)).
thf(mem_c_2Epatricia_2ENUMSET__OF__PTREE,axiom,(mem@c_2Epatricia_2ENUMSET__OF__PTREE@(arr@(ty_2Epatricia_2Eptree@ty_2Eone_2Eone)@(arr@ty_2Enum_2Enum@bool)))).
thf(tp_c_2Epatricia_2EPEEK,type,(c_2Epatricia_2EPEEK:(del>$i))).
thf(mem_c_2Epatricia_2EPEEK,axiom,( ! [A_27a:del] : (mem@(c_2Epatricia_2EPEEK@A_27a)@(arr@(ty_2Epatricia_2Eptree@A_27a)@(arr@ty_2Enum_2Enum@(ty_2Eoption_2Eoption@A_27a)))))).
thf(tp_c_2Epatricia_2EPTREE__OF__NUMSET,type,(c_2Epatricia_2EPTREE__OF__NUMSET:$i)).
thf(mem_c_2Epatricia_2EPTREE__OF__NUMSET,axiom,(mem@c_2Epatricia_2EPTREE__OF__NUMSET@(arr@(ty_2Epatricia_2Eptree@ty_2Eone_2Eone)@(arr@(arr@ty_2Enum_2Enum@bool)@(ty_2Epatricia_2Eptree@ty_2Eone_2Eone))))).
thf(tp_c_2Epatricia_2EREMOVE,type,(c_2Epatricia_2EREMOVE:(del>$i))).
thf(mem_c_2Epatricia_2EREMOVE,axiom,( ! [A_27a:del] : (mem@(c_2Epatricia_2EREMOVE@A_27a)@(arr@(ty_2Epatricia_2Eptree@A_27a)@(arr@ty_2Enum_2Enum@(ty_2Epatricia_2Eptree@A_27a)))))).
thf(tp_c_2Epatricia_2ESIZE,type,(c_2Epatricia_2ESIZE:(del>$i))).
thf(mem_c_2Epatricia_2ESIZE,axiom,( ! [A_27a:del] : (mem@(c_2Epatricia_2ESIZE@A_27a)@(arr@(ty_2Epatricia_2Eptree@A_27a)@ty_2Enum_2Enum)))).
thf(tp_c_2Epatricia_2ETRANSFORM,type,(c_2Epatricia_2ETRANSFORM:(del>(del>$i)))).
thf(mem_c_2Epatricia_2ETRANSFORM,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Epatricia_2ETRANSFORM@A_27a@A_27b)@(arr@(arr@A_27b@A_27a)@(arr@(ty_2Epatricia_2Eptree@A_27b)@(ty_2Epatricia_2Eptree@A_27a))))))).
thf(tp_c_2Epatricia_2ETRAVERSE,type,(c_2Epatricia_2ETRAVERSE:(del>$i))).
thf(mem_c_2Epatricia_2ETRAVERSE,axiom,( ! [A_27a:del] : (mem@(c_2Epatricia_2ETRAVERSE@A_27a)@(arr@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Elist_2Elist@ty_2Enum_2Enum))))).
thf(tp_c_2Epatricia_2ETRAVERSE__AUX,type,(c_2Epatricia_2ETRAVERSE__AUX:(del>$i))).
thf(mem_c_2Epatricia_2ETRAVERSE__AUX,axiom,( ! [A_27a:del] : (mem@(c_2Epatricia_2ETRAVERSE__AUX@A_27a)@(arr@(ty_2Epatricia_2Eptree@A_27a)@(arr@(ty_2Elist_2Elist@ty_2Enum_2Enum)@(ty_2Elist_2Elist@ty_2Enum_2Enum)))))).
thf(tp_c_2Epatricia_2EUNION__PTREE,type,(c_2Epatricia_2EUNION__PTREE:$i)).
thf(mem_c_2Epatricia_2EUNION__PTREE,axiom,(mem@c_2Epatricia_2EUNION__PTREE@(arr@(ty_2Epatricia_2Eptree@ty_2Eone_2Eone)@(arr@(ty_2Epatricia_2Eptree@ty_2Eone_2Eone)@(ty_2Epatricia_2Eptree@ty_2Eone_2Eone))))).
thf(tp_c_2Epatricia_2Eptree__CASE,type,(c_2Epatricia_2Eptree__CASE:(del>(del>$i)))).
thf(mem_c_2Epatricia_2Eptree__CASE,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Epatricia_2Eptree__CASE@A_27a@A_27b)@(arr@(ty_2Epatricia_2Eptree@A_27a)@(arr@A_27b@(arr@(arr@ty_2Enum_2Enum@(arr@A_27a@A_27b))@(arr@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@(arr@(ty_2Epatricia_2Eptree@A_27a)@(arr@(ty_2Epatricia_2Eptree@A_27a)@A_27b))))@A_27b)))))))).
thf(tp_c_2Epatricia_2Eptree__size,type,(c_2Epatricia_2Eptree__size:(del>$i))).
thf(mem_c_2Epatricia_2Eptree__size,axiom,( ! [A_27a:del] : (mem@(c_2Epatricia_2Eptree__size@A_27a)@(arr@(arr@A_27a@ty_2Enum_2Enum)@(arr@(ty_2Epatricia_2Eptree@A_27a)@ty_2Enum_2Enum))))).
thf(ax_thm_2Epatricia_2Eptree__TY__DEF,axiom,( ! [A_27a:del]: (? [V0rep:$i] : ((mem@V0rep@(arr@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@A_27a@ty_2Enum_2Enum))))) & (p@(ap@(ap@(c_2Ebool_2ETYPE__DEFINITION@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@A_27a@ty_2Enum_2Enum)))@(ty_2Epatricia_2Eptree@A_27a))@(lam@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@A_27a@ty_2Enum_2Enum)))@(^ [V1a0_27:$i] : (ap@(c_2Ebool_2E_21@(arr@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@A_27a@ty_2Enum_2Enum)))@bool))@(lam@(arr@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@A_27a@ty_2Enum_2Enum)))@bool)@(^ [V2_27ptree_27:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@(c_2Ebool_2E_21@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@A_27a@ty_2Enum_2Enum))))@(lam@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@A_27a@ty_2Enum_2Enum)))@(^ [V3a0_27:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@(c_2Emin_2E_3D@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@A_27a@ty_2Enum_2Enum))))@V3a0_27)@(ap@(ap@(ap@(c_2Eind__type_2ECONSTR@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@A_27a@ty_2Enum_2Enum)))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@A_27a@ty_2Enum_2Enum))@(c_2Ebool_2EARB@ty_2Enum_2Enum))@(ap@(ap@(c_2Epair_2E_2C@A_27a@ty_2Enum_2Enum)@(c_2Ebool_2EARB@A_27a))@(c_2Ebool_2EARB@ty_2Enum_2Enum))))@(lam@ty_2Enum_2Enum@(^ [V4n:$i] : (c_2Eind__type_2EBOTTOM@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@A_27a@ty_2Enum_2Enum))))))))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(c_2Ebool_2E_3F@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V5a0:$i] : (ap@(c_2Ebool_2E_3F@A_27a)@(lam@A_27a@(^ [V6a1:$i] : (ap@(ap@(c_2Emin_2E_3D@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@A_27a@ty_2Enum_2Enum))))@V3a0_27)@(ap@(ap@(lam@ty_2Enum_2Enum@(^ [V7a0:$i] : (lam@A_27a@(^ [V8a1:$i] : (ap@(ap@(ap@(c_2Eind__type_2ECONSTR@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@A_27a@ty_2Enum_2Enum)))@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@A_27a@ty_2Enum_2Enum))@V7a0)@(ap@(ap@(c_2Epair_2E_2C@A_27a@ty_2Enum_2Enum)@V8a1)@(c_2Ebool_2EARB@ty_2Enum_2Enum))))@(lam@ty_2Enum_2Enum@(^ [V9n:$i] : (c_2Eind__type_2EBOTTOM@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@A_27a@ty_2Enum_2Enum))))))))))@V5a0)@V6a1)))))))))@(ap@(c_2Ebool_2E_3F@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V10a0:$i] : (ap@(c_2Ebool_2E_3F@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V11a1:$i] : (ap@(c_2Ebool_2E_3F@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@A_27a@ty_2Enum_2Enum))))@(lam@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@A_27a@ty_2Enum_2Enum)))@(^ [V12a2:$i] : (ap@(c_2Ebool_2E_3F@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@A_27a@ty_2Enum_2Enum))))@(lam@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@A_27a@ty_2Enum_2Enum)))@(^ [V13a3:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Emin_2E_3D@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@A_27a@ty_2Enum_2Enum))))@V3a0_27)@(ap@(ap@(ap@(ap@(lam@ty_2Enum_2Enum@(^ [V14a0:$i] : (lam@ty_2Enum_2Enum@(^ [V15a1:$i] : (lam@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@A_27a@ty_2Enum_2Enum)))@(^ [V16a2:$i] : (lam@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@A_27a@ty_2Enum_2Enum)))@(^ [V17a3:$i] : (ap@(ap@(ap@(c_2Eind__type_2ECONSTR@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@A_27a@ty_2Enum_2Enum)))@(ap@c_2Enum_2ESUC@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@A_27a@ty_2Enum_2Enum))@V14a0)@(ap@(ap@(c_2Epair_2E_2C@A_27a@ty_2Enum_2Enum)@(c_2Ebool_2EARB@A_27a))@V15a1)))@(ap@(ap@(c_2Eind__type_2EFCONS@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@A_27a@ty_2Enum_2Enum))))@V16a2)@(ap@(ap@(c_2Eind__type_2EFCONS@(ty_2Eind__type_2Erecspace@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@A_27a@ty_2Enum_2Enum))))@V17a3)@(lam@ty_2Enum_2Enum@(^ [V18n:$i] : (c_2Eind__type_2EBOTTOM@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@A_27a@ty_2Enum_2Enum))))))))))))))))@V10a0)@V11a1)@V12a2)@V13a3)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@V2_27ptree_27@V12a2))@(ap@V2_27ptree_27@V13a3))))))))))))))))))@(ap@V2_27ptree_27@V3a0_27))))))@(ap@V2_27ptree_27@V1a0_27))))))))@V0rep)))))).
thf(ax_thm_2Epatricia_2Eptree__case__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0v:$i] : ((mem@V0v@A_27b) => ( ! [V1f:$i] : ((mem@V1f@(arr@ty_2Enum_2Enum@(arr@A_27a@A_27b))) => ( ! [V2f1:$i] : ((mem@V2f1@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@(arr@(ty_2Epatricia_2Eptree@A_27a)@(arr@(ty_2Epatricia_2Eptree@A_27a)@A_27b))))) => ((ap@(ap@(ap@(ap@(c_2Epatricia_2Eptree__CASE@A_27a@A_27b)@(c_2Epatricia_2EEmpty@A_27a))@V0v)@V1f)@V2f1) = V0v))))))) & (( ! [V3a0:tp__ty_2Enum_2Enum] : ( ! [V4a1:$i] : ((mem@V4a1@A_27a) => ( ! [V5v:$i] : ((mem@V5v@A_27b) => ( ! [V6f:$i] : ((mem@V6f@(arr@ty_2Enum_2Enum@(arr@A_27a@A_27b))) => ( ! [V7f1:$i] : ((mem@V7f1@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@(arr@(ty_2Epatricia_2Eptree@A_27a)@(arr@(ty_2Epatricia_2Eptree@A_27a)@A_27b))))) => ((ap@(ap@(ap@(ap@(c_2Epatricia_2Eptree__CASE@A_27a@A_27b)@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V3a0))@V4a1))@V5v)@V6f)@V7f1) = (ap@(ap@V6f@(inj__ty_2Enum_2Enum @ V3a0))@V4a1))))))))))) & ( ! [V8a0:tp__ty_2Enum_2Enum] : ( ! [V9a1:tp__ty_2Enum_2Enum] : ( ! [V10a2:$i] : ((mem@V10a2@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V11a3:$i] : ((mem@V11a3@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V12v:$i] : ((mem@V12v@A_27b) => ( ! [V13f:$i] : ((mem@V13f@(arr@ty_2Enum_2Enum@(arr@A_27a@A_27b))) => ( ! [V14f1:$i] : ((mem@V14f1@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@(arr@(ty_2Epatricia_2Eptree@A_27a)@(arr@(ty_2Epatricia_2Eptree@A_27a)@A_27b))))) => ((ap@(ap@(ap@(ap@(c_2Epatricia_2Eptree__CASE@A_27a@A_27b)@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V8a0))@(inj__ty_2Enum_2Enum @ V9a1))@V10a2)@V11a3))@V12v)@V13f)@V14f1) = (ap@(ap@(ap@(ap@V14f1@(inj__ty_2Enum_2Enum @ V8a0))@(inj__ty_2Enum_2Enum @ V9a1))@V10a2)@V11a3))))))))))))))))))).
thf(ax_thm_2Epatricia_2Eptree__size__def,axiom,( ! [A_27a:del]: (( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@ty_2Enum_2Enum)) => ((surj__ty_2Enum_2Enum @ (ap@(ap@(c_2Epatricia_2Eptree__size@A_27a)@V0f)@(c_2Epatricia_2EEmpty@A_27a))) = fo__c_2Enum_2E0))) & (( ! [V1f:$i] : ((mem@V1f@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V2a0:tp__ty_2Enum_2Enum] : ( ! [V3a1:$i] : ((mem@V3a1@A_27a) => ((surj__ty_2Enum_2Enum @ (ap@(ap@(c_2Epatricia_2Eptree__size@A_27a)@V1f)@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V2a0))@V3a1))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V2a0))@(ap@V1f@V3a1)))))))))) & ( ! [V4f:$i] : ((mem@V4f@(arr@A_27a@ty_2Enum_2Enum)) => ( ! [V5a0:tp__ty_2Enum_2Enum] : ( ! [V6a1:tp__ty_2Enum_2Enum] : ( ! [V7a2:$i] : ((mem@V7a2@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V8a3:$i] : ((mem@V8a3@(ty_2Epatricia_2Eptree@A_27a)) => ((surj__ty_2Enum_2Enum @ (ap@(ap@(c_2Epatricia_2Eptree__size@A_27a)@V4f)@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V5a0))@(inj__ty_2Enum_2Enum @ V6a1))@V7a2)@V8a3))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V5a0))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V6a1))@(ap@(ap@c_2Earithmetic_2E_2B@(ap@(ap@(c_2Epatricia_2Eptree__size@A_27a)@V4f)@V7a2))@(ap@(ap@(c_2Epatricia_2Eptree__size@A_27a)@V4f)@V8a3))))))))))))))))))).
thf(conj_thm_2Epatricia_2Edatatype__ptree,lemma,( ! [A_27a:del]: ( ! [V0ptree:$i] : ((mem@V0ptree@(arr@(ty_2Epatricia_2Eptree@A_27a)@(arr@(arr@ty_2Enum_2Enum@(arr@A_27a@(ty_2Epatricia_2Eptree@A_27a)))@(arr@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@(arr@(ty_2Epatricia_2Eptree@A_27a)@(arr@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a)))))@bool)))) => (p@(ap@(c_2Ebool_2EDATATYPE@bool)@(ap@(ap@(ap@V0ptree@(c_2Epatricia_2EEmpty@A_27a))@(c_2Epatricia_2ELeaf@A_27a))@(c_2Epatricia_2EBranch@A_27a)))))))).
thf(conj_thm_2Epatricia_2Eptree__11,lemma,( ! [A_27a:del]: (( ! [V0a0:tp__ty_2Enum_2Enum] : ( ! [V1a1:$i] : ((mem@V1a1@A_27a) => ( ! [V2a0_27:tp__ty_2Enum_2Enum] : ( ! [V3a1_27:$i] : ((mem@V3a1_27@A_27a) => (((ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V0a0))@V1a1) = (ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V2a0_27))@V3a1_27)) <=> ((V0a0 = V2a0_27) & (V1a1 = V3a1_27))))))))) & ( ! [V4a0:tp__ty_2Enum_2Enum] : ( ! [V5a1:tp__ty_2Enum_2Enum] : ( ! [V6a2:$i] : ((mem@V6a2@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V7a3:$i] : ((mem@V7a3@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V8a0_27:tp__ty_2Enum_2Enum] : ( ! [V9a1_27:tp__ty_2Enum_2Enum] : ( ! [V10a2_27:$i] : ((mem@V10a2_27@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V11a3_27:$i] : ((mem@V11a3_27@(ty_2Epatricia_2Eptree@A_27a)) => (((ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V4a0))@(inj__ty_2Enum_2Enum @ V5a1))@V6a2)@V7a3) = (ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V8a0_27))@(inj__ty_2Enum_2Enum @ V9a1_27))@V10a2_27)@V11a3_27)) <=> ((V4a0 = V8a0_27) & ((V5a1 = V9a1_27) & ((V6a2 = V10a2_27) & (V7a3 = V11a3_27)))))))))))))))))))).
thf(conj_thm_2Epatricia_2Eptree__distinct,lemma,( ! [A_27a:del]: (( ! [V0a1:$i] : ((mem@V0a1@A_27a) => ( ! [V1a0:tp__ty_2Enum_2Enum] : (~~ ((c_2Epatricia_2EEmpty@A_27a) = (ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V1a0))@V0a1)))))) & (( ! [V2a3:$i] : ((mem@V2a3@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V3a2:$i] : ((mem@V3a2@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V4a1:tp__ty_2Enum_2Enum] : ( ! [V5a0:tp__ty_2Enum_2Enum] : (~~ ((c_2Epatricia_2EEmpty@A_27a) = (ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V5a0))@(inj__ty_2Enum_2Enum @ V4a1))@V3a2)@V2a3))))))))) & ( ! [V6a3:$i] : ((mem@V6a3@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V7a2:$i] : ((mem@V7a2@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V8a1_27:tp__ty_2Enum_2Enum] : ( ! [V9a1:$i] : ((mem@V9a1@A_27a) => ( ! [V10a0_27:tp__ty_2Enum_2Enum] : ( ! [V11a0:tp__ty_2Enum_2Enum] : (~~ ((ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V11a0))@V9a1) = (ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V10a0_27))@(inj__ty_2Enum_2Enum @ V8a1_27))@V7a2)@V6a3)))))))))))))))).
thf(conj_thm_2Epatricia_2Eptree__nchotomy,lemma,( ! [A_27a:del]: ( ! [V0pp:$i] : ((mem@V0pp@(ty_2Epatricia_2Eptree@A_27a)) => ((V0pp = (c_2Epatricia_2EEmpty@A_27a)) | ((? [V1n:tp__ty_2Enum_2Enum] : (? [V2a:$i] : ((mem@V2a@A_27a) & (V0pp = (ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V1n))@V2a))))) | (? [V3n0:tp__ty_2Enum_2Enum] : (? [V4n:tp__ty_2Enum_2Enum] : (? [V5p:$i] : ((mem@V5p@(ty_2Epatricia_2Eptree@A_27a)) & (? [V6p0:$i] : ((mem@V6p0@(ty_2Epatricia_2Eptree@A_27a)) & (V0pp = (ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V3n0))@(inj__ty_2Enum_2Enum @ V4n))@V5p)@V6p0)))))))))))))).
thf(conj_thm_2Epatricia_2Eptree__Axiom,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f0:$i] : ((mem@V0f0@A_27b) => ( ! [V1f1:$i] : ((mem@V1f1@(arr@ty_2Enum_2Enum@(arr@A_27a@A_27b))) => ( ! [V2f2:$i] : ((mem@V2f2@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@(arr@(ty_2Epatricia_2Eptree@A_27a)@(arr@(ty_2Epatricia_2Eptree@A_27a)@(arr@A_27b@(arr@A_27b@A_27b))))))) => (? [V3fn:$i] : ((mem@V3fn@(arr@(ty_2Epatricia_2Eptree@A_27a)@A_27b)) & (((ap@V3fn@(c_2Epatricia_2EEmpty@A_27a)) = V0f0) & (( ! [V4a0:tp__ty_2Enum_2Enum] : ( ! [V5a1:$i] : ((mem@V5a1@A_27a) => ((ap@V3fn@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V4a0))@V5a1)) = (ap@(ap@V1f1@(inj__ty_2Enum_2Enum @ V4a0))@V5a1))))) & ( ! [V6a0:tp__ty_2Enum_2Enum] : ( ! [V7a1:tp__ty_2Enum_2Enum] : ( ! [V8a2:$i] : ((mem@V8a2@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V9a3:$i] : ((mem@V9a3@(ty_2Epatricia_2Eptree@A_27a)) => ((ap@V3fn@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V6a0))@(inj__ty_2Enum_2Enum @ V7a1))@V8a2)@V9a3)) = (ap@(ap@(ap@(ap@(ap@(ap@V2f2@(inj__ty_2Enum_2Enum @ V6a0))@(inj__ty_2Enum_2Enum @ V7a1))@V8a2)@V9a3)@(ap@V3fn@V8a2))@(ap@V3fn@V9a3)))))))))))))))))))))).
thf(conj_thm_2Epatricia_2Eptree__induction,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@(ty_2Epatricia_2Eptree@A_27a)@bool)) => (((p@(ap@V0P@(c_2Epatricia_2EEmpty@A_27a))) & (( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2a:$i] : ((mem@V2a@A_27a) => (p@(ap@V0P@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V1n))@V2a)))))) & ( ! [V3p:$i] : ((mem@V3p@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V4p0:$i] : ((mem@V4p0@(ty_2Epatricia_2Eptree@A_27a)) => (((p@(ap@V0P@V3p)) & (p@(ap@V0P@V4p0))) => ( ! [V5n:tp__ty_2Enum_2Enum] : ( ! [V6n0:tp__ty_2Enum_2Enum] : (p@(ap@V0P@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V6n0))@(inj__ty_2Enum_2Enum @ V5n))@V3p)@V4p0)))))))))))) => ( ! [V7p:$i] : ((mem@V7p@(ty_2Epatricia_2Eptree@A_27a)) => (p@(ap@V0P@V7p))))))))).
thf(conj_thm_2Epatricia_2Eptree__case__cong,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v_27:$i] : ((mem@V0v_27@A_27b) => ( ! [V1f_27:$i] : ((mem@V1f_27@(arr@ty_2Enum_2Enum@(arr@A_27a@A_27b))) => ( ! [V2f1_27:$i] : ((mem@V2f1_27@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@(arr@(ty_2Epatricia_2Eptree@A_27a)@(arr@(ty_2Epatricia_2Eptree@A_27a)@A_27b))))) => ( ! [V3M:$i] : ((mem@V3M@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V4M_27:$i] : ((mem@V4M_27@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V5v:$i] : ((mem@V5v@A_27b) => ( ! [V6f:$i] : ((mem@V6f@(arr@ty_2Enum_2Enum@(arr@A_27a@A_27b))) => ( ! [V7f1:$i] : ((mem@V7f1@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@(arr@(ty_2Epatricia_2Eptree@A_27a)@(arr@(ty_2Epatricia_2Eptree@A_27a)@A_27b))))) => (((V3M = V4M_27) & (((V4M_27 = (c_2Epatricia_2EEmpty@A_27a)) => (V5v = V0v_27)) & (( ! [V8a0:tp__ty_2Enum_2Enum] : ( ! [V9a1:$i] : ((mem@V9a1@A_27a) => ((V4M_27 = (ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V8a0))@V9a1)) => ((ap@(ap@V6f@(inj__ty_2Enum_2Enum @ V8a0))@V9a1) = (ap@(ap@V1f_27@(inj__ty_2Enum_2Enum @ V8a0))@V9a1)))))) & ( ! [V10a0:tp__ty_2Enum_2Enum] : ( ! [V11a1:tp__ty_2Enum_2Enum] : ( ! [V12a2:$i] : ((mem@V12a2@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V13a3:$i] : ((mem@V13a3@(ty_2Epatricia_2Eptree@A_27a)) => ((V4M_27 = (ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V10a0))@(inj__ty_2Enum_2Enum @ V11a1))@V12a2)@V13a3)) => ((ap@(ap@(ap@(ap@V7f1@(inj__ty_2Enum_2Enum @ V10a0))@(inj__ty_2Enum_2Enum @ V11a1))@V12a2)@V13a3) = (ap@(ap@(ap@(ap@V2f1_27@(inj__ty_2Enum_2Enum @ V10a0))@(inj__ty_2Enum_2Enum @ V11a1))@V12a2)@V13a3)))))))))))) => ((ap@(ap@(ap@(ap@(c_2Epatricia_2Eptree__CASE@A_27a@A_27b)@V3M)@V5v)@V6f)@V7f1) = (ap@(ap@(ap@(ap@(c_2Epatricia_2Eptree__CASE@A_27a@A_27b)@V4M_27)@V0v_27)@V1f_27)@V2f1_27)))))))))))))))))))))).
thf(conj_thm_2Epatricia_2Eptree__case__eq,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : ((mem@V0x@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V1v:$i] : ((mem@V1v@A_27b) => ( ! [V2f:$i] : ((mem@V2f@(arr@ty_2Enum_2Enum@(arr@A_27a@A_27b))) => ( ! [V3f1:$i] : ((mem@V3f1@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@(arr@(ty_2Epatricia_2Eptree@A_27a)@(arr@(ty_2Epatricia_2Eptree@A_27a)@A_27b))))) => ( ! [V4v_27:$i] : ((mem@V4v_27@A_27b) => (((ap@(ap@(ap@(ap@(c_2Epatricia_2Eptree__CASE@A_27a@A_27b)@V0x)@V1v)@V2f)@V3f1) = V4v_27) <=> (((V0x = (c_2Epatricia_2EEmpty@A_27a)) & (V1v = V4v_27)) | ((? [V5n:tp__ty_2Enum_2Enum] : (? [V6a:$i] : ((mem@V6a@A_27a) & ((V0x = (ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V5n))@V6a)) & ((ap@(ap@V2f@(inj__ty_2Enum_2Enum @ V5n))@V6a) = V4v_27))))) | (? [V7n0:tp__ty_2Enum_2Enum] : (? [V8n:tp__ty_2Enum_2Enum] : (? [V9p:$i] : ((mem@V9p@(ty_2Epatricia_2Eptree@A_27a)) & (? [V10p0:$i] : ((mem@V10p0@(ty_2Epatricia_2Eptree@A_27a)) & ((V0x = (ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V7n0))@(inj__ty_2Enum_2Enum @ V8n))@V9p)@V10p0)) & ((ap@(ap@(ap@(ap@V3f1@(inj__ty_2Enum_2Enum @ V7n0))@(inj__ty_2Enum_2Enum @ V8n))@V9p)@V10p0) = V4v_27)))))))))))))))))))))))).
thf(conj_thm_2Epatricia_2EBRANCHING__BIT__ind,lemma,( ! [V0P:$i] : ((mem@V0P@(arr@ty_2Enum_2Enum@(arr@ty_2Enum_2Enum@bool))) => (( ! [V1p0:tp__ty_2Enum_2Enum] : ( ! [V2p1:tp__ty_2Enum_2Enum] : (((~~ (((p@(ap@c_2Earithmetic_2EODD@(inj__ty_2Enum_2Enum @ V1p0))) <=> (p@(ap@c_2Earithmetic_2EEVEN@(inj__ty_2Enum_2Enum @ V2p1)))) | (V1p0 = V2p1))) => (p@(ap@(ap@V0P@(ap@c_2Earithmetic_2EDIV2@(inj__ty_2Enum_2Enum @ V1p0)))@(ap@c_2Earithmetic_2EDIV2@(inj__ty_2Enum_2Enum @ V2p1))))) => (p@(ap@(ap@V0P@(inj__ty_2Enum_2Enum @ V1p0))@(inj__ty_2Enum_2Enum @ V2p1)))))) => ( ! [V3v:tp__ty_2Enum_2Enum] : ( ! [V4v1:tp__ty_2Enum_2Enum] : (p@(ap@(ap@V0P@(inj__ty_2Enum_2Enum @ V3v))@(inj__ty_2Enum_2Enum @ V4v1))))))))).
thf(conj_thm_2Epatricia_2EBRANCHING__BIT__def,lemma,( ! [V0p1:tp__ty_2Enum_2Enum] : ( ! [V1p0:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Epatricia_2EBRANCHING__BIT@(inj__ty_2Enum_2Enum @ V1p0))@(inj__ty_2Enum_2Enum @ V0p1))) = (surj__ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ebool_2ECOND@ty_2Enum_2Enum)@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@(c_2Emin_2E_3D@bool)@(ap@c_2Earithmetic_2EODD@(inj__ty_2Enum_2Enum @ V1p0)))@(ap@c_2Earithmetic_2EEVEN@(inj__ty_2Enum_2Enum @ V0p1))))@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V1p0))@(inj__ty_2Enum_2Enum @ V0p1))))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@c_2Enum_2ESUC@(ap@(ap@c_2Epatricia_2EBRANCHING__BIT@(ap@c_2Earithmetic_2EDIV2@(inj__ty_2Enum_2Enum @ V1p0)))@(ap@c_2Earithmetic_2EDIV2@(inj__ty_2Enum_2Enum @ V0p1)))))))))).
thf(conj_thm_2Epatricia_2EPEEK__ind,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@(ty_2Epatricia_2Eptree@A_27a)@(arr@ty_2Enum_2Enum@bool))) => ((( ! [V1k:tp__ty_2Enum_2Enum] : (p@(ap@(ap@V0P@(c_2Epatricia_2EEmpty@A_27a))@(inj__ty_2Enum_2Enum @ V1k)))) & (( ! [V2j:tp__ty_2Enum_2Enum] : ( ! [V3d:$i] : ((mem@V3d@A_27a) => ( ! [V4k:tp__ty_2Enum_2Enum] : (p@(ap@(ap@V0P@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V2j))@V3d))@(inj__ty_2Enum_2Enum @ V4k))))))) & ( ! [V5p:tp__ty_2Enum_2Enum] : ( ! [V6m:tp__ty_2Enum_2Enum] : ( ! [V7l:$i] : ((mem@V7l@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V8r:$i] : ((mem@V8r@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V9k:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@V0P@(ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epatricia_2Eptree@A_27a))@(ap@(ap@c_2Ebit_2EBIT@(inj__ty_2Enum_2Enum @ V6m))@(inj__ty_2Enum_2Enum @ V9k)))@V7l)@V8r))@(inj__ty_2Enum_2Enum @ V9k))) => (p@(ap@(ap@V0P@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V5p))@(inj__ty_2Enum_2Enum @ V6m))@V7l)@V8r))@(inj__ty_2Enum_2Enum @ V9k))))))))))))) => ( ! [V10v:$i] : ((mem@V10v@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V11v1:tp__ty_2Enum_2Enum] : (p@(ap@(ap@V0P@V10v)@(inj__ty_2Enum_2Enum @ V11v1))))))))))).
thf(conj_thm_2Epatricia_2EPEEK__def,lemma,( ! [A_27a:del]: (( ! [V0k:tp__ty_2Enum_2Enum] : ((ap@(ap@(c_2Epatricia_2EPEEK@A_27a)@(c_2Epatricia_2EEmpty@A_27a))@(inj__ty_2Enum_2Enum @ V0k)) = (c_2Eoption_2ENONE@A_27a))) & (( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2j:tp__ty_2Enum_2Enum] : ( ! [V3d:$i] : ((mem@V3d@A_27a) => ((ap@(ap@(c_2Epatricia_2EPEEK@A_27a)@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V2j))@V3d))@(inj__ty_2Enum_2Enum @ V1k)) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@A_27a))@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V1k))@(inj__ty_2Enum_2Enum @ V2j)))@(ap@(c_2Eoption_2ESOME@A_27a)@V3d))@(c_2Eoption_2ENONE@A_27a))))))) & ( ! [V4r:$i] : ((mem@V4r@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V5p:tp__ty_2Enum_2Enum] : ( ! [V6m:tp__ty_2Enum_2Enum] : ( ! [V7l:$i] : ((mem@V7l@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V8k:tp__ty_2Enum_2Enum] : ((ap@(ap@(c_2Epatricia_2EPEEK@A_27a)@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V5p))@(inj__ty_2Enum_2Enum @ V6m))@V7l)@V4r))@(inj__ty_2Enum_2Enum @ V8k)) = (ap@(ap@(c_2Epatricia_2EPEEK@A_27a)@(ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epatricia_2Eptree@A_27a))@(ap@(ap@c_2Ebit_2EBIT@(inj__ty_2Enum_2Enum @ V6m))@(inj__ty_2Enum_2Enum @ V8k)))@V7l)@V4r))@(inj__ty_2Enum_2Enum @ V8k)))))))))))))).
thf(ax_thm_2Epatricia_2EJOIN__def,axiom,( ! [A_27a:del]: ( ! [V0p0:tp__ty_2Enum_2Enum] : ( ! [V1t0:$i] : ((mem@V1t0@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V2p1:tp__ty_2Enum_2Enum] : ( ! [V3t1:$i] : ((mem@V3t1@(ty_2Epatricia_2Eptree@A_27a)) => ((ap@(c_2Epatricia_2EJOIN@A_27a)@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epatricia_2Eptree@A_27a))))@(inj__ty_2Enum_2Enum @ V0p0))@(ap@(ap@(c_2Epair_2E_2C@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epatricia_2Eptree@A_27a)))@V1t0)@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epatricia_2Eptree@A_27a))@(inj__ty_2Enum_2Enum @ V2p1))@V3t1)))) = (ap@(ap@(c_2Ebool_2ELET@ty_2Enum_2Enum@(ty_2Epatricia_2Eptree@A_27a))@(lam@ty_2Enum_2Enum@(^ [V4m:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epatricia_2Eptree@A_27a))@(ap@(ap@c_2Ebit_2EBIT@V4m)@(inj__ty_2Enum_2Enum @ V0p0)))@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(ap@(ap@c_2Ebit_2EMOD__2EXP@V4m)@(inj__ty_2Enum_2Enum @ V0p0)))@V4m)@V1t0)@V3t1))@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(ap@(ap@c_2Ebit_2EMOD__2EXP@V4m)@(inj__ty_2Enum_2Enum @ V0p0)))@V4m)@V3t1)@V1t0)))))@(ap@(ap@c_2Epatricia_2EBRANCHING__BIT@(inj__ty_2Enum_2Enum @ V0p0))@(inj__ty_2Enum_2Enum @ V2p1)))))))))))).
thf(conj_thm_2Epatricia_2EADD__ind,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@(ty_2Epatricia_2Eptree@A_27a)@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@A_27a)@bool))) => ((( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2e:$i] : ((mem@V2e@A_27a) => (p@(ap@(ap@V0P@(c_2Epatricia_2EEmpty@A_27a))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@A_27a)@(inj__ty_2Enum_2Enum @ V1k))@V2e)))))) & (( ! [V3j:tp__ty_2Enum_2Enum] : ( ! [V4d:$i] : ((mem@V4d@A_27a) => ( ! [V5k:tp__ty_2Enum_2Enum] : ( ! [V6e:$i] : ((mem@V6e@A_27a) => (p@(ap@(ap@V0P@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V3j))@V4d))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@A_27a)@(inj__ty_2Enum_2Enum @ V5k))@V6e))))))))) & ( ! [V7p:tp__ty_2Enum_2Enum] : ( ! [V8m:tp__ty_2Enum_2Enum] : ( ! [V9l:$i] : ((mem@V9l@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V10r:$i] : ((mem@V10r@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V11k:tp__ty_2Enum_2Enum] : ( ! [V12e:$i] : ((mem@V12e@A_27a) => (((((p@(ap@(ap@(ap@c_2Ebit_2EMOD__2EXP__EQ@(inj__ty_2Enum_2Enum @ V8m))@(inj__ty_2Enum_2Enum @ V11k))@(inj__ty_2Enum_2Enum @ V7p))) & (~~ (p@(ap@(ap@c_2Ebit_2EBIT@(inj__ty_2Enum_2Enum @ V8m))@(inj__ty_2Enum_2Enum @ V11k))))) => (p@(ap@(ap@V0P@V10r)@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@A_27a)@(inj__ty_2Enum_2Enum @ V11k))@V12e)))) & (((p@(ap@(ap@(ap@c_2Ebit_2EMOD__2EXP__EQ@(inj__ty_2Enum_2Enum @ V8m))@(inj__ty_2Enum_2Enum @ V11k))@(inj__ty_2Enum_2Enum @ V7p))) & (p@(ap@(ap@c_2Ebit_2EBIT@(inj__ty_2Enum_2Enum @ V8m))@(inj__ty_2Enum_2Enum @ V11k)))) => (p@(ap@(ap@V0P@V9l)@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@A_27a)@(inj__ty_2Enum_2Enum @ V11k))@V12e))))) => (p@(ap@(ap@V0P@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V7p))@(inj__ty_2Enum_2Enum @ V8m))@V9l)@V10r))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@A_27a)@(inj__ty_2Enum_2Enum @ V11k))@V12e))))))))))))))) => ( ! [V13v:$i] : ((mem@V13v@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V14v1:tp__ty_2Enum_2Enum] : ( ! [V15v2:$i] : ((mem@V15v2@A_27a) => (p@(ap@(ap@V0P@V13v)@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@A_27a)@(inj__ty_2Enum_2Enum @ V14v1))@V15v2))))))))))))).
thf(conj_thm_2Epatricia_2EADD__def,lemma,( ! [A_27a:del]: (( ! [V0k:tp__ty_2Enum_2Enum] : ( ! [V1e:$i] : ((mem@V1e@A_27a) => ((ap@(ap@(c_2Epatricia_2EADD@A_27a)@(c_2Epatricia_2EEmpty@A_27a))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@A_27a)@(inj__ty_2Enum_2Enum @ V0k))@V1e)) = (ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V0k))@V1e))))) & (( ! [V2k:tp__ty_2Enum_2Enum] : ( ! [V3j:tp__ty_2Enum_2Enum] : ( ! [V4e:$i] : ((mem@V4e@A_27a) => ( ! [V5d:$i] : ((mem@V5d@A_27a) => ((ap@(ap@(c_2Epatricia_2EADD@A_27a)@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V3j))@V5d))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@A_27a)@(inj__ty_2Enum_2Enum @ V2k))@V4e)) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epatricia_2Eptree@A_27a))@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V3j))@(inj__ty_2Enum_2Enum @ V2k)))@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V2k))@V4e))@(ap@(c_2Epatricia_2EJOIN@A_27a)@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epatricia_2Eptree@A_27a))))@(inj__ty_2Enum_2Enum @ V2k))@(ap@(ap@(c_2Epair_2E_2C@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epatricia_2Eptree@A_27a)))@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V2k))@V4e))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epatricia_2Eptree@A_27a))@(inj__ty_2Enum_2Enum @ V3j))@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V3j))@V5d))))))))))))) & ( ! [V6r:$i] : ((mem@V6r@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V7p:tp__ty_2Enum_2Enum] : ( ! [V8m:tp__ty_2Enum_2Enum] : ( ! [V9l:$i] : ((mem@V9l@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V10k:tp__ty_2Enum_2Enum] : ( ! [V11e:$i] : ((mem@V11e@A_27a) => ((ap@(ap@(c_2Epatricia_2EADD@A_27a)@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V7p))@(inj__ty_2Enum_2Enum @ V8m))@V9l)@V6r))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@A_27a)@(inj__ty_2Enum_2Enum @ V10k))@V11e)) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epatricia_2Eptree@A_27a))@(ap@(ap@(ap@c_2Ebit_2EMOD__2EXP__EQ@(inj__ty_2Enum_2Enum @ V8m))@(inj__ty_2Enum_2Enum @ V10k))@(inj__ty_2Enum_2Enum @ V7p)))@(ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epatricia_2Eptree@A_27a))@(ap@(ap@c_2Ebit_2EBIT@(inj__ty_2Enum_2Enum @ V8m))@(inj__ty_2Enum_2Enum @ V10k)))@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V7p))@(inj__ty_2Enum_2Enum @ V8m))@(ap@(ap@(c_2Epatricia_2EADD@A_27a)@V9l)@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@A_27a)@(inj__ty_2Enum_2Enum @ V10k))@V11e)))@V6r))@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V7p))@(inj__ty_2Enum_2Enum @ V8m))@V9l)@(ap@(ap@(c_2Epatricia_2EADD@A_27a)@V6r)@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@A_27a)@(inj__ty_2Enum_2Enum @ V10k))@V11e)))))@(ap@(c_2Epatricia_2EJOIN@A_27a)@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epatricia_2Eptree@A_27a))))@(inj__ty_2Enum_2Enum @ V10k))@(ap@(ap@(c_2Epair_2E_2C@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epatricia_2Eptree@A_27a)))@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V10k))@V11e))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epatricia_2Eptree@A_27a))@(inj__ty_2Enum_2Enum @ V7p))@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V7p))@(inj__ty_2Enum_2Enum @ V8m))@V9l)@V6r)))))))))))))))))))).
thf(ax_thm_2Epatricia_2EBRANCH__primitive__def,axiom,( ! [A_27a:del]: ((c_2Epatricia_2EBRANCH@A_27a) = (ap@(ap@(c_2Erelation_2EWFREC@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))))@(ty_2Epatricia_2Eptree@A_27a))@(ap@(c_2Emin_2E_40@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))))@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))))@bool)))@(lam@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))))@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))))@bool))@(^ [V0R:$i] : (ap@(c_2Erelation_2EWF@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a)))))@V0R)))))@(lam@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))))@(ty_2Epatricia_2Eptree@A_27a))@(^ [V1BRANCH:$i] : (lam@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))))@(^ [V2a:$i] : (ap@(ap@(c_2Epair_2Epair__CASE@(ty_2Epatricia_2Eptree@A_27a)@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))))@V2a)@(lam@ty_2Enum_2Enum@(^ [V3p:$i] : (lam@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a)))@(^ [V4v1:$i] : (ap@(ap@(c_2Epair_2Epair__CASE@(ty_2Epatricia_2Eptree@A_27a)@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a)))@V4v1)@(lam@ty_2Enum_2Enum@(^ [V5m:$i] : (lam@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))@(^ [V6v3:$i] : (ap@(ap@(c_2Epair_2Epair__CASE@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))@V6v3)@(lam@(ty_2Epatricia_2Eptree@A_27a)@(^ [V7v4:$i] : (lam@(ty_2Epatricia_2Eptree@A_27a)@(^ [V8t:$i] : (ap@(ap@(ap@(ap@(c_2Epatricia_2Eptree__CASE@A_27a@(ty_2Epatricia_2Eptree@A_27a))@V7v4)@(ap@(c_2Ecombin_2EI@(ty_2Epatricia_2Eptree@A_27a))@V8t))@(lam@ty_2Enum_2Enum@(^ [V9v18:$i] : (lam@A_27a@(^ [V10v19:$i] : (ap@(ap@(ap@(ap@(c_2Epatricia_2Eptree__CASE@A_27a@(ty_2Epatricia_2Eptree@A_27a))@V8t)@(ap@(c_2Ecombin_2EI@(ty_2Epatricia_2Eptree@A_27a))@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@V9v18)@V10v19)))@(lam@ty_2Enum_2Enum@(^ [V11v30:$i] : (lam@A_27a@(^ [V12v31:$i] : (ap@(c_2Ecombin_2EI@(ty_2Epatricia_2Eptree@A_27a))@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@V3p)@V5m)@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@V9v18)@V10v19))@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@V11v30)@V12v31))))))))@(lam@ty_2Enum_2Enum@(^ [V13v32:$i] : (lam@ty_2Enum_2Enum@(^ [V14v33:$i] : (lam@(ty_2Epatricia_2Eptree@A_27a)@(^ [V15v34:$i] : (lam@(ty_2Epatricia_2Eptree@A_27a)@(^ [V16v35:$i] : (ap@(c_2Ecombin_2EI@(ty_2Epatricia_2Eptree@A_27a))@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@V3p)@V5m)@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@V9v18)@V10v19))@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@V13v32)@V14v33)@V15v34)@V16v35)))))))))))))))))@(lam@ty_2Enum_2Enum@(^ [V17v20:$i] : (lam@ty_2Enum_2Enum@(^ [V18v21:$i] : (lam@(ty_2Epatricia_2Eptree@A_27a)@(^ [V19v22:$i] : (lam@(ty_2Epatricia_2Eptree@A_27a)@(^ [V20v23:$i] : (ap@(ap@(ap@(ap@(c_2Epatricia_2Eptree__CASE@A_27a@(ty_2Epatricia_2Eptree@A_27a))@V8t)@(ap@(c_2Ecombin_2EI@(ty_2Epatricia_2Eptree@A_27a))@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@V17v20)@V18v21)@V19v22)@V20v23)))@(lam@ty_2Enum_2Enum@(^ [V21v42:$i] : (lam@A_27a@(^ [V22v43:$i] : (ap@(c_2Ecombin_2EI@(ty_2Epatricia_2Eptree@A_27a))@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@V3p)@V5m)@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@V17v20)@V18v21)@V19v22)@V20v23))@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@V21v42)@V22v43))))))))@(lam@ty_2Enum_2Enum@(^ [V23v44:$i] : (lam@ty_2Enum_2Enum@(^ [V24v45:$i] : (lam@(ty_2Epatricia_2Eptree@A_27a)@(^ [V25v46:$i] : (lam@(ty_2Epatricia_2Eptree@A_27a)@(^ [V26v47:$i] : (ap@(c_2Ecombin_2EI@(ty_2Epatricia_2Eptree@A_27a))@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@V3p)@V5m)@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@V17v20)@V18v21)@V19v22)@V20v23))@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@V23v44)@V24v45)@V25v46)@V26v47)))))))))))))))))))))))))))))))))))))))))))).
thf(conj_thm_2Epatricia_2EBRANCH__ind,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))))@bool)) => ((( ! [V1p:tp__ty_2Enum_2Enum] : ( ! [V2m:tp__ty_2Enum_2Enum] : ( ! [V3t:$i] : ((mem@V3t@(ty_2Epatricia_2Eptree@A_27a)) => (p@(ap@V0P@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))))@(inj__ty_2Enum_2Enum @ V1p))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a)))@(inj__ty_2Enum_2Enum @ V2m))@(ap@(ap@(c_2Epair_2E_2C@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))@(c_2Epatricia_2EEmpty@A_27a))@V3t))))))))) & (( ! [V4p:tp__ty_2Enum_2Enum] : ( ! [V5m:tp__ty_2Enum_2Enum] : ( ! [V6v6:tp__ty_2Enum_2Enum] : ( ! [V7v7:$i] : ((mem@V7v7@A_27a) => (p@(ap@V0P@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))))@(inj__ty_2Enum_2Enum @ V4p))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a)))@(inj__ty_2Enum_2Enum @ V5m))@(ap@(ap@(c_2Epair_2E_2C@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V6v6))@V7v7))@(c_2Epatricia_2EEmpty@A_27a))))))))))) & (( ! [V8p:tp__ty_2Enum_2Enum] : ( ! [V9m:tp__ty_2Enum_2Enum] : ( ! [V10v8:tp__ty_2Enum_2Enum] : ( ! [V11v9:tp__ty_2Enum_2Enum] : ( ! [V12v10:$i] : ((mem@V12v10@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V13v11:$i] : ((mem@V13v11@(ty_2Epatricia_2Eptree@A_27a)) => (p@(ap@V0P@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))))@(inj__ty_2Enum_2Enum @ V8p))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a)))@(inj__ty_2Enum_2Enum @ V9m))@(ap@(ap@(c_2Epair_2E_2C@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V10v8))@(inj__ty_2Enum_2Enum @ V11v9))@V12v10)@V13v11))@(c_2Epatricia_2EEmpty@A_27a)))))))))))))) & (( ! [V14p:tp__ty_2Enum_2Enum] : ( ! [V15m:tp__ty_2Enum_2Enum] : ( ! [V16v12:tp__ty_2Enum_2Enum] : ( ! [V17v13:$i] : ((mem@V17v13@A_27a) => ( ! [V18v24:tp__ty_2Enum_2Enum] : ( ! [V19v25:$i] : ((mem@V19v25@A_27a) => (p@(ap@V0P@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))))@(inj__ty_2Enum_2Enum @ V14p))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a)))@(inj__ty_2Enum_2Enum @ V15m))@(ap@(ap@(c_2Epair_2E_2C@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V16v12))@V17v13))@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V18v24))@V19v25)))))))))))))) & (( ! [V20p:tp__ty_2Enum_2Enum] : ( ! [V21m:tp__ty_2Enum_2Enum] : ( ! [V22v12:tp__ty_2Enum_2Enum] : ( ! [V23v13:$i] : ((mem@V23v13@A_27a) => ( ! [V24v26:tp__ty_2Enum_2Enum] : ( ! [V25v27:tp__ty_2Enum_2Enum] : ( ! [V26v28:$i] : ((mem@V26v28@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V27v29:$i] : ((mem@V27v29@(ty_2Epatricia_2Eptree@A_27a)) => (p@(ap@V0P@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))))@(inj__ty_2Enum_2Enum @ V20p))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a)))@(inj__ty_2Enum_2Enum @ V21m))@(ap@(ap@(c_2Epair_2E_2C@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V22v12))@V23v13))@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V24v26))@(inj__ty_2Enum_2Enum @ V25v27))@V26v28)@V27v29))))))))))))))))) & (( ! [V28p:tp__ty_2Enum_2Enum] : ( ! [V29m:tp__ty_2Enum_2Enum] : ( ! [V30v14:tp__ty_2Enum_2Enum] : ( ! [V31v15:tp__ty_2Enum_2Enum] : ( ! [V32v16:$i] : ((mem@V32v16@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V33v17:$i] : ((mem@V33v17@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V34v36:tp__ty_2Enum_2Enum] : ( ! [V35v37:$i] : ((mem@V35v37@A_27a) => (p@(ap@V0P@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))))@(inj__ty_2Enum_2Enum @ V28p))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a)))@(inj__ty_2Enum_2Enum @ V29m))@(ap@(ap@(c_2Epair_2E_2C@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V30v14))@(inj__ty_2Enum_2Enum @ V31v15))@V32v16)@V33v17))@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V34v36))@V35v37))))))))))))))))) & ( ! [V36p:tp__ty_2Enum_2Enum] : ( ! [V37m:tp__ty_2Enum_2Enum] : ( ! [V38v14:tp__ty_2Enum_2Enum] : ( ! [V39v15:tp__ty_2Enum_2Enum] : ( ! [V40v16:$i] : ((mem@V40v16@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V41v17:$i] : ((mem@V41v17@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V42v38:tp__ty_2Enum_2Enum] : ( ! [V43v39:tp__ty_2Enum_2Enum] : ( ! [V44v40:$i] : ((mem@V44v40@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V45v41:$i] : ((mem@V45v41@(ty_2Epatricia_2Eptree@A_27a)) => (p@(ap@V0P@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))))@(inj__ty_2Enum_2Enum @ V36p))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a)))@(inj__ty_2Enum_2Enum @ V37m))@(ap@(ap@(c_2Epair_2E_2C@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V38v14))@(inj__ty_2Enum_2Enum @ V39v15))@V40v16)@V41v17))@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V42v38))@(inj__ty_2Enum_2Enum @ V43v39))@V44v40)@V45v41)))))))))))))))))))))))))) => ( ! [V46v:tp__ty_2Enum_2Enum] : ( ! [V47v1:tp__ty_2Enum_2Enum] : ( ! [V48v2:$i] : ((mem@V48v2@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V49v3:$i] : ((mem@V49v3@(ty_2Epatricia_2Eptree@A_27a)) => (p@(ap@V0P@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))))@(inj__ty_2Enum_2Enum @ V46v))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a)))@(inj__ty_2Enum_2Enum @ V47v1))@(ap@(ap@(c_2Epair_2E_2C@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))@V48v2)@V49v3)))))))))))))))).
thf(conj_thm_2Epatricia_2EBRANCH__def,lemma,( ! [A_27a:del]: ( ! [V0p:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2t:$i] : ((mem@V2t@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V3v6:tp__ty_2Enum_2Enum] : ( ! [V4v7:$i] : ((mem@V4v7@A_27a) => ( ! [V5v8:tp__ty_2Enum_2Enum] : ( ! [V6v9:tp__ty_2Enum_2Enum] : ( ! [V7v10:$i] : ((mem@V7v10@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V8v11:$i] : ((mem@V8v11@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V9v12:tp__ty_2Enum_2Enum] : ( ! [V10v13:$i] : ((mem@V10v13@A_27a) => ( ! [V11v24:tp__ty_2Enum_2Enum] : ( ! [V12v25:$i] : ((mem@V12v25@A_27a) => ( ! [V13v26:tp__ty_2Enum_2Enum] : ( ! [V14v27:tp__ty_2Enum_2Enum] : ( ! [V15v28:$i] : ((mem@V15v28@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V16v29:$i] : ((mem@V16v29@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V17v14:tp__ty_2Enum_2Enum] : ( ! [V18v15:tp__ty_2Enum_2Enum] : ( ! [V19v16:$i] : ((mem@V19v16@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V20v17:$i] : ((mem@V20v17@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V21v36:tp__ty_2Enum_2Enum] : ( ! [V22v37:$i] : ((mem@V22v37@A_27a) => ( ! [V23v38:tp__ty_2Enum_2Enum] : ( ! [V24v39:tp__ty_2Enum_2Enum] : ( ! [V25v40:$i] : ((mem@V25v40@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V26v41:$i] : ((mem@V26v41@(ty_2Epatricia_2Eptree@A_27a)) => (((ap@(c_2Epatricia_2EBRANCH@A_27a)@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))))@(inj__ty_2Enum_2Enum @ V0p))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a)))@(inj__ty_2Enum_2Enum @ V1m))@(ap@(ap@(c_2Epair_2E_2C@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))@(c_2Epatricia_2EEmpty@A_27a))@V2t)))) = V2t) & (((ap@(c_2Epatricia_2EBRANCH@A_27a)@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))))@(inj__ty_2Enum_2Enum @ V0p))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a)))@(inj__ty_2Enum_2Enum @ V1m))@(ap@(ap@(c_2Epair_2E_2C@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V3v6))@V4v7))@(c_2Epatricia_2EEmpty@A_27a))))) = (ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V3v6))@V4v7)) & (((ap@(c_2Epatricia_2EBRANCH@A_27a)@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))))@(inj__ty_2Enum_2Enum @ V0p))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a)))@(inj__ty_2Enum_2Enum @ V1m))@(ap@(ap@(c_2Epair_2E_2C@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V5v8))@(inj__ty_2Enum_2Enum @ V6v9))@V7v10)@V8v11))@(c_2Epatricia_2EEmpty@A_27a))))) = (ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V5v8))@(inj__ty_2Enum_2Enum @ V6v9))@V7v10)@V8v11)) & (((ap@(c_2Epatricia_2EBRANCH@A_27a)@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))))@(inj__ty_2Enum_2Enum @ V0p))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a)))@(inj__ty_2Enum_2Enum @ V1m))@(ap@(ap@(c_2Epair_2E_2C@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V9v12))@V10v13))@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V11v24))@V12v25))))) = (ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V0p))@(inj__ty_2Enum_2Enum @ V1m))@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V9v12))@V10v13))@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V11v24))@V12v25))) & (((ap@(c_2Epatricia_2EBRANCH@A_27a)@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))))@(inj__ty_2Enum_2Enum @ V0p))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a)))@(inj__ty_2Enum_2Enum @ V1m))@(ap@(ap@(c_2Epair_2E_2C@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V9v12))@V10v13))@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V13v26))@(inj__ty_2Enum_2Enum @ V14v27))@V15v28)@V16v29))))) = (ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V0p))@(inj__ty_2Enum_2Enum @ V1m))@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V9v12))@V10v13))@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V13v26))@(inj__ty_2Enum_2Enum @ V14v27))@V15v28)@V16v29))) & (((ap@(c_2Epatricia_2EBRANCH@A_27a)@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))))@(inj__ty_2Enum_2Enum @ V0p))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a)))@(inj__ty_2Enum_2Enum @ V1m))@(ap@(ap@(c_2Epair_2E_2C@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V17v14))@(inj__ty_2Enum_2Enum @ V18v15))@V19v16)@V20v17))@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V21v36))@V22v37))))) = (ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V0p))@(inj__ty_2Enum_2Enum @ V1m))@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V17v14))@(inj__ty_2Enum_2Enum @ V18v15))@V19v16)@V20v17))@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V21v36))@V22v37))) & ((ap@(c_2Epatricia_2EBRANCH@A_27a)@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))))@(inj__ty_2Enum_2Enum @ V0p))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a)))@(inj__ty_2Enum_2Enum @ V1m))@(ap@(ap@(c_2Epair_2E_2C@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V17v14))@(inj__ty_2Enum_2Enum @ V18v15))@V19v16)@V20v17))@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V23v38))@(inj__ty_2Enum_2Enum @ V24v39))@V25v40)@V26v41))))) = (ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V0p))@(inj__ty_2Enum_2Enum @ V1m))@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V17v14))@(inj__ty_2Enum_2Enum @ V18v15))@V19v16)@V20v17))@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V23v38))@(inj__ty_2Enum_2Enum @ V24v39))@V25v40)@V26v41))))))))))))))))))))))))))))))))))))))))))))))))))).
thf(ax_thm_2Epatricia_2EREMOVE__def,axiom,( ! [A_27a:del]: (( ! [V0k:tp__ty_2Enum_2Enum] : ((ap@(ap@(c_2Epatricia_2EREMOVE@A_27a)@(c_2Epatricia_2EEmpty@A_27a))@(inj__ty_2Enum_2Enum @ V0k)) = (c_2Epatricia_2EEmpty@A_27a))) & (( ! [V1j:tp__ty_2Enum_2Enum] : ( ! [V2d:$i] : ((mem@V2d@A_27a) => ( ! [V3k:tp__ty_2Enum_2Enum] : ((ap@(ap@(c_2Epatricia_2EREMOVE@A_27a)@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V1j))@V2d))@(inj__ty_2Enum_2Enum @ V3k)) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epatricia_2Eptree@A_27a))@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V1j))@(inj__ty_2Enum_2Enum @ V3k)))@(c_2Epatricia_2EEmpty@A_27a))@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V1j))@V2d))))))) & ( ! [V4p:tp__ty_2Enum_2Enum] : ( ! [V5m:tp__ty_2Enum_2Enum] : ( ! [V6l:$i] : ((mem@V6l@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V7r:$i] : ((mem@V7r@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V8k:tp__ty_2Enum_2Enum] : ((ap@(ap@(c_2Epatricia_2EREMOVE@A_27a)@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V4p))@(inj__ty_2Enum_2Enum @ V5m))@V6l)@V7r))@(inj__ty_2Enum_2Enum @ V8k)) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epatricia_2Eptree@A_27a))@(ap@(ap@(ap@c_2Ebit_2EMOD__2EXP__EQ@(inj__ty_2Enum_2Enum @ V5m))@(inj__ty_2Enum_2Enum @ V8k))@(inj__ty_2Enum_2Enum @ V4p)))@(ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epatricia_2Eptree@A_27a))@(ap@(ap@c_2Ebit_2EBIT@(inj__ty_2Enum_2Enum @ V5m))@(inj__ty_2Enum_2Enum @ V8k)))@(ap@(c_2Epatricia_2EBRANCH@A_27a)@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))))@(inj__ty_2Enum_2Enum @ V4p))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a)))@(inj__ty_2Enum_2Enum @ V5m))@(ap@(ap@(c_2Epair_2E_2C@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))@(ap@(ap@(c_2Epatricia_2EREMOVE@A_27a)@V6l)@(inj__ty_2Enum_2Enum @ V8k)))@V7r)))))@(ap@(c_2Epatricia_2EBRANCH@A_27a)@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))))@(inj__ty_2Enum_2Enum @ V4p))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a)))@(inj__ty_2Enum_2Enum @ V5m))@(ap@(ap@(c_2Epair_2E_2C@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))@V6l)@(ap@(ap@(c_2Epatricia_2EREMOVE@A_27a)@V7r)@(inj__ty_2Enum_2Enum @ V8k))))))))@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V4p))@(inj__ty_2Enum_2Enum @ V5m))@V6l)@V7r)))))))))))))).
thf(ax_thm_2Epatricia_2ETRAVERSE__AUX__def,axiom,( ! [A_27a:del]: (( ! [V0a:tp__c_ty_2Elist_2Elist_ty_2Enum_2Enum] : ((surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ (ap@(ap@(c_2Epatricia_2ETRAVERSE__AUX@A_27a)@(c_2Epatricia_2EEmpty@A_27a))@(inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ V0a))) = V0a)) & (( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2d:$i] : ((mem@V2d@A_27a) => ( ! [V3a:tp__c_ty_2Elist_2Elist_ty_2Enum_2Enum] : ((surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ (ap@(ap@(c_2Epatricia_2ETRAVERSE__AUX@A_27a)@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V1k))@V2d))@(inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ V3a))) = (surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ (ap@(ap@(c_2Elist_2ECONS@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V1k))@(inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ V3a)))))))) & ( ! [V4p:tp__ty_2Enum_2Enum] : ( ! [V5m:tp__ty_2Enum_2Enum] : ( ! [V6l:$i] : ((mem@V6l@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V7r:$i] : ((mem@V7r@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V8a:tp__c_ty_2Elist_2Elist_ty_2Enum_2Enum] : ((surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ (ap@(ap@(c_2Epatricia_2ETRAVERSE__AUX@A_27a)@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V4p))@(inj__ty_2Enum_2Enum @ V5m))@V6l)@V7r))@(inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ V8a))) = (surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ (ap@(ap@(c_2Epatricia_2ETRAVERSE__AUX@A_27a)@V6l)@(ap@(ap@(c_2Epatricia_2ETRAVERSE__AUX@A_27a)@V7r)@(inj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ V8a)))))))))))))))).
thf(ax_thm_2Epatricia_2ETRAVERSE__def,axiom,( ! [A_27a:del]: (((surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ (ap@(c_2Epatricia_2ETRAVERSE@A_27a)@(c_2Epatricia_2EEmpty@A_27a))) = (surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ (c_2Elist_2ENIL@ty_2Enum_2Enum))) & (( ! [V0j:tp__ty_2Enum_2Enum] : ( ! [V1d:$i] : ((mem@V1d@A_27a) => ((surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ (ap@(c_2Epatricia_2ETRAVERSE@A_27a)@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V0j))@V1d))) = (surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ (ap@(ap@(c_2Elist_2ECONS@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V0j))@(c_2Elist_2ENIL@ty_2Enum_2Enum))))))) & ( ! [V2p:tp__ty_2Enum_2Enum] : ( ! [V3m:tp__ty_2Enum_2Enum] : ( ! [V4l:$i] : ((mem@V4l@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V5r:$i] : ((mem@V5r@(ty_2Epatricia_2Eptree@A_27a)) => ((surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ (ap@(c_2Epatricia_2ETRAVERSE@A_27a)@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V2p))@(inj__ty_2Enum_2Enum @ V3m))@V4l)@V5r))) = (surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ (ap@(ap@(c_2Elist_2EAPPEND@ty_2Enum_2Enum)@(ap@(c_2Epatricia_2ETRAVERSE@A_27a)@V4l))@(ap@(c_2Epatricia_2ETRAVERSE@A_27a)@V5r)))))))))))))).
thf(ax_thm_2Epatricia_2EKEYS__def,axiom,( ! [A_27a:del]: ( ! [V0t:$i] : ((mem@V0t@(ty_2Epatricia_2Eptree@A_27a)) => ((surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ (ap@(c_2Epatricia_2EKEYS@A_27a)@V0t)) = (surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ (ap@(ap@(c_2Esorting_2EQSORT@ty_2Enum_2Enum)@c_2Eprim__rec_2E_3C)@(ap@(c_2Epatricia_2ETRAVERSE@A_27a)@V0t)))))))).
thf(ax_thm_2Epatricia_2ETRANSFORM__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0f:$i] : ((mem@V0f@(arr@A_27b@A_27a)) => ((ap@(ap@(c_2Epatricia_2ETRANSFORM@A_27a@A_27b)@V0f)@(c_2Epatricia_2EEmpty@A_27b)) = (c_2Epatricia_2EEmpty@A_27a)))) & (( ! [V1f:$i] : ((mem@V1f@(arr@A_27b@A_27a)) => ( ! [V2j:tp__ty_2Enum_2Enum] : ( ! [V3d:$i] : ((mem@V3d@A_27b) => ((ap@(ap@(c_2Epatricia_2ETRANSFORM@A_27a@A_27b)@V1f)@(ap@(ap@(c_2Epatricia_2ELeaf@A_27b)@(inj__ty_2Enum_2Enum @ V2j))@V3d)) = (ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V2j))@(ap@V1f@V3d)))))))) & ( ! [V4f:$i] : ((mem@V4f@(arr@A_27b@A_27a)) => ( ! [V5p:tp__ty_2Enum_2Enum] : ( ! [V6m:tp__ty_2Enum_2Enum] : ( ! [V7l:$i] : ((mem@V7l@(ty_2Epatricia_2Eptree@A_27b)) => ( ! [V8r:$i] : ((mem@V8r@(ty_2Epatricia_2Eptree@A_27b)) => ((ap@(ap@(c_2Epatricia_2ETRANSFORM@A_27a@A_27b)@V4f)@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27b)@(inj__ty_2Enum_2Enum @ V5p))@(inj__ty_2Enum_2Enum @ V6m))@V7l)@V8r)) = (ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V5p))@(inj__ty_2Enum_2Enum @ V6m))@(ap@(ap@(c_2Epatricia_2ETRANSFORM@A_27a@A_27b)@V4f)@V7l))@(ap@(ap@(c_2Epatricia_2ETRANSFORM@A_27a@A_27b)@V4f)@V8r)))))))))))))))).
thf(ax_thm_2Epatricia_2EEVERY__LEAF__def,axiom,( ! [A_27a:del]: (( ! [V0P:$i] : ((mem@V0P@(arr@ty_2Enum_2Enum@(arr@A_27a@bool))) => ((p@(ap@(ap@(c_2Epatricia_2EEVERY__LEAF@A_27a)@V0P)@(c_2Epatricia_2EEmpty@A_27a))) <=> $true))) & (( ! [V1P:$i] : ((mem@V1P@(arr@ty_2Enum_2Enum@(arr@A_27a@bool))) => ( ! [V2j:tp__ty_2Enum_2Enum] : ( ! [V3d:$i] : ((mem@V3d@A_27a) => ((p@(ap@(ap@(c_2Epatricia_2EEVERY__LEAF@A_27a)@V1P)@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V2j))@V3d))) <=> (p@(ap@(ap@V1P@(inj__ty_2Enum_2Enum @ V2j))@V3d)))))))) & ( ! [V4P:$i] : ((mem@V4P@(arr@ty_2Enum_2Enum@(arr@A_27a@bool))) => ( ! [V5p:tp__ty_2Enum_2Enum] : ( ! [V6m:tp__ty_2Enum_2Enum] : ( ! [V7l:$i] : ((mem@V7l@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V8r:$i] : ((mem@V8r@(ty_2Epatricia_2Eptree@A_27a)) => ((p@(ap@(ap@(c_2Epatricia_2EEVERY__LEAF@A_27a)@V4P)@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V5p))@(inj__ty_2Enum_2Enum @ V6m))@V7l)@V8r))) <=> ((p@(ap@(ap@(c_2Epatricia_2EEVERY__LEAF@A_27a)@V4P)@V7l)) & (p@(ap@(ap@(c_2Epatricia_2EEVERY__LEAF@A_27a)@V4P)@V8r)))))))))))))))).
thf(ax_thm_2Epatricia_2EEXISTS__LEAF__def,axiom,( ! [A_27a:del]: (( ! [V0P:$i] : ((mem@V0P@(arr@ty_2Enum_2Enum@(arr@A_27a@bool))) => ((p@(ap@(ap@(c_2Epatricia_2EEXISTS__LEAF@A_27a)@V0P)@(c_2Epatricia_2EEmpty@A_27a))) <=> $false))) & (( ! [V1P:$i] : ((mem@V1P@(arr@ty_2Enum_2Enum@(arr@A_27a@bool))) => ( ! [V2j:tp__ty_2Enum_2Enum] : ( ! [V3d:$i] : ((mem@V3d@A_27a) => ((p@(ap@(ap@(c_2Epatricia_2EEXISTS__LEAF@A_27a)@V1P)@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V2j))@V3d))) <=> (p@(ap@(ap@V1P@(inj__ty_2Enum_2Enum @ V2j))@V3d)))))))) & ( ! [V4P:$i] : ((mem@V4P@(arr@ty_2Enum_2Enum@(arr@A_27a@bool))) => ( ! [V5p:tp__ty_2Enum_2Enum] : ( ! [V6m:tp__ty_2Enum_2Enum] : ( ! [V7l:$i] : ((mem@V7l@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V8r:$i] : ((mem@V8r@(ty_2Epatricia_2Eptree@A_27a)) => ((p@(ap@(ap@(c_2Epatricia_2EEXISTS__LEAF@A_27a)@V4P)@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V5p))@(inj__ty_2Enum_2Enum @ V6m))@V7l)@V8r))) <=> ((p@(ap@(ap@(c_2Epatricia_2EEXISTS__LEAF@A_27a)@V4P)@V7l)) | (p@(ap@(ap@(c_2Epatricia_2EEXISTS__LEAF@A_27a)@V4P)@V8r)))))))))))))))).
thf(ax_thm_2Epatricia_2ESIZE__def,axiom,( ! [A_27a:del]: ( ! [V0t:$i] : ((mem@V0t@(ty_2Epatricia_2Eptree@A_27a)) => ((surj__ty_2Enum_2Enum @ (ap@(c_2Epatricia_2ESIZE@A_27a)@V0t)) = (surj__ty_2Enum_2Enum @ (ap@(c_2Elist_2ELENGTH@ty_2Enum_2Enum)@(ap@(c_2Epatricia_2ETRAVERSE@A_27a)@V0t)))))))).
thf(ax_thm_2Epatricia_2EDEPTH__def,axiom,( ! [A_27a:del]: (((surj__ty_2Enum_2Enum @ (ap@(c_2Epatricia_2EDEPTH@A_27a)@(c_2Epatricia_2EEmpty@A_27a))) = fo__c_2Enum_2E0) & (( ! [V0j:tp__ty_2Enum_2Enum] : ( ! [V1d:$i] : ((mem@V1d@A_27a) => ((surj__ty_2Enum_2Enum @ (ap@(c_2Epatricia_2EDEPTH@A_27a)@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V0j))@V1d))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))) & ( ! [V2p:tp__ty_2Enum_2Enum] : ( ! [V3m:tp__ty_2Enum_2Enum] : ( ! [V4l:$i] : ((mem@V4l@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V5r:$i] : ((mem@V5r@(ty_2Epatricia_2Eptree@A_27a)) => ((surj__ty_2Enum_2Enum @ (ap@(c_2Epatricia_2EDEPTH@A_27a)@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V2p))@(inj__ty_2Enum_2Enum @ V3m))@V4l)@V5r))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2E_2B@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(ap@(ap@c_2Earithmetic_2EMAX@(ap@(c_2Epatricia_2EDEPTH@A_27a)@V4l))@(ap@(c_2Epatricia_2EDEPTH@A_27a)@V5r))))))))))))))).
thf(ax_thm_2Epatricia_2EIS__PTREE__def,axiom,( ! [A_27a:del]: (((p@(ap@(c_2Epatricia_2EIS__PTREE@A_27a)@(c_2Epatricia_2EEmpty@A_27a))) <=> $true) & (( ! [V0k:tp__ty_2Enum_2Enum] : ( ! [V1d:$i] : ((mem@V1d@A_27a) => ((p@(ap@(c_2Epatricia_2EIS__PTREE@A_27a)@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V0k))@V1d))) <=> $true)))) & ( ! [V2p:tp__ty_2Enum_2Enum] : ( ! [V3m:tp__ty_2Enum_2Enum] : ( ! [V4l:$i] : ((mem@V4l@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V5r:$i] : ((mem@V5r@(ty_2Epatricia_2Eptree@A_27a)) => ((p@(ap@(c_2Epatricia_2EIS__PTREE@A_27a)@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V2p))@(inj__ty_2Enum_2Enum @ V3m))@V4l)@V5r))) <=> ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V2p))@(ap@(ap@c_2Earithmetic_2EEXP@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V3m)))) & ((p@(ap@(c_2Epatricia_2EIS__PTREE@A_27a)@V4l)) & ((p@(ap@(c_2Epatricia_2EIS__PTREE@A_27a)@V5r)) & ((~ (V4l = (c_2Epatricia_2EEmpty@A_27a))) & ((~ (V5r = (c_2Epatricia_2EEmpty@A_27a))) & ((p@(ap@(ap@(c_2Epatricia_2EEVERY__LEAF@A_27a)@(lam@ty_2Enum_2Enum@(^ [V6k:$i] : (lam@A_27a@(^ [V7d:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(ap@c_2Ebit_2EMOD__2EXP__EQ@(inj__ty_2Enum_2Enum @ V3m))@V6k)@(inj__ty_2Enum_2Enum @ V2p)))@(ap@(ap@c_2Ebit_2EBIT@(inj__ty_2Enum_2Enum @ V3m))@V6k)))))))@V4l)) & (p@(ap@(ap@(c_2Epatricia_2EEVERY__LEAF@A_27a)@(lam@ty_2Enum_2Enum@(^ [V8k:$i] : (lam@A_27a@(^ [V9d:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(ap@c_2Ebit_2EMOD__2EXP__EQ@(inj__ty_2Enum_2Enum @ V3m))@V8k)@(inj__ty_2Enum_2Enum @ V2p)))@(ap@c_2Ebool_2E_7E@(ap@(ap@c_2Ebit_2EBIT@(inj__ty_2Enum_2Enum @ V3m))@V8k))))))))@V5r))))))))))))))))))).
thf(ax_thm_2Epatricia_2EIN__PTREE__def,axiom,( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1t:tp__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone] : ((p@(ap@(ap@c_2Epatricia_2EIN__PTREE@(inj__ty_2Enum_2Enum @ V0n))@(inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone @ V1t))) <=> (p@(ap@(c_2Eoption_2EIS__SOME@ty_2Eone_2Eone)@(ap@(ap@(c_2Epatricia_2EPEEK@ty_2Eone_2Eone)@(inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone @ V1t))@(inj__ty_2Enum_2Enum @ V0n)))))))).
thf(ax_thm_2Epatricia_2EINSERT__PTREE__def,axiom,( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1t:tp__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone] : ((surj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone @ (ap@(ap@c_2Epatricia_2EINSERT__PTREE@(inj__ty_2Enum_2Enum @ V0n))@(inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone @ V1t))) = (surj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone @ (ap@(ap@(c_2Epatricia_2EADD@ty_2Eone_2Eone)@(inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone @ V1t))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Eone_2Eone)@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Eone_2Eone @ fo__c_2Eone_2Eone)))))))).
thf(ax_thm_2Epatricia_2EPTREE__OF__NUMSET__def,axiom,( ! [V0t:tp__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone] : ( ! [V1s:$i] : ((mem@V1s@(arr@ty_2Enum_2Enum@bool)) => ((surj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone @ (ap@(ap@c_2Epatricia_2EPTREE__OF__NUMSET@(inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone @ V0t))@V1s)) = (surj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone @ (ap@(ap@(ap@(c_2Elist_2EFOLDL@ty_2Enum_2Enum@(ty_2Epatricia_2Eptree@ty_2Eone_2Eone))@(ap@(c_2Ecombin_2EC@ty_2Enum_2Enum@(ty_2Epatricia_2Eptree@ty_2Eone_2Eone)@(ty_2Epatricia_2Eptree@ty_2Eone_2Eone))@c_2Epatricia_2EINSERT__PTREE))@(inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone @ V0t))@(ap@(c_2Elist_2ESET__TO__LIST@ty_2Enum_2Enum)@V1s)))))))).
thf(ax_thm_2Epatricia_2ENUMSET__OF__PTREE__def,axiom,( ! [V0t:tp__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone] : ((ap@c_2Epatricia_2ENUMSET__OF__PTREE@(inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone @ V0t)) = (ap@(c_2Elist_2ELIST__TO__SET@ty_2Enum_2Enum)@(ap@(c_2Epatricia_2ETRAVERSE@ty_2Eone_2Eone)@(inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone @ V0t)))))).
thf(ax_thm_2Epatricia_2EUNION__PTREE__def,axiom,( ! [V0t1:tp__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone] : ( ! [V1t2:tp__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone] : ((surj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone @ (ap@(ap@c_2Epatricia_2EUNION__PTREE@(inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone @ V0t1))@(inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone @ V1t2))) = (surj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone @ (ap@(ap@c_2Epatricia_2EPTREE__OF__NUMSET@(inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone @ V0t1))@(ap@c_2Epatricia_2ENUMSET__OF__PTREE@(inj__c_ty_2Epatricia_2Eptree_ty_2Eone_2Eone @ V1t2)))))))).
thf(ax_thm_2Epatricia_2EIS__EMPTY__primitive__def,axiom,( ! [A_27a:del]: ((c_2Epatricia_2EIS__EMPTY@A_27a) = (ap@(ap@(c_2Erelation_2EWFREC@(ty_2Epatricia_2Eptree@A_27a)@bool)@(ap@(c_2Emin_2E_40@(arr@(ty_2Epatricia_2Eptree@A_27a)@(arr@(ty_2Epatricia_2Eptree@A_27a)@bool)))@(lam@(arr@(ty_2Epatricia_2Eptree@A_27a)@(arr@(ty_2Epatricia_2Eptree@A_27a)@bool))@(^ [V0R:$i] : (ap@(c_2Erelation_2EWF@(ty_2Epatricia_2Eptree@A_27a))@V0R)))))@(lam@(arr@(ty_2Epatricia_2Eptree@A_27a)@bool)@(^ [V1IS__EMPTY:$i] : (lam@(ty_2Epatricia_2Eptree@A_27a)@(^ [V2a:$i] : (ap@(ap@(ap@(ap@(c_2Epatricia_2Eptree__CASE@A_27a@bool)@V2a)@(ap@(c_2Ecombin_2EI@bool)@c_2Ebool_2ET))@(lam@ty_2Enum_2Enum@(^ [V3v6:$i] : (lam@A_27a@(^ [V4v7:$i] : (ap@(c_2Ecombin_2EI@bool)@c_2Ebool_2EF))))))@(lam@ty_2Enum_2Enum@(^ [V5v8:$i] : (lam@ty_2Enum_2Enum@(^ [V6v9:$i] : (lam@(ty_2Epatricia_2Eptree@A_27a)@(^ [V7v10:$i] : (lam@(ty_2Epatricia_2Eptree@A_27a)@(^ [V8v11:$i] : (ap@(c_2Ecombin_2EI@bool)@c_2Ebool_2EF)))))))))))))))))).
thf(conj_thm_2Epatricia_2EIS__EMPTY__ind,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@(ty_2Epatricia_2Eptree@A_27a)@bool)) => (((p@(ap@V0P@(c_2Epatricia_2EEmpty@A_27a))) & (( ! [V1v:tp__ty_2Enum_2Enum] : ( ! [V2v1:$i] : ((mem@V2v1@A_27a) => (p@(ap@V0P@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V1v))@V2v1)))))) & ( ! [V3v2:tp__ty_2Enum_2Enum] : ( ! [V4v3:tp__ty_2Enum_2Enum] : ( ! [V5v4:$i] : ((mem@V5v4@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V6v5:$i] : ((mem@V6v5@(ty_2Epatricia_2Eptree@A_27a)) => (p@(ap@V0P@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V3v2))@(inj__ty_2Enum_2Enum @ V4v3))@V5v4)@V6v5))))))))))) => ( ! [V7v:$i] : ((mem@V7v@(ty_2Epatricia_2Eptree@A_27a)) => (p@(ap@V0P@V7v))))))))).
thf(conj_thm_2Epatricia_2EIS__EMPTY__def,lemma,( ! [A_27a:del]: ( ! [V0v:tp__ty_2Enum_2Enum] : ( ! [V1v1:$i] : ((mem@V1v1@A_27a) => ( ! [V2v2:tp__ty_2Enum_2Enum] : ( ! [V3v3:tp__ty_2Enum_2Enum] : ( ! [V4v4:$i] : ((mem@V4v4@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V5v5:$i] : ((mem@V5v5@(ty_2Epatricia_2Eptree@A_27a)) => (((p@(ap@(c_2Epatricia_2EIS__EMPTY@A_27a)@(c_2Epatricia_2EEmpty@A_27a))) <=> $true) & (((p@(ap@(c_2Epatricia_2EIS__EMPTY@A_27a)@(ap@(ap@(c_2Epatricia_2ELeaf@A_27a)@(inj__ty_2Enum_2Enum @ V0v))@V1v1))) <=> $false) & ((p@(ap@(c_2Epatricia_2EIS__EMPTY@A_27a)@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V2v2))@(inj__ty_2Enum_2Enum @ V3v3))@V4v4)@V5v5))) <=> $false)))))))))))))).
thf(ax_thm_2Epatricia_2EFIND__def,axiom,( ! [A_27a:del]: ( ! [V0t:$i] : ((mem@V0t@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V1k:tp__ty_2Enum_2Enum] : ((ap@(ap@(c_2Epatricia_2EFIND@A_27a)@V0t)@(inj__ty_2Enum_2Enum @ V1k)) = (ap@(c_2Eoption_2ETHE@A_27a)@(ap@(ap@(c_2Epatricia_2EPEEK@A_27a)@V0t)@(inj__ty_2Enum_2Enum @ V1k))))))))).
thf(ax_thm_2Epatricia_2EADD__LIST__def,axiom,( ! [A_27a:del]: ((c_2Epatricia_2EADD__LIST@A_27a) = (ap@(c_2Elist_2EFOLDL@(ty_2Epair_2Eprod@ty_2Enum_2Enum@A_27a)@(ty_2Epatricia_2Eptree@A_27a))@(c_2Epatricia_2EADD@A_27a))))).
thf(conj_thm_2Epatricia_2EBRANCHING__BIT,lemma,( ! [V0a:tp__ty_2Enum_2Enum] : ( ! [V1b:tp__ty_2Enum_2Enum] : ((~~ (V0a = V1b)) => (~~ ((p@(ap@(ap@c_2Ebit_2EBIT@(ap@(ap@c_2Epatricia_2EBRANCHING__BIT@(inj__ty_2Enum_2Enum @ V0a))@(inj__ty_2Enum_2Enum @ V1b)))@(inj__ty_2Enum_2Enum @ V0a))) <=> (p@(ap@(ap@c_2Ebit_2EBIT@(ap@(ap@c_2Epatricia_2EBRANCHING__BIT@(inj__ty_2Enum_2Enum @ V0a))@(inj__ty_2Enum_2Enum @ V1b)))@(inj__ty_2Enum_2Enum @ V1b))))))))).
thf(conj_thm_2Epatricia_2EBRANCHING__BIT__ZERO,lemma,( ! [V0a:tp__ty_2Enum_2Enum] : ( ! [V1b:tp__ty_2Enum_2Enum] : (((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Epatricia_2EBRANCHING__BIT@(inj__ty_2Enum_2Enum @ V0a))@(inj__ty_2Enum_2Enum @ V1b))) = fo__c_2Enum_2E0) <=> (((p@(ap@c_2Earithmetic_2EODD@(inj__ty_2Enum_2Enum @ V0a))) <=> (p@(ap@c_2Earithmetic_2EEVEN@(inj__ty_2Enum_2Enum @ V1b)))) | (V0a = V1b)))))).
thf(conj_thm_2Epatricia_2EBRANCHING__BIT__SYM,lemma,( ! [V0a:tp__ty_2Enum_2Enum] : ( ! [V1b:tp__ty_2Enum_2Enum] : ((surj__ty_2Enum_2Enum @ (ap@(ap@c_2Epatricia_2EBRANCHING__BIT@(inj__ty_2Enum_2Enum @ V0a))@(inj__ty_2Enum_2Enum @ V1b))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Epatricia_2EBRANCHING__BIT@(inj__ty_2Enum_2Enum @ V1b))@(inj__ty_2Enum_2Enum @ V0a))))))).
thf(conj_thm_2Epatricia_2EEVERY__LEAF__ADD,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@ty_2Enum_2Enum@(arr@A_27a@bool))) => ( ! [V1t:$i] : ((mem@V1t@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V2k:tp__ty_2Enum_2Enum] : ( ! [V3d:$i] : ((mem@V3d@A_27a) => (((p@(ap@(ap@V0P@(inj__ty_2Enum_2Enum @ V2k))@V3d)) & (p@(ap@(ap@(c_2Epatricia_2EEVERY__LEAF@A_27a)@V0P)@V1t))) => (p@(ap@(ap@(c_2Epatricia_2EEVERY__LEAF@A_27a)@V0P)@(ap@(ap@(c_2Epatricia_2EADD@A_27a)@V1t)@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@A_27a)@(inj__ty_2Enum_2Enum @ V2k))@V3d)))))))))))))).
thf(conj_thm_2Epatricia_2EMONO__EVERY__LEAF,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@ty_2Enum_2Enum@(arr@A_27a@bool))) => ( ! [V1Q:$i] : ((mem@V1Q@(arr@ty_2Enum_2Enum@(arr@A_27a@bool))) => ( ! [V2t:$i] : ((mem@V2t@(ty_2Epatricia_2Eptree@A_27a)) => ((( ! [V3k:tp__ty_2Enum_2Enum] : ( ! [V4d:$i] : ((mem@V4d@A_27a) => ((p@(ap@(ap@V0P@(inj__ty_2Enum_2Enum @ V3k))@V4d)) => (p@(ap@(ap@V1Q@(inj__ty_2Enum_2Enum @ V3k))@V4d)))))) & (p@(ap@(ap@(c_2Epatricia_2EEVERY__LEAF@A_27a)@V0P)@V2t))) => (p@(ap@(ap@(c_2Epatricia_2EEVERY__LEAF@A_27a)@V1Q)@V2t))))))))))).
thf(conj_thm_2Epatricia_2ENOT__ADD__EMPTY,lemma,( ! [A_27a:del]: ( ! [V0t:$i] : ((mem@V0t@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2d:$i] : ((mem@V2d@A_27a) => (~~ ((ap@(ap@(c_2Epatricia_2EADD@A_27a)@V0t)@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@A_27a)@(inj__ty_2Enum_2Enum @ V1k))@V2d)) = (c_2Epatricia_2EEmpty@A_27a)))))))))).
thf(conj_thm_2Epatricia_2EEMPTY__IS__PTREE,lemma,( ! [A_27a:del]: (p@(ap@(c_2Epatricia_2EIS__PTREE@A_27a)@(c_2Epatricia_2EEmpty@A_27a))))).
thf(conj_thm_2Epatricia_2EADD__IS__PTREE,lemma,( ! [A_27a:del]: ( ! [V0t:$i] : ((mem@V0t@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V1x:$i] : ((mem@V1x@(ty_2Epair_2Eprod@ty_2Enum_2Enum@A_27a)) => ((p@(ap@(c_2Epatricia_2EIS__PTREE@A_27a)@V0t)) => (p@(ap@(c_2Epatricia_2EIS__PTREE@A_27a)@(ap@(ap@(c_2Epatricia_2EADD@A_27a)@V0t)@V1x)))))))))).
thf(conj_thm_2Epatricia_2EEVERY__LEAF__BRANCH,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@ty_2Enum_2Enum@(arr@A_27a@bool))) => ( ! [V1p:tp__ty_2Enum_2Enum] : ( ! [V2m:tp__ty_2Enum_2Enum] : ( ! [V3l:$i] : ((mem@V3l@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V4r:$i] : ((mem@V4r@(ty_2Epatricia_2Eptree@A_27a)) => ((p@(ap@(ap@(c_2Epatricia_2EEVERY__LEAF@A_27a)@V0P)@(ap@(c_2Epatricia_2EBRANCH@A_27a)@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))))@(inj__ty_2Enum_2Enum @ V1p))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a)))@(inj__ty_2Enum_2Enum @ V2m))@(ap@(ap@(c_2Epair_2E_2C@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))@V3l)@V4r)))))) <=> ((p@(ap@(ap@(c_2Epatricia_2EEVERY__LEAF@A_27a)@V0P)@V3l)) & (p@(ap@(ap@(c_2Epatricia_2EEVERY__LEAF@A_27a)@V0P)@V4r)))))))))))))).
thf(conj_thm_2Epatricia_2EEVERY__LEAF__REMOVE,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@ty_2Enum_2Enum@(arr@A_27a@bool))) => ( ! [V1t:$i] : ((mem@V1t@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V2k:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@(c_2Epatricia_2EEVERY__LEAF@A_27a)@V0P)@V1t)) => (p@(ap@(ap@(c_2Epatricia_2EEVERY__LEAF@A_27a)@V0P)@(ap@(ap@(c_2Epatricia_2EREMOVE@A_27a)@V1t)@(inj__ty_2Enum_2Enum @ V2k)))))))))))).
thf(conj_thm_2Epatricia_2EIS__PTREE__BRANCH,lemma,( ! [A_27a:del]: ( ! [V0p:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2l:$i] : ((mem@V2l@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V3r:$i] : ((mem@V3r@(ty_2Epatricia_2Eptree@A_27a)) => (((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0p))@(ap@(ap@c_2Earithmetic_2EEXP@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V1m)))) & ((~~ ((V2l = (c_2Epatricia_2EEmpty@A_27a)) & (V3r = (c_2Epatricia_2EEmpty@A_27a)))) & ((p@(ap@(ap@(c_2Epatricia_2EEVERY__LEAF@A_27a)@(lam@ty_2Enum_2Enum@(^ [V4k:$i] : (lam@A_27a@(^ [V5d:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(ap@c_2Ebit_2EMOD__2EXP__EQ@(inj__ty_2Enum_2Enum @ V1m))@V4k)@(inj__ty_2Enum_2Enum @ V0p)))@(ap@(ap@c_2Ebit_2EBIT@(inj__ty_2Enum_2Enum @ V1m))@V4k)))))))@V2l)) & ((p@(ap@(ap@(c_2Epatricia_2EEVERY__LEAF@A_27a)@(lam@ty_2Enum_2Enum@(^ [V6k:$i] : (lam@A_27a@(^ [V7d:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(ap@c_2Ebit_2EMOD__2EXP__EQ@(inj__ty_2Enum_2Enum @ V1m))@V6k)@(inj__ty_2Enum_2Enum @ V0p)))@(ap@c_2Ebool_2E_7E@(ap@(ap@c_2Ebit_2EBIT@(inj__ty_2Enum_2Enum @ V1m))@V6k))))))))@V3r)) & ((p@(ap@(c_2Epatricia_2EIS__PTREE@A_27a)@V2l)) & (p@(ap@(c_2Epatricia_2EIS__PTREE@A_27a)@V3r))))))) => (p@(ap@(c_2Epatricia_2EIS__PTREE@A_27a)@(ap@(c_2Epatricia_2EBRANCH@A_27a)@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))))@(inj__ty_2Enum_2Enum @ V0p))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a)))@(inj__ty_2Enum_2Enum @ V1m))@(ap@(ap@(c_2Epair_2E_2C@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))@V2l)@V3r))))))))))))))).
thf(conj_thm_2Epatricia_2EREMOVE__IS__PTREE,lemma,( ! [A_27a:del]: ( ! [V0t:$i] : ((mem@V0t@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V1k:tp__ty_2Enum_2Enum] : ((p@(ap@(c_2Epatricia_2EIS__PTREE@A_27a)@V0t)) => (p@(ap@(c_2Epatricia_2EIS__PTREE@A_27a)@(ap@(ap@(c_2Epatricia_2EREMOVE@A_27a)@V0t)@(inj__ty_2Enum_2Enum @ V1k)))))))))).
thf(conj_thm_2Epatricia_2EPEEK__NONE,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@ty_2Enum_2Enum@(arr@A_27a@bool))) => ( ! [V1t:$i] : ((mem@V1t@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V2k:tp__ty_2Enum_2Enum] : ((( ! [V3d:$i] : ((mem@V3d@A_27a) => (~~ (p@(ap@(ap@V0P@(inj__ty_2Enum_2Enum @ V2k))@V3d))))) & (p@(ap@(ap@(c_2Epatricia_2EEVERY__LEAF@A_27a)@V0P)@V1t))) => ((ap@(ap@(c_2Epatricia_2EPEEK@A_27a)@V1t)@(inj__ty_2Enum_2Enum @ V2k)) = (c_2Eoption_2ENONE@A_27a)))))))))).
thf(conj_thm_2Epatricia_2EPEEK__ADD,lemma,( ! [A_27a:del]: ( ! [V0t:$i] : ((mem@V0t@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2d:$i] : ((mem@V2d@A_27a) => ( ! [V3j:tp__ty_2Enum_2Enum] : ((p@(ap@(c_2Epatricia_2EIS__PTREE@A_27a)@V0t)) => ((ap@(ap@(c_2Epatricia_2EPEEK@A_27a)@(ap@(ap@(c_2Epatricia_2EADD@A_27a)@V0t)@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@A_27a)@(inj__ty_2Enum_2Enum @ V1k))@V2d)))@(inj__ty_2Enum_2Enum @ V3j)) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@A_27a))@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V1k))@(inj__ty_2Enum_2Enum @ V3j)))@(ap@(c_2Eoption_2ESOME@A_27a)@V2d))@(ap@(ap@(c_2Epatricia_2EPEEK@A_27a)@V0t)@(inj__ty_2Enum_2Enum @ V3j))))))))))))).
thf(conj_thm_2Epatricia_2EBRANCH,lemma,( ! [A_27a:del]: ( ! [V0p:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2l:$i] : ((mem@V2l@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V3r:$i] : ((mem@V3r@(ty_2Epatricia_2Eptree@A_27a)) => ((ap@(c_2Epatricia_2EBRANCH@A_27a)@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))))@(inj__ty_2Enum_2Enum @ V0p))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a)))@(inj__ty_2Enum_2Enum @ V1m))@(ap@(ap@(c_2Epair_2E_2C@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))@V2l)@V3r)))) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epatricia_2Eptree@A_27a))@(ap@(ap@(c_2Emin_2E_3D@(ty_2Epatricia_2Eptree@A_27a))@V2l)@(c_2Epatricia_2EEmpty@A_27a)))@V3r)@(ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epatricia_2Eptree@A_27a))@(ap@(ap@(c_2Emin_2E_3D@(ty_2Epatricia_2Eptree@A_27a))@V3r)@(c_2Epatricia_2EEmpty@A_27a)))@V2l)@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27a)@(inj__ty_2Enum_2Enum @ V0p))@(inj__ty_2Enum_2Enum @ V1m))@V2l)@V3r)))))))))))).
thf(conj_thm_2Epatricia_2EPEEK__REMOVE,lemma,( ! [A_27a:del]: ( ! [V0t:$i] : ((mem@V0t@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2j:tp__ty_2Enum_2Enum] : ((p@(ap@(c_2Epatricia_2EIS__PTREE@A_27a)@V0t)) => ((ap@(ap@(c_2Epatricia_2EPEEK@A_27a)@(ap@(ap@(c_2Epatricia_2EREMOVE@A_27a)@V0t)@(inj__ty_2Enum_2Enum @ V1k)))@(inj__ty_2Enum_2Enum @ V2j)) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@A_27a))@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V1k))@(inj__ty_2Enum_2Enum @ V2j)))@(c_2Eoption_2ENONE@A_27a))@(ap@(ap@(c_2Epatricia_2EPEEK@A_27a)@V0t)@(inj__ty_2Enum_2Enum @ V2j))))))))))).
thf(conj_thm_2Epatricia_2EEVERY__LEAF__TRANSFORM,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@ty_2Enum_2Enum@(arr@A_27a@bool))) => ( ! [V1Q:$i] : ((mem@V1Q@(arr@ty_2Enum_2Enum@(arr@A_27b@bool))) => ( ! [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27b)) => ( ! [V3t:$i] : ((mem@V3t@(ty_2Epatricia_2Eptree@A_27a)) => ((( ! [V4k:tp__ty_2Enum_2Enum] : ( ! [V5d:$i] : ((mem@V5d@A_27a) => ((p@(ap@(ap@V0P@(inj__ty_2Enum_2Enum @ V4k))@V5d)) => (p@(ap@(ap@V1Q@(inj__ty_2Enum_2Enum @ V4k))@(ap@V2f@V5d))))))) & (p@(ap@(ap@(c_2Epatricia_2EEVERY__LEAF@A_27a)@V0P)@V3t))) => (p@(ap@(ap@(c_2Epatricia_2EEVERY__LEAF@A_27b)@V1Q)@(ap@(ap@(c_2Epatricia_2ETRANSFORM@A_27b@A_27a)@V2f)@V3t))))))))))))))).
thf(conj_thm_2Epatricia_2ETRANSFORM__EMPTY,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1t:$i] : ((mem@V1t@(ty_2Epatricia_2Eptree@A_27a)) => (((ap@(ap@(c_2Epatricia_2ETRANSFORM@A_27b@A_27a)@V0f)@V1t) = (c_2Epatricia_2EEmpty@A_27b)) <=> (V1t = (c_2Epatricia_2EEmpty@A_27a)))))))))).
thf(conj_thm_2Epatricia_2ETRANSFORM__IS__PTREE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1t:$i] : ((mem@V1t@(ty_2Epatricia_2Eptree@A_27a)) => ((p@(ap@(c_2Epatricia_2EIS__PTREE@A_27a)@V1t)) => (p@(ap@(c_2Epatricia_2EIS__PTREE@A_27b)@(ap@(ap@(c_2Epatricia_2ETRANSFORM@A_27b@A_27a)@V0f)@V1t))))))))))).
thf(conj_thm_2Epatricia_2EPEEK__TRANSFORM,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1t:$i] : ((mem@V1t@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V2k:tp__ty_2Enum_2Enum] : ((ap@(ap@(c_2Epatricia_2EPEEK@A_27b)@(ap@(ap@(c_2Epatricia_2ETRANSFORM@A_27b@A_27a)@V0f)@V1t))@(inj__ty_2Enum_2Enum @ V2k)) = (ap@(ap@(ap@(c_2Eoption_2Eoption__CASE@A_27a@(ty_2Eoption_2Eoption@A_27b))@(ap@(ap@(c_2Epatricia_2EPEEK@A_27a)@V1t)@(inj__ty_2Enum_2Enum @ V2k)))@(c_2Eoption_2ENONE@A_27b))@(lam@A_27a@(^ [V3x:$i] : (ap@(c_2Eoption_2ESOME@A_27b)@(ap@V0f@V3x)))))))))))))).
thf(conj_thm_2Epatricia_2EADD__TRANSFORM,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1t:$i] : ((mem@V1t@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V2k:tp__ty_2Enum_2Enum] : ( ! [V3d:$i] : ((mem@V3d@A_27a) => ((ap@(ap@(c_2Epatricia_2ETRANSFORM@A_27b@A_27a)@V0f)@(ap@(ap@(c_2Epatricia_2EADD@A_27a)@V1t)@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@A_27a)@(inj__ty_2Enum_2Enum @ V2k))@V3d))) = (ap@(ap@(c_2Epatricia_2EADD@A_27b)@(ap@(ap@(c_2Epatricia_2ETRANSFORM@A_27b@A_27a)@V0f)@V1t))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@A_27b)@(inj__ty_2Enum_2Enum @ V2k))@(ap@V0f@V3d)))))))))))))).
thf(conj_thm_2Epatricia_2ETRANSFORM__BRANCH,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1p:tp__ty_2Enum_2Enum] : ( ! [V2m:tp__ty_2Enum_2Enum] : ( ! [V3l:$i] : ((mem@V3l@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V4r:$i] : ((mem@V4r@(ty_2Epatricia_2Eptree@A_27a)) => ((ap@(ap@(c_2Epatricia_2ETRANSFORM@A_27b@A_27a)@V0f)@(ap@(c_2Epatricia_2EBRANCH@A_27a)@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))))@(inj__ty_2Enum_2Enum @ V1p))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a)))@(inj__ty_2Enum_2Enum @ V2m))@(ap@(ap@(c_2Epair_2E_2C@(ty_2Epatricia_2Eptree@A_27a)@(ty_2Epatricia_2Eptree@A_27a))@V3l)@V4r))))) = (ap@(c_2Epatricia_2EBRANCH@A_27b)@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27b)@(ty_2Epatricia_2Eptree@A_27b))))@(inj__ty_2Enum_2Enum @ V1p))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epatricia_2Eptree@A_27b)@(ty_2Epatricia_2Eptree@A_27b)))@(inj__ty_2Enum_2Enum @ V2m))@(ap@(ap@(c_2Epair_2E_2C@(ty_2Epatricia_2Eptree@A_27b)@(ty_2Epatricia_2Eptree@A_27b))@(ap@(ap@(c_2Epatricia_2ETRANSFORM@A_27b@A_27a)@V0f)@V3l))@(ap@(ap@(c_2Epatricia_2ETRANSFORM@A_27b@A_27a)@V0f)@V4r))))))))))))))))).
thf(conj_thm_2Epatricia_2EREMOVE__TRANSFORM,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1t:$i] : ((mem@V1t@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V2k:tp__ty_2Enum_2Enum] : ((ap@(ap@(c_2Epatricia_2ETRANSFORM@A_27b@A_27a)@V0f)@(ap@(ap@(c_2Epatricia_2EREMOVE@A_27a)@V1t)@(inj__ty_2Enum_2Enum @ V2k))) = (ap@(ap@(c_2Epatricia_2EREMOVE@A_27b)@(ap@(ap@(c_2Epatricia_2ETRANSFORM@A_27b@A_27a)@V0f)@V1t))@(inj__ty_2Enum_2Enum @ V2k))))))))))).
thf(conj_thm_2Epatricia_2EREMOVE__ADD__EQ,lemma,( ! [A_27a:del]: ( ! [V0t:$i] : ((mem@V0t@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2d:$i] : ((mem@V2d@A_27a) => ((ap@(ap@(c_2Epatricia_2EREMOVE@A_27a)@(ap@(ap@(c_2Epatricia_2EADD@A_27a)@V0t)@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@A_27a)@(inj__ty_2Enum_2Enum @ V1k))@V2d)))@(inj__ty_2Enum_2Enum @ V1k)) = (ap@(ap@(c_2Epatricia_2EREMOVE@A_27a)@V0t)@(inj__ty_2Enum_2Enum @ V1k)))))))))).
thf(conj_thm_2Epatricia_2EADD__ADD,lemma,( ! [A_27a:del]: ( ! [V0t:$i] : ((mem@V0t@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2d:$i] : ((mem@V2d@A_27a) => ( ! [V3e:$i] : ((mem@V3e@A_27a) => ((ap@(ap@(c_2Epatricia_2EADD@A_27a)@(ap@(ap@(c_2Epatricia_2EADD@A_27a)@V0t)@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@A_27a)@(inj__ty_2Enum_2Enum @ V1k))@V2d)))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@A_27a)@(inj__ty_2Enum_2Enum @ V1k))@V3e)) = (ap@(ap@(c_2Epatricia_2EADD@A_27a)@V0t)@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@A_27a)@(inj__ty_2Enum_2Enum @ V1k))@V3e)))))))))))).
thf(conj_thm_2Epatricia_2EEVERY__LEAF__PEEK,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@ty_2Enum_2Enum@(arr@A_27a@bool))) => ( ! [V1t:$i] : ((mem@V1t@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V2k:tp__ty_2Enum_2Enum] : (((p@(ap@(ap@(c_2Epatricia_2EEVERY__LEAF@A_27a)@V0P)@V1t)) & (p@(ap@(c_2Eoption_2EIS__SOME@A_27a)@(ap@(ap@(c_2Epatricia_2EPEEK@A_27a)@V1t)@(inj__ty_2Enum_2Enum @ V2k))))) => (p@(ap@(ap@V0P@(inj__ty_2Enum_2Enum @ V2k))@(ap@(c_2Eoption_2ETHE@A_27a)@(ap@(ap@(c_2Epatricia_2EPEEK@A_27a)@V1t)@(inj__ty_2Enum_2Enum @ V2k))))))))))))).
thf(conj_thm_2Epatricia_2EIS__PTREE__PEEK,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: (( ! [V0k:tp__ty_2Enum_2Enum] : (~~ (p@(ap@(c_2Eoption_2EIS__SOME@A_27a)@(ap@(ap@(c_2Epatricia_2EPEEK@A_27a)@(c_2Epatricia_2EEmpty@A_27a))@(inj__ty_2Enum_2Enum @ V0k)))))) & (( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2j:tp__ty_2Enum_2Enum] : ( ! [V3b:$i] : ((mem@V3b@A_27b) => ((p@(ap@(c_2Eoption_2EIS__SOME@A_27b)@(ap@(ap@(c_2Epatricia_2EPEEK@A_27b)@(ap@(ap@(c_2Epatricia_2ELeaf@A_27b)@(inj__ty_2Enum_2Enum @ V2j))@V3b))@(inj__ty_2Enum_2Enum @ V1k)))) <=> (V2j = V1k)))))) & ( ! [V4p:tp__ty_2Enum_2Enum] : ( ! [V5m:tp__ty_2Enum_2Enum] : ( ! [V6l:$i] : ((mem@V6l@(ty_2Epatricia_2Eptree@A_27c)) => ( ! [V7r:$i] : ((mem@V7r@(ty_2Epatricia_2Eptree@A_27c)) => ((p@(ap@(c_2Epatricia_2EIS__PTREE@A_27c)@(ap@(ap@(ap@(ap@(c_2Epatricia_2EBranch@A_27c)@(inj__ty_2Enum_2Enum @ V4p))@(inj__ty_2Enum_2Enum @ V5m))@V6l)@V7r))) => ((? [V8k:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Ebit_2EBIT@(inj__ty_2Enum_2Enum @ V5m))@(inj__ty_2Enum_2Enum @ V8k))) & (p@(ap@(c_2Eoption_2EIS__SOME@A_27c)@(ap@(ap@(c_2Epatricia_2EPEEK@A_27c)@V6l)@(inj__ty_2Enum_2Enum @ V8k)))))) & ((? [V9k:tp__ty_2Enum_2Enum] : ((~~ (p@(ap@(ap@c_2Ebit_2EBIT@(inj__ty_2Enum_2Enum @ V5m))@(inj__ty_2Enum_2Enum @ V9k)))) & (p@(ap@(c_2Eoption_2EIS__SOME@A_27c)@(ap@(ap@(c_2Epatricia_2EPEEK@A_27c)@V7r)@(inj__ty_2Enum_2Enum @ V9k)))))) & ( ! [V10k:tp__ty_2Enum_2Enum] : ( ! [V11n:tp__ty_2Enum_2Enum] : (((~~ (p@(ap@(ap@(ap@c_2Ebit_2EMOD__2EXP__EQ@(inj__ty_2Enum_2Enum @ V5m))@(inj__ty_2Enum_2Enum @ V10k))@(inj__ty_2Enum_2Enum @ V4p)))) | ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V11n))@(inj__ty_2Enum_2Enum @ V5m))) & (~~ ((p@(ap@(ap@c_2Ebit_2EBIT@(inj__ty_2Enum_2Enum @ V11n))@(inj__ty_2Enum_2Enum @ V4p))) <=> (p@(ap@(ap@c_2Ebit_2EBIT@(inj__ty_2Enum_2Enum @ V11n))@(inj__ty_2Enum_2Enum @ V10k))))))) => ((~~ (p@(ap@(c_2Eoption_2EIS__SOME@A_27c)@(ap@(ap@(c_2Epatricia_2EPEEK@A_27c)@V6l)@(inj__ty_2Enum_2Enum @ V10k))))) & (~~ (p@(ap@(c_2Eoption_2EIS__SOME@A_27c)@(ap@(ap@(c_2Epatricia_2EPEEK@A_27c)@V7r)@(inj__ty_2Enum_2Enum @ V10k)))))))))))))))))))))))).
thf(conj_thm_2Epatricia_2EPTREE__EQ,lemma,( ! [A_27a:del]: ( ! [V0t1:$i] : ((mem@V0t1@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V1t2:$i] : ((mem@V1t2@(ty_2Epatricia_2Eptree@A_27a)) => (((p@(ap@(c_2Epatricia_2EIS__PTREE@A_27a)@V0t1)) & (p@(ap@(c_2Epatricia_2EIS__PTREE@A_27a)@V1t2))) => (( ! [V2k:tp__ty_2Enum_2Enum] : ((ap@(ap@(c_2Epatricia_2EPEEK@A_27a)@V0t1)@(inj__ty_2Enum_2Enum @ V2k)) = (ap@(ap@(c_2Epatricia_2EPEEK@A_27a)@V1t2)@(inj__ty_2Enum_2Enum @ V2k)))) <=> (V0t1 = V1t2))))))))).
thf(conj_thm_2Epatricia_2EREMOVE__REMOVE,lemma,( ! [A_27a:del]: ( ! [V0t:$i] : ((mem@V0t@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V1k:tp__ty_2Enum_2Enum] : ((p@(ap@(c_2Epatricia_2EIS__PTREE@A_27a)@V0t)) => ((ap@(ap@(c_2Epatricia_2EREMOVE@A_27a)@(ap@(ap@(c_2Epatricia_2EREMOVE@A_27a)@V0t)@(inj__ty_2Enum_2Enum @ V1k)))@(inj__ty_2Enum_2Enum @ V1k)) = (ap@(ap@(c_2Epatricia_2EREMOVE@A_27a)@V0t)@(inj__ty_2Enum_2Enum @ V1k))))))))).
thf(conj_thm_2Epatricia_2EREMOVE__ADD,lemma,( ! [A_27a:del]: ( ! [V0t:$i] : ((mem@V0t@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2d:$i] : ((mem@V2d@A_27a) => ( ! [V3j:tp__ty_2Enum_2Enum] : ((p@(ap@(c_2Epatricia_2EIS__PTREE@A_27a)@V0t)) => ((ap@(ap@(c_2Epatricia_2EREMOVE@A_27a)@(ap@(ap@(c_2Epatricia_2EADD@A_27a)@V0t)@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@A_27a)@(inj__ty_2Enum_2Enum @ V1k))@V2d)))@(inj__ty_2Enum_2Enum @ V3j)) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Epatricia_2Eptree@A_27a))@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V1k))@(inj__ty_2Enum_2Enum @ V3j)))@(ap@(ap@(c_2Epatricia_2EREMOVE@A_27a)@V0t)@(inj__ty_2Enum_2Enum @ V3j)))@(ap@(ap@(c_2Epatricia_2EADD@A_27a)@(ap@(ap@(c_2Epatricia_2EREMOVE@A_27a)@V0t)@(inj__ty_2Enum_2Enum @ V3j)))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@A_27a)@(inj__ty_2Enum_2Enum @ V1k))@V2d))))))))))))).
thf(conj_thm_2Epatricia_2EADD__ADD__SYM,lemma,( ! [A_27a:del]: ( ! [V0t:$i] : ((mem@V0t@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2j:tp__ty_2Enum_2Enum] : ( ! [V3d:$i] : ((mem@V3d@A_27a) => ( ! [V4e:$i] : ((mem@V4e@A_27a) => (((p@(ap@(c_2Epatricia_2EIS__PTREE@A_27a)@V0t)) & (~~ (V1k = V2j))) => ((ap@(ap@(c_2Epatricia_2EADD@A_27a)@(ap@(ap@(c_2Epatricia_2EADD@A_27a)@V0t)@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@A_27a)@(inj__ty_2Enum_2Enum @ V1k))@V3d)))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@A_27a)@(inj__ty_2Enum_2Enum @ V2j))@V4e)) = (ap@(ap@(c_2Epatricia_2EADD@A_27a)@(ap@(ap@(c_2Epatricia_2EADD@A_27a)@V0t)@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@A_27a)@(inj__ty_2Enum_2Enum @ V2j))@V4e)))@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@A_27a)@(inj__ty_2Enum_2Enum @ V1k))@V3d)))))))))))))).
thf(conj_thm_2Epatricia_2EFILTER__ALL,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => (( ! [V2n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V2n))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))) => (~~ (p@(ap@V0P@(ap@(ap@(c_2Elist_2EEL@A_27a)@(inj__ty_2Enum_2Enum @ V2n))@V1l)))))) <=> ((ap@(ap@(c_2Elist_2EFILTER@A_27a)@V0P)@V1l) = (c_2Elist_2ENIL@A_27a))))))))).
thf(conj_thm_2Epatricia_2ETRAVERSE__TRANSFORM,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1t:$i] : ((mem@V1t@(ty_2Epatricia_2Eptree@A_27a)) => ((surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ (ap@(c_2Epatricia_2ETRAVERSE@A_27b)@(ap@(ap@(c_2Epatricia_2ETRANSFORM@A_27b@A_27a)@V0f)@V1t))) = (surj__c_ty_2Elist_2Elist_ty_2Enum_2Enum @ (ap@(c_2Epatricia_2ETRAVERSE@A_27a)@V1t)))))))))).
thf(conj_thm_2Epatricia_2EMEM__TRAVERSE__PEEK,conjecture,( ! [A_27a:del]: ( ! [V0t:$i] : ((mem@V0t@(ty_2Epatricia_2Eptree@A_27a)) => ( ! [V1k:tp__ty_2Enum_2Enum] : ((p@(ap@(c_2Epatricia_2EIS__PTREE@A_27a)@V0t)) => ((p@(ap@(ap@(c_2Ebool_2EIN@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V1k))@(ap@(c_2Elist_2ELIST__TO__SET@ty_2Enum_2Enum)@(ap@(c_2Epatricia_2ETRAVERSE@A_27a)@V0t)))) <=> (p@(ap@(c_2Eoption_2EIS__SOME@A_27a)@(ap@(ap@(c_2Epatricia_2EPEEK@A_27a)@V0t)@(inj__ty_2Enum_2Enum @ V1k))))))))))).
