include('Axioms/bft^2.ax').
thf(tp_ty_2Epath_2Epath,type,( ty_2Epath_2Epath: del > del >del )).
thf(tp_c_2Epath_2EPL,type,(c_2Epath_2EPL:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2Epath_2ESN,type,(c_2Epath_2ESN:(del>(del>$i)))).
thf(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))))).
thf(tp_c_2Epath_2Edrop,type,(c_2Epath_2Edrop:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2Epath_2Eel,type,(c_2Epath_2Eel:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2Epath_2Eevery,type,(c_2Epath_2Eevery:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2Epath_2Eexists,type,(c_2Epath_2Eexists:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2Epath_2Efilter,type,(c_2Epath_2Efilter:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2Epath_2Efinite,type,(c_2Epath_2Efinite:(del>(del>$i)))).
thf(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))))).
thf(tp_c_2Epath_2Efirst,type,(c_2Epath_2Efirst:(del>(del>$i)))).
thf(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))))).
thf(tp_c_2Epath_2EfirstP__at,type,(c_2Epath_2EfirstP__at:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2Epath_2Efirst__label,type,(c_2Epath_2Efirst__label:(del>(del>$i)))).
thf(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))))).
thf(tp_c_2Epath_2EfromPath,type,(c_2Epath_2EfromPath:(del>(del>$i)))).
thf(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)))))))).
thf(tp_c_2Epath_2Eis__stopped,type,(c_2Epath_2Eis__stopped:(del>(del>$i)))).
thf(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))))).
thf(tp_c_2Epath_2Elabels,type,(c_2Epath_2Elabels:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2Epath_2Elast,type,(c_2Epath_2Elast:(del>(del>$i)))).
thf(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))))).
thf(tp_c_2Epath_2Elength,type,(c_2Epath_2Elength:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2Epath_2Emem,type,(c_2Epath_2Emem:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2Epath_2Enth__label,type,(c_2Epath_2Enth__label:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2Epath_2Eokpath,type,(c_2Epath_2Eokpath:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2Epath_2Eokpath__f,type,(c_2Epath_2Eokpath__f:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2Epath_2Eparallel__comp,type,(c_2Epath_2Eparallel__comp:(del>(del>(del>(del>(del>$i))))))).
thf(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)))))))))))).
thf(tp_c_2Epath_2Epconcat,type,(c_2Epath_2Epconcat:(del>(del>$i)))).
thf(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)))))))).
thf(tp_c_2Epath_2Epcons,type,(c_2Epath_2Epcons:(del>(del>$i)))).
thf(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)))))))).
thf(tp_c_2Epath_2Epgenerate,type,(c_2Epath_2Epgenerate:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2Epath_2Eplink,type,(c_2Epath_2Eplink:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2Epath_2Epmap,type,(c_2Epath_2Epmap:(del>(del>(del>(del>$i)))))).
thf(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)))))))))).
thf(tp_c_2Epath_2Eseg,type,(c_2Epath_2Eseg:(del>(del>$i)))).
thf(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)))))))).
thf(tp_c_2Epath_2Estopped__at,type,(c_2Epath_2Estopped__at:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2Epath_2Etail,type,(c_2Epath_2Etail:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2Epath_2Etake,type,(c_2Epath_2Etake:(del>(del>$i)))).
thf(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))))))).
thf(tp_c_2Epath_2EtoPath,type,(c_2Epath_2EtoPath:(del>(del>$i)))).
thf(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)))))).
thf(tp_c_2Epath_2Etrace__machine,type,(c_2Epath_2Etrace__machine:(del>$i))).
thf(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))))))).
thf(tp_c_2Epath_2Eunfold,type,(c_2Epath_2Eunfold:(del>(del>(del>$i))))).
thf(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))))))))).
thf(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))@(lam@(ty_2Epair_2Eprod@A_27a@(ty_2Ellist_2Ellist@(ty_2Epair_2Eprod@A_27b@A_27a)))@(^ [V1x:$i] : c_2Ebool_2ET)))@V0rep))))))).
thf(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@(lam@(ty_2Epair_2Eprod@A_27a@(ty_2Ellist_2Ellist@(ty_2Epair_2Eprod@A_27b@A_27a)))@(^ [V2x:$i] : c_2Ebool_2ET))@V1r)) <=> ((ap@(c_2Epath_2EfromPath@A_27a@A_27b)@(ap@(c_2Epath_2EtoPath@A_27a@A_27b)@V1r)) = V1r)))))))).
thf(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))))))).
thf(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))))))))).
thf(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))))))))).
thf(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))))))))).
thf(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))))))))).
thf(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)))))))).
thf(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)))))))))).
thf(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))))))))))))))).
thf(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))))))))).
thf(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))))))))))))))))))).
thf(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))))))))))))))).
thf(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)))))))))))))).
thf(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)))))))))))))))).
thf(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)))))))))))))))).
thf(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))))))))))).
thf(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)))))))))).
thf(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))))))))))))).
thf(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)))))))))))).
thf(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))))))))))))))))))))))))))))).
thf(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))))))))))).
thf(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))))))))))))))).
thf(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))))))))))))))))))).
thf(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)))))))))))))).
thf(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))))))))))))))).
thf(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)))))))))))))).
thf(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)))))))))).
thf(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)))))))))).
thf(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))))))))).
thf(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)))))))))))))))).
thf(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)))))))))))))))).
thf(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)))))))))).
thf(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)))))))))).
thf(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)))))))))))))).
thf(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)))))))))).
thf(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))))))))))).
thf(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)))))))))).
thf(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))))))))))).
thf(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))@(lam@A_27b@(^ [V3y:$i] : (lam@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@A_27c@A_27a))@(^ [V4v2:$i] : (ap@(ap@(ap@(c_2Eoption_2Eoption__CASE@(ty_2Epair_2Eprod@A_27c@A_27a)@(ty_2Epath_2Epath@A_27b@A_27c))@V4v2)@(ap@(c_2Epath_2Estopped__at@A_27b@A_27c)@V3y))@(lam@(ty_2Epair_2Eprod@A_27c@A_27a)@(^ [V5v3:$i] : (ap@(ap@(c_2Epair_2Epair__CASE@(ty_2Epath_2Epath@A_27b@A_27c)@A_27c@A_27a)@V5v3)@(lam@A_27c@(^ [V6l:$i] : (lam@A_27a@(^ [V7v:$i] : (ap@(ap@(ap@(c_2Epath_2Epcons@A_27b@A_27c)@V3y)@V6l)@(ap@V1g@V7v)))))))))))))))))))))))))).
thf(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)))))))))))))))).
thf(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))))))))))))))))))).
thf(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))))))))))))))).
thf(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))))))))))))))))))))))).
thf(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))))))))))))).
thf(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)@(lam@ty_2Enum_2Enum@(^ [V1i:$i] : (ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@bool)@V1i)@(ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@(c_2Epath_2Efinite@A_27a@A_27b)@V0p))@(ap@(ap@c_2Eprim__rec_2E_3C@V1i)@(ap@(c_2Eoption_2ETHE@ty_2Enum_2Enum)@(ap@(c_2Epath_2Elength@A_27a@A_27b)@V0p)))))))))))))).
thf(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)))))))))).
thf(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))))))))))))).
thf(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)))))))).
thf(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)))))))))))))).
thf(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)))))))).
thf(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)))))))))))).
thf(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))))))))))))).
thf(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)))))))))))))))).
thf(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)))))))))))))))).
thf(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))))))))))))))))).
thf(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))))))))))))))))))))))).
thf(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))))))))))).
thf(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)))))))))))).
thf(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))))))))))).
thf(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))))))))))))))))).
thf(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))))))))))))))))).
thf(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)))))))))).
thf(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)))))))))).
thf(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))))))))))))).
thf(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))))))))))))).
thf(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))))))))))))).
thf(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))))))))))))).
thf(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)))))))))))).
thf(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)))))))))))))))))).
thf(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)))))))))).
thf(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))))))))))).
thf(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)))))))))).
thf(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)))))))))).
thf(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))@(lam@ty_2Enum_2Enum@(^ [V2m:$i] : (ap@(c_2Eoption_2ESOME@ty_2Enum_2Enum)@(ap@(ap@c_2Earithmetic_2E_2D@V2m)@(inj__ty_2Enum_2Enum @ V1n))))))))))))))).
thf(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)@(lam@ty_2Enum_2Enum@(^ [V2n:$i] : (ap@(ap@c_2Earithmetic_2E_2D@V2n)@(inj__ty_2Enum_2Enum @ V1i)))))@(ap@(c_2Epath_2EPL@A_27a@A_27b)@V0p)))))))))).
thf(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)))))))))))).
thf(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))))))))).
thf(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))))))))).
thf(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))))))))).
thf(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)))))))))).
thf(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)))))))))).
thf(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))))))))))).
thf(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)))))))))))).
thf(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)))))))).
thf(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)))))))))).
thf(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)))))))))))))).
thf(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)@(lam@ty_2Enum_2Enum@(^ [V2n:$i] : (ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@bool)@V2n)@(ap@(ap@c_2Earithmetic_2E_3C_3D@V2n)@(inj__ty_2Enum_2Enum @ V1i)))))))))))))).
thf(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))))))))).
thf(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)))))))))).
thf(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)))))))))).
thf(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)))))))))).
thf(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))))))))))).
thf(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)@(lam@ty_2Enum_2Enum@(^ [V3n:$i] : (ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@bool)@V3n)@(ap@(ap@c_2Earithmetic_2E_3C_3D@V3n)@(ap@(ap@c_2Earithmetic_2E_2D@(inj__ty_2Enum_2Enum @ V1j))@(inj__ty_2Enum_2Enum @ V0i)))))))))))))))).
thf(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))))))))))).
thf(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)))))))))).
thf(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)))))))))).
thf(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))))))))))))).
thf(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)))))))))))).
thf(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)))))))))).
thf(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))))))))))))).
thf(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))))))))))))))).
thf(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))))))))))).
thf(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))))))))))).
thf(conj_thm_2Epath_2Epgenerate__infinite,lemma,( ! [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))))))))))).
thf(conj_thm_2Epath_2Epgenerate__not__stopped,lemma,( ! [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)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => (~~ ((ap@(c_2Epath_2Estopped__at@A_27a@A_27b)@V2x) = (ap@(ap@(c_2Epath_2Epgenerate@A_27a@A_27b)@V0f)@V1g)))))))))))).
thf(conj_thm_2Epath_2Eel__pgenerate,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1f:$i] : ((mem@V1f@(arr@ty_2Enum_2Enum@A_27a)) => ( ! [V2g:$i] : ((mem@V2g@(arr@ty_2Enum_2Enum@A_27b)) => ((ap@(ap@(c_2Epath_2Eel@A_27a@A_27b)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(ap@(c_2Epath_2Epgenerate@A_27a@A_27b)@V1f)@V2g)) = (ap@V1f@(inj__ty_2Enum_2Enum @ V0n))))))))))).
thf(conj_thm_2Epath_2Enth__label__pgenerate,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1f:$i] : ((mem@V1f@(arr@ty_2Enum_2Enum@A_27a)) => ( ! [V2g:$i] : ((mem@V2g@(arr@ty_2Enum_2Enum@A_27b)) => ((ap@(ap@(c_2Epath_2Enth__label@A_27b@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(ap@(c_2Epath_2Epgenerate@A_27a@A_27b)@V1f)@V2g)) = (ap@V2g@(inj__ty_2Enum_2Enum @ V0n))))))))))).
thf(conj_thm_2Epath_2Epgenerate__11,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f1:$i] : ((mem@V0f1@(arr@ty_2Enum_2Enum@A_27a)) => ( ! [V1g1:$i] : ((mem@V1g1@(arr@ty_2Enum_2Enum@A_27b)) => ( ! [V2f2:$i] : ((mem@V2f2@(arr@ty_2Enum_2Enum@A_27a)) => ( ! [V3g2:$i] : ((mem@V3g2@(arr@ty_2Enum_2Enum@A_27b)) => (((ap@(ap@(c_2Epath_2Epgenerate@A_27a@A_27b)@V0f1)@V1g1) = (ap@(ap@(c_2Epath_2Epgenerate@A_27a@A_27b)@V2f2)@V3g2)) <=> ((V0f1 = V2f2) & (V1g1 = V3g2)))))))))))))).
thf(conj_thm_2Epath_2Epgenerate__onto,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))) => (? [V1f:$i] : ((mem@V1f@(arr@ty_2Enum_2Enum@A_27a)) & (? [V2g:$i] : ((mem@V2g@(arr@ty_2Enum_2Enum@A_27b)) & (V0p = (ap@(ap@(c_2Epath_2Epgenerate@A_27a@A_27b)@V1f)@V2g)))))))))))).
thf(ax_thm_2Epath_2Eokpath__f__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27b@(arr@A_27a@bool)))) => ( ! [V1X:$i] : ((mem@V1X@(arr@(ty_2Epath_2Epath@A_27a@A_27b)@bool)) => ((ap@(ap@(c_2Epath_2Eokpath__f@A_27a@A_27b)@V0R)@V1X) = (ap@(ap@(c_2Epred__set_2EUNION@(ty_2Epath_2Epath@A_27a@A_27b))@(ap@(c_2Epred__set_2EGSPEC@(ty_2Epath_2Epath@A_27a@A_27b)@A_27a)@(lam@A_27a@(^ [V2x:$i] : (ap@(ap@(c_2Epair_2E_2C@(ty_2Epath_2Epath@A_27a@A_27b)@bool)@(ap@(c_2Epath_2Estopped__at@A_27a@A_27b)@V2x))@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(c_2Epred__set_2EUNIV@A_27a)))))))@(ap@(c_2Epred__set_2EGSPEC@(ty_2Epath_2Epath@A_27a@A_27b)@(ty_2Epair_2Eprod@A_27a@(ty_2Epair_2Eprod@A_27b@(ty_2Epath_2Epath@A_27a@A_27b))))@(ap@(c_2Epair_2EUNCURRY@A_27a@(ty_2Epair_2Eprod@A_27b@(ty_2Epath_2Epath@A_27a@A_27b))@(ty_2Epair_2Eprod@(ty_2Epath_2Epath@A_27a@A_27b)@bool))@(lam@A_27a@(^ [V3x:$i] : (ap@(c_2Epair_2EUNCURRY@A_27b@(ty_2Epath_2Epath@A_27a@A_27b)@(ty_2Epair_2Eprod@(ty_2Epath_2Epath@A_27a@A_27b)@bool))@(lam@A_27b@(^ [V4r:$i] : (lam@(ty_2Epath_2Epath@A_27a@A_27b)@(^ [V5p:$i] : (ap@(ap@(c_2Epair_2E_2C@(ty_2Epath_2Epath@A_27a@A_27b)@bool)@(ap@(ap@(ap@(c_2Epath_2Epcons@A_27a@A_27b)@V3x)@V4r)@V5p))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(ap@V0R@V3x)@V4r)@(ap@(c_2Epath_2Efirst@A_27a@A_27b)@V5p)))@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epath_2Epath@A_27a@A_27b))@V5p)@V1X))))))))))))))))))))).
thf(conj_thm_2Epath_2Eokpath__monotone,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27b@(arr@A_27a@bool)))) => (p@(ap@(c_2EfixedPoint_2Emonotone@(ty_2Epath_2Epath@A_27a@A_27b)@(ty_2Epath_2Epath@A_27a@A_27b))@(ap@(c_2Epath_2Eokpath__f@A_27a@A_27b)@V0R)))))))).
thf(ax_thm_2Epath_2Eokpath__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27b@(arr@A_27a@bool)))) => ((ap@(c_2Epath_2Eokpath@A_27a@A_27b)@V0R) = (ap@(c_2EfixedPoint_2Egfp@(ty_2Epath_2Epath@A_27a@A_27b))@(ap@(c_2Epath_2Eokpath__f@A_27a@A_27b)@V0R)))))))).
thf(conj_thm_2Epath_2Eokpath__co__ind,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27b@(arr@A_27a@bool)))) => ( ! [V1P:$i] : ((mem@V1P@(arr@(ty_2Epath_2Epath@A_27a@A_27b)@bool)) => (( ! [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@V1P@(ap@(ap@(ap@(c_2Epath_2Epcons@A_27a@A_27b)@V2x)@V3r)@V4p))) => ((p@(ap@(ap@(ap@V0R@V2x)@V3r)@(ap@(c_2Epath_2Efirst@A_27a@A_27b)@V4p))) & (p@(ap@V1P@V4p)))))))))) => ( ! [V5p:$i] : ((mem@V5p@(ty_2Epath_2Epath@A_27a@A_27b)) => ((p@(ap@V1P@V5p)) => (p@(ap@(ap@(c_2Epath_2Eokpath@A_27a@A_27b)@V0R)@V5p))))))))))))).
thf(conj_thm_2Epath_2Eokpath__cases,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27b@(arr@A_27a@bool)))) => ( ! [V1x:$i] : ((mem@V1x@(ty_2Epath_2Epath@A_27a@A_27b)) => ((p@(ap@(ap@(c_2Epath_2Eokpath@A_27a@A_27b)@V0R)@V1x)) <=> ((? [V2x_27:$i] : ((mem@V2x_27@A_27a) & (V1x = (ap@(c_2Epath_2Estopped__at@A_27a@A_27b)@V2x_27)))) | (? [V3x_27:$i] : ((mem@V3x_27@A_27a) & (? [V4r:$i] : ((mem@V4r@A_27b) & (? [V5p:$i] : ((mem@V5p@(ty_2Epath_2Epath@A_27a@A_27b)) & ((V1x = (ap@(ap@(ap@(c_2Epath_2Epcons@A_27a@A_27b)@V3x_27)@V4r)@V5p)) & ((p@(ap@(ap@(ap@V0R@V3x_27)@V4r)@(ap@(c_2Epath_2Efirst@A_27a@A_27b)@V5p))) & (p@(ap@(ap@(c_2Epath_2Eokpath@A_27a@A_27b)@V0R)@V5p))))))))))))))))))).
thf(conj_thm_2Epath_2Eokpath__thm,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27b@(arr@A_27a@bool)))) => (( ! [V1x:$i] : ((mem@V1x@A_27a) => (p@(ap@(ap@(c_2Epath_2Eokpath@A_27a@A_27b)@V0R)@(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@(ap@(c_2Epath_2Eokpath@A_27a@A_27b)@V0R)@(ap@(ap@(ap@(c_2Epath_2Epcons@A_27a@A_27b)@V2x)@V3r)@V4p))) <=> ((p@(ap@(ap@(ap@V0R@V2x)@V3r)@(ap@(c_2Epath_2Efirst@A_27a@A_27b)@V4p))) & (p@(ap@(ap@(c_2Epath_2Eokpath@A_27a@A_27b)@V0R)@V4p)))))))))))))))).
thf(conj_thm_2Epath_2Efinite__okpath__ind,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@(ty_2Epath_2Epath@A_27a@A_27b)@bool)) => ( ! [V1R:$i] : ((mem@V1R@(arr@A_27a@(arr@A_27b@(arr@A_27a@bool)))) => ((( ! [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@(ap@(c_2Epath_2Eokpath@A_27a@A_27b)@V1R)@V5p)) & ((p@(ap@(c_2Epath_2Efinite@A_27a@A_27b)@V5p)) & ((p@(ap@(ap@(ap@V1R@V3x)@V4r)@(ap@(c_2Epath_2Efirst@A_27a@A_27b)@V5p))) & (p@(ap@V0P@V5p))))) => (p@(ap@V0P@(ap@(ap@(ap@(c_2Epath_2Epcons@A_27a@A_27b)@V3x)@V4r)@V5p))))))))))) => ( ! [V6sigma:$i] : ((mem@V6sigma@(ty_2Epath_2Epath@A_27a@A_27b)) => (((p@(ap@(ap@(c_2Epath_2Eokpath@A_27a@A_27b)@V1R)@V6sigma)) & (p@(ap@(c_2Epath_2Efinite@A_27a@A_27b)@V6sigma))) => (p@(ap@V0P@V6sigma))))))))))))).
thf(conj_thm_2Epath_2Eokpath__pmap,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27b@(arr@A_27a@bool)))) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27a@A_27a)) => ( ! [V2g:$i] : ((mem@V2g@(arr@A_27b@A_27b)) => ( ! [V3p:$i] : ((mem@V3p@(ty_2Epath_2Epath@A_27a@A_27b)) => (((p@(ap@(ap@(c_2Epath_2Eokpath@A_27a@A_27b)@V0R)@V3p)) & ( ! [V4x:$i] : ((mem@V4x@A_27a) => ( ! [V5r:$i] : ((mem@V5r@A_27b) => ( ! [V6y:$i] : ((mem@V6y@A_27a) => ((p@(ap@(ap@(ap@V0R@V4x)@V5r)@V6y)) => (p@(ap@(ap@(ap@V0R@(ap@V1f@V4x))@(ap@V2g@V5r))@(ap@V1f@V6y))))))))))) => (p@(ap@(ap@(c_2Epath_2Eokpath@A_27a@A_27b)@V0R)@(ap@(ap@(ap@(c_2Epath_2Epmap@A_27a@A_27b@A_27a@A_27b)@V1f)@V2g)@V3p))))))))))))))).
thf(ax_thm_2Epath_2Eplink__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1p:$i] : ((mem@V1p@(ty_2Epath_2Epath@A_27a@A_27b)) => ((ap@(ap@(c_2Epath_2Eplink@A_27a@A_27b)@(ap@(c_2Epath_2Estopped__at@A_27a@A_27b)@V0x))@V1p) = V1p))))) & ( ! [V2x:$i] : ((mem@V2x@A_27a) => ( ! [V3r:$i] : ((mem@V3r@A_27b) => ( ! [V4p1:$i] : ((mem@V4p1@(ty_2Epath_2Epath@A_27a@A_27b)) => ( ! [V5p2:$i] : ((mem@V5p2@(ty_2Epath_2Epath@A_27a@A_27b)) => ((ap@(ap@(c_2Epath_2Eplink@A_27a@A_27b)@(ap@(ap@(ap@(c_2Epath_2Epcons@A_27a@A_27b)@V2x)@V3r)@V4p1))@V5p2) = (ap@(ap@(ap@(c_2Epath_2Epcons@A_27a@A_27b)@V2x)@V3r)@(ap@(ap@(c_2Epath_2Eplink@A_27a@A_27b)@V4p1)@V5p2))))))))))))))).
thf(conj_thm_2Epath_2Efinite__plink,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)) => ((p@(ap@(c_2Epath_2Efinite@A_27a@A_27b)@(ap@(ap@(c_2Epath_2Eplink@A_27a@A_27b)@V0p1)@V1p2))) <=> ((p@(ap@(c_2Epath_2Efinite@A_27a@A_27b)@V0p1)) & (p@(ap@(c_2Epath_2Efinite@A_27a@A_27b)@V1p2))))))))))).
thf(conj_thm_2Epath_2Efirst__plink,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)) => (((ap@(c_2Epath_2Elast@A_27a@A_27b)@V0p1) = (ap@(c_2Epath_2Efirst@A_27a@A_27b)@V1p2)) => ((ap@(c_2Epath_2Efirst@A_27a@A_27b)@(ap@(ap@(c_2Epath_2Eplink@A_27a@A_27b)@V0p1)@V1p2)) = (ap@(c_2Epath_2Efirst@A_27a@A_27b)@V0p1)))))))))).
thf(conj_thm_2Epath_2Elast__plink,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)) => (((p@(ap@(c_2Epath_2Efinite@A_27a@A_27b)@V0p1)) & ((p@(ap@(c_2Epath_2Efinite@A_27a@A_27b)@V1p2)) & ((ap@(c_2Epath_2Elast@A_27a@A_27b)@V0p1) = (ap@(c_2Epath_2Efirst@A_27a@A_27b)@V1p2)))) => ((ap@(c_2Epath_2Elast@A_27a@A_27b)@(ap@(ap@(c_2Epath_2Eplink@A_27a@A_27b)@V0p1)@V1p2)) = (ap@(c_2Epath_2Elast@A_27a@A_27b)@V1p2)))))))))).
thf(conj_thm_2Epath_2Eokpath__plink,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27b@(arr@A_27a@bool)))) => ( ! [V1p1:$i] : ((mem@V1p1@(ty_2Epath_2Epath@A_27a@A_27b)) => ( ! [V2p2:$i] : ((mem@V2p2@(ty_2Epath_2Epath@A_27a@A_27b)) => (((p@(ap@(c_2Epath_2Efinite@A_27a@A_27b)@V1p1)) & ((ap@(c_2Epath_2Elast@A_27a@A_27b)@V1p1) = (ap@(c_2Epath_2Efirst@A_27a@A_27b)@V2p2))) => ((p@(ap@(ap@(c_2Epath_2Eokpath@A_27a@A_27b)@V0R)@(ap@(ap@(c_2Epath_2Eplink@A_27a@A_27b)@V1p1)@V2p2))) <=> ((p@(ap@(ap@(c_2Epath_2Eokpath@A_27a@A_27b)@V0R)@V1p1)) & (p@(ap@(ap@(c_2Epath_2Eokpath@A_27a@A_27b)@V0R)@V2p2)))))))))))))).
thf(conj_thm_2Epath_2Eokpath__take,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27b@(arr@A_27a@bool)))) => ( ! [V1p:$i] : ((mem@V1p@(ty_2Epath_2Epath@A_27a@A_27b)) => ( ! [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@(ap@(c_2Epath_2Eokpath@A_27a@A_27b)@V0R)@V1p))) => (p@(ap@(ap@(c_2Epath_2Eokpath@A_27a@A_27b)@V0R)@(ap@(ap@(c_2Epath_2Etake@A_27a@A_27b)@(inj__ty_2Enum_2Enum @ V2i))@V1p)))))))))))).
thf(conj_thm_2Epath_2Eokpath__drop,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27b@(arr@A_27a@bool)))) => ( ! [V1p:$i] : ((mem@V1p@(ty_2Epath_2Epath@A_27a@A_27b)) => ( ! [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@(ap@(c_2Epath_2Eokpath@A_27a@A_27b)@V0R)@V1p))) => (p@(ap@(ap@(c_2Epath_2Eokpath@A_27a@A_27b)@V0R)@(ap@(ap@(c_2Epath_2Edrop@A_27a@A_27b)@(inj__ty_2Enum_2Enum @ V2i))@V1p)))))))))))).
thf(conj_thm_2Epath_2Eokpath__seg,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27b@(arr@A_27a@bool)))) => ( ! [V1p:$i] : ((mem@V1p@(ty_2Epath_2Epath@A_27a@A_27b)) => ( ! [V2i:tp__ty_2Enum_2Enum] : ( ! [V3j:tp__ty_2Enum_2Enum] : (((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V2i))@(inj__ty_2Enum_2Enum @ V3j))) & ((p@(ap@(ap@(c_2Ebool_2EIN@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V3j))@(ap@(c_2Epath_2EPL@A_27a@A_27b)@V1p))) & (p@(ap@(ap@(c_2Epath_2Eokpath@A_27a@A_27b)@V0R)@V1p)))) => (p@(ap@(ap@(c_2Epath_2Eokpath@A_27a@A_27b)@V0R)@(ap@(ap@(ap@(c_2Epath_2Eseg@A_27a@A_27b)@(inj__ty_2Enum_2Enum @ V2i))@(inj__ty_2Enum_2Enum @ V3j))@V1p))))))))))))).
thf(ax_thm_2Epath_2ESN__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27b@(arr@A_27a@bool)))) => ((p@(ap@(c_2Epath_2ESN@A_27a@A_27b)@V0R)) <=> (p@(ap@(c_2Erelation_2EWF@A_27a)@(lam@A_27a@(^ [V1x:$i] : (lam@A_27a@(^ [V2y:$i] : (ap@(c_2Ebool_2E_3F@A_27b)@(lam@A_27b@(^ [V3l:$i] : (ap@(ap@(ap@V0R@V2y)@V3l)@V1x)))))))))))))))).
thf(conj_thm_2Epath_2ESN__finite__paths,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27b@(arr@A_27a@bool)))) => ( ! [V1p:$i] : ((mem@V1p@(ty_2Epath_2Epath@A_27a@A_27b)) => (((p@(ap@(c_2Epath_2ESN@A_27a@A_27b)@V0R)) & (p@(ap@(ap@(c_2Epath_2Eokpath@A_27a@A_27b)@V0R)@V1p))) => (p@(ap@(c_2Epath_2Efinite@A_27a@A_27b)@V1p)))))))))).
thf(conj_thm_2Epath_2Efinite__paths__SN,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27b@(arr@A_27a@bool)))) => (( ! [V1p:$i] : ((mem@V1p@(ty_2Epath_2Epath@A_27a@A_27b)) => ((p@(ap@(ap@(c_2Epath_2Eokpath@A_27a@A_27b)@V0R)@V1p)) => (p@(ap@(c_2Epath_2Efinite@A_27a@A_27b)@V1p))))) => (p@(ap@(c_2Epath_2ESN@A_27a@A_27b)@V0R)))))))).
thf(conj_thm_2Epath_2ESN__finite__paths__EQ,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27b@(arr@A_27a@bool)))) => ((p@(ap@(c_2Epath_2ESN@A_27a@A_27b)@V0R)) <=> ( ! [V1p:$i] : ((mem@V1p@(ty_2Epath_2Epath@A_27a@A_27b)) => ((p@(ap@(ap@(c_2Epath_2Eokpath@A_27a@A_27b)@V0R)@V1p)) => (p@(ap@(c_2Epath_2Efinite@A_27a@A_27b)@V1p))))))))))).
thf(conj_thm_2Epath_2Elabels__LMAP,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0p:$i] : ((mem@V0p@(ty_2Epath_2Epath@A_27a@A_27b)) => ((ap@(c_2Epath_2Elabels@A_27a@A_27b)@V0p) = (ap@(ap@(c_2Ellist_2ELMAP@(ty_2Epair_2Eprod@A_27b@A_27a)@A_27b)@(c_2Epair_2EFST@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))))))))).
thf(conj_thm_2Epath_2Elabels__plink,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)) => ((ap@(c_2Epath_2Elabels@A_27a@A_27b)@(ap@(ap@(c_2Epath_2Eplink@A_27a@A_27b)@V0p1)@V1p2)) = (ap@(ap@(c_2Ellist_2ELAPPEND@A_27b)@(ap@(c_2Epath_2Elabels@A_27a@A_27b)@V0p1))@(ap@(c_2Epath_2Elabels@A_27a@A_27b)@V1p2)))))))))).
thf(conj_thm_2Epath_2Efinite__labels,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0p:$i] : ((mem@V0p@(ty_2Epath_2Epath@A_27a@A_27b)) => ((p@(ap@(c_2Ellist_2ELFINITE@A_27b)@(ap@(c_2Epath_2Elabels@A_27a@A_27b)@V0p))) <=> (p@(ap@(c_2Epath_2Efinite@A_27a@A_27b)@V0p)))))))).
thf(ax_thm_2Epath_2Eunfold__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0proj:$i] : ((mem@V0proj@(arr@A_27c@A_27a)) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27c@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@A_27c@A_27b)))) => ( ! [V2s:$i] : ((mem@V2s@A_27c) => ((ap@(ap@(ap@(c_2Epath_2Eunfold@A_27a@A_27b@A_27c)@V0proj)@V1f)@V2s) = (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@V0proj@V2s))@(ap@(ap@(c_2Ellist_2ELUNFOLD@(ty_2Epair_2Eprod@A_27b@A_27a)@A_27c)@(lam@A_27c@(^ [V3s:$i] : (ap@(ap@(c_2Eoption_2EOPTION__MAP@(ty_2Epair_2Eprod@A_27c@A_27b)@(ty_2Epair_2Eprod@A_27c@(ty_2Epair_2Eprod@A_27b@A_27a)))@(ap@(c_2Epair_2EUNCURRY@A_27c@A_27b@(ty_2Epair_2Eprod@A_27c@(ty_2Epair_2Eprod@A_27b@A_27a)))@(lam@A_27c@(^ [V4next__s:$i] : (lam@A_27b@(^ [V5lbl:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27c@(ty_2Epair_2Eprod@A_27b@A_27a))@V4next__s)@(ap@(ap@(c_2Epair_2E_2C@A_27b@A_27a)@V5lbl)@(ap@V0proj@V4next__s)))))))))@(ap@V1f@V3s)))))@V2s)))))))))))))).
thf(conj_thm_2Epath_2Eunfold__thm,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0proj:$i] : ((mem@V0proj@(arr@A_27a@A_27b)) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27a@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@A_27a@A_27c)))) => ( ! [V2s:$i] : ((mem@V2s@A_27a) => ((ap@(ap@(ap@(c_2Epath_2Eunfold@A_27b@A_27c@A_27a)@V0proj)@V1f)@V2s) = (ap@(ap@(ap@(c_2Eoption_2Eoption__CASE@(ty_2Epair_2Eprod@A_27a@A_27c)@(ty_2Epath_2Epath@A_27b@A_27c))@(ap@V1f@V2s))@(ap@(c_2Epath_2Estopped__at@A_27b@A_27c)@(ap@V0proj@V2s)))@(lam@(ty_2Epair_2Eprod@A_27a@A_27c)@(^ [V3v:$i] : (ap@(ap@(c_2Epair_2Epair__CASE@(ty_2Epath_2Epath@A_27b@A_27c)@A_27a@A_27c)@V3v)@(lam@A_27a@(^ [V4s_27:$i] : (lam@A_27c@(^ [V5l:$i] : (ap@(ap@(ap@(c_2Epath_2Epcons@A_27b@A_27c)@(ap@V0proj@V2s))@V5l)@(ap@(ap@(ap@(c_2Epath_2Eunfold@A_27b@A_27c@A_27a)@V0proj)@V1f)@V4s_27))))))))))))))))))))).
thf(conj_thm_2Epath_2Eunfold__thm2,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0proj:$i] : ((mem@V0proj@(arr@A_27a@A_27b)) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27a@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@A_27a@A_27c)))) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ( ! [V3v1:$i] : ((mem@V3v1@A_27a) => ( ! [V4v2:$i] : ((mem@V4v2@A_27c) => ((((ap@V1f@V2x) = (c_2Eoption_2ENONE@(ty_2Epair_2Eprod@A_27a@A_27c))) => ((ap@(ap@(ap@(c_2Epath_2Eunfold@A_27b@A_27c@A_27a)@V0proj)@V1f)@V2x) = (ap@(c_2Epath_2Estopped__at@A_27b@A_27c)@(ap@V0proj@V2x)))) & (((ap@V1f@V2x) = (ap@(c_2Eoption_2ESOME@(ty_2Epair_2Eprod@A_27a@A_27c))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27c)@V3v1)@V4v2))) => ((ap@(ap@(ap@(c_2Epath_2Eunfold@A_27b@A_27c@A_27a)@V0proj)@V1f)@V2x) = (ap@(ap@(ap@(c_2Epath_2Epcons@A_27b@A_27c)@(ap@V0proj@V2x))@V4v2)@(ap@(ap@(ap@(c_2Epath_2Eunfold@A_27b@A_27c@A_27a)@V0proj)@V1f)@V3v1))))))))))))))))))).
thf(conj_thm_2Epath_2Elabels__unfold,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0proj:$i] : ((mem@V0proj@(arr@A_27a@A_27b)) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27a@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@A_27a@A_27c)))) => ( ! [V2s:$i] : ((mem@V2s@A_27a) => ((ap@(c_2Epath_2Elabels@A_27b@A_27c)@(ap@(ap@(ap@(c_2Epath_2Eunfold@A_27b@A_27c@A_27a)@V0proj)@V1f)@V2s)) = (ap@(ap@(c_2Ellist_2ELUNFOLD@A_27c@A_27a)@V1f)@V2s)))))))))))).
thf(conj_thm_2Epath_2Eokpath__unfold,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1m:$i] : ((mem@V1m@(arr@A_27b@(arr@A_27c@(arr@A_27b@bool)))) => ( ! [V2proj:$i] : ((mem@V2proj@(arr@A_27a@A_27b)) => ( ! [V3f:$i] : ((mem@V3f@(arr@A_27a@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@A_27a@A_27c)))) => ( ! [V4s:$i] : ((mem@V4s@A_27a) => (((p@(ap@V0P@V4s)) & (( ! [V5s:$i] : ((mem@V5s@A_27a) => ( ! [V6s_27:$i] : ((mem@V6s_27@A_27a) => ( ! [V7l:$i] : ((mem@V7l@A_27c) => (((p@(ap@V0P@V5s)) & ((ap@V3f@V5s) = (ap@(c_2Eoption_2ESOME@(ty_2Epair_2Eprod@A_27a@A_27c))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27c)@V6s_27)@V7l)))) => (p@(ap@V0P@V6s_27))))))))) & ( ! [V8s:$i] : ((mem@V8s@A_27a) => ( ! [V9s_27:$i] : ((mem@V9s_27@A_27a) => ( ! [V10l:$i] : ((mem@V10l@A_27c) => (((p@(ap@V0P@V8s)) & ((ap@V3f@V8s) = (ap@(c_2Eoption_2ESOME@(ty_2Epair_2Eprod@A_27a@A_27c))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27c)@V9s_27)@V10l)))) => (p@(ap@(ap@(ap@V1m@(ap@V2proj@V8s))@V10l)@(ap@V2proj@V9s_27)))))))))))) => (p@(ap@(ap@(c_2Epath_2Eokpath@A_27b@A_27c)@V1m)@(ap@(ap@(ap@(c_2Epath_2Eunfold@A_27b@A_27c@A_27a)@V2proj)@V3f)@V4s)))))))))))))))))).
thf(ax_thm_2Epath_2Etrace__machine__def,axiom,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@(ty_2Elist_2Elist@A_27a)@bool)) => ( ! [V1s:$i] : ((mem@V1s@(ty_2Elist_2Elist@A_27a)) => ( ! [V2l:$i] : ((mem@V2l@A_27a) => ( ! [V3s_27:$i] : ((mem@V3s_27@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@(ap@(ap@(c_2Epath_2Etrace__machine@A_27a)@V0P)@V1s)@V2l)@V3s_27)) <=> ((p@(ap@V0P@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V1s)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V2l)@(c_2Elist_2ENIL@A_27a))))) & (V3s_27 = (ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V1s)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V2l)@(c_2Elist_2ENIL@A_27a)))))))))))))))).
thf(conj_thm_2Epath_2Etrace__machine__thm,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@(ty_2Elist_2Elist@A_27a)@bool)) => ( ! [V1tr:$i] : ((mem@V1tr@(ty_2Ellist_2Ellist@A_27a)) => (( ! [V2n:tp__ty_2Enum_2Enum] : ( ! [V3l:$i] : ((mem@V3l@(ty_2Elist_2Elist@A_27a)) => (((ap@(ap@(c_2Ellist_2ELTAKE@A_27a)@(inj__ty_2Enum_2Enum @ V2n))@V1tr) = (ap@(c_2Eoption_2ESOME@(ty_2Elist_2Elist@A_27a))@V3l)) => (p@(ap@V0P@V3l)))))) => (? [V4p:$i] : ((mem@V4p@(ty_2Epath_2Epath@(ty_2Elist_2Elist@A_27a)@A_27a)) & ((V1tr = (ap@(c_2Epath_2Elabels@(ty_2Elist_2Elist@A_27a)@A_27a)@V4p)) & ((p@(ap@(ap@(c_2Epath_2Eokpath@(ty_2Elist_2Elist@A_27a)@A_27a)@(ap@(c_2Epath_2Etrace__machine@A_27a)@V0P))@V4p)) & ((ap@(c_2Epath_2Efirst@(ty_2Elist_2Elist@A_27a)@A_27a)@V4p) = (c_2Elist_2ENIL@A_27a))))))))))))).
thf(conj_thm_2Epath_2Etrace__machine__thm2,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ( ! [V2P:$i] : ((mem@V2P@(arr@(ty_2Elist_2Elist@A_27a)@bool)) => ( ! [V3p:$i] : ((mem@V3p@(ty_2Epath_2Epath@(ty_2Elist_2Elist@A_27a)@A_27a)) => ( ! [V4init:$i] : ((mem@V4init@A_27b) => (((p@(ap@(ap@(c_2Epath_2Eokpath@(ty_2Elist_2Elist@A_27a)@A_27a)@(ap@(c_2Epath_2Etrace__machine@A_27a)@V2P))@V3p)) & (p@(ap@V2P@(ap@(c_2Epath_2Efirst@(ty_2Elist_2Elist@A_27a)@A_27a)@V3p)))) => (((ap@(ap@(c_2Ellist_2ELTAKE@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Epath_2Elabels@(ty_2Elist_2Elist@A_27a)@A_27a)@V3p)) = (ap@(c_2Eoption_2ESOME@(ty_2Elist_2Elist@A_27a))@V1l)) => (p@(ap@V2P@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(c_2Epath_2Efirst@(ty_2Elist_2Elist@A_27a)@A_27a)@V3p))@V1l))))))))))))))))).
thf(conj_thm_2Epath_2ELTAKE__labels,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1p:$i] : ((mem@V1p@(ty_2Epath_2Epath@A_27a@A_27b)) => ( ! [V2l:$i] : ((mem@V2l@(ty_2Elist_2Elist@A_27b)) => (((ap@(ap@(c_2Ellist_2ELTAKE@A_27b)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Epath_2Elabels@A_27a@A_27b)@V1p)) = (ap@(c_2Eoption_2ESOME@(ty_2Elist_2Elist@A_27b))@V2l)) <=> ((p@(ap@(ap@(c_2Ebool_2EIN@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Epath_2EPL@A_27a@A_27b)@V1p))) & ((ap@(c_2Ellist_2EtoList@A_27b)@(ap@(c_2Epath_2Elabels@A_27a@A_27b)@(ap@(ap@(c_2Epath_2Etake@A_27a@A_27b)@(inj__ty_2Enum_2Enum @ V0n))@V1p))) = (ap@(c_2Eoption_2ESOME@(ty_2Elist_2Elist@A_27b))@V2l)))))))))))).
thf(conj_thm_2Epath_2Edrop__eq__pcons,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1p:$i] : ((mem@V1p@(ty_2Epath_2Epath@A_27a@A_27b)) => ( ! [V2h:$i] : ((mem@V2h@A_27a) => ( ! [V3l:$i] : ((mem@V3l@A_27b) => ( ! [V4t:$i] : ((mem@V4t@(ty_2Epath_2Epath@A_27a@A_27b)) => (((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_2Edrop@A_27a@A_27b)@(inj__ty_2Enum_2Enum @ V0n))@V1p) = (ap@(ap@(ap@(c_2Epath_2Epcons@A_27a@A_27b)@V2h)@V3l)@V4t))) => (p@(ap@(ap@(c_2Ebool_2EIN@ty_2Enum_2Enum)@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0n))@(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)))))))))))))))).
thf(ax_thm_2Epath_2Eparallel__comp__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [A_27e:del]: ( ! [V0m1:$i] : ((mem@V0m1@(arr@A_27a@(arr@A_27b@(arr@A_27c@bool)))) => ( ! [V1m2:$i] : ((mem@V1m2@(arr@A_27d@(arr@A_27b@(arr@A_27e@bool)))) => ( ! [V2s1:$i] : ((mem@V2s1@A_27a) => ( ! [V3s2:$i] : ((mem@V3s2@A_27d) => ( ! [V4l:$i] : ((mem@V4l@A_27b) => ( ! [V5s1_27:$i] : ((mem@V5s1_27@A_27c) => ( ! [V6s2_27:$i] : ((mem@V6s2_27@A_27e) => ((p@(ap@(ap@(ap@(ap@(ap@(c_2Epath_2Eparallel__comp@A_27a@A_27b@A_27c@A_27d@A_27e)@V0m1)@V1m2)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27d)@V2s1)@V3s2))@V4l)@(ap@(ap@(c_2Epair_2E_2C@A_27c@A_27e)@V5s1_27)@V6s2_27))) <=> ((p@(ap@(ap@(ap@V0m1@V2s1)@V4l)@V5s1_27)) & (p@(ap@(ap@(ap@V1m2@V3s2)@V4l)@V6s2_27)))))))))))))))))))))))).
thf(conj_thm_2Epath_2Eokpath__parallel__comp,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0p:$i] : ((mem@V0p@(ty_2Epath_2Epath@(ty_2Epair_2Eprod@A_27a@A_27b)@A_27c)) => ( ! [V1m1:$i] : ((mem@V1m1@(arr@A_27a@(arr@A_27c@(arr@A_27a@bool)))) => ( ! [V2m2:$i] : ((mem@V2m2@(arr@A_27b@(arr@A_27c@(arr@A_27b@bool)))) => ((p@(ap@(ap@(c_2Epath_2Eokpath@(ty_2Epair_2Eprod@A_27a@A_27b)@A_27c)@(ap@(ap@(c_2Epath_2Eparallel__comp@A_27a@A_27c@A_27a@A_27b@A_27b)@V1m1)@V2m2))@V0p)) <=> ((p@(ap@(ap@(c_2Epath_2Eokpath@A_27a@A_27c)@V1m1)@(ap@(ap@(ap@(c_2Epath_2Epmap@(ty_2Epair_2Eprod@A_27a@A_27b)@A_27c@A_27a@A_27c)@(c_2Epair_2EFST@A_27a@A_27b))@(lam@A_27c@(^ [V3x:$i] : V3x)))@V0p))) & (p@(ap@(ap@(c_2Epath_2Eokpath@A_27b@A_27c)@V2m2)@(ap@(ap@(ap@(c_2Epath_2Epmap@(ty_2Epair_2Eprod@A_27a@A_27b)@A_27c@A_27b@A_27c)@(c_2Epair_2ESND@A_27a@A_27b))@(lam@A_27c@(^ [V4x:$i] : V4x)))@V0p))))))))))))))).
thf(conj_thm_2Epath_2Ebuild__pcomp__trace,conjecture,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0m1:$i] : ((mem@V0m1@(arr@A_27a@(arr@A_27b@(arr@A_27a@bool)))) => ( ! [V1p1:$i] : ((mem@V1p1@(ty_2Epath_2Epath@A_27a@A_27b)) => ( ! [V2m2:$i] : ((mem@V2m2@(arr@A_27c@(arr@A_27b@(arr@A_27c@bool)))) => ( ! [V3p2:$i] : ((mem@V3p2@(ty_2Epath_2Epath@A_27c@A_27b)) => (((p@(ap@(ap@(c_2Epath_2Eokpath@A_27a@A_27b)@V0m1)@V1p1)) & ((p@(ap@(ap@(c_2Epath_2Eokpath@A_27c@A_27b)@V2m2)@V3p2)) & ((ap@(c_2Epath_2Elabels@A_27a@A_27b)@V1p1) = (ap@(c_2Epath_2Elabels@A_27c@A_27b)@V3p2)))) => (? [V4p:$i] : ((mem@V4p@(ty_2Epath_2Epath@(ty_2Epair_2Eprod@A_27a@A_27c)@A_27b)) & ((p@(ap@(ap@(c_2Epath_2Eokpath@(ty_2Epair_2Eprod@A_27a@A_27c)@A_27b)@(ap@(ap@(c_2Epath_2Eparallel__comp@A_27a@A_27b@A_27a@A_27c@A_27c)@V0m1)@V2m2))@V4p)) & (((ap@(c_2Epath_2Elabels@(ty_2Epair_2Eprod@A_27a@A_27c)@A_27b)@V4p) = (ap@(c_2Epath_2Elabels@A_27a@A_27b)@V1p1)) & ((ap@(c_2Epath_2Efirst@(ty_2Epair_2Eprod@A_27a@A_27c)@A_27b)@V4p) = (ap@(ap@(c_2Epair_2E_2C@A_27a@A_27c)@(ap@(c_2Epath_2Efirst@A_27a@A_27b)@V1p1))@(ap@(c_2Epath_2Efirst@A_27c@A_27b)@V3p2)))))))))))))))))))).
