include('Axioms/alignment_2.ax').
tff(tp_ty_2Esptree_2Espt,type,( ty_2Esptree_2Espt: del > del )).
tff(tp_c_2Esptree_2EBN,type,(c_2Esptree_2EBN:del > $i)).
tff(mem_c_2Esptree_2EBN,axiom,( ! [A_27a:del] : mem(c_2Esptree_2EBN(A_27a),arr(ty_2Esptree_2Espt(A_27a),arr(ty_2Esptree_2Espt(A_27a),ty_2Esptree_2Espt(A_27a)))))).
tff(tp_c_2Esptree_2EBS,type,(c_2Esptree_2EBS:del > $i)).
tff(mem_c_2Esptree_2EBS,axiom,( ! [A_27a:del] : mem(c_2Esptree_2EBS(A_27a),arr(ty_2Esptree_2Espt(A_27a),arr(A_27a,arr(ty_2Esptree_2Espt(A_27a),ty_2Esptree_2Espt(A_27a))))))).
tff(tp_c_2Esptree_2ELN,type,(c_2Esptree_2ELN:del > $i)).
tff(mem_c_2Esptree_2ELN,axiom,( ! [A_27a:del] : mem(c_2Esptree_2ELN(A_27a),ty_2Esptree_2Espt(A_27a)))).
tff(tp_c_2Esptree_2ELS,type,(c_2Esptree_2ELS:del > $i)).
tff(mem_c_2Esptree_2ELS,axiom,( ! [A_27a:del] : mem(c_2Esptree_2ELS(A_27a),arr(A_27a,ty_2Esptree_2Espt(A_27a))))).
tff(tp_c_2Esptree_2Edelete,type,(c_2Esptree_2Edelete:del > $i)).
tff(mem_c_2Esptree_2Edelete,axiom,( ! [A_27a:del] : mem(c_2Esptree_2Edelete(A_27a),arr(ty_2Enum_2Enum,arr(ty_2Esptree_2Espt(A_27a),ty_2Esptree_2Espt(A_27a)))))).
tff(tp_c_2Esptree_2Edifference,type,(c_2Esptree_2Edifference:(del * del) > $i)).
tff(mem_c_2Esptree_2Edifference,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Esptree_2Edifference(A_27a,A_27b),arr(ty_2Esptree_2Espt(A_27a),arr(ty_2Esptree_2Espt(A_27b),ty_2Esptree_2Espt(A_27a))))))).
tff(tp_c_2Esptree_2Edomain,type,(c_2Esptree_2Edomain:del > $i)).
tff(mem_c_2Esptree_2Edomain,axiom,( ! [A_27a:del] : mem(c_2Esptree_2Edomain(A_27a),arr(ty_2Esptree_2Espt(A_27a),arr(ty_2Enum_2Enum,bool))))).
tff(tp_c_2Esptree_2Efilter__v,type,(c_2Esptree_2Efilter__v:del > $i)).
tff(mem_c_2Esptree_2Efilter__v,axiom,( ! [A_27a:del] : mem(c_2Esptree_2Efilter__v(A_27a),arr(arr(A_27a,bool),arr(ty_2Esptree_2Espt(A_27a),ty_2Esptree_2Espt(A_27a)))))).
tff(tp_c_2Esptree_2Efoldi,type,(c_2Esptree_2Efoldi:(del * del) > $i)).
tff(mem_c_2Esptree_2Efoldi,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Esptree_2Efoldi(A_27a,A_27b),arr(arr(ty_2Enum_2Enum,arr(A_27b,arr(A_27a,A_27a))),arr(ty_2Enum_2Enum,arr(A_27a,arr(ty_2Esptree_2Espt(A_27b),A_27a)))))))).
tff(tp_c_2Esptree_2EfromAList,type,(c_2Esptree_2EfromAList:del > $i)).
tff(mem_c_2Esptree_2EfromAList,axiom,( ! [A_27a:del] : mem(c_2Esptree_2EfromAList(A_27a),arr(ty_2Elist_2Elist(ty_2Epair_2Eprod(ty_2Enum_2Enum,A_27a)),ty_2Esptree_2Espt(A_27a))))).
tff(tp_c_2Esptree_2EfromList,type,(c_2Esptree_2EfromList:del > $i)).
tff(mem_c_2Esptree_2EfromList,axiom,( ! [A_27a:del] : mem(c_2Esptree_2EfromList(A_27a),arr(ty_2Elist_2Elist(A_27a),ty_2Esptree_2Espt(A_27a))))).
tff(tp_c_2Esptree_2Einsert,type,(c_2Esptree_2Einsert:del > $i)).
tff(mem_c_2Esptree_2Einsert,axiom,( ! [A_27a:del] : mem(c_2Esptree_2Einsert(A_27a),arr(ty_2Enum_2Enum,arr(A_27a,arr(ty_2Esptree_2Espt(A_27a),ty_2Esptree_2Espt(A_27a))))))).
tff(tp_c_2Esptree_2Einter,type,(c_2Esptree_2Einter:(del * del) > $i)).
tff(mem_c_2Esptree_2Einter,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Esptree_2Einter(A_27a,A_27b),arr(ty_2Esptree_2Espt(A_27a),arr(ty_2Esptree_2Espt(A_27b),ty_2Esptree_2Espt(A_27a))))))).
tff(tp_c_2Esptree_2Einter__eq,type,(c_2Esptree_2Einter__eq:del > $i)).
tff(mem_c_2Esptree_2Einter__eq,axiom,( ! [A_27a:del] : mem(c_2Esptree_2Einter__eq(A_27a),arr(ty_2Esptree_2Espt(A_27a),arr(ty_2Esptree_2Espt(A_27a),ty_2Esptree_2Espt(A_27a)))))).
tff(stp_c_ty_2Esptree_2Espt_ty_2Eone_2Eone,type,(tp__c_ty_2Esptree_2Espt_ty_2Eone_2Eone : $tType)).
tff(stp_inj_c_ty_2Esptree_2Espt_ty_2Eone_2Eone,type,(inj__c_ty_2Esptree_2Espt_ty_2Eone_2Eone : tp__c_ty_2Esptree_2Espt_ty_2Eone_2Eone > $i)).
tff(stp_surj_c_ty_2Esptree_2Espt_ty_2Eone_2Eone,type,(surj__c_ty_2Esptree_2Espt_ty_2Eone_2Eone : $i > tp__c_ty_2Esptree_2Espt_ty_2Eone_2Eone)).
tff(stp_inj_surj_c_ty_2Esptree_2Espt_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Esptree_2Espt_ty_2Eone_2Eone] : (surj__c_ty_2Esptree_2Espt_ty_2Eone_2Eone(inj__c_ty_2Esptree_2Espt_ty_2Eone_2Eone(X)) = X))).
tff(stp_inj_mem_c_ty_2Esptree_2Espt_ty_2Eone_2Eone,axiom,( ! [X:tp__c_ty_2Esptree_2Espt_ty_2Eone_2Eone] : (mem(inj__c_ty_2Esptree_2Espt_ty_2Eone_2Eone(X),ty_2Esptree_2Espt(ty_2Eone_2Eone))))).
tff(stp_iso_mem_c_ty_2Esptree_2Espt_ty_2Eone_2Eone,axiom,( ! [X:$i] : (mem(X,ty_2Esptree_2Espt(ty_2Eone_2Eone)) => (X = inj__c_ty_2Esptree_2Espt_ty_2Eone_2Eone(surj__c_ty_2Esptree_2Espt_ty_2Eone_2Eone(X)))))).
tff(tp_c_2Esptree_2Elist__insert,type,(c_2Esptree_2Elist__insert:$i)).
tff(mem_c_2Esptree_2Elist__insert,axiom,mem(c_2Esptree_2Elist__insert,arr(ty_2Elist_2Elist(ty_2Enum_2Enum),arr(ty_2Esptree_2Espt(ty_2Eone_2Eone),ty_2Esptree_2Espt(ty_2Eone_2Eone))))).
tff(tp_c_2Esptree_2Elist__to__num__set,type,(c_2Esptree_2Elist__to__num__set:$i)).
tff(mem_c_2Esptree_2Elist__to__num__set,axiom,mem(c_2Esptree_2Elist__to__num__set,arr(ty_2Elist_2Elist(ty_2Enum_2Enum),ty_2Esptree_2Espt(ty_2Eone_2Eone)))).
tff(tp_c_2Esptree_2Elookup,type,(c_2Esptree_2Elookup:del > $i)).
tff(mem_c_2Esptree_2Elookup,axiom,( ! [A_27a:del] : mem(c_2Esptree_2Elookup(A_27a),arr(ty_2Enum_2Enum,arr(ty_2Esptree_2Espt(A_27a),ty_2Eoption_2Eoption(A_27a)))))).
tff(tp_c_2Esptree_2Elrnext,type,(c_2Esptree_2Elrnext:$i)).
tff(mem_c_2Esptree_2Elrnext,axiom,mem(c_2Esptree_2Elrnext,arr(ty_2Enum_2Enum,ty_2Enum_2Enum))).
tff(stp_fo_c_2Esptree_2Elrnext,type,(fo__c_2Esptree_2Elrnext:(tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Esptree_2Elrnext,axiom,( ! [X0:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Esptree_2Elrnext(X0)) = ap(c_2Esptree_2Elrnext,inj__ty_2Enum_2Enum(X0))))).
tff(tp_c_2Esptree_2Emap,type,(c_2Esptree_2Emap:(del * del) > $i)).
tff(mem_c_2Esptree_2Emap,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Esptree_2Emap(A_27a,A_27b),arr(arr(A_27b,A_27a),arr(ty_2Esptree_2Espt(A_27b),ty_2Esptree_2Espt(A_27a))))))).
tff(tp_c_2Esptree_2Emapi,type,(c_2Esptree_2Emapi:(del * del) > $i)).
tff(mem_c_2Esptree_2Emapi,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Esptree_2Emapi(A_27a,A_27b),arr(arr(ty_2Enum_2Enum,arr(A_27b,A_27a)),arr(ty_2Esptree_2Espt(A_27b),ty_2Esptree_2Espt(A_27a))))))).
tff(tp_c_2Esptree_2Emapi0,type,(c_2Esptree_2Emapi0:(del * del) > $i)).
tff(mem_c_2Esptree_2Emapi0,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Esptree_2Emapi0(A_27a,A_27b),arr(arr(ty_2Enum_2Enum,arr(A_27b,A_27a)),arr(ty_2Enum_2Enum,arr(ty_2Esptree_2Espt(A_27b),ty_2Esptree_2Espt(A_27a)))))))).
tff(tp_c_2Esptree_2Emk__BN,type,(c_2Esptree_2Emk__BN:del > $i)).
tff(mem_c_2Esptree_2Emk__BN,axiom,( ! [A_27a:del] : mem(c_2Esptree_2Emk__BN(A_27a),arr(ty_2Esptree_2Espt(A_27a),arr(ty_2Esptree_2Espt(A_27a),ty_2Esptree_2Espt(A_27a)))))).
tff(tp_c_2Esptree_2Emk__BS,type,(c_2Esptree_2Emk__BS:del > $i)).
tff(mem_c_2Esptree_2Emk__BS,axiom,( ! [A_27a:del] : mem(c_2Esptree_2Emk__BS(A_27a),arr(ty_2Esptree_2Espt(A_27a),arr(A_27a,arr(ty_2Esptree_2Espt(A_27a),ty_2Esptree_2Espt(A_27a))))))).
tff(tp_c_2Esptree_2Emk__wf,type,(c_2Esptree_2Emk__wf:del > $i)).
tff(mem_c_2Esptree_2Emk__wf,axiom,( ! [A_27a:del] : mem(c_2Esptree_2Emk__wf(A_27a),arr(ty_2Esptree_2Espt(A_27a),ty_2Esptree_2Espt(A_27a))))).
tff(tp_c_2Esptree_2Esize,type,(c_2Esptree_2Esize:del > $i)).
tff(mem_c_2Esptree_2Esize,axiom,( ! [A_27a:del] : mem(c_2Esptree_2Esize(A_27a),arr(ty_2Esptree_2Espt(A_27a),ty_2Enum_2Enum)))).
tff(tp_c_2Esptree_2Espt__CASE,type,(c_2Esptree_2Espt__CASE:(del * del) > $i)).
tff(mem_c_2Esptree_2Espt__CASE,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Esptree_2Espt__CASE(A_27a,A_27b),arr(ty_2Esptree_2Espt(A_27a),arr(A_27b,arr(arr(A_27a,A_27b),arr(arr(ty_2Esptree_2Espt(A_27a),arr(ty_2Esptree_2Espt(A_27a),A_27b)),arr(arr(ty_2Esptree_2Espt(A_27a),arr(A_27a,arr(ty_2Esptree_2Espt(A_27a),A_27b))),A_27b))))))))).
tff(tp_c_2Esptree_2Espt__acc,type,(c_2Esptree_2Espt__acc:$i)).
tff(mem_c_2Esptree_2Espt__acc,axiom,mem(c_2Esptree_2Espt__acc,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,ty_2Enum_2Enum)))).
tff(stp_fo_c_2Esptree_2Espt__acc,type,(fo__c_2Esptree_2Espt__acc:(tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum) > tp__ty_2Enum_2Enum)).
tff(stp_eq_fo_c_2Esptree_2Espt__acc,axiom,( ! [X0:tp__ty_2Enum_2Enum] : ( ! [X1:tp__ty_2Enum_2Enum] : (inj__ty_2Enum_2Enum(fo__c_2Esptree_2Espt__acc(X0,X1)) = ap(ap(c_2Esptree_2Espt__acc,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))))).
tff(tp_c_2Esptree_2Espt__center,type,(c_2Esptree_2Espt__center:del > $i)).
tff(mem_c_2Esptree_2Espt__center,axiom,( ! [A_27a:del] : mem(c_2Esptree_2Espt__center(A_27a),arr(ty_2Esptree_2Espt(A_27a),ty_2Eoption_2Eoption(A_27a))))).
tff(tp_c_2Esptree_2Espt__fold,type,(c_2Esptree_2Espt__fold:(del * del) > $i)).
tff(mem_c_2Esptree_2Espt__fold,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Esptree_2Espt__fold(A_27a,A_27b),arr(arr(A_27b,arr(A_27a,A_27a)),arr(A_27a,arr(ty_2Esptree_2Espt(A_27b),A_27a))))))).
tff(tp_c_2Esptree_2Espt__left,type,(c_2Esptree_2Espt__left:del > $i)).
tff(mem_c_2Esptree_2Espt__left,axiom,( ! [A_27a:del] : mem(c_2Esptree_2Espt__left(A_27a),arr(ty_2Esptree_2Espt(A_27a),ty_2Esptree_2Espt(A_27a))))).
tff(tp_c_2Esptree_2Espt__right,type,(c_2Esptree_2Espt__right:del > $i)).
tff(mem_c_2Esptree_2Espt__right,axiom,( ! [A_27a:del] : mem(c_2Esptree_2Espt__right(A_27a),arr(ty_2Esptree_2Espt(A_27a),ty_2Esptree_2Espt(A_27a))))).
tff(tp_c_2Esptree_2Espt__size,type,(c_2Esptree_2Espt__size:del > $i)).
tff(mem_c_2Esptree_2Espt__size,axiom,( ! [A_27a:del] : mem(c_2Esptree_2Espt__size(A_27a),arr(arr(A_27a,ty_2Enum_2Enum),arr(ty_2Esptree_2Espt(A_27a),ty_2Enum_2Enum))))).
tff(tp_c_2Esptree_2Esubspt,type,(c_2Esptree_2Esubspt:del > $i)).
tff(mem_c_2Esptree_2Esubspt,axiom,( ! [A_27a:del] : mem(c_2Esptree_2Esubspt(A_27a),arr(ty_2Esptree_2Espt(A_27a),arr(ty_2Esptree_2Espt(A_27a),bool))))).
tff(tp_c_2Esptree_2EtoAList,type,(c_2Esptree_2EtoAList:del > $i)).
tff(mem_c_2Esptree_2EtoAList,axiom,( ! [A_27a:del] : mem(c_2Esptree_2EtoAList(A_27a),arr(ty_2Esptree_2Espt(A_27a),ty_2Elist_2Elist(ty_2Epair_2Eprod(ty_2Enum_2Enum,A_27a)))))).
tff(tp_c_2Esptree_2EtoList,type,(c_2Esptree_2EtoList:del > $i)).
tff(mem_c_2Esptree_2EtoList,axiom,( ! [A_27a:del] : mem(c_2Esptree_2EtoList(A_27a),arr(ty_2Esptree_2Espt(A_27a),ty_2Elist_2Elist(A_27a))))).
tff(tp_c_2Esptree_2EtoListA,type,(c_2Esptree_2EtoListA:del > $i)).
tff(mem_c_2Esptree_2EtoListA,axiom,( ! [A_27a:del] : mem(c_2Esptree_2EtoListA(A_27a),arr(ty_2Elist_2Elist(A_27a),arr(ty_2Esptree_2Espt(A_27a),ty_2Elist_2Elist(A_27a)))))).
tff(tp_c_2Esptree_2Eunion,type,(c_2Esptree_2Eunion:del > $i)).
tff(mem_c_2Esptree_2Eunion,axiom,( ! [A_27a:del] : mem(c_2Esptree_2Eunion(A_27a),arr(ty_2Esptree_2Espt(A_27a),arr(ty_2Esptree_2Espt(A_27a),ty_2Esptree_2Espt(A_27a)))))).
tff(tp_c_2Esptree_2Ewf,type,(c_2Esptree_2Ewf:del > $i)).
tff(mem_c_2Esptree_2Ewf,axiom,( ! [A_27a:del] : mem(c_2Esptree_2Ewf(A_27a),arr(ty_2Esptree_2Espt(A_27a),bool)))).
tff(ax_thm_2Esptree_2Espt__TY__DEF,axiom,( ! [A_27a:del]: (? [V0rep:$i] : (mem(V0rep,arr(ty_2Esptree_2Espt(A_27a),ty_2Eind__type_2Erecspace(A_27a))) & p(ap(ap(c_2Ebool_2ETYPE__DEFINITION(ty_2Eind__type_2Erecspace(A_27a),ty_2Esptree_2Espt(A_27a)),f2345(A_27a)),V0rep)))))).
tff(ax_thm_2Esptree_2Espt__case__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0v:$i] : (mem(V0v,A_27b) => ( ! [V1f:$i] : (mem(V1f,arr(A_27a,A_27b)) => ( ! [V2f1:$i] : (mem(V2f1,arr(ty_2Esptree_2Espt(A_27a),arr(ty_2Esptree_2Espt(A_27a),A_27b))) => ( ! [V3f2:$i] : (mem(V3f2,arr(ty_2Esptree_2Espt(A_27a),arr(A_27a,arr(ty_2Esptree_2Espt(A_27a),A_27b)))) => (ap(ap(ap(ap(ap(c_2Esptree_2Espt__CASE(A_27a,A_27b),c_2Esptree_2ELN(A_27a)),V0v),V1f),V2f1),V3f2) = V0v))))))))) & (( ! [V4a:$i] : (mem(V4a,A_27a) => ( ! [V5v:$i] : (mem(V5v,A_27b) => ( ! [V6f:$i] : (mem(V6f,arr(A_27a,A_27b)) => ( ! [V7f1:$i] : (mem(V7f1,arr(ty_2Esptree_2Espt(A_27a),arr(ty_2Esptree_2Espt(A_27a),A_27b))) => ( ! [V8f2:$i] : (mem(V8f2,arr(ty_2Esptree_2Espt(A_27a),arr(A_27a,arr(ty_2Esptree_2Espt(A_27a),A_27b)))) => (ap(ap(ap(ap(ap(c_2Esptree_2Espt__CASE(A_27a,A_27b),ap(c_2Esptree_2ELS(A_27a),V4a)),V5v),V6f),V7f1),V8f2) = ap(V6f,V4a)))))))))))) & (( ! [V9a0:$i] : (mem(V9a0,ty_2Esptree_2Espt(A_27a)) => ( ! [V10a1:$i] : (mem(V10a1,ty_2Esptree_2Espt(A_27a)) => ( ! [V11v:$i] : (mem(V11v,A_27b) => ( ! [V12f:$i] : (mem(V12f,arr(A_27a,A_27b)) => ( ! [V13f1:$i] : (mem(V13f1,arr(ty_2Esptree_2Espt(A_27a),arr(ty_2Esptree_2Espt(A_27a),A_27b))) => ( ! [V14f2:$i] : (mem(V14f2,arr(ty_2Esptree_2Espt(A_27a),arr(A_27a,arr(ty_2Esptree_2Espt(A_27a),A_27b)))) => (ap(ap(ap(ap(ap(c_2Esptree_2Espt__CASE(A_27a,A_27b),ap(ap(c_2Esptree_2EBN(A_27a),V9a0),V10a1)),V11v),V12f),V13f1),V14f2) = ap(ap(V13f1,V9a0),V10a1)))))))))))))) & ( ! [V15a0:$i] : (mem(V15a0,ty_2Esptree_2Espt(A_27a)) => ( ! [V16a1:$i] : (mem(V16a1,A_27a) => ( ! [V17a2:$i] : (mem(V17a2,ty_2Esptree_2Espt(A_27a)) => ( ! [V18v:$i] : (mem(V18v,A_27b) => ( ! [V19f:$i] : (mem(V19f,arr(A_27a,A_27b)) => ( ! [V20f1:$i] : (mem(V20f1,arr(ty_2Esptree_2Espt(A_27a),arr(ty_2Esptree_2Espt(A_27a),A_27b))) => ( ! [V21f2:$i] : (mem(V21f2,arr(ty_2Esptree_2Espt(A_27a),arr(A_27a,arr(ty_2Esptree_2Espt(A_27a),A_27b)))) => (ap(ap(ap(ap(ap(c_2Esptree_2Espt__CASE(A_27a,A_27b),ap(ap(ap(c_2Esptree_2EBS(A_27a),V15a0),V16a1),V17a2)),V18v),V19f),V20f1),V21f2) = ap(ap(ap(V21f2,V15a0),V16a1),V17a2)))))))))))))))))))))).
tff(ax_thm_2Esptree_2Espt__size__def,axiom,( ! [A_27a:del]: (( ! [V0f:$i] : (mem(V0f,arr(A_27a,ty_2Enum_2Enum)) => (surj__ty_2Enum_2Enum(ap(ap(c_2Esptree_2Espt__size(A_27a),V0f),c_2Esptree_2ELN(A_27a))) = fo__c_2Enum_2E0))) & (( ! [V1f:$i] : (mem(V1f,arr(A_27a,ty_2Enum_2Enum)) => ( ! [V2a:$i] : (mem(V2a,A_27a) => (surj__ty_2Enum_2Enum(ap(ap(c_2Esptree_2Espt__size(A_27a),V1f),ap(c_2Esptree_2ELS(A_27a),V2a))) = 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(V1f,V2a)))))))) & (( ! [V3f:$i] : (mem(V3f,arr(A_27a,ty_2Enum_2Enum)) => ( ! [V4a0:$i] : (mem(V4a0,ty_2Esptree_2Espt(A_27a)) => ( ! [V5a1:$i] : (mem(V5a1,ty_2Esptree_2Espt(A_27a)) => (surj__ty_2Enum_2Enum(ap(ap(c_2Esptree_2Espt__size(A_27a),V3f),ap(ap(c_2Esptree_2EBN(A_27a),V4a0),V5a1))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Esptree_2Espt__size(A_27a),V3f),V4a0)),ap(ap(c_2Esptree_2Espt__size(A_27a),V3f),V5a1))))))))))) & ( ! [V6f:$i] : (mem(V6f,arr(A_27a,ty_2Enum_2Enum)) => ( ! [V7a0:$i] : (mem(V7a0,ty_2Esptree_2Espt(A_27a)) => ( ! [V8a1:$i] : (mem(V8a1,A_27a) => ( ! [V9a2:$i] : (mem(V9a2,ty_2Esptree_2Espt(A_27a)) => (surj__ty_2Enum_2Enum(ap(ap(c_2Esptree_2Espt__size(A_27a),V6f),ap(ap(ap(c_2Esptree_2EBS(A_27a),V7a0),V8a1),V9a2))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Esptree_2Espt__size(A_27a),V6f),V7a0)),ap(ap(c_2Earithmetic_2E_2B,ap(V6f,V8a1)),ap(ap(c_2Esptree_2Espt__size(A_27a),V6f),V9a2))))))))))))))))))).
tff(conj_thm_2Esptree_2Edatatype__spt,lemma,(( ! [A_27a:del]: ( ! [V0spt:$i] : (mem(V0spt,arr(ty_2Esptree_2Espt(A_27a),arr(arr(A_27a,ty_2Esptree_2Espt(A_27a)),arr(arr(ty_2Esptree_2Espt(A_27a),arr(ty_2Esptree_2Espt(A_27a),ty_2Esptree_2Espt(A_27a))),arr(arr(ty_2Esptree_2Espt(A_27a),arr(A_27a,arr(ty_2Esptree_2Espt(A_27a),ty_2Esptree_2Espt(A_27a)))),bool))))) => p(ap(c_2Ebool_2EDATATYPE(bool),ap(ap(ap(ap(V0spt,c_2Esptree_2ELN(A_27a)),c_2Esptree_2ELS(A_27a)),c_2Esptree_2EBN(A_27a)),c_2Esptree_2EBS(A_27a))))))))).
tff(conj_thm_2Esptree_2Espt__11,lemma,(( ! [A_27a:del]: (( ! [V0a:$i] : (mem(V0a,A_27a) => ( ! [V1a_27:$i] : (mem(V1a_27,A_27a) => ((ap(c_2Esptree_2ELS(A_27a),V0a) = ap(c_2Esptree_2ELS(A_27a),V1a_27)) <=> (V0a = V1a_27)))))) & (( ! [V2a0:$i] : (mem(V2a0,ty_2Esptree_2Espt(A_27a)) => ( ! [V3a1:$i] : (mem(V3a1,ty_2Esptree_2Espt(A_27a)) => ( ! [V4a0_27:$i] : (mem(V4a0_27,ty_2Esptree_2Espt(A_27a)) => ( ! [V5a1_27:$i] : (mem(V5a1_27,ty_2Esptree_2Espt(A_27a)) => ((ap(ap(c_2Esptree_2EBN(A_27a),V2a0),V3a1) = ap(ap(c_2Esptree_2EBN(A_27a),V4a0_27),V5a1_27)) <=> ((V2a0 = V4a0_27) & (V3a1 = V5a1_27))))))))))) & ( ! [V6a0:$i] : (mem(V6a0,ty_2Esptree_2Espt(A_27a)) => ( ! [V7a1:$i] : (mem(V7a1,A_27a) => ( ! [V8a2:$i] : (mem(V8a2,ty_2Esptree_2Espt(A_27a)) => ( ! [V9a0_27:$i] : (mem(V9a0_27,ty_2Esptree_2Espt(A_27a)) => ( ! [V10a1_27:$i] : (mem(V10a1_27,A_27a) => ( ! [V11a2_27:$i] : (mem(V11a2_27,ty_2Esptree_2Espt(A_27a)) => ((ap(ap(ap(c_2Esptree_2EBS(A_27a),V6a0),V7a1),V8a2) = ap(ap(ap(c_2Esptree_2EBS(A_27a),V9a0_27),V10a1_27),V11a2_27)) <=> ((V6a0 = V9a0_27) & ((V7a1 = V10a1_27) & (V8a2 = V11a2_27))))))))))))))))))))).
tff(conj_thm_2Esptree_2Espt__distinct,lemma,(( ! [A_27a:del]: (( ! [V0a:$i] : (mem(V0a,A_27a) => (~~ (c_2Esptree_2ELN(A_27a) = ap(c_2Esptree_2ELS(A_27a),V0a))))) & (( ! [V1a1:$i] : (mem(V1a1,ty_2Esptree_2Espt(A_27a)) => ( ! [V2a0:$i] : (mem(V2a0,ty_2Esptree_2Espt(A_27a)) => (~~ (c_2Esptree_2ELN(A_27a) = ap(ap(c_2Esptree_2EBN(A_27a),V2a0),V1a1))))))) & (( ! [V3a2:$i] : (mem(V3a2,ty_2Esptree_2Espt(A_27a)) => ( ! [V4a1:$i] : (mem(V4a1,A_27a) => ( ! [V5a0:$i] : (mem(V5a0,ty_2Esptree_2Espt(A_27a)) => (~~ (c_2Esptree_2ELN(A_27a) = ap(ap(ap(c_2Esptree_2EBS(A_27a),V5a0),V4a1),V3a2))))))))) & (( ! [V6a1:$i] : (mem(V6a1,ty_2Esptree_2Espt(A_27a)) => ( ! [V7a0:$i] : (mem(V7a0,ty_2Esptree_2Espt(A_27a)) => ( ! [V8a:$i] : (mem(V8a,A_27a) => (~~ (ap(c_2Esptree_2ELS(A_27a),V8a) = ap(ap(c_2Esptree_2EBN(A_27a),V7a0),V6a1))))))))) & (( ! [V9a2:$i] : (mem(V9a2,ty_2Esptree_2Espt(A_27a)) => ( ! [V10a1:$i] : (mem(V10a1,A_27a) => ( ! [V11a0:$i] : (mem(V11a0,ty_2Esptree_2Espt(A_27a)) => ( ! [V12a:$i] : (mem(V12a,A_27a) => (~~ (ap(c_2Esptree_2ELS(A_27a),V12a) = ap(ap(ap(c_2Esptree_2EBS(A_27a),V11a0),V10a1),V9a2))))))))))) & ( ! [V13a2:$i] : (mem(V13a2,ty_2Esptree_2Espt(A_27a)) => ( ! [V14a1_27:$i] : (mem(V14a1_27,A_27a) => ( ! [V15a1:$i] : (mem(V15a1,ty_2Esptree_2Espt(A_27a)) => ( ! [V16a0_27:$i] : (mem(V16a0_27,ty_2Esptree_2Espt(A_27a)) => ( ! [V17a0:$i] : (mem(V17a0,ty_2Esptree_2Espt(A_27a)) => (~~ (ap(ap(c_2Esptree_2EBN(A_27a),V17a0),V15a1) = ap(ap(ap(c_2Esptree_2EBS(A_27a),V16a0_27),V14a1_27),V13a2))))))))))))))))))))).
tff(conj_thm_2Esptree_2Espt__nchotomy,lemma,(( ! [A_27a:del]: ( ! [V0ss:$i] : (mem(V0ss,ty_2Esptree_2Espt(A_27a)) => ((V0ss = c_2Esptree_2ELN(A_27a)) | ((? [V1a:$i] : (mem(V1a,A_27a) & (V0ss = ap(c_2Esptree_2ELS(A_27a),V1a)))) | ((? [V2s:$i] : (mem(V2s,ty_2Esptree_2Espt(A_27a)) & (? [V3s0:$i] : (mem(V3s0,ty_2Esptree_2Espt(A_27a)) & (V0ss = ap(ap(c_2Esptree_2EBN(A_27a),V2s),V3s0)))))) | (? [V4s:$i] : (mem(V4s,ty_2Esptree_2Espt(A_27a)) & (? [V5a:$i] : (mem(V5a,A_27a) & (? [V6s0:$i] : (mem(V6s0,ty_2Esptree_2Espt(A_27a)) & (V0ss = ap(ap(ap(c_2Esptree_2EBS(A_27a),V4s),V5a),V6s0)))))))))))))))).
tff(conj_thm_2Esptree_2Espt__Axiom,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f0:$i] : (mem(V0f0,A_27b) => ( ! [V1f1:$i] : (mem(V1f1,arr(A_27a,A_27b)) => ( ! [V2f2:$i] : (mem(V2f2,arr(ty_2Esptree_2Espt(A_27a),arr(ty_2Esptree_2Espt(A_27a),arr(A_27b,arr(A_27b,A_27b))))) => ( ! [V3f3:$i] : (mem(V3f3,arr(A_27a,arr(ty_2Esptree_2Espt(A_27a),arr(ty_2Esptree_2Espt(A_27a),arr(A_27b,arr(A_27b,A_27b)))))) => (? [V4fn:$i] : (mem(V4fn,arr(ty_2Esptree_2Espt(A_27a),A_27b)) & ((ap(V4fn,c_2Esptree_2ELN(A_27a)) = V0f0) & (( ! [V5a:$i] : (mem(V5a,A_27a) => (ap(V4fn,ap(c_2Esptree_2ELS(A_27a),V5a)) = ap(V1f1,V5a)))) & (( ! [V6a0:$i] : (mem(V6a0,ty_2Esptree_2Espt(A_27a)) => ( ! [V7a1:$i] : (mem(V7a1,ty_2Esptree_2Espt(A_27a)) => (ap(V4fn,ap(ap(c_2Esptree_2EBN(A_27a),V6a0),V7a1)) = ap(ap(ap(ap(V2f2,V6a0),V7a1),ap(V4fn,V6a0)),ap(V4fn,V7a1))))))) & ( ! [V8a0:$i] : (mem(V8a0,ty_2Esptree_2Espt(A_27a)) => ( ! [V9a1:$i] : (mem(V9a1,A_27a) => ( ! [V10a2:$i] : (mem(V10a2,ty_2Esptree_2Espt(A_27a)) => (ap(V4fn,ap(ap(ap(c_2Esptree_2EBS(A_27a),V8a0),V9a1),V10a2)) = ap(ap(ap(ap(ap(V3f3,V9a1),V8a0),V10a2),ap(V4fn,V8a0)),ap(V4fn,V10a2)))))))))))))))))))))))))).
tff(conj_thm_2Esptree_2Espt__induction,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Esptree_2Espt(A_27a),bool)) => ((p(ap(V0P,c_2Esptree_2ELN(A_27a))) & (( ! [V1a:$i] : (mem(V1a,A_27a) => p(ap(V0P,ap(c_2Esptree_2ELS(A_27a),V1a))))) & (( ! [V2s:$i] : (mem(V2s,ty_2Esptree_2Espt(A_27a)) => ( ! [V3s0:$i] : (mem(V3s0,ty_2Esptree_2Espt(A_27a)) => ((p(ap(V0P,V2s)) & p(ap(V0P,V3s0))) => p(ap(V0P,ap(ap(c_2Esptree_2EBN(A_27a),V2s),V3s0)))))))) & ( ! [V4s:$i] : (mem(V4s,ty_2Esptree_2Espt(A_27a)) => ( ! [V5s0:$i] : (mem(V5s0,ty_2Esptree_2Espt(A_27a)) => ((p(ap(V0P,V4s)) & p(ap(V0P,V5s0))) => ( ! [V6a:$i] : (mem(V6a,A_27a) => p(ap(V0P,ap(ap(ap(c_2Esptree_2EBS(A_27a),V4s),V6a),V5s0))))))))))))) => ( ! [V7s:$i] : (mem(V7s,ty_2Esptree_2Espt(A_27a)) => p(ap(V0P,V7s)))))))))).
tff(conj_thm_2Esptree_2Espt__case__cong,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0v_27:$i] : (mem(V0v_27,A_27b) => ( ! [V1f_27:$i] : (mem(V1f_27,arr(A_27a,A_27b)) => ( ! [V2f1_27:$i] : (mem(V2f1_27,arr(ty_2Esptree_2Espt(A_27a),arr(ty_2Esptree_2Espt(A_27a),A_27b))) => ( ! [V3f2_27:$i] : (mem(V3f2_27,arr(ty_2Esptree_2Espt(A_27a),arr(A_27a,arr(ty_2Esptree_2Espt(A_27a),A_27b)))) => ( ! [V4M:$i] : (mem(V4M,ty_2Esptree_2Espt(A_27a)) => ( ! [V5M_27:$i] : (mem(V5M_27,ty_2Esptree_2Espt(A_27a)) => ( ! [V6v:$i] : (mem(V6v,A_27b) => ( ! [V7f:$i] : (mem(V7f,arr(A_27a,A_27b)) => ( ! [V8f1:$i] : (mem(V8f1,arr(ty_2Esptree_2Espt(A_27a),arr(ty_2Esptree_2Espt(A_27a),A_27b))) => ( ! [V9f2:$i] : (mem(V9f2,arr(ty_2Esptree_2Espt(A_27a),arr(A_27a,arr(ty_2Esptree_2Espt(A_27a),A_27b)))) => (((V4M = V5M_27) & (((V5M_27 = c_2Esptree_2ELN(A_27a)) => (V6v = V0v_27)) & (( ! [V10a:$i] : (mem(V10a,A_27a) => ((V5M_27 = ap(c_2Esptree_2ELS(A_27a),V10a)) => (ap(V7f,V10a) = ap(V1f_27,V10a))))) & (( ! [V11a0:$i] : (mem(V11a0,ty_2Esptree_2Espt(A_27a)) => ( ! [V12a1:$i] : (mem(V12a1,ty_2Esptree_2Espt(A_27a)) => ((V5M_27 = ap(ap(c_2Esptree_2EBN(A_27a),V11a0),V12a1)) => (ap(ap(V8f1,V11a0),V12a1) = ap(ap(V2f1_27,V11a0),V12a1))))))) & ( ! [V13a0:$i] : (mem(V13a0,ty_2Esptree_2Espt(A_27a)) => ( ! [V14a1:$i] : (mem(V14a1,A_27a) => ( ! [V15a2:$i] : (mem(V15a2,ty_2Esptree_2Espt(A_27a)) => ((V5M_27 = ap(ap(ap(c_2Esptree_2EBS(A_27a),V13a0),V14a1),V15a2)) => (ap(ap(ap(V9f2,V13a0),V14a1),V15a2) = ap(ap(ap(V3f2_27,V13a0),V14a1),V15a2))))))))))))) => (ap(ap(ap(ap(ap(c_2Esptree_2Espt__CASE(A_27a,A_27b),V4M),V6v),V7f),V8f1),V9f2) = ap(ap(ap(ap(ap(c_2Esptree_2Espt__CASE(A_27a,A_27b),V5M_27),V0v_27),V1f_27),V2f1_27),V3f2_27))))))))))))))))))))))))))).
tff(conj_thm_2Esptree_2Espt__case__eq,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : (mem(V0x,ty_2Esptree_2Espt(A_27a)) => ( ! [V1v:$i] : (mem(V1v,A_27b) => ( ! [V2f:$i] : (mem(V2f,arr(A_27a,A_27b)) => ( ! [V3f1:$i] : (mem(V3f1,arr(ty_2Esptree_2Espt(A_27a),arr(ty_2Esptree_2Espt(A_27a),A_27b))) => ( ! [V4f2:$i] : (mem(V4f2,arr(ty_2Esptree_2Espt(A_27a),arr(A_27a,arr(ty_2Esptree_2Espt(A_27a),A_27b)))) => ( ! [V5v_27:$i] : (mem(V5v_27,A_27b) => ((ap(ap(ap(ap(ap(c_2Esptree_2Espt__CASE(A_27a,A_27b),V0x),V1v),V2f),V3f1),V4f2) = V5v_27) <=> (((V0x = c_2Esptree_2ELN(A_27a)) & (V1v = V5v_27)) | ((? [V6a:$i] : (mem(V6a,A_27a) & ((V0x = ap(c_2Esptree_2ELS(A_27a),V6a)) & (ap(V2f,V6a) = V5v_27)))) | ((? [V7s:$i] : (mem(V7s,ty_2Esptree_2Espt(A_27a)) & (? [V8s0:$i] : (mem(V8s0,ty_2Esptree_2Espt(A_27a)) & ((V0x = ap(ap(c_2Esptree_2EBN(A_27a),V7s),V8s0)) & (ap(ap(V3f1,V7s),V8s0) = V5v_27)))))) | (? [V9s:$i] : (mem(V9s,ty_2Esptree_2Espt(A_27a)) & (? [V10a:$i] : (mem(V10a,A_27a) & (? [V11s0:$i] : (mem(V11s0,ty_2Esptree_2Espt(A_27a)) & ((V0x = ap(ap(ap(c_2Esptree_2EBS(A_27a),V9s),V10a),V11s0)) & (ap(ap(ap(V4f2,V9s),V10a),V11s0) = V5v_27)))))))))))))))))))))))))))).
tff(ax_thm_2Esptree_2Ewf__def,axiom,( ! [A_27a:del]: ((p(ap(c_2Esptree_2Ewf(A_27a),c_2Esptree_2ELN(A_27a))) <=> $true) & (( ! [V0a:$i] : (mem(V0a,A_27a) => (p(ap(c_2Esptree_2Ewf(A_27a),ap(c_2Esptree_2ELS(A_27a),V0a))) <=> $true))) & (( ! [V1t1:$i] : (mem(V1t1,ty_2Esptree_2Espt(A_27a)) => ( ! [V2t2:$i] : (mem(V2t2,ty_2Esptree_2Espt(A_27a)) => (p(ap(c_2Esptree_2Ewf(A_27a),ap(ap(c_2Esptree_2EBN(A_27a),V1t1),V2t2))) <=> (p(ap(c_2Esptree_2Ewf(A_27a),V1t1)) & (p(ap(c_2Esptree_2Ewf(A_27a),V2t2)) & (~~ ((V1t1 = c_2Esptree_2ELN(A_27a)) & (V2t2 = c_2Esptree_2ELN(A_27a))))))))))) & ( ! [V3t1:$i] : (mem(V3t1,ty_2Esptree_2Espt(A_27a)) => ( ! [V4a:$i] : (mem(V4a,A_27a) => ( ! [V5t2:$i] : (mem(V5t2,ty_2Esptree_2Espt(A_27a)) => (p(ap(c_2Esptree_2Ewf(A_27a),ap(ap(ap(c_2Esptree_2EBS(A_27a),V3t1),V4a),V5t2))) <=> (p(ap(c_2Esptree_2Ewf(A_27a),V3t1)) & (p(ap(c_2Esptree_2Ewf(A_27a),V5t2)) & (~~ ((V3t1 = c_2Esptree_2ELN(A_27a)) & (V5t2 = c_2Esptree_2ELN(A_27a)))))))))))))))))).
tff(conj_thm_2Esptree_2Elookup__ind,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Enum_2Enum,arr(ty_2Esptree_2Espt(A_27a),bool))) => ((( ! [V1k:tp__ty_2Enum_2Enum] : p(ap(ap(V0P,inj__ty_2Enum_2Enum(V1k)),c_2Esptree_2ELN(A_27a)))) & (( ! [V2k:tp__ty_2Enum_2Enum] : ( ! [V3a:$i] : (mem(V3a,A_27a) => p(ap(ap(V0P,inj__ty_2Enum_2Enum(V2k)),ap(c_2Esptree_2ELS(A_27a),V3a)))))) & (( ! [V4k:tp__ty_2Enum_2Enum] : ( ! [V5t1:$i] : (mem(V5t1,ty_2Esptree_2Espt(A_27a)) => ( ! [V6t2:$i] : (mem(V6t2,ty_2Esptree_2Espt(A_27a)) => (((~~ (V4k = fo__c_2Enum_2E0)) => p(ap(ap(V0P,ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V4k)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(ap(c_2Ebool_2ECOND(ty_2Esptree_2Espt(A_27a)),ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V4k))),V5t1),V6t2)))) => p(ap(ap(V0P,inj__ty_2Enum_2Enum(V4k)),ap(ap(c_2Esptree_2EBN(A_27a),V5t1),V6t2))))))))) & ( ! [V7k:tp__ty_2Enum_2Enum] : ( ! [V8t1:$i] : (mem(V8t1,ty_2Esptree_2Espt(A_27a)) => ( ! [V9a:$i] : (mem(V9a,A_27a) => ( ! [V10t2:$i] : (mem(V10t2,ty_2Esptree_2Espt(A_27a)) => (((~~ (V7k = fo__c_2Enum_2E0)) => p(ap(ap(V0P,ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V7k)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(ap(c_2Ebool_2ECOND(ty_2Esptree_2Espt(A_27a)),ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V7k))),V8t1),V10t2)))) => p(ap(ap(V0P,inj__ty_2Enum_2Enum(V7k)),ap(ap(ap(c_2Esptree_2EBS(A_27a),V8t1),V9a),V10t2)))))))))))))) => ( ! [V11v:tp__ty_2Enum_2Enum] : ( ! [V12v1:$i] : (mem(V12v1,ty_2Esptree_2Espt(A_27a)) => p(ap(ap(V0P,inj__ty_2Enum_2Enum(V11v)),V12v1))))))))))).
tff(conj_thm_2Esptree_2Elookup__def,lemma,(( ! [A_27a:del]: (( ! [V0k:tp__ty_2Enum_2Enum] : (ap(ap(c_2Esptree_2Elookup(A_27a),inj__ty_2Enum_2Enum(V0k)),c_2Esptree_2ELN(A_27a)) = c_2Eoption_2ENONE(A_27a))) & (( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2a:$i] : (mem(V2a,A_27a) => (ap(ap(c_2Esptree_2Elookup(A_27a),inj__ty_2Enum_2Enum(V1k)),ap(c_2Esptree_2ELS(A_27a),V2a)) = 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(fo__c_2Enum_2E0))),ap(c_2Eoption_2ESOME(A_27a),V2a)),c_2Eoption_2ENONE(A_27a)))))) & (( ! [V3t2:$i] : (mem(V3t2,ty_2Esptree_2Espt(A_27a)) => ( ! [V4t1:$i] : (mem(V4t1,ty_2Esptree_2Espt(A_27a)) => ( ! [V5k:tp__ty_2Enum_2Enum] : (ap(ap(c_2Esptree_2Elookup(A_27a),inj__ty_2Enum_2Enum(V5k)),ap(ap(c_2Esptree_2EBN(A_27a),V4t1),V3t2)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eoption_2Eoption(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V5k)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),c_2Eoption_2ENONE(A_27a)),ap(ap(c_2Esptree_2Elookup(A_27a),ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V5k)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(ap(c_2Ebool_2ECOND(ty_2Esptree_2Espt(A_27a)),ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V5k))),V4t1),V3t2))))))))) & ( ! [V6t2:$i] : (mem(V6t2,ty_2Esptree_2Espt(A_27a)) => ( ! [V7t1:$i] : (mem(V7t1,ty_2Esptree_2Espt(A_27a)) => ( ! [V8k:tp__ty_2Enum_2Enum] : ( ! [V9a:$i] : (mem(V9a,A_27a) => (ap(ap(c_2Esptree_2Elookup(A_27a),inj__ty_2Enum_2Enum(V8k)),ap(ap(ap(c_2Esptree_2EBS(A_27a),V7t1),V9a),V6t2)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eoption_2Eoption(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V8k)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(c_2Eoption_2ESOME(A_27a),V9a)),ap(ap(c_2Esptree_2Elookup(A_27a),ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V8k)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(ap(ap(c_2Ebool_2ECOND(ty_2Esptree_2Espt(A_27a)),ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V8k))),V7t1),V6t2))))))))))))))))).
tff(conj_thm_2Esptree_2Einsert__ind,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Enum_2Enum,arr(A_27a,arr(ty_2Esptree_2Espt(A_27a),bool)))) => ((( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2a:$i] : (mem(V2a,A_27a) => (((((~~ (V1k = fo__c_2Enum_2E0)) & p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V1k)))) => p(ap(ap(ap(V0P,ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V1k)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),V2a),c_2Esptree_2ELN(A_27a)))) & (((~~ (V1k = fo__c_2Enum_2E0)) & (~~ p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V1k))))) => p(ap(ap(ap(V0P,ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V1k)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),V2a),c_2Esptree_2ELN(A_27a))))) => p(ap(ap(ap(V0P,inj__ty_2Enum_2Enum(V1k)),V2a),c_2Esptree_2ELN(A_27a))))))) & (( ! [V3k:tp__ty_2Enum_2Enum] : ( ! [V4a:$i] : (mem(V4a,A_27a) => ( ! [V5a_27:$i] : (mem(V5a_27,A_27a) => (((((~~ (V3k = fo__c_2Enum_2E0)) & p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V3k)))) => p(ap(ap(ap(V0P,ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V3k)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),V4a),c_2Esptree_2ELN(A_27a)))) & (((~~ (V3k = fo__c_2Enum_2E0)) & (~~ p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V3k))))) => p(ap(ap(ap(V0P,ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V3k)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),V4a),c_2Esptree_2ELN(A_27a))))) => p(ap(ap(ap(V0P,inj__ty_2Enum_2Enum(V3k)),V4a),ap(c_2Esptree_2ELS(A_27a),V5a_27))))))))) & (( ! [V6k:tp__ty_2Enum_2Enum] : ( ! [V7a:$i] : (mem(V7a,A_27a) => ( ! [V8t1:$i] : (mem(V8t1,ty_2Esptree_2Espt(A_27a)) => ( ! [V9t2:$i] : (mem(V9t2,ty_2Esptree_2Espt(A_27a)) => (((((~~ (V6k = fo__c_2Enum_2E0)) & p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V6k)))) => p(ap(ap(ap(V0P,ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V6k)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),V7a),V8t1))) & (((~~ (V6k = fo__c_2Enum_2E0)) & (~~ p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V6k))))) => p(ap(ap(ap(V0P,ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V6k)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),V7a),V9t2)))) => p(ap(ap(ap(V0P,inj__ty_2Enum_2Enum(V6k)),V7a),ap(ap(c_2Esptree_2EBN(A_27a),V8t1),V9t2))))))))))) & ( ! [V10k:tp__ty_2Enum_2Enum] : ( ! [V11a:$i] : (mem(V11a,A_27a) => ( ! [V12t1:$i] : (mem(V12t1,ty_2Esptree_2Espt(A_27a)) => ( ! [V13a_27:$i] : (mem(V13a_27,A_27a) => ( ! [V14t2:$i] : (mem(V14t2,ty_2Esptree_2Espt(A_27a)) => (((((~~ (V10k = fo__c_2Enum_2E0)) & p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V10k)))) => p(ap(ap(ap(V0P,ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V10k)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),V11a),V12t1))) & (((~~ (V10k = fo__c_2Enum_2E0)) & (~~ p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V10k))))) => p(ap(ap(ap(V0P,ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V10k)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),V11a),V14t2)))) => p(ap(ap(ap(V0P,inj__ty_2Enum_2Enum(V10k)),V11a),ap(ap(ap(c_2Esptree_2EBS(A_27a),V12t1),V13a_27),V14t2)))))))))))))))) => ( ! [V15v:tp__ty_2Enum_2Enum] : ( ! [V16v1:$i] : (mem(V16v1,A_27a) => ( ! [V17v2:$i] : (mem(V17v2,ty_2Esptree_2Espt(A_27a)) => p(ap(ap(ap(V0P,inj__ty_2Enum_2Enum(V15v)),V16v1),V17v2))))))))))))).
tff(conj_thm_2Esptree_2Einsert__def,lemma,(( ! [A_27a:del]: (( ! [V0k:tp__ty_2Enum_2Enum] : ( ! [V1a:$i] : (mem(V1a,A_27a) => (ap(ap(ap(c_2Esptree_2Einsert(A_27a),inj__ty_2Enum_2Enum(V0k)),V1a),c_2Esptree_2ELN(A_27a)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Esptree_2Espt(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V0k)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(c_2Esptree_2ELS(A_27a),V1a)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Esptree_2Espt(A_27a)),ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V0k))),ap(ap(c_2Esptree_2EBN(A_27a),ap(ap(ap(c_2Esptree_2Einsert(A_27a),ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0k)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),V1a),c_2Esptree_2ELN(A_27a))),c_2Esptree_2ELN(A_27a))),ap(ap(c_2Esptree_2EBN(A_27a),c_2Esptree_2ELN(A_27a)),ap(ap(ap(c_2Esptree_2Einsert(A_27a),ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0k)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),V1a),c_2Esptree_2ELN(A_27a))))))))) & (( ! [V2k:tp__ty_2Enum_2Enum] : ( ! [V3a_27:$i] : (mem(V3a_27,A_27a) => ( ! [V4a:$i] : (mem(V4a,A_27a) => (ap(ap(ap(c_2Esptree_2Einsert(A_27a),inj__ty_2Enum_2Enum(V2k)),V4a),ap(c_2Esptree_2ELS(A_27a),V3a_27)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Esptree_2Espt(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V2k)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(c_2Esptree_2ELS(A_27a),V4a)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Esptree_2Espt(A_27a)),ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V2k))),ap(ap(ap(c_2Esptree_2EBS(A_27a),ap(ap(ap(c_2Esptree_2Einsert(A_27a),ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V2k)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),V4a),c_2Esptree_2ELN(A_27a))),V3a_27),c_2Esptree_2ELN(A_27a))),ap(ap(ap(c_2Esptree_2EBS(A_27a),c_2Esptree_2ELN(A_27a)),V3a_27),ap(ap(ap(c_2Esptree_2Einsert(A_27a),ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V2k)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),V4a),c_2Esptree_2ELN(A_27a))))))))))) & (( ! [V5t2:$i] : (mem(V5t2,ty_2Esptree_2Espt(A_27a)) => ( ! [V6t1:$i] : (mem(V6t1,ty_2Esptree_2Espt(A_27a)) => ( ! [V7k:tp__ty_2Enum_2Enum] : ( ! [V8a:$i] : (mem(V8a,A_27a) => (ap(ap(ap(c_2Esptree_2Einsert(A_27a),inj__ty_2Enum_2Enum(V7k)),V8a),ap(ap(c_2Esptree_2EBN(A_27a),V6t1),V5t2)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Esptree_2Espt(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V7k)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(ap(ap(c_2Esptree_2EBS(A_27a),V6t1),V8a),V5t2)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Esptree_2Espt(A_27a)),ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V7k))),ap(ap(c_2Esptree_2EBN(A_27a),ap(ap(ap(c_2Esptree_2Einsert(A_27a),ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V7k)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),V8a),V6t1)),V5t2)),ap(ap(c_2Esptree_2EBN(A_27a),V6t1),ap(ap(ap(c_2Esptree_2Einsert(A_27a),ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V7k)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),V8a),V5t2)))))))))))) & ( ! [V9t2:$i] : (mem(V9t2,ty_2Esptree_2Espt(A_27a)) => ( ! [V10t1:$i] : (mem(V10t1,ty_2Esptree_2Espt(A_27a)) => ( ! [V11k:tp__ty_2Enum_2Enum] : ( ! [V12a_27:$i] : (mem(V12a_27,A_27a) => ( ! [V13a:$i] : (mem(V13a,A_27a) => (ap(ap(ap(c_2Esptree_2Einsert(A_27a),inj__ty_2Enum_2Enum(V11k)),V13a),ap(ap(ap(c_2Esptree_2EBS(A_27a),V10t1),V12a_27),V9t2)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Esptree_2Espt(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V11k)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(ap(ap(c_2Esptree_2EBS(A_27a),V10t1),V13a),V9t2)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Esptree_2Espt(A_27a)),ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V11k))),ap(ap(ap(c_2Esptree_2EBS(A_27a),ap(ap(ap(c_2Esptree_2Einsert(A_27a),ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V11k)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),V13a),V10t1)),V12a_27),V9t2)),ap(ap(ap(c_2Esptree_2EBS(A_27a),V10t1),V12a_27),ap(ap(ap(c_2Esptree_2Einsert(A_27a),ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V11k)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),V13a),V9t2)))))))))))))))))))).
tff(conj_thm_2Esptree_2Emk__BN__ind,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Esptree_2Espt(A_27a),arr(ty_2Esptree_2Espt(A_27a),bool))) => ((p(ap(ap(V0P,c_2Esptree_2ELN(A_27a)),c_2Esptree_2ELN(A_27a))) & (( ! [V1v14:$i] : (mem(V1v14,A_27a) => p(ap(ap(V0P,c_2Esptree_2ELN(A_27a)),ap(c_2Esptree_2ELS(A_27a),V1v14))))) & (( ! [V2v15:$i] : (mem(V2v15,ty_2Esptree_2Espt(A_27a)) => ( ! [V3v16:$i] : (mem(V3v16,ty_2Esptree_2Espt(A_27a)) => p(ap(ap(V0P,c_2Esptree_2ELN(A_27a)),ap(ap(c_2Esptree_2EBN(A_27a),V2v15),V3v16))))))) & (( ! [V4v17:$i] : (mem(V4v17,ty_2Esptree_2Espt(A_27a)) => ( ! [V5v18:$i] : (mem(V5v18,A_27a) => ( ! [V6v19:$i] : (mem(V6v19,ty_2Esptree_2Espt(A_27a)) => p(ap(ap(V0P,c_2Esptree_2ELN(A_27a)),ap(ap(ap(c_2Esptree_2EBS(A_27a),V4v17),V5v18),V6v19))))))))) & (( ! [V7v2:$i] : (mem(V7v2,A_27a) => ( ! [V8t2:$i] : (mem(V8t2,ty_2Esptree_2Espt(A_27a)) => p(ap(ap(V0P,ap(c_2Esptree_2ELS(A_27a),V7v2)),V8t2)))))) & (( ! [V9v3:$i] : (mem(V9v3,ty_2Esptree_2Espt(A_27a)) => ( ! [V10v4:$i] : (mem(V10v4,ty_2Esptree_2Espt(A_27a)) => ( ! [V11t2:$i] : (mem(V11t2,ty_2Esptree_2Espt(A_27a)) => p(ap(ap(V0P,ap(ap(c_2Esptree_2EBN(A_27a),V9v3),V10v4)),V11t2)))))))) & ( ! [V12v5:$i] : (mem(V12v5,ty_2Esptree_2Espt(A_27a)) => ( ! [V13v6:$i] : (mem(V13v6,A_27a) => ( ! [V14v7:$i] : (mem(V14v7,ty_2Esptree_2Espt(A_27a)) => ( ! [V15t2:$i] : (mem(V15t2,ty_2Esptree_2Espt(A_27a)) => p(ap(ap(V0P,ap(ap(ap(c_2Esptree_2EBS(A_27a),V12v5),V13v6),V14v7)),V15t2)))))))))))))))) => ( ! [V16v:$i] : (mem(V16v,ty_2Esptree_2Espt(A_27a)) => ( ! [V17v1:$i] : (mem(V17v1,ty_2Esptree_2Espt(A_27a)) => p(ap(ap(V0P,V16v),V17v1)))))))))))).
tff(conj_thm_2Esptree_2Emk__BN__def,lemma,(( ! [A_27a:del]: ( ! [V0v14:$i] : (mem(V0v14,A_27a) => ( ! [V1v15:$i] : (mem(V1v15,ty_2Esptree_2Espt(A_27a)) => ( ! [V2v16:$i] : (mem(V2v16,ty_2Esptree_2Espt(A_27a)) => ( ! [V3v17:$i] : (mem(V3v17,ty_2Esptree_2Espt(A_27a)) => ( ! [V4v18:$i] : (mem(V4v18,A_27a) => ( ! [V5v19:$i] : (mem(V5v19,ty_2Esptree_2Espt(A_27a)) => ( ! [V6v2:$i] : (mem(V6v2,A_27a) => ( ! [V7t2:$i] : (mem(V7t2,ty_2Esptree_2Espt(A_27a)) => ( ! [V8v3:$i] : (mem(V8v3,ty_2Esptree_2Espt(A_27a)) => ( ! [V9v4:$i] : (mem(V9v4,ty_2Esptree_2Espt(A_27a)) => ( ! [V10v5:$i] : (mem(V10v5,ty_2Esptree_2Espt(A_27a)) => ( ! [V11v6:$i] : (mem(V11v6,A_27a) => ( ! [V12v7:$i] : (mem(V12v7,ty_2Esptree_2Espt(A_27a)) => ((ap(ap(c_2Esptree_2Emk__BN(A_27a),c_2Esptree_2ELN(A_27a)),c_2Esptree_2ELN(A_27a)) = c_2Esptree_2ELN(A_27a)) & ((ap(ap(c_2Esptree_2Emk__BN(A_27a),c_2Esptree_2ELN(A_27a)),ap(c_2Esptree_2ELS(A_27a),V0v14)) = ap(ap(c_2Esptree_2EBN(A_27a),c_2Esptree_2ELN(A_27a)),ap(c_2Esptree_2ELS(A_27a),V0v14))) & ((ap(ap(c_2Esptree_2Emk__BN(A_27a),c_2Esptree_2ELN(A_27a)),ap(ap(c_2Esptree_2EBN(A_27a),V1v15),V2v16)) = ap(ap(c_2Esptree_2EBN(A_27a),c_2Esptree_2ELN(A_27a)),ap(ap(c_2Esptree_2EBN(A_27a),V1v15),V2v16))) & ((ap(ap(c_2Esptree_2Emk__BN(A_27a),c_2Esptree_2ELN(A_27a)),ap(ap(ap(c_2Esptree_2EBS(A_27a),V3v17),V4v18),V5v19)) = ap(ap(c_2Esptree_2EBN(A_27a),c_2Esptree_2ELN(A_27a)),ap(ap(ap(c_2Esptree_2EBS(A_27a),V3v17),V4v18),V5v19))) & ((ap(ap(c_2Esptree_2Emk__BN(A_27a),ap(c_2Esptree_2ELS(A_27a),V6v2)),V7t2) = ap(ap(c_2Esptree_2EBN(A_27a),ap(c_2Esptree_2ELS(A_27a),V6v2)),V7t2)) & ((ap(ap(c_2Esptree_2Emk__BN(A_27a),ap(ap(c_2Esptree_2EBN(A_27a),V8v3),V9v4)),V7t2) = ap(ap(c_2Esptree_2EBN(A_27a),ap(ap(c_2Esptree_2EBN(A_27a),V8v3),V9v4)),V7t2)) & (ap(ap(c_2Esptree_2Emk__BN(A_27a),ap(ap(ap(c_2Esptree_2EBS(A_27a),V10v5),V11v6),V12v7)),V7t2) = ap(ap(c_2Esptree_2EBN(A_27a),ap(ap(ap(c_2Esptree_2EBS(A_27a),V10v5),V11v6),V12v7)),V7t2))))))))))))))))))))))))))))))))))))).
tff(conj_thm_2Esptree_2Emk__BS__ind,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Esptree_2Espt(A_27a),arr(A_27a,arr(ty_2Esptree_2Espt(A_27a),bool)))) => ((( ! [V1x:$i] : (mem(V1x,A_27a) => p(ap(ap(ap(V0P,c_2Esptree_2ELN(A_27a)),V1x),c_2Esptree_2ELN(A_27a))))) & (( ! [V2v16:$i] : (mem(V2v16,A_27a) => ( ! [V3x:$i] : (mem(V3x,A_27a) => p(ap(ap(ap(V0P,ap(c_2Esptree_2ELS(A_27a),V2v16)),V3x),c_2Esptree_2ELN(A_27a))))))) & (( ! [V4v17:$i] : (mem(V4v17,ty_2Esptree_2Espt(A_27a)) => ( ! [V5v18:$i] : (mem(V5v18,ty_2Esptree_2Espt(A_27a)) => ( ! [V6x:$i] : (mem(V6x,A_27a) => p(ap(ap(ap(V0P,ap(ap(c_2Esptree_2EBN(A_27a),V4v17),V5v18)),V6x),c_2Esptree_2ELN(A_27a))))))))) & (( ! [V7v19:$i] : (mem(V7v19,ty_2Esptree_2Espt(A_27a)) => ( ! [V8v20:$i] : (mem(V8v20,A_27a) => ( ! [V9v21:$i] : (mem(V9v21,ty_2Esptree_2Espt(A_27a)) => ( ! [V10x:$i] : (mem(V10x,A_27a) => p(ap(ap(ap(V0P,ap(ap(ap(c_2Esptree_2EBS(A_27a),V7v19),V8v20),V9v21)),V10x),c_2Esptree_2ELN(A_27a))))))))))) & (( ! [V11t1:$i] : (mem(V11t1,ty_2Esptree_2Espt(A_27a)) => ( ! [V12x:$i] : (mem(V12x,A_27a) => ( ! [V13v4:$i] : (mem(V13v4,A_27a) => p(ap(ap(ap(V0P,V11t1),V12x),ap(c_2Esptree_2ELS(A_27a),V13v4))))))))) & (( ! [V14t1:$i] : (mem(V14t1,ty_2Esptree_2Espt(A_27a)) => ( ! [V15x:$i] : (mem(V15x,A_27a) => ( ! [V16v5:$i] : (mem(V16v5,ty_2Esptree_2Espt(A_27a)) => ( ! [V17v6:$i] : (mem(V17v6,ty_2Esptree_2Espt(A_27a)) => p(ap(ap(ap(V0P,V14t1),V15x),ap(ap(c_2Esptree_2EBN(A_27a),V16v5),V17v6))))))))))) & ( ! [V18t1:$i] : (mem(V18t1,ty_2Esptree_2Espt(A_27a)) => ( ! [V19x:$i] : (mem(V19x,A_27a) => ( ! [V20v7:$i] : (mem(V20v7,ty_2Esptree_2Espt(A_27a)) => ( ! [V21v8:$i] : (mem(V21v8,A_27a) => ( ! [V22v9:$i] : (mem(V22v9,ty_2Esptree_2Espt(A_27a)) => p(ap(ap(ap(V0P,V18t1),V19x),ap(ap(ap(c_2Esptree_2EBS(A_27a),V20v7),V21v8),V22v9))))))))))))))))))) => ( ! [V23v:$i] : (mem(V23v,ty_2Esptree_2Espt(A_27a)) => ( ! [V24v1:$i] : (mem(V24v1,A_27a) => ( ! [V25v2:$i] : (mem(V25v2,ty_2Esptree_2Espt(A_27a)) => p(ap(ap(ap(V0P,V23v),V24v1),V25v2)))))))))))))).
tff(conj_thm_2Esptree_2Emk__BS__def,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1v16:$i] : (mem(V1v16,A_27a) => ( ! [V2v17:$i] : (mem(V2v17,ty_2Esptree_2Espt(A_27a)) => ( ! [V3v18:$i] : (mem(V3v18,ty_2Esptree_2Espt(A_27a)) => ( ! [V4v19:$i] : (mem(V4v19,ty_2Esptree_2Espt(A_27a)) => ( ! [V5v20:$i] : (mem(V5v20,A_27a) => ( ! [V6v21:$i] : (mem(V6v21,ty_2Esptree_2Espt(A_27a)) => ( ! [V7t1:$i] : (mem(V7t1,ty_2Esptree_2Espt(A_27a)) => ( ! [V8v4:$i] : (mem(V8v4,A_27a) => ( ! [V9v5:$i] : (mem(V9v5,ty_2Esptree_2Espt(A_27a)) => ( ! [V10v6:$i] : (mem(V10v6,ty_2Esptree_2Espt(A_27a)) => ( ! [V11v7:$i] : (mem(V11v7,ty_2Esptree_2Espt(A_27a)) => ( ! [V12v8:$i] : (mem(V12v8,A_27a) => ( ! [V13v9:$i] : (mem(V13v9,ty_2Esptree_2Espt(A_27a)) => ((ap(ap(ap(c_2Esptree_2Emk__BS(A_27a),c_2Esptree_2ELN(A_27a)),V0x),c_2Esptree_2ELN(A_27a)) = ap(c_2Esptree_2ELS(A_27a),V0x)) & ((ap(ap(ap(c_2Esptree_2Emk__BS(A_27a),ap(c_2Esptree_2ELS(A_27a),V1v16)),V0x),c_2Esptree_2ELN(A_27a)) = ap(ap(ap(c_2Esptree_2EBS(A_27a),ap(c_2Esptree_2ELS(A_27a),V1v16)),V0x),c_2Esptree_2ELN(A_27a))) & ((ap(ap(ap(c_2Esptree_2Emk__BS(A_27a),ap(ap(c_2Esptree_2EBN(A_27a),V2v17),V3v18)),V0x),c_2Esptree_2ELN(A_27a)) = ap(ap(ap(c_2Esptree_2EBS(A_27a),ap(ap(c_2Esptree_2EBN(A_27a),V2v17),V3v18)),V0x),c_2Esptree_2ELN(A_27a))) & ((ap(ap(ap(c_2Esptree_2Emk__BS(A_27a),ap(ap(ap(c_2Esptree_2EBS(A_27a),V4v19),V5v20),V6v21)),V0x),c_2Esptree_2ELN(A_27a)) = ap(ap(ap(c_2Esptree_2EBS(A_27a),ap(ap(ap(c_2Esptree_2EBS(A_27a),V4v19),V5v20),V6v21)),V0x),c_2Esptree_2ELN(A_27a))) & ((ap(ap(ap(c_2Esptree_2Emk__BS(A_27a),V7t1),V0x),ap(c_2Esptree_2ELS(A_27a),V8v4)) = ap(ap(ap(c_2Esptree_2EBS(A_27a),V7t1),V0x),ap(c_2Esptree_2ELS(A_27a),V8v4))) & ((ap(ap(ap(c_2Esptree_2Emk__BS(A_27a),V7t1),V0x),ap(ap(c_2Esptree_2EBN(A_27a),V9v5),V10v6)) = ap(ap(ap(c_2Esptree_2EBS(A_27a),V7t1),V0x),ap(ap(c_2Esptree_2EBN(A_27a),V9v5),V10v6))) & (ap(ap(ap(c_2Esptree_2Emk__BS(A_27a),V7t1),V0x),ap(ap(ap(c_2Esptree_2EBS(A_27a),V11v7),V12v8),V13v9)) = ap(ap(ap(c_2Esptree_2EBS(A_27a),V7t1),V0x),ap(ap(ap(c_2Esptree_2EBS(A_27a),V11v7),V12v8),V13v9)))))))))))))))))))))))))))))))))))))))).
tff(ax_thm_2Esptree_2Edelete__def,axiom,( ! [A_27a:del]: (( ! [V0k:tp__ty_2Enum_2Enum] : (ap(ap(c_2Esptree_2Edelete(A_27a),inj__ty_2Enum_2Enum(V0k)),c_2Esptree_2ELN(A_27a)) = c_2Esptree_2ELN(A_27a))) & (( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2a:$i] : (mem(V2a,A_27a) => (ap(ap(c_2Esptree_2Edelete(A_27a),inj__ty_2Enum_2Enum(V1k)),ap(c_2Esptree_2ELS(A_27a),V2a)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Esptree_2Espt(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V1k)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),c_2Esptree_2ELN(A_27a)),ap(c_2Esptree_2ELS(A_27a),V2a)))))) & (( ! [V3k:tp__ty_2Enum_2Enum] : ( ! [V4t1:$i] : (mem(V4t1,ty_2Esptree_2Espt(A_27a)) => ( ! [V5t2:$i] : (mem(V5t2,ty_2Esptree_2Espt(A_27a)) => (ap(ap(c_2Esptree_2Edelete(A_27a),inj__ty_2Enum_2Enum(V3k)),ap(ap(c_2Esptree_2EBN(A_27a),V4t1),V5t2)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Esptree_2Espt(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V3k)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(ap(c_2Esptree_2EBN(A_27a),V4t1),V5t2)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Esptree_2Espt(A_27a)),ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V3k))),ap(ap(c_2Esptree_2Emk__BN(A_27a),ap(ap(c_2Esptree_2Edelete(A_27a),ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V3k)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),V4t1)),V5t2)),ap(ap(c_2Esptree_2Emk__BN(A_27a),V4t1),ap(ap(c_2Esptree_2Edelete(A_27a),ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V3k)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),V5t2)))))))))) & ( ! [V6k:tp__ty_2Enum_2Enum] : ( ! [V7t1:$i] : (mem(V7t1,ty_2Esptree_2Espt(A_27a)) => ( ! [V8a:$i] : (mem(V8a,A_27a) => ( ! [V9t2:$i] : (mem(V9t2,ty_2Esptree_2Espt(A_27a)) => (ap(ap(c_2Esptree_2Edelete(A_27a),inj__ty_2Enum_2Enum(V6k)),ap(ap(ap(c_2Esptree_2EBS(A_27a),V7t1),V8a),V9t2)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Esptree_2Espt(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V6k)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(ap(c_2Esptree_2EBN(A_27a),V7t1),V9t2)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Esptree_2Espt(A_27a)),ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V6k))),ap(ap(ap(c_2Esptree_2Emk__BS(A_27a),ap(ap(c_2Esptree_2Edelete(A_27a),ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V6k)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),V7t1)),V8a),V9t2)),ap(ap(ap(c_2Esptree_2Emk__BS(A_27a),V7t1),V8a),ap(ap(c_2Esptree_2Edelete(A_27a),ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V6k)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),V9t2))))))))))))))))).
tff(ax_thm_2Esptree_2EfromList__def,axiom,( ! [A_27a:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => (ap(c_2Esptree_2EfromList(A_27a),V0l) = ap(c_2Epair_2ESND(ty_2Enum_2Enum,ty_2Esptree_2Espt(A_27a)),ap(ap(ap(c_2Elist_2EFOLDL(A_27a,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Esptree_2Espt(A_27a))),ap(c_2Epair_2EUNCURRY(ty_2Enum_2Enum,ty_2Esptree_2Espt(A_27a),arr(A_27a,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Esptree_2Espt(A_27a)))),f2348(A_27a))),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,ty_2Esptree_2Espt(A_27a)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),c_2Esptree_2ELN(A_27a))),V0l))))))).
tff(ax_thm_2Esptree_2Esize__def,axiom,( ! [A_27a:del]: ((surj__ty_2Enum_2Enum(ap(c_2Esptree_2Esize(A_27a),c_2Esptree_2ELN(A_27a))) = fo__c_2Enum_2E0) & (( ! [V0a:$i] : (mem(V0a,A_27a) => (surj__ty_2Enum_2Enum(ap(c_2Esptree_2Esize(A_27a),ap(c_2Esptree_2ELS(A_27a),V0a))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) & (( ! [V1t1:$i] : (mem(V1t1,ty_2Esptree_2Espt(A_27a)) => ( ! [V2t2:$i] : (mem(V2t2,ty_2Esptree_2Espt(A_27a)) => (surj__ty_2Enum_2Enum(ap(c_2Esptree_2Esize(A_27a),ap(ap(c_2Esptree_2EBN(A_27a),V1t1),V2t2))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(c_2Esptree_2Esize(A_27a),V1t1)),ap(c_2Esptree_2Esize(A_27a),V2t2)))))))) & ( ! [V3t1:$i] : (mem(V3t1,ty_2Esptree_2Espt(A_27a)) => ( ! [V4a:$i] : (mem(V4a,A_27a) => ( ! [V5t2:$i] : (mem(V5t2,ty_2Esptree_2Espt(A_27a)) => (surj__ty_2Enum_2Enum(ap(c_2Esptree_2Esize(A_27a),ap(ap(ap(c_2Esptree_2EBS(A_27a),V3t1),V4a),V5t2))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2B,ap(c_2Esptree_2Esize(A_27a),V3t1)),ap(c_2Esptree_2Esize(A_27a),V5t2))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))))))))))).
tff(conj_thm_2Esptree_2Einsert__notEmpty,lemma,(( ! [A_27a:del]: ( ! [V0k:tp__ty_2Enum_2Enum] : ( ! [V1a:$i] : (mem(V1a,A_27a) => ( ! [V2t:$i] : (mem(V2t,ty_2Esptree_2Espt(A_27a)) => (~~ (ap(ap(ap(c_2Esptree_2Einsert(A_27a),inj__ty_2Enum_2Enum(V0k)),V1a),V2t) = c_2Esptree_2ELN(A_27a))))))))))).
tff(conj_thm_2Esptree_2Ewf__insert,lemma,(( ! [A_27a:del]: ( ! [V0k:tp__ty_2Enum_2Enum] : ( ! [V1a:$i] : (mem(V1a,A_27a) => ( ! [V2t:$i] : (mem(V2t,ty_2Esptree_2Espt(A_27a)) => (p(ap(c_2Esptree_2Ewf(A_27a),V2t)) => p(ap(c_2Esptree_2Ewf(A_27a),ap(ap(ap(c_2Esptree_2Einsert(A_27a),inj__ty_2Enum_2Enum(V0k)),V1a),V2t)))))))))))).
tff(conj_thm_2Esptree_2Ewf__delete,lemma,(( ! [A_27a:del]: ( ! [V0t:$i] : (mem(V0t,ty_2Esptree_2Espt(A_27a)) => ( ! [V1k:tp__ty_2Enum_2Enum] : (p(ap(c_2Esptree_2Ewf(A_27a),V0t)) => p(ap(c_2Esptree_2Ewf(A_27a),ap(ap(c_2Esptree_2Edelete(A_27a),inj__ty_2Enum_2Enum(V1k)),V0t)))))))))).
tff(conj_thm_2Esptree_2Elookup__insert1,lemma,(( ! [A_27a:del]: ( ! [V0k:tp__ty_2Enum_2Enum] : ( ! [V1a:$i] : (mem(V1a,A_27a) => ( ! [V2t:$i] : (mem(V2t,ty_2Esptree_2Espt(A_27a)) => (ap(ap(c_2Esptree_2Elookup(A_27a),inj__ty_2Enum_2Enum(V0k)),ap(ap(ap(c_2Esptree_2Einsert(A_27a),inj__ty_2Enum_2Enum(V0k)),V1a),V2t)) = ap(c_2Eoption_2ESOME(A_27a),V1a)))))))))).
tff(conj_thm_2Esptree_2Elookup__insert,lemma,(( ! [A_27a:del]: ( ! [V0k2:tp__ty_2Enum_2Enum] : ( ! [V1v:$i] : (mem(V1v,A_27a) => ( ! [V2t:$i] : (mem(V2t,ty_2Esptree_2Espt(A_27a)) => ( ! [V3k1:tp__ty_2Enum_2Enum] : (ap(ap(c_2Esptree_2Elookup(A_27a),inj__ty_2Enum_2Enum(V3k1)),ap(ap(ap(c_2Esptree_2Einsert(A_27a),inj__ty_2Enum_2Enum(V0k2)),V1v),V2t)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eoption_2Eoption(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V3k1)),inj__ty_2Enum_2Enum(V0k2))),ap(c_2Eoption_2ESOME(A_27a),V1v)),ap(ap(c_2Esptree_2Elookup(A_27a),inj__ty_2Enum_2Enum(V3k1)),V2t)))))))))))).
tff(ax_thm_2Esptree_2Eunion__def,axiom,( ! [A_27a:del]: (( ! [V0t:$i] : (mem(V0t,ty_2Esptree_2Espt(A_27a)) => (ap(ap(c_2Esptree_2Eunion(A_27a),c_2Esptree_2ELN(A_27a)),V0t) = V0t))) & (( ! [V1a:$i] : (mem(V1a,A_27a) => ( ! [V2t:$i] : (mem(V2t,ty_2Esptree_2Espt(A_27a)) => (ap(ap(c_2Esptree_2Eunion(A_27a),ap(c_2Esptree_2ELS(A_27a),V1a)),V2t) = ap(ap(ap(ap(ap(c_2Esptree_2Espt__CASE(A_27a,ty_2Esptree_2Espt(A_27a)),V2t),ap(c_2Esptree_2ELS(A_27a),V1a)),k(A_27a,ap(c_2Esptree_2ELS(A_27a),V1a))),f2350(A_27a,V1a)),f2352(A_27a,V1a))))))) & (( ! [V9t1:$i] : (mem(V9t1,ty_2Esptree_2Espt(A_27a)) => ( ! [V10t2:$i] : (mem(V10t2,ty_2Esptree_2Espt(A_27a)) => ( ! [V11t:$i] : (mem(V11t,ty_2Esptree_2Espt(A_27a)) => (ap(ap(c_2Esptree_2Eunion(A_27a),ap(ap(c_2Esptree_2EBN(A_27a),V9t1),V10t2)),V11t) = ap(ap(ap(ap(ap(c_2Esptree_2Espt__CASE(A_27a,ty_2Esptree_2Espt(A_27a)),V11t),ap(ap(c_2Esptree_2EBN(A_27a),V9t1),V10t2)),f2353(A_27a,V9t1,V10t2)),f2355(A_27a,V9t1,V10t2)),f2358(A_27a,V9t1,V10t2))))))))) & ( ! [V18t1:$i] : (mem(V18t1,ty_2Esptree_2Espt(A_27a)) => ( ! [V19a:$i] : (mem(V19a,A_27a) => ( ! [V20t2:$i] : (mem(V20t2,ty_2Esptree_2Espt(A_27a)) => ( ! [V21t:$i] : (mem(V21t,ty_2Esptree_2Espt(A_27a)) => (ap(ap(c_2Esptree_2Eunion(A_27a),ap(ap(ap(c_2Esptree_2EBS(A_27a),V18t1),V19a),V20t2)),V21t) = ap(ap(ap(ap(ap(c_2Esptree_2Espt__CASE(A_27a,ty_2Esptree_2Espt(A_27a)),V21t),ap(ap(ap(c_2Esptree_2EBS(A_27a),V18t1),V19a),V20t2)),k(A_27a,ap(ap(ap(c_2Esptree_2EBS(A_27a),V18t1),V19a),V20t2))),f2360(A_27a,V19a,V18t1,V20t2)),f2362(A_27a,V19a,V18t1,V20t2)))))))))))))))).
tff(conj_thm_2Esptree_2EisEmpty__union,lemma,(( ! [A_27a:del]: ( ! [V0m1:$i] : (mem(V0m1,ty_2Esptree_2Espt(A_27a)) => ( ! [V1m2:$i] : (mem(V1m2,ty_2Esptree_2Espt(A_27a)) => ((ap(ap(c_2Esptree_2Eunion(A_27a),V0m1),V1m2) = c_2Esptree_2ELN(A_27a)) <=> ((V0m1 = c_2Esptree_2ELN(A_27a)) & (V1m2 = c_2Esptree_2ELN(A_27a))))))))))).
tff(conj_thm_2Esptree_2Ewf__union,lemma,(( ! [A_27a:del]: ( ! [V0m1:$i] : (mem(V0m1,ty_2Esptree_2Espt(A_27a)) => ( ! [V1m2:$i] : (mem(V1m2,ty_2Esptree_2Espt(A_27a)) => ((p(ap(c_2Esptree_2Ewf(A_27a),V0m1)) & p(ap(c_2Esptree_2Ewf(A_27a),V1m2))) => p(ap(c_2Esptree_2Ewf(A_27a),ap(ap(c_2Esptree_2Eunion(A_27a),V0m1),V1m2))))))))))).
tff(conj_thm_2Esptree_2Elookup__union,lemma,(( ! [A_27a:del]: ( ! [V0m1:$i] : (mem(V0m1,ty_2Esptree_2Espt(A_27a)) => ( ! [V1m2:$i] : (mem(V1m2,ty_2Esptree_2Espt(A_27a)) => ( ! [V2k:tp__ty_2Enum_2Enum] : (ap(ap(c_2Esptree_2Elookup(A_27a),inj__ty_2Enum_2Enum(V2k)),ap(ap(c_2Esptree_2Eunion(A_27a),V0m1),V1m2)) = ap(ap(ap(c_2Eoption_2Eoption__CASE(A_27a,ty_2Eoption_2Eoption(A_27a)),ap(ap(c_2Esptree_2Elookup(A_27a),inj__ty_2Enum_2Enum(V2k)),V0m1)),ap(ap(c_2Esptree_2Elookup(A_27a),inj__ty_2Enum_2Enum(V2k)),V1m2)),f1905(A_27a))))))))))).
tff(ax_thm_2Esptree_2Einter__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0t:$i] : (mem(V0t,ty_2Esptree_2Espt(A_27b)) => (ap(ap(c_2Esptree_2Einter(A_27a,A_27b),c_2Esptree_2ELN(A_27a)),V0t) = c_2Esptree_2ELN(A_27a)))) & (( ! [V1a:$i] : (mem(V1a,A_27a) => ( ! [V2t:$i] : (mem(V2t,ty_2Esptree_2Espt(A_27b)) => (ap(ap(c_2Esptree_2Einter(A_27a,A_27b),ap(c_2Esptree_2ELS(A_27a),V1a)),V2t) = ap(ap(ap(ap(ap(c_2Esptree_2Espt__CASE(A_27b,ty_2Esptree_2Espt(A_27a)),V2t),c_2Esptree_2ELN(A_27a)),k(A_27b,ap(c_2Esptree_2ELS(A_27a),V1a))),k(ty_2Esptree_2Espt(A_27b),k(ty_2Esptree_2Espt(A_27b),c_2Esptree_2ELN(A_27a)))),k(ty_2Esptree_2Espt(A_27b),k(A_27b,k(ty_2Esptree_2Espt(A_27b),ap(c_2Esptree_2ELS(A_27a),V1a)))))))))) & (( ! [V9t1:$i] : (mem(V9t1,ty_2Esptree_2Espt(A_27a)) => ( ! [V10t2:$i] : (mem(V10t2,ty_2Esptree_2Espt(A_27a)) => ( ! [V11t:$i] : (mem(V11t,ty_2Esptree_2Espt(A_27b)) => (ap(ap(c_2Esptree_2Einter(A_27a,A_27b),ap(ap(c_2Esptree_2EBN(A_27a),V9t1),V10t2)),V11t) = ap(ap(ap(ap(ap(c_2Esptree_2Espt__CASE(A_27b,ty_2Esptree_2Espt(A_27a)),V11t),c_2Esptree_2ELN(A_27a)),k(A_27b,c_2Esptree_2ELN(A_27a))),f2364(A_27a,A_27b,V9t1,V10t2)),f2366(A_27a,A_27b,V9t1,V10t2))))))))) & ( ! [V18t1:$i] : (mem(V18t1,ty_2Esptree_2Espt(A_27a)) => ( ! [V19a:$i] : (mem(V19a,A_27a) => ( ! [V20t2:$i] : (mem(V20t2,ty_2Esptree_2Espt(A_27a)) => ( ! [V21t:$i] : (mem(V21t,ty_2Esptree_2Espt(A_27b)) => (ap(ap(c_2Esptree_2Einter(A_27a,A_27b),ap(ap(ap(c_2Esptree_2EBS(A_27a),V18t1),V19a),V20t2)),V21t) = ap(ap(ap(ap(ap(c_2Esptree_2Espt__CASE(A_27b,ty_2Esptree_2Espt(A_27a)),V21t),c_2Esptree_2ELN(A_27a)),k(A_27b,ap(c_2Esptree_2ELS(A_27a),V19a))),f2368(A_27a,A_27b,V18t1,V20t2)),f2370(A_27a,A_27b,V19a,V18t1,V20t2))))))))))))))))).
tff(ax_thm_2Esptree_2Einter__eq__def,axiom,( ! [A_27a:del]: (( ! [V0t:$i] : (mem(V0t,ty_2Esptree_2Espt(A_27a)) => (ap(ap(c_2Esptree_2Einter__eq(A_27a),c_2Esptree_2ELN(A_27a)),V0t) = c_2Esptree_2ELN(A_27a)))) & (( ! [V1a:$i] : (mem(V1a,A_27a) => ( ! [V2t:$i] : (mem(V2t,ty_2Esptree_2Espt(A_27a)) => (ap(ap(c_2Esptree_2Einter__eq(A_27a),ap(c_2Esptree_2ELS(A_27a),V1a)),V2t) = ap(ap(ap(ap(ap(c_2Esptree_2Espt__CASE(A_27a,ty_2Esptree_2Espt(A_27a)),V2t),c_2Esptree_2ELN(A_27a)),f2371(A_27a,V1a)),k(ty_2Esptree_2Espt(A_27a),k(ty_2Esptree_2Espt(A_27a),c_2Esptree_2ELN(A_27a)))),k(ty_2Esptree_2Espt(A_27a),f2372(A_27a,V1a)))))))) & (( ! [V9t1:$i] : (mem(V9t1,ty_2Esptree_2Espt(A_27a)) => ( ! [V10t2:$i] : (mem(V10t2,ty_2Esptree_2Espt(A_27a)) => ( ! [V11t:$i] : (mem(V11t,ty_2Esptree_2Espt(A_27a)) => (ap(ap(c_2Esptree_2Einter__eq(A_27a),ap(ap(c_2Esptree_2EBN(A_27a),V9t1),V10t2)),V11t) = ap(ap(ap(ap(ap(c_2Esptree_2Espt__CASE(A_27a,ty_2Esptree_2Espt(A_27a)),V11t),c_2Esptree_2ELN(A_27a)),k(A_27a,c_2Esptree_2ELN(A_27a))),f2374(A_27a,V9t1,V10t2)),f2376(A_27a,V9t1,V10t2))))))))) & ( ! [V18t1:$i] : (mem(V18t1,ty_2Esptree_2Espt(A_27a)) => ( ! [V19a:$i] : (mem(V19a,A_27a) => ( ! [V20t2:$i] : (mem(V20t2,ty_2Esptree_2Espt(A_27a)) => ( ! [V21t:$i] : (mem(V21t,ty_2Esptree_2Espt(A_27a)) => (ap(ap(c_2Esptree_2Einter__eq(A_27a),ap(ap(ap(c_2Esptree_2EBS(A_27a),V18t1),V19a),V20t2)),V21t) = ap(ap(ap(ap(ap(c_2Esptree_2Espt__CASE(A_27a,ty_2Esptree_2Espt(A_27a)),V21t),c_2Esptree_2ELN(A_27a)),f2377(A_27a,V19a)),f2379(A_27a,V18t1,V20t2)),f2382(A_27a,V19a,V18t1,V20t2)))))))))))))))).
tff(ax_thm_2Esptree_2Edifference__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0t:$i] : (mem(V0t,ty_2Esptree_2Espt(A_27b)) => (ap(ap(c_2Esptree_2Edifference(A_27a,A_27b),c_2Esptree_2ELN(A_27a)),V0t) = c_2Esptree_2ELN(A_27a)))) & (( ! [V1a:$i] : (mem(V1a,A_27a) => ( ! [V2t:$i] : (mem(V2t,ty_2Esptree_2Espt(A_27b)) => (ap(ap(c_2Esptree_2Edifference(A_27a,A_27b),ap(c_2Esptree_2ELS(A_27a),V1a)),V2t) = ap(ap(ap(ap(ap(c_2Esptree_2Espt__CASE(A_27b,ty_2Esptree_2Espt(A_27a)),V2t),ap(c_2Esptree_2ELS(A_27a),V1a)),k(A_27b,c_2Esptree_2ELN(A_27a))),k(ty_2Esptree_2Espt(A_27b),k(ty_2Esptree_2Espt(A_27b),ap(c_2Esptree_2ELS(A_27a),V1a)))),k(ty_2Esptree_2Espt(A_27b),k(A_27b,k(ty_2Esptree_2Espt(A_27b),c_2Esptree_2ELN(A_27a)))))))))) & (( ! [V9t1:$i] : (mem(V9t1,ty_2Esptree_2Espt(A_27a)) => ( ! [V10t2:$i] : (mem(V10t2,ty_2Esptree_2Espt(A_27a)) => ( ! [V11t:$i] : (mem(V11t,ty_2Esptree_2Espt(A_27b)) => (ap(ap(c_2Esptree_2Edifference(A_27a,A_27b),ap(ap(c_2Esptree_2EBN(A_27a),V9t1),V10t2)),V11t) = ap(ap(ap(ap(ap(c_2Esptree_2Espt__CASE(A_27b,ty_2Esptree_2Espt(A_27a)),V11t),ap(ap(c_2Esptree_2EBN(A_27a),V9t1),V10t2)),k(A_27b,ap(ap(c_2Esptree_2EBN(A_27a),V9t1),V10t2))),f2384(A_27a,A_27b,V9t1,V10t2)),f2386(A_27a,A_27b,V9t1,V10t2))))))))) & ( ! [V18t1:$i] : (mem(V18t1,ty_2Esptree_2Espt(A_27a)) => ( ! [V19a:$i] : (mem(V19a,A_27a) => ( ! [V20t2:$i] : (mem(V20t2,ty_2Esptree_2Espt(A_27a)) => ( ! [V21t:$i] : (mem(V21t,ty_2Esptree_2Espt(A_27b)) => (ap(ap(c_2Esptree_2Edifference(A_27a,A_27b),ap(ap(ap(c_2Esptree_2EBS(A_27a),V18t1),V19a),V20t2)),V21t) = ap(ap(ap(ap(ap(c_2Esptree_2Espt__CASE(A_27b,ty_2Esptree_2Espt(A_27a)),V21t),ap(ap(ap(c_2Esptree_2EBS(A_27a),V18t1),V19a),V20t2)),k(A_27b,ap(ap(c_2Esptree_2EBN(A_27a),V18t1),V20t2))),f2388(A_27a,A_27b,V19a,V18t1,V20t2)),f2390(A_27a,A_27b,V18t1,V20t2))))))))))))))))).
tff(conj_thm_2Esptree_2Ewf__inter,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0m1:$i] : (mem(V0m1,ty_2Esptree_2Espt(A_27a)) => ( ! [V1m2:$i] : (mem(V1m2,ty_2Esptree_2Espt(A_27b)) => p(ap(c_2Esptree_2Ewf(A_27a),ap(ap(c_2Esptree_2Einter(A_27a,A_27b),V0m1),V1m2))))))))))).
tff(conj_thm_2Esptree_2Elookup__inter,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0m1:$i] : (mem(V0m1,ty_2Esptree_2Espt(A_27a)) => ( ! [V1m2:$i] : (mem(V1m2,ty_2Esptree_2Espt(A_27b)) => ( ! [V2k:tp__ty_2Enum_2Enum] : (ap(ap(c_2Esptree_2Elookup(A_27a),inj__ty_2Enum_2Enum(V2k)),ap(ap(c_2Esptree_2Einter(A_27a,A_27b),V0m1),V1m2)) = ap(ap(c_2Epair_2Epair__CASE(ty_2Eoption_2Eoption(A_27a),ty_2Eoption_2Eoption(A_27a),ty_2Eoption_2Eoption(A_27b)),ap(ap(c_2Epair_2E_2C(ty_2Eoption_2Eoption(A_27a),ty_2Eoption_2Eoption(A_27b)),ap(ap(c_2Esptree_2Elookup(A_27a),inj__ty_2Enum_2Enum(V2k)),V0m1)),ap(ap(c_2Esptree_2Elookup(A_27b),inj__ty_2Enum_2Enum(V2k)),V1m2))),f2393(A_27b,A_27a)))))))))))).
tff(conj_thm_2Esptree_2Elookup__inter__eq,lemma,(( ! [A_27a:del]: ( ! [V0m1:$i] : (mem(V0m1,ty_2Esptree_2Espt(A_27a)) => ( ! [V1m2:$i] : (mem(V1m2,ty_2Esptree_2Espt(A_27a)) => ( ! [V2k:tp__ty_2Enum_2Enum] : (ap(ap(c_2Esptree_2Elookup(A_27a),inj__ty_2Enum_2Enum(V2k)),ap(ap(c_2Esptree_2Einter__eq(A_27a),V0m1),V1m2)) = ap(ap(ap(c_2Eoption_2Eoption__CASE(A_27a,ty_2Eoption_2Eoption(A_27a)),ap(ap(c_2Esptree_2Elookup(A_27a),inj__ty_2Enum_2Enum(V2k)),V0m1)),c_2Eoption_2ENONE(A_27a)),f2394(A_27a,V1m2,V2k))))))))))).
tff(conj_thm_2Esptree_2Elookup__inter__EQ,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:tp__ty_2Enum_2Enum] : ( ! [V1t1:$i] : (mem(V1t1,ty_2Esptree_2Espt(A_27a)) => ( ! [V2t2:$i] : (mem(V2t2,ty_2Esptree_2Espt(A_27b)) => ( ! [V3y:$i] : (mem(V3y,A_27a) => (((ap(ap(c_2Esptree_2Elookup(A_27a),inj__ty_2Enum_2Enum(V0x)),ap(ap(c_2Esptree_2Einter(A_27a,A_27b),V1t1),V2t2)) = ap(c_2Eoption_2ESOME(A_27a),V3y)) <=> ((ap(ap(c_2Esptree_2Elookup(A_27a),inj__ty_2Enum_2Enum(V0x)),V1t1) = ap(c_2Eoption_2ESOME(A_27a),V3y)) & (~~ (ap(ap(c_2Esptree_2Elookup(A_27b),inj__ty_2Enum_2Enum(V0x)),V2t2) = c_2Eoption_2ENONE(A_27b))))) & ((ap(ap(c_2Esptree_2Elookup(A_27a),inj__ty_2Enum_2Enum(V0x)),ap(ap(c_2Esptree_2Einter(A_27a,A_27b),V1t1),V2t2)) = c_2Eoption_2ENONE(A_27a)) <=> ((ap(ap(c_2Esptree_2Elookup(A_27a),inj__ty_2Enum_2Enum(V0x)),V1t1) = c_2Eoption_2ENONE(A_27a)) | (ap(ap(c_2Esptree_2Elookup(A_27b),inj__ty_2Enum_2Enum(V0x)),V2t2) = c_2Eoption_2ENONE(A_27b)))))))))))))))).
tff(conj_thm_2Esptree_2Elookup__inter__assoc,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0x:tp__ty_2Enum_2Enum] : ( ! [V1t1:$i] : (mem(V1t1,ty_2Esptree_2Espt(A_27a)) => ( ! [V2t2:$i] : (mem(V2t2,ty_2Esptree_2Espt(A_27b)) => ( ! [V3t3:$i] : (mem(V3t3,ty_2Esptree_2Espt(A_27c)) => (ap(ap(c_2Esptree_2Elookup(A_27a),inj__ty_2Enum_2Enum(V0x)),ap(ap(c_2Esptree_2Einter(A_27a,A_27b),V1t1),ap(ap(c_2Esptree_2Einter(A_27b,A_27c),V2t2),V3t3))) = ap(ap(c_2Esptree_2Elookup(A_27a),inj__ty_2Enum_2Enum(V0x)),ap(ap(c_2Esptree_2Einter(A_27a,A_27c),ap(ap(c_2Esptree_2Einter(A_27a,A_27b),V1t1),V2t2)),V3t3))))))))))))))).
tff(conj_thm_2Esptree_2Elookup__difference,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0m1:$i] : (mem(V0m1,ty_2Esptree_2Espt(A_27a)) => ( ! [V1m2:$i] : (mem(V1m2,ty_2Esptree_2Espt(A_27b)) => ( ! [V2k:tp__ty_2Enum_2Enum] : (ap(ap(c_2Esptree_2Elookup(A_27a),inj__ty_2Enum_2Enum(V2k)),ap(ap(c_2Esptree_2Edifference(A_27a,A_27b),V0m1),V1m2)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eoption_2Eoption(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Eoption_2Eoption(A_27b)),ap(ap(c_2Esptree_2Elookup(A_27b),inj__ty_2Enum_2Enum(V2k)),V1m2)),c_2Eoption_2ENONE(A_27b))),ap(ap(c_2Esptree_2Elookup(A_27a),inj__ty_2Enum_2Enum(V2k)),V0m1)),c_2Eoption_2ENONE(A_27a)))))))))))).
tff(ax_thm_2Esptree_2Elrnext__primitive__def,axiom,(c_2Esptree_2Elrnext = ap(ap(c_2Erelation_2EWFREC(ty_2Enum_2Enum,ty_2Enum_2Enum),ap(c_2Emin_2E_40(arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool))),f2396)),f2398))).
tff(conj_thm_2Esptree_2Elrnext__ind,lemma,(( ! [V0P:$i] : (mem(V0P,arr(ty_2Enum_2Enum,bool)) => (( ! [V1n:tp__ty_2Enum_2Enum] : (((~~ (V1n = fo__c_2Enum_2E0)) => p(ap(V0P,ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V1n)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) => p(ap(V0P,inj__ty_2Enum_2Enum(V1n))))) => ( ! [V2v:tp__ty_2Enum_2Enum] : p(ap(V0P,inj__ty_2Enum_2Enum(V2v))))))))).
tff(conj_thm_2Esptree_2Elrnext__def,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Esptree_2Elrnext,inj__ty_2Enum_2Enum(V0n))) = surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V0n)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(c_2Esptree_2Elrnext,ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V0n)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))).
tff(conj_thm_2Esptree_2Elrnext__thm,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0a:$i] : (mem(V0a,A_27a) => (surj__ty_2Enum_2Enum(ap(c_2Esptree_2Elrnext,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))) & (( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2a:$i] : (mem(V2a,A_27b) => (surj__ty_2Enum_2Enum(ap(c_2Esptree_2Elrnext,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(V1n)))) = surj__ty_2Enum_2Enum(ap(c_2Esptree_2Elrnext,inj__ty_2Enum_2Enum(V1n))))))) & ((surj__ty_2Enum_2Enum(ap(c_2Esptree_2Elrnext,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) & (( ! [V3n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Esptree_2Elrnext,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V3n)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(c_2Esptree_2Elrnext,inj__ty_2Enum_2Enum(V3n)))))) & ( ! [V4n:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(c_2Esptree_2Elrnext,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V4n)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(c_2Esptree_2Elrnext,inj__ty_2Enum_2Enum(V4n)))))))))))))).
tff(ax_thm_2Esptree_2Edomain__def,axiom,( ! [A_27a:del]: ((ap(c_2Esptree_2Edomain(A_27a),c_2Esptree_2ELN(A_27a)) = c_2Epred__set_2EEMPTY(ty_2Enum_2Enum)) & (( ! [V0v0:$i] : (mem(V0v0,A_27a) => (ap(c_2Esptree_2Edomain(A_27a),ap(c_2Esptree_2ELS(A_27a),V0v0)) = ap(ap(c_2Epred__set_2EINSERT(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),c_2Epred__set_2EEMPTY(ty_2Enum_2Enum))))) & (( ! [V1t1:$i] : (mem(V1t1,ty_2Esptree_2Espt(A_27a)) => ( ! [V2t2:$i] : (mem(V2t2,ty_2Esptree_2Espt(A_27a)) => (ap(c_2Esptree_2Edomain(A_27a),ap(ap(c_2Esptree_2EBN(A_27a),V1t1),V2t2)) = ap(ap(c_2Epred__set_2EUNION(ty_2Enum_2Enum),ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,ty_2Enum_2Enum),f2399),ap(c_2Esptree_2Edomain(A_27a),V1t1))),ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,ty_2Enum_2Enum),f2400),ap(c_2Esptree_2Edomain(A_27a),V2t2)))))))) & ( ! [V5t1:$i] : (mem(V5t1,ty_2Esptree_2Espt(A_27a)) => ( ! [V6v1:$i] : (mem(V6v1,A_27a) => ( ! [V7t2:$i] : (mem(V7t2,ty_2Esptree_2Espt(A_27a)) => (ap(c_2Esptree_2Edomain(A_27a),ap(ap(ap(c_2Esptree_2EBS(A_27a),V5t1),V6v1),V7t2)) = ap(ap(c_2Epred__set_2EUNION(ty_2Enum_2Enum),ap(ap(c_2Epred__set_2EUNION(ty_2Enum_2Enum),ap(ap(c_2Epred__set_2EINSERT(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),c_2Epred__set_2EEMPTY(ty_2Enum_2Enum))),ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,ty_2Enum_2Enum),f2401),ap(c_2Esptree_2Edomain(A_27a),V5t1)))),ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,ty_2Enum_2Enum),f2402),ap(c_2Esptree_2Edomain(A_27a),V7t2))))))))))))))).
tff(conj_thm_2Esptree_2EFINITE__domain,lemma,(( ! [A_27a:del]: ( ! [V0t:$i] : (mem(V0t,ty_2Esptree_2Espt(A_27a)) => p(ap(c_2Epred__set_2EFINITE(ty_2Enum_2Enum),ap(c_2Esptree_2Edomain(A_27a),V0t)))))))).
tff(conj_thm_2Esptree_2Esize__insert,lemma,(( ! [A_27a:del]: ( ! [V0k:tp__ty_2Enum_2Enum] : ( ! [V1v:$i] : (mem(V1v,A_27a) => ( ! [V2m:$i] : (mem(V2m,ty_2Esptree_2Espt(A_27a)) => (surj__ty_2Enum_2Enum(ap(c_2Esptree_2Esize(A_27a),ap(ap(ap(c_2Esptree_2Einsert(A_27a),inj__ty_2Enum_2Enum(V0k)),V1v),V2m))) = surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V0k)),ap(c_2Esptree_2Edomain(A_27a),V2m))),ap(c_2Esptree_2Esize(A_27a),V2m)),ap(ap(c_2Earithmetic_2E_2B,ap(c_2Esptree_2Esize(A_27a),V2m)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))))))))).
tff(conj_thm_2Esptree_2Elookup__fromList,lemma,(( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : (mem(V1l,ty_2Elist_2Elist(A_27a)) => (ap(ap(c_2Esptree_2Elookup(A_27a),inj__ty_2Enum_2Enum(V0n)),ap(c_2Esptree_2EfromList(A_27a),V1l)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eoption_2Eoption(A_27a)),ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0n)),ap(c_2Elist_2ELENGTH(A_27a),V1l))),ap(c_2Eoption_2ESOME(A_27a),ap(ap(c_2Elist_2EEL(A_27a),inj__ty_2Enum_2Enum(V0n)),V1l))),c_2Eoption_2ENONE(A_27a))))))))).
tff(conj_thm_2Esptree_2Edomain__lookup,lemma,(( ! [A_27a:del]: ( ! [V0t:$i] : (mem(V0t,ty_2Esptree_2Espt(A_27a)) => ( ! [V1k:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V1k)),ap(c_2Esptree_2Edomain(A_27a),V0t))) <=> (? [V2v:$i] : (mem(V2v,A_27a) & (ap(ap(c_2Esptree_2Elookup(A_27a),inj__ty_2Enum_2Enum(V1k)),V0t) = ap(c_2Eoption_2ESOME(A_27a),V2v))))))))))).
tff(conj_thm_2Esptree_2Elookup__inter__alt,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:tp__ty_2Enum_2Enum] : ( ! [V1t1:$i] : (mem(V1t1,ty_2Esptree_2Espt(A_27a)) => ( ! [V2t2:$i] : (mem(V2t2,ty_2Esptree_2Espt(A_27b)) => (ap(ap(c_2Esptree_2Elookup(A_27a),inj__ty_2Enum_2Enum(V0x)),ap(ap(c_2Esptree_2Einter(A_27a,A_27b),V1t1),V2t2)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eoption_2Eoption(A_27a)),ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V0x)),ap(c_2Esptree_2Edomain(A_27b),V2t2))),ap(ap(c_2Esptree_2Elookup(A_27a),inj__ty_2Enum_2Enum(V0x)),V1t1)),c_2Eoption_2ENONE(A_27a)))))))))))).
tff(conj_thm_2Esptree_2Elookup__NONE__domain,lemma,(( ! [A_27a:del]: ( ! [V0k:tp__ty_2Enum_2Enum] : ( ! [V1t:$i] : (mem(V1t,ty_2Esptree_2Espt(A_27a)) => ((ap(ap(c_2Esptree_2Elookup(A_27a),inj__ty_2Enum_2Enum(V0k)),V1t) = c_2Eoption_2ENONE(A_27a)) <=> (~~ p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V0k)),ap(c_2Esptree_2Edomain(A_27a),V1t))))))))))).
tff(conj_thm_2Esptree_2Edomain__union,lemma,(( ! [A_27a:del]: ( ! [V0t1:$i] : (mem(V0t1,ty_2Esptree_2Espt(A_27a)) => ( ! [V1t2:$i] : (mem(V1t2,ty_2Esptree_2Espt(A_27a)) => (ap(c_2Esptree_2Edomain(A_27a),ap(ap(c_2Esptree_2Eunion(A_27a),V0t1),V1t2)) = ap(ap(c_2Epred__set_2EUNION(ty_2Enum_2Enum),ap(c_2Esptree_2Edomain(A_27a),V0t1)),ap(c_2Esptree_2Edomain(A_27a),V1t2)))))))))).
tff(conj_thm_2Esptree_2Edomain__inter,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0t1:$i] : (mem(V0t1,ty_2Esptree_2Espt(A_27a)) => ( ! [V1t2:$i] : (mem(V1t2,ty_2Esptree_2Espt(A_27b)) => (ap(c_2Esptree_2Edomain(A_27a),ap(ap(c_2Esptree_2Einter(A_27a,A_27b),V0t1),V1t2)) = ap(ap(c_2Epred__set_2EINTER(ty_2Enum_2Enum),ap(c_2Esptree_2Edomain(A_27a),V0t1)),ap(c_2Esptree_2Edomain(A_27b),V1t2))))))))))).
tff(conj_thm_2Esptree_2Edomain__insert,lemma,(( ! [A_27a:del]: ( ! [V0k:tp__ty_2Enum_2Enum] : ( ! [V1v:$i] : (mem(V1v,A_27a) => ( ! [V2t:$i] : (mem(V2t,ty_2Esptree_2Espt(A_27a)) => (ap(c_2Esptree_2Edomain(A_27a),ap(ap(ap(c_2Esptree_2Einsert(A_27a),inj__ty_2Enum_2Enum(V0k)),V1v),V2t)) = ap(ap(c_2Epred__set_2EINSERT(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V0k)),ap(c_2Esptree_2Edomain(A_27a),V2t))))))))))).
tff(conj_thm_2Esptree_2Edomain__difference,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0t1:$i] : (mem(V0t1,ty_2Esptree_2Espt(A_27a)) => ( ! [V1t2:$i] : (mem(V1t2,ty_2Esptree_2Espt(A_27b)) => (ap(c_2Esptree_2Edomain(A_27a),ap(ap(c_2Esptree_2Edifference(A_27a,A_27b),V0t1),V1t2)) = ap(ap(c_2Epred__set_2EDIFF(ty_2Enum_2Enum),ap(c_2Esptree_2Edomain(A_27a),V0t1)),ap(c_2Esptree_2Edomain(A_27b),V1t2))))))))))).
tff(conj_thm_2Esptree_2Edomain__sing,lemma,(( ! [A_27a:del]: ( ! [V0k:tp__ty_2Enum_2Enum] : ( ! [V1v:$i] : (mem(V1v,A_27a) => (ap(c_2Esptree_2Edomain(A_27a),ap(ap(ap(c_2Esptree_2Einsert(A_27a),inj__ty_2Enum_2Enum(V0k)),V1v),c_2Esptree_2ELN(A_27a))) = ap(ap(c_2Epred__set_2EINSERT(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V0k)),c_2Epred__set_2EEMPTY(ty_2Enum_2Enum))))))))).
tff(conj_thm_2Esptree_2Edomain__fromList,lemma,(( ! [A_27a:del]: ( ! [V0l:$i] : (mem(V0l,ty_2Elist_2Elist(A_27a)) => (ap(c_2Esptree_2Edomain(A_27a),ap(c_2Esptree_2EfromList(A_27a),V0l)) = ap(c_2Epred__set_2Ecount,ap(c_2Elist_2ELENGTH(A_27a),V0l)))))))).
tff(conj_thm_2Esptree_2Elookup__delete,lemma,(( ! [A_27a:del]: ( ! [V0t:$i] : (mem(V0t,ty_2Esptree_2Espt(A_27a)) => ( ! [V1k1:tp__ty_2Enum_2Enum] : ( ! [V2k2:tp__ty_2Enum_2Enum] : (ap(ap(c_2Esptree_2Elookup(A_27a),inj__ty_2Enum_2Enum(V1k1)),ap(ap(c_2Esptree_2Edelete(A_27a),inj__ty_2Enum_2Enum(V2k2)),V0t)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eoption_2Eoption(A_27a)),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V1k1)),inj__ty_2Enum_2Enum(V2k2))),c_2Eoption_2ENONE(A_27a)),ap(ap(c_2Esptree_2Elookup(A_27a),inj__ty_2Enum_2Enum(V1k1)),V0t)))))))))).
tff(conj_thm_2Esptree_2Edomain__delete,lemma,(( ! [A_27a:del]: ( ! [V0k:tp__ty_2Enum_2Enum] : ( ! [V1t:$i] : (mem(V1t,ty_2Esptree_2Espt(A_27a)) => (ap(c_2Esptree_2Edomain(A_27a),ap(ap(c_2Esptree_2Edelete(A_27a),inj__ty_2Enum_2Enum(V0k)),V1t)) = ap(ap(c_2Epred__set_2EDELETE(ty_2Enum_2Enum),ap(c_2Esptree_2Edomain(A_27a),V1t)),inj__ty_2Enum_2Enum(V0k))))))))).
tff(ax_thm_2Esptree_2Efoldi__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0f:$i] : (mem(V0f,arr(ty_2Enum_2Enum,arr(A_27b,arr(A_27a,A_27a)))) => ( ! [V1i:tp__ty_2Enum_2Enum] : ( ! [V2acc:$i] : (mem(V2acc,A_27a) => (ap(ap(ap(ap(c_2Esptree_2Efoldi(A_27a,A_27b),V0f),inj__ty_2Enum_2Enum(V1i)),V2acc),c_2Esptree_2ELN(A_27b)) = V2acc)))))) & (( ! [V3f:$i] : (mem(V3f,arr(ty_2Enum_2Enum,arr(A_27b,arr(A_27a,A_27a)))) => ( ! [V4i:tp__ty_2Enum_2Enum] : ( ! [V5acc:$i] : (mem(V5acc,A_27a) => ( ! [V6a:$i] : (mem(V6a,A_27b) => (ap(ap(ap(ap(c_2Esptree_2Efoldi(A_27a,A_27b),V3f),inj__ty_2Enum_2Enum(V4i)),V5acc),ap(c_2Esptree_2ELS(A_27b),V6a)) = ap(ap(ap(V3f,inj__ty_2Enum_2Enum(V4i)),V6a),V5acc))))))))) & (( ! [V7f:$i] : (mem(V7f,arr(ty_2Enum_2Enum,arr(A_27b,arr(A_27a,A_27a)))) => ( ! [V8i:tp__ty_2Enum_2Enum] : ( ! [V9acc:$i] : (mem(V9acc,A_27a) => ( ! [V10t1:$i] : (mem(V10t1,ty_2Esptree_2Espt(A_27b)) => ( ! [V11t2:$i] : (mem(V11t2,ty_2Esptree_2Espt(A_27b)) => (ap(ap(ap(ap(c_2Esptree_2Efoldi(A_27a,A_27b),V7f),inj__ty_2Enum_2Enum(V8i)),V9acc),ap(ap(c_2Esptree_2EBN(A_27b),V10t1),V11t2)) = ap(ap(c_2Ebool_2ELET(ty_2Enum_2Enum,A_27a),f2403(A_27a,A_27b,V7f,V8i,V9acc,V10t1,V11t2)),ap(c_2Esptree_2Elrnext,inj__ty_2Enum_2Enum(V8i))))))))))))) & ( ! [V13f:$i] : (mem(V13f,arr(ty_2Enum_2Enum,arr(A_27b,arr(A_27a,A_27a)))) => ( ! [V14i:tp__ty_2Enum_2Enum] : ( ! [V15acc:$i] : (mem(V15acc,A_27a) => ( ! [V16t1:$i] : (mem(V16t1,ty_2Esptree_2Espt(A_27b)) => ( ! [V17a:$i] : (mem(V17a,A_27b) => ( ! [V18t2:$i] : (mem(V18t2,ty_2Esptree_2Espt(A_27b)) => (ap(ap(ap(ap(c_2Esptree_2Efoldi(A_27a,A_27b),V13f),inj__ty_2Enum_2Enum(V14i)),V15acc),ap(ap(ap(c_2Esptree_2EBS(A_27b),V16t1),V17a),V18t2)) = ap(ap(c_2Ebool_2ELET(ty_2Enum_2Enum,A_27a),f2404(A_27a,A_27b,V13f,V14i,V16t1,V15acc,V17a,V18t2)),ap(c_2Esptree_2Elrnext,inj__ty_2Enum_2Enum(V14i))))))))))))))))))))).
tff(conj_thm_2Esptree_2Espt__acc__ind,lemma,(( ! [V0P:$i] : (mem(V0P,arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,bool))) => ((( ! [V1i:tp__ty_2Enum_2Enum] : p(ap(ap(V0P,inj__ty_2Enum_2Enum(V1i)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)))) & ( ! [V2i:tp__ty_2Enum_2Enum] : ( ! [V3k:tp__ty_2Enum_2Enum] : (p(ap(ap(V0P,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V2i)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(c_2Earithmetic_2EEVEN,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V3k)))),ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(c_2Esptree_2Elrnext,inj__ty_2Enum_2Enum(V2i)))),ap(c_2Esptree_2Elrnext,inj__ty_2Enum_2Enum(V2i))))),ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V3k)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))) => p(ap(ap(V0P,inj__ty_2Enum_2Enum(V2i)),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V3k)))))))) => ( ! [V4v:tp__ty_2Enum_2Enum] : ( ! [V5v1:tp__ty_2Enum_2Enum] : p(ap(ap(V0P,inj__ty_2Enum_2Enum(V4v)),inj__ty_2Enum_2Enum(V5v1)))))))))).
tff(conj_thm_2Esptree_2Espt__acc__def,lemma,((( ! [V0i:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Esptree_2Espt__acc,inj__ty_2Enum_2Enum(V0i)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = V0i)) & ( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2i:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Esptree_2Espt__acc,inj__ty_2Enum_2Enum(V2i)),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1k)))) = surj__ty_2Enum_2Enum(ap(ap(c_2Esptree_2Espt__acc,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V2i)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(c_2Earithmetic_2EEVEN,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1k)))),ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(c_2Esptree_2Elrnext,inj__ty_2Enum_2Enum(V2i)))),ap(c_2Esptree_2Elrnext,inj__ty_2Enum_2Enum(V2i))))),ap(ap(c_2Earithmetic_2EDIV,inj__ty_2Enum_2Enum(V1k)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))).
tff(conj_thm_2Esptree_2Espt__acc__def__compute,lemma,((( ! [V0i:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Esptree_2Espt__acc,inj__ty_2Enum_2Enum(V0i)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = V0i)) & (( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2i:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Esptree_2Espt__acc,inj__ty_2Enum_2Enum(V2i)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1k))))) = surj__ty_2Enum_2Enum(ap(ap(c_2Esptree_2Espt__acc,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V2i)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(c_2Earithmetic_2EEVEN,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1k))))),ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(c_2Esptree_2Elrnext,inj__ty_2Enum_2Enum(V2i)))),ap(c_2Esptree_2Elrnext,inj__ty_2Enum_2Enum(V2i))))),ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1k)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))) & ( ! [V3k:tp__ty_2Enum_2Enum] : ( ! [V4i:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Esptree_2Espt__acc,inj__ty_2Enum_2Enum(V4i)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V3k))))) = surj__ty_2Enum_2Enum(ap(ap(c_2Esptree_2Espt__acc,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V4i)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(c_2Earithmetic_2EEVEN,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V3k))))),ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(c_2Esptree_2Elrnext,inj__ty_2Enum_2Enum(V4i)))),ap(c_2Esptree_2Elrnext,inj__ty_2Enum_2Enum(V4i))))),ap(ap(c_2Earithmetic_2EDIV,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V3k)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))))))).
tff(conj_thm_2Esptree_2Espt__acc__thm,lemma,(( ! [V0i:tp__ty_2Enum_2Enum] : ( ! [V1k:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Esptree_2Espt__acc,inj__ty_2Enum_2Enum(V0i)),inj__ty_2Enum_2Enum(V1k))) = surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(ap(c_2Emin_2E_3D(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V1k)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),inj__ty_2Enum_2Enum(V0i)),ap(ap(c_2Esptree_2Espt__acc,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0i)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(V1k))),ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),ap(c_2Esptree_2Elrnext,inj__ty_2Enum_2Enum(V0i)))),ap(c_2Esptree_2Elrnext,inj__ty_2Enum_2Enum(V0i))))),ap(ap(c_2Earithmetic_2EDIV,ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V1k)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))).
tff(conj_thm_2Esptree_2Espt__acc__eqn,lemma,(( ! [V0k:tp__ty_2Enum_2Enum] : ( ! [V1i:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Esptree_2Espt__acc,inj__ty_2Enum_2Enum(V1i)),inj__ty_2Enum_2Enum(V0k))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,ap(c_2Esptree_2Elrnext,inj__ty_2Enum_2Enum(V1i))),inj__ty_2Enum_2Enum(V0k))),inj__ty_2Enum_2Enum(V1i)))))))).
tff(conj_thm_2Esptree_2Espt__acc__0,lemma,(( ! [V0k:tp__ty_2Enum_2Enum] : (surj__ty_2Enum_2Enum(ap(ap(c_2Esptree_2Espt__acc,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V0k))) = V0k)))).
tff(conj_thm_2Esptree_2Eset__foldi__keys,lemma,(( ! [A_27a:del]: ( ! [V0t:$i] : (mem(V0t,ty_2Esptree_2Espt(A_27a)) => ( ! [V1a:$i] : (mem(V1a,arr(ty_2Enum_2Enum,bool)) => ( ! [V2i:tp__ty_2Enum_2Enum] : (ap(ap(ap(ap(c_2Esptree_2Efoldi(arr(ty_2Enum_2Enum,bool),A_27a),f2406),inj__ty_2Enum_2Enum(V2i)),V1a),V0t) = ap(ap(c_2Epred__set_2EUNION(ty_2Enum_2Enum),V1a),ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,ty_2Enum_2Enum),f2407(V2i)),ap(c_2Esptree_2Edomain(A_27a),V0t)))))))))))).
tff(conj_thm_2Esptree_2Edomain__foldi,lemma,(( ! [A_27a:del]: ( ! [V0t:$i] : (mem(V0t,ty_2Esptree_2Espt(A_27a)) => (ap(c_2Esptree_2Edomain(A_27a),V0t) = ap(ap(ap(ap(c_2Esptree_2Efoldi(arr(ty_2Enum_2Enum,bool),A_27a),f2409),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),c_2Epred__set_2EEMPTY(ty_2Enum_2Enum)),V0t))))))).
tff(ax_thm_2Esptree_2Emapi0__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0f:$i] : (mem(V0f,arr(ty_2Enum_2Enum,arr(A_27b,A_27a))) => ( ! [V1i:tp__ty_2Enum_2Enum] : (ap(ap(ap(c_2Esptree_2Emapi0(A_27a,A_27b),V0f),inj__ty_2Enum_2Enum(V1i)),c_2Esptree_2ELN(A_27b)) = c_2Esptree_2ELN(A_27a))))) & (( ! [V2f:$i] : (mem(V2f,arr(ty_2Enum_2Enum,arr(A_27b,A_27a))) => ( ! [V3i:tp__ty_2Enum_2Enum] : ( ! [V4a:$i] : (mem(V4a,A_27b) => (ap(ap(ap(c_2Esptree_2Emapi0(A_27a,A_27b),V2f),inj__ty_2Enum_2Enum(V3i)),ap(c_2Esptree_2ELS(A_27b),V4a)) = ap(c_2Esptree_2ELS(A_27a),ap(ap(V2f,inj__ty_2Enum_2Enum(V3i)),V4a)))))))) & (( ! [V5f:$i] : (mem(V5f,arr(ty_2Enum_2Enum,arr(A_27b,A_27a))) => ( ! [V6i:tp__ty_2Enum_2Enum] : ( ! [V7t1:$i] : (mem(V7t1,ty_2Esptree_2Espt(A_27b)) => ( ! [V8t2:$i] : (mem(V8t2,ty_2Esptree_2Espt(A_27b)) => (ap(ap(ap(c_2Esptree_2Emapi0(A_27a,A_27b),V5f),inj__ty_2Enum_2Enum(V6i)),ap(ap(c_2Esptree_2EBN(A_27b),V7t1),V8t2)) = ap(ap(c_2Ebool_2ELET(ty_2Enum_2Enum,ty_2Esptree_2Espt(A_27a)),f2410(A_27a,A_27b,V7t1,V5f,V6i,V8t2)),ap(c_2Esptree_2Elrnext,inj__ty_2Enum_2Enum(V6i))))))))))) & ( ! [V10f:$i] : (mem(V10f,arr(ty_2Enum_2Enum,arr(A_27b,A_27a))) => ( ! [V11i:tp__ty_2Enum_2Enum] : ( ! [V12t1:$i] : (mem(V12t1,ty_2Esptree_2Espt(A_27b)) => ( ! [V13a:$i] : (mem(V13a,A_27b) => ( ! [V14t2:$i] : (mem(V14t2,ty_2Esptree_2Espt(A_27b)) => (ap(ap(ap(c_2Esptree_2Emapi0(A_27a,A_27b),V10f),inj__ty_2Enum_2Enum(V11i)),ap(ap(ap(c_2Esptree_2EBS(A_27b),V12t1),V13a),V14t2)) = ap(ap(c_2Ebool_2ELET(ty_2Enum_2Enum,ty_2Esptree_2Espt(A_27a)),f2411(A_27a,A_27b,V13a,V12t1,V10f,V11i,V14t2)),ap(c_2Esptree_2Elrnext,inj__ty_2Enum_2Enum(V11i))))))))))))))))))).
tff(ax_thm_2Esptree_2Emapi__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,arr(ty_2Enum_2Enum,arr(A_27b,A_27a))) => ( ! [V1pt:$i] : (mem(V1pt,ty_2Esptree_2Espt(A_27b)) => (ap(ap(c_2Esptree_2Emapi(A_27a,A_27b),V0f),V1pt) = ap(ap(ap(c_2Esptree_2Emapi0(A_27a,A_27b),V0f),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),V1pt))))))))).
tff(conj_thm_2Esptree_2Elookup__mapi0,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,arr(ty_2Enum_2Enum,arr(A_27a,A_27b))) => ( ! [V1pt:$i] : (mem(V1pt,ty_2Esptree_2Espt(A_27a)) => ( ! [V2i:tp__ty_2Enum_2Enum] : ( ! [V3k:tp__ty_2Enum_2Enum] : (ap(ap(c_2Esptree_2Elookup(A_27b),inj__ty_2Enum_2Enum(V3k)),ap(ap(ap(c_2Esptree_2Emapi0(A_27b,A_27a),V0f),inj__ty_2Enum_2Enum(V2i)),V1pt)) = ap(ap(ap(c_2Eoption_2Eoption__CASE(A_27a,ty_2Eoption_2Eoption(A_27b)),ap(ap(c_2Esptree_2Elookup(A_27a),inj__ty_2Enum_2Enum(V3k)),V1pt)),c_2Eoption_2ENONE(A_27b)),f2412(A_27a,A_27b,V3k,V2i,V0f))))))))))))).
tff(conj_thm_2Esptree_2Elookup__mapi,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0k:tp__ty_2Enum_2Enum] : ( ! [V1f:$i] : (mem(V1f,arr(ty_2Enum_2Enum,arr(A_27b,A_27a))) => ( ! [V2pt:$i] : (mem(V2pt,ty_2Esptree_2Espt(A_27b)) => (ap(ap(c_2Esptree_2Elookup(A_27a),inj__ty_2Enum_2Enum(V0k)),ap(ap(c_2Esptree_2Emapi(A_27a,A_27b),V1f),V2pt)) = ap(ap(c_2Eoption_2EOPTION__MAP(A_27b,A_27a),ap(V1f,inj__ty_2Enum_2Enum(V0k))),ap(ap(c_2Esptree_2Elookup(A_27b),inj__ty_2Enum_2Enum(V0k)),V2pt)))))))))))).
tff(ax_thm_2Esptree_2EtoAList__def,axiom,( ! [A_27a:del]: (c_2Esptree_2EtoAList(A_27a) = ap(ap(ap(c_2Esptree_2Efoldi(ty_2Elist_2Elist(ty_2Epair_2Eprod(ty_2Enum_2Enum,A_27a)),A_27a),f2415(A_27a)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),c_2Elist_2ENIL(ty_2Epair_2Eprod(ty_2Enum_2Enum,A_27a)))))).
tff(conj_thm_2Esptree_2EMEM__toAList,lemma,(( ! [A_27a:del]: ( ! [V0t:$i] : (mem(V0t,ty_2Esptree_2Espt(A_27a)) => ( ! [V1k:tp__ty_2Enum_2Enum] : ( ! [V2v:$i] : (mem(V2v,A_27a) => (p(ap(ap(c_2Ebool_2EIN(ty_2Epair_2Eprod(ty_2Enum_2Enum,A_27a)),ap(ap(c_2Epair_2E_2C(ty_2Enum_2Enum,A_27a),inj__ty_2Enum_2Enum(V1k)),V2v)),ap(c_2Elist_2ELIST__TO__SET(ty_2Epair_2Eprod(ty_2Enum_2Enum,A_27a)),ap(c_2Esptree_2EtoAList(A_27a),V0t)))) <=> (ap(ap(c_2Esptree_2Elookup(A_27a),inj__ty_2Enum_2Enum(V1k)),V0t) = ap(c_2Eoption_2ESOME(A_27a),V2v))))))))))).
tff(conj_thm_2Esptree_2EALOOKUP__toAList,lemma,(( ! [A_27a:del]: ( ! [V0t:$i] : (mem(V0t,ty_2Esptree_2Espt(A_27a)) => ( ! [V1x:tp__ty_2Enum_2Enum] : (ap(ap(c_2Ealist_2EALOOKUP(A_27a,ty_2Enum_2Enum),ap(c_2Esptree_2EtoAList(A_27a),V0t)),inj__ty_2Enum_2Enum(V1x)) = ap(ap(c_2Esptree_2Elookup(A_27a),inj__ty_2Enum_2Enum(V1x)),V0t)))))))).
tff(conj_thm_2Esptree_2Einsert__union,lemma,(( ! [A_27a:del]: ( ! [V0k:tp__ty_2Enum_2Enum] : ( ! [V1v:$i] : (mem(V1v,A_27a) => ( ! [V2s:$i] : (mem(V2s,ty_2Esptree_2Espt(A_27a)) => (ap(ap(ap(c_2Esptree_2Einsert(A_27a),inj__ty_2Enum_2Enum(V0k)),V1v),V2s) = ap(ap(c_2Esptree_2Eunion(A_27a),ap(ap(ap(c_2Esptree_2Einsert(A_27a),inj__ty_2Enum_2Enum(V0k)),V1v),c_2Esptree_2ELN(A_27a))),V2s)))))))))).
tff(conj_thm_2Esptree_2Edomain__empty,lemma,(( ! [A_27a:del]: ( ! [V0t:$i] : (mem(V0t,ty_2Esptree_2Espt(A_27a)) => (p(ap(c_2Esptree_2Ewf(A_27a),V0t)) => ((V0t = c_2Esptree_2ELN(A_27a)) <=> (ap(c_2Esptree_2Edomain(A_27a),V0t) = c_2Epred__set_2EEMPTY(ty_2Enum_2Enum))))))))).
tff(conj_thm_2Esptree_2EALL__DISTINCT__MAP__FST__toAList,lemma,(( ! [A_27a:del]: ( ! [V0t:$i] : (mem(V0t,ty_2Esptree_2Espt(A_27a)) => p(ap(c_2Elist_2EALL__DISTINCT(ty_2Enum_2Enum),ap(ap(c_2Elist_2EMAP(ty_2Epair_2Eprod(ty_2Enum_2Enum,A_27a),ty_2Enum_2Enum),c_2Epair_2EFST(ty_2Enum_2Enum,A_27a)),ap(c_2Esptree_2EtoAList(A_27a),V0t))))))))).
tff(conj_thm_2Esptree_2Efoldi__FOLDR__toAList,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,arr(ty_2Enum_2Enum,arr(A_27a,arr(A_27b,A_27b)))) => ( ! [V1a:$i] : (mem(V1a,A_27b) => ( ! [V2t:$i] : (mem(V2t,ty_2Esptree_2Espt(A_27a)) => (ap(ap(ap(ap(c_2Esptree_2Efoldi(A_27b,A_27a),V0f),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),V1a),V2t) = ap(ap(ap(c_2Elist_2EFOLDR(ty_2Epair_2Eprod(ty_2Enum_2Enum,A_27a),A_27b),ap(c_2Epair_2EUNCURRY(ty_2Enum_2Enum,A_27a,arr(A_27b,A_27b)),V0f)),V1a),ap(c_2Esptree_2EtoAList(A_27a),V2t))))))))))))).
tff(ax_thm_2Esptree_2EtoListA__def,axiom,( ! [A_27a:del]: (( ! [V0acc:$i] : (mem(V0acc,ty_2Elist_2Elist(A_27a)) => (ap(ap(c_2Esptree_2EtoListA(A_27a),V0acc),c_2Esptree_2ELN(A_27a)) = V0acc))) & (( ! [V1acc:$i] : (mem(V1acc,ty_2Elist_2Elist(A_27a)) => ( ! [V2a:$i] : (mem(V2a,A_27a) => (ap(ap(c_2Esptree_2EtoListA(A_27a),V1acc),ap(c_2Esptree_2ELS(A_27a),V2a)) = ap(ap(c_2Elist_2ECONS(A_27a),V2a),V1acc)))))) & (( ! [V3acc:$i] : (mem(V3acc,ty_2Elist_2Elist(A_27a)) => ( ! [V4t1:$i] : (mem(V4t1,ty_2Esptree_2Espt(A_27a)) => ( ! [V5t2:$i] : (mem(V5t2,ty_2Esptree_2Espt(A_27a)) => (ap(ap(c_2Esptree_2EtoListA(A_27a),V3acc),ap(ap(c_2Esptree_2EBN(A_27a),V4t1),V5t2)) = ap(ap(c_2Esptree_2EtoListA(A_27a),ap(ap(c_2Esptree_2EtoListA(A_27a),V3acc),V5t2)),V4t1)))))))) & ( ! [V6acc:$i] : (mem(V6acc,ty_2Elist_2Elist(A_27a)) => ( ! [V7t1:$i] : (mem(V7t1,ty_2Esptree_2Espt(A_27a)) => ( ! [V8a:$i] : (mem(V8a,A_27a) => ( ! [V9t2:$i] : (mem(V9t2,ty_2Esptree_2Espt(A_27a)) => (ap(ap(c_2Esptree_2EtoListA(A_27a),V6acc),ap(ap(ap(c_2Esptree_2EBS(A_27a),V7t1),V8a),V9t2)) = ap(ap(c_2Esptree_2EtoListA(A_27a),ap(ap(c_2Elist_2ECONS(A_27a),V8a),ap(ap(c_2Esptree_2EtoListA(A_27a),V6acc),V9t2))),V7t1))))))))))))))).
tff(conj_thm_2Esptree_2EtoListA__append,lemma,(( ! [A_27a:del]: ( ! [V0t:$i] : (mem(V0t,ty_2Esptree_2Espt(A_27a)) => ( ! [V1acc:$i] : (mem(V1acc,ty_2Elist_2Elist(A_27a)) => (ap(ap(c_2Esptree_2EtoListA(A_27a),V1acc),V0t) = ap(ap(c_2Elist_2EAPPEND(A_27a),ap(ap(c_2Esptree_2EtoListA(A_27a),c_2Elist_2ENIL(A_27a)),V0t)),V1acc))))))))).
tff(conj_thm_2Esptree_2EisEmpty__toListA,lemma,(( ! [A_27a:del]: ( ! [V0t:$i] : (mem(V0t,ty_2Esptree_2Espt(A_27a)) => ( ! [V1acc:$i] : (mem(V1acc,ty_2Elist_2Elist(A_27a)) => (p(ap(c_2Esptree_2Ewf(A_27a),V0t)) => ((V0t = c_2Esptree_2ELN(A_27a)) <=> (ap(ap(c_2Esptree_2EtoListA(A_27a),V1acc),V0t) = V1acc)))))))))).
tff(ax_thm_2Esptree_2EtoList__def,axiom,( ! [A_27a:del]: ( ! [V0m:$i] : (mem(V0m,ty_2Esptree_2Espt(A_27a)) => (ap(c_2Esptree_2EtoList(A_27a),V0m) = ap(ap(c_2Esptree_2EtoListA(A_27a),c_2Elist_2ENIL(A_27a)),V0m)))))).
tff(conj_thm_2Esptree_2EisEmpty__toList,lemma,(( ! [A_27a:del]: ( ! [V0t:$i] : (mem(V0t,ty_2Esptree_2Espt(A_27a)) => (p(ap(c_2Esptree_2Ewf(A_27a),V0t)) => ((V0t = c_2Esptree_2ELN(A_27a)) <=> (ap(c_2Esptree_2EtoList(A_27a),V0t) = c_2Elist_2ENIL(A_27a))))))))).
tff(conj_thm_2Esptree_2EMEM__toList,lemma,(( ! [A_27a:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1t:$i] : (mem(V1t,ty_2Esptree_2Espt(A_27a)) => (p(ap(ap(c_2Ebool_2EIN(A_27a),V0x),ap(c_2Elist_2ELIST__TO__SET(A_27a),ap(c_2Esptree_2EtoList(A_27a),V1t)))) <=> (? [V2k:tp__ty_2Enum_2Enum] : (ap(ap(c_2Esptree_2Elookup(A_27a),inj__ty_2Enum_2Enum(V2k)),V1t) = ap(c_2Eoption_2ESOME(A_27a),V0x))))))))))).
tff(conj_thm_2Esptree_2Espt__eq__thm,lemma,(( ! [A_27a:del]: ( ! [V0t1:$i] : (mem(V0t1,ty_2Esptree_2Espt(A_27a)) => ( ! [V1t2:$i] : (mem(V1t2,ty_2Esptree_2Espt(A_27a)) => ((p(ap(c_2Esptree_2Ewf(A_27a),V0t1)) & p(ap(c_2Esptree_2Ewf(A_27a),V1t2))) => ((V0t1 = V1t2) <=> ( ! [V2n:tp__ty_2Enum_2Enum] : (ap(ap(c_2Esptree_2Elookup(A_27a),inj__ty_2Enum_2Enum(V2n)),V0t1) = ap(ap(c_2Esptree_2Elookup(A_27a),inj__ty_2Enum_2Enum(V2n)),V1t2)))))))))))).
tff(ax_thm_2Esptree_2Emk__wf__def,axiom,( ! [A_27a:del]: ((ap(c_2Esptree_2Emk__wf(A_27a),c_2Esptree_2ELN(A_27a)) = c_2Esptree_2ELN(A_27a)) & (( ! [V0x:$i] : (mem(V0x,A_27a) => (ap(c_2Esptree_2Emk__wf(A_27a),ap(c_2Esptree_2ELS(A_27a),V0x)) = ap(c_2Esptree_2ELS(A_27a),V0x)))) & (( ! [V1t1:$i] : (mem(V1t1,ty_2Esptree_2Espt(A_27a)) => ( ! [V2t2:$i] : (mem(V2t2,ty_2Esptree_2Espt(A_27a)) => (ap(c_2Esptree_2Emk__wf(A_27a),ap(ap(c_2Esptree_2EBN(A_27a),V1t1),V2t2)) = ap(ap(c_2Esptree_2Emk__BN(A_27a),ap(c_2Esptree_2Emk__wf(A_27a),V1t1)),ap(c_2Esptree_2Emk__wf(A_27a),V2t2))))))) & ( ! [V3t1:$i] : (mem(V3t1,ty_2Esptree_2Espt(A_27a)) => ( ! [V4x:$i] : (mem(V4x,A_27a) => ( ! [V5t2:$i] : (mem(V5t2,ty_2Esptree_2Espt(A_27a)) => (ap(c_2Esptree_2Emk__wf(A_27a),ap(ap(ap(c_2Esptree_2EBS(A_27a),V3t1),V4x),V5t2)) = ap(ap(ap(c_2Esptree_2Emk__BS(A_27a),ap(c_2Esptree_2Emk__wf(A_27a),V3t1)),V4x),ap(c_2Esptree_2Emk__wf(A_27a),V5t2)))))))))))))).
tff(conj_thm_2Esptree_2Ewf__mk__wf,lemma,(( ! [A_27a:del]: ( ! [V0t:$i] : (mem(V0t,ty_2Esptree_2Espt(A_27a)) => p(ap(c_2Esptree_2Ewf(A_27a),ap(c_2Esptree_2Emk__wf(A_27a),V0t)))))))).
tff(conj_thm_2Esptree_2Ewf__mk__id,lemma,(( ! [A_27a:del]: ( ! [V0t:$i] : (mem(V0t,ty_2Esptree_2Espt(A_27a)) => (p(ap(c_2Esptree_2Ewf(A_27a),V0t)) => (ap(c_2Esptree_2Emk__wf(A_27a),V0t) = V0t))))))).
tff(conj_thm_2Esptree_2Elookup__mk__wf,lemma,(( ! [A_27a:del]: ( ! [V0x:tp__ty_2Enum_2Enum] : ( ! [V1t:$i] : (mem(V1t,ty_2Esptree_2Espt(A_27a)) => (ap(ap(c_2Esptree_2Elookup(A_27a),inj__ty_2Enum_2Enum(V0x)),ap(c_2Esptree_2Emk__wf(A_27a),V1t)) = ap(ap(c_2Esptree_2Elookup(A_27a),inj__ty_2Enum_2Enum(V0x)),V1t)))))))).
tff(conj_thm_2Esptree_2Edomain__mk__wf,lemma,(( ! [A_27a:del]: ( ! [V0t:$i] : (mem(V0t,ty_2Esptree_2Espt(A_27a)) => (ap(c_2Esptree_2Edomain(A_27a),ap(c_2Esptree_2Emk__wf(A_27a),V0t)) = ap(c_2Esptree_2Edomain(A_27a),V0t))))))).
tff(conj_thm_2Esptree_2Emk__wf__eq,conjecture,(( ! [A_27a:del]: ( ! [V0t1:$i] : (mem(V0t1,ty_2Esptree_2Espt(A_27a)) => ( ! [V1t2:$i] : (mem(V1t2,ty_2Esptree_2Espt(A_27a)) => ((ap(c_2Esptree_2Emk__wf(A_27a),V0t1) = ap(c_2Esptree_2Emk__wf(A_27a),V1t2)) <=> ( ! [V2x:tp__ty_2Enum_2Enum] : (ap(ap(c_2Esptree_2Elookup(A_27a),inj__ty_2Enum_2Enum(V2x)),V0t1) = ap(ap(c_2Esptree_2Elookup(A_27a),inj__ty_2Enum_2Enum(V2x)),V1t2))))))))))).
