include('Axioms/semi_ring^2.ax').
thf(tp_ty_2Ewellorder_2Ewellorder,type,( ty_2Ewellorder_2Ewellorder: del >del )).
thf(tp_c_2Ewellorder_2EADD1,type,(c_2Ewellorder_2EADD1:(del>$i))).
thf(mem_c_2Ewellorder_2EADD1,axiom,( ! [A_27a:del] : (mem@(c_2Ewellorder_2EADD1@A_27a)@(arr@A_27a@(arr@(ty_2Ewellorder_2Ewellorder@A_27a)@(ty_2Ewellorder_2Ewellorder@A_27a)))))).
thf(tp_c_2Ewellorder_2EChain,type,(c_2Ewellorder_2EChain:(del>$i))).
thf(mem_c_2Ewellorder_2EChain,axiom,( ! [A_27a:del] : (mem@(c_2Ewellorder_2EChain@A_27a)@(arr@(arr@(ty_2Epair_2Eprod@A_27a@A_27a)@bool)@(arr@(arr@A_27a@bool)@bool))))).
thf(tp_c_2Ewellorder_2EelsOf,type,(c_2Ewellorder_2EelsOf:(del>$i))).
thf(mem_c_2Ewellorder_2EelsOf,axiom,( ! [A_27a:del] : (mem@(c_2Ewellorder_2EelsOf@A_27a)@(arr@(ty_2Ewellorder_2Ewellorder@A_27a)@(arr@A_27a@bool))))).
thf(tp_c_2Ewellorder_2Efinite,type,(c_2Ewellorder_2Efinite:(del>$i))).
thf(mem_c_2Ewellorder_2Efinite,axiom,( ! [A_27a:del] : (mem@(c_2Ewellorder_2Efinite@A_27a)@(arr@(ty_2Ewellorder_2Ewellorder@A_27a)@bool)))).
thf(tp_c_2Ewellorder_2Efl,type,(c_2Ewellorder_2Efl:(del>$i))).
thf(mem_c_2Ewellorder_2Efl,axiom,( ! [A_27a:del] : (mem@(c_2Ewellorder_2Efl@A_27a)@(arr@(arr@(ty_2Epair_2Eprod@A_27a@A_27a)@bool)@(arr@A_27a@bool))))).
thf(tp_c_2Ewellorder_2EfromNatWO,type,(c_2Ewellorder_2EfromNatWO:(del>$i))).
thf(mem_c_2Ewellorder_2EfromNatWO,axiom,( ! [A_27a:del] : (mem@(c_2Ewellorder_2EfromNatWO@A_27a)@(arr@ty_2Enum_2Enum@(ty_2Ewellorder_2Ewellorder@(ty_2Esum_2Esum@ty_2Enum_2Enum@A_27a)))))).
thf(tp_c_2Ewellorder_2Eiseg,type,(c_2Ewellorder_2Eiseg:(del>$i))).
thf(mem_c_2Ewellorder_2Eiseg,axiom,( ! [A_27a:del] : (mem@(c_2Ewellorder_2Eiseg@A_27a)@(arr@(ty_2Ewellorder_2Ewellorder@A_27a)@(arr@A_27a@(arr@A_27a@bool)))))).
thf(tp_c_2Ewellorder_2Eorderiso,type,(c_2Ewellorder_2Eorderiso:(del>(del>$i)))).
thf(mem_c_2Ewellorder_2Eorderiso,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Ewellorder_2Eorderiso@A_27a@A_27b)@(arr@(ty_2Ewellorder_2Ewellorder@A_27a)@(arr@(ty_2Ewellorder_2Ewellorder@A_27b)@bool)))))).
thf(tp_c_2Ewellorder_2Eorderlt,type,(c_2Ewellorder_2Eorderlt:(del>(del>$i)))).
thf(mem_c_2Ewellorder_2Eorderlt,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Ewellorder_2Eorderlt@A_27a@A_27b)@(arr@(ty_2Ewellorder_2Ewellorder@A_27a)@(arr@(ty_2Ewellorder_2Ewellorder@A_27b)@bool)))))).
thf(tp_c_2Ewellorder_2Eposet,type,(c_2Ewellorder_2Eposet:(del>$i))).
thf(mem_c_2Ewellorder_2Eposet,axiom,( ! [A_27a:del] : (mem@(c_2Ewellorder_2Eposet@A_27a)@(arr@(arr@(ty_2Epair_2Eprod@A_27a@A_27a)@bool)@bool)))).
thf(tp_c_2Ewellorder_2Eremove,type,(c_2Ewellorder_2Eremove:(del>$i))).
thf(mem_c_2Ewellorder_2Eremove,axiom,( ! [A_27a:del] : (mem@(c_2Ewellorder_2Eremove@A_27a)@(arr@A_27a@(arr@(ty_2Ewellorder_2Ewellorder@A_27a)@(ty_2Ewellorder_2Ewellorder@A_27a)))))).
thf(tp_c_2Ewellorder_2EwZERO,type,(c_2Ewellorder_2EwZERO:(del>$i))).
thf(mem_c_2Ewellorder_2EwZERO,axiom,( ! [A_27a:del] : (mem@(c_2Ewellorder_2EwZERO@A_27a)@(ty_2Ewellorder_2Ewellorder@A_27a)))).
thf(tp_c_2Ewellorder_2Ewellfounded,type,(c_2Ewellorder_2Ewellfounded:(del>$i))).
thf(mem_c_2Ewellorder_2Ewellfounded,axiom,( ! [A_27a:del] : (mem@(c_2Ewellorder_2Ewellfounded@A_27a)@(arr@(arr@(ty_2Epair_2Eprod@A_27a@A_27a)@bool)@bool)))).
thf(tp_c_2Ewellorder_2Ewellorder,type,(c_2Ewellorder_2Ewellorder:(del>$i))).
thf(mem_c_2Ewellorder_2Ewellorder,axiom,( ! [A_27a:del] : (mem@(c_2Ewellorder_2Ewellorder@A_27a)@(arr@(arr@(ty_2Epair_2Eprod@A_27a@A_27a)@bool)@bool)))).
thf(tp_c_2Ewellorder_2Ewellorder__ABS,type,(c_2Ewellorder_2Ewellorder__ABS:(del>$i))).
thf(mem_c_2Ewellorder_2Ewellorder__ABS,axiom,( ! [A_27a:del] : (mem@(c_2Ewellorder_2Ewellorder__ABS@A_27a)@(arr@(arr@(ty_2Epair_2Eprod@A_27a@A_27a)@bool)@(ty_2Ewellorder_2Ewellorder@A_27a))))).
thf(tp_c_2Ewellorder_2Ewellorder__REP,type,(c_2Ewellorder_2Ewellorder__REP:(del>$i))).
thf(mem_c_2Ewellorder_2Ewellorder__REP,axiom,( ! [A_27a:del] : (mem@(c_2Ewellorder_2Ewellorder__REP@A_27a)@(arr@(ty_2Ewellorder_2Ewellorder@A_27a)@(arr@(ty_2Epair_2Eprod@A_27a@A_27a)@bool))))).
thf(tp_c_2Ewellorder_2Ewleast,type,(c_2Ewellorder_2Ewleast:(del>$i))).
thf(mem_c_2Ewellorder_2Ewleast,axiom,( ! [A_27a:del] : (mem@(c_2Ewellorder_2Ewleast@A_27a)@(arr@(ty_2Ewellorder_2Ewellorder@A_27a)@(arr@(arr@A_27a@bool)@(ty_2Eoption_2Eoption@A_27a)))))).
thf(tp_c_2Ewellorder_2Ewo2wo,type,(c_2Ewellorder_2Ewo2wo:(del>(del>$i)))).
thf(mem_c_2Ewellorder_2Ewo2wo,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Ewellorder_2Ewo2wo@A_27a@A_27b)@(arr@(ty_2Ewellorder_2Ewellorder@A_27a)@(arr@(ty_2Ewellorder_2Ewellorder@A_27b)@(arr@A_27a@(ty_2Eoption_2Eoption@A_27b)))))))).
thf(tp_c_2Ewellorder_2Ewobound,type,(c_2Ewellorder_2Ewobound:(del>$i))).
thf(mem_c_2Ewellorder_2Ewobound,axiom,( ! [A_27a:del] : (mem@(c_2Ewellorder_2Ewobound@A_27a)@(arr@A_27a@(arr@(ty_2Ewellorder_2Ewellorder@A_27a)@(ty_2Ewellorder_2Ewellorder@A_27a)))))).
thf(ax_thm_2Ewellorder_2Ewellfounded__def,axiom,( ! [A_27a:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@(ty_2Epair_2Eprod@A_27a@A_27a)@bool)) => ((p@(ap@(c_2Ewellorder_2Ewellfounded@A_27a)@V0R)) <=> ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ((? [V2w:$i] : ((mem@V2w@A_27a) & (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2w)@V1s)))) => (? [V3min:$i] : ((mem@V3min@A_27a) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3min)@V1s)) & ( ! [V4w:$i] : ((mem@V4w@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V4w)@V3min))@V0R)) => (~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V4w)@V1s))))))))))))))))).
thf(conj_thm_2Ewellorder_2Ewellfounded__WF,lemma,( ! [A_27a:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@(ty_2Epair_2Eprod@A_27a@A_27a)@bool)) => ((p@(ap@(c_2Ewellorder_2Ewellfounded@A_27a)@V0R)) <=> (p@(ap@(c_2Erelation_2EWF@A_27a)@(ap@(c_2Epair_2ECURRY@A_27a@A_27a@bool)@V0R)))))))).
thf(ax_thm_2Ewellorder_2Ewellorder__def,axiom,( ! [A_27a:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@(ty_2Epair_2Eprod@A_27a@A_27a)@bool)) => ((p@(ap@(c_2Ewellorder_2Ewellorder@A_27a)@V0R)) <=> ((p@(ap@(c_2Ewellorder_2Ewellfounded@A_27a)@(ap@(c_2Eset__relation_2Estrict@A_27a)@V0R))) & ((p@(ap@(ap@(c_2Eset__relation_2Elinear__order@A_27a)@V0R)@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@(ap@(c_2Eset__relation_2Edomain@A_27a@A_27a)@V0R))@(ap@(c_2Eset__relation_2Erange@A_27a@A_27a)@V0R)))) & (p@(ap@(ap@(c_2Eset__relation_2Ereflexive@A_27a)@V0R)@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@(ap@(c_2Eset__relation_2Edomain@A_27a@A_27a)@V0R))@(ap@(c_2Eset__relation_2Erange@A_27a@A_27a)@V0R))))))))))).
thf(conj_thm_2Ewellorder_2Ewellorder__EMPTY,lemma,( ! [A_27a:del]: (p@(ap@(c_2Ewellorder_2Ewellorder@A_27a)@(c_2Epred__set_2EEMPTY@(ty_2Epair_2Eprod@A_27a@A_27a)))))).
thf(conj_thm_2Ewellorder_2Ewellorder__SING,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1y:$i] : ((mem@V1y@A_27a) => ((p@(ap@(c_2Ewellorder_2Ewellorder@A_27a)@(ap@(ap@(c_2Epred__set_2EINSERT@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V0x)@V1y))@(c_2Epred__set_2EEMPTY@(ty_2Epair_2Eprod@A_27a@A_27a))))) <=> (V0x = V1y)))))))).
thf(conj_thm_2Ewellorder_2Errestrict__SUBSET,lemma,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(arr@(ty_2Epair_2Eprod@A_27a@A_27a)@bool)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => (p@(ap@(ap@(c_2Epred__set_2ESUBSET@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Eset__relation_2Errestrict@A_27a)@V0r)@V1s))@V0r)))))))).
thf(conj_thm_2Ewellorder_2Ewellfounded__subset,lemma,( ! [A_27a:del]: ( ! [V0r0:$i] : ((mem@V0r0@(arr@(ty_2Epair_2Eprod@A_27a@A_27a)@bool)) => ( ! [V1r:$i] : ((mem@V1r@(arr@(ty_2Epair_2Eprod@A_27a@A_27a)@bool)) => (((p@(ap@(c_2Ewellorder_2Ewellfounded@A_27a)@V1r)) & (p@(ap@(ap@(c_2Epred__set_2ESUBSET@(ty_2Epair_2Eprod@A_27a@A_27a))@V0r0)@V1r))) => (p@(ap@(c_2Ewellorder_2Ewellfounded@A_27a)@V0r0))))))))).
thf(ax_thm_2Ewellorder_2Ewellorder__TY__DEF,axiom,( ! [A_27a:del]: (? [V0rep:$i] : ((mem@V0rep@(arr@(ty_2Ewellorder_2Ewellorder@A_27a)@(arr@(ty_2Epair_2Eprod@A_27a@A_27a)@bool))) & (p@(ap@(ap@(c_2Ebool_2ETYPE__DEFINITION@(arr@(ty_2Epair_2Eprod@A_27a@A_27a)@bool)@(ty_2Ewellorder_2Ewellorder@A_27a))@(c_2Ewellorder_2Ewellorder@A_27a))@V0rep)))))).
thf(ax_thm_2Ewellorder_2Ewellorder__ABSREP,axiom,( ! [A_27a:del]: (( ! [V0a:$i] : ((mem@V0a@(ty_2Ewellorder_2Ewellorder@A_27a)) => ((ap@(c_2Ewellorder_2Ewellorder__ABS@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V0a)) = V0a))) & ( ! [V1r:$i] : ((mem@V1r@(arr@(ty_2Epair_2Eprod@A_27a@A_27a)@bool)) => ((p@(ap@(c_2Ewellorder_2Ewellorder@A_27a)@V1r)) <=> ((ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__ABS@A_27a)@V1r)) = V1r))))))).
thf(conj_thm_2Ewellorder_2EmkWO__destWO,lemma,( ! [A_27a:del]: ( ! [V0a:$i] : ((mem@V0a@(ty_2Ewellorder_2Ewellorder@A_27a)) => ((ap@(c_2Ewellorder_2Ewellorder__ABS@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V0a)) = V0a))))).
thf(conj_thm_2Ewellorder_2EdestWO__mkWO,lemma,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(arr@(ty_2Epair_2Eprod@A_27a@A_27a)@bool)) => ((p@(ap@(c_2Ewellorder_2Ewellorder@A_27a)@V0r)) => ((ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__ABS@A_27a)@V0r)) = V0r)))))).
thf(ax_thm_2Ewellorder_2EelsOf__def,axiom,( ! [A_27a:del]: ( ! [V0w:$i] : ((mem@V0w@(ty_2Ewellorder_2Ewellorder@A_27a)) => ((ap@(c_2Ewellorder_2EelsOf@A_27a)@V0w) = (ap@(ap@(c_2Epred__set_2EUNION@A_27a)@(ap@(c_2Eset__relation_2Edomain@A_27a@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V0w)))@(ap@(c_2Eset__relation_2Erange@A_27a@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V0w)))))))).
thf(conj_thm_2Ewellorder_2EWIN__elsOf,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1y:$i] : ((mem@V1y@A_27a) => ( ! [V2w:$i] : ((mem@V2w@(ty_2Ewellorder_2Ewellorder@A_27a)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V0x)@V1y))@(ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V2w)))) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@(ap@(c_2Ewellorder_2EelsOf@A_27a)@V2w))) & (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1y)@(ap@(c_2Ewellorder_2EelsOf@A_27a)@V2w))))))))))))).
thf(conj_thm_2Ewellorder_2EWLE__elsOf,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1y:$i] : ((mem@V1y@A_27a) => ( ! [V2w:$i] : ((mem@V2w@(ty_2Ewellorder_2Ewellorder@A_27a)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V0x)@V1y))@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V2w))) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@(ap@(c_2Ewellorder_2EelsOf@A_27a)@V2w))) & (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1y)@(ap@(c_2Ewellorder_2EelsOf@A_27a)@V2w))))))))))))).
thf(conj_thm_2Ewellorder_2EWIN__trichotomy,lemma,( ! [A_27a:del]: ( ! [V0w:$i] : ((mem@V0w@(ty_2Ewellorder_2Ewellorder@A_27a)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ( ! [V2y:$i] : ((mem@V2y@A_27a) => (((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1x)@(ap@(c_2Ewellorder_2EelsOf@A_27a)@V0w))) & (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2y)@(ap@(c_2Ewellorder_2EelsOf@A_27a)@V0w)))) => ((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V1x)@V2y))@(ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V0w)))) | ((V1x = V2y) | (p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V2y)@V1x))@(ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V0w))))))))))))))).
thf(conj_thm_2Ewellorder_2EWIN__REFL,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1w:$i] : ((mem@V1w@(ty_2Ewellorder_2Ewellorder@A_27a)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V0x)@V0x))@(ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V1w)))) <=> $false))))))).
thf(conj_thm_2Ewellorder_2EWLE__TRANS,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1y:$i] : ((mem@V1y@A_27a) => ( ! [V2w:$i] : ((mem@V2w@(ty_2Ewellorder_2Ewellorder@A_27a)) => ( ! [V3z:$i] : ((mem@V3z@A_27a) => (((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V0x)@V1y))@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V2w))) & (p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V1y)@V3z))@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V2w)))) => (p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V0x)@V3z))@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V2w)))))))))))))).
thf(conj_thm_2Ewellorder_2EWLE__ANTISYM,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1y:$i] : ((mem@V1y@A_27a) => ( ! [V2w:$i] : ((mem@V2w@(ty_2Ewellorder_2Ewellorder@A_27a)) => (((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V0x)@V1y))@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V2w))) & (p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V1y)@V0x))@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V2w)))) => (V0x = V1y)))))))))).
thf(conj_thm_2Ewellorder_2EWIN__WLE,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1y:$i] : ((mem@V1y@A_27a) => ( ! [V2w:$i] : ((mem@V2w@(ty_2Ewellorder_2Ewellorder@A_27a)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V0x)@V1y))@(ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V2w)))) => (p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V0x)@V1y))@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V2w)))))))))))).
thf(conj_thm_2Ewellorder_2EelsOf__WLE,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1w:$i] : ((mem@V1w@(ty_2Ewellorder_2Ewellorder@A_27a)) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@(ap@(c_2Ewellorder_2EelsOf@A_27a)@V1w))) <=> (p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V0x)@V0x))@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V1w)))))))))).
thf(conj_thm_2Ewellorder_2Etransitive__strict,lemma,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(arr@(ty_2Epair_2Eprod@A_27a@A_27a)@bool)) => (((p@(ap@(c_2Eset__relation_2Etransitive@A_27a)@V0r)) & (p@(ap@(c_2Eset__relation_2Eantisym@A_27a)@V0r))) => (p@(ap@(c_2Eset__relation_2Etransitive@A_27a)@(ap@(c_2Eset__relation_2Estrict@A_27a)@V0r)))))))).
thf(conj_thm_2Ewellorder_2EWIN__TRANS,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1y:$i] : ((mem@V1y@A_27a) => ( ! [V2w:$i] : ((mem@V2w@(ty_2Ewellorder_2Ewellorder@A_27a)) => ( ! [V3z:$i] : ((mem@V3z@A_27a) => (((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V0x)@V1y))@(ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V2w)))) & (p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V1y)@V3z))@(ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V2w))))) => (p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V0x)@V3z))@(ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V2w))))))))))))))).
thf(conj_thm_2Ewellorder_2EWIN__WF,lemma,( ! [A_27a:del]: ( ! [V0w:$i] : ((mem@V0w@(ty_2Ewellorder_2Ewellorder@A_27a)) => (p@(ap@(c_2Ewellorder_2Ewellfounded@A_27a)@(lam@(ty_2Epair_2Eprod@A_27a@A_27a)@(^ [V1p:$i] : (ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@V1p)@(ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V0w))))))))))).
thf(conj_thm_2Ewellorder_2EWIN__WF2,lemma,( ! [A_27a:del]: ( ! [V0w:$i] : ((mem@V0w@(ty_2Ewellorder_2Ewellorder@A_27a)) => (p@(ap@(c_2Erelation_2EWF@A_27a)@(lam@A_27a@(^ [V1x:$i] : (lam@A_27a@(^ [V2y:$i] : (ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V1x)@V2y))@(ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V0w))))))))))))).
thf(ax_thm_2Ewellorder_2Eiseg__def,axiom,( ! [A_27a:del]: ( ! [V0w:$i] : ((mem@V0w@(ty_2Ewellorder_2Ewellorder@A_27a)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ((ap@(ap@(c_2Ewellorder_2Eiseg@A_27a)@V0w)@V1x) = (ap@(c_2Epred__set_2EGSPEC@A_27a@A_27a)@(lam@A_27a@(^ [V2y:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27a@bool)@V2y)@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V2y)@V1x))@(ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V0w)))))))))))))).
thf(conj_thm_2Ewellorder_2Estrict__subset,lemma,( ! [A_27a:del]: ( ! [V0r1:$i] : ((mem@V0r1@(arr@(ty_2Epair_2Eprod@A_27a@A_27a)@bool)) => ( ! [V1r2:$i] : ((mem@V1r2@(arr@(ty_2Epair_2Eprod@A_27a@A_27a)@bool)) => ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@(ty_2Epair_2Eprod@A_27a@A_27a))@V0r1)@V1r2)) => (p@(ap@(ap@(c_2Epred__set_2ESUBSET@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(c_2Eset__relation_2Estrict@A_27a)@V0r1))@(ap@(c_2Eset__relation_2Estrict@A_27a)@V1r2)))))))))).
thf(conj_thm_2Ewellorder_2Etransitive__rrestrict,lemma,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(arr@(ty_2Epair_2Eprod@A_27a@A_27a)@bool)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ((p@(ap@(c_2Eset__relation_2Etransitive@A_27a)@V0r)) => (p@(ap@(c_2Eset__relation_2Etransitive@A_27a)@(ap@(ap@(c_2Eset__relation_2Errestrict@A_27a)@V0r)@V1s)))))))))).
thf(conj_thm_2Ewellorder_2Eantisym__rrestrict,lemma,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(arr@(ty_2Epair_2Eprod@A_27a@A_27a)@bool)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ((p@(ap@(c_2Eset__relation_2Eantisym@A_27a)@V0r)) => (p@(ap@(c_2Eset__relation_2Eantisym@A_27a)@(ap@(ap@(c_2Eset__relation_2Errestrict@A_27a)@V0r)@V1s)))))))))).
thf(conj_thm_2Ewellorder_2Elinear__order__rrestrict,lemma,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(arr@(ty_2Epair_2Eprod@A_27a@A_27a)@bool)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Eset__relation_2Elinear__order@A_27a)@V0r)@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@(ap@(c_2Eset__relation_2Edomain@A_27a@A_27a)@V0r))@(ap@(c_2Eset__relation_2Erange@A_27a@A_27a)@V0r)))) => (p@(ap@(ap@(c_2Eset__relation_2Elinear__order@A_27a)@(ap@(ap@(c_2Eset__relation_2Errestrict@A_27a)@V0r)@V1s))@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@(ap@(c_2Eset__relation_2Edomain@A_27a@A_27a)@(ap@(ap@(c_2Eset__relation_2Errestrict@A_27a)@V0r)@V1s)))@(ap@(c_2Eset__relation_2Erange@A_27a@A_27a)@(ap@(ap@(c_2Eset__relation_2Errestrict@A_27a)@V0r)@V1s)))))))))))).
thf(conj_thm_2Ewellorder_2Ereflexive__rrestrict,lemma,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(arr@(ty_2Epair_2Eprod@A_27a@A_27a)@bool)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Eset__relation_2Ereflexive@A_27a)@V0r)@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@(ap@(c_2Eset__relation_2Edomain@A_27a@A_27a)@V0r))@(ap@(c_2Eset__relation_2Erange@A_27a@A_27a)@V0r)))) => (p@(ap@(ap@(c_2Eset__relation_2Ereflexive@A_27a)@(ap@(ap@(c_2Eset__relation_2Errestrict@A_27a)@V0r)@V1s))@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@(ap@(c_2Eset__relation_2Edomain@A_27a@A_27a)@(ap@(ap@(c_2Eset__relation_2Errestrict@A_27a)@V0r)@V1s)))@(ap@(c_2Eset__relation_2Erange@A_27a@A_27a)@(ap@(ap@(c_2Eset__relation_2Errestrict@A_27a)@V0r)@V1s)))))))))))).
thf(conj_thm_2Ewellorder_2Ewellorder__rrestrict,lemma,( ! [A_27a:del]: ( ! [V0w:$i] : ((mem@V0w@(ty_2Ewellorder_2Ewellorder@A_27a)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => (p@(ap@(c_2Ewellorder_2Ewellorder@A_27a)@(ap@(ap@(c_2Eset__relation_2Errestrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V0w))@V1s))))))))).
thf(ax_thm_2Ewellorder_2Ewobound__def,axiom,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1w:$i] : ((mem@V1w@(ty_2Ewellorder_2Ewellorder@A_27a)) => ((ap@(ap@(c_2Ewellorder_2Ewobound@A_27a)@V0x)@V1w) = (ap@(c_2Ewellorder_2Ewellorder__ABS@A_27a)@(ap@(ap@(c_2Eset__relation_2Errestrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V1w))@(ap@(ap@(c_2Ewellorder_2Eiseg@A_27a)@V1w)@V0x)))))))))).
thf(conj_thm_2Ewellorder_2EWIN__wobound,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1y:$i] : ((mem@V1y@A_27a) => ( ! [V2z:$i] : ((mem@V2z@A_27a) => ( ! [V3w:$i] : ((mem@V3w@(ty_2Ewellorder_2Ewellorder@A_27a)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V0x)@V1y))@(ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@(ap@(ap@(c_2Ewellorder_2Ewobound@A_27a)@V2z)@V3w))))) <=> ((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V0x)@V2z))@(ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V3w)))) & ((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V1y)@V2z))@(ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V3w)))) & (p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V0x)@V1y))@(ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V3w))))))))))))))))).
thf(conj_thm_2Ewellorder_2EWLE__wobound,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1y:$i] : ((mem@V1y@A_27a) => ( ! [V2z:$i] : ((mem@V2z@A_27a) => ( ! [V3w:$i] : ((mem@V3w@(ty_2Ewellorder_2Ewellorder@A_27a)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V0x)@V1y))@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@(ap@(ap@(c_2Ewellorder_2Ewobound@A_27a)@V2z)@V3w)))) <=> ((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V0x)@V2z))@(ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V3w)))) & ((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V1y)@V2z))@(ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V3w)))) & (p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V0x)@V1y))@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V3w)))))))))))))))).
thf(conj_thm_2Ewellorder_2Ewellorder__cases,lemma,( ! [A_27a:del]: ( ! [V0w:$i] : ((mem@V0w@(ty_2Ewellorder_2Ewellorder@A_27a)) => (? [V1s:$i] : ((mem@V1s@(arr@(ty_2Epair_2Eprod@A_27a@A_27a)@bool)) & ((p@(ap@(c_2Ewellorder_2Ewellorder@A_27a)@V1s)) & (V0w = (ap@(c_2Ewellorder_2Ewellorder__ABS@A_27a)@V1s))))))))).
thf(conj_thm_2Ewellorder_2EWEXTENSION,lemma,( ! [A_27a:del]: ( ! [V0w1:$i] : ((mem@V0w1@(ty_2Ewellorder_2Ewellorder@A_27a)) => ( ! [V1w2:$i] : ((mem@V1w2@(ty_2Ewellorder_2Ewellorder@A_27a)) => ((V0w1 = V1w2) <=> ( ! [V2a:$i] : ((mem@V2a@A_27a) => ( ! [V3b:$i] : ((mem@V3b@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V2a)@V3b))@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V0w1))) <=> (p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V2a)@V3b))@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V1w2))))))))))))))).
thf(conj_thm_2Ewellorder_2Ewobound2,lemma,( ! [A_27a:del]: ( ! [V0a:$i] : ((mem@V0a@A_27a) => ( ! [V1b:$i] : ((mem@V1b@A_27a) => ( ! [V2w:$i] : ((mem@V2w@(ty_2Ewellorder_2Ewellorder@A_27a)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V0a)@V1b))@(ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V2w)))) => ((ap@(ap@(c_2Ewellorder_2Ewobound@A_27a)@V0a)@(ap@(ap@(c_2Ewellorder_2Ewobound@A_27a)@V1b)@V2w)) = (ap@(ap@(c_2Ewellorder_2Ewobound@A_27a)@V0a)@V2w))))))))))).
thf(stp_c_ty_2Epair_2Eprod_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum_o,type,(tp__c_ty_2Epair_2Eprod_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum_o : $tType)).
thf(stp_inj_c_ty_2Epair_2Eprod_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum_o,type,(inj__c_ty_2Epair_2Eprod_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum_o : (tp__c_ty_2Epair_2Eprod_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum_o > $i))).
thf(stp_surj_c_ty_2Epair_2Eprod_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum_o,type,(surj__c_ty_2Epair_2Eprod_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum_o : ($i > tp__c_ty_2Epair_2Eprod_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum_o))).
thf(stp_inj_surj_c_ty_2Epair_2Eprod_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum_o,axiom,( ! [X:tp__c_ty_2Epair_2Eprod_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum_o] : ((surj__c_ty_2Epair_2Eprod_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum_o @ (inj__c_ty_2Epair_2Eprod_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum_o @ X)) = X))).
thf(stp_inj_mem_c_ty_2Epair_2Eprod_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum_o,axiom,( ! [X:tp__c_ty_2Epair_2Eprod_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum_o] : (mem @ (inj__c_ty_2Epair_2Eprod_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum_o @ X) @ (ty_2Epair_2Eprod@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@bool)))).
thf(stp_iso_mem_c_ty_2Epair_2Eprod_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum_o,axiom,( ! [X:$i] : ((mem @ X @ (ty_2Epair_2Eprod@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@bool)) => (X = (inj__c_ty_2Epair_2Eprod_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum_o @ (surj__c_ty_2Epair_2Eprod_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum_o @ X)))))).
thf(conj_thm_2Ewellorder_2Ewellorder__fromNat,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : (p@(ap@(c_2Ewellorder_2Ewellorder@ty_2Enum_2Enum)@(ap@(c_2Epred__set_2EGSPEC@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(ap@(c_2Epair_2EUNCURRY@ty_2Enum_2Enum@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@bool))@(lam@ty_2Enum_2Enum@(^ [V1i:$i] : (lam@ty_2Enum_2Enum@(^ [V2j:$i] : (ap@(ap@(c_2Epair_2E_2C@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum)@bool)@(ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@ty_2Enum_2Enum)@V1i)@V2j))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Earithmetic_2E_3C_3D@V1i)@V2j))@(ap@(ap@c_2Eprim__rec_2E_3C@V2j)@(inj__ty_2Enum_2Enum @ V0n)))))))))))))).
thf(conj_thm_2Ewellorder_2EINJ__preserves__transitive,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0r:$i] : ((mem@V0r@(arr@(ty_2Epair_2Eprod@A_27a@A_27a)@bool)) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27a@A_27b)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27b@bool)) => (((p@(ap@(c_2Eset__relation_2Etransitive@A_27a)@V0r)) & (p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27a@A_27b)@V1f)@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@(ap@(c_2Eset__relation_2Edomain@A_27a@A_27a)@V0r))@(ap@(c_2Eset__relation_2Erange@A_27a@A_27a)@V0r)))@V2t))) => (p@(ap@(c_2Eset__relation_2Etransitive@A_27b)@(ap@(ap@(c_2Epred__set_2EIMAGE@(ty_2Epair_2Eprod@A_27a@A_27a)@(ty_2Epair_2Eprod@A_27b@A_27b))@(ap@(ap@(c_2Epair_2E_23_23@A_27a@A_27a@A_27b@A_27b)@V1f)@V1f))@V0r))))))))))))).
thf(conj_thm_2Ewellorder_2EINJ__preserves__antisym,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0r:$i] : ((mem@V0r@(arr@(ty_2Epair_2Eprod@A_27a@A_27a)@bool)) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27a@A_27b)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27b@bool)) => (((p@(ap@(c_2Eset__relation_2Eantisym@A_27a)@V0r)) & (p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27a@A_27b)@V1f)@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@(ap@(c_2Eset__relation_2Edomain@A_27a@A_27a)@V0r))@(ap@(c_2Eset__relation_2Erange@A_27a@A_27a)@V0r)))@V2t))) => (p@(ap@(c_2Eset__relation_2Eantisym@A_27b)@(ap@(ap@(c_2Epred__set_2EIMAGE@(ty_2Epair_2Eprod@A_27a@A_27a)@(ty_2Epair_2Eprod@A_27b@A_27b))@(ap@(ap@(c_2Epair_2E_23_23@A_27a@A_27a@A_27b@A_27b)@V1f)@V1f))@V0r))))))))))))).
thf(conj_thm_2Ewellorder_2EINJ__preserves__linear__order,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0r:$i] : ((mem@V0r@(arr@(ty_2Epair_2Eprod@A_27a@A_27a)@bool)) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27a@A_27b)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27b@bool)) => (((p@(ap@(ap@(c_2Eset__relation_2Elinear__order@A_27a)@V0r)@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@(ap@(c_2Eset__relation_2Edomain@A_27a@A_27a)@V0r))@(ap@(c_2Eset__relation_2Erange@A_27a@A_27a)@V0r)))) & (p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27a@A_27b)@V1f)@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@(ap@(c_2Eset__relation_2Edomain@A_27a@A_27a)@V0r))@(ap@(c_2Eset__relation_2Erange@A_27a@A_27a)@V0r)))@V2t))) => (p@(ap@(ap@(c_2Eset__relation_2Elinear__order@A_27b)@(ap@(ap@(c_2Epred__set_2EIMAGE@(ty_2Epair_2Eprod@A_27a@A_27a)@(ty_2Epair_2Eprod@A_27b@A_27b))@(ap@(ap@(c_2Epair_2E_23_23@A_27a@A_27a@A_27b@A_27b)@V1f)@V1f))@V0r))@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V1f)@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@(ap@(c_2Eset__relation_2Edomain@A_27a@A_27a)@V0r))@(ap@(c_2Eset__relation_2Erange@A_27a@A_27a)@V0r))))))))))))))).
thf(conj_thm_2Ewellorder_2Edomain__IMAGE__ff,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)) => ( ! [V2r:$i] : ((mem@V2r@(arr@(ty_2Epair_2Eprod@A_27c@A_27d)@bool)) => ((ap@(c_2Eset__relation_2Edomain@A_27a@A_27b)@(ap@(ap@(c_2Epred__set_2EIMAGE@(ty_2Epair_2Eprod@A_27c@A_27d)@(ty_2Epair_2Eprod@A_27a@A_27b))@(ap@(ap@(c_2Epair_2E_23_23@A_27c@A_27d@A_27a@A_27b)@V0f)@V1g))@V2r)) = (ap@(ap@(c_2Epred__set_2EIMAGE@A_27c@A_27a)@V0f)@(ap@(c_2Eset__relation_2Edomain@A_27c@A_27d)@V2r)))))))))))))).
thf(conj_thm_2Ewellorder_2Erange__IMAGE__ff,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27c@A_27b)) => ( ! [V1g:$i] : ((mem@V1g@(arr@A_27d@A_27a)) => ( ! [V2r:$i] : ((mem@V2r@(arr@(ty_2Epair_2Eprod@A_27c@A_27d)@bool)) => ((ap@(c_2Eset__relation_2Erange@A_27a@A_27b)@(ap@(ap@(c_2Epred__set_2EIMAGE@(ty_2Epair_2Eprod@A_27c@A_27d)@(ty_2Epair_2Eprod@A_27b@A_27a))@(ap@(ap@(c_2Epair_2E_23_23@A_27c@A_27d@A_27b@A_27a)@V0f)@V1g))@V2r)) = (ap@(ap@(c_2Epred__set_2EIMAGE@A_27d@A_27a)@V1g)@(ap@(c_2Eset__relation_2Erange@A_27d@A_27c)@V2r)))))))))))))).
thf(conj_thm_2Ewellorder_2EINJ__preserves__wellorder,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0r:$i] : ((mem@V0r@(arr@(ty_2Epair_2Eprod@A_27a@A_27a)@bool)) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27a@A_27b)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27b@bool)) => (((p@(ap@(c_2Ewellorder_2Ewellorder@A_27a)@V0r)) & (p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27a@A_27b)@V1f)@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@(ap@(c_2Eset__relation_2Edomain@A_27a@A_27a)@V0r))@(ap@(c_2Eset__relation_2Erange@A_27a@A_27a)@V0r)))@V2t))) => (p@(ap@(c_2Ewellorder_2Ewellorder@A_27b)@(ap@(ap@(c_2Epred__set_2EIMAGE@(ty_2Epair_2Eprod@A_27a@A_27a)@(ty_2Epair_2Eprod@A_27b@A_27b))@(ap@(ap@(c_2Epair_2E_23_23@A_27a@A_27a@A_27b@A_27b)@V1f)@V1f))@V0r))))))))))))).
thf(conj_thm_2Ewellorder_2Ewellorder__fromNat__SUM,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : (p@(ap@(c_2Ewellorder_2Ewellorder@(ty_2Esum_2Esum@ty_2Enum_2Enum@A_27a))@(ap@(c_2Epred__set_2EGSPEC@(ty_2Epair_2Eprod@(ty_2Esum_2Esum@ty_2Enum_2Enum@A_27a)@(ty_2Esum_2Esum@ty_2Enum_2Enum@A_27a))@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(ap@(c_2Epair_2EUNCURRY@ty_2Enum_2Enum@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epair_2Eprod@(ty_2Esum_2Esum@ty_2Enum_2Enum@A_27a)@(ty_2Esum_2Esum@ty_2Enum_2Enum@A_27a))@bool))@(lam@ty_2Enum_2Enum@(^ [V1i:$i] : (lam@ty_2Enum_2Enum@(^ [V2j:$i] : (ap@(ap@(c_2Epair_2E_2C@(ty_2Epair_2Eprod@(ty_2Esum_2Esum@ty_2Enum_2Enum@A_27a)@(ty_2Esum_2Esum@ty_2Enum_2Enum@A_27a))@bool)@(ap@(ap@(c_2Epair_2E_2C@(ty_2Esum_2Esum@ty_2Enum_2Enum@A_27a)@(ty_2Esum_2Esum@ty_2Enum_2Enum@A_27a))@(ap@(c_2Esum_2EINL@ty_2Enum_2Enum@A_27a)@V1i))@(ap@(c_2Esum_2EINL@ty_2Enum_2Enum@A_27a)@V2j)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Earithmetic_2E_3C_3D@V1i)@V2j))@(ap@(ap@c_2Eprim__rec_2E_3C@V2j)@(inj__ty_2Enum_2Enum @ V0n))))))))))))))).
thf(ax_thm_2Ewellorder_2EfromNatWO__def,axiom,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ((ap@(c_2Ewellorder_2EfromNatWO@A_27a)@(inj__ty_2Enum_2Enum @ V0n)) = (ap@(c_2Ewellorder_2Ewellorder__ABS@(ty_2Esum_2Esum@ty_2Enum_2Enum@A_27a))@(ap@(c_2Epred__set_2EGSPEC@(ty_2Epair_2Eprod@(ty_2Esum_2Esum@ty_2Enum_2Enum@A_27a)@(ty_2Esum_2Esum@ty_2Enum_2Enum@A_27a))@(ty_2Epair_2Eprod@ty_2Enum_2Enum@ty_2Enum_2Enum))@(ap@(c_2Epair_2EUNCURRY@ty_2Enum_2Enum@ty_2Enum_2Enum@(ty_2Epair_2Eprod@(ty_2Epair_2Eprod@(ty_2Esum_2Esum@ty_2Enum_2Enum@A_27a)@(ty_2Esum_2Esum@ty_2Enum_2Enum@A_27a))@bool))@(lam@ty_2Enum_2Enum@(^ [V1i:$i] : (lam@ty_2Enum_2Enum@(^ [V2j:$i] : (ap@(ap@(c_2Epair_2E_2C@(ty_2Epair_2Eprod@(ty_2Esum_2Esum@ty_2Enum_2Enum@A_27a)@(ty_2Esum_2Esum@ty_2Enum_2Enum@A_27a))@bool)@(ap@(ap@(c_2Epair_2E_2C@(ty_2Esum_2Esum@ty_2Enum_2Enum@A_27a)@(ty_2Esum_2Esum@ty_2Enum_2Enum@A_27a))@(ap@(c_2Esum_2EINL@ty_2Enum_2Enum@A_27a)@V1i))@(ap@(c_2Esum_2EINL@ty_2Enum_2Enum@A_27a)@V2j)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Earithmetic_2E_3C_3D@V1i)@V2j))@(ap@(ap@c_2Eprim__rec_2E_3C@V2j)@(inj__ty_2Enum_2Enum @ V0n))))))))))))))).
thf(conj_thm_2Ewellorder_2EfromNatWO__11,lemma,( ! [A_27a:del]: ( ! [V0i:tp__ty_2Enum_2Enum] : ( ! [V1j:tp__ty_2Enum_2Enum] : (((ap@(c_2Ewellorder_2EfromNatWO@A_27a)@(inj__ty_2Enum_2Enum @ V0i)) = (ap@(c_2Ewellorder_2EfromNatWO@A_27a)@(inj__ty_2Enum_2Enum @ V1j))) <=> (V0i = V1j)))))).
thf(conj_thm_2Ewellorder_2EelsOf__fromNatWO,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ((ap@(c_2Ewellorder_2EelsOf@(ty_2Esum_2Esum@ty_2Enum_2Enum@A_27a))@(ap@(c_2Ewellorder_2EfromNatWO@A_27a)@(inj__ty_2Enum_2Enum @ V0n))) = (ap@(ap@(c_2Epred__set_2EIMAGE@ty_2Enum_2Enum@(ty_2Esum_2Esum@ty_2Enum_2Enum@A_27a))@(c_2Esum_2EINL@ty_2Enum_2Enum@A_27a))@(ap@c_2Epred__set_2Ecount@(inj__ty_2Enum_2Enum @ V0n))))))).
thf(conj_thm_2Ewellorder_2EWLE__WIN,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1y:$i] : ((mem@V1y@A_27a) => ( ! [V2w:$i] : ((mem@V2w@(ty_2Ewellorder_2Ewellorder@A_27a)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V0x)@V1y))@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V2w))) => ((V0x = V1y) | (p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V0x)@V1y))@(ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V2w)))))))))))))).
thf(conj_thm_2Ewellorder_2EelsOf__wobound,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1w:$i] : ((mem@V1w@(ty_2Ewellorder_2Ewellorder@A_27a)) => ((ap@(c_2Ewellorder_2EelsOf@A_27a)@(ap@(ap@(c_2Ewellorder_2Ewobound@A_27a)@V0x)@V1w)) = (ap@(c_2Epred__set_2EGSPEC@A_27a@A_27a)@(lam@A_27a@(^ [V2y:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27a@bool)@V2y)@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V2y)@V0x))@(ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V1w)))))))))))))).
thf(ax_thm_2Ewellorder_2Eorderiso__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0w1:$i] : ((mem@V0w1@(ty_2Ewellorder_2Ewellorder@A_27a)) => ( ! [V1w2:$i] : ((mem@V1w2@(ty_2Ewellorder_2Ewellorder@A_27b)) => ((p@(ap@(ap@(c_2Ewellorder_2Eorderiso@A_27a@A_27b)@V0w1)@V1w2)) <=> (? [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27b)) & (( ! [V3x:$i] : ((mem@V3x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@(ap@(c_2Ewellorder_2EelsOf@A_27a)@V0w1))) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@(ap@V2f@V3x))@(ap@(c_2Ewellorder_2EelsOf@A_27b)@V1w2)))))) & (( ! [V4x1:$i] : ((mem@V4x1@A_27a) => ( ! [V5x2:$i] : ((mem@V5x2@A_27a) => (((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V4x1)@(ap@(c_2Ewellorder_2EelsOf@A_27a)@V0w1))) & (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V5x2)@(ap@(c_2Ewellorder_2EelsOf@A_27a)@V0w1)))) => (((ap@V2f@V4x1) = (ap@V2f@V5x2)) <=> (V4x1 = V5x2))))))) & (( ! [V6y:$i] : ((mem@V6y@A_27b) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V6y)@(ap@(c_2Ewellorder_2EelsOf@A_27b)@V1w2))) => (? [V7x:$i] : ((mem@V7x@A_27a) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V7x)@(ap@(c_2Ewellorder_2EelsOf@A_27a)@V0w1))) & ((ap@V2f@V7x) = V6y))))))) & ( ! [V8x:$i] : ((mem@V8x@A_27a) => ( ! [V9y:$i] : ((mem@V9y@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V8x)@V9y))@(ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V0w1)))) => (p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27b@A_27b))@(ap@(ap@(c_2Epair_2E_2C@A_27b@A_27b)@(ap@V2f@V8x))@(ap@V2f@V9y)))@(ap@(c_2Eset__relation_2Estrict@A_27b)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27b)@V1w2)))))))))))))))))))))).
thf(conj_thm_2Ewellorder_2Eorderiso__thm,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0w1:$i] : ((mem@V0w1@(ty_2Ewellorder_2Ewellorder@A_27a)) => ( ! [V1w2:$i] : ((mem@V1w2@(ty_2Ewellorder_2Ewellorder@A_27b)) => ((p@(ap@(ap@(c_2Ewellorder_2Eorderiso@A_27a@A_27b)@V0w1)@V1w2)) <=> (? [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27b)) & ((p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27b)@V2f)@(ap@(c_2Ewellorder_2EelsOf@A_27a)@V0w1))@(ap@(c_2Ewellorder_2EelsOf@A_27b)@V1w2))) & ( ! [V3x:$i] : ((mem@V3x@A_27a) => ( ! [V4y:$i] : ((mem@V4y@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V3x)@V4y))@(ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V0w1)))) => (p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27b@A_27b))@(ap@(ap@(c_2Epair_2E_2C@A_27b@A_27b)@(ap@V2f@V3x))@(ap@V2f@V4y)))@(ap@(c_2Eset__relation_2Estrict@A_27b)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27b)@V1w2)))))))))))))))))))).
thf(conj_thm_2Ewellorder_2Eorderiso__REFL,lemma,( ! [A_27a:del]: ( ! [V0w:$i] : ((mem@V0w@(ty_2Ewellorder_2Ewellorder@A_27a)) => (p@(ap@(ap@(c_2Ewellorder_2Eorderiso@A_27a@A_27a)@V0w)@V0w)))))).
thf(conj_thm_2Ewellorder_2Eorderiso__SYM,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0w1:$i] : ((mem@V0w1@(ty_2Ewellorder_2Ewellorder@A_27a)) => ( ! [V1w2:$i] : ((mem@V1w2@(ty_2Ewellorder_2Ewellorder@A_27b)) => ((p@(ap@(ap@(c_2Ewellorder_2Eorderiso@A_27a@A_27b)@V0w1)@V1w2)) => (p@(ap@(ap@(c_2Ewellorder_2Eorderiso@A_27b@A_27a)@V1w2)@V0w1)))))))))).
thf(conj_thm_2Ewellorder_2Eorderiso__TRANS,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0w1:$i] : ((mem@V0w1@(ty_2Ewellorder_2Ewellorder@A_27a)) => ( ! [V1w2:$i] : ((mem@V1w2@(ty_2Ewellorder_2Ewellorder@A_27b)) => ( ! [V2w3:$i] : ((mem@V2w3@(ty_2Ewellorder_2Ewellorder@A_27c)) => (((p@(ap@(ap@(c_2Ewellorder_2Eorderiso@A_27a@A_27b)@V0w1)@V1w2)) & (p@(ap@(ap@(c_2Ewellorder_2Eorderiso@A_27b@A_27c)@V1w2)@V2w3))) => (p@(ap@(ap@(c_2Ewellorder_2Eorderiso@A_27a@A_27c)@V0w1)@V2w3))))))))))))).
thf(ax_thm_2Ewellorder_2Eorderlt__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0w1:$i] : ((mem@V0w1@(ty_2Ewellorder_2Ewellorder@A_27a)) => ( ! [V1w2:$i] : ((mem@V1w2@(ty_2Ewellorder_2Ewellorder@A_27b)) => ((p@(ap@(ap@(c_2Ewellorder_2Eorderlt@A_27a@A_27b)@V0w1)@V1w2)) <=> (? [V2x:$i] : ((mem@V2x@A_27b) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V2x)@(ap@(c_2Ewellorder_2EelsOf@A_27b)@V1w2))) & (p@(ap@(ap@(c_2Ewellorder_2Eorderiso@A_27a@A_27b)@V0w1)@(ap@(ap@(c_2Ewellorder_2Ewobound@A_27b)@V2x)@V1w2)))))))))))))).
thf(conj_thm_2Ewellorder_2Eorderlt__REFL,lemma,( ! [A_27a:del]: ( ! [V0w:$i] : ((mem@V0w@(ty_2Ewellorder_2Ewellorder@A_27a)) => ((p@(ap@(ap@(c_2Ewellorder_2Eorderlt@A_27a@A_27a)@V0w)@V0w)) <=> $false))))).
thf(conj_thm_2Ewellorder_2Ewobounds__preserve__bijections,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1w1:$i] : ((mem@V1w1@(ty_2Ewellorder_2Ewellorder@A_27a)) => ( ! [V2w2:$i] : ((mem@V2w2@(ty_2Ewellorder_2Ewellorder@A_27b)) => ( ! [V3x:$i] : ((mem@V3x@A_27a) => (((p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27b)@V0f)@(ap@(c_2Ewellorder_2EelsOf@A_27a)@V1w1))@(ap@(c_2Ewellorder_2EelsOf@A_27b)@V2w2))) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@(ap@(c_2Ewellorder_2EelsOf@A_27a)@V1w1))) & ( ! [V4x:$i] : ((mem@V4x@A_27a) => ( ! [V5y:$i] : ((mem@V5y@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V4x)@V5y))@(ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V1w1)))) => (p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27b@A_27b))@(ap@(ap@(c_2Epair_2E_2C@A_27b@A_27b)@(ap@V0f@V4x))@(ap@V0f@V5y)))@(ap@(c_2Eset__relation_2Estrict@A_27b)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27b)@V2w2))))))))))) => (p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27b)@V0f)@(ap@(c_2Ewellorder_2EelsOf@A_27a)@(ap@(ap@(c_2Ewellorder_2Ewobound@A_27a)@V3x)@V1w1)))@(ap@(c_2Ewellorder_2EelsOf@A_27b)@(ap@(ap@(c_2Ewellorder_2Ewobound@A_27b)@(ap@V0f@V3x))@V2w2)))))))))))))))).
thf(conj_thm_2Ewellorder_2Eorderlt__TRANS,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0w1:$i] : ((mem@V0w1@(ty_2Ewellorder_2Ewellorder@A_27a)) => ( ! [V1w2:$i] : ((mem@V1w2@(ty_2Ewellorder_2Ewellorder@A_27b)) => ( ! [V2w3:$i] : ((mem@V2w3@(ty_2Ewellorder_2Ewellorder@A_27c)) => (((p@(ap@(ap@(c_2Ewellorder_2Eorderlt@A_27a@A_27b)@V0w1)@V1w2)) & (p@(ap@(ap@(c_2Ewellorder_2Eorderlt@A_27b@A_27c)@V1w2)@V2w3))) => (p@(ap@(ap@(c_2Ewellorder_2Eorderlt@A_27a@A_27c)@V0w1)@V2w3))))))))))))).
thf(ax_thm_2Ewellorder_2Ewleast__def,axiom,( ! [A_27a:del]: ( ! [V0w:$i] : ((mem@V0w@(ty_2Ewellorder_2Ewellorder@A_27a)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ((ap@(ap@(c_2Ewellorder_2Ewleast@A_27a)@V0w)@V1s) = (ap@(c_2Eoption_2Esome@A_27a)@(lam@A_27a@(^ [V2x:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(c_2Ewellorder_2EelsOf@A_27a)@V0w)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V1s)))@(ap@(c_2Ebool_2E_21@A_27a)@(lam@A_27a@(^ [V3y:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3y)@(ap@(c_2Ewellorder_2EelsOf@A_27a)@V0w)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3y)@V1s)))@(ap@c_2Ebool_2E_7E@(ap@(ap@(c_2Emin_2E_3D@A_27a)@V2x)@V3y)))))@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V2x)@V3y))@(ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V0w))))))))))))))))))).
thf(ax_thm_2Ewellorder_2Ewo2wo__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0w1:$i] : ((mem@V0w1@(ty_2Ewellorder_2Ewellorder@A_27a)) => ( ! [V1w2:$i] : ((mem@V1w2@(ty_2Ewellorder_2Ewellorder@A_27b)) => ((ap@(ap@(c_2Ewellorder_2Ewo2wo@A_27a@A_27b)@V0w1)@V1w2) = (ap@(ap@(c_2Erelation_2EWFREC@A_27a@(ty_2Eoption_2Eoption@A_27b))@(lam@A_27a@(^ [V2x:$i] : (lam@A_27a@(^ [V3y:$i] : (ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V2x)@V3y))@(ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V0w1))))))))@(lam@(arr@A_27a@(ty_2Eoption_2Eoption@A_27b))@(^ [V4f:$i] : (lam@A_27a@(^ [V5x:$i] : (ap@(ap@(c_2Ebool_2ELET@(arr@(ty_2Eoption_2Eoption@A_27b)@bool)@(ty_2Eoption_2Eoption@A_27b))@(lam@(arr@(ty_2Eoption_2Eoption@A_27b)@bool)@(^ [V6s0:$i] : (ap@(ap@(c_2Ebool_2ELET@(arr@A_27b@bool)@(ty_2Eoption_2Eoption@A_27b))@(lam@(arr@A_27b@bool)@(^ [V7s1:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@A_27b))@(ap@(ap@(c_2Emin_2E_3D@(arr@A_27b@bool))@V7s1)@(ap@(c_2Ewellorder_2EelsOf@A_27b)@V1w2)))@(c_2Eoption_2ENONE@A_27b))@(ap@(ap@(c_2Ewellorder_2Ewleast@A_27b)@V1w2)@V7s1)))))@(ap@(ap@(c_2Epred__set_2EIMAGE@(ty_2Eoption_2Eoption@A_27b)@A_27b)@(c_2Eoption_2ETHE@A_27b))@(ap@(ap@(c_2Epred__set_2EDELETE@(ty_2Eoption_2Eoption@A_27b))@V6s0)@(c_2Eoption_2ENONE@A_27b)))))))@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@(ty_2Eoption_2Eoption@A_27b))@V4f)@(ap@(ap@(c_2Ewellorder_2Eiseg@A_27a)@V0w1)@V5x)))))))))))))))).
thf(conj_thm_2Ewellorder_2Ewo2wo__thm,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0w:$i] : ((mem@V0w@(ty_2Ewellorder_2Ewellorder@A_27a)) => ( ! [V1w2:$i] : ((mem@V1w2@(ty_2Ewellorder_2Ewellorder@A_27b)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ((ap@(ap@(ap@(c_2Ewellorder_2Ewo2wo@A_27a@A_27b)@V0w)@V1w2)@V2x) = (ap@(ap@(c_2Ebool_2ELET@(arr@(ty_2Eoption_2Eoption@A_27b)@bool)@(ty_2Eoption_2Eoption@A_27b))@(lam@(arr@(ty_2Eoption_2Eoption@A_27b)@bool)@(^ [V3s0:$i] : (ap@(ap@(c_2Ebool_2ELET@(arr@A_27b@bool)@(ty_2Eoption_2Eoption@A_27b))@(lam@(arr@A_27b@bool)@(^ [V4s1:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@A_27b))@(ap@(ap@(c_2Emin_2E_3D@(arr@A_27b@bool))@V4s1)@(ap@(c_2Ewellorder_2EelsOf@A_27b)@V1w2)))@(c_2Eoption_2ENONE@A_27b))@(ap@(ap@(c_2Ewellorder_2Ewleast@A_27b)@V1w2)@V4s1)))))@(ap@(ap@(c_2Epred__set_2EIMAGE@(ty_2Eoption_2Eoption@A_27b)@A_27b)@(c_2Eoption_2ETHE@A_27b))@(ap@(ap@(c_2Epred__set_2EDELETE@(ty_2Eoption_2Eoption@A_27b))@V3s0)@(c_2Eoption_2ENONE@A_27b)))))))@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@(ty_2Eoption_2Eoption@A_27b))@(ap@(ap@(c_2Ewellorder_2Ewo2wo@A_27a@A_27b)@V0w)@V1w2))@(ap@(ap@(c_2Ewellorder_2Eiseg@A_27a)@V0w)@V2x))))))))))))).
thf(conj_thm_2Ewellorder_2Ewleast__IN__wo,lemma,( ! [A_27a:del]: ( ! [V0w:$i] : ((mem@V0w@(ty_2Ewellorder_2Ewellorder@A_27a)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => (((ap@(ap@(c_2Ewellorder_2Ewleast@A_27a)@V0w)@V1s) = (ap@(c_2Eoption_2ESOME@A_27a)@V2x)) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(c_2Ewellorder_2EelsOf@A_27a)@V0w))) & ((~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V1s))) & ( ! [V3y:$i] : ((mem@V3y@A_27a) => (((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3y)@(ap@(c_2Ewellorder_2EelsOf@A_27a)@V0w))) & ((~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3y)@V1s))) & (~~ (V2x = V3y)))) => (p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V2x)@V3y))@(ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V0w)))))))))))))))))).
thf(conj_thm_2Ewellorder_2Ewleast__EQ__NONE,lemma,( ! [A_27a:del]: ( ! [V0w:$i] : ((mem@V0w@(ty_2Ewellorder_2Ewellorder@A_27a)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => (((ap@(ap@(c_2Ewellorder_2Ewleast@A_27a)@V0w)@V1s) = (c_2Eoption_2ENONE@A_27a)) => (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@(ap@(c_2Ewellorder_2EelsOf@A_27a)@V0w))@V1s))))))))).
thf(conj_thm_2Ewellorder_2Ewo2wo__IN__w2,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0w1:$i] : ((mem@V0w1@(ty_2Ewellorder_2Ewellorder@A_27a)) => ( ! [V1w2:$i] : ((mem@V1w2@(ty_2Ewellorder_2Ewellorder@A_27b)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ( ! [V3y:$i] : ((mem@V3y@A_27b) => (((ap@(ap@(ap@(c_2Ewellorder_2Ewo2wo@A_27a@A_27b)@V0w1)@V1w2)@V2x) = (ap@(c_2Eoption_2ESOME@A_27b)@V3y)) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V3y)@(ap@(c_2Ewellorder_2EelsOf@A_27b)@V1w2))))))))))))))).
thf(conj_thm_2Ewellorder_2EIMAGE__wo2wo__SUBSET,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0w1:$i] : ((mem@V0w1@(ty_2Ewellorder_2Ewellorder@A_27b)) => ( ! [V1w2:$i] : ((mem@V1w2@(ty_2Ewellorder_2Ewellorder@A_27a)) => ( ! [V2x:$i] : ((mem@V2x@A_27b) => (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@(ap@(ap@(c_2Epred__set_2EIMAGE@(ty_2Eoption_2Eoption@A_27a)@A_27a)@(c_2Eoption_2ETHE@A_27a))@(ap@(ap@(c_2Epred__set_2EDELETE@(ty_2Eoption_2Eoption@A_27a))@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27b@(ty_2Eoption_2Eoption@A_27a))@(ap@(ap@(c_2Ewellorder_2Ewo2wo@A_27b@A_27a)@V0w1)@V1w2))@(ap@(ap@(c_2Ewellorder_2Eiseg@A_27b)@V0w1)@V2x)))@(c_2Eoption_2ENONE@A_27a))))@(ap@(c_2Ewellorder_2EelsOf@A_27a)@V1w2)))))))))))).
thf(conj_thm_2Ewellorder_2Ewo2wo__EQ__NONE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0w1:$i] : ((mem@V0w1@(ty_2Ewellorder_2Ewellorder@A_27a)) => ( ! [V1w2:$i] : ((mem@V1w2@(ty_2Ewellorder_2Ewellorder@A_27b)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => (((ap@(ap@(ap@(c_2Ewellorder_2Ewo2wo@A_27a@A_27b)@V0w1)@V1w2)@V2x) = (c_2Eoption_2ENONE@A_27b)) => ( ! [V3y:$i] : ((mem@V3y@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V2x)@V3y))@(ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V0w1)))) => ((ap@(ap@(ap@(c_2Ewellorder_2Ewo2wo@A_27a@A_27b)@V0w1)@V1w2)@V3y) = (c_2Eoption_2ENONE@A_27b))))))))))))))).
thf(conj_thm_2Ewellorder_2Ewo2wo__EQ__SOME__downwards,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0w1:$i] : ((mem@V0w1@(ty_2Ewellorder_2Ewellorder@A_27a)) => ( ! [V1w2:$i] : ((mem@V1w2@(ty_2Ewellorder_2Ewellorder@A_27b)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ( ! [V3y:$i] : ((mem@V3y@A_27b) => (((ap@(ap@(ap@(c_2Ewellorder_2Ewo2wo@A_27a@A_27b)@V0w1)@V1w2)@V2x) = (ap@(c_2Eoption_2ESOME@A_27b)@V3y)) => ( ! [V4x0:$i] : ((mem@V4x0@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V4x0)@V2x))@(ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V0w1)))) => (? [V5y0:$i] : ((mem@V5y0@A_27b) & ((ap@(ap@(ap@(c_2Ewellorder_2Ewo2wo@A_27a@A_27b)@V0w1)@V1w2)@V4x0) = (ap@(c_2Eoption_2ESOME@A_27b)@V5y0))))))))))))))))))).
thf(conj_thm_2Ewellorder_2Emono__woseg,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x1:$i] : ((mem@V0x1@A_27a) => ( ! [V1x2:$i] : ((mem@V1x2@A_27a) => ( ! [V2w1:$i] : ((mem@V2w1@(ty_2Ewellorder_2Ewellorder@A_27a)) => ( ! [V3w2:$i] : ((mem@V3w2@(ty_2Ewellorder_2Ewellorder@A_27b)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V0x1)@V1x2))@(ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V2w1)))) => (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27b)@(ap@(ap@(c_2Epred__set_2EIMAGE@(ty_2Eoption_2Eoption@A_27b)@A_27b)@(c_2Eoption_2ETHE@A_27b))@(ap@(ap@(c_2Epred__set_2EDELETE@(ty_2Eoption_2Eoption@A_27b))@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@(ty_2Eoption_2Eoption@A_27b))@(ap@(ap@(c_2Ewellorder_2Ewo2wo@A_27a@A_27b)@V2w1)@V3w2))@(ap@(ap@(c_2Ewellorder_2Eiseg@A_27a)@V2w1)@V0x1)))@(c_2Eoption_2ENONE@A_27b))))@(ap@(ap@(c_2Epred__set_2EIMAGE@(ty_2Eoption_2Eoption@A_27b)@A_27b)@(c_2Eoption_2ETHE@A_27b))@(ap@(ap@(c_2Epred__set_2EDELETE@(ty_2Eoption_2Eoption@A_27b))@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@(ty_2Eoption_2Eoption@A_27b))@(ap@(ap@(c_2Ewellorder_2Ewo2wo@A_27a@A_27b)@V2w1)@V3w2))@(ap@(ap@(c_2Ewellorder_2Eiseg@A_27a)@V2w1)@V1x2)))@(c_2Eoption_2ENONE@A_27b))))))))))))))))).
thf(conj_thm_2Ewellorder_2Ewo2wo__11,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x1:$i] : ((mem@V0x1@A_27a) => ( ! [V1w1:$i] : ((mem@V1w1@(ty_2Ewellorder_2Ewellorder@A_27a)) => ( ! [V2x2:$i] : ((mem@V2x2@A_27a) => ( ! [V3w2:$i] : ((mem@V3w2@(ty_2Ewellorder_2Ewellorder@A_27b)) => ( ! [V4y:$i] : ((mem@V4y@A_27b) => (((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x1)@(ap@(c_2Ewellorder_2EelsOf@A_27a)@V1w1))) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x2)@(ap@(c_2Ewellorder_2EelsOf@A_27a)@V1w1))) & (((ap@(ap@(ap@(c_2Ewellorder_2Ewo2wo@A_27a@A_27b)@V1w1)@V3w2)@V0x1) = (ap@(c_2Eoption_2ESOME@A_27b)@V4y)) & ((ap@(ap@(ap@(c_2Ewellorder_2Ewo2wo@A_27a@A_27b)@V1w1)@V3w2)@V2x2) = (ap@(c_2Eoption_2ESOME@A_27b)@V4y))))) => (V0x1 = V2x2))))))))))))))).
thf(conj_thm_2Ewellorder_2Ewleast__SUBSET,lemma,( ! [A_27a:del]: ( ! [V0w:$i] : ((mem@V0w@(ty_2Ewellorder_2Ewellorder@A_27a)) => ( ! [V1s1:$i] : ((mem@V1s1@(arr@A_27a@bool)) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => ( ! [V3s2:$i] : ((mem@V3s2@(arr@A_27a@bool)) => ( ! [V4y:$i] : ((mem@V4y@A_27a) => ((((ap@(ap@(c_2Ewellorder_2Ewleast@A_27a)@V0w)@V1s1) = (ap@(c_2Eoption_2ESOME@A_27a)@V2x)) & (((ap@(ap@(c_2Ewellorder_2Ewleast@A_27a)@V0w)@V3s2) = (ap@(c_2Eoption_2ESOME@A_27a)@V4y)) & (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V1s1)@V3s2)))) => ((V2x = V4y) | (p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V2x)@V4y))@(ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V0w)))))))))))))))))).
thf(conj_thm_2Ewellorder_2Ewo2wo__mono,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0w1:$i] : ((mem@V0w1@(ty_2Ewellorder_2Ewellorder@A_27b)) => ( ! [V1w2:$i] : ((mem@V1w2@(ty_2Ewellorder_2Ewellorder@A_27a)) => ( ! [V2x0:$i] : ((mem@V2x0@A_27b) => ( ! [V3y0:$i] : ((mem@V3y0@A_27a) => ( ! [V4x:$i] : ((mem@V4x@A_27b) => ( ! [V5y:$i] : ((mem@V5y@A_27a) => ((((ap@(ap@(ap@(c_2Ewellorder_2Ewo2wo@A_27b@A_27a)@V0w1)@V1w2)@V2x0) = (ap@(c_2Eoption_2ESOME@A_27a)@V3y0)) & (((ap@(ap@(ap@(c_2Ewellorder_2Ewo2wo@A_27b@A_27a)@V0w1)@V1w2)@V4x) = (ap@(c_2Eoption_2ESOME@A_27a)@V5y)) & (p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27b@A_27b))@(ap@(ap@(c_2Epair_2E_2C@A_27b@A_27b)@V2x0)@V4x))@(ap@(c_2Eset__relation_2Estrict@A_27b)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27b)@V0w1)))))) => (p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V3y0)@V5y))@(ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V1w2)))))))))))))))))))).
thf(conj_thm_2Ewellorder_2Ewo2wo__ONTO,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1w1:$i] : ((mem@V1w1@(ty_2Ewellorder_2Ewellorder@A_27a)) => ( ! [V2w2:$i] : ((mem@V2w2@(ty_2Ewellorder_2Ewellorder@A_27b)) => ( ! [V3y:$i] : ((mem@V3y@A_27b) => ( ! [V4y0:$i] : ((mem@V4y0@A_27b) => (((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@(ap@(c_2Ewellorder_2EelsOf@A_27a)@V1w1))) & (((ap@(ap@(ap@(c_2Ewellorder_2Ewo2wo@A_27a@A_27b)@V1w1)@V2w2)@V0x) = (ap@(c_2Eoption_2ESOME@A_27b)@V3y)) & (p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27b@A_27b))@(ap@(ap@(c_2Epair_2E_2C@A_27b@A_27b)@V4y0)@V3y))@(ap@(c_2Eset__relation_2Estrict@A_27b)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27b)@V2w2)))))) => (? [V5x0:$i] : ((mem@V5x0@A_27a) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V5x0)@(ap@(c_2Ewellorder_2EelsOf@A_27a)@V1w1))) & ((ap@(ap@(ap@(c_2Ewellorder_2Ewo2wo@A_27a@A_27b)@V1w1)@V2w2)@V5x0) = (ap@(c_2Eoption_2ESOME@A_27b)@V4y0))))))))))))))))))).
thf(conj_thm_2Ewellorder_2Ewo2wo__EQ__NONE__woseg,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0w1:$i] : ((mem@V0w1@(ty_2Ewellorder_2Ewellorder@A_27b)) => ( ! [V1w2:$i] : ((mem@V1w2@(ty_2Ewellorder_2Ewellorder@A_27a)) => ( ! [V2x:$i] : ((mem@V2x@A_27b) => (((ap@(ap@(ap@(c_2Ewellorder_2Ewo2wo@A_27b@A_27a)@V0w1)@V1w2)@V2x) = (c_2Eoption_2ENONE@A_27a)) => ((ap@(c_2Ewellorder_2EelsOf@A_27a)@V1w2) = (ap@(ap@(c_2Epred__set_2EIMAGE@(ty_2Eoption_2Eoption@A_27a)@A_27a)@(c_2Eoption_2ETHE@A_27a))@(ap@(ap@(c_2Epred__set_2EDELETE@(ty_2Eoption_2Eoption@A_27a))@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27b@(ty_2Eoption_2Eoption@A_27a))@(ap@(ap@(c_2Ewellorder_2Ewo2wo@A_27b@A_27a)@V0w1)@V1w2))@(ap@(ap@(c_2Ewellorder_2Eiseg@A_27b)@V0w1)@V2x)))@(c_2Eoption_2ENONE@A_27a)))))))))))))).
thf(conj_thm_2Ewellorder_2Eorderlt__trichotomy,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0w1:$i] : ((mem@V0w1@(ty_2Ewellorder_2Ewellorder@A_27a)) => ( ! [V1w2:$i] : ((mem@V1w2@(ty_2Ewellorder_2Ewellorder@A_27b)) => ((p@(ap@(ap@(c_2Ewellorder_2Eorderlt@A_27a@A_27b)@V0w1)@V1w2)) | ((p@(ap@(ap@(c_2Ewellorder_2Eorderiso@A_27a@A_27b)@V0w1)@V1w2)) | (p@(ap@(ap@(c_2Ewellorder_2Eorderlt@A_27b@A_27a)@V1w2)@V0w1))))))))))).
thf(ax_thm_2Ewellorder_2EwZERO__def,axiom,( ! [A_27a:del]: ((c_2Ewellorder_2EwZERO@A_27a) = (ap@(c_2Ewellorder_2Ewellorder__ABS@A_27a)@(c_2Epred__set_2EEMPTY@(ty_2Epair_2Eprod@A_27a@A_27a)))))).
thf(conj_thm_2Ewellorder_2EelsOf__wZERO,lemma,( ! [A_27a:del]: ((ap@(c_2Ewellorder_2EelsOf@A_27a)@(c_2Ewellorder_2EwZERO@A_27a)) = (c_2Epred__set_2EEMPTY@A_27a)))).
thf(conj_thm_2Ewellorder_2EWIN__wZERO,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1y:$i] : ((mem@V1y@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V0x)@V1y))@(ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@(c_2Ewellorder_2EwZERO@A_27a))))) <=> $false))))))).
thf(conj_thm_2Ewellorder_2EWLE__wZERO,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1y:$i] : ((mem@V1y@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V0x)@V1y))@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@(c_2Ewellorder_2EwZERO@A_27a)))) <=> $false))))))).
thf(conj_thm_2Ewellorder_2Eorderiso__wZERO,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0w:$i] : ((mem@V0w@(ty_2Ewellorder_2Ewellorder@A_27b)) => ((p@(ap@(ap@(c_2Ewellorder_2Eorderiso@A_27a@A_27b)@(c_2Ewellorder_2EwZERO@A_27a))@V0w)) <=> (V0w = (c_2Ewellorder_2EwZERO@A_27b)))))))).
thf(conj_thm_2Ewellorder_2EelsOf__EQ__EMPTY,lemma,( ! [A_27a:del]: ( ! [V0w:$i] : ((mem@V0w@(ty_2Ewellorder_2Ewellorder@A_27a)) => (((ap@(c_2Ewellorder_2EelsOf@A_27a)@V0w) = (c_2Epred__set_2EEMPTY@A_27a)) <=> (V0w = (c_2Ewellorder_2EwZERO@A_27a))))))).
thf(conj_thm_2Ewellorder_2ELT__wZERO,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0w:$i] : ((mem@V0w@(ty_2Ewellorder_2Ewellorder@A_27a)) => ((p@(ap@(ap@(c_2Ewellorder_2Eorderlt@A_27a@A_27b)@V0w)@(c_2Ewellorder_2EwZERO@A_27b))) <=> $false)))))).
thf(conj_thm_2Ewellorder_2Eorderlt__WF,lemma,( ! [A_27a:del]: (p@(ap@(c_2Erelation_2EWF@(ty_2Ewellorder_2Ewellorder@A_27a))@(c_2Ewellorder_2Eorderlt@A_27a@A_27a))))).
thf(conj_thm_2Ewellorder_2Eorderlt__orderiso,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [V0x0:$i] : ((mem@V0x0@(ty_2Ewellorder_2Ewellorder@A_27a)) => ( ! [V1y0:$i] : ((mem@V1y0@(ty_2Ewellorder_2Ewellorder@A_27b)) => ( ! [V2a0:$i] : ((mem@V2a0@(ty_2Ewellorder_2Ewellorder@A_27c)) => ( ! [V3b0:$i] : ((mem@V3b0@(ty_2Ewellorder_2Ewellorder@A_27d)) => (((p@(ap@(ap@(c_2Ewellorder_2Eorderiso@A_27a@A_27b)@V0x0)@V1y0)) & (p@(ap@(ap@(c_2Ewellorder_2Eorderiso@A_27c@A_27d)@V2a0)@V3b0))) => ((p@(ap@(ap@(c_2Ewellorder_2Eorderlt@A_27a@A_27c)@V0x0)@V2a0)) <=> (p@(ap@(ap@(c_2Ewellorder_2Eorderlt@A_27b@A_27d)@V1y0)@V3b0))))))))))))))))).
thf(ax_thm_2Ewellorder_2Efinite__def,axiom,( ! [A_27a:del]: ( ! [V0w:$i] : ((mem@V0w@(ty_2Ewellorder_2Ewellorder@A_27a)) => ((p@(ap@(c_2Ewellorder_2Efinite@A_27a)@V0w)) <=> (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@(ap@(c_2Ewellorder_2EelsOf@A_27a)@V0w)))))))).
thf(conj_thm_2Ewellorder_2Efinite__iso,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0w1:$i] : ((mem@V0w1@(ty_2Ewellorder_2Ewellorder@A_27a)) => ( ! [V1w2:$i] : ((mem@V1w2@(ty_2Ewellorder_2Ewellorder@A_27b)) => ((p@(ap@(ap@(c_2Ewellorder_2Eorderiso@A_27a@A_27b)@V0w1)@V1w2)) => ((p@(ap@(c_2Ewellorder_2Efinite@A_27a)@V0w1)) <=> (p@(ap@(c_2Ewellorder_2Efinite@A_27b)@V1w2))))))))))).
thf(conj_thm_2Ewellorder_2Efinite__wZERO,lemma,( ! [A_27a:del]: (p@(ap@(c_2Ewellorder_2Efinite@A_27a)@(c_2Ewellorder_2EwZERO@A_27a))))).
thf(conj_thm_2Ewellorder_2Eorderiso__unique,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f1:$i] : ((mem@V0f1@(arr@A_27a@A_27b)) => ( ! [V1w1:$i] : ((mem@V1w1@(ty_2Ewellorder_2Ewellorder@A_27a)) => ( ! [V2w2:$i] : ((mem@V2w2@(ty_2Ewellorder_2Ewellorder@A_27b)) => ( ! [V3f2:$i] : ((mem@V3f2@(arr@A_27a@A_27b)) => (((p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27b)@V0f1)@(ap@(c_2Ewellorder_2EelsOf@A_27a)@V1w1))@(ap@(c_2Ewellorder_2EelsOf@A_27b)@V2w2))) & ((p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27b)@V3f2)@(ap@(c_2Ewellorder_2EelsOf@A_27a)@V1w1))@(ap@(c_2Ewellorder_2EelsOf@A_27b)@V2w2))) & (( ! [V4x:$i] : ((mem@V4x@A_27a) => ( ! [V5y:$i] : ((mem@V5y@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V4x)@V5y))@(ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V1w1)))) => (p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27b@A_27b))@(ap@(ap@(c_2Epair_2E_2C@A_27b@A_27b)@(ap@V0f1@V4x))@(ap@V0f1@V5y)))@(ap@(c_2Eset__relation_2Estrict@A_27b)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27b)@V2w2))))))))) & ( ! [V6x:$i] : ((mem@V6x@A_27a) => ( ! [V7y:$i] : ((mem@V7y@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V6x)@V7y))@(ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V1w1)))) => (p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27b@A_27b))@(ap@(ap@(c_2Epair_2E_2C@A_27b@A_27b)@(ap@V3f2@V6x))@(ap@V3f2@V7y)))@(ap@(c_2Eset__relation_2Estrict@A_27b)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27b)@V2w2)))))))))))) => ( ! [V8x:$i] : ((mem@V8x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V8x)@(ap@(c_2Ewellorder_2EelsOf@A_27a)@V1w1))) => ((ap@V0f1@V8x) = (ap@V3f2@V8x))))))))))))))))).
thf(conj_thm_2Ewellorder_2Eseteq__wlog,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@(arr@A_27a@bool))) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27a@(arr@A_27b@bool))) => ((( ! [V2a:$i] : ((mem@V2a@A_27a) => ( ! [V3b:$i] : ((mem@V3b@A_27a) => ((p@(ap@(ap@V0P@V2a)@V3b)) => (p@(ap@(ap@V0P@V3b)@V2a))))))) & ( ! [V4x:$i] : ((mem@V4x@A_27b) => ( ! [V5a:$i] : ((mem@V5a@A_27a) => ( ! [V6b:$i] : ((mem@V6b@A_27a) => (((p@(ap@(ap@V0P@V5a)@V6b)) & (p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V4x)@(ap@V1f@V5a)))) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V4x)@(ap@V1f@V6b))))))))))) => ( ! [V7a:$i] : ((mem@V7a@A_27a) => ( ! [V8b:$i] : ((mem@V8b@A_27a) => ((p@(ap@(ap@V0P@V7a)@V8b)) => ((ap@V1f@V7a) = (ap@V1f@V8b))))))))))))))).
thf(conj_thm_2Ewellorder_2Ewo__INDUCTION,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1w:$i] : ((mem@V1w@(ty_2Ewellorder_2Ewellorder@A_27a)) => (( ! [V2x:$i] : ((mem@V2x@A_27a) => (( ! [V3y:$i] : ((mem@V3y@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V3y)@V2x))@(ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V1w)))) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3y)@(ap@(c_2Ewellorder_2EelsOf@A_27a)@V1w))) => (p@(ap@V0P@V3y)))))) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(c_2Ewellorder_2EelsOf@A_27a)@V1w))) => (p@(ap@V0P@V2x)))))) => ( ! [V4x:$i] : ((mem@V4x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V4x)@(ap@(c_2Ewellorder_2EelsOf@A_27a)@V1w))) => (p@(ap@V0P@V4x)))))))))))).
thf(conj_thm_2Ewellorder_2EFORALL__NUM,lemma,( ! [V0P:$i] : ((mem@V0P@(arr@ty_2Enum_2Enum@bool)) => (( ! [V1n:tp__ty_2Enum_2Enum] : (p@(ap@V0P@(inj__ty_2Enum_2Enum @ V1n)))) <=> ((p@(ap@V0P@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) & ( ! [V2n:tp__ty_2Enum_2Enum] : (p@(ap@V0P@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V2n)))))))))).
thf(conj_thm_2Ewellorder_2Estrict__UNION,lemma,( ! [A_27a:del]: ( ! [V0r1:$i] : ((mem@V0r1@(arr@(ty_2Epair_2Eprod@A_27a@A_27a)@bool)) => ( ! [V1r2:$i] : ((mem@V1r2@(arr@(ty_2Epair_2Eprod@A_27a@A_27a)@bool)) => ((ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(ap@(c_2Epred__set_2EUNION@(ty_2Epair_2Eprod@A_27a@A_27a))@V0r1)@V1r2)) = (ap@(ap@(c_2Epred__set_2EUNION@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(c_2Eset__relation_2Estrict@A_27a)@V0r1))@(ap@(c_2Eset__relation_2Estrict@A_27a)@V1r2))))))))).
thf(conj_thm_2Ewellorder_2EWLE__WIN__EQ,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1y:$i] : ((mem@V1y@A_27a) => ( ! [V2w:$i] : ((mem@V2w@(ty_2Ewellorder_2Ewellorder@A_27a)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V0x)@V1y))@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V2w))) <=> (((V0x = V1y) & (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@(ap@(c_2Ewellorder_2EelsOf@A_27a)@V2w)))) | (p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V0x)@V1y))@(ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V2w)))))))))))))).
thf(ax_thm_2Ewellorder_2Eremove__def,axiom,( ! [A_27a:del]: ( ! [V0e:$i] : ((mem@V0e@A_27a) => ( ! [V1w:$i] : ((mem@V1w@(ty_2Ewellorder_2Ewellorder@A_27a)) => ((ap@(ap@(c_2Ewellorder_2Eremove@A_27a)@V0e)@V1w) = (ap@(c_2Ewellorder_2Ewellorder__ABS@A_27a)@(ap@(c_2Epred__set_2EGSPEC@(ty_2Epair_2Eprod@A_27a@A_27a)@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(c_2Epair_2EUNCURRY@A_27a@A_27a@(ty_2Epair_2Eprod@(ty_2Epair_2Eprod@A_27a@A_27a)@bool))@(lam@A_27a@(^ [V2x:$i] : (lam@A_27a@(^ [V3y:$i] : (ap@(ap@(c_2Epair_2E_2C@(ty_2Epair_2Eprod@A_27a@A_27a)@bool)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V2x)@V3y))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@(ap@(c_2Emin_2E_3D@A_27a)@V2x)@V0e)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@(ap@(c_2Emin_2E_3D@A_27a)@V3y)@V0e)))@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V2x)@V3y))@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V1w))))))))))))))))))).
thf(conj_thm_2Ewellorder_2Ewellorder__remove,lemma,( ! [A_27a:del]: ( ! [V0e:$i] : ((mem@V0e@A_27a) => ( ! [V1w:$i] : ((mem@V1w@(ty_2Ewellorder_2Ewellorder@A_27a)) => (p@(ap@(c_2Ewellorder_2Ewellorder@A_27a)@(ap@(c_2Epred__set_2EGSPEC@(ty_2Epair_2Eprod@A_27a@A_27a)@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(c_2Epair_2EUNCURRY@A_27a@A_27a@(ty_2Epair_2Eprod@(ty_2Epair_2Eprod@A_27a@A_27a)@bool))@(lam@A_27a@(^ [V2x:$i] : (lam@A_27a@(^ [V3y:$i] : (ap@(ap@(c_2Epair_2E_2C@(ty_2Epair_2Eprod@A_27a@A_27a)@bool)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V2x)@V3y))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@(ap@(c_2Emin_2E_3D@A_27a)@V2x)@V0e)))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@c_2Ebool_2E_7E@(ap@(ap@(c_2Emin_2E_3D@A_27a)@V3y)@V0e)))@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V2x)@V3y))@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V1w))))))))))))))))))).
thf(conj_thm_2Ewellorder_2EelsOf__remove,lemma,( ! [A_27a:del]: ( ! [V0e:$i] : ((mem@V0e@A_27a) => ( ! [V1w:$i] : ((mem@V1w@(ty_2Ewellorder_2Ewellorder@A_27a)) => ((ap@(c_2Ewellorder_2EelsOf@A_27a)@(ap@(ap@(c_2Ewellorder_2Eremove@A_27a)@V0e)@V1w)) = (ap@(ap@(c_2Epred__set_2EDELETE@A_27a)@(ap@(c_2Ewellorder_2EelsOf@A_27a)@V1w))@V0e)))))))).
thf(conj_thm_2Ewellorder_2EWIN__remove,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1y:$i] : ((mem@V1y@A_27a) => ( ! [V2e:$i] : ((mem@V2e@A_27a) => ( ! [V3w:$i] : ((mem@V3w@(ty_2Ewellorder_2Ewellorder@A_27a)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V0x)@V1y))@(ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@(ap@(ap@(c_2Ewellorder_2Eremove@A_27a)@V2e)@V3w))))) <=> ((~~ (V0x = V2e)) & ((~~ (V1y = V2e)) & (p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V0x)@V1y))@(ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V3w))))))))))))))))).
thf(ax_thm_2Ewellorder_2EADD1__def,axiom,( ! [A_27a:del]: ( ! [V0e:$i] : ((mem@V0e@A_27a) => ( ! [V1w:$i] : ((mem@V1w@(ty_2Ewellorder_2Ewellorder@A_27a)) => ((ap@(ap@(c_2Ewellorder_2EADD1@A_27a)@V0e)@V1w) = (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Ewellorder_2Ewellorder@A_27a))@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0e)@(ap@(c_2Ewellorder_2EelsOf@A_27a)@V1w)))@V1w)@(ap@(c_2Ewellorder_2Ewellorder__ABS@A_27a)@(ap@(ap@(c_2Epred__set_2EUNION@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epred__set_2EUNION@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V1w))@(ap@(c_2Epred__set_2EGSPEC@(ty_2Epair_2Eprod@A_27a@A_27a)@A_27a)@(lam@A_27a@(^ [V2x:$i] : (ap@(ap@(c_2Epair_2E_2C@(ty_2Epair_2Eprod@A_27a@A_27a)@bool)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V2x)@V0e))@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(c_2Ewellorder_2EelsOf@A_27a)@V1w))))))))@(ap@(ap@(c_2Epred__set_2EINSERT@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V0e)@V0e))@(c_2Epred__set_2EEMPTY@(ty_2Epair_2Eprod@A_27a@A_27a))))))))))))).
thf(conj_thm_2Ewellorder_2Ewellorder__ADD1,lemma,( ! [A_27a:del]: ( ! [V0e:$i] : ((mem@V0e@A_27a) => ( ! [V1w:$i] : ((mem@V1w@(ty_2Ewellorder_2Ewellorder@A_27a)) => ((~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0e)@(ap@(c_2Ewellorder_2EelsOf@A_27a)@V1w)))) => (p@(ap@(c_2Ewellorder_2Ewellorder@A_27a)@(ap@(ap@(c_2Epred__set_2EUNION@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epred__set_2EUNION@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V1w))@(ap@(c_2Epred__set_2EGSPEC@(ty_2Epair_2Eprod@A_27a@A_27a)@A_27a)@(lam@A_27a@(^ [V2x:$i] : (ap@(ap@(c_2Epair_2E_2C@(ty_2Epair_2Eprod@A_27a@A_27a)@bool)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V2x)@V0e))@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@(ap@(c_2Ewellorder_2EelsOf@A_27a)@V1w))))))))@(ap@(ap@(c_2Epred__set_2EINSERT@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V0e)@V0e))@(c_2Epred__set_2EEMPTY@(ty_2Epair_2Eprod@A_27a@A_27a))))))))))))).
thf(conj_thm_2Ewellorder_2EelsOf__ADD1,lemma,( ! [A_27a:del]: ( ! [V0e:$i] : ((mem@V0e@A_27a) => ( ! [V1w:$i] : ((mem@V1w@(ty_2Ewellorder_2Ewellorder@A_27a)) => ((ap@(c_2Ewellorder_2EelsOf@A_27a)@(ap@(ap@(c_2Ewellorder_2EADD1@A_27a)@V0e)@V1w)) = (ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0e)@(ap@(c_2Ewellorder_2EelsOf@A_27a)@V1w))))))))).
thf(conj_thm_2Ewellorder_2EWIN__ADD1,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1y:$i] : ((mem@V1y@A_27a) => ( ! [V2e:$i] : ((mem@V2e@A_27a) => ( ! [V3w:$i] : ((mem@V3w@(ty_2Ewellorder_2Ewellorder@A_27a)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V0x)@V1y))@(ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@(ap@(ap@(c_2Ewellorder_2EADD1@A_27a)@V2e)@V3w))))) <=> (((~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2e)@(ap@(c_2Ewellorder_2EelsOf@A_27a)@V3w)))) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@(ap@(c_2Ewellorder_2EelsOf@A_27a)@V3w))) & (V1y = V2e))) | (p@(ap@(ap@(c_2Ebool_2EIN@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V0x)@V1y))@(ap@(c_2Eset__relation_2Estrict@A_27a)@(ap@(c_2Ewellorder_2Ewellorder__REP@A_27a)@V3w)))))))))))))))).
thf(conj_thm_2Ewellorder_2EelsOf__cardeq__iso,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27b@A_27a)) => ( ! [V1wo:$i] : ((mem@V1wo@(ty_2Ewellorder_2Ewellorder@A_27b)) => ((p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27b@A_27a)@V0f)@(ap@(c_2Ewellorder_2EelsOf@A_27b)@V1wo))@(c_2Epred__set_2EUNIV@A_27a))) => (? [V2wo_27:$i] : ((mem@V2wo_27@(ty_2Ewellorder_2Ewellorder@A_27a)) & (p@(ap@(ap@(c_2Ewellorder_2Eorderiso@A_27b@A_27a)@V1wo)@V2wo_27)))))))))))).
thf(conj_thm_2Ewellorder_2Eallsets__wellorderable,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => (? [V1wo:$i] : ((mem@V1wo@(ty_2Ewellorder_2Ewellorder@A_27a)) & ((ap@(c_2Ewellorder_2EelsOf@A_27a)@V1wo) = V0s))))))).
thf(conj_thm_2Ewellorder_2EWF,lemma,( ! [A_27a:del]: ( ! [V0_3C_3C:$i] : ((mem@V0_3C_3C@(arr@A_27a@(arr@A_27a@bool))) => ((p@(ap@(c_2Erelation_2EWF@A_27a)@V0_3C_3C)) <=> ( ! [V1P:$i] : ((mem@V1P@(arr@A_27a@bool)) => ((? [V2x:$i] : ((mem@V2x@A_27a) & (p@(ap@V1P@V2x)))) => (? [V3x:$i] : ((mem@V3x@A_27a) & ((p@(ap@V1P@V3x)) & ( ! [V4y:$i] : ((mem@V4y@A_27a) => ((p@(ap@(ap@V0_3C_3C@V4y)@V3x)) => (~~ (p@(ap@V1P@V4y))))))))))))))))).
thf(conj_thm_2Ewellorder_2EWF__EQ,lemma,( ! [A_27a:del]: ( ! [V0_3C_3C:$i] : ((mem@V0_3C_3C@(arr@A_27a@(arr@A_27a@bool))) => ((p@(ap@(c_2Erelation_2EWF@A_27a)@V0_3C_3C)) <=> ( ! [V1P:$i] : ((mem@V1P@(arr@A_27a@bool)) => ((? [V2x:$i] : ((mem@V2x@A_27a) & (p@(ap@V1P@V2x)))) <=> (? [V3x:$i] : ((mem@V3x@A_27a) & ((p@(ap@V1P@V3x)) & ( ! [V4y:$i] : ((mem@V4y@A_27a) => ((p@(ap@(ap@V0_3C_3C@V4y)@V3x)) => (~~ (p@(ap@V1P@V4y))))))))))))))))).
thf(conj_thm_2Ewellorder_2EWF__IND,lemma,( ! [A_27a:del]: ( ! [V0_3C_3C:$i] : ((mem@V0_3C_3C@(arr@A_27a@(arr@A_27a@bool))) => ((p@(ap@(c_2Erelation_2EWF@A_27a)@V0_3C_3C)) <=> ( ! [V1P:$i] : ((mem@V1P@(arr@A_27a@bool)) => (( ! [V2x:$i] : ((mem@V2x@A_27a) => (( ! [V3y:$i] : ((mem@V3y@A_27a) => ((p@(ap@(ap@V0_3C_3C@V3y)@V2x)) => (p@(ap@V1P@V3y))))) => (p@(ap@V1P@V2x))))) => ( ! [V4x:$i] : ((mem@V4x@A_27a) => (p@(ap@V1P@V4x)))))))))))).
thf(conj_thm_2Ewellorder_2EWF__DCHAIN,lemma,( ! [A_27a:del]: ( ! [V0_3C_3C:$i] : ((mem@V0_3C_3C@(arr@A_27a@(arr@A_27a@bool))) => ((p@(ap@(c_2Erelation_2EWF@A_27a)@V0_3C_3C)) <=> (~~ (? [V1s:$i] : ((mem@V1s@(arr@ty_2Enum_2Enum@A_27a)) & ( ! [V2n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@V0_3C_3C@(ap@V1s@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V2n))))@(ap@V1s@(inj__ty_2Enum_2Enum @ V2n))))))))))))).
thf(conj_thm_2Ewellorder_2EWF__UREC,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0_3C_3C:$i] : ((mem@V0_3C_3C@(arr@A_27a@(arr@A_27a@bool))) => ((p@(ap@(c_2Erelation_2EWF@A_27a)@V0_3C_3C)) => ( ! [V1H:$i] : ((mem@V1H@(arr@(arr@A_27a@A_27b)@(arr@A_27a@A_27b))) => (( ! [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27b)) => ( ! [V3g:$i] : ((mem@V3g@(arr@A_27a@A_27b)) => ( ! [V4x:$i] : ((mem@V4x@A_27a) => (( ! [V5z:$i] : ((mem@V5z@A_27a) => ((p@(ap@(ap@V0_3C_3C@V5z)@V4x)) => ((ap@V2f@V5z) = (ap@V3g@V5z))))) => ((ap@(ap@V1H@V2f)@V4x) = (ap@(ap@V1H@V3g)@V4x))))))))) => ( ! [V6f:$i] : ((mem@V6f@(arr@A_27a@A_27b)) => ( ! [V7g:$i] : ((mem@V7g@(arr@A_27a@A_27b)) => ((( ! [V8x:$i] : ((mem@V8x@A_27a) => ((ap@V6f@V8x) = (ap@(ap@V1H@V6f)@V8x)))) & ( ! [V9x:$i] : ((mem@V9x@A_27a) => ((ap@V7g@V9x) = (ap@(ap@V1H@V7g)@V9x))))) => (V6f = V7g))))))))))))))).
thf(conj_thm_2Ewellorder_2EWF__UREC__WF,lemma,( ! [A_27a:del]: ( ! [V0_3C_3C:$i] : ((mem@V0_3C_3C@(arr@A_27a@(arr@A_27a@bool))) => (( ! [V1H:$i] : ((mem@V1H@(arr@(arr@A_27a@bool)@(arr@A_27a@bool))) => (( ! [V2f:$i] : ((mem@V2f@(arr@A_27a@bool)) => ( ! [V3g:$i] : ((mem@V3g@(arr@A_27a@bool)) => ( ! [V4x:$i] : ((mem@V4x@A_27a) => (( ! [V5z:$i] : ((mem@V5z@A_27a) => ((p@(ap@(ap@V0_3C_3C@V5z)@V4x)) => ((p@(ap@V2f@V5z)) <=> (p@(ap@V3g@V5z)))))) => ((p@(ap@(ap@V1H@V2f)@V4x)) <=> (p@(ap@(ap@V1H@V3g)@V4x)))))))))) => ( ! [V6f:$i] : ((mem@V6f@(arr@A_27a@bool)) => ( ! [V7g:$i] : ((mem@V7g@(arr@A_27a@bool)) => ((( ! [V8x:$i] : ((mem@V8x@A_27a) => ((p@(ap@V6f@V8x)) <=> (p@(ap@(ap@V1H@V6f)@V8x))))) & ( ! [V9x:$i] : ((mem@V9x@A_27a) => ((p@(ap@V7g@V9x)) <=> (p@(ap@(ap@V1H@V7g)@V9x)))))) => (V6f = V7g))))))))) => (p@(ap@(c_2Erelation_2EWF@A_27a)@V0_3C_3C))))))).
thf(conj_thm_2Ewellorder_2EWF__REC__INVARIANT,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0_3C_3C:$i] : ((mem@V0_3C_3C@(arr@A_27a@(arr@A_27a@bool))) => ((p@(ap@(c_2Erelation_2EWF@A_27a)@V0_3C_3C)) => ( ! [V1H:$i] : ((mem@V1H@(arr@(arr@A_27a@A_27b)@(arr@A_27a@A_27b))) => ( ! [V2S:$i] : ((mem@V2S@(arr@A_27a@(arr@A_27b@bool))) => (( ! [V3f:$i] : ((mem@V3f@(arr@A_27a@A_27b)) => ( ! [V4g:$i] : ((mem@V4g@(arr@A_27a@A_27b)) => ( ! [V5x:$i] : ((mem@V5x@A_27a) => (( ! [V6z:$i] : ((mem@V6z@A_27a) => ((p@(ap@(ap@V0_3C_3C@V6z)@V5x)) => (((ap@V3f@V6z) = (ap@V4g@V6z)) & (p@(ap@(ap@V2S@V6z)@(ap@V3f@V6z))))))) => (((ap@(ap@V1H@V3f)@V5x) = (ap@(ap@V1H@V4g)@V5x)) & (p@(ap@(ap@V2S@V5x)@(ap@(ap@V1H@V3f)@V5x))))))))))) => (? [V7f:$i] : ((mem@V7f@(arr@A_27a@A_27b)) & ( ! [V8x:$i] : ((mem@V8x@A_27a) => ((ap@V7f@V8x) = (ap@(ap@V1H@V7f)@V8x))))))))))))))))).
thf(conj_thm_2Ewellorder_2EWF__REC,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0_3C_3C:$i] : ((mem@V0_3C_3C@(arr@A_27a@(arr@A_27a@bool))) => ((p@(ap@(c_2Erelation_2EWF@A_27a)@V0_3C_3C)) => ( ! [V1H:$i] : ((mem@V1H@(arr@(arr@A_27a@A_27b)@(arr@A_27a@A_27b))) => (( ! [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27b)) => ( ! [V3g:$i] : ((mem@V3g@(arr@A_27a@A_27b)) => ( ! [V4x:$i] : ((mem@V4x@A_27a) => (( ! [V5z:$i] : ((mem@V5z@A_27a) => ((p@(ap@(ap@V0_3C_3C@V5z)@V4x)) => ((ap@V2f@V5z) = (ap@V3g@V5z))))) => ((ap@(ap@V1H@V2f)@V4x) = (ap@(ap@V1H@V3g)@V4x))))))))) => (? [V6f:$i] : ((mem@V6f@(arr@A_27a@A_27b)) & ( ! [V7x:$i] : ((mem@V7x@A_27a) => ((ap@V6f@V7x) = (ap@(ap@V1H@V6f)@V7x))))))))))))))).
thf(conj_thm_2Ewellorder_2EWF__num,lemma,(p@(ap@(c_2Erelation_2EWF@ty_2Enum_2Enum)@c_2Eprim__rec_2E_3C))).
thf(conj_thm_2Ewellorder_2EWF__REC__num,lemma,( ! [A_27a:del]: ( ! [V0H:$i] : ((mem@V0H@(arr@(arr@ty_2Enum_2Enum@A_27a)@(arr@ty_2Enum_2Enum@A_27a))) => (( ! [V1f:$i] : ((mem@V1f@(arr@ty_2Enum_2Enum@A_27a)) => ( ! [V2g:$i] : ((mem@V2g@(arr@ty_2Enum_2Enum@A_27a)) => ( ! [V3n:tp__ty_2Enum_2Enum] : (( ! [V4m:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V4m))@(inj__ty_2Enum_2Enum @ V3n))) => ((ap@V1f@(inj__ty_2Enum_2Enum @ V4m)) = (ap@V2g@(inj__ty_2Enum_2Enum @ V4m))))) => ((ap@(ap@V0H@V1f)@(inj__ty_2Enum_2Enum @ V3n)) = (ap@(ap@V0H@V2g)@(inj__ty_2Enum_2Enum @ V3n))))))))) => (? [V5f:$i] : ((mem@V5f@(arr@ty_2Enum_2Enum@A_27a)) & ( ! [V6n:tp__ty_2Enum_2Enum] : ((ap@V5f@(inj__ty_2Enum_2Enum @ V6n)) = (ap@(ap@V0H@V5f)@(inj__ty_2Enum_2Enum @ V6n))))))))))).
thf(ax_thm_2Ewellorder_2Efl,axiom,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(arr@(ty_2Epair_2Eprod@A_27a@A_27a)@bool)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ((p@(ap@(ap@(c_2Ewellorder_2Efl@A_27a)@V0l)@V1x)) <=> (? [V2y:$i] : ((mem@V2y@A_27a) & ((p@(ap@V0l@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V1x)@V2y))) | (p@(ap@V0l@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V2y)@V1x))))))))))))).
thf(ax_thm_2Ewellorder_2Eposet,axiom,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(arr@(ty_2Epair_2Eprod@A_27a@A_27a)@bool)) => ((p@(ap@(c_2Ewellorder_2Eposet@A_27a)@V0l)) <=> (( ! [V1x:$i] : ((mem@V1x@A_27a) => ((p@(ap@(ap@(c_2Ewellorder_2Efl@A_27a)@V0l)@V1x)) => (p@(ap@V0l@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V1x)@V1x)))))) & (( ! [V2x:$i] : ((mem@V2x@A_27a) => ( ! [V3y:$i] : ((mem@V3y@A_27a) => ( ! [V4z:$i] : ((mem@V4z@A_27a) => (((p@(ap@V0l@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V2x)@V3y))) & (p@(ap@V0l@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V3y)@V4z)))) => (p@(ap@V0l@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V2x)@V4z)))))))))) & ( ! [V5x:$i] : ((mem@V5x@A_27a) => ( ! [V6y:$i] : ((mem@V6y@A_27a) => (((p@(ap@V0l@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V5x)@V6y))) & (p@(ap@V0l@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V6y)@V5x)))) => (V5x = V6y))))))))))))).
thf(ax_thm_2Ewellorder_2Echain,axiom,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(arr@(ty_2Epair_2Eprod@A_27a@A_27a)@bool)) => ( ! [V1P:$i] : ((mem@V1P@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Ewellorder_2EChain@A_27a)@V0l)@V1P)) <=> ( ! [V2x:$i] : ((mem@V2x@A_27a) => ( ! [V3y:$i] : ((mem@V3y@A_27a) => (((p@(ap@V1P@V2x)) & (p@(ap@V1P@V3y))) => ((p@(ap@V0l@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V2x)@V3y))) | (p@(ap@V0l@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V3y)@V2x)))))))))))))))).
thf(conj_thm_2Ewellorder_2EZL,lemma,( ! [A_27a:del]: ( ! [V0l:$i] : ((mem@V0l@(arr@(ty_2Epair_2Eprod@A_27a@A_27a)@bool)) => (((p@(ap@(c_2Ewellorder_2Eposet@A_27a)@V0l)) & ((? [V1x:$i] : ((mem@V1x@A_27a) & (p@(ap@(lam@A_27a@(^ [V2x:$i] : (ap@(ap@(c_2Ewellorder_2Efl@A_27a)@V0l)@V2x)))@V1x)))) & ( ! [V3P:$i] : ((mem@V3P@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Ewellorder_2EChain@A_27a)@V0l)@V3P)) => (? [V4y:$i] : ((mem@V4y@A_27a) & ((p@(ap@(ap@(c_2Ewellorder_2Efl@A_27a)@V0l)@V4y)) & ( ! [V5x:$i] : ((mem@V5x@A_27a) => ((p@(ap@V3P@V5x)) => (p@(ap@V0l@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V5x)@V4y)))))))))))))) => (? [V6y:$i] : ((mem@V6y@A_27a) & ((p@(ap@(ap@(c_2Ewellorder_2Efl@A_27a)@V0l)@V6y)) & ( ! [V7x:$i] : ((mem@V7x@A_27a) => ((p@(ap@V0l@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27a)@V6y)@V7x))) => (V6y = V7x)))))))))))).
thf(conj_thm_2Ewellorder_2EPOSET__RESTRICTED__SUBSET,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@(arr@A_27a@bool)@bool)) => (p@(ap@(c_2Ewellorder_2Eposet@(arr@A_27a@bool))@(ap@(c_2Epair_2EUNCURRY@(arr@A_27a@bool)@(arr@A_27a@bool)@bool)@(lam@(arr@A_27a@bool)@(^ [V1x:$i] : (lam@(arr@A_27a@bool)@(^ [V2y:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0P@V1x))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0P@V2y))@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V1x)@V2y)))))))))))))).
thf(conj_thm_2Ewellorder_2EFL__RESTRICTED__SUBSET,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@(arr@A_27a@bool)@bool)) => ((ap@(c_2Ewellorder_2Efl@(arr@A_27a@bool))@(ap@(c_2Epair_2EUNCURRY@(arr@A_27a@bool)@(arr@A_27a@bool)@bool)@(lam@(arr@A_27a@bool)@(^ [V1x:$i] : (lam@(arr@A_27a@bool)@(^ [V2y:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0P@V1x))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@V0P@V2y))@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V1x)@V2y))))))))) = V0P))))).
thf(conj_thm_2Ewellorder_2EZL__SUBSETS,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@(arr@A_27a@bool)@bool)) => (( ! [V1c:$i] : ((mem@V1c@(arr@(arr@A_27a@bool)@bool)) => ((( ! [V2x:$i] : ((mem@V2x@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@bool))@V2x)@V1c)) => (p@(ap@V0P@V2x))))) & ( ! [V3x:$i] : ((mem@V3x@(arr@A_27a@bool)) => ( ! [V4y:$i] : ((mem@V4y@(arr@A_27a@bool)) => (((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@bool))@V3x)@V1c)) & (p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@bool))@V4y)@V1c))) => ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V3x)@V4y)) | (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V4y)@V3x))))))))) => (? [V5z:$i] : ((mem@V5z@(arr@A_27a@bool)) & ((p@(ap@V0P@V5z)) & ( ! [V6x:$i] : ((mem@V6x@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@bool))@V6x)@V1c)) => (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V6x)@V5z))))))))))) => (? [V7a:$i] : ((mem@V7a@(arr@A_27a@bool)) & ((p@(ap@V0P@V7a)) & ( ! [V8x:$i] : ((mem@V8x@(arr@A_27a@bool)) => (((p@(ap@V0P@V8x)) & (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V7a)@V8x))) => (V7a = V8x)))))))))))).
thf(conj_thm_2Ewellorder_2EZL__SUBSETS__BIGUNION,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@(arr@A_27a@bool)@bool)) => (( ! [V1c:$i] : ((mem@V1c@(arr@(arr@A_27a@bool)@bool)) => ((( ! [V2x:$i] : ((mem@V2x@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@bool))@V2x)@V1c)) => (p@(ap@V0P@V2x))))) & ( ! [V3x:$i] : ((mem@V3x@(arr@A_27a@bool)) => ( ! [V4y:$i] : ((mem@V4y@(arr@A_27a@bool)) => (((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@bool))@V3x)@V1c)) & (p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@bool))@V4y)@V1c))) => ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V3x)@V4y)) | (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V4y)@V3x))))))))) => (p@(ap@V0P@(ap@(c_2Epred__set_2EBIGUNION@A_27a)@V1c)))))) => (? [V5a:$i] : ((mem@V5a@(arr@A_27a@bool)) & ((p@(ap@V0P@V5a)) & ( ! [V6x:$i] : ((mem@V6x@(arr@A_27a@bool)) => (((p@(ap@V0P@V6x)) & (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V5a)@V6x))) => (V5a = V6x)))))))))))).
thf(conj_thm_2Ewellorder_2EZL__SUBSETS__BIGUNION__NONEMPTY,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@(arr@A_27a@bool)@bool)) => (((? [V1x:$i] : ((mem@V1x@(arr@A_27a@bool)) & (p@(ap@V0P@V1x)))) & ( ! [V2c:$i] : ((mem@V2c@(arr@(arr@A_27a@bool)@bool)) => (((? [V3x:$i] : ((mem@V3x@(arr@A_27a@bool)) & (p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@bool))@V3x)@V2c)))) & (( ! [V4x:$i] : ((mem@V4x@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@bool))@V4x)@V2c)) => (p@(ap@V0P@V4x))))) & ( ! [V5x:$i] : ((mem@V5x@(arr@A_27a@bool)) => ( ! [V6y:$i] : ((mem@V6y@(arr@A_27a@bool)) => (((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@bool))@V5x)@V2c)) & (p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@bool))@V6y)@V2c))) => ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V5x)@V6y)) | (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V6y)@V5x)))))))))) => (p@(ap@V0P@(ap@(c_2Epred__set_2EBIGUNION@A_27a)@V2c))))))) => (? [V7a:$i] : ((mem@V7a@(arr@A_27a@bool)) & ((p@(ap@V0P@V7a)) & ( ! [V8x:$i] : ((mem@V8x@(arr@A_27a@bool)) => (((p@(ap@V0P@V8x)) & (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V7a)@V8x))) => (V7a = V8x)))))))))))).
thf(conj_thm_2Ewellorder_2EFLATTEN__LEMMA,conjecture,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0g:$i] : ((mem@V0g@(arr@A_27b@A_27a)) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27a@A_27b)) => ( ! [V2s:$i] : ((mem@V2s@(arr@A_27a@bool)) => (( ! [V3x:$i] : ((mem@V3x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@V2s)) => ((ap@V0g@(ap@V1f@V3x)) = V3x)))) <=> ( ! [V4y:$i] : ((mem@V4y@A_27b) => ( ! [V5x:$i] : ((mem@V5x@A_27a) => (((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V5x)@V2s)) & (V4y = (ap@V1f@V5x))) => ((ap@V0g@V4y) = V5x)))))))))))))))).
