include('Axioms/bft_2.ax').
tff(tp_ty_2Epath_2Epath,type,( ty_2Epath_2Epath: ( del * del ) > del )).
tff(tp_c_2Epath_2EPL,type,(c_2Epath_2EPL:(del * del) > $i)).
tff(mem_c_2Epath_2EPL,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Epath_2EPL(A_27a,A_27b),arr(ty_2Epath_2Epath(A_27a,A_27b),arr(ty_2Enum_2Enum,bool)))))).
tff(tp_c_2Epath_2ESN,type,(c_2Epath_2ESN:(del * del) > $i)).
tff(mem_c_2Epath_2ESN,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Epath_2ESN(A_27a,A_27b),arr(arr(A_27a,arr(A_27b,arr(A_27a,bool))),bool))))).
tff(tp_c_2Epath_2Edrop,type,(c_2Epath_2Edrop:(del * del) > $i)).
tff(mem_c_2Epath_2Edrop,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Epath_2Edrop(A_27a,A_27b),arr(ty_2Enum_2Enum,arr(ty_2Epath_2Epath(A_27a,A_27b),ty_2Epath_2Epath(A_27a,A_27b))))))).
tff(tp_c_2Epath_2Eel,type,(c_2Epath_2Eel:(del * del) > $i)).
tff(mem_c_2Epath_2Eel,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Epath_2Eel(A_27a,A_27b),arr(ty_2Enum_2Enum,arr(ty_2Epath_2Epath(A_27a,A_27b),A_27a)))))).
tff(tp_c_2Epath_2Eevery,type,(c_2Epath_2Eevery:(del * del) > $i)).
tff(mem_c_2Epath_2Eevery,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Epath_2Eevery(A_27a,A_27b),arr(arr(A_27a,bool),arr(ty_2Epath_2Epath(A_27a,A_27b),bool)))))).
tff(tp_c_2Epath_2Eexists,type,(c_2Epath_2Eexists:(del * del) > $i)).
tff(mem_c_2Epath_2Eexists,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Epath_2Eexists(A_27a,A_27b),arr(arr(A_27a,bool),arr(ty_2Epath_2Epath(A_27a,A_27b),bool)))))).
tff(tp_c_2Epath_2Efilter,type,(c_2Epath_2Efilter:(del * del) > $i)).
tff(mem_c_2Epath_2Efilter,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Epath_2Efilter(A_27a,A_27b),arr(arr(A_27a,bool),arr(ty_2Epath_2Epath(A_27a,A_27b),ty_2Epath_2Epath(A_27a,A_27b))))))).
tff(tp_c_2Epath_2Efinite,type,(c_2Epath_2Efinite:(del * del) > $i)).
tff(mem_c_2Epath_2Efinite,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Epath_2Efinite(A_27a,A_27b),arr(ty_2Epath_2Epath(A_27a,A_27b),bool))))).
tff(tp_c_2Epath_2Efirst,type,(c_2Epath_2Efirst:(del * del) > $i)).
tff(mem_c_2Epath_2Efirst,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Epath_2Efirst(A_27a,A_27b),arr(ty_2Epath_2Epath(A_27a,A_27b),A_27a))))).
tff(tp_c_2Epath_2EfirstP__at,type,(c_2Epath_2EfirstP__at:(del * del) > $i)).
tff(mem_c_2Epath_2EfirstP__at,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Epath_2EfirstP__at(A_27a,A_27b),arr(arr(A_27a,bool),arr(ty_2Epath_2Epath(A_27a,A_27b),arr(ty_2Enum_2Enum,bool))))))).
tff(tp_c_2Epath_2Efirst__label,type,(c_2Epath_2Efirst__label:(del * del) > $i)).
tff(mem_c_2Epath_2Efirst__label,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Epath_2Efirst__label(A_27a,A_27b),arr(ty_2Epath_2Epath(A_27a,A_27b),A_27b))))).
tff(tp_c_2Epath_2EfromPath,type,(c_2Epath_2EfromPath:(del * del) > $i)).
tff(mem_c_2Epath_2EfromPath,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Epath_2EfromPath(A_27a,A_27b),arr(ty_2Epath_2Epath(A_27a,A_27b),ty_2Epair_2Eprod(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a)))))))).
tff(tp_c_2Epath_2Eis__stopped,type,(c_2Epath_2Eis__stopped:(del * del) > $i)).
tff(mem_c_2Epath_2Eis__stopped,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Epath_2Eis__stopped(A_27a,A_27b),arr(ty_2Epath_2Epath(A_27a,A_27b),bool))))).
tff(tp_c_2Epath_2Elabels,type,(c_2Epath_2Elabels:(del * del) > $i)).
tff(mem_c_2Epath_2Elabels,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Epath_2Elabels(A_27a,A_27b),arr(ty_2Epath_2Epath(A_27a,A_27b),ty_2Ellist_2Ellist(A_27b)))))).
tff(tp_c_2Epath_2Elast,type,(c_2Epath_2Elast:(del * del) > $i)).
tff(mem_c_2Epath_2Elast,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Epath_2Elast(A_27a,A_27b),arr(ty_2Epath_2Epath(A_27a,A_27b),A_27a))))).
tff(tp_c_2Epath_2Elength,type,(c_2Epath_2Elength:(del * del) > $i)).
tff(mem_c_2Epath_2Elength,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Epath_2Elength(A_27a,A_27b),arr(ty_2Epath_2Epath(A_27a,A_27b),ty_2Eoption_2Eoption(ty_2Enum_2Enum)))))).
tff(tp_c_2Epath_2Emem,type,(c_2Epath_2Emem:(del * del) > $i)).
tff(mem_c_2Epath_2Emem,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Epath_2Emem(A_27a,A_27b),arr(A_27a,arr(ty_2Epath_2Epath(A_27a,A_27b),bool)))))).
tff(tp_c_2Epath_2Enth__label,type,(c_2Epath_2Enth__label:(del * del) > $i)).
tff(mem_c_2Epath_2Enth__label,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Epath_2Enth__label(A_27a,A_27b),arr(ty_2Enum_2Enum,arr(ty_2Epath_2Epath(A_27b,A_27a),A_27a)))))).
tff(tp_c_2Epath_2Eokpath,type,(c_2Epath_2Eokpath:(del * del) > $i)).
tff(mem_c_2Epath_2Eokpath,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Epath_2Eokpath(A_27a,A_27b),arr(arr(A_27a,arr(A_27b,arr(A_27a,bool))),arr(ty_2Epath_2Epath(A_27a,A_27b),bool)))))).
tff(tp_c_2Epath_2Eokpath__f,type,(c_2Epath_2Eokpath__f:(del * del) > $i)).
tff(mem_c_2Epath_2Eokpath__f,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Epath_2Eokpath__f(A_27a,A_27b),arr(arr(A_27a,arr(A_27b,arr(A_27a,bool))),arr(arr(ty_2Epath_2Epath(A_27a,A_27b),bool),arr(ty_2Epath_2Epath(A_27a,A_27b),bool))))))).
tff(tp_c_2Epath_2Eparallel__comp,type,(c_2Epath_2Eparallel__comp:(del * del * del * del * del) > $i)).
tff(mem_c_2Epath_2Eparallel__comp,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27c:del] : ( ! [A_27d:del] : ( ! [A_27e:del] : mem(c_2Epath_2Eparallel__comp(A_27a,A_27b,A_27c,A_27d,A_27e),arr(arr(A_27a,arr(A_27b,arr(A_27c,bool))),arr(arr(A_27d,arr(A_27b,arr(A_27e,bool))),arr(ty_2Epair_2Eprod(A_27a,A_27d),arr(A_27b,arr(ty_2Epair_2Eprod(A_27c,A_27e),bool)))))))))))).
tff(tp_c_2Epath_2Epconcat,type,(c_2Epath_2Epconcat:(del * del) > $i)).
tff(mem_c_2Epath_2Epconcat,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Epath_2Epconcat(A_27a,A_27b),arr(ty_2Epath_2Epath(A_27a,A_27b),arr(A_27b,arr(ty_2Epath_2Epath(A_27a,A_27b),ty_2Epath_2Epath(A_27a,A_27b)))))))).
tff(tp_c_2Epath_2Epcons,type,(c_2Epath_2Epcons:(del * del) > $i)).
tff(mem_c_2Epath_2Epcons,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Epath_2Epcons(A_27a,A_27b),arr(A_27a,arr(A_27b,arr(ty_2Epath_2Epath(A_27a,A_27b),ty_2Epath_2Epath(A_27a,A_27b)))))))).
tff(tp_c_2Epath_2Epgenerate,type,(c_2Epath_2Epgenerate:(del * del) > $i)).
tff(mem_c_2Epath_2Epgenerate,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Epath_2Epgenerate(A_27a,A_27b),arr(arr(ty_2Enum_2Enum,A_27a),arr(arr(ty_2Enum_2Enum,A_27b),ty_2Epath_2Epath(A_27a,A_27b))))))).
tff(tp_c_2Epath_2Eplink,type,(c_2Epath_2Eplink:(del * del) > $i)).
tff(mem_c_2Epath_2Eplink,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Epath_2Eplink(A_27a,A_27b),arr(ty_2Epath_2Epath(A_27a,A_27b),arr(ty_2Epath_2Epath(A_27a,A_27b),ty_2Epath_2Epath(A_27a,A_27b))))))).
tff(tp_c_2Epath_2Epmap,type,(c_2Epath_2Epmap:(del * del * del * del) > $i)).
tff(mem_c_2Epath_2Epmap,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27c:del] : ( ! [A_27d:del] : mem(c_2Epath_2Epmap(A_27a,A_27b,A_27c,A_27d),arr(arr(A_27a,A_27c),arr(arr(A_27b,A_27d),arr(ty_2Epath_2Epath(A_27a,A_27b),ty_2Epath_2Epath(A_27c,A_27d)))))))))).
tff(tp_c_2Epath_2Eseg,type,(c_2Epath_2Eseg:(del * del) > $i)).
tff(mem_c_2Epath_2Eseg,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Epath_2Eseg(A_27a,A_27b),arr(ty_2Enum_2Enum,arr(ty_2Enum_2Enum,arr(ty_2Epath_2Epath(A_27a,A_27b),ty_2Epath_2Epath(A_27a,A_27b)))))))).
tff(tp_c_2Epath_2Estopped__at,type,(c_2Epath_2Estopped__at:(del * del) > $i)).
tff(mem_c_2Epath_2Estopped__at,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Epath_2Estopped__at(A_27a,A_27b),arr(A_27a,ty_2Epath_2Epath(A_27a,A_27b)))))).
tff(tp_c_2Epath_2Etail,type,(c_2Epath_2Etail:(del * del) > $i)).
tff(mem_c_2Epath_2Etail,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Epath_2Etail(A_27a,A_27b),arr(ty_2Epath_2Epath(A_27a,A_27b),ty_2Epath_2Epath(A_27a,A_27b)))))).
tff(tp_c_2Epath_2Etake,type,(c_2Epath_2Etake:(del * del) > $i)).
tff(mem_c_2Epath_2Etake,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Epath_2Etake(A_27a,A_27b),arr(ty_2Enum_2Enum,arr(ty_2Epath_2Epath(A_27a,A_27b),ty_2Epath_2Epath(A_27a,A_27b))))))).
tff(tp_c_2Epath_2EtoPath,type,(c_2Epath_2EtoPath:(del * del) > $i)).
tff(mem_c_2Epath_2EtoPath,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : mem(c_2Epath_2EtoPath(A_27a,A_27b),arr(ty_2Epair_2Eprod(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a))),ty_2Epath_2Epath(A_27a,A_27b)))))).
tff(tp_c_2Epath_2Etrace__machine,type,(c_2Epath_2Etrace__machine:del > $i)).
tff(mem_c_2Epath_2Etrace__machine,axiom,( ! [A_27a:del] : mem(c_2Epath_2Etrace__machine(A_27a),arr(arr(ty_2Elist_2Elist(A_27a),bool),arr(ty_2Elist_2Elist(A_27a),arr(A_27a,arr(ty_2Elist_2Elist(A_27a),bool))))))).
tff(tp_c_2Epath_2Eunfold,type,(c_2Epath_2Eunfold:(del * del * del) > $i)).
tff(mem_c_2Epath_2Eunfold,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : ( ! [A_27c:del] : mem(c_2Epath_2Eunfold(A_27a,A_27b,A_27c),arr(arr(A_27c,A_27a),arr(arr(A_27c,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27c,A_27b))),arr(A_27c,ty_2Epath_2Epath(A_27a,A_27b))))))))).
tff(ax_thm_2Epath_2Epath__TY__DEF,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (? [V0rep:$i] : (mem(V0rep,arr(ty_2Epath_2Epath(A_27a,A_27b),ty_2Epair_2Eprod(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a))))) & p(ap(ap(c_2Ebool_2ETYPE__DEFINITION(ty_2Epair_2Eprod(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a))),ty_2Epath_2Epath(A_27a,A_27b)),k(ty_2Epair_2Eprod(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a))),c_2Ebool_2ET)),V0rep))))))).
tff(ax_thm_2Epath_2Epath__absrep__bijections,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0a:$i] : (mem(V0a,ty_2Epath_2Epath(A_27a,A_27b)) => (ap(c_2Epath_2EtoPath(A_27a,A_27b),ap(c_2Epath_2EfromPath(A_27a,A_27b),V0a)) = V0a))) & ( ! [V1r:$i] : (mem(V1r,ty_2Epair_2Eprod(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a)))) => (p(ap(k(ty_2Epair_2Eprod(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a))),c_2Ebool_2ET),V1r)) <=> (ap(c_2Epath_2EfromPath(A_27a,A_27b),ap(c_2Epath_2EtoPath(A_27a,A_27b),V1r)) = V1r)))))))).
tff(conj_thm_2Epath_2Epath__rep__bijections__thm,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0a:$i] : (mem(V0a,ty_2Epath_2Epath(A_27a,A_27b)) => (ap(c_2Epath_2EtoPath(A_27a,A_27b),ap(c_2Epath_2EfromPath(A_27a,A_27b),V0a)) = V0a))) & ( ! [V1r:$i] : (mem(V1r,ty_2Epair_2Eprod(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a)))) => (ap(c_2Epath_2EfromPath(A_27a,A_27b),ap(c_2Epath_2EtoPath(A_27a,A_27b),V1r)) = V1r)))))))).
tff(conj_thm_2Epath_2EtoPath__11,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0r:$i] : (mem(V0r,ty_2Epair_2Eprod(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a)))) => ( ! [V1r_27:$i] : (mem(V1r_27,ty_2Epair_2Eprod(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a)))) => ((ap(c_2Epath_2EtoPath(A_27a,A_27b),V0r) = ap(c_2Epath_2EtoPath(A_27a,A_27b),V1r_27)) <=> (V0r = V1r_27)))))))))).
tff(conj_thm_2Epath_2EfromPath__11,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Epath_2Epath(A_27a,A_27b)) => ( ! [V1a_27:$i] : (mem(V1a_27,ty_2Epath_2Epath(A_27a,A_27b)) => ((ap(c_2Epath_2EfromPath(A_27a,A_27b),V0a) = ap(c_2Epath_2EfromPath(A_27a,A_27b),V1a_27)) <=> (V0a = V1a_27)))))))))).
tff(conj_thm_2Epath_2EfromPath__onto,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0r:$i] : (mem(V0r,ty_2Epair_2Eprod(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a)))) => (? [V1a:$i] : (mem(V1a,ty_2Epath_2Epath(A_27a,A_27b)) & (V0r = ap(c_2Epath_2EfromPath(A_27a,A_27b),V1a)))))))))).
tff(conj_thm_2Epath_2EtoPath__onto,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0a:$i] : (mem(V0a,ty_2Epath_2Epath(A_27a,A_27b)) => (? [V1r:$i] : (mem(V1r,ty_2Epair_2Eprod(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a)))) & (V0a = ap(c_2Epath_2EtoPath(A_27a,A_27b),V1r)))))))))).
tff(ax_thm_2Epath_2Efirst__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0p:$i] : (mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => (ap(c_2Epath_2Efirst(A_27a,A_27b),V0p) = ap(c_2Epair_2EFST(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a))),ap(c_2Epath_2EfromPath(A_27a,A_27b),V0p)))))))).
tff(ax_thm_2Epath_2Estopped__at__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => (ap(c_2Epath_2Estopped__at(A_27a,A_27b),V0x) = ap(c_2Epath_2EtoPath(A_27a,A_27b),ap(ap(c_2Epair_2E_2C(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a))),V0x),c_2Ellist_2ELNIL(ty_2Epair_2Eprod(A_27b,A_27a)))))))))).
tff(ax_thm_2Epath_2Epcons__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1r:$i] : (mem(V1r,A_27b) => ( ! [V2p:$i] : (mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => (ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V0x),V1r),V2p) = ap(c_2Epath_2EtoPath(A_27a,A_27b),ap(ap(c_2Epair_2E_2C(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a))),V0x),ap(ap(c_2Ellist_2ELCONS(ty_2Epair_2Eprod(A_27b,A_27a)),ap(ap(c_2Epair_2E_2C(A_27b,A_27a),V1r),ap(c_2Epath_2Efirst(A_27a,A_27b),V2p))),ap(c_2Epair_2ESND(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a))),ap(c_2Epath_2EfromPath(A_27a,A_27b),V2p))))))))))))))).
tff(conj_thm_2Epath_2Estopped__at__11,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1y:$i] : (mem(V1y,A_27a) => ((ap(c_2Epath_2Estopped__at(A_27a,A_27b),V0x) = ap(c_2Epath_2Estopped__at(A_27a,A_27b),V1y)) <=> (V0x = V1y)))))))))).
tff(conj_thm_2Epath_2Epcons__11,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1r:$i] : (mem(V1r,A_27b) => ( ! [V2p:$i] : (mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ! [V3y:$i] : (mem(V3y,A_27a) => ( ! [V4s:$i] : (mem(V4s,A_27b) => ( ! [V5q:$i] : (mem(V5q,ty_2Epath_2Epath(A_27a,A_27b)) => ((ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V0x),V1r),V2p) = ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V3y),V4s),V5q)) <=> ((V0x = V3y) & ((V1r = V4s) & (V2p = V5q)))))))))))))))))))).
tff(conj_thm_2Epath_2Estopped__at__not__pcons,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1y:$i] : (mem(V1y,A_27a) => ( ! [V2r:$i] : (mem(V2r,A_27b) => ( ! [V3p:$i] : (mem(V3p,ty_2Epath_2Epath(A_27a,A_27b)) => ((~~ (ap(c_2Epath_2Estopped__at(A_27a,A_27b),V0x) = ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V1y),V2r),V3p))) & (~~ (ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V1y),V2r),V3p) = ap(c_2Epath_2Estopped__at(A_27a,A_27b),V0x)))))))))))))))).
tff(conj_thm_2Epath_2Epath__cases,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0p:$i] : (mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => ((? [V1x:$i] : (mem(V1x,A_27a) & (V0p = ap(c_2Epath_2Estopped__at(A_27a,A_27b),V1x)))) | (? [V2x:$i] : (mem(V2x,A_27a) & (? [V3r:$i] : (mem(V3r,A_27b) & (? [V4q:$i] : (mem(V4q,ty_2Epath_2Epath(A_27a,A_27b)) & (V0p = ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V2x),V3r),V4q))))))))))))))).
tff(conj_thm_2Epath_2EFORALL__path,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Epath_2Epath(A_27a,A_27b),bool)) => (( ! [V1p:$i] : (mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) => p(ap(V0P,V1p)))) <=> (( ! [V2x:$i] : (mem(V2x,A_27a) => p(ap(V0P,ap(c_2Epath_2Estopped__at(A_27a,A_27b),V2x))))) & ( ! [V3x:$i] : (mem(V3x,A_27a) => ( ! [V4r:$i] : (mem(V4r,A_27b) => ( ! [V5p:$i] : (mem(V5p,ty_2Epath_2Epath(A_27a,A_27b)) => p(ap(V0P,ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V3x),V4r),V5p))))))))))))))))).
tff(conj_thm_2Epath_2EEXISTS__path,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Epath_2Epath(A_27a,A_27b),bool)) => ((? [V1p:$i] : (mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) & p(ap(V0P,V1p)))) <=> ((? [V2x:$i] : (mem(V2x,A_27a) & p(ap(V0P,ap(c_2Epath_2Estopped__at(A_27a,A_27b),V2x))))) | (? [V3x:$i] : (mem(V3x,A_27a) & (? [V4r:$i] : (mem(V4r,A_27b) & (? [V5p:$i] : (mem(V5p,ty_2Epath_2Epath(A_27a,A_27b)) & p(ap(V0P,ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V3x),V4r),V5p))))))))))))))))).
tff(conj_thm_2Epath_2Efirst__thm,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0x:$i] : (mem(V0x,A_27a) => (ap(c_2Epath_2Efirst(A_27a,A_27b),ap(c_2Epath_2Estopped__at(A_27a,A_27b),V0x)) = V0x))) & ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2r:$i] : (mem(V2r,A_27b) => ( ! [V3p:$i] : (mem(V3p,ty_2Epath_2Epath(A_27a,A_27b)) => (ap(c_2Epath_2Efirst(A_27a,A_27b),ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V1x),V2r),V3p)) = V1x)))))))))))).
tff(ax_thm_2Epath_2Efinite__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0sigma:$i] : (mem(V0sigma,ty_2Epath_2Epath(A_27a,A_27b)) => (p(ap(c_2Epath_2Efinite(A_27a,A_27b),V0sigma)) <=> p(ap(c_2Ellist_2ELFINITE(ty_2Epair_2Eprod(A_27b,A_27a)),ap(c_2Epair_2ESND(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a))),ap(c_2Epath_2EfromPath(A_27a,A_27b),V0sigma)))))))))).
tff(conj_thm_2Epath_2Efinite__thm,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0x:$i] : (mem(V0x,A_27a) => (p(ap(c_2Epath_2Efinite(A_27a,A_27b),ap(c_2Epath_2Estopped__at(A_27a,A_27b),V0x))) <=> $true))) & ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2r:$i] : (mem(V2r,A_27b) => ( ! [V3p:$i] : (mem(V3p,ty_2Epath_2Epath(A_27a,A_27b)) => (p(ap(c_2Epath_2Efinite(A_27a,A_27b),ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V1x),V2r),V3p))) <=> p(ap(c_2Epath_2Efinite(A_27a,A_27b),V3p)))))))))))))).
tff(ax_thm_2Epath_2Elast__thm,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0x:$i] : (mem(V0x,A_27a) => (ap(c_2Epath_2Elast(A_27a,A_27b),ap(c_2Epath_2Estopped__at(A_27a,A_27b),V0x)) = V0x))) & ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2r:$i] : (mem(V2r,A_27b) => ( ! [V3p:$i] : (mem(V3p,ty_2Epath_2Epath(A_27a,A_27b)) => (ap(c_2Epath_2Elast(A_27a,A_27b),ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V1x),V2r),V3p)) = ap(c_2Epath_2Elast(A_27a,A_27b),V3p)))))))))))).
tff(conj_thm_2Epath_2Epath__bisimulation,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0p1:$i] : (mem(V0p1,ty_2Epath_2Epath(A_27a,A_27b)) => ( ! [V1p2:$i] : (mem(V1p2,ty_2Epath_2Epath(A_27a,A_27b)) => ((V0p1 = V1p2) <=> (? [V2R:$i] : (mem(V2R,arr(ty_2Epath_2Epath(A_27a,A_27b),arr(ty_2Epath_2Epath(A_27a,A_27b),bool))) & (p(ap(ap(V2R,V0p1),V1p2)) & ( ! [V3q1:$i] : (mem(V3q1,ty_2Epath_2Epath(A_27a,A_27b)) => ( ! [V4q2:$i] : (mem(V4q2,ty_2Epath_2Epath(A_27a,A_27b)) => (p(ap(ap(V2R,V3q1),V4q2)) => ((? [V5x:$i] : (mem(V5x,A_27a) & ((V3q1 = ap(c_2Epath_2Estopped__at(A_27a,A_27b),V5x)) & (V4q2 = ap(c_2Epath_2Estopped__at(A_27a,A_27b),V5x))))) | (? [V6x:$i] : (mem(V6x,A_27a) & (? [V7r:$i] : (mem(V7r,A_27b) & (? [V8q1_27:$i] : (mem(V8q1_27,ty_2Epath_2Epath(A_27a,A_27b)) & (? [V9q2_27:$i] : (mem(V9q2_27,ty_2Epath_2Epath(A_27a,A_27b)) & ((V3q1 = ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V6x),V7r),V8q1_27)) & ((V4q2 = ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V6x),V7r),V9q2_27)) & p(ap(ap(V2R,V8q1_27),V9q2_27)))))))))))))))))))))))))))))).
tff(conj_thm_2Epath_2Efinite__path__ind,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Epath_2Epath(A_27a,A_27b),bool)) => ((( ! [V1x:$i] : (mem(V1x,A_27a) => p(ap(V0P,ap(c_2Epath_2Estopped__at(A_27a,A_27b),V1x))))) & ( ! [V2x:$i] : (mem(V2x,A_27a) => ( ! [V3r:$i] : (mem(V3r,A_27b) => ( ! [V4p:$i] : (mem(V4p,ty_2Epath_2Epath(A_27a,A_27b)) => ((p(ap(c_2Epath_2Efinite(A_27a,A_27b),V4p)) & p(ap(V0P,V4p))) => p(ap(V0P,ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V2x),V3r),V4p))))))))))) => ( ! [V5q:$i] : (mem(V5q,ty_2Epath_2Epath(A_27a,A_27b)) => (p(ap(c_2Epath_2Efinite(A_27a,A_27b),V5q)) => p(ap(V0P,V5q)))))))))))).
tff(ax_thm_2Epath_2Epmap__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27c)) => ( ! [V1g:$i] : (mem(V1g,arr(A_27b,A_27d)) => ( ! [V2p:$i] : (mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => (ap(ap(ap(c_2Epath_2Epmap(A_27a,A_27b,A_27c,A_27d),V0f),V1g),V2p) = ap(c_2Epath_2EtoPath(A_27c,A_27d),ap(ap(ap(c_2Epair_2E_23_23(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a)),A_27c,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27d,A_27c))),V0f),ap(c_2Ellist_2ELMAP(ty_2Epair_2Eprod(A_27b,A_27a),ty_2Epair_2Eprod(A_27d,A_27c)),ap(ap(c_2Epair_2E_23_23(A_27b,A_27a,A_27d,A_27c),V1g),V0f))),ap(c_2Epath_2EfromPath(A_27a,A_27b),V2p))))))))))))))).
tff(conj_thm_2Epath_2Epmap__thm,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27b)) => ( ! [V1g:$i] : (mem(V1g,arr(A_27d,A_27c)) => (( ! [V2x:$i] : (mem(V2x,A_27a) => (ap(ap(ap(c_2Epath_2Epmap(A_27a,A_27d,A_27b,A_27c),V0f),V1g),ap(c_2Epath_2Estopped__at(A_27a,A_27d),V2x)) = ap(c_2Epath_2Estopped__at(A_27b,A_27c),ap(V0f,V2x))))) & ( ! [V3x:$i] : (mem(V3x,A_27a) => ( ! [V4r:$i] : (mem(V4r,A_27d) => ( ! [V5p:$i] : (mem(V5p,ty_2Epath_2Epath(A_27a,A_27d)) => (ap(ap(ap(c_2Epath_2Epmap(A_27a,A_27d,A_27b,A_27c),V0f),V1g),ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27d),V3x),V4r),V5p)) = ap(ap(ap(c_2Epath_2Epcons(A_27b,A_27c),ap(V0f,V3x)),ap(V1g,V4r)),ap(ap(ap(c_2Epath_2Epmap(A_27a,A_27d,A_27b,A_27c),V0f),V1g),V5p)))))))))))))))))))).
tff(conj_thm_2Epath_2Efirst__pmap,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27c)) => ( ! [V1g:$i] : (mem(V1g,arr(A_27b,A_27d)) => ( ! [V2p:$i] : (mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => (ap(c_2Epath_2Efirst(A_27c,A_27d),ap(ap(ap(c_2Epath_2Epmap(A_27a,A_27b,A_27c,A_27d),V0f),V1g),V2p)) = ap(V0f,ap(c_2Epath_2Efirst(A_27a,A_27b),V2p))))))))))))))).
tff(conj_thm_2Epath_2Elast__pmap,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27c)) => ( ! [V1g:$i] : (mem(V1g,arr(A_27b,A_27d)) => ( ! [V2p:$i] : (mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => (p(ap(c_2Epath_2Efinite(A_27a,A_27b),V2p)) => (ap(c_2Epath_2Elast(A_27c,A_27d),ap(ap(ap(c_2Epath_2Epmap(A_27a,A_27b,A_27c,A_27d),V0f),V1g),V2p)) = ap(V0f,ap(c_2Epath_2Elast(A_27a,A_27b),V2p)))))))))))))))).
tff(conj_thm_2Epath_2Efinite__pmap,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27c)) => ( ! [V1g:$i] : (mem(V1g,arr(A_27b,A_27d)) => ( ! [V2p:$i] : (mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => (p(ap(c_2Epath_2Efinite(A_27c,A_27d),ap(ap(ap(c_2Epath_2Epmap(A_27a,A_27b,A_27c,A_27d),V0f),V1g),V2p))) <=> p(ap(c_2Epath_2Efinite(A_27a,A_27b),V2p))))))))))))))).
tff(ax_thm_2Epath_2Etail__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1r:$i] : (mem(V1r,A_27b) => ( ! [V2p:$i] : (mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => (ap(c_2Epath_2Etail(A_27a,A_27b),ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V0x),V1r),V2p)) = V2p)))))))))).
tff(ax_thm_2Epath_2Efirst__label__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1r:$i] : (mem(V1r,A_27b) => ( ! [V2p:$i] : (mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => (ap(c_2Epath_2Efirst__label(A_27a,A_27b),ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V0x),V1r),V2p)) = V1r)))))))))).
tff(ax_thm_2Epath_2Elength__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0p:$i] : (mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => (surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum(ap(c_2Epath_2Elength(A_27a,A_27b),V0p)) = surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum(ap(ap(ap(c_2Ebool_2ECOND(ty_2Eoption_2Eoption(ty_2Enum_2Enum)),ap(c_2Epath_2Efinite(A_27a,A_27b),V0p)),ap(c_2Eoption_2ESOME(ty_2Enum_2Enum),ap(ap(c_2Earithmetic_2E_2B,ap(c_2Elist_2ELENGTH(ty_2Epair_2Eprod(A_27b,A_27a)),ap(c_2Eoption_2ETHE(ty_2Elist_2Elist(ty_2Epair_2Eprod(A_27b,A_27a))),ap(c_2Ellist_2EtoList(ty_2Epair_2Eprod(A_27b,A_27a)),ap(c_2Epair_2ESND(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a))),ap(c_2Epath_2EfromPath(A_27a,A_27b),V0p)))))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),c_2Eoption_2ENONE(ty_2Enum_2Enum))))))))).
tff(conj_thm_2Epath_2Elength__thm,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: (( ! [V0x:$i] : (mem(V0x,A_27a) => (surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum(ap(c_2Epath_2Elength(A_27a,A_27b),ap(c_2Epath_2Estopped__at(A_27a,A_27b),V0x))) = surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum(ap(c_2Eoption_2ESOME(ty_2Enum_2Enum),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))) & ( ! [V1x:$i] : (mem(V1x,A_27c) => ( ! [V2r:$i] : (mem(V2r,A_27d) => ( ! [V3p:$i] : (mem(V3p,ty_2Epath_2Epath(A_27c,A_27d)) => (surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum(ap(c_2Epath_2Elength(A_27c,A_27d),ap(ap(ap(c_2Epath_2Epcons(A_27c,A_27d),V1x),V2r),V3p))) = surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum(ap(ap(ap(c_2Ebool_2ECOND(ty_2Eoption_2Eoption(ty_2Enum_2Enum)),ap(c_2Epath_2Efinite(A_27c,A_27d),V3p)),ap(c_2Eoption_2ESOME(ty_2Enum_2Enum),ap(ap(c_2Earithmetic_2E_2B,ap(c_2Eoption_2ETHE(ty_2Enum_2Enum),ap(c_2Epath_2Elength(A_27c,A_27d),V3p))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))),c_2Eoption_2ENONE(ty_2Enum_2Enum))))))))))))))))).
tff(conj_thm_2Epath_2Ealt__length__thm,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: (( ! [V0x:$i] : (mem(V0x,A_27a) => (surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum(ap(c_2Epath_2Elength(A_27a,A_27b),ap(c_2Epath_2Estopped__at(A_27a,A_27b),V0x))) = surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum(ap(c_2Eoption_2ESOME(ty_2Enum_2Enum),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))) & ( ! [V1x:$i] : (mem(V1x,A_27c) => ( ! [V2r:$i] : (mem(V2r,A_27d) => ( ! [V3p:$i] : (mem(V3p,ty_2Epath_2Epath(A_27c,A_27d)) => (surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum(ap(c_2Epath_2Elength(A_27c,A_27d),ap(ap(ap(c_2Epath_2Epcons(A_27c,A_27d),V1x),V2r),V3p))) = surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum(ap(ap(c_2Eoption_2EOPTION__MAP(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Enum_2ESUC),ap(c_2Epath_2Elength(A_27c,A_27d),V3p))))))))))))))))).
tff(conj_thm_2Epath_2Elength__never__zero,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0p:$i] : (mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => (~~ (surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum(ap(c_2Epath_2Elength(A_27a,A_27b),V0p)) = surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum(ap(c_2Eoption_2ESOME(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))))))))))).
tff(conj_thm_2Epath_2Efinite__length,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0p:$i] : (mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => ((p(ap(c_2Epath_2Efinite(A_27a,A_27b),V0p)) <=> (? [V1n:tp__ty_2Enum_2Enum] : (surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum(ap(c_2Epath_2Elength(A_27a,A_27b),V0p)) = surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum(ap(c_2Eoption_2ESOME(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V1n)))))) & ((~~ p(ap(c_2Epath_2Efinite(A_27a,A_27b),V0p))) <=> (surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum(ap(c_2Epath_2Elength(A_27a,A_27b),V0p)) = surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum(c_2Eoption_2ENONE(ty_2Enum_2Enum))))))))))).
tff(conj_thm_2Epath_2Elength__pmap,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27b)) => ( ! [V1g:$i] : (mem(V1g,arr(A_27c,A_27d)) => ( ! [V2p:$i] : (mem(V2p,ty_2Epath_2Epath(A_27a,A_27c)) => (surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum(ap(c_2Epath_2Elength(A_27b,A_27d),ap(ap(ap(c_2Epath_2Epmap(A_27a,A_27c,A_27b,A_27d),V0f),V1g),V2p))) = surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum(ap(c_2Epath_2Elength(A_27a,A_27c),V2p))))))))))))))).
tff(ax_thm_2Epath_2Eel__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0p:$i] : (mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => (ap(ap(c_2Epath_2Eel(A_27a,A_27b),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),V0p) = ap(c_2Epath_2Efirst(A_27a,A_27b),V0p)))) & ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:$i] : (mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => (ap(ap(c_2Epath_2Eel(A_27a,A_27b),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1n))),V2p) = ap(ap(c_2Epath_2Eel(A_27a,A_27b),inj__ty_2Enum_2Enum(V1n)),ap(c_2Epath_2Etail(A_27a,A_27b),V2p)))))))))).
tff(conj_thm_2Epath_2Eel__def__compute,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0p:$i] : (mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => (ap(ap(c_2Epath_2Eel(A_27a,A_27b),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),V0p) = ap(c_2Epath_2Efirst(A_27a,A_27b),V0p)))) & (( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:$i] : (mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => (ap(ap(c_2Epath_2Eel(A_27a,A_27b),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1n)))),V2p) = ap(ap(c_2Epath_2Eel(A_27a,A_27b),ap(ap(c_2Earithmetic_2E_2D,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1n)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Epath_2Etail(A_27a,A_27b),V2p)))))) & ( ! [V3n:tp__ty_2Enum_2Enum] : ( ! [V4p:$i] : (mem(V4p,ty_2Epath_2Epath(A_27a,A_27b)) => (ap(ap(c_2Epath_2Eel(A_27a,A_27b),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V3n)))),V4p) = ap(ap(c_2Epath_2Eel(A_27a,A_27b),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V3n)))),ap(c_2Epath_2Etail(A_27a,A_27b),V4p)))))))))))).
tff(ax_thm_2Epath_2Enth__label__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0p:$i] : (mem(V0p,ty_2Epath_2Epath(A_27b,A_27a)) => (ap(ap(c_2Epath_2Enth__label(A_27a,A_27b),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),V0p) = ap(c_2Epath_2Efirst__label(A_27b,A_27a),V0p)))) & ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:$i] : (mem(V2p,ty_2Epath_2Epath(A_27b,A_27a)) => (ap(ap(c_2Epath_2Enth__label(A_27a,A_27b),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1n))),V2p) = ap(ap(c_2Epath_2Enth__label(A_27a,A_27b),inj__ty_2Enum_2Enum(V1n)),ap(c_2Epath_2Etail(A_27b,A_27a),V2p)))))))))).
tff(conj_thm_2Epath_2Enth__label__def__compute,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0p:$i] : (mem(V0p,ty_2Epath_2Epath(A_27b,A_27a)) => (ap(ap(c_2Epath_2Enth__label(A_27a,A_27b),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),V0p) = ap(c_2Epath_2Efirst__label(A_27b,A_27a),V0p)))) & (( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:$i] : (mem(V2p,ty_2Epath_2Epath(A_27b,A_27a)) => (ap(ap(c_2Epath_2Enth__label(A_27a,A_27b),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1n)))),V2p) = ap(ap(c_2Epath_2Enth__label(A_27a,A_27b),ap(ap(c_2Earithmetic_2E_2D,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1n)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Epath_2Etail(A_27b,A_27a),V2p)))))) & ( ! [V3n:tp__ty_2Enum_2Enum] : ( ! [V4p:$i] : (mem(V4p,ty_2Epath_2Epath(A_27b,A_27a)) => (ap(ap(c_2Epath_2Enth__label(A_27a,A_27b),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V3n)))),V4p) = ap(ap(c_2Epath_2Enth__label(A_27a,A_27b),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V3n)))),ap(c_2Epath_2Etail(A_27b,A_27a),V4p)))))))))))).
tff(conj_thm_2Epath_2Epath__Axiom,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,ty_2Epair_2Eprod(A_27b,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27c,A_27a))))) => (? [V1g:$i] : (mem(V1g,arr(A_27a,ty_2Epath_2Epath(A_27b,A_27c))) & ( ! [V2x:$i] : (mem(V2x,A_27a) => (ap(V1g,V2x) = ap(ap(c_2Epair_2Epair__CASE(ty_2Epath_2Epath(A_27b,A_27c),A_27b,ty_2Eoption_2Eoption(ty_2Epair_2Eprod(A_27c,A_27a))),ap(V0f,V2x)),f1683(A_27a,A_27b,A_27c,V1g)))))))))))))).
tff(ax_thm_2Epath_2Epconcat__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0p1:$i] : (mem(V0p1,ty_2Epath_2Epath(A_27a,A_27b)) => ( ! [V1lab:$i] : (mem(V1lab,A_27b) => ( ! [V2p2:$i] : (mem(V2p2,ty_2Epath_2Epath(A_27a,A_27b)) => (ap(ap(ap(c_2Epath_2Epconcat(A_27a,A_27b),V0p1),V1lab),V2p2) = ap(c_2Epath_2EtoPath(A_27a,A_27b),ap(ap(c_2Epair_2E_2C(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a))),ap(c_2Epath_2Efirst(A_27a,A_27b),V0p1)),ap(ap(c_2Ellist_2ELAPPEND(ty_2Epair_2Eprod(A_27b,A_27a)),ap(c_2Epair_2ESND(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a))),ap(c_2Epath_2EfromPath(A_27a,A_27b),V0p1))),ap(ap(c_2Ellist_2ELCONS(ty_2Epair_2Eprod(A_27b,A_27a)),ap(ap(c_2Epair_2E_2C(A_27b,A_27a),V1lab),ap(c_2Epath_2Efirst(A_27a,A_27b),V2p2))),ap(c_2Epair_2ESND(A_27a,ty_2Ellist_2Ellist(ty_2Epair_2Eprod(A_27b,A_27a))),ap(c_2Epath_2EfromPath(A_27a,A_27b),V2p2)))))))))))))))).
tff(conj_thm_2Epath_2Epconcat__thm,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: (( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1lab:$i] : (mem(V1lab,A_27b) => ( ! [V2p2:$i] : (mem(V2p2,ty_2Epath_2Epath(A_27a,A_27b)) => (ap(ap(ap(c_2Epath_2Epconcat(A_27a,A_27b),ap(c_2Epath_2Estopped__at(A_27a,A_27b),V0x)),V1lab),V2p2) = ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V0x),V1lab),V2p2)))))))) & ( ! [V3x:$i] : (mem(V3x,A_27c) => ( ! [V4r:$i] : (mem(V4r,A_27d) => ( ! [V5p:$i] : (mem(V5p,ty_2Epath_2Epath(A_27c,A_27d)) => ( ! [V6lab:$i] : (mem(V6lab,A_27d) => ( ! [V7p2:$i] : (mem(V7p2,ty_2Epath_2Epath(A_27c,A_27d)) => (ap(ap(ap(c_2Epath_2Epconcat(A_27c,A_27d),ap(ap(ap(c_2Epath_2Epcons(A_27c,A_27d),V3x),V4r),V5p)),V6lab),V7p2) = ap(ap(ap(c_2Epath_2Epcons(A_27c,A_27d),V3x),V4r),ap(ap(ap(c_2Epath_2Epconcat(A_27c,A_27d),V5p),V6lab),V7p2)))))))))))))))))))).
tff(conj_thm_2Epath_2Epconcat__eq__stopped,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0p1:$i] : (mem(V0p1,ty_2Epath_2Epath(A_27a,A_27b)) => ( ! [V1lab:$i] : (mem(V1lab,A_27b) => ( ! [V2p2:$i] : (mem(V2p2,ty_2Epath_2Epath(A_27a,A_27b)) => ( ! [V3x:$i] : (mem(V3x,A_27a) => ((~~ (ap(ap(ap(c_2Epath_2Epconcat(A_27a,A_27b),V0p1),V1lab),V2p2) = ap(c_2Epath_2Estopped__at(A_27a,A_27b),V3x))) & (~~ (ap(c_2Epath_2Estopped__at(A_27a,A_27b),V3x) = ap(ap(ap(c_2Epath_2Epconcat(A_27a,A_27b),V0p1),V1lab),V2p2)))))))))))))))).
tff(conj_thm_2Epath_2Epconcat__eq__pcons,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1r:$i] : (mem(V1r,A_27b) => ( ! [V2p:$i] : (mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ! [V3p1:$i] : (mem(V3p1,ty_2Epath_2Epath(A_27a,A_27b)) => ( ! [V4lab:$i] : (mem(V4lab,A_27b) => ( ! [V5p2:$i] : (mem(V5p2,ty_2Epath_2Epath(A_27a,A_27b)) => (((ap(ap(ap(c_2Epath_2Epconcat(A_27a,A_27b),V3p1),V4lab),V5p2) = ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V0x),V1r),V2p)) <=> (((V4lab = V1r) & ((V3p1 = ap(c_2Epath_2Estopped__at(A_27a,A_27b),V0x)) & (V2p = V5p2))) | (? [V6p1_27:$i] : (mem(V6p1_27,ty_2Epath_2Epath(A_27a,A_27b)) & ((V3p1 = ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V0x),V1r),V6p1_27)) & (V2p = ap(ap(ap(c_2Epath_2Epconcat(A_27a,A_27b),V6p1_27),V4lab),V5p2))))))) & ((ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V0x),V1r),V2p) = ap(ap(ap(c_2Epath_2Epconcat(A_27a,A_27b),V3p1),V4lab),V5p2)) <=> (((V4lab = V1r) & ((V3p1 = ap(c_2Epath_2Estopped__at(A_27a,A_27b),V0x)) & (V2p = V5p2))) | (? [V7p1_27:$i] : (mem(V7p1_27,ty_2Epath_2Epath(A_27a,A_27b)) & ((V3p1 = ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V0x),V1r),V7p1_27)) & (V2p = ap(ap(ap(c_2Epath_2Epconcat(A_27a,A_27b),V7p1_27),V4lab),V5p2)))))))))))))))))))))))).
tff(conj_thm_2Epath_2Efinite__pconcat,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0p1:$i] : (mem(V0p1,ty_2Epath_2Epath(A_27a,A_27b)) => ( ! [V1lab:$i] : (mem(V1lab,A_27b) => ( ! [V2p2:$i] : (mem(V2p2,ty_2Epath_2Epath(A_27a,A_27b)) => (p(ap(c_2Epath_2Efinite(A_27a,A_27b),ap(ap(ap(c_2Epath_2Epconcat(A_27a,A_27b),V0p1),V1lab),V2p2))) <=> (p(ap(c_2Epath_2Efinite(A_27a,A_27b),V0p1)) & p(ap(c_2Epath_2Efinite(A_27a,A_27b),V2p2)))))))))))))).
tff(ax_thm_2Epath_2EPL__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0p:$i] : (mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => (ap(c_2Epath_2EPL(A_27a,A_27b),V0p) = ap(c_2Epred__set_2EGSPEC(ty_2Enum_2Enum,ty_2Enum_2Enum),f1684(A_27b,A_27a,V0p)))))))).
tff(conj_thm_2Epath_2Einfinite__PL,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0p:$i] : (mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => ((~~ p(ap(c_2Epath_2Efinite(A_27a,A_27b),V0p))) => ( ! [V1i:tp__ty_2Enum_2Enum] : p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V1i)),ap(c_2Epath_2EPL(A_27a,A_27b),V0p))))))))))).
tff(conj_thm_2Epath_2EPL__pcons,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1r:$i] : (mem(V1r,A_27b) => ( ! [V2q:$i] : (mem(V2q,ty_2Epath_2Epath(A_27a,A_27b)) => (ap(c_2Epath_2EPL(A_27a,A_27b),ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V0x),V1r),V2q)) = ap(ap(c_2Epred__set_2EINSERT(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Enum_2ESUC),ap(c_2Epath_2EPL(A_27a,A_27b),V2q)))))))))))))).
tff(conj_thm_2Epath_2EPL__stopped__at,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : (mem(V0x,A_27a) => (ap(c_2Epath_2EPL(A_27a,A_27b),ap(c_2Epath_2Estopped__at(A_27a,A_27b),V0x)) = ap(ap(c_2Epred__set_2EINSERT(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),c_2Epred__set_2EEMPTY(ty_2Enum_2Enum))))))))).
tff(conj_thm_2Epath_2EPL__thm,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0x:$i] : (mem(V0x,A_27a) => (ap(c_2Epath_2EPL(A_27a,A_27b),ap(c_2Epath_2Estopped__at(A_27a,A_27b),V0x)) = ap(ap(c_2Epred__set_2EINSERT(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),c_2Epred__set_2EEMPTY(ty_2Enum_2Enum))))) & ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2r:$i] : (mem(V2r,A_27b) => ( ! [V3q:$i] : (mem(V3q,ty_2Epath_2Epath(A_27a,A_27b)) => (ap(c_2Epath_2EPL(A_27a,A_27b),ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V1x),V2r),V3q)) = ap(ap(c_2Epred__set_2EINSERT(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Enum_2ESUC),ap(c_2Epath_2EPL(A_27a,A_27b),V3q))))))))))))))).
tff(conj_thm_2Epath_2EPL__0,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0p:$i] : (mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(c_2Epath_2EPL(A_27a,A_27b),V0p))))))))).
tff(conj_thm_2Epath_2EPL__downward__closed,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:tp__ty_2Enum_2Enum] : ( ! [V1p:$i] : (mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) => (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V0i)),ap(c_2Epath_2EPL(A_27a,A_27b),V1p))) => ( ! [V2j:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V2j)),inj__ty_2Enum_2Enum(V0i))) => p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V2j)),ap(c_2Epath_2EPL(A_27a,A_27b),V1p))))))))))))).
tff(conj_thm_2Epath_2EPL__pmap,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27c,A_27a)) => ( ! [V1g:$i] : (mem(V1g,arr(A_27d,A_27b)) => ( ! [V2p:$i] : (mem(V2p,ty_2Epath_2Epath(A_27c,A_27d)) => (ap(c_2Epath_2EPL(A_27a,A_27b),ap(ap(ap(c_2Epath_2Epmap(A_27c,A_27d,A_27a,A_27b),V0f),V1g),V2p)) = ap(c_2Epath_2EPL(A_27c,A_27d),V2p)))))))))))))).
tff(conj_thm_2Epath_2Eel__pmap,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27c)) => ( ! [V1g:$i] : (mem(V1g,arr(A_27b,A_27d)) => ( ! [V2i:tp__ty_2Enum_2Enum] : ( ! [V3p:$i] : (mem(V3p,ty_2Epath_2Epath(A_27a,A_27b)) => (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V2i)),ap(c_2Epath_2EPL(A_27a,A_27b),V3p))) => (ap(ap(c_2Epath_2Eel(A_27c,A_27d),inj__ty_2Enum_2Enum(V2i)),ap(ap(ap(c_2Epath_2Epmap(A_27a,A_27b,A_27c,A_27d),V0f),V1g),V3p)) = ap(V0f,ap(ap(c_2Epath_2Eel(A_27a,A_27b),inj__ty_2Enum_2Enum(V2i)),V3p))))))))))))))))).
tff(conj_thm_2Epath_2Enth__label__pmap,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [V0f:$i] : (mem(V0f,arr(A_27a,A_27d)) => ( ! [V1g:$i] : (mem(V1g,arr(A_27b,A_27c)) => ( ! [V2i:tp__ty_2Enum_2Enum] : ( ! [V3p:$i] : (mem(V3p,ty_2Epath_2Epath(A_27a,A_27b)) => (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V2i))),ap(c_2Epath_2EPL(A_27a,A_27b),V3p))) => (ap(ap(c_2Epath_2Enth__label(A_27c,A_27d),inj__ty_2Enum_2Enum(V2i)),ap(ap(ap(c_2Epath_2Epmap(A_27a,A_27b,A_27d,A_27c),V0f),V1g),V3p)) = ap(V1g,ap(ap(c_2Epath_2Enth__label(A_27b,A_27a),inj__ty_2Enum_2Enum(V2i)),V3p))))))))))))))))).
tff(ax_thm_2Epath_2EfirstP__at__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1p:$i] : (mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ! [V2i:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2Epath_2EfirstP__at(A_27a,A_27b),V0P),V1p),inj__ty_2Enum_2Enum(V2i))) <=> (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V2i)),ap(c_2Epath_2EPL(A_27a,A_27b),V1p))) & (p(ap(V0P,ap(ap(c_2Epath_2Eel(A_27a,A_27b),inj__ty_2Enum_2Enum(V2i)),V1p))) & ( ! [V3j:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V3j)),inj__ty_2Enum_2Enum(V2i))) => (~~ p(ap(V0P,ap(ap(c_2Epath_2Eel(A_27a,A_27b),inj__ty_2Enum_2Enum(V3j)),V1p))))))))))))))))).
tff(conj_thm_2Epath_2EfirstP__at__thm,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2n:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2Epath_2EfirstP__at(A_27a,A_27b),V0P),ap(c_2Epath_2Estopped__at(A_27a,A_27b),V1x)),inj__ty_2Enum_2Enum(V2n))) <=> ((V2n = fo__c_2Enum_2E0) & p(ap(V0P,V1x))))))))) & ( ! [V3P:$i] : (mem(V3P,arr(A_27a,bool)) => ( ! [V4n:tp__ty_2Enum_2Enum] : ( ! [V5x:$i] : (mem(V5x,A_27a) => ( ! [V6r:$i] : (mem(V6r,A_27b) => ( ! [V7p:$i] : (mem(V7p,ty_2Epath_2Epath(A_27a,A_27b)) => (p(ap(ap(ap(c_2Epath_2EfirstP__at(A_27a,A_27b),V3P),ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V5x),V6r),V7p)),inj__ty_2Enum_2Enum(V4n))) <=> (((V4n = fo__c_2Enum_2E0) & p(ap(V3P,V5x))) | (p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(V4n))) & ((~~ p(ap(V3P,V5x))) & p(ap(ap(ap(c_2Epath_2EfirstP__at(A_27a,A_27b),V3P),V7p),ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V4n)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))))))))))))))))))))))).
tff(conj_thm_2Epath_2EfirstP__at__zero,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1p:$i] : (mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) => (p(ap(ap(ap(c_2Epath_2EfirstP__at(A_27a,A_27b),V0P),V1p),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) <=> p(ap(V0P,ap(c_2Epath_2Efirst(A_27a,A_27b),V1p)))))))))))).
tff(ax_thm_2Epath_2Eexists__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1p:$i] : (mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) => (p(ap(ap(c_2Epath_2Eexists(A_27a,A_27b),V0P),V1p)) <=> (? [V2i:tp__ty_2Enum_2Enum] : p(ap(ap(ap(c_2Epath_2EfirstP__at(A_27a,A_27b),V0P),V1p),inj__ty_2Enum_2Enum(V2i)))))))))))).
tff(ax_thm_2Epath_2Eevery__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1p:$i] : (mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) => (p(ap(ap(c_2Epath_2Eevery(A_27a,A_27b),V0P),V1p)) <=> (~~ p(ap(ap(c_2Epath_2Eexists(A_27a,A_27b),ap(ap(c_2Ecombin_2Eo(A_27a,bool,bool),c_2Ebool_2E_7E),V0P)),V1p))))))))))).
tff(conj_thm_2Epath_2Eexists__thm,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => (( ! [V1x:$i] : (mem(V1x,A_27a) => (p(ap(ap(c_2Epath_2Eexists(A_27a,A_27b),V0P),ap(c_2Epath_2Estopped__at(A_27a,A_27b),V1x))) <=> p(ap(V0P,V1x))))) & ( ! [V2x:$i] : (mem(V2x,A_27a) => ( ! [V3r:$i] : (mem(V3r,A_27c) => ( ! [V4p:$i] : (mem(V4p,ty_2Epath_2Epath(A_27a,A_27c)) => (p(ap(ap(c_2Epath_2Eexists(A_27a,A_27c),V0P),ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27c),V2x),V3r),V4p))) <=> (p(ap(V0P,V2x)) | p(ap(ap(c_2Epath_2Eexists(A_27a,A_27c),V0P),V4p)))))))))))))))))).
tff(conj_thm_2Epath_2Eevery__thm,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => (( ! [V1x:$i] : (mem(V1x,A_27a) => (p(ap(ap(c_2Epath_2Eevery(A_27a,A_27b),V0P),ap(c_2Epath_2Estopped__at(A_27a,A_27b),V1x))) <=> p(ap(V0P,V1x))))) & ( ! [V2x:$i] : (mem(V2x,A_27a) => ( ! [V3r:$i] : (mem(V3r,A_27c) => ( ! [V4p:$i] : (mem(V4p,ty_2Epath_2Epath(A_27a,A_27c)) => (p(ap(ap(c_2Epath_2Eevery(A_27a,A_27c),V0P),ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27c),V2x),V3r),V4p))) <=> (p(ap(V0P,V2x)) & p(ap(ap(c_2Epath_2Eevery(A_27a,A_27c),V0P),V4p)))))))))))))))))).
tff(conj_thm_2Epath_2Enot__every,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1p:$i] : (mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) => ((~~ p(ap(ap(c_2Epath_2Eevery(A_27a,A_27b),V0P),V1p))) <=> p(ap(ap(c_2Epath_2Eexists(A_27a,A_27b),ap(ap(c_2Ecombin_2Eo(A_27a,bool,bool),c_2Ebool_2E_7E),V0P)),V1p))))))))))).
tff(conj_thm_2Epath_2Enot__exists,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1p:$i] : (mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) => ((~~ p(ap(ap(c_2Epath_2Eexists(A_27a,A_27b),V0P),V1p))) <=> p(ap(ap(c_2Epath_2Eevery(A_27a,A_27b),ap(ap(c_2Ecombin_2Eo(A_27a,bool,bool),c_2Ebool_2E_7E),V0P)),V1p))))))))))).
tff(conj_thm_2Epath_2Eexists__el,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1p:$i] : (mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) => (p(ap(ap(c_2Epath_2Eexists(A_27a,A_27b),V0P),V1p)) <=> (? [V2i:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V2i)),ap(c_2Epath_2EPL(A_27a,A_27b),V1p))) & p(ap(V0P,ap(ap(c_2Epath_2Eel(A_27a,A_27b),inj__ty_2Enum_2Enum(V2i)),V1p)))))))))))))).
tff(conj_thm_2Epath_2Eevery__el,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1p:$i] : (mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) => (p(ap(ap(c_2Epath_2Eevery(A_27a,A_27b),V0P),V1p)) <=> ( ! [V2i:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V2i)),ap(c_2Epath_2EPL(A_27a,A_27b),V1p))) => p(ap(V0P,ap(ap(c_2Epath_2Eel(A_27a,A_27b),inj__ty_2Enum_2Enum(V2i)),V1p)))))))))))))).
tff(conj_thm_2Epath_2Eevery__coinduction,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(ty_2Epath_2Epath(A_27a,A_27b),bool)) => ( ! [V1Q:$i] : (mem(V1Q,arr(A_27a,bool)) => ((( ! [V2x:$i] : (mem(V2x,A_27a) => (p(ap(V0P,ap(c_2Epath_2Estopped__at(A_27a,A_27b),V2x))) => p(ap(V1Q,V2x))))) & ( ! [V3x:$i] : (mem(V3x,A_27a) => ( ! [V4r:$i] : (mem(V4r,A_27b) => ( ! [V5p:$i] : (mem(V5p,ty_2Epath_2Epath(A_27a,A_27b)) => (p(ap(V0P,ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V3x),V4r),V5p))) => (p(ap(V1Q,V3x)) & p(ap(V0P,V5p))))))))))) => ( ! [V6p:$i] : (mem(V6p,ty_2Epath_2Epath(A_27a,A_27b)) => (p(ap(V0P,V6p)) => p(ap(ap(c_2Epath_2Eevery(A_27a,A_27b),V1Q),V6p)))))))))))))).
tff(conj_thm_2Epath_2Eexists__induction,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0Q:$i] : (mem(V0Q,arr(A_27a,bool)) => ( ! [V1P:$i] : (mem(V1P,arr(ty_2Epath_2Epath(A_27a,A_27b),bool)) => ((( ! [V2x:$i] : (mem(V2x,A_27a) => (p(ap(V0Q,V2x)) => p(ap(V1P,ap(c_2Epath_2Estopped__at(A_27a,A_27b),V2x)))))) & (( ! [V3x:$i] : (mem(V3x,A_27a) => ( ! [V4r:$i] : (mem(V4r,A_27b) => ( ! [V5p:$i] : (mem(V5p,ty_2Epath_2Epath(A_27a,A_27b)) => (p(ap(V0Q,V3x)) => p(ap(V1P,ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V3x),V4r),V5p)))))))))) & ( ! [V6x:$i] : (mem(V6x,A_27a) => ( ! [V7r:$i] : (mem(V7r,A_27b) => ( ! [V8p:$i] : (mem(V8p,ty_2Epath_2Epath(A_27a,A_27b)) => (p(ap(V1P,V8p)) => p(ap(V1P,ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V6x),V7r),V8p)))))))))))) => ( ! [V9p:$i] : (mem(V9p,ty_2Epath_2Epath(A_27a,A_27b)) => (p(ap(ap(c_2Epath_2Eexists(A_27a,A_27b),V0Q),V9p)) => p(ap(V1P,V9p)))))))))))))).
tff(ax_thm_2Epath_2Emem__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : (mem(V0s,A_27a) => ( ! [V1p:$i] : (mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) => (p(ap(ap(c_2Epath_2Emem(A_27a,A_27b),V0s),V1p)) <=> (? [V2i:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V2i)),ap(c_2Epath_2EPL(A_27a,A_27b),V1p))) & (V0s = ap(ap(c_2Epath_2Eel(A_27a,A_27b),inj__ty_2Enum_2Enum(V2i)),V1p)))))))))))).
tff(conj_thm_2Epath_2Emem__thm,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: (( ! [V0x:$i] : (mem(V0x,A_27a) => ( ! [V1s:$i] : (mem(V1s,A_27a) => (p(ap(ap(c_2Epath_2Emem(A_27a,A_27b),V1s),ap(c_2Epath_2Estopped__at(A_27a,A_27b),V0x))) <=> (V1s = V0x)))))) & ( ! [V2x:$i] : (mem(V2x,A_27c) => ( ! [V3r:$i] : (mem(V3r,A_27d) => ( ! [V4p:$i] : (mem(V4p,ty_2Epath_2Epath(A_27c,A_27d)) => ( ! [V5s:$i] : (mem(V5s,A_27c) => (p(ap(ap(c_2Epath_2Emem(A_27c,A_27d),V5s),ap(ap(ap(c_2Epath_2Epcons(A_27c,A_27d),V2x),V3r),V4p))) <=> ((V5s = V2x) | p(ap(ap(c_2Epath_2Emem(A_27c,A_27d),V5s),V4p))))))))))))))))))).
tff(ax_thm_2Epath_2Edrop__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0p:$i] : (mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => (ap(ap(c_2Epath_2Edrop(A_27a,A_27b),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),V0p) = V0p))) & ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:$i] : (mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => (ap(ap(c_2Epath_2Edrop(A_27a,A_27b),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1n))),V2p) = ap(ap(c_2Epath_2Edrop(A_27a,A_27b),inj__ty_2Enum_2Enum(V1n)),ap(c_2Epath_2Etail(A_27a,A_27b),V2p)))))))))).
tff(conj_thm_2Epath_2Edrop__def__compute,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0p:$i] : (mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => (ap(ap(c_2Epath_2Edrop(A_27a,A_27b),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),V0p) = V0p))) & (( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:$i] : (mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => (ap(ap(c_2Epath_2Edrop(A_27a,A_27b),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1n)))),V2p) = ap(ap(c_2Epath_2Edrop(A_27a,A_27b),ap(ap(c_2Earithmetic_2E_2D,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1n)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Epath_2Etail(A_27a,A_27b),V2p)))))) & ( ! [V3n:tp__ty_2Enum_2Enum] : ( ! [V4p:$i] : (mem(V4p,ty_2Epath_2Epath(A_27a,A_27b)) => (ap(ap(c_2Epath_2Edrop(A_27a,A_27b),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V3n)))),V4p) = ap(ap(c_2Epath_2Edrop(A_27a,A_27b),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V3n)))),ap(c_2Epath_2Etail(A_27a,A_27b),V4p)))))))))))).
tff(conj_thm_2Epath_2Enumeral__drop,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1p:$i] : (mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) => (ap(ap(c_2Epath_2Edrop(A_27a,A_27b),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n)))),V1p) = ap(ap(c_2Epath_2Edrop(A_27a,A_27b),ap(ap(c_2Earithmetic_2E_2D,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V0n)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Epath_2Etail(A_27a,A_27b),V1p)))))) & ( ! [V2n:tp__ty_2Enum_2Enum] : ( ! [V3p:$i] : (mem(V3p,ty_2Epath_2Epath(A_27a,A_27b)) => (ap(ap(c_2Epath_2Edrop(A_27a,A_27b),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V2n)))),V3p) = ap(ap(c_2Epath_2Edrop(A_27a,A_27b),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V2n)))),ap(c_2Epath_2Etail(A_27a,A_27b),V3p))))))))))).
tff(conj_thm_2Epath_2Efinite__drop,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0p:$i] : (mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V1n)),ap(c_2Epath_2EPL(A_27a,A_27b),V0p))) => (p(ap(c_2Epath_2Efinite(A_27a,A_27b),ap(ap(c_2Epath_2Edrop(A_27a,A_27b),inj__ty_2Enum_2Enum(V1n)),V0p))) <=> p(ap(c_2Epath_2Efinite(A_27a,A_27b),V0p))))))))))).
tff(conj_thm_2Epath_2Elength__drop,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0p:$i] : (mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ! [V1n:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V1n)),ap(c_2Epath_2EPL(A_27a,A_27b),V0p))) => (surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum(ap(c_2Epath_2Elength(A_27a,A_27b),ap(ap(c_2Epath_2Edrop(A_27a,A_27b),inj__ty_2Enum_2Enum(V1n)),V0p))) = surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum(ap(ap(ap(c_2Eoption_2Eoption__CASE(ty_2Enum_2Enum,ty_2Eoption_2Eoption(ty_2Enum_2Enum)),ap(c_2Epath_2Elength(A_27a,A_27b),V0p)),c_2Eoption_2ENONE(ty_2Enum_2Enum)),f1685(V1n)))))))))))).
tff(conj_thm_2Epath_2EPL__drop,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0p:$i] : (mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ! [V1i:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V1i)),ap(c_2Epath_2EPL(A_27a,A_27b),V0p))) => (ap(c_2Epath_2EPL(A_27a,A_27b),ap(ap(c_2Epath_2Edrop(A_27a,A_27b),inj__ty_2Enum_2Enum(V1i)),V0p)) = ap(ap(c_2Epred__set_2EIMAGE(ty_2Enum_2Enum,ty_2Enum_2Enum),f1686(V1i)),ap(c_2Epath_2EPL(A_27a,A_27b),V0p))))))))))).
tff(conj_thm_2Epath_2EIN__PL__drop,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:tp__ty_2Enum_2Enum] : ( ! [V1j:tp__ty_2Enum_2Enum] : ( ! [V2p:$i] : (mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V0i)),ap(c_2Epath_2EPL(A_27a,A_27b),V2p))) => (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V1j)),ap(c_2Epath_2EPL(A_27a,A_27b),ap(ap(c_2Epath_2Edrop(A_27a,A_27b),inj__ty_2Enum_2Enum(V0i)),V2p)))) <=> p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0i)),inj__ty_2Enum_2Enum(V1j))),ap(c_2Epath_2EPL(A_27a,A_27b),V2p))))))))))))).
tff(conj_thm_2Epath_2Efirst__drop,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:tp__ty_2Enum_2Enum] : ( ! [V1p:$i] : (mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) => (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V0i)),ap(c_2Epath_2EPL(A_27a,A_27b),V1p))) => (ap(c_2Epath_2Efirst(A_27a,A_27b),ap(ap(c_2Epath_2Edrop(A_27a,A_27b),inj__ty_2Enum_2Enum(V0i)),V1p)) = ap(ap(c_2Epath_2Eel(A_27a,A_27b),inj__ty_2Enum_2Enum(V0i)),V1p)))))))))).
tff(conj_thm_2Epath_2Efirst__label__drop,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:tp__ty_2Enum_2Enum] : ( ! [V1p:$i] : (mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) => (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V0i)),ap(c_2Epath_2EPL(A_27a,A_27b),V1p))) => (ap(c_2Epath_2Efirst__label(A_27a,A_27b),ap(ap(c_2Epath_2Edrop(A_27a,A_27b),inj__ty_2Enum_2Enum(V0i)),V1p)) = ap(ap(c_2Epath_2Enth__label(A_27b,A_27a),inj__ty_2Enum_2Enum(V0i)),V1p)))))))))).
tff(conj_thm_2Epath_2Etail__drop,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:tp__ty_2Enum_2Enum] : ( ! [V1p:$i] : (mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) => (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0i)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Epath_2EPL(A_27a,A_27b),V1p))) => (ap(c_2Epath_2Etail(A_27a,A_27b),ap(ap(c_2Epath_2Edrop(A_27a,A_27b),inj__ty_2Enum_2Enum(V0i)),V1p)) = ap(ap(c_2Epath_2Edrop(A_27a,A_27b),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0i)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),V1p)))))))))).
tff(conj_thm_2Epath_2Eel__drop,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:tp__ty_2Enum_2Enum] : ( ! [V1j:tp__ty_2Enum_2Enum] : ( ! [V2p:$i] : (mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0i)),inj__ty_2Enum_2Enum(V1j))),ap(c_2Epath_2EPL(A_27a,A_27b),V2p))) => (ap(ap(c_2Epath_2Eel(A_27a,A_27b),inj__ty_2Enum_2Enum(V0i)),ap(ap(c_2Epath_2Edrop(A_27a,A_27b),inj__ty_2Enum_2Enum(V1j)),V2p)) = ap(ap(c_2Epath_2Eel(A_27a,A_27b),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0i)),inj__ty_2Enum_2Enum(V1j))),V2p))))))))))).
tff(conj_thm_2Epath_2Enth__label__drop,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:tp__ty_2Enum_2Enum] : ( ! [V1j:tp__ty_2Enum_2Enum] : ( ! [V2p:$i] : (mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0i)),inj__ty_2Enum_2Enum(V1j)))),ap(c_2Epath_2EPL(A_27a,A_27b),V2p))) => (ap(ap(c_2Epath_2Enth__label(A_27b,A_27a),inj__ty_2Enum_2Enum(V0i)),ap(ap(c_2Epath_2Edrop(A_27a,A_27b),inj__ty_2Enum_2Enum(V1j)),V2p)) = ap(ap(c_2Epath_2Enth__label(A_27b,A_27a),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0i)),inj__ty_2Enum_2Enum(V1j))),V2p))))))))))).
tff(ax_thm_2Epath_2Etake__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0p:$i] : (mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => (ap(ap(c_2Epath_2Etake(A_27a,A_27b),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),V0p) = ap(c_2Epath_2Estopped__at(A_27a,A_27b),ap(c_2Epath_2Efirst(A_27a,A_27b),V0p))))) & ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:$i] : (mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => (ap(ap(c_2Epath_2Etake(A_27a,A_27b),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(V1n))),V2p) = ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),ap(c_2Epath_2Efirst(A_27a,A_27b),V2p)),ap(c_2Epath_2Efirst__label(A_27a,A_27b),V2p)),ap(ap(c_2Epath_2Etake(A_27a,A_27b),inj__ty_2Enum_2Enum(V1n)),ap(c_2Epath_2Etail(A_27a,A_27b),V2p))))))))))).
tff(conj_thm_2Epath_2Etake__def__compute,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0p:$i] : (mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => (ap(ap(c_2Epath_2Etake(A_27a,A_27b),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),V0p) = ap(c_2Epath_2Estopped__at(A_27a,A_27b),ap(c_2Epath_2Efirst(A_27a,A_27b),V0p))))) & (( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2p:$i] : (mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => (ap(ap(c_2Epath_2Etake(A_27a,A_27b),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1n)))),V2p) = ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),ap(c_2Epath_2Efirst(A_27a,A_27b),V2p)),ap(c_2Epath_2Efirst__label(A_27a,A_27b),V2p)),ap(ap(c_2Epath_2Etake(A_27a,A_27b),ap(ap(c_2Earithmetic_2E_2D,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V1n)))),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),ap(c_2Epath_2Etail(A_27a,A_27b),V2p))))))) & ( ! [V3n:tp__ty_2Enum_2Enum] : ( ! [V4p:$i] : (mem(V4p,ty_2Epath_2Epath(A_27a,A_27b)) => (ap(ap(c_2Epath_2Etake(A_27a,A_27b),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(V3n)))),V4p) = ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),ap(c_2Epath_2Efirst(A_27a,A_27b),V4p)),ap(c_2Epath_2Efirst__label(A_27a,A_27b),V4p)),ap(ap(c_2Epath_2Etake(A_27a,A_27b),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(V3n)))),ap(c_2Epath_2Etail(A_27a,A_27b),V4p))))))))))))).
tff(conj_thm_2Epath_2Efirst__take,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0p:$i] : (mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ! [V1i:tp__ty_2Enum_2Enum] : (ap(c_2Epath_2Efirst(A_27a,A_27b),ap(ap(c_2Epath_2Etake(A_27a,A_27b),inj__ty_2Enum_2Enum(V1i)),V0p)) = ap(c_2Epath_2Efirst(A_27a,A_27b),V0p))))))))).
tff(conj_thm_2Epath_2Efinite__take,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0p:$i] : (mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ! [V1i:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V1i)),ap(c_2Epath_2EPL(A_27a,A_27b),V0p))) => p(ap(c_2Epath_2Efinite(A_27a,A_27b),ap(ap(c_2Epath_2Etake(A_27a,A_27b),inj__ty_2Enum_2Enum(V1i)),V0p))))))))))).
tff(conj_thm_2Epath_2Elength__take,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0p:$i] : (mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ! [V1i:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V1i)),ap(c_2Epath_2EPL(A_27a,A_27b),V0p))) => (surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum(ap(c_2Epath_2Elength(A_27a,A_27b),ap(ap(c_2Epath_2Etake(A_27a,A_27b),inj__ty_2Enum_2Enum(V1i)),V0p))) = surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum(ap(c_2Eoption_2ESOME(ty_2Enum_2Enum),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V1i)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))))))))))))).
tff(conj_thm_2Epath_2EPL__take,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0p:$i] : (mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ! [V1i:tp__ty_2Enum_2Enum] : (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V1i)),ap(c_2Epath_2EPL(A_27a,A_27b),V0p))) => (ap(c_2Epath_2EPL(A_27a,A_27b),ap(ap(c_2Epath_2Etake(A_27a,A_27b),inj__ty_2Enum_2Enum(V1i)),V0p)) = ap(c_2Epred__set_2EGSPEC(ty_2Enum_2Enum,ty_2Enum_2Enum),f1687(V1i))))))))))).
tff(conj_thm_2Epath_2Elast__take,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:tp__ty_2Enum_2Enum] : ( ! [V1p:$i] : (mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) => (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V0i)),ap(c_2Epath_2EPL(A_27a,A_27b),V1p))) => (ap(c_2Epath_2Elast(A_27a,A_27b),ap(ap(c_2Epath_2Etake(A_27a,A_27b),inj__ty_2Enum_2Enum(V0i)),V1p)) = ap(ap(c_2Epath_2Eel(A_27a,A_27b),inj__ty_2Enum_2Enum(V0i)),V1p)))))))))).
tff(conj_thm_2Epath_2Enth__label__take,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1p:$i] : (mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ! [V2i:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V2i)),inj__ty_2Enum_2Enum(V0n))) & p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V0n)),ap(c_2Epath_2EPL(A_27a,A_27b),V1p)))) => (ap(ap(c_2Epath_2Enth__label(A_27b,A_27a),inj__ty_2Enum_2Enum(V2i)),ap(ap(c_2Epath_2Etake(A_27a,A_27b),inj__ty_2Enum_2Enum(V0n)),V1p)) = ap(ap(c_2Epath_2Enth__label(A_27b,A_27a),inj__ty_2Enum_2Enum(V2i)),V1p))))))))))).
tff(ax_thm_2Epath_2Eseg__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:tp__ty_2Enum_2Enum] : ( ! [V1j:tp__ty_2Enum_2Enum] : ( ! [V2p:$i] : (mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => (ap(ap(ap(c_2Epath_2Eseg(A_27a,A_27b),inj__ty_2Enum_2Enum(V0i)),inj__ty_2Enum_2Enum(V1j)),V2p) = ap(ap(c_2Epath_2Etake(A_27a,A_27b),ap(ap(c_2Earithmetic_2E_2D,inj__ty_2Enum_2Enum(V1j)),inj__ty_2Enum_2Enum(V0i))),ap(ap(c_2Epath_2Edrop(A_27a,A_27b),inj__ty_2Enum_2Enum(V0i)),V2p)))))))))).
tff(conj_thm_2Epath_2Esingleton__seg,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:tp__ty_2Enum_2Enum] : ( ! [V1p:$i] : (mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) => (p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V0i)),ap(c_2Epath_2EPL(A_27a,A_27b),V1p))) => (ap(ap(ap(c_2Epath_2Eseg(A_27a,A_27b),inj__ty_2Enum_2Enum(V0i)),inj__ty_2Enum_2Enum(V0i)),V1p) = ap(c_2Epath_2Estopped__at(A_27a,A_27b),ap(ap(c_2Epath_2Eel(A_27a,A_27b),inj__ty_2Enum_2Enum(V0i)),V1p))))))))))).
tff(conj_thm_2Epath_2Erecursive__seg,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:tp__ty_2Enum_2Enum] : ( ! [V1j:tp__ty_2Enum_2Enum] : ( ! [V2p:$i] : (mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => ((p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(V0i)),inj__ty_2Enum_2Enum(V1j))) & p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V1j)),ap(c_2Epath_2EPL(A_27a,A_27b),V2p)))) => (ap(ap(ap(c_2Epath_2Eseg(A_27a,A_27b),inj__ty_2Enum_2Enum(V0i)),inj__ty_2Enum_2Enum(V1j)),V2p) = ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),ap(ap(c_2Epath_2Eel(A_27a,A_27b),inj__ty_2Enum_2Enum(V0i)),V2p)),ap(ap(c_2Epath_2Enth__label(A_27b,A_27a),inj__ty_2Enum_2Enum(V0i)),V2p)),ap(ap(ap(c_2Epath_2Eseg(A_27a,A_27b),ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(V0i)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),inj__ty_2Enum_2Enum(V1j)),V2p)))))))))))).
tff(conj_thm_2Epath_2EPL__seg,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:tp__ty_2Enum_2Enum] : ( ! [V1j:tp__ty_2Enum_2Enum] : ( ! [V2p:$i] : (mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => ((p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0i)),inj__ty_2Enum_2Enum(V1j))) & p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V1j)),ap(c_2Epath_2EPL(A_27a,A_27b),V2p)))) => (ap(c_2Epath_2EPL(A_27a,A_27b),ap(ap(ap(c_2Epath_2Eseg(A_27a,A_27b),inj__ty_2Enum_2Enum(V0i)),inj__ty_2Enum_2Enum(V1j)),V2p)) = ap(c_2Epred__set_2EGSPEC(ty_2Enum_2Enum,ty_2Enum_2Enum),f1688(V1j,V0i)))))))))))).
tff(conj_thm_2Epath_2Efinite__seg,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0p:$i] : (mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ! [V1i:tp__ty_2Enum_2Enum] : ( ! [V2j:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V1i)),inj__ty_2Enum_2Enum(V2j))) & p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V2j)),ap(c_2Epath_2EPL(A_27a,A_27b),V0p)))) => p(ap(c_2Epath_2Efinite(A_27a,A_27b),ap(ap(ap(c_2Epath_2Eseg(A_27a,A_27b),inj__ty_2Enum_2Enum(V1i)),inj__ty_2Enum_2Enum(V2j)),V0p)))))))))))).
tff(conj_thm_2Epath_2Efirst__seg,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:tp__ty_2Enum_2Enum] : ( ! [V1j:tp__ty_2Enum_2Enum] : ( ! [V2p:$i] : (mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => ((p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0i)),inj__ty_2Enum_2Enum(V1j))) & p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V1j)),ap(c_2Epath_2EPL(A_27a,A_27b),V2p)))) => (ap(c_2Epath_2Efirst(A_27a,A_27b),ap(ap(ap(c_2Epath_2Eseg(A_27a,A_27b),inj__ty_2Enum_2Enum(V0i)),inj__ty_2Enum_2Enum(V1j)),V2p)) = ap(ap(c_2Epath_2Eel(A_27a,A_27b),inj__ty_2Enum_2Enum(V0i)),V2p))))))))))).
tff(conj_thm_2Epath_2Elast__seg,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0i:tp__ty_2Enum_2Enum] : ( ! [V1j:tp__ty_2Enum_2Enum] : ( ! [V2p:$i] : (mem(V2p,ty_2Epath_2Epath(A_27a,A_27b)) => ((p(ap(ap(c_2Earithmetic_2E_3C_3D,inj__ty_2Enum_2Enum(V0i)),inj__ty_2Enum_2Enum(V1j))) & p(ap(ap(c_2Ebool_2EIN(ty_2Enum_2Enum),inj__ty_2Enum_2Enum(V1j)),ap(c_2Epath_2EPL(A_27a,A_27b),V2p)))) => (ap(c_2Epath_2Elast(A_27a,A_27b),ap(ap(ap(c_2Epath_2Eseg(A_27a,A_27b),inj__ty_2Enum_2Enum(V0i)),inj__ty_2Enum_2Enum(V1j)),V2p)) = ap(ap(c_2Epath_2Eel(A_27a,A_27b),inj__ty_2Enum_2Enum(V1j)),V2p))))))))))).
tff(ax_thm_2Epath_2Elabels__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0x:$i] : (mem(V0x,A_27a) => (ap(c_2Epath_2Elabels(A_27a,A_27b),ap(c_2Epath_2Estopped__at(A_27a,A_27b),V0x)) = c_2Ellist_2ELNIL(A_27b)))) & ( ! [V1x:$i] : (mem(V1x,A_27a) => ( ! [V2r:$i] : (mem(V2r,A_27b) => ( ! [V3p:$i] : (mem(V3p,ty_2Epath_2Epath(A_27a,A_27b)) => (ap(c_2Epath_2Elabels(A_27a,A_27b),ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V1x),V2r),V3p)) = ap(ap(c_2Ellist_2ELCONS(A_27b),V2r),ap(c_2Epath_2Elabels(A_27a,A_27b),V3p))))))))))))).
tff(conj_thm_2Epath_2EfirstP__at__unique,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1p:$i] : (mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) => ( ! [V2n:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2Epath_2EfirstP__at(A_27a,A_27b),V0P),V1p),inj__ty_2Enum_2Enum(V2n))) => ( ! [V3m:tp__ty_2Enum_2Enum] : (p(ap(ap(ap(c_2Epath_2EfirstP__at(A_27a,A_27b),V0P),V1p),inj__ty_2Enum_2Enum(V3m))) <=> (V3m = V2n))))))))))))).
tff(ax_thm_2Epath_2Eis__stopped__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0p:$i] : (mem(V0p,ty_2Epath_2Epath(A_27a,A_27b)) => (p(ap(c_2Epath_2Eis__stopped(A_27a,A_27b),V0p)) <=> (? [V1x:$i] : (mem(V1x,A_27a) & (V0p = ap(c_2Epath_2Estopped__at(A_27a,A_27b),V1x)))))))))).
tff(conj_thm_2Epath_2Eis__stopped__thm,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: (( ! [V0x:$i] : (mem(V0x,A_27a) => (p(ap(c_2Epath_2Eis__stopped(A_27a,A_27b),ap(c_2Epath_2Estopped__at(A_27a,A_27b),V0x))) <=> $true))) & ( ! [V1x:$i] : (mem(V1x,A_27c) => ( ! [V2r:$i] : (mem(V2r,A_27d) => ( ! [V3p:$i] : (mem(V3p,ty_2Epath_2Epath(A_27c,A_27d)) => (p(ap(c_2Epath_2Eis__stopped(A_27c,A_27d),ap(ap(ap(c_2Epath_2Epcons(A_27c,A_27d),V1x),V2r),V3p))) <=> $false)))))))))))))).
tff(ax_thm_2Epath_2Efilter__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => (( ! [V1x:$i] : (mem(V1x,A_27a) => (p(ap(V0P,V1x)) => (ap(ap(c_2Epath_2Efilter(A_27a,A_27b),V0P),ap(c_2Epath_2Estopped__at(A_27a,A_27b),V1x)) = ap(c_2Epath_2Estopped__at(A_27a,A_27b),V1x))))) & ( ! [V2x:$i] : (mem(V2x,A_27a) => ( ! [V3r:$i] : (mem(V3r,A_27b) => ( ! [V4p:$i] : (mem(V4p,ty_2Epath_2Epath(A_27a,A_27b)) => (ap(ap(c_2Epath_2Efilter(A_27a,A_27b),V0P),ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V2x),V3r),V4p)) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Epath_2Epath(A_27a,A_27b)),ap(V0P,V2x)),ap(ap(ap(c_2Ebool_2ECOND(ty_2Epath_2Epath(A_27a,A_27b)),ap(ap(c_2Epath_2Eexists(A_27a,A_27b),V0P),V4p)),ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),V2x),V3r),ap(ap(c_2Epath_2Efilter(A_27a,A_27b),V0P),V4p))),ap(c_2Epath_2Estopped__at(A_27a,A_27b),V2x))),ap(ap(c_2Epath_2Efilter(A_27a,A_27b),V0P),V4p))))))))))))))).
tff(conj_thm_2Epath_2Efilter__every,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1p:$i] : (mem(V1p,ty_2Epath_2Epath(A_27a,A_27b)) => (p(ap(ap(c_2Epath_2Eexists(A_27a,A_27b),V0P),V1p)) => p(ap(ap(c_2Epath_2Eevery(A_27a,A_27b),V0P),ap(ap(c_2Epath_2Efilter(A_27a,A_27b),V0P),V1p)))))))))))).
tff(ax_thm_2Epath_2Epgenerate__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,arr(ty_2Enum_2Enum,A_27a)) => ( ! [V1g:$i] : (mem(V1g,arr(ty_2Enum_2Enum,A_27b)) => (ap(ap(c_2Epath_2Epgenerate(A_27a,A_27b),V0f),V1g) = ap(ap(ap(c_2Epath_2Epcons(A_27a,A_27b),ap(V0f,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(V1g,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),ap(ap(c_2Epath_2Epgenerate(A_27a,A_27b),ap(ap(c_2Ecombin_2Eo(ty_2Enum_2Enum,A_27a,ty_2Enum_2Enum),V0f),c_2Enum_2ESUC)),ap(ap(c_2Ecombin_2Eo(ty_2Enum_2Enum,A_27b,ty_2Enum_2Enum),V1g),c_2Enum_2ESUC))))))))))).
tff(conj_thm_2Epath_2Epgenerate__infinite,conjecture,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : (mem(V0f,arr(ty_2Enum_2Enum,A_27a)) => ( ! [V1g:$i] : (mem(V1g,arr(ty_2Enum_2Enum,A_27b)) => (~~ p(ap(c_2Epath_2Efinite(A_27a,A_27b),ap(ap(c_2Epath_2Epgenerate(A_27a,A_27b),V0f),V1g)))))))))))).
