include('Axioms/wot^2.ax').
thf(tp_ty_2Ellist_2Ellist,type,( ty_2Ellist_2Ellist: del >del )).
thf(tp_c_2Ellist_2ELAPPEND,type,(c_2Ellist_2ELAPPEND:(del>$i))).
thf(mem_c_2Ellist_2ELAPPEND,axiom,( ! [A_27a:del] : (mem@(c_2Ellist_2ELAPPEND@A_27a)@(arr@(ty_2Ellist_2Ellist@A_27a)@(arr@(ty_2Ellist_2Ellist@A_27a)@(ty_2Ellist_2Ellist@A_27a)))))).
thf(tp_c_2Ellist_2ELCONS,type,(c_2Ellist_2ELCONS:(del>$i))).
thf(mem_c_2Ellist_2ELCONS,axiom,( ! [A_27a:del] : (mem@(c_2Ellist_2ELCONS@A_27a)@(arr@A_27a@(arr@(ty_2Ellist_2Ellist@A_27a)@(ty_2Ellist_2Ellist@A_27a)))))).
thf(tp_c_2Ellist_2ELDROP,type,(c_2Ellist_2ELDROP:(del>$i))).
thf(mem_c_2Ellist_2ELDROP,axiom,( ! [A_27a:del] : (mem@(c_2Ellist_2ELDROP@A_27a)@(arr@ty_2Enum_2Enum@(arr@(ty_2Ellist_2Ellist@A_27a)@(ty_2Eoption_2Eoption@(ty_2Ellist_2Ellist@A_27a))))))).
thf(tp_c_2Ellist_2ELFILTER,type,(c_2Ellist_2ELFILTER:(del>$i))).
thf(mem_c_2Ellist_2ELFILTER,axiom,( ! [A_27a:del] : (mem@(c_2Ellist_2ELFILTER@A_27a)@(arr@(arr@A_27a@bool)@(arr@(ty_2Ellist_2Ellist@A_27a)@(ty_2Ellist_2Ellist@A_27a)))))).
thf(tp_c_2Ellist_2ELFINITE,type,(c_2Ellist_2ELFINITE:(del>$i))).
thf(mem_c_2Ellist_2ELFINITE,axiom,( ! [A_27a:del] : (mem@(c_2Ellist_2ELFINITE@A_27a)@(arr@(ty_2Ellist_2Ellist@A_27a)@bool)))).
thf(tp_c_2Ellist_2ELFLATTEN,type,(c_2Ellist_2ELFLATTEN:(del>$i))).
thf(mem_c_2Ellist_2ELFLATTEN,axiom,( ! [A_27a:del] : (mem@(c_2Ellist_2ELFLATTEN@A_27a)@(arr@(ty_2Ellist_2Ellist@(ty_2Ellist_2Ellist@A_27a))@(ty_2Ellist_2Ellist@A_27a))))).
thf(tp_c_2Ellist_2ELGENLIST,type,(c_2Ellist_2ELGENLIST:(del>$i))).
thf(mem_c_2Ellist_2ELGENLIST,axiom,( ! [A_27a:del] : (mem@(c_2Ellist_2ELGENLIST@A_27a)@(arr@(arr@ty_2Enum_2Enum@A_27a)@(arr@(ty_2Eoption_2Eoption@ty_2Enum_2Enum)@(ty_2Ellist_2Ellist@A_27a)))))).
thf(tp_c_2Ellist_2ELHD,type,(c_2Ellist_2ELHD:(del>$i))).
thf(mem_c_2Ellist_2ELHD,axiom,( ! [A_27a:del] : (mem@(c_2Ellist_2ELHD@A_27a)@(arr@(ty_2Ellist_2Ellist@A_27a)@(ty_2Eoption_2Eoption@A_27a))))).
thf(tp_c_2Ellist_2ELLENGTH,type,(c_2Ellist_2ELLENGTH:(del>$i))).
thf(mem_c_2Ellist_2ELLENGTH,axiom,( ! [A_27a:del] : (mem@(c_2Ellist_2ELLENGTH@A_27a)@(arr@(ty_2Ellist_2Ellist@A_27a)@(ty_2Eoption_2Eoption@ty_2Enum_2Enum))))).
thf(tp_c_2Ellist_2ELMAP,type,(c_2Ellist_2ELMAP:(del>(del>$i)))).
thf(mem_c_2Ellist_2ELMAP,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Ellist_2ELMAP@A_27a@A_27b)@(arr@(arr@A_27a@A_27b)@(arr@(ty_2Ellist_2Ellist@A_27a)@(ty_2Ellist_2Ellist@A_27b))))))).
thf(tp_c_2Ellist_2ELNIL,type,(c_2Ellist_2ELNIL:(del>$i))).
thf(mem_c_2Ellist_2ELNIL,axiom,( ! [A_27a:del] : (mem@(c_2Ellist_2ELNIL@A_27a)@(ty_2Ellist_2Ellist@A_27a)))).
thf(tp_c_2Ellist_2ELNTH,type,(c_2Ellist_2ELNTH:(del>$i))).
thf(mem_c_2Ellist_2ELNTH,axiom,( ! [A_27a:del] : (mem@(c_2Ellist_2ELNTH@A_27a)@(arr@ty_2Enum_2Enum@(arr@(ty_2Ellist_2Ellist@A_27a)@(ty_2Eoption_2Eoption@A_27a)))))).
thf(tp_c_2Ellist_2ELPREFIX,type,(c_2Ellist_2ELPREFIX:(del>$i))).
thf(mem_c_2Ellist_2ELPREFIX,axiom,( ! [A_27a:del] : (mem@(c_2Ellist_2ELPREFIX@A_27a)@(arr@(ty_2Ellist_2Ellist@A_27a)@(arr@(ty_2Ellist_2Ellist@A_27a)@bool))))).
thf(tp_c_2Ellist_2ELREPEAT,type,(c_2Ellist_2ELREPEAT:(del>$i))).
thf(mem_c_2Ellist_2ELREPEAT,axiom,( ! [A_27a:del] : (mem@(c_2Ellist_2ELREPEAT@A_27a)@(arr@(ty_2Elist_2Elist@A_27a)@(ty_2Ellist_2Ellist@A_27a))))).
thf(tp_c_2Ellist_2ELTAKE,type,(c_2Ellist_2ELTAKE:(del>$i))).
thf(mem_c_2Ellist_2ELTAKE,axiom,( ! [A_27a:del] : (mem@(c_2Ellist_2ELTAKE@A_27a)@(arr@ty_2Enum_2Enum@(arr@(ty_2Ellist_2Ellist@A_27a)@(ty_2Eoption_2Eoption@(ty_2Elist_2Elist@A_27a))))))).
thf(tp_c_2Ellist_2ELTL,type,(c_2Ellist_2ELTL:(del>$i))).
thf(mem_c_2Ellist_2ELTL,axiom,( ! [A_27a:del] : (mem@(c_2Ellist_2ELTL@A_27a)@(arr@(ty_2Ellist_2Ellist@A_27a)@(ty_2Eoption_2Eoption@(ty_2Ellist_2Ellist@A_27a)))))).
thf(tp_c_2Ellist_2ELTL__HD,type,(c_2Ellist_2ELTL__HD:(del>$i))).
thf(mem_c_2Ellist_2ELTL__HD,axiom,( ! [A_27a:del] : (mem@(c_2Ellist_2ELTL__HD@A_27a)@(arr@(ty_2Ellist_2Ellist@A_27a)@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@(ty_2Ellist_2Ellist@A_27a)@A_27a)))))).
thf(tp_c_2Ellist_2ELUNFOLD,type,(c_2Ellist_2ELUNFOLD:(del>(del>$i)))).
thf(mem_c_2Ellist_2ELUNFOLD,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Ellist_2ELUNFOLD@A_27a@A_27b)@(arr@(arr@A_27b@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@A_27b@A_27a)))@(arr@A_27b@(ty_2Ellist_2Ellist@A_27a))))))).
thf(tp_c_2Ellist_2ELUNZIP,type,(c_2Ellist_2ELUNZIP:(del>(del>$i)))).
thf(mem_c_2Ellist_2ELUNZIP,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Ellist_2ELUNZIP@A_27a@A_27b)@(arr@(ty_2Ellist_2Ellist@(ty_2Epair_2Eprod@A_27a@A_27b))@(ty_2Epair_2Eprod@(ty_2Ellist_2Ellist@A_27a)@(ty_2Ellist_2Ellist@A_27b))))))).
thf(tp_c_2Ellist_2ELZIP,type,(c_2Ellist_2ELZIP:(del>(del>$i)))).
thf(mem_c_2Ellist_2ELZIP,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Ellist_2ELZIP@A_27a@A_27b)@(arr@(ty_2Epair_2Eprod@(ty_2Ellist_2Ellist@A_27a)@(ty_2Ellist_2Ellist@A_27b))@(ty_2Ellist_2Ellist@(ty_2Epair_2Eprod@A_27a@A_27b))))))).
thf(tp_c_2Ellist_2Eevery,type,(c_2Ellist_2Eevery:(del>$i))).
thf(mem_c_2Ellist_2Eevery,axiom,( ! [A_27a:del] : (mem@(c_2Ellist_2Eevery@A_27a)@(arr@(arr@A_27a@bool)@(arr@(ty_2Ellist_2Ellist@A_27a)@bool))))).
thf(tp_c_2Ellist_2Eexists,type,(c_2Ellist_2Eexists:(del>$i))).
thf(mem_c_2Ellist_2Eexists,axiom,( ! [A_27a:del] : (mem@(c_2Ellist_2Eexists@A_27a)@(arr@(arr@A_27a@bool)@(arr@(ty_2Ellist_2Ellist@A_27a)@bool))))).
thf(tp_c_2Ellist_2EfromList,type,(c_2Ellist_2EfromList:(del>$i))).
thf(mem_c_2Ellist_2EfromList,axiom,( ! [A_27a:del] : (mem@(c_2Ellist_2EfromList@A_27a)@(arr@(ty_2Elist_2Elist@A_27a)@(ty_2Ellist_2Ellist@A_27a))))).
thf(tp_c_2Ellist_2Elinear__order__to__list__f,type,(c_2Ellist_2Elinear__order__to__list__f:(del>$i))).
thf(mem_c_2Ellist_2Elinear__order__to__list__f,axiom,( ! [A_27a:del] : (mem@(c_2Ellist_2Elinear__order__to__list__f@A_27a)@(arr@(arr@(ty_2Epair_2Eprod@A_27a@A_27a)@bool)@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@(arr@(ty_2Epair_2Eprod@A_27a@A_27a)@bool)@A_27a)))))).
thf(tp_c_2Ellist_2Ellength__rel,type,(c_2Ellist_2Ellength__rel:(del>$i))).
thf(mem_c_2Ellist_2Ellength__rel,axiom,( ! [A_27a:del] : (mem@(c_2Ellist_2Ellength__rel@A_27a)@(arr@(ty_2Ellist_2Ellist@A_27a)@(arr@ty_2Enum_2Enum@bool))))).
thf(tp_c_2Ellist_2Ellist__abs,type,(c_2Ellist_2Ellist__abs:(del>$i))).
thf(mem_c_2Ellist_2Ellist__abs,axiom,( ! [A_27a:del] : (mem@(c_2Ellist_2Ellist__abs@A_27a)@(arr@(arr@ty_2Enum_2Enum@(ty_2Eoption_2Eoption@A_27a))@(ty_2Ellist_2Ellist@A_27a))))).
thf(tp_c_2Ellist_2Ellist__rep,type,(c_2Ellist_2Ellist__rep:(del>$i))).
thf(mem_c_2Ellist_2Ellist__rep,axiom,( ! [A_27a:del] : (mem@(c_2Ellist_2Ellist__rep@A_27a)@(arr@(ty_2Ellist_2Ellist@A_27a)@(arr@ty_2Enum_2Enum@(ty_2Eoption_2Eoption@A_27a)))))).
thf(tp_c_2Ellist_2Elrep__ok,type,(c_2Ellist_2Elrep__ok:(del>$i))).
thf(mem_c_2Ellist_2Elrep__ok,axiom,( ! [A_27a:del] : (mem@(c_2Ellist_2Elrep__ok@A_27a)@(arr@(arr@ty_2Enum_2Enum@(ty_2Eoption_2Eoption@A_27a))@bool)))).
thf(tp_c_2Ellist_2EtoList,type,(c_2Ellist_2EtoList:(del>$i))).
thf(mem_c_2Ellist_2EtoList,axiom,( ! [A_27a:del] : (mem@(c_2Ellist_2EtoList@A_27a)@(arr@(ty_2Ellist_2Ellist@A_27a)@(ty_2Eoption_2Eoption@(ty_2Elist_2Elist@A_27a)))))).
thf(ax_thm_2Ellist_2Elrep__ok__def,axiom,( ! [A_27a:del]: ((c_2Ellist_2Elrep__ok@A_27a) = (lam@(arr@ty_2Enum_2Enum@(ty_2Eoption_2Eoption@A_27a))@(^ [V0a0:$i] : (ap@(c_2Ebool_2E_3F@(arr@(arr@ty_2Enum_2Enum@(ty_2Eoption_2Eoption@A_27a))@bool))@(lam@(arr@(arr@ty_2Enum_2Enum@(ty_2Eoption_2Eoption@A_27a))@bool)@(^ [V1lrep__ok_27:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V1lrep__ok_27@V0a0))@(ap@(c_2Ebool_2E_21@(arr@ty_2Enum_2Enum@(ty_2Eoption_2Eoption@A_27a)))@(lam@(arr@ty_2Enum_2Enum@(ty_2Eoption_2Eoption@A_27a))@(^ [V2a0:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@V1lrep__ok_27@V2a0))@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@(c_2Emin_2E_3D@(arr@ty_2Enum_2Enum@(ty_2Eoption_2Eoption@A_27a)))@V2a0)@(lam@ty_2Enum_2Enum@(^ [V3n:$i] : (c_2Eoption_2ENONE@A_27a)))))@(ap@(c_2Ebool_2E_3F@A_27a)@(lam@A_27a@(^ [V4h:$i] : (ap@(c_2Ebool_2E_3F@(arr@ty_2Enum_2Enum@(ty_2Eoption_2Eoption@A_27a)))@(lam@(arr@ty_2Enum_2Enum@(ty_2Eoption_2Eoption@A_27a))@(^ [V5t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Emin_2E_3D@(arr@ty_2Enum_2Enum@(ty_2Eoption_2Eoption@A_27a)))@V2a0)@(lam@ty_2Enum_2Enum@(^ [V6n:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@A_27a))@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@V6n)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@(c_2Eoption_2ESOME@A_27a)@V4h))@(ap@V5t@(ap@(ap@c_2Earithmetic_2E_2D@V6n)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))@(ap@V1lrep__ok_27@V5t)))))))))))))))))))))).
thf(conj_thm_2Ellist_2Elrep__ok__rules,lemma,( ! [A_27a:del]: ((p@(ap@(c_2Ellist_2Elrep__ok@A_27a)@(lam@ty_2Enum_2Enum@(^ [V0n:$i] : (c_2Eoption_2ENONE@A_27a))))) & ( ! [V1h:$i] : ((mem@V1h@A_27a) => ( ! [V2t:$i] : ((mem@V2t@(arr@ty_2Enum_2Enum@(ty_2Eoption_2Eoption@A_27a))) => ((p@(ap@(c_2Ellist_2Elrep__ok@A_27a)@V2t)) => (p@(ap@(c_2Ellist_2Elrep__ok@A_27a)@(lam@ty_2Enum_2Enum@(^ [V3n:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@A_27a))@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@V3n)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@(c_2Eoption_2ESOME@A_27a)@V1h))@(ap@V2t@(ap@(ap@c_2Earithmetic_2E_2D@V3n)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))))))))).
thf(conj_thm_2Ellist_2Elrep__ok__coind,lemma,( ! [A_27a:del]: ( ! [V0lrep__ok_27:$i] : ((mem@V0lrep__ok_27@(arr@(arr@ty_2Enum_2Enum@(ty_2Eoption_2Eoption@A_27a))@bool)) => (( ! [V1a0:$i] : ((mem@V1a0@(arr@ty_2Enum_2Enum@(ty_2Eoption_2Eoption@A_27a))) => ((p@(ap@V0lrep__ok_27@V1a0)) => ((V1a0 = (lam@ty_2Enum_2Enum@(^ [V2n:$i] : (c_2Eoption_2ENONE@A_27a)))) | (? [V3h:$i] : ((mem@V3h@A_27a) & (? [V4t:$i] : ((mem@V4t@(arr@ty_2Enum_2Enum@(ty_2Eoption_2Eoption@A_27a))) & ((V1a0 = (lam@ty_2Enum_2Enum@(^ [V5n:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@A_27a))@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@V5n)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@(c_2Eoption_2ESOME@A_27a)@V3h))@(ap@V4t@(ap@(ap@c_2Earithmetic_2E_2D@V5n)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))) & (p@(ap@V0lrep__ok_27@V4t))))))))))) => ( ! [V6a0:$i] : ((mem@V6a0@(arr@ty_2Enum_2Enum@(ty_2Eoption_2Eoption@A_27a))) => ((p@(ap@V0lrep__ok_27@V6a0)) => (p@(ap@(c_2Ellist_2Elrep__ok@A_27a)@V6a0)))))))))).
thf(conj_thm_2Ellist_2Elrep__ok__cases,lemma,( ! [A_27a:del]: ( ! [V0a0:$i] : ((mem@V0a0@(arr@ty_2Enum_2Enum@(ty_2Eoption_2Eoption@A_27a))) => ((p@(ap@(c_2Ellist_2Elrep__ok@A_27a)@V0a0)) <=> ((V0a0 = (lam@ty_2Enum_2Enum@(^ [V1n:$i] : (c_2Eoption_2ENONE@A_27a)))) | (? [V2h:$i] : ((mem@V2h@A_27a) & (? [V3t:$i] : ((mem@V3t@(arr@ty_2Enum_2Enum@(ty_2Eoption_2Eoption@A_27a))) & ((V0a0 = (lam@ty_2Enum_2Enum@(^ [V4n:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@A_27a))@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@V4n)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@(c_2Eoption_2ESOME@A_27a)@V2h))@(ap@V3t@(ap@(ap@c_2Earithmetic_2E_2D@V4n)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))) & (p@(ap@(c_2Ellist_2Elrep__ok@A_27a)@V3t))))))))))))).
thf(conj_thm_2Ellist_2Elrep__ok__alt,lemma,( ! [A_27a:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@ty_2Enum_2Enum@(ty_2Eoption_2Eoption@A_27a))) => ((p@(ap@(c_2Ellist_2Elrep__ok@A_27a)@V0f)) <=> ( ! [V1n:tp__ty_2Enum_2Enum] : ((p@(ap@(c_2Eoption_2EIS__SOME@A_27a)@(ap@V0f@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n))))) => (p@(ap@(c_2Eoption_2EIS__SOME@A_27a)@(ap@V0f@(inj__ty_2Enum_2Enum @ V1n))))))))))).
thf(ax_thm_2Ellist_2Ellist__TY__DEF,axiom,( ! [A_27a:del]: (? [V0rep:$i] : ((mem@V0rep@(arr@(ty_2Ellist_2Ellist@A_27a)@(arr@ty_2Enum_2Enum@(ty_2Eoption_2Eoption@A_27a)))) & (p@(ap@(ap@(c_2Ebool_2ETYPE__DEFINITION@(arr@ty_2Enum_2Enum@(ty_2Eoption_2Eoption@A_27a))@(ty_2Ellist_2Ellist@A_27a))@(c_2Ellist_2Elrep__ok@A_27a))@V0rep)))))).
thf(ax_thm_2Ellist_2Ellist__absrep,axiom,( ! [A_27a:del]: (( ! [V0a:$i] : ((mem@V0a@(ty_2Ellist_2Ellist@A_27a)) => ((ap@(c_2Ellist_2Ellist__abs@A_27a)@(ap@(c_2Ellist_2Ellist__rep@A_27a)@V0a)) = V0a))) & ( ! [V1r:$i] : ((mem@V1r@(arr@ty_2Enum_2Enum@(ty_2Eoption_2Eoption@A_27a))) => ((p@(ap@(c_2Ellist_2Elrep__ok@A_27a)@V1r)) <=> ((ap@(c_2Ellist_2Ellist__rep@A_27a)@(ap@(c_2Ellist_2Ellist__abs@A_27a)@V1r)) = V1r))))))).
thf(conj_thm_2Ellist_2Elrep__ok__MAP,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27b@A_27a)) => ( ! [V1g:$i] : ((mem@V1g@(arr@ty_2Enum_2Enum@(ty_2Eoption_2Eoption@A_27b))) => ((p@(ap@(c_2Ellist_2Elrep__ok@A_27a)@(lam@ty_2Enum_2Enum@(^ [V2n:$i] : (ap@(ap@(c_2Eoption_2EOPTION__MAP@A_27b@A_27a)@V0f)@(ap@V1g@V2n)))))) <=> (p@(ap@(c_2Ellist_2Elrep__ok@A_27b)@V1g)))))))))).
thf(conj_thm_2Ellist_2Elrep__ok__FUNPOW__BIND,lemma,( ! [A_27a:del]: ( ! [V0g:$i] : ((mem@V0g@(arr@A_27a@(ty_2Eoption_2Eoption@A_27a))) => ( ! [V1fz:$i] : ((mem@V1fz@(ty_2Eoption_2Eoption@A_27a)) => (p@(ap@(c_2Ellist_2Elrep__ok@A_27a)@(lam@ty_2Enum_2Enum@(^ [V2n:$i] : (ap@(ap@(ap@(c_2Earithmetic_2EFUNPOW@(ty_2Eoption_2Eoption@A_27a))@(lam@(ty_2Eoption_2Eoption@A_27a)@(^ [V3m:$i] : (ap@(ap@(c_2Eoption_2EOPTION__BIND@A_27a@A_27a)@V3m)@V0g))))@V2n)@V1fz))))))))))).
thf(ax_thm_2Ellist_2ELNIL,axiom,( ! [A_27a:del]: ((c_2Ellist_2ELNIL@A_27a) = (ap@(c_2Ellist_2Ellist__abs@A_27a)@(lam@ty_2Enum_2Enum@(^ [V0n:$i] : (c_2Eoption_2ENONE@A_27a))))))).
thf(ax_thm_2Ellist_2ELCONS,axiom,( ! [A_27a:del]: ( ! [V0h:$i] : ((mem@V0h@A_27a) => ( ! [V1t:$i] : ((mem@V1t@(ty_2Ellist_2Ellist@A_27a)) => ((ap@(ap@(c_2Ellist_2ELCONS@A_27a)@V0h)@V1t) = (ap@(c_2Ellist_2Ellist__abs@A_27a)@(lam@ty_2Enum_2Enum@(^ [V2n:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@A_27a))@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@V2n)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@(c_2Eoption_2ESOME@A_27a)@V0h))@(ap@(ap@(c_2Ellist_2Ellist__rep@A_27a)@V1t)@(ap@(ap@c_2Earithmetic_2E_2D@V2n)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))))))))).
thf(conj_thm_2Ellist_2Ellist__rep__LCONS,lemma,( ! [A_27a:del]: ( ! [V0h:$i] : ((mem@V0h@A_27a) => ( ! [V1t:$i] : ((mem@V1t@(ty_2Ellist_2Ellist@A_27a)) => ((ap@(c_2Ellist_2Ellist__rep@A_27a)@(ap@(ap@(c_2Ellist_2ELCONS@A_27a)@V0h)@V1t)) = (lam@ty_2Enum_2Enum@(^ [V2n:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@A_27a))@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@V2n)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(ap@(c_2Eoption_2ESOME@A_27a)@V0h))@(ap@(ap@(c_2Ellist_2Ellist__rep@A_27a)@V1t)@(ap@(ap@c_2Earithmetic_2E_2D@V2n)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))))))).
thf(conj_thm_2Ellist_2Ellist__rep__LNIL,lemma,( ! [A_27a:del]: ((ap@(c_2Ellist_2Ellist__rep@A_27a)@(c_2Ellist_2ELNIL@A_27a)) = (lam@ty_2Enum_2Enum@(^ [V0n:$i] : (c_2Eoption_2ENONE@A_27a)))))).
thf(ax_thm_2Ellist_2ELTL__HD__def,axiom,( ! [A_27a:del]: ( ! [V0ll:$i] : ((mem@V0ll@(ty_2Ellist_2Ellist@A_27a)) => ((ap@(c_2Ellist_2ELTL__HD@A_27a)@V0ll) = (ap@(ap@(ap@(c_2Eoption_2Eoption__CASE@A_27a@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@(ty_2Ellist_2Ellist@A_27a)@A_27a)))@(ap@(ap@(c_2Ellist_2Ellist__rep@A_27a)@V0ll)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))@(c_2Eoption_2ENONE@(ty_2Epair_2Eprod@(ty_2Ellist_2Ellist@A_27a)@A_27a)))@(lam@A_27a@(^ [V1h:$i] : (ap@(c_2Eoption_2ESOME@(ty_2Epair_2Eprod@(ty_2Ellist_2Ellist@A_27a)@A_27a))@(ap@(ap@(c_2Epair_2E_2C@(ty_2Ellist_2Ellist@A_27a)@A_27a)@(ap@(c_2Ellist_2Ellist__abs@A_27a)@(ap@(ap@(c_2Ecombin_2Eo@ty_2Enum_2Enum@(ty_2Eoption_2Eoption@A_27a)@ty_2Enum_2Enum)@(ap@(c_2Ellist_2Ellist__rep@A_27a)@V0ll))@c_2Enum_2ESUC)))@V1h)))))))))).
thf(conj_thm_2Ellist_2ELTL__HD__LNIL,lemma,( ! [A_27a:del]: ((ap@(c_2Ellist_2ELTL__HD@A_27a)@(c_2Ellist_2ELNIL@A_27a)) = (c_2Eoption_2ENONE@(ty_2Epair_2Eprod@(ty_2Ellist_2Ellist@A_27a)@A_27a))))).
thf(conj_thm_2Ellist_2ELTL__HD__LCONS,lemma,( ! [A_27a:del]: ( ! [V0h:$i] : ((mem@V0h@A_27a) => ( ! [V1t:$i] : ((mem@V1t@(ty_2Ellist_2Ellist@A_27a)) => ((ap@(c_2Ellist_2ELTL__HD@A_27a)@(ap@(ap@(c_2Ellist_2ELCONS@A_27a)@V0h)@V1t)) = (ap@(c_2Eoption_2ESOME@(ty_2Epair_2Eprod@(ty_2Ellist_2Ellist@A_27a)@A_27a))@(ap@(ap@(c_2Epair_2E_2C@(ty_2Ellist_2Ellist@A_27a)@A_27a)@V1t)@V0h))))))))).
thf(ax_thm_2Ellist_2ELHD,axiom,( ! [A_27a:del]: ( ! [V0ll:$i] : ((mem@V0ll@(ty_2Ellist_2Ellist@A_27a)) => ((ap@(c_2Ellist_2ELHD@A_27a)@V0ll) = (ap@(ap@(c_2Ellist_2Ellist__rep@A_27a)@V0ll)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))))).
thf(ax_thm_2Ellist_2ELTL,axiom,( ! [A_27a:del]: ( ! [V0ll:$i] : ((mem@V0ll@(ty_2Ellist_2Ellist@A_27a)) => ((ap@(c_2Ellist_2ELTL@A_27a)@V0ll) = (ap@(ap@(ap@(c_2Eoption_2Eoption__CASE@A_27a@(ty_2Eoption_2Eoption@(ty_2Ellist_2Ellist@A_27a)))@(ap@(c_2Ellist_2ELHD@A_27a)@V0ll))@(c_2Eoption_2ENONE@(ty_2Ellist_2Ellist@A_27a)))@(lam@A_27a@(^ [V1v:$i] : (ap@(c_2Eoption_2ESOME@(ty_2Ellist_2Ellist@A_27a))@(ap@(c_2Ellist_2Ellist__abs@A_27a)@(lam@ty_2Enum_2Enum@(^ [V2n:$i] : (ap@(ap@(c_2Ellist_2Ellist__rep@A_27a)@V0ll)@(ap@(ap@c_2Earithmetic_2E_2B@V2n)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))))))))).
thf(conj_thm_2Ellist_2ELTL__HD__HD,lemma,( ! [A_27a:del]: ( ! [V0ll:$i] : ((mem@V0ll@(ty_2Ellist_2Ellist@A_27a)) => ((ap@(c_2Ellist_2ELHD@A_27a)@V0ll) = (ap@(ap@(c_2Eoption_2EOPTION__MAP@(ty_2Epair_2Eprod@(ty_2Ellist_2Ellist@A_27a)@A_27a)@A_27a)@(c_2Epair_2ESND@(ty_2Ellist_2Ellist@A_27a)@A_27a))@(ap@(c_2Ellist_2ELTL__HD@A_27a)@V0ll))))))).
thf(conj_thm_2Ellist_2ELTL__HD__TL,lemma,( ! [A_27a:del]: ( ! [V0ll:$i] : ((mem@V0ll@(ty_2Ellist_2Ellist@A_27a)) => ((ap@(c_2Ellist_2ELTL@A_27a)@V0ll) = (ap@(ap@(c_2Eoption_2EOPTION__MAP@(ty_2Epair_2Eprod@(ty_2Ellist_2Ellist@A_27a)@A_27a)@(ty_2Ellist_2Ellist@A_27a))@(c_2Epair_2EFST@(ty_2Ellist_2Ellist@A_27a)@A_27a))@(ap@(c_2Ellist_2ELTL__HD@A_27a)@V0ll))))))).
thf(conj_thm_2Ellist_2ELHD__LCONS,lemma,( ! [A_27a:del]: ( ! [V0h:$i] : ((mem@V0h@A_27a) => ( ! [V1t:$i] : ((mem@V1t@(ty_2Ellist_2Ellist@A_27a)) => ((ap@(c_2Ellist_2ELHD@A_27a)@(ap@(ap@(c_2Ellist_2ELCONS@A_27a)@V0h)@V1t)) = (ap@(c_2Eoption_2ESOME@A_27a)@V0h)))))))).
thf(conj_thm_2Ellist_2ELTL__LCONS,lemma,( ! [A_27a:del]: ( ! [V0h:$i] : ((mem@V0h@A_27a) => ( ! [V1t:$i] : ((mem@V1t@(ty_2Ellist_2Ellist@A_27a)) => ((ap@(c_2Ellist_2ELTL@A_27a)@(ap@(ap@(c_2Ellist_2ELCONS@A_27a)@V0h)@V1t)) = (ap@(c_2Eoption_2ESOME@(ty_2Ellist_2Ellist@A_27a))@V1t)))))))).
thf(conj_thm_2Ellist_2ELHDTL__CONS__THM,lemma,( ! [A_27a:del]: ( ! [V0h:$i] : ((mem@V0h@A_27a) => ( ! [V1t:$i] : ((mem@V1t@(ty_2Ellist_2Ellist@A_27a)) => (((ap@(c_2Ellist_2ELHD@A_27a)@(ap@(ap@(c_2Ellist_2ELCONS@A_27a)@V0h)@V1t)) = (ap@(c_2Eoption_2ESOME@A_27a)@V0h)) & ((ap@(c_2Ellist_2ELTL@A_27a)@(ap@(ap@(c_2Ellist_2ELCONS@A_27a)@V0h)@V1t)) = (ap@(c_2Eoption_2ESOME@(ty_2Ellist_2Ellist@A_27a))@V1t))))))))).
thf(conj_thm_2Ellist_2Ellist__CASES,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Ellist_2Ellist@A_27a)) => ((V0l = (c_2Ellist_2ELNIL@A_27a)) | (? [V1h:$i] : ((mem@V1h@A_27a) & (? [V2t:$i] : ((mem@V2t@(ty_2Ellist_2Ellist@A_27a)) & (V0l = (ap@(ap@(c_2Ellist_2ELCONS@A_27a)@V1h)@V2t))))))))))).
thf(conj_thm_2Ellist_2ELTL__HD__11,lemma,( ! [A_27a:del]: ( ! [V0ll1:$i] : ((mem@V0ll1@(ty_2Ellist_2Ellist@A_27a)) => ( ! [V1ll2:$i] : ((mem@V1ll2@(ty_2Ellist_2Ellist@A_27a)) => (((ap@(c_2Ellist_2ELTL__HD@A_27a)@V0ll1) = (ap@(c_2Ellist_2ELTL__HD@A_27a)@V1ll2)) => (V0ll1 = V1ll2)))))))).
thf(conj_thm_2Ellist_2ELHD__THM,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: (((ap@(c_2Ellist_2ELHD@A_27a)@(c_2Ellist_2ELNIL@A_27a)) = (c_2Eoption_2ENONE@A_27a)) & ( ! [V0h:$i] : ((mem@V0h@A_27b) => ( ! [V1t:$i] : ((mem@V1t@(ty_2Ellist_2Ellist@A_27b)) => ((ap@(c_2Ellist_2ELHD@A_27b)@(ap@(ap@(c_2Ellist_2ELCONS@A_27b)@V0h)@V1t)) = (ap@(c_2Eoption_2ESOME@A_27b)@V0h)))))))))).
thf(conj_thm_2Ellist_2ELTL__THM,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: (((ap@(c_2Ellist_2ELTL@A_27a)@(c_2Ellist_2ELNIL@A_27a)) = (c_2Eoption_2ENONE@(ty_2Ellist_2Ellist@A_27a))) & ( ! [V0h:$i] : ((mem@V0h@A_27b) => ( ! [V1t:$i] : ((mem@V1t@(ty_2Ellist_2Ellist@A_27b)) => ((ap@(c_2Ellist_2ELTL@A_27b)@(ap@(ap@(c_2Ellist_2ELCONS@A_27b)@V0h)@V1t)) = (ap@(c_2Eoption_2ESOME@(ty_2Ellist_2Ellist@A_27b))@V1t)))))))))).
thf(conj_thm_2Ellist_2ELCONS__NOT__NIL,lemma,( ! [A_27a:del]: ( ! [V0h:$i] : ((mem@V0h@A_27a) => ( ! [V1t:$i] : ((mem@V1t@(ty_2Ellist_2Ellist@A_27a)) => ((~~ ((ap@(ap@(c_2Ellist_2ELCONS@A_27a)@V0h)@V1t) = (c_2Ellist_2ELNIL@A_27a))) & (~~ ((c_2Ellist_2ELNIL@A_27a) = (ap@(ap@(c_2Ellist_2ELCONS@A_27a)@V0h)@V1t)))))))))).
thf(conj_thm_2Ellist_2ELCONS__11,lemma,( ! [A_27a:del]: ( ! [V0h1:$i] : ((mem@V0h1@A_27a) => ( ! [V1t1:$i] : ((mem@V1t1@(ty_2Ellist_2Ellist@A_27a)) => ( ! [V2h2:$i] : ((mem@V2h2@A_27a) => ( ! [V3t2:$i] : ((mem@V3t2@(ty_2Ellist_2Ellist@A_27a)) => (((ap@(ap@(c_2Ellist_2ELCONS@A_27a)@V0h1)@V1t1) = (ap@(ap@(c_2Ellist_2ELCONS@A_27a)@V2h2)@V3t2)) <=> ((V0h1 = V2h2) & (V1t1 = V3t2))))))))))))).
thf(conj_thm_2Ellist_2ELTL__HD__iff,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@(ty_2Ellist_2Ellist@A_27a)) => ( ! [V1t:$i] : ((mem@V1t@(ty_2Ellist_2Ellist@A_27a)) => ( ! [V2h:$i] : ((mem@V2h@A_27a) => ((((ap@(c_2Ellist_2ELTL__HD@A_27a)@V0x) = (ap@(c_2Eoption_2ESOME@(ty_2Epair_2Eprod@(ty_2Ellist_2Ellist@A_27a)@A_27a))@(ap@(ap@(c_2Epair_2E_2C@(ty_2Ellist_2Ellist@A_27a)@A_27a)@V1t)@V2h))) <=> (V0x = (ap@(ap@(c_2Ellist_2ELCONS@A_27a)@V2h)@V1t))) & (((ap@(c_2Ellist_2ELTL__HD@A_27a)@V0x) = (c_2Eoption_2ENONE@(ty_2Epair_2Eprod@(ty_2Ellist_2Ellist@A_27a)@A_27a))) <=> (V0x = (c_2Ellist_2ELNIL@A_27a)))))))))))).
thf(conj_thm_2Ellist_2ELHD__EQ__NONE,lemma,( ! [A_27a:del]: ( ! [V0ll:$i] : ((mem@V0ll@(ty_2Ellist_2Ellist@A_27a)) => ((((ap@(c_2Ellist_2ELHD@A_27a)@V0ll) = (c_2Eoption_2ENONE@A_27a)) <=> (V0ll = (c_2Ellist_2ELNIL@A_27a))) & (((c_2Eoption_2ENONE@A_27a) = (ap@(c_2Ellist_2ELHD@A_27a)@V0ll)) <=> (V0ll = (c_2Ellist_2ELNIL@A_27a)))))))).
thf(conj_thm_2Ellist_2ELTL__EQ__NONE,lemma,( ! [A_27a:del]: ( ! [V0ll:$i] : ((mem@V0ll@(ty_2Ellist_2Ellist@A_27a)) => ((((ap@(c_2Ellist_2ELTL@A_27a)@V0ll) = (c_2Eoption_2ENONE@(ty_2Ellist_2Ellist@A_27a))) <=> (V0ll = (c_2Ellist_2ELNIL@A_27a))) & (((c_2Eoption_2ENONE@(ty_2Ellist_2Ellist@A_27a)) = (ap@(c_2Ellist_2ELTL@A_27a)@V0ll)) <=> (V0ll = (c_2Ellist_2ELNIL@A_27a)))))))).
thf(conj_thm_2Ellist_2ELHDTL__EQ__SOME,lemma,( ! [A_27a:del]: ( ! [V0h:$i] : ((mem@V0h@A_27a) => ( ! [V1t:$i] : ((mem@V1t@(ty_2Ellist_2Ellist@A_27a)) => ( ! [V2ll:$i] : ((mem@V2ll@(ty_2Ellist_2Ellist@A_27a)) => ((V2ll = (ap@(ap@(c_2Ellist_2ELCONS@A_27a)@V0h)@V1t)) <=> (((ap@(c_2Ellist_2ELHD@A_27a)@V2ll) = (ap@(c_2Eoption_2ESOME@A_27a)@V0h)) & ((ap@(c_2Ellist_2ELTL@A_27a)@V2ll) = (ap@(c_2Eoption_2ESOME@(ty_2Ellist_2Ellist@A_27a))@V1t)))))))))))).
thf(ax_thm_2Ellist_2ELNTH,axiom,( ! [A_27a:del]: (( ! [V0ll:$i] : ((mem@V0ll@(ty_2Ellist_2Ellist@A_27a)) => ((ap@(ap@(c_2Ellist_2ELNTH@A_27a)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@V0ll) = (ap@(c_2Ellist_2ELHD@A_27a)@V0ll)))) & ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2ll:$i] : ((mem@V2ll@(ty_2Ellist_2Ellist@A_27a)) => ((ap@(ap@(c_2Ellist_2ELNTH@A_27a)@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n)))@V2ll) = (ap@(c_2Eoption_2EOPTION__JOIN@A_27a)@(ap@(ap@(c_2Eoption_2EOPTION__MAP@(ty_2Ellist_2Ellist@A_27a)@(ty_2Eoption_2Eoption@A_27a))@(ap@(c_2Ellist_2ELNTH@A_27a)@(inj__ty_2Enum_2Enum @ V1n)))@(ap@(c_2Ellist_2ELTL@A_27a)@V2ll)))))))))).
thf(conj_thm_2Ellist_2ELNTH__THM,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: (( ! [V0n:tp__ty_2Enum_2Enum] : ((ap@(ap@(c_2Ellist_2ELNTH@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@(c_2Ellist_2ELNIL@A_27a)) = (c_2Eoption_2ENONE@A_27a))) & (( ! [V1h:$i] : ((mem@V1h@A_27b) => ( ! [V2t:$i] : ((mem@V2t@(ty_2Ellist_2Ellist@A_27b)) => ((ap@(ap@(c_2Ellist_2ELNTH@A_27b)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@(ap@(c_2Ellist_2ELCONS@A_27b)@V1h)@V2t)) = (ap@(c_2Eoption_2ESOME@A_27b)@V1h)))))) & ( ! [V3n:tp__ty_2Enum_2Enum] : ( ! [V4h:$i] : ((mem@V4h@A_27c) => ( ! [V5t:$i] : ((mem@V5t@(ty_2Ellist_2Ellist@A_27c)) => ((ap@(ap@(c_2Ellist_2ELNTH@A_27c)@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V3n)))@(ap@(ap@(c_2Ellist_2ELCONS@A_27c)@V4h)@V5t)) = (ap@(ap@(c_2Ellist_2ELNTH@A_27c)@(inj__ty_2Enum_2Enum @ V3n))@V5t))))))))))))).
thf(conj_thm_2Ellist_2ELNTH__rep,lemma,( ! [A_27a:del]: ( ! [V0i:tp__ty_2Enum_2Enum] : ( ! [V1ll:$i] : ((mem@V1ll@(ty_2Ellist_2Ellist@A_27a)) => ((ap@(ap@(c_2Ellist_2ELNTH@A_27a)@(inj__ty_2Enum_2Enum @ V0i))@V1ll) = (ap@(ap@(c_2Ellist_2Ellist__rep@A_27a)@V1ll)@(inj__ty_2Enum_2Enum @ V0i)))))))).
thf(conj_thm_2Ellist_2ELNTH__EQ,lemma,( ! [A_27a:del]: ( ! [V0ll1:$i] : ((mem@V0ll1@(ty_2Ellist_2Ellist@A_27a)) => ( ! [V1ll2:$i] : ((mem@V1ll2@(ty_2Ellist_2Ellist@A_27a)) => ((V0ll1 = V1ll2) <=> ( ! [V2n:tp__ty_2Enum_2Enum] : ((ap@(ap@(c_2Ellist_2ELNTH@A_27a)@(inj__ty_2Enum_2Enum @ V2n))@V0ll1) = (ap@(ap@(c_2Ellist_2ELNTH@A_27a)@(inj__ty_2Enum_2Enum @ V2n))@V1ll2)))))))))).
thf(ax_thm_2Ellist_2ELUNFOLD__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27b@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@A_27b@A_27a)))) => ( ! [V1z:$i] : ((mem@V1z@A_27b) => ((ap@(ap@(c_2Ellist_2ELUNFOLD@A_27a@A_27b)@V0f)@V1z) = (ap@(c_2Ellist_2Ellist__abs@A_27a)@(lam@ty_2Enum_2Enum@(^ [V2n:$i] : (ap@(ap@(c_2Eoption_2EOPTION__MAP@(ty_2Epair_2Eprod@A_27b@A_27a)@A_27a)@(c_2Epair_2ESND@A_27b@A_27a))@(ap@(ap@(ap@(c_2Earithmetic_2EFUNPOW@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@A_27b@A_27a)))@(lam@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@A_27b@A_27a))@(^ [V3m:$i] : (ap@(ap@(c_2Eoption_2EOPTION__BIND@(ty_2Epair_2Eprod@A_27b@A_27a)@(ty_2Epair_2Eprod@A_27b@A_27a))@V3m)@(ap@(c_2Epair_2EUNCURRY@A_27b@A_27a@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@A_27b@A_27a)))@(ap@(ap@(c_2Ecombin_2Eo@A_27b@(arr@A_27a@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@A_27b@A_27a)))@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@A_27b@A_27a)))@(c_2Ecombin_2EK@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@A_27b@A_27a))@A_27a))@V0f))))))@V2n)@(ap@V0f@V1z)))))))))))))).
thf(conj_thm_2Ellist_2ELUNFOLD,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@A_27a@A_27b)))) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ((ap@(ap@(c_2Ellist_2ELUNFOLD@A_27b@A_27a)@V0f)@V1x) = (ap@(ap@(ap@(c_2Eoption_2Eoption__CASE@(ty_2Epair_2Eprod@A_27a@A_27b)@(ty_2Ellist_2Ellist@A_27b))@(ap@V0f@V1x))@(c_2Ellist_2ELNIL@A_27b))@(lam@(ty_2Epair_2Eprod@A_27a@A_27b)@(^ [V2v:$i] : (ap@(ap@(c_2Epair_2Epair__CASE@(ty_2Ellist_2Ellist@A_27b)@A_27a@A_27b)@V2v)@(lam@A_27a@(^ [V3v1:$i] : (lam@A_27b@(^ [V4v2:$i] : (ap@(ap@(c_2Ellist_2ELCONS@A_27b)@V4v2)@(ap@(ap@(c_2Ellist_2ELUNFOLD@A_27b@A_27a)@V0f)@V3v1)))))))))))))))))).
thf(conj_thm_2Ellist_2ELUNFOLD__UNIQUE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@A_27a@A_27b)))) => ( ! [V1g:$i] : ((mem@V1g@(arr@A_27a@(ty_2Ellist_2Ellist@A_27b))) => (( ! [V2x:$i] : ((mem@V2x@A_27a) => ((ap@V1g@V2x) = (ap@(ap@(ap@(c_2Eoption_2Eoption__CASE@(ty_2Epair_2Eprod@A_27a@A_27b)@(ty_2Ellist_2Ellist@A_27b))@(ap@V0f@V2x))@(c_2Ellist_2ELNIL@A_27b))@(lam@(ty_2Epair_2Eprod@A_27a@A_27b)@(^ [V3v:$i] : (ap@(ap@(c_2Epair_2Epair__CASE@(ty_2Ellist_2Ellist@A_27b)@A_27a@A_27b)@V3v)@(lam@A_27a@(^ [V4v1:$i] : (lam@A_27b@(^ [V5v2:$i] : (ap@(ap@(c_2Ellist_2ELCONS@A_27b)@V5v2)@(ap@V1g@V4v1))))))))))))) => ( ! [V6y:$i] : ((mem@V6y@A_27a) => ((ap@V1g@V6y) = (ap@(ap@(c_2Ellist_2ELUNFOLD@A_27b@A_27a)@V0f)@V6y)))))))))))).
thf(conj_thm_2Ellist_2ELUNFOLD__LTL__HD,lemma,( ! [A_27a:del]: ( ! [V0ll:$i] : ((mem@V0ll@(ty_2Ellist_2Ellist@A_27a)) => ((ap@(ap@(c_2Ellist_2ELUNFOLD@A_27a@(ty_2Ellist_2Ellist@A_27a))@(c_2Ellist_2ELTL__HD@A_27a))@V0ll) = V0ll))))).
thf(conj_thm_2Ellist_2ELTL__HD__LUNFOLD,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27b@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@A_27b@A_27a)))) => ( ! [V1x:$i] : ((mem@V1x@A_27b) => ((ap@(c_2Ellist_2ELTL__HD@A_27a)@(ap@(ap@(c_2Ellist_2ELUNFOLD@A_27a@A_27b)@V0f)@V1x)) = (ap@(ap@(c_2Eoption_2EOPTION__MAP@(ty_2Epair_2Eprod@A_27b@A_27a)@(ty_2Epair_2Eprod@(ty_2Ellist_2Ellist@A_27a)@A_27a))@(ap@(ap@(c_2Epair_2E_23_23@A_27b@A_27a@(ty_2Ellist_2Ellist@A_27a)@A_27a)@(ap@(c_2Ellist_2ELUNFOLD@A_27a@A_27b)@V0f))@(c_2Ecombin_2EI@A_27a)))@(ap@V0f@V1x)))))))))).
thf(conj_thm_2Ellist_2ELNTH__LUNFOLD,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27b@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@A_27b@A_27a)))) => ( ! [V1x:$i] : ((mem@V1x@A_27b) => ( ! [V2n:tp__ty_2Enum_2Enum] : (((ap@(ap@(c_2Ellist_2ELNTH@A_27a)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@(ap@(c_2Ellist_2ELUNFOLD@A_27a@A_27b)@V0f)@V1x)) = (ap@(ap@(c_2Eoption_2EOPTION__MAP@(ty_2Epair_2Eprod@A_27b@A_27a)@A_27a)@(c_2Epair_2ESND@A_27b@A_27a))@(ap@V0f@V1x))) & ((ap@(ap@(c_2Ellist_2ELNTH@A_27a)@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V2n)))@(ap@(ap@(c_2Ellist_2ELUNFOLD@A_27a@A_27b)@V0f)@V1x)) = (ap@(ap@(ap@(c_2Eoption_2Eoption__CASE@(ty_2Epair_2Eprod@A_27b@A_27a)@(ty_2Eoption_2Eoption@A_27a))@(ap@V0f@V1x))@(c_2Eoption_2ENONE@A_27a))@(lam@(ty_2Epair_2Eprod@A_27b@A_27a)@(^ [V3v:$i] : (ap@(ap@(c_2Epair_2Epair__CASE@(ty_2Eoption_2Eoption@A_27a)@A_27b@A_27a)@V3v)@(lam@A_27b@(^ [V4tx:$i] : (lam@A_27a@(^ [V5hx:$i] : (ap@(ap@(c_2Ellist_2ELNTH@A_27a)@(inj__ty_2Enum_2Enum @ V2n))@(ap@(ap@(c_2Ellist_2ELUNFOLD@A_27a@A_27b)@V0f)@V4tx)))))))))))))))))))).
thf(conj_thm_2Ellist_2ELNTH__LUNFOLD__compute,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27b@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@A_27b@A_27a)))) => ( ! [V1x:$i] : ((mem@V1x@A_27b) => (((ap@(ap@(c_2Ellist_2ELNTH@A_27a)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@(ap@(c_2Ellist_2ELUNFOLD@A_27a@A_27b)@V0f)@V1x)) = (ap@(ap@(c_2Eoption_2EOPTION__MAP@(ty_2Epair_2Eprod@A_27b@A_27a)@A_27a)@(c_2Epair_2ESND@A_27b@A_27a))@(ap@V0f@V1x))) & (( ! [V2n:tp__ty_2Enum_2Enum] : ((ap@(ap@(c_2Ellist_2ELNTH@A_27a)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V2n))))@(ap@(ap@(c_2Ellist_2ELUNFOLD@A_27a@A_27b)@V0f)@V1x)) = (ap@(ap@(ap@(c_2Eoption_2Eoption__CASE@(ty_2Epair_2Eprod@A_27b@A_27a)@(ty_2Eoption_2Eoption@A_27a))@(ap@V0f@V1x))@(c_2Eoption_2ENONE@A_27a))@(lam@(ty_2Epair_2Eprod@A_27b@A_27a)@(^ [V3v:$i] : (ap@(ap@(c_2Epair_2Epair__CASE@(ty_2Eoption_2Eoption@A_27a)@A_27b@A_27a)@V3v)@(lam@A_27b@(^ [V4tx:$i] : (lam@A_27a@(^ [V5hx:$i] : (ap@(ap@(c_2Ellist_2ELNTH@A_27a)@(ap@(ap@c_2Earithmetic_2E_2D@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V2n))))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@(ap@(ap@(c_2Ellist_2ELUNFOLD@A_27a@A_27b)@V0f)@V4tx)))))))))))) & ( ! [V6n:tp__ty_2Enum_2Enum] : ((ap@(ap@(c_2Ellist_2ELNTH@A_27a)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ V6n))))@(ap@(ap@(c_2Ellist_2ELUNFOLD@A_27a@A_27b)@V0f)@V1x)) = (ap@(ap@(ap@(c_2Eoption_2Eoption__CASE@(ty_2Epair_2Eprod@A_27b@A_27a)@(ty_2Eoption_2Eoption@A_27a))@(ap@V0f@V1x))@(c_2Eoption_2ENONE@A_27a))@(lam@(ty_2Epair_2Eprod@A_27b@A_27a)@(^ [V7v:$i] : (ap@(ap@(c_2Epair_2Epair__CASE@(ty_2Eoption_2Eoption@A_27a)@A_27b@A_27a)@V7v)@(lam@A_27b@(^ [V8tx:$i] : (lam@A_27a@(^ [V9hx:$i] : (ap@(ap@(c_2Ellist_2ELNTH@A_27a)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ V6n))))@(ap@(ap@(c_2Ellist_2ELUNFOLD@A_27a@A_27b)@V0f)@V8tx))))))))))))))))))))).
thf(conj_thm_2Ellist_2ELHD__LUNFOLD,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27b@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@A_27b@A_27a)))) => ( ! [V1x:$i] : ((mem@V1x@A_27b) => ((ap@(c_2Ellist_2ELHD@A_27a)@(ap@(ap@(c_2Ellist_2ELUNFOLD@A_27a@A_27b)@V0f)@V1x)) = (ap@(ap@(c_2Eoption_2EOPTION__MAP@(ty_2Epair_2Eprod@A_27b@A_27a)@A_27a)@(c_2Epair_2ESND@A_27b@A_27a))@(ap@V0f@V1x)))))))))).
thf(conj_thm_2Ellist_2ELTL__LUNFOLD,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27b@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@A_27b@A_27a)))) => ( ! [V1x:$i] : ((mem@V1x@A_27b) => ((ap@(c_2Ellist_2ELTL@A_27a)@(ap@(ap@(c_2Ellist_2ELUNFOLD@A_27a@A_27b)@V0f)@V1x)) = (ap@(ap@(c_2Eoption_2EOPTION__MAP@(ty_2Epair_2Eprod@A_27b@A_27a)@(ty_2Ellist_2Ellist@A_27a))@(ap@(ap@(c_2Ecombin_2Eo@(ty_2Epair_2Eprod@A_27b@A_27a)@(ty_2Ellist_2Ellist@A_27a)@A_27b)@(ap@(c_2Ellist_2ELUNFOLD@A_27a@A_27b)@V0f))@(c_2Epair_2EFST@A_27b@A_27a)))@(ap@V0f@V1x)))))))))).
thf(conj_thm_2Ellist_2Ellist__Axiom__1,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@A_27a@A_27b)))) => (? [V1g:$i] : ((mem@V1g@(arr@A_27a@(ty_2Ellist_2Ellist@A_27b))) & ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((ap@V1g@V2x) = (ap@(ap@(ap@(c_2Eoption_2Eoption__CASE@(ty_2Epair_2Eprod@A_27a@A_27b)@(ty_2Ellist_2Ellist@A_27b))@(ap@V0f@V2x))@(c_2Ellist_2ELNIL@A_27b))@(lam@(ty_2Epair_2Eprod@A_27a@A_27b)@(^ [V3v:$i] : (ap@(ap@(c_2Epair_2Epair__CASE@(ty_2Ellist_2Ellist@A_27b)@A_27a@A_27b)@V3v)@(lam@A_27a@(^ [V4a:$i] : (lam@A_27b@(^ [V5b:$i] : (ap@(ap@(c_2Ellist_2ELCONS@A_27b)@V5b)@(ap@V1g@V4a)))))))))))))))))))).
thf(conj_thm_2Ellist_2Ellist__Axiom__1ue,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@A_27a@A_27b)))) => (p@(ap@(c_2Ebool_2E_3F_21@(arr@A_27a@(ty_2Ellist_2Ellist@A_27b)))@(lam@(arr@A_27a@(ty_2Ellist_2Ellist@A_27b))@(^ [V1g:$i] : (ap@(c_2Ebool_2E_21@A_27a)@(lam@A_27a@(^ [V2x:$i] : (ap@(ap@(c_2Emin_2E_3D@(ty_2Ellist_2Ellist@A_27b))@(ap@V1g@V2x))@(ap@(ap@(ap@(c_2Eoption_2Eoption__CASE@(ty_2Epair_2Eprod@A_27a@A_27b)@(ty_2Ellist_2Ellist@A_27b))@(ap@V0f@V2x))@(c_2Ellist_2ELNIL@A_27b))@(lam@(ty_2Epair_2Eprod@A_27a@A_27b)@(^ [V3v:$i] : (ap@(ap@(c_2Epair_2Epair__CASE@(ty_2Ellist_2Ellist@A_27b)@A_27a@A_27b)@V3v)@(lam@A_27a@(^ [V4a:$i] : (lam@A_27b@(^ [V5b:$i] : (ap@(ap@(c_2Ellist_2ELCONS@A_27b)@V5b)@(ap@V1g@V4a))))))))))))))))))))))).
thf(conj_thm_2Ellist_2Ellist__ue__Axiom,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@A_27a@A_27b)))) => (p@(ap@(c_2Ebool_2E_3F_21@(arr@A_27a@(ty_2Ellist_2Ellist@A_27b)))@(lam@(arr@A_27a@(ty_2Ellist_2Ellist@A_27b))@(^ [V1g:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(c_2Ebool_2E_21@A_27a)@(lam@A_27a@(^ [V2x:$i] : (ap@(ap@(c_2Emin_2E_3D@(ty_2Eoption_2Eoption@A_27b))@(ap@(c_2Ellist_2ELHD@A_27b)@(ap@V1g@V2x)))@(ap@(ap@(c_2Eoption_2EOPTION__MAP@(ty_2Epair_2Eprod@A_27a@A_27b)@A_27b)@(c_2Epair_2ESND@A_27a@A_27b))@(ap@V0f@V2x)))))))@(ap@(c_2Ebool_2E_21@A_27a)@(lam@A_27a@(^ [V3x:$i] : (ap@(ap@(c_2Emin_2E_3D@(ty_2Eoption_2Eoption@(ty_2Ellist_2Ellist@A_27b)))@(ap@(c_2Ellist_2ELTL@A_27b)@(ap@V1g@V3x)))@(ap@(ap@(c_2Eoption_2EOPTION__MAP@(ty_2Epair_2Eprod@A_27a@A_27b)@(ty_2Ellist_2Ellist@A_27b))@(ap@(ap@(c_2Ecombin_2Eo@(ty_2Epair_2Eprod@A_27a@A_27b)@(ty_2Ellist_2Ellist@A_27b)@A_27a)@V1g)@(c_2Epair_2EFST@A_27a@A_27b)))@(ap@V0f@V3x)))))))))))))))).
thf(conj_thm_2Ellist_2Ellist__Axiom,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@A_27a@A_27b)))) => (? [V1g:$i] : ((mem@V1g@(arr@A_27a@(ty_2Ellist_2Ellist@A_27b))) & (( ! [V2x:$i] : ((mem@V2x@A_27a) => ((ap@(c_2Ellist_2ELHD@A_27b)@(ap@V1g@V2x)) = (ap@(ap@(c_2Eoption_2EOPTION__MAP@(ty_2Epair_2Eprod@A_27a@A_27b)@A_27b)@(c_2Epair_2ESND@A_27a@A_27b))@(ap@V0f@V2x))))) & ( ! [V3x:$i] : ((mem@V3x@A_27a) => ((ap@(c_2Ellist_2ELTL@A_27b)@(ap@V1g@V3x)) = (ap@(ap@(c_2Eoption_2EOPTION__MAP@(ty_2Epair_2Eprod@A_27a@A_27b)@(ty_2Ellist_2Ellist@A_27b))@(ap@(ap@(c_2Ecombin_2Eo@(ty_2Epair_2Eprod@A_27a@A_27b)@(ty_2Ellist_2Ellist@A_27b)@A_27a)@V1g)@(c_2Epair_2EFST@A_27a@A_27b)))@(ap@V0f@V3x))))))))))))).
thf(conj_thm_2Ellist_2ELUNFOLD__BISIMULATION,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f1:$i] : ((mem@V0f1@(arr@A_27a@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@A_27a@A_27b)))) => ( ! [V1f2:$i] : ((mem@V1f2@(arr@A_27c@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@A_27c@A_27b)))) => ( ! [V2x1:$i] : ((mem@V2x1@A_27a) => ( ! [V3x2:$i] : ((mem@V3x2@A_27c) => (((ap@(ap@(c_2Ellist_2ELUNFOLD@A_27b@A_27a)@V0f1)@V2x1) = (ap@(ap@(c_2Ellist_2ELUNFOLD@A_27b@A_27c)@V1f2)@V3x2)) <=> (? [V4R:$i] : ((mem@V4R@(arr@A_27a@(arr@A_27c@bool))) & ((p@(ap@(ap@V4R@V2x1)@V3x2)) & ( ! [V5y1:$i] : ((mem@V5y1@A_27a) => ( ! [V6y2:$i] : ((mem@V6y2@A_27c) => ((p@(ap@(ap@V4R@V5y1)@V6y2)) => ((((ap@V0f1@V5y1) = (c_2Eoption_2ENONE@(ty_2Epair_2Eprod@A_27a@A_27b))) & ((ap@V1f2@V6y2) = (c_2Eoption_2ENONE@(ty_2Epair_2Eprod@A_27c@A_27b)))) | (? [V7h:$i] : ((mem@V7h@A_27b) & (? [V8t1:$i] : ((mem@V8t1@A_27a) & (? [V9t2:$i] : ((mem@V9t2@A_27c) & (((ap@V0f1@V5y1) = (ap@(c_2Eoption_2ESOME@(ty_2Epair_2Eprod@A_27a@A_27b))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V8t1)@V7h))) & (((ap@V1f2@V6y2) = (ap@(c_2Eoption_2ESOME@(ty_2Epair_2Eprod@A_27c@A_27b))@(ap@(ap@(c_2Epair_2E_2C@A_27c@A_27b)@V9t2)@V7h))) & (p@(ap@(ap@V4R@V8t1)@V9t2)))))))))))))))))))))))))))))))).
thf(conj_thm_2Ellist_2ELLIST__BISIMULATION0,lemma,( ! [A_27a:del]: ( ! [V0ll1:$i] : ((mem@V0ll1@(ty_2Ellist_2Ellist@A_27a)) => ( ! [V1ll2:$i] : ((mem@V1ll2@(ty_2Ellist_2Ellist@A_27a)) => ((V0ll1 = V1ll2) <=> (? [V2R:$i] : ((mem@V2R@(arr@(ty_2Ellist_2Ellist@A_27a)@(arr@(ty_2Ellist_2Ellist@A_27a)@bool))) & ((p@(ap@(ap@V2R@V0ll1)@V1ll2)) & ( ! [V3ll3:$i] : ((mem@V3ll3@(ty_2Ellist_2Ellist@A_27a)) => ( ! [V4ll4:$i] : ((mem@V4ll4@(ty_2Ellist_2Ellist@A_27a)) => ((p@(ap@(ap@V2R@V3ll3)@V4ll4)) => (((V3ll3 = (c_2Ellist_2ELNIL@A_27a)) & (V4ll4 = (c_2Ellist_2ELNIL@A_27a))) | (? [V5h:$i] : ((mem@V5h@A_27a) & (? [V6t1:$i] : ((mem@V6t1@(ty_2Ellist_2Ellist@A_27a)) & (? [V7t2:$i] : ((mem@V7t2@(ty_2Ellist_2Ellist@A_27a)) & ((V3ll3 = (ap@(ap@(c_2Ellist_2ELCONS@A_27a)@V5h)@V6t1)) & ((V4ll4 = (ap@(ap@(c_2Ellist_2ELCONS@A_27a)@V5h)@V7t2)) & (p@(ap@(ap@V2R@V6t1)@V7t2)))))))))))))))))))))))))).
thf(conj_thm_2Ellist_2ELLIST__BISIMULATION,lemma,( ! [A_27a:del]: ( ! [V0ll1:$i] : ((mem@V0ll1@(ty_2Ellist_2Ellist@A_27a)) => ( ! [V1ll2:$i] : ((mem@V1ll2@(ty_2Ellist_2Ellist@A_27a)) => ((V0ll1 = V1ll2) <=> (? [V2R:$i] : ((mem@V2R@(arr@(ty_2Ellist_2Ellist@A_27a)@(arr@(ty_2Ellist_2Ellist@A_27a)@bool))) & ((p@(ap@(ap@V2R@V0ll1)@V1ll2)) & ( ! [V3ll3:$i] : ((mem@V3ll3@(ty_2Ellist_2Ellist@A_27a)) => ( ! [V4ll4:$i] : ((mem@V4ll4@(ty_2Ellist_2Ellist@A_27a)) => ((p@(ap@(ap@V2R@V3ll3)@V4ll4)) => (((V3ll3 = (c_2Ellist_2ELNIL@A_27a)) & (V4ll4 = (c_2Ellist_2ELNIL@A_27a))) | (((ap@(c_2Ellist_2ELHD@A_27a)@V3ll3) = (ap@(c_2Ellist_2ELHD@A_27a)@V4ll4)) & (p@(ap@(ap@V2R@(ap@(c_2Eoption_2ETHE@(ty_2Ellist_2Ellist@A_27a))@(ap@(c_2Ellist_2ELTL@A_27a)@V3ll3)))@(ap@(c_2Eoption_2ETHE@(ty_2Ellist_2Ellist@A_27a))@(ap@(c_2Ellist_2ELTL@A_27a)@V4ll4))))))))))))))))))))).
thf(conj_thm_2Ellist_2ELLIST__STRONG__BISIMULATION,lemma,( ! [A_27a:del]: ( ! [V0ll1:$i] : ((mem@V0ll1@(ty_2Ellist_2Ellist@A_27a)) => ( ! [V1ll2:$i] : ((mem@V1ll2@(ty_2Ellist_2Ellist@A_27a)) => ((V0ll1 = V1ll2) <=> (? [V2R:$i] : ((mem@V2R@(arr@(ty_2Ellist_2Ellist@A_27a)@(arr@(ty_2Ellist_2Ellist@A_27a)@bool))) & ((p@(ap@(ap@V2R@V0ll1)@V1ll2)) & ( ! [V3ll3:$i] : ((mem@V3ll3@(ty_2Ellist_2Ellist@A_27a)) => ( ! [V4ll4:$i] : ((mem@V4ll4@(ty_2Ellist_2Ellist@A_27a)) => ((p@(ap@(ap@V2R@V3ll3)@V4ll4)) => ((V3ll3 = V4ll4) | (? [V5h:$i] : ((mem@V5h@A_27a) & (? [V6t1:$i] : ((mem@V6t1@(ty_2Ellist_2Ellist@A_27a)) & (? [V7t2:$i] : ((mem@V7t2@(ty_2Ellist_2Ellist@A_27a)) & ((V3ll3 = (ap@(ap@(c_2Ellist_2ELCONS@A_27a)@V5h)@V6t1)) & ((V4ll4 = (ap@(ap@(c_2Ellist_2ELCONS@A_27a)@V5h)@V7t2)) & (p@(ap@(ap@V2R@V6t1)@V7t2)))))))))))))))))))))))))).
thf(ax_thm_2Ellist_2ELTAKE,axiom,( ! [A_27a:del]: (( ! [V0ll:$i] : ((mem@V0ll@(ty_2Ellist_2Ellist@A_27a)) => ((ap@(ap@(c_2Ellist_2ELTAKE@A_27a)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@V0ll) = (ap@(c_2Eoption_2ESOME@(ty_2Elist_2Elist@A_27a))@(c_2Elist_2ENIL@A_27a))))) & ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2ll:$i] : ((mem@V2ll@(ty_2Ellist_2Ellist@A_27a)) => ((ap@(ap@(c_2Ellist_2ELTAKE@A_27a)@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n)))@V2ll) = (ap@(ap@(ap@(c_2Eoption_2Eoption__CASE@A_27a@(ty_2Eoption_2Eoption@(ty_2Elist_2Elist@A_27a)))@(ap@(c_2Ellist_2ELHD@A_27a)@V2ll))@(c_2Eoption_2ENONE@(ty_2Elist_2Elist@A_27a)))@(lam@A_27a@(^ [V3hd:$i] : (ap@(ap@(ap@(c_2Eoption_2Eoption__CASE@(ty_2Elist_2Elist@A_27a)@(ty_2Eoption_2Eoption@(ty_2Elist_2Elist@A_27a)))@(ap@(ap@(c_2Ellist_2ELTAKE@A_27a)@(inj__ty_2Enum_2Enum @ V1n))@(ap@(c_2Eoption_2ETHE@(ty_2Ellist_2Ellist@A_27a))@(ap@(c_2Ellist_2ELTL@A_27a)@V2ll))))@(c_2Eoption_2ENONE@(ty_2Elist_2Elist@A_27a)))@(lam@(ty_2Elist_2Elist@A_27a)@(^ [V4tl:$i] : (ap@(c_2Eoption_2ESOME@(ty_2Elist_2Elist@A_27a))@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V3hd)@V4tl))))))))))))))).
thf(conj_thm_2Ellist_2ELTAKE__LUNFOLD,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27b@(ty_2Eoption_2Eoption@(ty_2Epair_2Eprod@A_27b@A_27a)))) => ( ! [V1x:$i] : ((mem@V1x@A_27b) => ( ! [V2n:tp__ty_2Enum_2Enum] : (((ap@(ap@(c_2Ellist_2ELTAKE@A_27a)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(ap@(ap@(c_2Ellist_2ELUNFOLD@A_27a@A_27b)@V0f)@V1x)) = (ap@(c_2Eoption_2ESOME@(ty_2Elist_2Elist@A_27a))@(c_2Elist_2ENIL@A_27a))) & ((ap@(ap@(c_2Ellist_2ELTAKE@A_27a)@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V2n)))@(ap@(ap@(c_2Ellist_2ELUNFOLD@A_27a@A_27b)@V0f)@V1x)) = (ap@(ap@(ap@(c_2Eoption_2Eoption__CASE@(ty_2Epair_2Eprod@A_27b@A_27a)@(ty_2Eoption_2Eoption@(ty_2Elist_2Elist@A_27a)))@(ap@V0f@V1x))@(c_2Eoption_2ENONE@(ty_2Elist_2Elist@A_27a)))@(lam@(ty_2Epair_2Eprod@A_27b@A_27a)@(^ [V3v:$i] : (ap@(ap@(c_2Epair_2Epair__CASE@(ty_2Eoption_2Eoption@(ty_2Elist_2Elist@A_27a))@A_27b@A_27a)@V3v)@(lam@A_27b@(^ [V4tx:$i] : (lam@A_27a@(^ [V5hx:$i] : (ap@(ap@(c_2Eoption_2EOPTION__MAP@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))@(ap@(c_2Elist_2ECONS@A_27a)@V5hx))@(ap@(ap@(c_2Ellist_2ELTAKE@A_27a)@(inj__ty_2Enum_2Enum @ V2n))@(ap@(ap@(c_2Ellist_2ELUNFOLD@A_27a@A_27b)@V0f)@V4tx))))))))))))))))))))).
thf(conj_thm_2Ellist_2ELTAKE__THM,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: (( ! [V0l:$i] : ((mem@V0l@(ty_2Ellist_2Ellist@A_27a)) => ((ap@(ap@(c_2Ellist_2ELTAKE@A_27a)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@V0l) = (ap@(c_2Eoption_2ESOME@(ty_2Elist_2Elist@A_27a))@(c_2Elist_2ENIL@A_27a))))) & (( ! [V1n:tp__ty_2Enum_2Enum] : ((ap@(ap@(c_2Ellist_2ELTAKE@A_27b)@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n)))@(c_2Ellist_2ELNIL@A_27b)) = (c_2Eoption_2ENONE@(ty_2Elist_2Elist@A_27b)))) & ( ! [V2n:tp__ty_2Enum_2Enum] : ( ! [V3h:$i] : ((mem@V3h@A_27c) => ( ! [V4t:$i] : ((mem@V4t@(ty_2Ellist_2Ellist@A_27c)) => ((ap@(ap@(c_2Ellist_2ELTAKE@A_27c)@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V2n)))@(ap@(ap@(c_2Ellist_2ELCONS@A_27c)@V3h)@V4t)) = (ap@(ap@(c_2Eoption_2EOPTION__MAP@(ty_2Elist_2Elist@A_27c)@(ty_2Elist_2Elist@A_27c))@(ap@(c_2Elist_2ECONS@A_27c)@V3h))@(ap@(ap@(c_2Ellist_2ELTAKE@A_27c)@(inj__ty_2Enum_2Enum @ V2n))@V4t)))))))))))))).
thf(conj_thm_2Ellist_2ELTAKE__SNOC__LNTH,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1ll:$i] : ((mem@V1ll@(ty_2Ellist_2Ellist@A_27a)) => ((ap@(ap@(c_2Ellist_2ELTAKE@A_27a)@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V0n)))@V1ll) = (ap@(ap@(ap@(c_2Eoption_2Eoption__CASE@(ty_2Elist_2Elist@A_27a)@(ty_2Eoption_2Eoption@(ty_2Elist_2Elist@A_27a)))@(ap@(ap@(c_2Ellist_2ELTAKE@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1ll))@(c_2Eoption_2ENONE@(ty_2Elist_2Elist@A_27a)))@(lam@(ty_2Elist_2Elist@A_27a)@(^ [V2l:$i] : (ap@(ap@(ap@(c_2Eoption_2Eoption__CASE@A_27a@(ty_2Eoption_2Eoption@(ty_2Elist_2Elist@A_27a)))@(ap@(ap@(c_2Ellist_2ELNTH@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1ll))@(c_2Eoption_2ENONE@(ty_2Elist_2Elist@A_27a)))@(lam@A_27a@(^ [V3e:$i] : (ap@(c_2Eoption_2ESOME@(ty_2Elist_2Elist@A_27a))@(ap@(ap@(c_2Elist_2EAPPEND@A_27a)@V2l)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V3e)@(c_2Elist_2ENIL@A_27a)))))))))))))))).
thf(conj_thm_2Ellist_2ELTAKE__EQ__NONE__LNTH,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1ll:$i] : ((mem@V1ll@(ty_2Ellist_2Ellist@A_27a)) => (((ap@(ap@(c_2Ellist_2ELTAKE@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1ll) = (c_2Eoption_2ENONE@(ty_2Elist_2Elist@A_27a))) => ((ap@(ap@(c_2Ellist_2ELNTH@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1ll) = (c_2Eoption_2ENONE@A_27a)))))))).
thf(conj_thm_2Ellist_2ELTAKE__NIL__EQ__SOME,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ( ! [V1m:tp__ty_2Enum_2Enum] : (((ap@(ap@(c_2Ellist_2ELTAKE@A_27a)@(inj__ty_2Enum_2Enum @ V1m))@(c_2Ellist_2ELNIL@A_27a)) = (ap@(c_2Eoption_2ESOME@(ty_2Elist_2Elist@A_27a))@V0l)) <=> ((V1m = fo__c_2Enum_2E0) & (V0l = (c_2Elist_2ENIL@A_27a))))))))).
thf(conj_thm_2Ellist_2ELTAKE__NIL__EQ__NONE,lemma,( ! [A_27a:del]: ( ! [V0m:tp__ty_2Enum_2Enum] : (((ap@(ap@(c_2Ellist_2ELTAKE@A_27a)@(inj__ty_2Enum_2Enum @ V0m))@(c_2Ellist_2ELNIL@A_27a)) = (c_2Eoption_2ENONE@(ty_2Elist_2Elist@A_27a))) <=> (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V0m))))))).
thf(conj_thm_2Ellist_2ELTAKE__EQ,lemma,( ! [A_27a:del]: ( ! [V0ll1:$i] : ((mem@V0ll1@(ty_2Ellist_2Ellist@A_27a)) => ( ! [V1ll2:$i] : ((mem@V1ll2@(ty_2Ellist_2Ellist@A_27a)) => ((V0ll1 = V1ll2) <=> ( ! [V2n:tp__ty_2Enum_2Enum] : ((ap@(ap@(c_2Ellist_2ELTAKE@A_27a)@(inj__ty_2Enum_2Enum @ V2n))@V0ll1) = (ap@(ap@(c_2Ellist_2ELTAKE@A_27a)@(inj__ty_2Enum_2Enum @ V2n))@V1ll2)))))))))).
thf(conj_thm_2Ellist_2ELTAKE__CONS__EQ__NONE,lemma,( ! [A_27a:del]: ( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1h:$i] : ((mem@V1h@A_27a) => ( ! [V2t:$i] : ((mem@V2t@(ty_2Ellist_2Ellist@A_27a)) => (((ap@(ap@(c_2Ellist_2ELTAKE@A_27a)@(inj__ty_2Enum_2Enum @ V0m))@(ap@(ap@(c_2Ellist_2ELCONS@A_27a)@V1h)@V2t)) = (c_2Eoption_2ENONE@(ty_2Elist_2Elist@A_27a))) <=> (? [V3n:tp__ty_2Enum_2Enum] : ((V0m = (surj__ty_2Enum_2Enum @ (ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V3n)))) & ((ap@(ap@(c_2Ellist_2ELTAKE@A_27a)@(inj__ty_2Enum_2Enum @ V3n))@V2t) = (c_2Eoption_2ENONE@(ty_2Elist_2Elist@A_27a))))))))))))).
thf(conj_thm_2Ellist_2ELTAKE__CONS__EQ__SOME,lemma,( ! [A_27a:del]: ( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1h:$i] : ((mem@V1h@A_27a) => ( ! [V2t:$i] : ((mem@V2t@(ty_2Ellist_2Ellist@A_27a)) => ( ! [V3l:$i] : ((mem@V3l@(ty_2Elist_2Elist@A_27a)) => (((ap@(ap@(c_2Ellist_2ELTAKE@A_27a)@(inj__ty_2Enum_2Enum @ V0m))@(ap@(ap@(c_2Ellist_2ELCONS@A_27a)@V1h)@V2t)) = (ap@(c_2Eoption_2ESOME@(ty_2Elist_2Elist@A_27a))@V3l)) <=> (((V0m = fo__c_2Enum_2E0) & (V3l = (c_2Elist_2ENIL@A_27a))) | (? [V4n:tp__ty_2Enum_2Enum] : (? [V5l_27:$i] : ((mem@V5l_27@(ty_2Elist_2Elist@A_27a)) & ((V0m = (surj__ty_2Enum_2Enum @ (ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V4n)))) & (((ap@(ap@(c_2Ellist_2ELTAKE@A_27a)@(inj__ty_2Enum_2Enum @ V4n))@V2t) = (ap@(c_2Eoption_2ESOME@(ty_2Elist_2Elist@A_27a))@V5l_27)) & (V3l = (ap@(ap@(c_2Elist_2ECONS@A_27a)@V1h)@V5l_27)))))))))))))))))).
thf(conj_thm_2Ellist_2ELTAKE__EQ__SOME__CONS,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : ((mem@V1l@(ty_2Ellist_2Ellist@A_27a)) => ( ! [V2x:$i] : ((mem@V2x@(ty_2Elist_2Elist@A_27a)) => (((ap@(ap@(c_2Ellist_2ELTAKE@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1l) = (ap@(c_2Eoption_2ESOME@(ty_2Elist_2Elist@A_27a))@V2x)) => ( ! [V3h:$i] : ((mem@V3h@A_27a) => (? [V4y:$i] : ((mem@V4y@(ty_2Elist_2Elist@A_27a)) & ((ap@(ap@(c_2Ellist_2ELTAKE@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(ap@(c_2Ellist_2ELCONS@A_27a)@V3h)@V1l)) = (ap@(c_2Eoption_2ESOME@(ty_2Elist_2Elist@A_27a))@V4y)))))))))))))).
thf(ax_thm_2Ellist_2ELMAP,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: (( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ((ap@(ap@(c_2Ellist_2ELMAP@A_27a@A_27b)@V0f)@(c_2Ellist_2ELNIL@A_27a)) = (c_2Ellist_2ELNIL@A_27b)))) & ( ! [V1f:$i] : ((mem@V1f@(arr@A_27a@A_27b)) => ( ! [V2h:$i] : ((mem@V2h@A_27a) => ( ! [V3t:$i] : ((mem@V3t@(ty_2Ellist_2Ellist@A_27a)) => ((ap@(ap@(c_2Ellist_2ELMAP@A_27a@A_27b)@V1f)@(ap@(ap@(c_2Ellist_2ELCONS@A_27a)@V2h)@V3t)) = (ap@(ap@(c_2Ellist_2ELCONS@A_27b)@(ap@V1f@V2h))@(ap@(ap@(c_2Ellist_2ELMAP@A_27a@A_27b)@V1f)@V3t))))))))))))).
thf(ax_thm_2Ellist_2ELAPPEND,axiom,( ! [A_27a:del]: (( ! [V0x:$i] : ((mem@V0x@(ty_2Ellist_2Ellist@A_27a)) => ((ap@(ap@(c_2Ellist_2ELAPPEND@A_27a)@(c_2Ellist_2ELNIL@A_27a))@V0x) = V0x))) & ( ! [V1h:$i] : ((mem@V1h@A_27a) => ( ! [V2t:$i] : ((mem@V2t@(ty_2Ellist_2Ellist@A_27a)) => ( ! [V3x:$i] : ((mem@V3x@(ty_2Ellist_2Ellist@A_27a)) => ((ap@(ap@(c_2Ellist_2ELAPPEND@A_27a)@(ap@(ap@(c_2Ellist_2ELCONS@A_27a)@V1h)@V2t))@V3x) = (ap@(ap@(c_2Ellist_2ELCONS@A_27a)@V1h)@(ap@(ap@(c_2Ellist_2ELAPPEND@A_27a)@V2t)@V3x)))))))))))).
thf(conj_thm_2Ellist_2ELMAP__APPEND,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1ll1:$i] : ((mem@V1ll1@(ty_2Ellist_2Ellist@A_27a)) => ( ! [V2ll2:$i] : ((mem@V2ll2@(ty_2Ellist_2Ellist@A_27a)) => ((ap@(ap@(c_2Ellist_2ELMAP@A_27a@A_27b)@V0f)@(ap@(ap@(c_2Ellist_2ELAPPEND@A_27a)@V1ll1)@V2ll2)) = (ap@(ap@(c_2Ellist_2ELAPPEND@A_27b)@(ap@(ap@(c_2Ellist_2ELMAP@A_27a@A_27b)@V0f)@V1ll1))@(ap@(ap@(c_2Ellist_2ELMAP@A_27a@A_27b)@V0f)@V2ll2)))))))))))).
thf(conj_thm_2Ellist_2ELAPPEND__EQ__LNIL,lemma,( ! [A_27a:del]: ( ! [V0l1:$i] : ((mem@V0l1@(ty_2Ellist_2Ellist@A_27a)) => ( ! [V1l2:$i] : ((mem@V1l2@(ty_2Ellist_2Ellist@A_27a)) => (((ap@(ap@(c_2Ellist_2ELAPPEND@A_27a)@V0l1)@V1l2) = (c_2Ellist_2ELNIL@A_27a)) <=> ((V0l1 = (c_2Ellist_2ELNIL@A_27a)) & (V1l2 = (c_2Ellist_2ELNIL@A_27a)))))))))).
thf(conj_thm_2Ellist_2ELAPPEND__ASSOC,lemma,( ! [A_27a:del]: ( ! [V0ll1:$i] : ((mem@V0ll1@(ty_2Ellist_2Ellist@A_27a)) => ( ! [V1ll2:$i] : ((mem@V1ll2@(ty_2Ellist_2Ellist@A_27a)) => ( ! [V2ll3:$i] : ((mem@V2ll3@(ty_2Ellist_2Ellist@A_27a)) => ((ap@(ap@(c_2Ellist_2ELAPPEND@A_27a)@(ap@(ap@(c_2Ellist_2ELAPPEND@A_27a)@V0ll1)@V1ll2))@V2ll3) = (ap@(ap@(c_2Ellist_2ELAPPEND@A_27a)@V0ll1)@(ap@(ap@(c_2Ellist_2ELAPPEND@A_27a)@V1ll2)@V2ll3))))))))))).
thf(conj_thm_2Ellist_2ELMAP__MAP,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1g:$i] : ((mem@V1g@(arr@A_27c@A_27a)) => ( ! [V2ll:$i] : ((mem@V2ll@(ty_2Ellist_2Ellist@A_27c)) => ((ap@(ap@(c_2Ellist_2ELMAP@A_27a@A_27b)@V0f)@(ap@(ap@(c_2Ellist_2ELMAP@A_27c@A_27a)@V1g)@V2ll)) = (ap@(ap@(c_2Ellist_2ELMAP@A_27c@A_27b)@(ap@(ap@(c_2Ecombin_2Eo@A_27c@A_27b@A_27a)@V0f)@V1g))@V2ll)))))))))))).
thf(conj_thm_2Ellist_2ELAPPEND__NIL__2ND,lemma,( ! [A_27a:del]: ( ! [V0ll:$i] : ((mem@V0ll@(ty_2Ellist_2Ellist@A_27a)) => ((ap@(ap@(c_2Ellist_2ELAPPEND@A_27a)@V0ll)@(c_2Ellist_2ELNIL@A_27a)) = V0ll))))).
thf(conj_thm_2Ellist_2ELHD__LAPPEND,lemma,( ! [A_27a:del]: ( ! [V0l1:$i] : ((mem@V0l1@(ty_2Ellist_2Ellist@A_27a)) => ( ! [V1l2:$i] : ((mem@V1l2@(ty_2Ellist_2Ellist@A_27a)) => ((ap@(c_2Ellist_2ELHD@A_27a)@(ap@(ap@(c_2Ellist_2ELAPPEND@A_27a)@V0l1)@V1l2)) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@A_27a))@(ap@(ap@(c_2Emin_2E_3D@(ty_2Ellist_2Ellist@A_27a))@V0l1)@(c_2Ellist_2ELNIL@A_27a)))@(ap@(c_2Ellist_2ELHD@A_27a)@V1l2))@(ap@(c_2Ellist_2ELHD@A_27a)@V0l1))))))))).
thf(conj_thm_2Ellist_2ELTL__LAPPEND,lemma,( ! [A_27a:del]: ( ! [V0l1:$i] : ((mem@V0l1@(ty_2Ellist_2Ellist@A_27a)) => ( ! [V1l2:$i] : ((mem@V1l2@(ty_2Ellist_2Ellist@A_27a)) => ((ap@(c_2Ellist_2ELTL@A_27a)@(ap@(ap@(c_2Ellist_2ELAPPEND@A_27a)@V0l1)@V1l2)) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@(ty_2Ellist_2Ellist@A_27a)))@(ap@(ap@(c_2Emin_2E_3D@(ty_2Ellist_2Ellist@A_27a))@V0l1)@(c_2Ellist_2ELNIL@A_27a)))@(ap@(c_2Ellist_2ELTL@A_27a)@V1l2))@(ap@(c_2Eoption_2ESOME@(ty_2Ellist_2Ellist@A_27a))@(ap@(ap@(c_2Ellist_2ELAPPEND@A_27a)@(ap@(c_2Eoption_2ETHE@(ty_2Ellist_2Ellist@A_27a))@(ap@(c_2Ellist_2ELTL@A_27a)@V0l1)))@V1l2)))))))))).
thf(conj_thm_2Ellist_2ELTAKE__LAPPEND1,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l1:$i] : ((mem@V1l1@(ty_2Ellist_2Ellist@A_27a)) => ( ! [V2l2:$i] : ((mem@V2l2@(ty_2Ellist_2Ellist@A_27a)) => ((p@(ap@(c_2Eoption_2EIS__SOME@(ty_2Elist_2Elist@A_27a))@(ap@(ap@(c_2Ellist_2ELTAKE@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1l1))) => ((ap@(ap@(c_2Ellist_2ELTAKE@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(ap@(c_2Ellist_2ELAPPEND@A_27a)@V1l1)@V2l2)) = (ap@(ap@(c_2Ellist_2ELTAKE@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1l1)))))))))).
thf(ax_thm_2Ellist_2ELFINITE__def,axiom,( ! [A_27a:del]: ((c_2Ellist_2ELFINITE@A_27a) = (lam@(ty_2Ellist_2Ellist@A_27a)@(^ [V0a0:$i] : (ap@(c_2Ebool_2E_21@(arr@(ty_2Ellist_2Ellist@A_27a)@bool))@(lam@(arr@(ty_2Ellist_2Ellist@A_27a)@bool)@(^ [V1LFINITE_27:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@(c_2Ebool_2E_21@(ty_2Ellist_2Ellist@A_27a))@(lam@(ty_2Ellist_2Ellist@A_27a)@(^ [V2a0:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@(c_2Emin_2E_3D@(ty_2Ellist_2Ellist@A_27a))@V2a0)@(c_2Ellist_2ELNIL@A_27a)))@(ap@(c_2Ebool_2E_3F@A_27a)@(lam@A_27a@(^ [V3h:$i] : (ap@(c_2Ebool_2E_3F@(ty_2Ellist_2Ellist@A_27a))@(lam@(ty_2Ellist_2Ellist@A_27a)@(^ [V4t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Emin_2E_3D@(ty_2Ellist_2Ellist@A_27a))@V2a0)@(ap@(ap@(c_2Ellist_2ELCONS@A_27a)@V3h)@V4t)))@(ap@V1LFINITE_27@V4t))))))))))@(ap@V1LFINITE_27@V2a0))))))@(ap@V1LFINITE_27@V0a0)))))))))).
thf(conj_thm_2Ellist_2ELFINITE__rules,lemma,( ! [A_27a:del]: ((p@(ap@(c_2Ellist_2ELFINITE@A_27a)@(c_2Ellist_2ELNIL@A_27a))) & ( ! [V0h:$i] : ((mem@V0h@A_27a) => ( ! [V1t:$i] : ((mem@V1t@(ty_2Ellist_2Ellist@A_27a)) => ((p@(ap@(c_2Ellist_2ELFINITE@A_27a)@V1t)) => (p@(ap@(c_2Ellist_2ELFINITE@A_27a)@(ap@(ap@(c_2Ellist_2ELCONS@A_27a)@V0h)@V1t))))))))))).
thf(conj_thm_2Ellist_2ELFINITE__ind,lemma,( ! [A_27a:del]: ( ! [V0LFINITE_27:$i] : ((mem@V0LFINITE_27@(arr@(ty_2Ellist_2Ellist@A_27a)@bool)) => (((p@(ap@V0LFINITE_27@(c_2Ellist_2ELNIL@A_27a))) & ( ! [V1h:$i] : ((mem@V1h@A_27a) => ( ! [V2t:$i] : ((mem@V2t@(ty_2Ellist_2Ellist@A_27a)) => ((p@(ap@V0LFINITE_27@V2t)) => (p@(ap@V0LFINITE_27@(ap@(ap@(c_2Ellist_2ELCONS@A_27a)@V1h)@V2t))))))))) => ( ! [V3a0:$i] : ((mem@V3a0@(ty_2Ellist_2Ellist@A_27a)) => ((p@(ap@(c_2Ellist_2ELFINITE@A_27a)@V3a0)) => (p@(ap@V0LFINITE_27@V3a0)))))))))).
thf(conj_thm_2Ellist_2ELFINITE__strongind,lemma,( ! [A_27a:del]: ( ! [V0LFINITE_27:$i] : ((mem@V0LFINITE_27@(arr@(ty_2Ellist_2Ellist@A_27a)@bool)) => (((p@(ap@V0LFINITE_27@(c_2Ellist_2ELNIL@A_27a))) & ( ! [V1h:$i] : ((mem@V1h@A_27a) => ( ! [V2t:$i] : ((mem@V2t@(ty_2Ellist_2Ellist@A_27a)) => (((p@(ap@(c_2Ellist_2ELFINITE@A_27a)@V2t)) & (p@(ap@V0LFINITE_27@V2t))) => (p@(ap@V0LFINITE_27@(ap@(ap@(c_2Ellist_2ELCONS@A_27a)@V1h)@V2t))))))))) => ( ! [V3a0:$i] : ((mem@V3a0@(ty_2Ellist_2Ellist@A_27a)) => ((p@(ap@(c_2Ellist_2ELFINITE@A_27a)@V3a0)) => (p@(ap@V0LFINITE_27@V3a0)))))))))).
thf(conj_thm_2Ellist_2ELFINITE__cases,lemma,( ! [A_27a:del]: ( ! [V0a0:$i] : ((mem@V0a0@(ty_2Ellist_2Ellist@A_27a)) => ((p@(ap@(c_2Ellist_2ELFINITE@A_27a)@V0a0)) <=> ((V0a0 = (c_2Ellist_2ELNIL@A_27a)) | (? [V1h:$i] : ((mem@V1h@A_27a) & (? [V2t:$i] : ((mem@V2t@(ty_2Ellist_2Ellist@A_27a)) & ((V0a0 = (ap@(ap@(c_2Ellist_2ELCONS@A_27a)@V1h)@V2t)) & (p@(ap@(c_2Ellist_2ELFINITE@A_27a)@V2t))))))))))))).
thf(conj_thm_2Ellist_2ELFINITE__THM,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: (((p@(ap@(c_2Ellist_2ELFINITE@A_27a)@(c_2Ellist_2ELNIL@A_27a))) <=> $true) & ( ! [V0h:$i] : ((mem@V0h@A_27b) => ( ! [V1t:$i] : ((mem@V1t@(ty_2Ellist_2Ellist@A_27b)) => ((p@(ap@(c_2Ellist_2ELFINITE@A_27b)@(ap@(ap@(c_2Ellist_2ELCONS@A_27b)@V0h)@V1t))) <=> (p@(ap@(c_2Ellist_2ELFINITE@A_27b)@V1t))))))))))).
thf(conj_thm_2Ellist_2ELFINITE,lemma,( ! [A_27a:del]: ( ! [V0ll:$i] : ((mem@V0ll@(ty_2Ellist_2Ellist@A_27a)) => ((p@(ap@(c_2Ellist_2ELFINITE@A_27a)@V0ll)) <=> (? [V1n:tp__ty_2Enum_2Enum] : ((ap@(ap@(c_2Ellist_2ELTAKE@A_27a)@(inj__ty_2Enum_2Enum @ V1n))@V0ll) = (c_2Eoption_2ENONE@(ty_2Elist_2Elist@A_27a))))))))).
thf(ax_thm_2Ellist_2Ellength__rel__def,axiom,( ! [A_27a:del]: ((c_2Ellist_2Ellength__rel@A_27a) = (lam@(ty_2Ellist_2Ellist@A_27a)@(^ [V0a0:$i] : (lam@ty_2Enum_2Enum@(^ [V1a1:$i] : (ap@(c_2Ebool_2E_21@(arr@(ty_2Ellist_2Ellist@A_27a)@(arr@ty_2Enum_2Enum@bool)))@(lam@(arr@(ty_2Ellist_2Ellist@A_27a)@(arr@ty_2Enum_2Enum@bool))@(^ [V2llength__rel_27:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@(c_2Ebool_2E_21@(ty_2Ellist_2Ellist@A_27a))@(lam@(ty_2Ellist_2Ellist@A_27a)@(^ [V3a0:$i] : (ap@(c_2Ebool_2E_21@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V4a1:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@(ap@c_2Ebool_2E_5C_2F@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Emin_2E_3D@(ty_2Ellist_2Ellist@A_27a))@V3a0)@(c_2Ellist_2ELNIL@A_27a)))@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@V4a1)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))))@(ap@(c_2Ebool_2E_3F@A_27a)@(lam@A_27a@(^ [V5h:$i] : (ap@(c_2Ebool_2E_3F@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V6n:$i] : (ap@(c_2Ebool_2E_3F@(ty_2Ellist_2Ellist@A_27a))@(lam@(ty_2Ellist_2Ellist@A_27a)@(^ [V7t:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Emin_2E_3D@(ty_2Ellist_2Ellist@A_27a))@V3a0)@(ap@(ap@(c_2Ellist_2ELCONS@A_27a)@V5h)@V7t)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@V4a1)@(ap@c_2Enum_2ESUC@V6n)))@(ap@(ap@V2llength__rel_27@V7t)@V6n))))))))))))))@(ap@(ap@V2llength__rel_27@V3a0)@V4a1)))))))))@(ap@(ap@V2llength__rel_27@V0a0)@V1a1)))))))))))).
thf(conj_thm_2Ellist_2Ellength__rel__rules,lemma,( ! [A_27a:del]: ((p@(ap@(ap@(c_2Ellist_2Ellength__rel@A_27a)@(c_2Ellist_2ELNIL@A_27a))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) & ( ! [V0h:$i] : ((mem@V0h@A_27a) => ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2t:$i] : ((mem@V2t@(ty_2Ellist_2Ellist@A_27a)) => ((p@(ap@(ap@(c_2Ellist_2Ellength__rel@A_27a)@V2t)@(inj__ty_2Enum_2Enum @ V1n))) => (p@(ap@(ap@(c_2Ellist_2Ellength__rel@A_27a)@(ap@(ap@(c_2Ellist_2ELCONS@A_27a)@V0h)@V2t))@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n))))))))))))).
thf(conj_thm_2Ellist_2Ellength__rel__ind,lemma,( ! [A_27a:del]: ( ! [V0llength__rel_27:$i] : ((mem@V0llength__rel_27@(arr@(ty_2Ellist_2Ellist@A_27a)@(arr@ty_2Enum_2Enum@bool))) => (((p@(ap@(ap@V0llength__rel_27@(c_2Ellist_2ELNIL@A_27a))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) & ( ! [V1h:$i] : ((mem@V1h@A_27a) => ( ! [V2n:tp__ty_2Enum_2Enum] : ( ! [V3t:$i] : ((mem@V3t@(ty_2Ellist_2Ellist@A_27a)) => ((p@(ap@(ap@V0llength__rel_27@V3t)@(inj__ty_2Enum_2Enum @ V2n))) => (p@(ap@(ap@V0llength__rel_27@(ap@(ap@(c_2Ellist_2ELCONS@A_27a)@V1h)@V3t))@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V2n))))))))))) => ( ! [V4a0:$i] : ((mem@V4a0@(ty_2Ellist_2Ellist@A_27a)) => ( ! [V5a1:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@(c_2Ellist_2Ellength__rel@A_27a)@V4a0)@(inj__ty_2Enum_2Enum @ V5a1))) => (p@(ap@(ap@V0llength__rel_27@V4a0)@(inj__ty_2Enum_2Enum @ V5a1)))))))))))).
thf(conj_thm_2Ellist_2Ellength__rel__strongind,lemma,( ! [A_27a:del]: ( ! [V0llength__rel_27:$i] : ((mem@V0llength__rel_27@(arr@(ty_2Ellist_2Ellist@A_27a)@(arr@ty_2Enum_2Enum@bool))) => (((p@(ap@(ap@V0llength__rel_27@(c_2Ellist_2ELNIL@A_27a))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) & ( ! [V1h:$i] : ((mem@V1h@A_27a) => ( ! [V2n:tp__ty_2Enum_2Enum] : ( ! [V3t:$i] : ((mem@V3t@(ty_2Ellist_2Ellist@A_27a)) => (((p@(ap@(ap@(c_2Ellist_2Ellength__rel@A_27a)@V3t)@(inj__ty_2Enum_2Enum @ V2n))) & (p@(ap@(ap@V0llength__rel_27@V3t)@(inj__ty_2Enum_2Enum @ V2n)))) => (p@(ap@(ap@V0llength__rel_27@(ap@(ap@(c_2Ellist_2ELCONS@A_27a)@V1h)@V3t))@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V2n))))))))))) => ( ! [V4a0:$i] : ((mem@V4a0@(ty_2Ellist_2Ellist@A_27a)) => ( ! [V5a1:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@(c_2Ellist_2Ellength__rel@A_27a)@V4a0)@(inj__ty_2Enum_2Enum @ V5a1))) => (p@(ap@(ap@V0llength__rel_27@V4a0)@(inj__ty_2Enum_2Enum @ V5a1)))))))))))).
thf(conj_thm_2Ellist_2Ellength__rel__cases,lemma,( ! [A_27a:del]: ( ! [V0a0:$i] : ((mem@V0a0@(ty_2Ellist_2Ellist@A_27a)) => ( ! [V1a1:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@(c_2Ellist_2Ellength__rel@A_27a)@V0a0)@(inj__ty_2Enum_2Enum @ V1a1))) <=> (((V0a0 = (c_2Ellist_2ELNIL@A_27a)) & (V1a1 = fo__c_2Enum_2E0)) | (? [V2h:$i] : ((mem@V2h@A_27a) & (? [V3n:tp__ty_2Enum_2Enum] : (? [V4t:$i] : ((mem@V4t@(ty_2Ellist_2Ellist@A_27a)) & ((V0a0 = (ap@(ap@(c_2Ellist_2ELCONS@A_27a)@V2h)@V4t)) & ((V1a1 = (surj__ty_2Enum_2Enum @ (ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V3n)))) & (p@(ap@(ap@(c_2Ellist_2Ellength__rel@A_27a)@V4t)@(inj__ty_2Enum_2Enum @ V3n))))))))))))))))).
thf(ax_thm_2Ellist_2ELLENGTH,axiom,( ! [A_27a:del]: ( ! [V0ll:$i] : ((mem@V0ll@(ty_2Ellist_2Ellist@A_27a)) => ((surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum @ (ap@(c_2Ellist_2ELLENGTH@A_27a)@V0ll)) = (surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@ty_2Enum_2Enum))@(ap@(c_2Ellist_2ELFINITE@A_27a)@V0ll))@(ap@(c_2Eoption_2ESOME@ty_2Enum_2Enum)@(ap@(c_2Emin_2E_40@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V1n:$i] : (ap@(ap@(c_2Ellist_2Ellength__rel@A_27a)@V0ll)@V1n))))))@(c_2Eoption_2ENONE@ty_2Enum_2Enum)))))))).
thf(conj_thm_2Ellist_2ELLENGTH__THM,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: (((surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum @ (ap@(c_2Ellist_2ELLENGTH@A_27a)@(c_2Ellist_2ELNIL@A_27a))) = (surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum @ (ap@(c_2Eoption_2ESOME@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) & ( ! [V0h:$i] : ((mem@V0h@A_27b) => ( ! [V1t:$i] : ((mem@V1t@(ty_2Ellist_2Ellist@A_27b)) => ((surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum @ (ap@(c_2Ellist_2ELLENGTH@A_27b)@(ap@(ap@(c_2Ellist_2ELCONS@A_27b)@V0h)@V1t))) = (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_2Ellist_2ELLENGTH@A_27b)@V1t)))))))))))).
thf(conj_thm_2Ellist_2ELLENGTH__0,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@(ty_2Ellist_2Ellist@A_27a)) => (((surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum @ (ap@(c_2Ellist_2ELLENGTH@A_27a)@V0x)) = (surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum @ (ap@(c_2Eoption_2ESOME@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0)))) <=> (V0x = (c_2Ellist_2ELNIL@A_27a))))))).
thf(conj_thm_2Ellist_2ELFINITE__HAS__LENGTH,lemma,( ! [A_27a:del]: ( ! [V0ll:$i] : ((mem@V0ll@(ty_2Ellist_2Ellist@A_27a)) => ((p@(ap@(c_2Ellist_2ELFINITE@A_27a)@V0ll)) => (? [V1n:tp__ty_2Enum_2Enum] : ((surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum @ (ap@(c_2Ellist_2ELLENGTH@A_27a)@V0ll)) = (surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum @ (ap@(c_2Eoption_2ESOME@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V1n)))))))))).
thf(conj_thm_2Ellist_2ENOT__LFINITE__NO__LENGTH,lemma,( ! [A_27a:del]: ( ! [V0ll:$i] : ((mem@V0ll@(ty_2Ellist_2Ellist@A_27a)) => ((~~ (p@(ap@(c_2Ellist_2ELFINITE@A_27a)@V0ll))) => ((surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum @ (ap@(c_2Ellist_2ELLENGTH@A_27a)@V0ll)) = (surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum @ (c_2Eoption_2ENONE@ty_2Enum_2Enum)))))))).
thf(conj_thm_2Ellist_2ELFINITE__LLENGTH,lemma,( ! [A_27a:del]: ( ! [V0ll:$i] : ((mem@V0ll@(ty_2Ellist_2Ellist@A_27a)) => ((p@(ap@(c_2Ellist_2ELFINITE@A_27a)@V0ll)) <=> (? [V1n:tp__ty_2Enum_2Enum] : ((surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum @ (ap@(c_2Ellist_2ELLENGTH@A_27a)@V0ll)) = (surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum @ (ap@(c_2Eoption_2ESOME@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V1n)))))))))).
thf(conj_thm_2Ellist_2ELFINITE__INDUCTION,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@(ty_2Ellist_2Ellist@A_27a)@bool)) => (((p@(ap@V0P@(c_2Ellist_2ELNIL@A_27a))) & ( ! [V1h:$i] : ((mem@V1h@A_27a) => ( ! [V2t:$i] : ((mem@V2t@(ty_2Ellist_2Ellist@A_27a)) => ((p@(ap@V0P@V2t)) => (p@(ap@V0P@(ap@(ap@(c_2Ellist_2ELCONS@A_27a)@V1h)@V2t))))))))) => ( ! [V3a0:$i] : ((mem@V3a0@(ty_2Ellist_2Ellist@A_27a)) => ((p@(ap@(c_2Ellist_2ELFINITE@A_27a)@V3a0)) => (p@(ap@V0P@V3a0)))))))))).
thf(conj_thm_2Ellist_2ELFINITE__STRONG__INDUCTION,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@(ty_2Ellist_2Ellist@A_27a)@bool)) => (((p@(ap@V0P@(c_2Ellist_2ELNIL@A_27a))) & ( ! [V1h:$i] : ((mem@V1h@A_27a) => ( ! [V2t:$i] : ((mem@V2t@(ty_2Ellist_2Ellist@A_27a)) => (((p@(ap@(c_2Ellist_2ELFINITE@A_27a)@V2t)) & (p@(ap@V0P@V2t))) => (p@(ap@V0P@(ap@(ap@(c_2Ellist_2ELCONS@A_27a)@V1h)@V2t))))))))) => ( ! [V3a0:$i] : ((mem@V3a0@(ty_2Ellist_2Ellist@A_27a)) => ((p@(ap@(c_2Ellist_2ELFINITE@A_27a)@V3a0)) => (p@(ap@V0P@V3a0)))))))))).
thf(conj_thm_2Ellist_2ELFINITE__MAP,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1ll:$i] : ((mem@V1ll@(ty_2Ellist_2Ellist@A_27a)) => ((p@(ap@(c_2Ellist_2ELFINITE@A_27b)@(ap@(ap@(c_2Ellist_2ELMAP@A_27a@A_27b)@V0f)@V1ll))) <=> (p@(ap@(c_2Ellist_2ELFINITE@A_27a)@V1ll)))))))))).
thf(conj_thm_2Ellist_2ELFINITE__APPEND,lemma,( ! [A_27a:del]: ( ! [V0ll1:$i] : ((mem@V0ll1@(ty_2Ellist_2Ellist@A_27a)) => ( ! [V1ll2:$i] : ((mem@V1ll2@(ty_2Ellist_2Ellist@A_27a)) => ((p@(ap@(c_2Ellist_2ELFINITE@A_27a)@(ap@(ap@(c_2Ellist_2ELAPPEND@A_27a)@V0ll1)@V1ll2))) <=> ((p@(ap@(c_2Ellist_2ELFINITE@A_27a)@V0ll1)) & (p@(ap@(c_2Ellist_2ELFINITE@A_27a)@V1ll2)))))))))).
thf(conj_thm_2Ellist_2ELTAKE__LNTH__EL,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1ll:$i] : ((mem@V1ll@(ty_2Ellist_2Ellist@A_27a)) => ( ! [V2m:tp__ty_2Enum_2Enum] : ( ! [V3l:$i] : ((mem@V3l@(ty_2Elist_2Elist@A_27a)) => ((((ap@(ap@(c_2Ellist_2ELTAKE@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1ll) = (ap@(c_2Eoption_2ESOME@(ty_2Elist_2Elist@A_27a))@V3l)) & (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V2m))@(inj__ty_2Enum_2Enum @ V0n)))) => ((ap@(ap@(c_2Ellist_2ELNTH@A_27a)@(inj__ty_2Enum_2Enum @ V2m))@V1ll) = (ap@(c_2Eoption_2ESOME@A_27a)@(ap@(ap@(c_2Elist_2EEL@A_27a)@(inj__ty_2Enum_2Enum @ V2m))@V3l)))))))))))).
thf(conj_thm_2Ellist_2ENOT__LFINITE__APPEND,lemma,( ! [A_27a:del]: ( ! [V0ll1:$i] : ((mem@V0ll1@(ty_2Ellist_2Ellist@A_27a)) => ( ! [V1ll2:$i] : ((mem@V1ll2@(ty_2Ellist_2Ellist@A_27a)) => ((~~ (p@(ap@(c_2Ellist_2ELFINITE@A_27a)@V0ll1))) => ((ap@(ap@(c_2Ellist_2ELAPPEND@A_27a)@V0ll1)@V1ll2) = V0ll1)))))))).
thf(conj_thm_2Ellist_2ELFINITE__LAPPEND__IMP__NIL,lemma,( ! [A_27a:del]: ( ! [V0ll:$i] : ((mem@V0ll@(ty_2Ellist_2Ellist@A_27a)) => ((p@(ap@(c_2Ellist_2ELFINITE@A_27a)@V0ll)) => ( ! [V1l2:$i] : ((mem@V1l2@(ty_2Ellist_2Ellist@A_27a)) => (((ap@(ap@(c_2Ellist_2ELAPPEND@A_27a)@V0ll)@V1l2) = V0ll) => (V1l2 = (c_2Ellist_2ELNIL@A_27a)))))))))).
thf(conj_thm_2Ellist_2ELLENGTH__MAP,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0ll:$i] : ((mem@V0ll@(ty_2Ellist_2Ellist@A_27a)) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27a@A_27b)) => ((surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum @ (ap@(c_2Ellist_2ELLENGTH@A_27b)@(ap@(ap@(c_2Ellist_2ELMAP@A_27a@A_27b)@V1f)@V0ll))) = (surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum @ (ap@(c_2Ellist_2ELLENGTH@A_27a)@V0ll)))))))))).
thf(conj_thm_2Ellist_2ELLENGTH__APPEND,lemma,( ! [A_27a:del]: ( ! [V0ll1:$i] : ((mem@V0ll1@(ty_2Ellist_2Ellist@A_27a)) => ( ! [V1ll2:$i] : ((mem@V1ll2@(ty_2Ellist_2Ellist@A_27a)) => ((surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum @ (ap@(c_2Ellist_2ELLENGTH@A_27a)@(ap@(ap@(c_2Ellist_2ELAPPEND@A_27a)@V0ll1)@V1ll2))) = (surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum @ (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@ty_2Enum_2Enum))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(c_2Ellist_2ELFINITE@A_27a)@V0ll1))@(ap@(c_2Ellist_2ELFINITE@A_27a)@V1ll2)))@(ap@(c_2Eoption_2ESOME@ty_2Enum_2Enum)@(ap@(ap@c_2Earithmetic_2E_2B@(ap@(c_2Eoption_2ETHE@ty_2Enum_2Enum)@(ap@(c_2Ellist_2ELLENGTH@A_27a)@V0ll1)))@(ap@(c_2Eoption_2ETHE@ty_2Enum_2Enum)@(ap@(c_2Ellist_2ELLENGTH@A_27a)@V1ll2)))))@(c_2Eoption_2ENONE@ty_2Enum_2Enum)))))))))).
thf(ax_thm_2Ellist_2EtoList,axiom,( ! [A_27a:del]: ( ! [V0ll:$i] : ((mem@V0ll@(ty_2Ellist_2Ellist@A_27a)) => ((ap@(c_2Ellist_2EtoList@A_27a)@V0ll) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@(ty_2Elist_2Elist@A_27a)))@(ap@(c_2Ellist_2ELFINITE@A_27a)@V0ll))@(ap@(ap@(c_2Ellist_2ELTAKE@A_27a)@(ap@(c_2Eoption_2ETHE@ty_2Enum_2Enum)@(ap@(c_2Ellist_2ELLENGTH@A_27a)@V0ll)))@V0ll))@(c_2Eoption_2ENONE@(ty_2Elist_2Elist@A_27a)))))))).
thf(conj_thm_2Ellist_2EtoList__THM,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: (((ap@(c_2Ellist_2EtoList@A_27a)@(c_2Ellist_2ELNIL@A_27a)) = (ap@(c_2Eoption_2ESOME@(ty_2Elist_2Elist@A_27a))@(c_2Elist_2ENIL@A_27a))) & ( ! [V0h:$i] : ((mem@V0h@A_27b) => ( ! [V1t:$i] : ((mem@V1t@(ty_2Ellist_2Ellist@A_27b)) => ((ap@(c_2Ellist_2EtoList@A_27b)@(ap@(ap@(c_2Ellist_2ELCONS@A_27b)@V0h)@V1t)) = (ap@(ap@(c_2Eoption_2EOPTION__MAP@(ty_2Elist_2Elist@A_27b)@(ty_2Elist_2Elist@A_27b))@(ap@(c_2Elist_2ECONS@A_27b)@V0h))@(ap@(c_2Ellist_2EtoList@A_27b)@V1t))))))))))).
thf(ax_thm_2Ellist_2EfromList__def,axiom,( ! [A_27a:del]: (((ap@(c_2Ellist_2EfromList@A_27a)@(c_2Elist_2ENIL@A_27a)) = (c_2Ellist_2ELNIL@A_27a)) & ( ! [V0h:$i] : ((mem@V0h@A_27a) => ( ! [V1t:$i] : ((mem@V1t@(ty_2Elist_2Elist@A_27a)) => ((ap@(c_2Ellist_2EfromList@A_27a)@(ap@(ap@(c_2Elist_2ECONS@A_27a)@V0h)@V1t)) = (ap@(ap@(c_2Ellist_2ELCONS@A_27a)@V0h)@(ap@(c_2Ellist_2EfromList@A_27a)@V1t)))))))))).
thf(conj_thm_2Ellist_2EfromList__EQ__LNIL,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => (((ap@(c_2Ellist_2EfromList@A_27a)@V0l) = (c_2Ellist_2ELNIL@A_27a)) <=> (V0l = (c_2Elist_2ENIL@A_27a))))))).
thf(conj_thm_2Ellist_2ELHD__fromList,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ((ap@(c_2Ellist_2ELHD@A_27a)@(ap@(c_2Ellist_2EfromList@A_27a)@V0l)) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@A_27a))@(ap@(c_2Elist_2ENULL@A_27a)@V0l))@(c_2Eoption_2ENONE@A_27a))@(ap@(c_2Eoption_2ESOME@A_27a)@(ap@(c_2Elist_2EHD@A_27a)@V0l)))))))).
thf(conj_thm_2Ellist_2ELTL__fromList,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ((ap@(c_2Ellist_2ELTL@A_27a)@(ap@(c_2Ellist_2EfromList@A_27a)@V0l)) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@(ty_2Ellist_2Ellist@A_27a)))@(ap@(c_2Elist_2ENULL@A_27a)@V0l))@(c_2Eoption_2ENONE@(ty_2Ellist_2Ellist@A_27a)))@(ap@(c_2Eoption_2ESOME@(ty_2Ellist_2Ellist@A_27a))@(ap@(c_2Ellist_2EfromList@A_27a)@(ap@(c_2Elist_2ETL@A_27a)@V0l))))))))).
thf(conj_thm_2Ellist_2ELFINITE__fromList,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => (p@(ap@(c_2Ellist_2ELFINITE@A_27a)@(ap@(c_2Ellist_2EfromList@A_27a)@V0l))))))).
thf(conj_thm_2Ellist_2ELLENGTH__fromList,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ((surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum @ (ap@(c_2Ellist_2ELLENGTH@A_27a)@(ap@(c_2Ellist_2EfromList@A_27a)@V0l))) = (surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum @ (ap@(c_2Eoption_2ESOME@ty_2Enum_2Enum)@(ap@(c_2Elist_2ELENGTH@A_27a)@V0l)))))))).
thf(conj_thm_2Ellist_2ELTAKE__fromList,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Ellist_2ELTAKE@A_27a)@(ap@(c_2Elist_2ELENGTH@A_27a)@V0l))@(ap@(c_2Ellist_2EfromList@A_27a)@V0l)) = (ap@(c_2Eoption_2ESOME@(ty_2Elist_2Elist@A_27a))@V0l)))))).
thf(conj_thm_2Ellist_2Efrom__toList,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(ty_2Elist_2Elist@A_27a)) => ((ap@(c_2Ellist_2EtoList@A_27a)@(ap@(c_2Ellist_2EfromList@A_27a)@V0l)) = (ap@(c_2Eoption_2ESOME@(ty_2Elist_2Elist@A_27a))@V0l)))))).
thf(conj_thm_2Ellist_2ELFINITE__toList,lemma,( ! [A_27a:del]: ( ! [V0ll:$i] : ((mem@V0ll@(ty_2Ellist_2Ellist@A_27a)) => ((p@(ap@(c_2Ellist_2ELFINITE@A_27a)@V0ll)) => (? [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) & ((ap@(c_2Ellist_2EtoList@A_27a)@V0ll) = (ap@(c_2Eoption_2ESOME@(ty_2Elist_2Elist@A_27a))@V1l))))))))).
thf(conj_thm_2Ellist_2ELFINITE__toList__SOME,lemma,( ! [A_27a:del]: ( ! [V0ll:$i] : ((mem@V0ll@(ty_2Ellist_2Ellist@A_27a)) => ((p@(ap@(c_2Ellist_2ELFINITE@A_27a)@V0ll)) <=> (p@(ap@(c_2Eoption_2EIS__SOME@(ty_2Elist_2Elist@A_27a))@(ap@(c_2Ellist_2EtoList@A_27a)@V0ll)))))))).
thf(conj_thm_2Ellist_2Eto__fromList,lemma,( ! [A_27a:del]: ( ! [V0ll:$i] : ((mem@V0ll@(ty_2Ellist_2Ellist@A_27a)) => ((p@(ap@(c_2Ellist_2ELFINITE@A_27a)@V0ll)) => ((ap@(c_2Ellist_2EfromList@A_27a)@(ap@(c_2Eoption_2ETHE@(ty_2Elist_2Elist@A_27a))@(ap@(c_2Ellist_2EtoList@A_27a)@V0ll))) = V0ll)))))).
thf(conj_thm_2Ellist_2ELTAKE__LAPPEND2,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l1:$i] : ((mem@V1l1@(ty_2Ellist_2Ellist@A_27a)) => ( ! [V2l2:$i] : ((mem@V2l2@(ty_2Ellist_2Ellist@A_27a)) => (((ap@(ap@(c_2Ellist_2ELTAKE@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1l1) = (c_2Eoption_2ENONE@(ty_2Elist_2Elist@A_27a))) => ((ap@(ap@(c_2Ellist_2ELTAKE@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(ap@(c_2Ellist_2ELAPPEND@A_27a)@V1l1)@V2l2)) = (ap@(ap@(c_2Eoption_2EOPTION__MAP@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))@(ap@(c_2Elist_2EAPPEND@A_27a)@(ap@(c_2Eoption_2ETHE@(ty_2Elist_2Elist@A_27a))@(ap@(c_2Ellist_2EtoList@A_27a)@V1l1))))@(ap@(ap@(c_2Ellist_2ELTAKE@A_27a)@(ap@(ap@c_2Earithmetic_2E_2D@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Eoption_2ETHE@ty_2Enum_2Enum)@(ap@(c_2Ellist_2ELLENGTH@A_27a)@V1l1))))@V2l2))))))))))).
thf(conj_thm_2Ellist_2ELNTH__fromList,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((ap@(ap@(c_2Ellist_2ELNTH@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Ellist_2EfromList@A_27a)@V1l)) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@A_27a))@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l)))@(ap@(c_2Eoption_2ESOME@A_27a)@(ap@(ap@(c_2Elist_2EEL@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1l)))@(c_2Eoption_2ENONE@A_27a)))))))).
thf(conj_thm_2Ellist_2Elnth__fromList__some,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1l:$i] : ((mem@V1l@(ty_2Elist_2Elist@A_27a)) => ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Elist_2ELENGTH@A_27a)@V1l))) <=> ((ap@(ap@(c_2Ellist_2ELNTH@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Ellist_2EfromList@A_27a)@V1l)) = (ap@(c_2Eoption_2ESOME@A_27a)@(ap@(ap@(c_2Elist_2EEL@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1l))))))))).
thf(ax_thm_2Ellist_2ELDROP,axiom,( ! [A_27a:del]: (( ! [V0ll:$i] : ((mem@V0ll@(ty_2Ellist_2Ellist@A_27a)) => ((ap@(ap@(c_2Ellist_2ELDROP@A_27a)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@V0ll) = (ap@(c_2Eoption_2ESOME@(ty_2Ellist_2Ellist@A_27a))@V0ll)))) & ( ! [V1n:tp__ty_2Enum_2Enum] : ( ! [V2ll:$i] : ((mem@V2ll@(ty_2Ellist_2Ellist@A_27a)) => ((ap@(ap@(c_2Ellist_2ELDROP@A_27a)@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n)))@V2ll) = (ap@(c_2Eoption_2EOPTION__JOIN@(ty_2Ellist_2Ellist@A_27a))@(ap@(ap@(c_2Eoption_2EOPTION__MAP@(ty_2Ellist_2Ellist@A_27a)@(ty_2Eoption_2Eoption@(ty_2Ellist_2Ellist@A_27a)))@(ap@(c_2Ellist_2ELDROP@A_27a)@(inj__ty_2Enum_2Enum @ V1n)))@(ap@(c_2Ellist_2ELTL@A_27a)@V2ll)))))))))).
thf(conj_thm_2Ellist_2ELDROP__FUNPOW,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1ll:$i] : ((mem@V1ll@(ty_2Ellist_2Ellist@A_27a)) => ((ap@(ap@(c_2Ellist_2ELDROP@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1ll) = (ap@(ap@(ap@(c_2Earithmetic_2EFUNPOW@(ty_2Eoption_2Eoption@(ty_2Ellist_2Ellist@A_27a)))@(lam@(ty_2Eoption_2Eoption@(ty_2Ellist_2Ellist@A_27a))@(^ [V2m:$i] : (ap@(ap@(c_2Eoption_2EOPTION__BIND@(ty_2Ellist_2Ellist@A_27a)@(ty_2Ellist_2Ellist@A_27a))@V2m)@(c_2Ellist_2ELTL@A_27a)))))@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Eoption_2ESOME@(ty_2Ellist_2Ellist@A_27a))@V1ll)))))))).
thf(conj_thm_2Ellist_2ELDROP__THM,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: (( ! [V0ll:$i] : ((mem@V0ll@(ty_2Ellist_2Ellist@A_27a)) => ((ap@(ap@(c_2Ellist_2ELDROP@A_27a)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@V0ll) = (ap@(c_2Eoption_2ESOME@(ty_2Ellist_2Ellist@A_27a))@V0ll)))) & (( ! [V1n:tp__ty_2Enum_2Enum] : ((ap@(ap@(c_2Ellist_2ELDROP@A_27b)@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n)))@(c_2Ellist_2ELNIL@A_27b)) = (c_2Eoption_2ENONE@(ty_2Ellist_2Ellist@A_27b)))) & ( ! [V2n:tp__ty_2Enum_2Enum] : ( ! [V3h:$i] : ((mem@V3h@A_27c) => ( ! [V4t:$i] : ((mem@V4t@(ty_2Ellist_2Ellist@A_27c)) => ((ap@(ap@(c_2Ellist_2ELDROP@A_27c)@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V2n)))@(ap@(ap@(c_2Ellist_2ELCONS@A_27c)@V3h)@V4t)) = (ap@(ap@(c_2Ellist_2ELDROP@A_27c)@(inj__ty_2Enum_2Enum @ V2n))@V4t))))))))))))).
thf(conj_thm_2Ellist_2ELDROP1__THM,lemma,( ! [A_27a:del]: ((ap@(c_2Ellist_2ELDROP@A_27a)@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))) = (c_2Ellist_2ELTL@A_27a)))).
thf(conj_thm_2Ellist_2ELNTH__HD__LDROP,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1ll:$i] : ((mem@V1ll@(ty_2Ellist_2Ellist@A_27a)) => ((ap@(ap@(c_2Ellist_2ELNTH@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1ll) = (ap@(ap@(c_2Eoption_2EOPTION__BIND@A_27a@(ty_2Ellist_2Ellist@A_27a))@(ap@(ap@(c_2Ellist_2ELDROP@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1ll))@(c_2Ellist_2ELHD@A_27a)))))))).
thf(conj_thm_2Ellist_2ENOT__LFINITE__TAKE,lemma,( ! [A_27a:del]: ( ! [V0ll:$i] : ((mem@V0ll@(ty_2Ellist_2Ellist@A_27a)) => ((~~ (p@(ap@(c_2Ellist_2ELFINITE@A_27a)@V0ll))) => ( ! [V1n:tp__ty_2Enum_2Enum] : (? [V2y:$i] : ((mem@V2y@(ty_2Elist_2Elist@A_27a)) & ((ap@(ap@(c_2Ellist_2ELTAKE@A_27a)@(inj__ty_2Enum_2Enum @ V1n))@V0ll) = (ap@(c_2Eoption_2ESOME@(ty_2Elist_2Elist@A_27a))@V2y)))))))))).
thf(conj_thm_2Ellist_2ELFINITE__TAKE,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1ll:$i] : ((mem@V1ll@(ty_2Ellist_2Ellist@A_27a)) => (((p@(ap@(c_2Ellist_2ELFINITE@A_27a)@V1ll)) & (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Eoption_2ETHE@ty_2Enum_2Enum)@(ap@(c_2Ellist_2ELLENGTH@A_27a)@V1ll))))) => (? [V2y:$i] : ((mem@V2y@(ty_2Elist_2Elist@A_27a)) & ((ap@(ap@(c_2Ellist_2ELTAKE@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1ll) = (ap@(c_2Eoption_2ESOME@(ty_2Elist_2Elist@A_27a))@V2y)))))))))).
thf(conj_thm_2Ellist_2ENOT__LFINITE__DROP,lemma,( ! [A_27a:del]: ( ! [V0ll:$i] : ((mem@V0ll@(ty_2Ellist_2Ellist@A_27a)) => ((~~ (p@(ap@(c_2Ellist_2ELFINITE@A_27a)@V0ll))) => ( ! [V1n:tp__ty_2Enum_2Enum] : (? [V2y:$i] : ((mem@V2y@(ty_2Ellist_2Ellist@A_27a)) & ((ap@(ap@(c_2Ellist_2ELDROP@A_27a)@(inj__ty_2Enum_2Enum @ V1n))@V0ll) = (ap@(c_2Eoption_2ESOME@(ty_2Ellist_2Ellist@A_27a))@V2y)))))))))).
thf(conj_thm_2Ellist_2ELFINITE__DROP,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1ll:$i] : ((mem@V1ll@(ty_2Ellist_2Ellist@A_27a)) => (((p@(ap@(c_2Ellist_2ELFINITE@A_27a)@V1ll)) & (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Eoption_2ETHE@ty_2Enum_2Enum)@(ap@(c_2Ellist_2ELLENGTH@A_27a)@V1ll))))) => (? [V2y:$i] : ((mem@V2y@(ty_2Ellist_2Ellist@A_27a)) & ((ap@(ap@(c_2Ellist_2ELDROP@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1ll) = (ap@(c_2Eoption_2ESOME@(ty_2Ellist_2Ellist@A_27a))@V2y)))))))))).
thf(conj_thm_2Ellist_2ELTAKE__DROP,lemma,( ! [A_27a:del]: (( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1ll:$i] : ((mem@V1ll@(ty_2Ellist_2Ellist@A_27a)) => ((~~ (p@(ap@(c_2Ellist_2ELFINITE@A_27a)@V1ll))) => ((ap@(ap@(c_2Ellist_2ELAPPEND@A_27a)@(ap@(c_2Ellist_2EfromList@A_27a)@(ap@(c_2Eoption_2ETHE@(ty_2Elist_2Elist@A_27a))@(ap@(ap@(c_2Ellist_2ELTAKE@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1ll))))@(ap@(c_2Eoption_2ETHE@(ty_2Ellist_2Ellist@A_27a))@(ap@(ap@(c_2Ellist_2ELDROP@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1ll))) = V1ll))))) & ( ! [V2n:tp__ty_2Enum_2Enum] : ( ! [V3ll:$i] : ((mem@V3ll@(ty_2Ellist_2Ellist@A_27a)) => (((p@(ap@(c_2Ellist_2ELFINITE@A_27a)@V3ll)) & (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V2n))@(ap@(c_2Eoption_2ETHE@ty_2Enum_2Enum)@(ap@(c_2Ellist_2ELLENGTH@A_27a)@V3ll))))) => ((ap@(ap@(c_2Ellist_2ELAPPEND@A_27a)@(ap@(c_2Ellist_2EfromList@A_27a)@(ap@(c_2Eoption_2ETHE@(ty_2Elist_2Elist@A_27a))@(ap@(ap@(c_2Ellist_2ELTAKE@A_27a)@(inj__ty_2Enum_2Enum @ V2n))@V3ll))))@(ap@(c_2Eoption_2ETHE@(ty_2Ellist_2Ellist@A_27a))@(ap@(ap@(c_2Ellist_2ELDROP@A_27a)@(inj__ty_2Enum_2Enum @ V2n))@V3ll))) = V3ll)))))))).
thf(conj_thm_2Ellist_2ELDROP__ADD,lemma,( ! [A_27a:del]: ( ! [V0k1:tp__ty_2Enum_2Enum] : ( ! [V1k2:tp__ty_2Enum_2Enum] : ( ! [V2x:$i] : ((mem@V2x@(ty_2Ellist_2Ellist@A_27a)) => ((ap@(ap@(c_2Ellist_2ELDROP@A_27a)@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0k1))@(inj__ty_2Enum_2Enum @ V1k2)))@V2x) = (ap@(ap@(ap@(c_2Eoption_2Eoption__CASE@(ty_2Ellist_2Ellist@A_27a)@(ty_2Eoption_2Eoption@(ty_2Ellist_2Ellist@A_27a)))@(ap@(ap@(c_2Ellist_2ELDROP@A_27a)@(inj__ty_2Enum_2Enum @ V0k1))@V2x))@(c_2Eoption_2ENONE@(ty_2Ellist_2Ellist@A_27a)))@(lam@(ty_2Ellist_2Ellist@A_27a)@(^ [V3ll:$i] : (ap@(ap@(c_2Ellist_2ELDROP@A_27a)@(inj__ty_2Enum_2Enum @ V1k2))@V3ll))))))))))).
thf(conj_thm_2Ellist_2ELDROP__SOME__LLENGTH,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1ll:$i] : ((mem@V1ll@(ty_2Ellist_2Ellist@A_27a)) => ( ! [V2l:$i] : ((mem@V2l@(ty_2Ellist_2Ellist@A_27a)) => ( ! [V3m:tp__ty_2Enum_2Enum] : ((((ap@(ap@(c_2Ellist_2ELDROP@A_27a)@(inj__ty_2Enum_2Enum @ V0n))@V1ll) = (ap@(c_2Eoption_2ESOME@(ty_2Ellist_2Ellist@A_27a))@V2l)) & ((surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum @ (ap@(c_2Ellist_2ELLENGTH@A_27a)@V1ll)) = (surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum @ (ap@(c_2Eoption_2ESOME@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V3m))))) => ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V3m))) & ((surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum @ (ap@(c_2Ellist_2ELLENGTH@A_27a)@V2l)) = (surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum @ (ap@(c_2Eoption_2ESOME@ty_2Enum_2Enum)@(ap@(ap@c_2Earithmetic_2E_2D@(inj__ty_2Enum_2Enum @ V3m))@(inj__ty_2Enum_2Enum @ V0n))))))))))))))).
thf(conj_thm_2Ellist_2ELFINITE__LNTH__NONE,conjecture,( ! [A_27a:del]: ( ! [V0ll:$i] : ((mem@V0ll@(ty_2Ellist_2Ellist@A_27a)) => ((p@(ap@(c_2Ellist_2ELFINITE@A_27a)@V0ll)) <=> (? [V1n:tp__ty_2Enum_2Enum] : ((ap@(ap@(c_2Ellist_2ELNTH@A_27a)@(inj__ty_2Enum_2Enum @ V1n))@V0ll) = (c_2Eoption_2ENONE@A_27a)))))))).
