include('Axioms/ring^2.ax').
thf(tp_c_2Ecardinal_2E_2B__c,type,(c_2Ecardinal_2E_2B__c:(del>(del>$i)))).
thf(mem_c_2Ecardinal_2E_2B__c,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Ecardinal_2E_2B__c@A_27a@A_27b)@(arr@(arr@A_27a@bool)@(arr@(arr@A_27b@bool)@(arr@(ty_2Esum_2Esum@A_27a@A_27b)@bool))))))).
thf(tp_c_2Ecardinal_2EHAS__SIZE,type,(c_2Ecardinal_2EHAS__SIZE:(del>$i))).
thf(mem_c_2Ecardinal_2EHAS__SIZE,axiom,( ! [A_27a:del] : (mem@(c_2Ecardinal_2EHAS__SIZE@A_27a)@(arr@(arr@A_27a@bool)@(arr@ty_2Enum_2Enum@bool))))).
thf(tp_c_2Ecardinal_2Ebijns,type,(c_2Ecardinal_2Ebijns:(del>$i))).
thf(mem_c_2Ecardinal_2Ebijns,axiom,( ! [A_27a:del] : (mem@(c_2Ecardinal_2Ebijns@A_27a)@(arr@(arr@A_27a@bool)@(arr@(arr@A_27a@(ty_2Eoption_2Eoption@A_27a))@bool))))).
thf(tp_c_2Ecardinal_2Ecardeq,type,(c_2Ecardinal_2Ecardeq:(del>(del>$i)))).
thf(mem_c_2Ecardinal_2Ecardeq,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Ecardinal_2Ecardeq@A_27a@A_27b)@(arr@(arr@A_27a@bool)@(arr@(arr@A_27b@bool)@bool)))))).
thf(tp_c_2Ecardinal_2Ecardgeq,type,(c_2Ecardinal_2Ecardgeq:(del>(del>$i)))).
thf(mem_c_2Ecardinal_2Ecardgeq,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Ecardinal_2Ecardgeq@A_27a@A_27b)@(arr@(arr@A_27a@bool)@(arr@(arr@A_27b@bool)@bool)))))).
thf(tp_c_2Ecardinal_2Ecardgt,type,(c_2Ecardinal_2Ecardgt:(del>(del>$i)))).
thf(mem_c_2Ecardinal_2Ecardgt,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Ecardinal_2Ecardgt@A_27a@A_27b)@(arr@(arr@A_27a@bool)@(arr@(arr@A_27b@bool)@bool)))))).
thf(tp_c_2Ecardinal_2Ecardleq,type,(c_2Ecardinal_2Ecardleq:(del>(del>$i)))).
thf(mem_c_2Ecardinal_2Ecardleq,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Ecardinal_2Ecardleq@A_27a@A_27b)@(arr@(arr@A_27a@bool)@(arr@(arr@A_27b@bool)@bool)))))).
thf(tp_c_2Ecardinal_2Elist,type,(c_2Ecardinal_2Elist:(del>$i))).
thf(mem_c_2Ecardinal_2Elist,axiom,( ! [A_27a:del] : (mem@(c_2Ecardinal_2Elist@A_27a)@(arr@(arr@A_27a@bool)@(arr@(ty_2Elist_2Elist@A_27a)@bool))))).
thf(tp_c_2Ecardinal_2Eset__exp,type,(c_2Ecardinal_2Eset__exp:(del>(del>$i)))).
thf(mem_c_2Ecardinal_2Eset__exp,axiom,( ! [A_27a:del] : ( ! [A_27b:del] : (mem@(c_2Ecardinal_2Eset__exp@A_27a@A_27b)@(arr@(arr@A_27b@bool)@(arr@(arr@A_27a@bool)@(arr@(arr@A_27a@(ty_2Eoption_2Eoption@A_27b))@bool))))))).
thf(ax_thm_2Ecardinal_2Ecardeq__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s1:$i] : ((mem@V0s1@(arr@A_27a@bool)) => ( ! [V1s2:$i] : ((mem@V1s2@(arr@A_27b@bool)) => ((p@(ap@(ap@(c_2Ecardinal_2Ecardeq@A_27a@A_27b)@V0s1)@V1s2)) <=> (? [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27b)) & (p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27b)@V2f)@V0s1)@V1s2)))))))))))).
thf(conj_thm_2Ecardinal_2Ecardeq__REFL,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => (p@(ap@(ap@(c_2Ecardinal_2Ecardeq@A_27a@A_27a)@V0s)@V0s)))))).
thf(conj_thm_2Ecardinal_2Ecardeq__SYM,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => ((p@(ap@(ap@(c_2Ecardinal_2Ecardeq@A_27a@A_27b)@V0s)@V1t)) <=> (p@(ap@(ap@(c_2Ecardinal_2Ecardeq@A_27b@A_27a)@V1t)@V0s)))))))))).
thf(conj_thm_2Ecardinal_2Ecardeq__TRANS,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => ( ! [V2u:$i] : ((mem@V2u@(arr@A_27c@bool)) => (((p@(ap@(ap@(c_2Ecardinal_2Ecardeq@A_27a@A_27b)@V0s)@V1t)) & (p@(ap@(ap@(c_2Ecardinal_2Ecardeq@A_27b@A_27c)@V1t)@V2u))) => (p@(ap@(ap@(c_2Ecardinal_2Ecardeq@A_27a@A_27c)@V0s)@V2u))))))))))))).
thf(ax_thm_2Ecardinal_2Ecardleq__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s1:$i] : ((mem@V0s1@(arr@A_27a@bool)) => ( ! [V1s2:$i] : ((mem@V1s2@(arr@A_27b@bool)) => ((p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27a@A_27b)@V0s1)@V1s2)) <=> (? [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27b)) & (p@(ap@(ap@(ap@(c_2Epred__set_2EINJ@A_27a@A_27b)@V2f)@V0s1)@V1s2)))))))))))).
thf(conj_thm_2Ecardinal_2Ecardleq__REFL,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27a@A_27a)@V0s)@V0s)))))).
thf(conj_thm_2Ecardinal_2Ecardleq__TRANS,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => ( ! [V2u:$i] : ((mem@V2u@(arr@A_27c@bool)) => (((p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27a@A_27b)@V0s)@V1t)) & (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27b@A_27c)@V1t)@V2u))) => (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27a@A_27c)@V0s)@V2u))))))))))))).
thf(conj_thm_2Ecardinal_2Ecardleq__ANTISYM,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => (((p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27a@A_27b)@V0s)@V1t)) & (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27b@A_27a)@V1t)@V0s))) => (p@(ap@(ap@(c_2Ecardinal_2Ecardeq@A_27a@A_27b)@V0s)@V1t)))))))))).
thf(conj_thm_2Ecardinal_2ECARDEQ__FINITE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s1:$i] : ((mem@V0s1@(arr@A_27a@bool)) => ( ! [V1s2:$i] : ((mem@V1s2@(arr@A_27b@bool)) => ((p@(ap@(ap@(c_2Ecardinal_2Ecardeq@A_27a@A_27b)@V0s1)@V1s2)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s1)) <=> (p@(ap@(c_2Epred__set_2EFINITE@A_27b)@V1s2))))))))))).
thf(conj_thm_2Ecardinal_2ECARDEQ__CARD,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s1:$i] : ((mem@V0s1@(arr@A_27a@bool)) => ( ! [V1s2:$i] : ((mem@V1s2@(arr@A_27b@bool)) => (((p@(ap@(ap@(c_2Ecardinal_2Ecardeq@A_27a@A_27b)@V0s1)@V1s2)) & (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s1))) => ((surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27a)@V0s1)) = (surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27b)@V1s2))))))))))).
thf(conj_thm_2Ecardinal_2ECARDEQ__0,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0x:$i] : ((mem@V0x@(arr@A_27a@bool)) => (((p@(ap@(ap@(c_2Ecardinal_2Ecardeq@A_27a@A_27b)@V0x)@(c_2Epred__set_2EEMPTY@A_27b))) <=> (V0x = (c_2Epred__set_2EEMPTY@A_27a))) & ((p@(ap@(ap@(c_2Ecardinal_2Ecardeq@A_27c@A_27a)@(c_2Epred__set_2EEMPTY@A_27c))@V0x)) <=> (V0x = (c_2Epred__set_2EEMPTY@A_27a)))))))))).
thf(conj_thm_2Ecardinal_2Ecardeq__INSERT,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Ecardinal_2Ecardeq@A_27a@A_27a)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@V1s))@V1s)) <=> ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0x)@V1s)) | (~~ (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1s))))))))))).
thf(conj_thm_2Ecardinal_2ECARDEQ__INSERT__RWT,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@A_27a) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ((~~ (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1s))) => (p@(ap@(ap@(c_2Ecardinal_2Ecardeq@A_27a@A_27a)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0x)@V1s))@V1s))))))))).
thf(conj_thm_2Ecardinal_2EEMPTY__CARDLEQ,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0t:$i] : ((mem@V0t@(arr@A_27b@bool)) => (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27a@A_27b)@(c_2Epred__set_2EEMPTY@A_27a))@V0t))))))).
thf(conj_thm_2Ecardinal_2EFINITE__CLE__INFINITE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => (((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s)) & (~~ (p@(ap@(c_2Epred__set_2EFINITE@A_27b)@V1t)))) => (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27a@A_27b)@V0s)@V1t)))))))))).
thf(conj_thm_2Ecardinal_2ECARDEQ__CROSS,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [V0s1:$i] : ((mem@V0s1@(arr@A_27a@bool)) => ( ! [V1s2:$i] : ((mem@V1s2@(arr@A_27b@bool)) => ( ! [V2t1:$i] : ((mem@V2t1@(arr@A_27c@bool)) => ( ! [V3t2:$i] : ((mem@V3t2@(arr@A_27d@bool)) => (((p@(ap@(ap@(c_2Ecardinal_2Ecardeq@A_27a@A_27b)@V0s1)@V1s2)) & (p@(ap@(ap@(c_2Ecardinal_2Ecardeq@A_27c@A_27d)@V2t1)@V3t2))) => (p@(ap@(ap@(c_2Ecardinal_2Ecardeq@(ty_2Epair_2Eprod@A_27a@A_27c)@(ty_2Epair_2Eprod@A_27b@A_27d))@(ap@(ap@(c_2Epred__set_2ECROSS@A_27a@A_27c)@V0s1)@V2t1))@(ap@(ap@(c_2Epred__set_2ECROSS@A_27b@A_27d)@V1s2)@V3t2))))))))))))))))).
thf(conj_thm_2Ecardinal_2ECARDEQ__CROSS__SYM,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => (p@(ap@(ap@(c_2Ecardinal_2Ecardeq@(ty_2Epair_2Eprod@A_27a@A_27b)@(ty_2Epair_2Eprod@A_27b@A_27a))@(ap@(ap@(c_2Epred__set_2ECROSS@A_27a@A_27b)@V0s)@V1t))@(ap@(ap@(c_2Epred__set_2ECROSS@A_27b@A_27a)@V1t)@V0s)))))))))).
thf(conj_thm_2Ecardinal_2ECARDEQ__SUBSET__CARDLEQ,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => ((p@(ap@(ap@(c_2Ecardinal_2Ecardeq@A_27a@A_27b)@V0s)@V1t)) => (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27a@A_27b)@V0s)@V1t)))))))))).
thf(conj_thm_2Ecardinal_2ECARDEQ__CARDLEQ,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [V0s1:$i] : ((mem@V0s1@(arr@A_27a@bool)) => ( ! [V1s2:$i] : ((mem@V1s2@(arr@A_27b@bool)) => ( ! [V2t1:$i] : ((mem@V2t1@(arr@A_27c@bool)) => ( ! [V3t2:$i] : ((mem@V3t2@(arr@A_27d@bool)) => (((p@(ap@(ap@(c_2Ecardinal_2Ecardeq@A_27a@A_27b)@V0s1)@V1s2)) & (p@(ap@(ap@(c_2Ecardinal_2Ecardeq@A_27c@A_27d)@V2t1)@V3t2))) => ((p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27a@A_27c)@V0s1)@V2t1)) <=> (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27b@A_27d)@V1s2)@V3t2))))))))))))))))).
thf(conj_thm_2Ecardinal_2ECARDLEQ__FINITE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s1:$i] : ((mem@V0s1@(arr@A_27a@bool)) => ( ! [V1s2:$i] : ((mem@V1s2@(arr@A_27b@bool)) => (((p@(ap@(c_2Epred__set_2EFINITE@A_27b)@V1s2)) & (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27a@A_27b)@V0s1)@V1s2))) => (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s1)))))))))).
thf(conj_thm_2Ecardinal_2EINFINITE__UNIV__INF,lemma,( ! [A_27a:del]: (~~ (p@(ap@(c_2Epred__set_2EFINITE@(ty_2Esum_2Esum@ty_2Enum_2Enum@A_27a))@(c_2Epred__set_2EUNIV@(ty_2Esum_2Esum@ty_2Enum_2Enum@A_27a))))))).
thf(conj_thm_2Ecardinal_2EIMAGE__cardleq,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27b@A_27a)@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@V1s))@V1s))))))))).
thf(conj_thm_2Ecardinal_2ECARDLEQ__CROSS__CONG,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [V0x1:$i] : ((mem@V0x1@(arr@A_27a@bool)) => ( ! [V1x2:$i] : ((mem@V1x2@(arr@A_27b@bool)) => ( ! [V2y1:$i] : ((mem@V2y1@(arr@A_27c@bool)) => ( ! [V3y2:$i] : ((mem@V3y2@(arr@A_27d@bool)) => (((p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27a@A_27b)@V0x1)@V1x2)) & (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27c@A_27d)@V2y1)@V3y2))) => (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@(ty_2Epair_2Eprod@A_27a@A_27c)@(ty_2Epair_2Eprod@A_27b@A_27d))@(ap@(ap@(c_2Epred__set_2ECROSS@A_27a@A_27c)@V0x1)@V2y1))@(ap@(ap@(c_2Epred__set_2ECROSS@A_27b@A_27d)@V1x2)@V3y2))))))))))))))))).
thf(conj_thm_2Ecardinal_2ESUBSET__CARDLEQ,lemma,( ! [A_27a:del]: ( ! [V0x:$i] : ((mem@V0x@(arr@A_27a@bool)) => ( ! [V1y:$i] : ((mem@V1y@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V0x)@V1y)) => (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27a@A_27a)@V0x)@V1y))))))))).
thf(conj_thm_2Ecardinal_2EIMAGE__cardleq__rwt,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27c)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27b@bool)) => ((p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27a@A_27b)@V1s)@V2t)) => (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27c@A_27b)@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27c)@V0f)@V1s))@V2t))))))))))))).
thf(conj_thm_2Ecardinal_2Ecountable__thm,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2Ecountable@A_27a)@V0s)) <=> (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27a@ty_2Enum_2Enum)@V0s)@(c_2Epred__set_2EUNIV@ty_2Enum_2Enum)))))))).
thf(conj_thm_2Ecardinal_2Ecountable__cardeq,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => ((p@(ap@(ap@(c_2Ecardinal_2Ecardeq@A_27a@A_27b)@V0s)@V1t)) => ((p@(ap@(c_2Epred__set_2Ecountable@A_27a)@V0s)) <=> (p@(ap@(c_2Epred__set_2Ecountable@A_27b)@V1t))))))))))).
thf(conj_thm_2Ecardinal_2Ecardleq__dichotomy,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => ((p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27a@A_27b)@V0s)@V1t)) | (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27b@A_27a)@V1t)@V0s)))))))))).
thf(conj_thm_2Ecardinal_2Ecardleq__lteq,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s1:$i] : ((mem@V0s1@(arr@A_27a@bool)) => ( ! [V1s2:$i] : ((mem@V1s2@(arr@A_27b@bool)) => ((p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27a@A_27b)@V0s1)@V1s2)) <=> ((~~ (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27b@A_27a)@V1s2)@V0s1))) | (p@(ap@(ap@(c_2Ecardinal_2Ecardeq@A_27a@A_27b)@V0s1)@V1s2))))))))))).
thf(conj_thm_2Ecardinal_2Ecardlt__REFL,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => (~~ (~~ (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27a@A_27a)@V0s)@V0s)))))))).
thf(conj_thm_2Ecardinal_2Ecardlt__lenoteq,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => ((~~ (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27b@A_27a)@V1t)@V0s))) <=> ((p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27a@A_27b)@V0s)@V1t)) & (~~ (p@(ap@(ap@(c_2Ecardinal_2Ecardeq@A_27a@A_27b)@V0s)@V1t)))))))))))).
thf(conj_thm_2Ecardinal_2Ecardlt__TRANS,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27b@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27c@bool)) => ( ! [V2u:$i] : ((mem@V2u@(arr@A_27a@bool)) => (((~~ (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27c@A_27b)@V1t)@V0s))) & (~~ (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27a@A_27c)@V2u)@V1t)))) => (~~ (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27a@A_27b)@V2u)@V0s)))))))))))))).
thf(conj_thm_2Ecardinal_2Ecardlt__leq__trans,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0r:$i] : ((mem@V0r@(arr@A_27a@bool)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27b@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27c@bool)) => (((~~ (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27b@A_27a)@V1s)@V0r))) & (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27b@A_27c)@V1s)@V2t))) => (~~ (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27c@A_27a)@V2t)@V0r)))))))))))))).
thf(conj_thm_2Ecardinal_2Ecardleq__lt__trans,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0r:$i] : ((mem@V0r@(arr@A_27a@bool)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27b@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27c@bool)) => (((p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27a@A_27b)@V0r)@V1s)) & (~~ (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27c@A_27b)@V2t)@V1s)))) => (~~ (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27c@A_27a)@V2t)@V0r)))))))))))))).
thf(conj_thm_2Ecardinal_2Ecardleq__empty,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0x:$i] : ((mem@V0x@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27a@A_27b)@V0x)@(c_2Epred__set_2EEMPTY@A_27b))) <=> (V0x = (c_2Epred__set_2EEMPTY@A_27a)))))))).
thf(conj_thm_2Ecardinal_2Eset__binomial2,lemma,( ! [A_27a:del]: ( ! [V0A:$i] : ((mem@V0A@(arr@A_27a@bool)) => ( ! [V1B:$i] : ((mem@V1B@(arr@A_27a@bool)) => ((ap@(ap@(c_2Epred__set_2ECROSS@A_27a@A_27a)@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V0A)@V1B))@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V0A)@V1B)) = (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@(ap@(c_2Epred__set_2EUNION@(ty_2Epair_2Eprod@A_27a@A_27a))@(ap@(ap@(c_2Epred__set_2ECROSS@A_27a@A_27a)@V0A)@V0A))@(ap@(ap@(c_2Epred__set_2ECROSS@A_27a@A_27a)@V0A)@V1B)))@(ap@(ap@(c_2Epred__set_2ECROSS@A_27a@A_27a)@V1B)@V0A)))@(ap@(ap@(c_2Epred__set_2ECROSS@A_27a@A_27a)@V1B)@V1B))))))))).
thf(conj_thm_2Ecardinal_2ESET__SQUARED__CARDEQ__SET,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((~~ (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s))) => (p@(ap@(ap@(c_2Ecardinal_2Ecardeq@(ty_2Epair_2Eprod@A_27a@A_27a)@A_27a)@(ap@(ap@(c_2Epred__set_2ECROSS@A_27a@A_27a)@V0s)@V0s))@V0s))))))).
thf(conj_thm_2Ecardinal_2ESET__SUM__CARDEQ__SET,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((~~ (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s))) => ((p@(ap@(ap@(c_2Ecardinal_2Ecardeq@A_27a@(ty_2Epair_2Eprod@bool@A_27a))@V0s)@(ap@(ap@(c_2Epred__set_2ECROSS@bool@A_27a)@(ap@(ap@(c_2Epred__set_2EINSERT@bool)@c_2Ebool_2ET)@(ap@(ap@(c_2Epred__set_2EINSERT@bool)@c_2Ebool_2EF)@(c_2Epred__set_2EEMPTY@bool))))@V0s))) & ( ! [V1A:$i] : ((mem@V1A@(arr@A_27b@bool)) => ( ! [V2B:$i] : ((mem@V2B@(arr@A_27b@bool)) => (((p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27b)@V1A)@V2B)) & ((p@(ap@(ap@(c_2Ecardinal_2Ecardeq@A_27b@A_27a)@V1A)@V0s)) & (p@(ap@(ap@(c_2Ecardinal_2Ecardeq@A_27b@A_27a)@V2B)@V0s)))) => (p@(ap@(ap@(c_2Ecardinal_2Ecardeq@A_27b@A_27a)@(ap@(ap@(c_2Epred__set_2EUNION@A_27b)@V1A)@V2B))@V0s)))))))))))))).
thf(conj_thm_2Ecardinal_2ECARD__BIGUNION,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0k:$i] : ((mem@V0k@(arr@A_27a@bool)) => ( ! [V1s1:$i] : ((mem@V1s1@(arr@(arr@A_27b@bool)@bool)) => (((~~ (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0k))) & ((p@(ap@(ap@(c_2Ecardinal_2Ecardleq@(arr@A_27b@bool)@A_27a)@V1s1)@V0k)) & ( ! [V2e:$i] : ((mem@V2e@(arr@A_27b@bool)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27b@bool))@V2e)@V1s1)) => (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27b@A_27a)@V2e)@V0k))))))) => (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27b@A_27a)@(ap@(c_2Epred__set_2EBIGUNION@A_27b)@V1s1))@V0k)))))))))).
thf(ax_thm_2Ecardinal_2Eset__exp__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0A:$i] : ((mem@V0A@(arr@A_27b@bool)) => ( ! [V1B:$i] : ((mem@V1B@(arr@A_27a@bool)) => ((ap@(ap@(c_2Ecardinal_2Eset__exp@A_27a@A_27b)@V0A)@V1B) = (ap@(c_2Epred__set_2EGSPEC@(arr@A_27a@(ty_2Eoption_2Eoption@A_27b))@(arr@A_27a@(ty_2Eoption_2Eoption@A_27b)))@(lam@(arr@A_27a@(ty_2Eoption_2Eoption@A_27b))@(^ [V2f:$i] : (ap@(ap@(c_2Epair_2E_2C@(arr@A_27a@(ty_2Eoption_2Eoption@A_27b))@bool)@V2f)@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(c_2Ebool_2E_21@A_27a)@(lam@A_27a@(^ [V3b:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3b)@V1B))@(ap@(c_2Ebool_2E_3F@A_27b)@(lam@A_27b@(^ [V4a:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V4a)@V0A))@(ap@(ap@(c_2Emin_2E_3D@(ty_2Eoption_2Eoption@A_27b))@(ap@V2f@V3b))@(ap@(c_2Eoption_2ESOME@A_27b)@V4a)))))))))))@(ap@(c_2Ebool_2E_21@A_27a)@(lam@A_27a@(^ [V5b:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@c_2Ebool_2E_7E@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V5b)@V1B)))@(ap@(ap@(c_2Emin_2E_3D@(ty_2Eoption_2Eoption@A_27b))@(ap@V2f@V5b))@(c_2Eoption_2ENONE@A_27b))))))))))))))))))).
thf(conj_thm_2Ecardinal_2EBIJ__functions__agree,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1g:$i] : ((mem@V1g@(arr@A_27a@A_27b)) => ( ! [V2s:$i] : ((mem@V2s@(arr@A_27a@bool)) => ( ! [V3t:$i] : ((mem@V3t@(arr@A_27b@bool)) => (((p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27b)@V0f)@V2s)@V3t)) & ( ! [V4x:$i] : ((mem@V4x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V4x)@V2s)) => ((ap@V0f@V4x) = (ap@V1g@V4x)))))) => (p@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27b)@V1g)@V2s)@V3t)))))))))))))).
thf(conj_thm_2Ecardinal_2ECARD__CARDEQ__I,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s1:$i] : ((mem@V0s1@(arr@A_27a@bool)) => ( ! [V1s2:$i] : ((mem@V1s2@(arr@A_27b@bool)) => (((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s1)) & ((p@(ap@(c_2Epred__set_2EFINITE@A_27b)@V1s2)) & ((surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27a)@V0s1)) = (surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27b)@V1s2))))) => (p@(ap@(ap@(c_2Ecardinal_2Ecardeq@A_27a@A_27b)@V0s1)@V1s2)))))))))).
thf(conj_thm_2Ecardinal_2ECARDEQ__CARD__EQN,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s1:$i] : ((mem@V0s1@(arr@A_27a@bool)) => ( ! [V1s2:$i] : ((mem@V1s2@(arr@A_27b@bool)) => (((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s1)) & (p@(ap@(c_2Epred__set_2EFINITE@A_27b)@V1s2))) => ((p@(ap@(ap@(c_2Ecardinal_2Ecardeq@A_27a@A_27b)@V0s1)@V1s2)) <=> ((surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27a)@V0s1)) = (surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27b)@V1s2)))))))))))).
thf(conj_thm_2Ecardinal_2ECARDLEQ__CARD,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s1:$i] : ((mem@V0s1@(arr@A_27a@bool)) => ( ! [V1s2:$i] : ((mem@V1s2@(arr@A_27b@bool)) => (((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s1)) & (p@(ap@(c_2Epred__set_2EFINITE@A_27b)@V1s2))) => ((p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27a@A_27b)@V0s1)@V1s2)) <=> (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(c_2Epred__set_2ECARD@A_27a)@V0s1))@(ap@(c_2Epred__set_2ECARD@A_27b)@V1s2)))))))))))).
thf(conj_thm_2Ecardinal_2EEMPTY__set__exp,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [V0A:$i] : ((mem@V0A@(arr@A_27b@bool)) => ( ! [V1B:$i] : ((mem@V1B@(arr@A_27c@bool)) => (((ap@(ap@(c_2Ecardinal_2Eset__exp@A_27a@A_27b)@V0A)@(c_2Epred__set_2EEMPTY@A_27a)) = (ap@(ap@(c_2Epred__set_2EINSERT@(arr@A_27a@(ty_2Eoption_2Eoption@A_27b)))@(ap@(c_2Ecombin_2EK@(ty_2Eoption_2Eoption@A_27b)@A_27a)@(c_2Eoption_2ENONE@A_27b)))@(c_2Epred__set_2EEMPTY@(arr@A_27a@(ty_2Eoption_2Eoption@A_27b))))) & ((~~ (V1B = (c_2Epred__set_2EEMPTY@A_27c))) => ((ap@(ap@(c_2Ecardinal_2Eset__exp@A_27c@A_27d)@(c_2Epred__set_2EEMPTY@A_27d))@V1B) = (c_2Epred__set_2EEMPTY@(arr@A_27c@(ty_2Eoption_2Eoption@A_27d))))))))))))))).
thf(conj_thm_2Ecardinal_2EEMPTY__set__exp__CARD,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0A:$i] : ((mem@V0A@(arr@A_27b@bool)) => (p@(ap@(ap@(c_2Ecardinal_2Ecardeq@(arr@A_27a@(ty_2Eoption_2Eoption@A_27b))@ty_2Enum_2Enum)@(ap@(ap@(c_2Ecardinal_2Eset__exp@A_27a@A_27b)@V0A)@(c_2Epred__set_2EEMPTY@A_27a)))@(ap@c_2Epred__set_2Ecount@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))))).
thf(conj_thm_2Ecardinal_2ESING__set__exp,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0x:$i] : ((mem@V0x@A_27b) => ( ! [V1B:$i] : ((mem@V1B@(arr@A_27a@bool)) => ( ! [V2A:$i] : ((mem@V2A@(arr@A_27c@bool)) => (((ap@(ap@(c_2Ecardinal_2Eset__exp@A_27a@A_27b)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27b)@V0x)@(c_2Epred__set_2EEMPTY@A_27b)))@V1B) = (ap@(ap@(c_2Epred__set_2EINSERT@(arr@A_27a@(ty_2Eoption_2Eoption@A_27b)))@(lam@A_27a@(^ [V3b:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@A_27b))@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3b)@V1B))@(ap@(c_2Eoption_2ESOME@A_27b)@V0x))@(c_2Eoption_2ENONE@A_27b)))))@(c_2Epred__set_2EEMPTY@(arr@A_27a@(ty_2Eoption_2Eoption@A_27b))))) & ((ap@(ap@(c_2Ecardinal_2Eset__exp@A_27b@A_27c)@V2A)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27b)@V0x)@(c_2Epred__set_2EEMPTY@A_27b))) = (ap@(c_2Epred__set_2EGSPEC@(arr@A_27b@(ty_2Eoption_2Eoption@A_27c))@A_27c)@(lam@A_27c@(^ [V4a:$i] : (ap@(ap@(c_2Epair_2E_2C@(arr@A_27b@(ty_2Eoption_2Eoption@A_27c))@bool)@(lam@A_27b@(^ [V5b:$i] : (ap@(ap@(ap@(c_2Ebool_2ECOND@(ty_2Eoption_2Eoption@A_27c))@(ap@(ap@(c_2Emin_2E_3D@A_27b)@V5b)@V0x))@(ap@(c_2Eoption_2ESOME@A_27c)@V4a))@(c_2Eoption_2ENONE@A_27c)))))@(ap@(ap@(c_2Ebool_2EIN@A_27c)@V4a)@V2A))))))))))))))))).
thf(conj_thm_2Ecardinal_2ESING__set__exp__CARD,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0x:$i] : ((mem@V0x@A_27b) => ( ! [V1B:$i] : ((mem@V1B@(arr@A_27a@bool)) => ( ! [V2A:$i] : ((mem@V2A@(arr@A_27c@bool)) => ((p@(ap@(ap@(c_2Ecardinal_2Ecardeq@(arr@A_27a@(ty_2Eoption_2Eoption@A_27b))@ty_2Enum_2Enum)@(ap@(ap@(c_2Ecardinal_2Eset__exp@A_27a@A_27b)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27b)@V0x)@(c_2Epred__set_2EEMPTY@A_27b)))@V1B))@(ap@c_2Epred__set_2Ecount@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))) & (p@(ap@(ap@(c_2Ecardinal_2Ecardeq@(arr@A_27b@(ty_2Eoption_2Eoption@A_27c))@A_27c)@(ap@(ap@(c_2Ecardinal_2Eset__exp@A_27b@A_27c)@V2A)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27b)@V0x)@(c_2Epred__set_2EEMPTY@A_27b))))@V2A))))))))))))).
thf(conj_thm_2Ecardinal_2EPOW__TWO__set__exp,lemma,( ! [A_27a:del]: ( ! [V0A:$i] : ((mem@V0A@(arr@A_27a@bool)) => (p@(ap@(ap@(c_2Ecardinal_2Ecardeq@(arr@A_27a@bool)@(arr@A_27a@(ty_2Eoption_2Eoption@ty_2Enum_2Enum)))@(ap@(c_2Epred__set_2EPOW@A_27a)@V0A))@(ap@(ap@(c_2Ecardinal_2Eset__exp@A_27a@ty_2Enum_2Enum)@(ap@c_2Epred__set_2Ecount@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))@V0A))))))).
thf(conj_thm_2Ecardinal_2Eset__exp__count,lemma,( ! [A_27a:del]: ( ! [V0A:$i] : ((mem@V0A@(arr@A_27a@bool)) => ( ! [V1n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@(c_2Ecardinal_2Ecardeq@(arr@ty_2Enum_2Enum@(ty_2Eoption_2Eoption@A_27a))@(ty_2Elist_2Elist@A_27a))@(ap@(ap@(c_2Ecardinal_2Eset__exp@ty_2Enum_2Enum@A_27a)@V0A)@(ap@c_2Epred__set_2Ecount@(inj__ty_2Enum_2Enum @ V1n))))@(ap@(c_2Epred__set_2EGSPEC@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))@(lam@(ty_2Elist_2Elist@A_27a)@(^ [V2l:$i] : (ap@(ap@(c_2Epair_2E_2C@(ty_2Elist_2Elist@A_27a)@bool)@V2l)@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Emin_2E_3D@ty_2Enum_2Enum)@(ap@(c_2Elist_2ELENGTH@A_27a)@V2l))@(inj__ty_2Enum_2Enum @ V1n)))@(ap@(c_2Ebool_2E_21@A_27a)@(lam@A_27a@(^ [V3e:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3e)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@V2l)))@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3e)@V0A))))))))))))))))).
thf(conj_thm_2Ecardinal_2Eset__exp__card__cong,lemma,( ! [A_27a1:del]: ( ! [A_27a2:del]: ( ! [A_27b1:del]: ( ! [A_27b2:del]: ( ! [V0a1:$i] : ((mem@V0a1@(arr@A_27a1@bool)) => ( ! [V1a2:$i] : ((mem@V1a2@(arr@A_27a2@bool)) => ( ! [V2b1:$i] : ((mem@V2b1@(arr@A_27b1@bool)) => ( ! [V3b2:$i] : ((mem@V3b2@(arr@A_27b2@bool)) => ((p@(ap@(ap@(c_2Ecardinal_2Ecardeq@A_27a1@A_27a2)@V0a1)@V1a2)) => ((p@(ap@(ap@(c_2Ecardinal_2Ecardeq@A_27b1@A_27b2)@V2b1)@V3b2)) => (p@(ap@(ap@(c_2Ecardinal_2Ecardeq@(arr@A_27b1@(ty_2Eoption_2Eoption@A_27a1))@(arr@A_27b2@(ty_2Eoption_2Eoption@A_27a2)))@(ap@(ap@(c_2Ecardinal_2Eset__exp@A_27b1@A_27a1)@V0a1)@V2b1))@(ap@(ap@(c_2Ecardinal_2Eset__exp@A_27b2@A_27a2)@V1a2)@V3b2)))))))))))))))))).
thf(conj_thm_2Ecardinal_2Eset__exp__cardle__cong,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [V0b:$i] : ((mem@V0b@(arr@A_27a@bool)) => ( ! [V1d:$i] : ((mem@V1d@(arr@A_27b@bool)) => ( ! [V2a:$i] : ((mem@V2a@(arr@A_27c@bool)) => ( ! [V3c:$i] : ((mem@V3c@(arr@A_27d@bool)) => (((V0b = (c_2Epred__set_2EEMPTY@A_27a)) => (V1d = (c_2Epred__set_2EEMPTY@A_27b))) => (((p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27c@A_27a)@V2a)@V0b)) & (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27d@A_27b)@V3c)@V1d))) => (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@(arr@A_27d@(ty_2Eoption_2Eoption@A_27c))@(arr@A_27b@(ty_2Eoption_2Eoption@A_27a)))@(ap@(ap@(c_2Ecardinal_2Eset__exp@A_27d@A_27c)@V2a)@V3c))@(ap@(ap@(c_2Ecardinal_2Eset__exp@A_27b@A_27a)@V0b)@V1d)))))))))))))))))).
thf(conj_thm_2Ecardinal_2Eexp__INSERT__cardeq,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0e:$i] : ((mem@V0e@A_27a) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2A:$i] : ((mem@V2A@(arr@A_27b@bool)) => ((~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V0e)@V1s))) => (p@(ap@(ap@(c_2Ecardinal_2Ecardeq@(arr@A_27a@(ty_2Eoption_2Eoption@A_27b))@(ty_2Epair_2Eprod@A_27b@(arr@A_27a@(ty_2Eoption_2Eoption@A_27b))))@(ap@(ap@(c_2Ecardinal_2Eset__exp@A_27a@A_27b)@V2A)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0e)@V1s)))@(ap@(ap@(c_2Epred__set_2ECROSS@A_27b@(arr@A_27a@(ty_2Eoption_2Eoption@A_27b)))@V2A)@(ap@(ap@(c_2Ecardinal_2Eset__exp@A_27a@A_27b)@V2A)@V1s)))))))))))))).
thf(conj_thm_2Ecardinal_2Eexp__count__cardeq,lemma,( ! [A_27a:del]: ( ! [V0A:$i] : ((mem@V0A@(arr@A_27a@bool)) => ( ! [V1n:tp__ty_2Enum_2Enum] : (((~~ (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0A))) & (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V1n)))) => (p@(ap@(ap@(c_2Ecardinal_2Ecardeq@(arr@ty_2Enum_2Enum@(ty_2Eoption_2Eoption@A_27a))@A_27a)@(ap@(ap@(c_2Ecardinal_2Eset__exp@ty_2Enum_2Enum@A_27a)@V0A)@(ap@c_2Epred__set_2Ecount@(inj__ty_2Enum_2Enum @ V1n))))@V0A)))))))).
thf(conj_thm_2Ecardinal_2EINFINITE__Unum,lemma,( ! [A_27a:del]: ( ! [V0A:$i] : ((mem@V0A@(arr@A_27a@bool)) => ((~~ (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0A))) <=> (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@ty_2Enum_2Enum@A_27a)@(c_2Epred__set_2EUNIV@ty_2Enum_2Enum))@V0A))))))).
thf(conj_thm_2Ecardinal_2Ecardleq__SURJ,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0A:$i] : ((mem@V0A@(arr@A_27a@bool)) => ( ! [V1B:$i] : ((mem@V1B@(arr@A_27b@bool)) => ((p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27a@A_27b)@V0A)@V1B)) <=> ((? [V2f:$i] : ((mem@V2f@(arr@A_27b@A_27a)) & (p@(ap@(ap@(ap@(c_2Epred__set_2ESURJ@A_27b@A_27a)@V2f)@V1B)@V0A)))) | (V0A = (c_2Epred__set_2EEMPTY@A_27a))))))))))).
thf(conj_thm_2Ecardinal_2EINFINITE__cardleq__INSERT,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0A:$i] : ((mem@V0A@(arr@A_27a@bool)) => ( ! [V1x:$i] : ((mem@V1x@A_27b) => ( ! [V2s:$i] : ((mem@V2s@(arr@A_27b@bool)) => ((~~ (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0A))) => ((p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27b@A_27a)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27b)@V1x)@V2s))@V0A)) <=> (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27b@A_27a)@V2s)@V0A))))))))))))).
thf(ax_thm_2Ecardinal_2Elist__def,axiom,( ! [A_27a:del]: ( ! [V0A:$i] : ((mem@V0A@(arr@A_27a@bool)) => ((ap@(c_2Ecardinal_2Elist@A_27a)@V0A) = (ap@(c_2Epred__set_2EGSPEC@(ty_2Elist_2Elist@A_27a)@(ty_2Elist_2Elist@A_27a))@(lam@(ty_2Elist_2Elist@A_27a)@(^ [V1l:$i] : (ap@(ap@(c_2Epair_2E_2C@(ty_2Elist_2Elist@A_27a)@bool)@V1l)@(ap@(c_2Ebool_2E_21@A_27a)@(lam@A_27a@(^ [V2e:$i] : (ap@(ap@c_2Emin_2E_3D_3D_3E@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2e)@(ap@(c_2Elist_2ELIST__TO__SET@A_27a)@V1l)))@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2e)@V0A)))))))))))))).
thf(conj_thm_2Ecardinal_2Elist__EMPTY,lemma,( ! [A_27a:del]: ((ap@(c_2Ecardinal_2Elist@A_27a)@(c_2Epred__set_2EEMPTY@A_27a)) = (ap@(ap@(c_2Epred__set_2EINSERT@(ty_2Elist_2Elist@A_27a))@(c_2Elist_2ENIL@A_27a))@(c_2Epred__set_2EEMPTY@(ty_2Elist_2Elist@A_27a)))))).
thf(conj_thm_2Ecardinal_2Elist__SING,lemma,( ! [A_27a:del]: ( ! [V0e:$i] : ((mem@V0e@A_27a) => (p@(ap@(ap@(c_2Ecardinal_2Ecardeq@(ty_2Elist_2Elist@A_27a)@ty_2Enum_2Enum)@(ap@(c_2Ecardinal_2Elist@A_27a)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V0e)@(c_2Epred__set_2EEMPTY@A_27a))))@(c_2Epred__set_2EUNIV@ty_2Enum_2Enum))))))).
thf(conj_thm_2Ecardinal_2EUNIV__list,lemma,( ! [A_27a:del]: ((c_2Epred__set_2EUNIV@(ty_2Elist_2Elist@A_27a)) = (ap@(c_2Ecardinal_2Elist@A_27a)@(c_2Epred__set_2EUNIV@A_27a))))).
thf(conj_thm_2Ecardinal_2Elist__BIGUNION__EXP,lemma,( ! [A_27a:del]: ( ! [V0A:$i] : ((mem@V0A@(arr@A_27a@bool)) => (p@(ap@(ap@(c_2Ecardinal_2Ecardeq@(ty_2Elist_2Elist@A_27a)@(arr@ty_2Enum_2Enum@(ty_2Eoption_2Eoption@A_27a)))@(ap@(c_2Ecardinal_2Elist@A_27a)@V0A))@(ap@(c_2Epred__set_2EBIGUNION@(arr@ty_2Enum_2Enum@(ty_2Eoption_2Eoption@A_27a)))@(ap@(ap@(c_2Epred__set_2EIMAGE@ty_2Enum_2Enum@(arr@(arr@ty_2Enum_2Enum@(ty_2Eoption_2Eoption@A_27a))@bool))@(lam@ty_2Enum_2Enum@(^ [V1n:$i] : (ap@(ap@(c_2Ecardinal_2Eset__exp@ty_2Enum_2Enum@A_27a)@V0A)@(ap@c_2Epred__set_2Ecount@V1n)))))@(c_2Epred__set_2EUNIV@ty_2Enum_2Enum))))))))).
thf(conj_thm_2Ecardinal_2EINFINITE__A__list__BIJ__A,lemma,( ! [A_27a:del]: ( ! [V0A:$i] : ((mem@V0A@(arr@A_27a@bool)) => ((~~ (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0A))) => (p@(ap@(ap@(c_2Ecardinal_2Ecardeq@(ty_2Elist_2Elist@A_27a)@A_27a)@(ap@(c_2Ecardinal_2Elist@A_27a)@V0A))@V0A))))))).
thf(conj_thm_2Ecardinal_2Efinite__subsets__bijection,lemma,( ! [A_27a:del]: ( ! [V0A:$i] : ((mem@V0A@(arr@A_27a@bool)) => ((~~ (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0A))) => (p@(ap@(ap@(c_2Ecardinal_2Ecardeq@A_27a@(arr@A_27a@bool))@V0A)@(ap@(c_2Epred__set_2EGSPEC@(arr@A_27a@bool)@(arr@A_27a@bool))@(lam@(arr@A_27a@bool)@(^ [V1s:$i] : (ap@(ap@(c_2Epair_2E_2C@(arr@A_27a@bool)@bool)@V1s)@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1s))@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V1s)@V0A))))))))))))).
thf(conj_thm_2Ecardinal_2EFINITE__IMAGE__INJ_27,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27a@A_27b)) => (( ! [V2x:$i] : ((mem@V2x@A_27a) => ( ! [V3y:$i] : ((mem@V3y@A_27a) => (((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V0s)) & (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3y)@V0s))) => (((ap@V1f@V2x) = (ap@V1f@V3y)) <=> (V2x = V3y))))))) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27b)@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V1f)@V0s))) <=> (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s))))))))))).
thf(conj_thm_2Ecardinal_2Ecountable__decomposition,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((~~ (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s))) => (? [V1A:$i] : ((mem@V1A@(arr@(arr@A_27a@bool)@bool)) & (((ap@(c_2Epred__set_2EBIGUNION@A_27a)@V1A) = V0s) & ( ! [V2a:$i] : ((mem@V2a@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@bool))@V2a)@V1A)) => ((~~ (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V2a))) & (p@(ap@(c_2Epred__set_2Ecountable@A_27a)@V2a)))))))))))))).
thf(conj_thm_2Ecardinal_2Edisjoint__countable__decomposition,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((~~ (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s))) => (? [V1A:$i] : ((mem@V1A@(arr@(arr@A_27a@bool)@bool)) & (((ap@(c_2Epred__set_2EBIGUNION@A_27a)@V1A) = V0s) & (( ! [V2a:$i] : ((mem@V2a@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@bool))@V2a)@V1A)) => ((~~ (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V2a))) & (p@(ap@(c_2Epred__set_2Ecountable@A_27a)@V2a)))))) & ( ! [V3a1:$i] : ((mem@V3a1@(arr@A_27a@bool)) => ( ! [V4a2:$i] : ((mem@V4a2@(arr@A_27a@bool)) => (((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@bool))@V3a1)@V1A)) & ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@bool))@V4a2)@V1A)) & (~~ (V3a1 = V4a2)))) => (p@(ap@(ap@(c_2Epred__set_2EDISJOINT@A_27a)@V3a1)@V4a2)))))))))))))))).
thf(conj_thm_2Ecardinal_2Ecount__cardle,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1A:$i] : ((mem@V1A@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Ecardinal_2Ecardleq@ty_2Enum_2Enum@A_27a)@(ap@c_2Epred__set_2Ecount@(inj__ty_2Enum_2Enum @ V0n)))@V1A)) <=> ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1A)) => (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0n))@(ap@(c_2Epred__set_2ECARD@A_27a)@V1A)))))))))).
thf(conj_thm_2Ecardinal_2ECANTOR,lemma,( ! [A_27a:del]: ( ! [V0A:$i] : ((mem@V0A@(arr@A_27a@bool)) => (~~ (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@(arr@A_27a@bool)@A_27a)@(ap@(c_2Epred__set_2EPOW@A_27a)@V0A))@V0A))))))).
thf(conj_thm_2Ecardinal_2Ecardlt__cardle,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0B:$i] : ((mem@V0B@(arr@A_27b@bool)) => ( ! [V1A:$i] : ((mem@V1A@(arr@A_27a@bool)) => ((~~ (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27b@A_27a)@V0B)@V1A))) => (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27a@A_27b)@V1A)@V0B)))))))))).
thf(conj_thm_2Ecardinal_2Eset__exp__product,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0A:$i] : ((mem@V0A@(arr@A_27c@bool)) => ( ! [V1B1:$i] : ((mem@V1B1@(arr@A_27b@bool)) => ( ! [V2B2:$i] : ((mem@V2B2@(arr@A_27a@bool)) => (p@(ap@(ap@(c_2Ecardinal_2Ecardeq@(arr@A_27a@(ty_2Eoption_2Eoption@(arr@A_27b@(ty_2Eoption_2Eoption@A_27c))))@(arr@(ty_2Epair_2Eprod@A_27b@A_27a)@(ty_2Eoption_2Eoption@A_27c)))@(ap@(ap@(c_2Ecardinal_2Eset__exp@A_27a@(arr@A_27b@(ty_2Eoption_2Eoption@A_27c)))@(ap@(ap@(c_2Ecardinal_2Eset__exp@A_27b@A_27c)@V0A)@V1B1))@V2B2))@(ap@(ap@(c_2Ecardinal_2Eset__exp@(ty_2Epair_2Eprod@A_27b@A_27a)@A_27c)@V0A)@(ap@(ap@(c_2Epred__set_2ECROSS@A_27b@A_27a)@V1B1)@V2B2)))))))))))))).
thf(conj_thm_2Ecardinal_2ECOUNT__EQ__EMPTY,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : (((ap@c_2Epred__set_2Ecount@(inj__ty_2Enum_2Enum @ V0n)) = (c_2Epred__set_2EEMPTY@ty_2Enum_2Enum)) <=> (V0n = fo__c_2Enum_2E0)))).
thf(conj_thm_2Ecardinal_2EPOW__EQ__X__EXP__X,lemma,( ! [A_27a:del]: ( ! [V0A:$i] : ((mem@V0A@(arr@A_27a@bool)) => ((~~ (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0A))) => (p@(ap@(ap@(c_2Ecardinal_2Ecardeq@(arr@A_27a@bool)@(arr@A_27a@(ty_2Eoption_2Eoption@A_27a)))@(ap@(c_2Epred__set_2EPOW@A_27a)@V0A))@(ap@(ap@(c_2Ecardinal_2Eset__exp@A_27a@A_27a)@V0A)@V0A)))))))).
thf(ax_thm_2Ecardinal_2Ebijns__def,axiom,( ! [A_27a:del]: ( ! [V0A:$i] : ((mem@V0A@(arr@A_27a@bool)) => ((ap@(c_2Ecardinal_2Ebijns@A_27a)@V0A) = (ap@(c_2Epred__set_2EGSPEC@(arr@A_27a@(ty_2Eoption_2Eoption@A_27a))@(arr@A_27a@(ty_2Eoption_2Eoption@A_27a)))@(lam@(arr@A_27a@(ty_2Eoption_2Eoption@A_27a))@(^ [V1f:$i] : (ap@(ap@(c_2Epair_2E_2C@(arr@A_27a@(ty_2Eoption_2Eoption@A_27a))@bool)@V1f)@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(ap@(c_2Epred__set_2EBIJ@A_27a@A_27a)@(ap@(ap@(c_2Ecombin_2Eo@A_27a@A_27a@(ty_2Eoption_2Eoption@A_27a))@(c_2Eoption_2ETHE@A_27a))@V1f))@V0A)@V0A))@(ap@(c_2Ebool_2E_21@A_27a)@(lam@A_27a@(^ [V2a:$i] : (ap@(ap@(c_2Emin_2E_3D@bool)@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2a)@V0A))@(ap@(c_2Ebool_2E_3F@A_27a)@(lam@A_27a@(^ [V3b:$i] : (ap@(ap@(c_2Emin_2E_3D@(ty_2Eoption_2Eoption@A_27a))@(ap@V1f@V2a))@(ap@(c_2Eoption_2ESOME@A_27a)@V3b))))))))))))))))))).
thf(conj_thm_2Ecardinal_2Ecardeq__bijns__cong,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0A:$i] : ((mem@V0A@(arr@A_27a@bool)) => ( ! [V1B:$i] : ((mem@V1B@(arr@A_27b@bool)) => ((p@(ap@(ap@(c_2Ecardinal_2Ecardeq@A_27a@A_27b)@V0A)@V1B)) => (p@(ap@(ap@(c_2Ecardinal_2Ecardeq@(arr@A_27a@(ty_2Eoption_2Eoption@A_27a))@(arr@A_27b@(ty_2Eoption_2Eoption@A_27b)))@(ap@(c_2Ecardinal_2Ebijns@A_27a)@V0A))@(ap@(c_2Ecardinal_2Ebijns@A_27b)@V1B))))))))))).
thf(conj_thm_2Ecardinal_2Ebijections__cardeq,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((~~ (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s))) => (p@(ap@(ap@(c_2Ecardinal_2Ecardeq@(arr@A_27a@(ty_2Eoption_2Eoption@A_27a))@(arr@A_27a@bool))@(ap@(c_2Ecardinal_2Ebijns@A_27a)@V0s))@(ap@(c_2Epred__set_2EPOW@A_27a)@V0s)))))))).
thf(conj_thm_2Ecardinal_2ELEFT__IMP__EXISTS__THM,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1Q:$i] : ((mem@V1Q@bool) => (((? [V2x:$i] : ((mem@V2x@A_27a) & (p@(ap@V0P@V2x)))) => (p@V1Q)) <=> ( ! [V3x:$i] : ((mem@V3x@A_27a) => ((p@(ap@V0P@V3x)) => (p@V1Q))))))))))).
thf(conj_thm_2Ecardinal_2ELEFT__IMP__FORALL__THM,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1Q:$i] : ((mem@V1Q@bool) => ((( ! [V2x:$i] : ((mem@V2x@A_27a) => (p@(ap@V0P@V2x)))) => (p@V1Q)) <=> (? [V3x:$i] : ((mem@V3x@A_27a) & ((p@(ap@V0P@V3x)) => (p@V1Q))))))))))).
thf(conj_thm_2Ecardinal_2ERIGHT__IMP__EXISTS__THM,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@bool) => ( ! [V1Q:$i] : ((mem@V1Q@(arr@A_27a@bool)) => (((p@V0P) => (? [V2x:$i] : ((mem@V2x@A_27a) & (p@(ap@V1Q@V2x))))) <=> (? [V3x:$i] : ((mem@V3x@A_27a) & ((p@V0P) => (p@(ap@V1Q@V3x)))))))))))).
thf(conj_thm_2Ecardinal_2ERIGHT__IMP__FORALL__THM,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@bool) => ( ! [V1Q:$i] : ((mem@V1Q@(arr@A_27a@bool)) => (((p@V0P) => ( ! [V2x:$i] : ((mem@V2x@A_27a) => (p@(ap@V1Q@V2x))))) <=> ( ! [V3x:$i] : ((mem@V3x@A_27a) => ((p@V0P) => (p@(ap@V1Q@V3x)))))))))))).
thf(conj_thm_2Ecardinal_2EFINITE__FINITE__BIGUNIONS,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@(arr@A_27a@bool)@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@(arr@A_27a@bool))@V0s)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@(ap@(c_2Epred__set_2EBIGUNION@A_27a)@V0s))) <=> ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@bool))@V1t)@V0s)) => (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1t))))))))))).
thf(conj_thm_2Ecardinal_2ECONJ__EQ__IMP,lemma,( ! [V0r:$i] : ((mem@V0r@bool) => ( ! [V1p:$i] : ((mem@V1p@bool) => ( ! [V2q:$i] : ((mem@V2q@bool) => ((((p@V1p) & (p@V2q)) => (p@V0r)) <=> ((p@V1p) => ((p@V2q) => (p@V0r))))))))))).
thf(conj_thm_2Ecardinal_2EIMP__CONJ__ALT,lemma,( ! [V0r:$i] : ((mem@V0r@bool) => ( ! [V1p:$i] : ((mem@V1p@bool) => ( ! [V2q:$i] : ((mem@V2q@bool) => ((((p@V1p) & (p@V2q)) => (p@V0r)) <=> ((p@V2q) => ((p@V1p) => (p@V0r))))))))))).
thf(conj_thm_2Ecardinal_2ELT__SUC__LE,lemma,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0m))@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n)))) <=> (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V1n))))))).
thf(conj_thm_2Ecardinal_2ESURJECTIVE__ON__RIGHT__INVERSE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27a@A_27b)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27b@bool)) => (( ! [V3y:$i] : ((mem@V3y@A_27b) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V3y)@V2t)) => (? [V4x:$i] : ((mem@V4x@A_27a) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V4x)@V0s)) & ((ap@V1f@V4x) = V3y))))))) <=> (? [V5g:$i] : ((mem@V5g@(arr@A_27b@A_27a)) & ( ! [V6y:$i] : ((mem@V6y@A_27b) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V6y)@V2t)) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@(ap@V5g@V6y))@V0s)) & ((ap@V1f@(ap@V5g@V6y)) = V6y))))))))))))))))).
thf(conj_thm_2Ecardinal_2ESURJECTIVE__RIGHT__INVERSE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27b@A_27a)) => (( ! [V1y:$i] : ((mem@V1y@A_27a) => (? [V2x:$i] : ((mem@V2x@A_27b) & ((ap@V0f@V2x) = V1y))))) <=> (? [V3g:$i] : ((mem@V3g@(arr@A_27a@A_27b)) & ( ! [V4y:$i] : ((mem@V4y@A_27a) => ((ap@V0f@(ap@V3g@V4y)) = V4y))))))))))).
thf(conj_thm_2Ecardinal_2EFINITE__IMAGE__INJ__GENERAL,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1A:$i] : ((mem@V1A@(arr@A_27b@bool)) => ( ! [V2s:$i] : ((mem@V2s@(arr@A_27a@bool)) => ((( ! [V3x:$i] : ((mem@V3x@A_27a) => ( ! [V4y:$i] : ((mem@V4y@A_27a) => (((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@V2s)) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V4y)@V2s)) & ((ap@V0f@V3x) = (ap@V0f@V4y)))) => (V3x = V4y)))))) & (p@(ap@(c_2Epred__set_2EFINITE@A_27b)@V1A))) => (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@(ap@(c_2Epred__set_2EGSPEC@A_27a@A_27a)@(lam@A_27a@(^ [V5x:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27a@bool)@V5x)@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V5x)@V2s))@(ap@(ap@(c_2Ebool_2EIN@A_27b)@(ap@V0f@V5x))@V1A)))))))))))))))))).
thf(conj_thm_2Ecardinal_2EFINITE__IMAGE__INJ,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1A:$i] : ((mem@V1A@(arr@A_27b@bool)) => ((( ! [V2x:$i] : ((mem@V2x@A_27a) => ( ! [V3y:$i] : ((mem@V3y@A_27a) => (((ap@V0f@V2x) = (ap@V0f@V3y)) => (V2x = V3y)))))) & (p@(ap@(c_2Epred__set_2EFINITE@A_27b)@V1A))) => (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@(ap@(c_2Epred__set_2EGSPEC@A_27a@A_27a)@(lam@A_27a@(^ [V4x:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27a@bool)@V4x)@(ap@(ap@(c_2Ebool_2EIN@A_27b)@(ap@V0f@V4x))@V1A))))))))))))))).
thf(conj_thm_2Ecardinal_2EFINITE__IMAGE__INJ__EQ,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => (( ! [V2x:$i] : ((mem@V2x@A_27a) => ( ! [V3y:$i] : ((mem@V3y@A_27a) => (((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V1s)) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3y)@V1s)) & ((ap@V0f@V2x) = (ap@V0f@V3y)))) => (V2x = V3y)))))) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27b)@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@V1s))) <=> (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1s))))))))))).
thf(conj_thm_2Ecardinal_2EINFINITE__IMAGE__INJ,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => (( ! [V1x:$i] : ((mem@V1x@A_27a) => ( ! [V2y:$i] : ((mem@V2y@A_27a) => (((ap@V0f@V1x) = (ap@V0f@V2y)) => (V1x = V2y)))))) => ( ! [V3s:$i] : ((mem@V3s@(arr@A_27a@bool)) => ((~~ (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V3s))) => (~~ (p@(ap@(c_2Epred__set_2EFINITE@A_27b)@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@V3s))))))))))))).
thf(conj_thm_2Ecardinal_2EINFINITE__NONEMPTY,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((~~ (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s))) => (~~ (V0s = (c_2Epred__set_2EEMPTY@A_27a)))))))).
thf(conj_thm_2Ecardinal_2EFINITE__PRODUCT__DEPENDENT,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@(arr@A_27b@A_27c))) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27a@(arr@A_27b@bool))) => (((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1s)) & ( ! [V3x:$i] : ((mem@V3x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@V1s)) => (p@(ap@(c_2Epred__set_2EFINITE@A_27b)@(ap@V2t@V3x))))))) => (p@(ap@(c_2Epred__set_2EFINITE@A_27c)@(ap@(c_2Epred__set_2EGSPEC@A_27c@(ty_2Epair_2Eprod@A_27a@A_27b))@(ap@(c_2Epair_2EUNCURRY@A_27a@A_27b@(ty_2Epair_2Eprod@A_27c@bool))@(lam@A_27a@(^ [V4x:$i] : (lam@A_27b@(^ [V5y:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27c@bool)@(ap@(ap@V0f@V4x)@V5y))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V4x)@V1s))@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V5y)@(ap@V2t@V4x))))))))))))))))))))))).
thf(conj_thm_2Ecardinal_2EFINITE__PRODUCT,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => (((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s)) & (p@(ap@(c_2Epred__set_2EFINITE@A_27b)@V1t))) => (p@(ap@(c_2Epred__set_2EFINITE@(ty_2Epair_2Eprod@A_27a@A_27b))@(ap@(c_2Epred__set_2EGSPEC@(ty_2Epair_2Eprod@A_27a@A_27b)@(ty_2Epair_2Eprod@A_27a@A_27b))@(ap@(c_2Epair_2EUNCURRY@A_27a@A_27b@(ty_2Epair_2Eprod@(ty_2Epair_2Eprod@A_27a@A_27b)@bool))@(lam@A_27a@(^ [V2x:$i] : (lam@A_27b@(^ [V3y:$i] : (ap@(ap@(c_2Epair_2E_2C@(ty_2Epair_2Eprod@A_27a@A_27b)@bool)@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V2x)@V3y))@(ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V0s))@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V3y)@V1t))))))))))))))))))).
thf(conj_thm_2Ecardinal_2ESURJECTIVE__IMAGE__THM,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => (( ! [V1y:$i] : ((mem@V1y@A_27b) => (? [V2x:$i] : ((mem@V2x@A_27a) & ((ap@V0f@V2x) = V1y))))) <=> ( ! [V3P:$i] : ((mem@V3P@(arr@A_27b@bool)) => ((ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@(ap@(c_2Epred__set_2EGSPEC@A_27a@A_27a)@(lam@A_27a@(^ [V4x:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27a@bool)@V4x)@(ap@V3P@(ap@V0f@V4x))))))) = (ap@(c_2Epred__set_2EGSPEC@A_27b@A_27b)@(lam@A_27b@(^ [V5x:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27b@bool)@V5x)@(ap@V3P@V5x)))))))))))))).
thf(conj_thm_2Ecardinal_2ESURJECTIVE__ON__IMAGE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1u:$i] : ((mem@V1u@(arr@A_27a@bool)) => ( ! [V2v:$i] : ((mem@V2v@(arr@A_27b@bool)) => (( ! [V3t:$i] : ((mem@V3t@(arr@A_27b@bool)) => ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27b)@V3t)@V2v)) => (? [V4s:$i] : ((mem@V4s@(arr@A_27a@bool)) & ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V4s)@V1u)) & ((ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@V4s) = V3t))))))) <=> ( ! [V5y:$i] : ((mem@V5y@A_27b) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V5y)@V2v)) => (? [V6x:$i] : ((mem@V6x@A_27a) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V6x)@V1u)) & ((ap@V0f@V6x) = V5y))))))))))))))))).
thf(conj_thm_2Ecardinal_2ESURJECTIVE__IMAGE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => (( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => (? [V2s:$i] : ((mem@V2s@(arr@A_27a@bool)) & ((ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@V2s) = V1t))))) <=> ( ! [V3y:$i] : ((mem@V3y@A_27b) => (? [V4x:$i] : ((mem@V4x@A_27a) & ((ap@V0f@V4x) = V3y))))))))))).
thf(conj_thm_2Ecardinal_2ECARD__LE__INJ,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => (((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s)) & ((p@(ap@(c_2Epred__set_2EFINITE@A_27b)@V1t)) & (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(c_2Epred__set_2ECARD@A_27a)@V0s))@(ap@(c_2Epred__set_2ECARD@A_27b)@V1t))))) => (? [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27b)) & ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27b)@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V2f)@V0s))@V1t)) & ( ! [V3x:$i] : ((mem@V3x@A_27a) => ( ! [V4y:$i] : ((mem@V4y@A_27a) => (((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@V0s)) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V4y)@V0s)) & ((ap@V2f@V3x) = (ap@V2f@V4y)))) => (V3x = V4y))))))))))))))))).
thf(conj_thm_2Ecardinal_2ECARD__IMAGE__INJ,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ((( ! [V2x:$i] : ((mem@V2x@A_27a) => ( ! [V3y:$i] : ((mem@V3y@A_27a) => (((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V1s)) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3y)@V1s)) & ((ap@V0f@V2x) = (ap@V0f@V3y)))) => (V2x = V3y)))))) & (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1s))) => ((surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27b)@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@V1s))) = (surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27a)@V1s))))))))))).
thf(conj_thm_2Ecardinal_2ECARD__IMAGE__LE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1s)) => (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(c_2Epred__set_2ECARD@A_27b)@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@V1s)))@(ap@(c_2Epred__set_2ECARD@A_27a)@V1s))))))))))).
thf(conj_thm_2Ecardinal_2ESURJECTIVE__IFF__INJECTIVE__GEN,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => ( ! [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27b)) => (((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s)) & ((p@(ap@(c_2Epred__set_2EFINITE@A_27b)@V1t)) & (((surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27a)@V0s)) = (surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27b)@V1t))) & (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27b)@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V2f)@V0s))@V1t))))) => (( ! [V3y:$i] : ((mem@V3y@A_27b) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V3y)@V1t)) => (? [V4x:$i] : ((mem@V4x@A_27a) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V4x)@V0s)) & ((ap@V2f@V4x) = V3y))))))) <=> ( ! [V5x:$i] : ((mem@V5x@A_27a) => ( ! [V6y:$i] : ((mem@V6y@A_27a) => (((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V5x)@V0s)) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V6y)@V0s)) & ((ap@V2f@V5x) = (ap@V2f@V6y)))) => (V5x = V6y))))))))))))))))).
thf(conj_thm_2Ecardinal_2ESURJECTIVE__IFF__INJECTIVE,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1f:$i] : ((mem@V1f@(arr@A_27a@A_27a)) => (((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s)) & (p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@(ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27a)@V1f)@V0s))@V0s))) => (( ! [V2y:$i] : ((mem@V2y@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2y)@V0s)) => (? [V3x:$i] : ((mem@V3x@A_27a) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@V0s)) & ((ap@V1f@V3x) = V2y))))))) <=> ( ! [V4x:$i] : ((mem@V4x@A_27a) => ( ! [V5y:$i] : ((mem@V5y@A_27a) => (((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V4x)@V0s)) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V5y)@V0s)) & ((ap@V1f@V4x) = (ap@V1f@V5y)))) => (V4x = V5y)))))))))))))).
thf(conj_thm_2Ecardinal_2ECARD__EQ__BIJECTION,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => (((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s)) & ((p@(ap@(c_2Epred__set_2EFINITE@A_27b)@V1t)) & ((surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27a)@V0s)) = (surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27b)@V1t))))) => (? [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27b)) & (( ! [V3x:$i] : ((mem@V3x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@V0s)) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@(ap@V2f@V3x))@V1t))))) & (( ! [V4y:$i] : ((mem@V4y@A_27b) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V4y)@V1t)) => (? [V5x:$i] : ((mem@V5x@A_27a) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V5x)@V0s)) & ((ap@V2f@V5x) = V4y))))))) & ( ! [V6x:$i] : ((mem@V6x@A_27a) => ( ! [V7y:$i] : ((mem@V7y@A_27a) => (((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V6x)@V0s)) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V7y)@V0s)) & ((ap@V2f@V6x) = (ap@V2f@V7y)))) => (V6x = V7y)))))))))))))))))).
thf(conj_thm_2Ecardinal_2ECARD__EQ__BIJECTIONS,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => (((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s)) & ((p@(ap@(c_2Epred__set_2EFINITE@A_27b)@V1t)) & ((surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27a)@V0s)) = (surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27b)@V1t))))) => (? [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27b)) & (? [V3g:$i] : ((mem@V3g@(arr@A_27b@A_27a)) & (( ! [V4x:$i] : ((mem@V4x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V4x)@V0s)) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@(ap@V2f@V4x))@V1t)) & ((ap@V3g@(ap@V2f@V4x)) = V4x))))) & ( ! [V5y:$i] : ((mem@V5y@A_27b) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V5y)@V1t)) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@(ap@V3g@V5y))@V0s)) & ((ap@V2f@(ap@V3g@V5y)) = V5y)))))))))))))))))).
thf(conj_thm_2Ecardinal_2ESING__SUBSET,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1x:$i] : ((mem@V1x@A_27a) => ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@(ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V1x)@(c_2Epred__set_2EEMPTY@A_27a)))@V0s)) <=> (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V1x)@V0s))))))))).
thf(conj_thm_2Ecardinal_2EINJECTIVE__ON__IMAGE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1u:$i] : ((mem@V1u@(arr@A_27a@bool)) => (( ! [V2s:$i] : ((mem@V2s@(arr@A_27a@bool)) => ( ! [V3t:$i] : ((mem@V3t@(arr@A_27a@bool)) => (((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V2s)@V1u)) & ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V3t)@V1u)) & ((ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@V2s) = (ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@V3t)))) => (V2s = V3t)))))) <=> ( ! [V4x:$i] : ((mem@V4x@A_27a) => ( ! [V5y:$i] : ((mem@V5y@A_27a) => (((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V4x)@V1u)) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V5y)@V1u)) & ((ap@V0f@V4x) = (ap@V0f@V5y)))) => (V4x = V5y)))))))))))))).
thf(conj_thm_2Ecardinal_2EINJECTIVE__IMAGE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => (( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27a@bool)) => (((ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@V1s) = (ap@(ap@(c_2Epred__set_2EIMAGE@A_27a@A_27b)@V0f)@V2t)) => (V1s = V2t)))))) <=> ( ! [V3x:$i] : ((mem@V3x@A_27a) => ( ! [V4y:$i] : ((mem@V4y@A_27a) => (((ap@V0f@V3x) = (ap@V0f@V4y)) => (V3x = V4y)))))))))))).
thf(conj_thm_2Ecardinal_2EFINITE__FINITE__BIGUNION,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@(arr@A_27a@bool)@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@(arr@A_27a@bool))@V0s)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@(ap@(c_2Epred__set_2EBIGUNION@A_27a)@V0s))) <=> ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Ebool_2EIN@(arr@A_27a@bool))@V1t)@V0s)) => (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1t))))))))))).
thf(conj_thm_2Ecardinal_2Enum__FINITE,lemma,( ! [V0s:$i] : ((mem@V0s@(arr@ty_2Enum_2Enum@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@ty_2Enum_2Enum)@V0s)) <=> (? [V1a:tp__ty_2Enum_2Enum] : ( ! [V2x:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@(c_2Ebool_2EIN@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V2x))@V0s)) => (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V2x))@(inj__ty_2Enum_2Enum @ V1a)))))))))).
thf(conj_thm_2Ecardinal_2Enum__FINITE__AVOID,lemma,( ! [V0s:$i] : ((mem@V0s@(arr@ty_2Enum_2Enum@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@ty_2Enum_2Enum)@V0s)) => (? [V1a:tp__ty_2Enum_2Enum] : (~~ (p@(ap@(ap@(c_2Ebool_2EIN@ty_2Enum_2Enum)@(inj__ty_2Enum_2Enum @ V1a))@V0s)))))))).
thf(conj_thm_2Ecardinal_2Enum__INFINITE,lemma,(~~ (p@(ap@(c_2Epred__set_2EFINITE@ty_2Enum_2Enum)@(c_2Epred__set_2EUNIV@ty_2Enum_2Enum))))).
thf(ax_thm_2Ecardinal_2EHAS__SIZE,axiom,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@(c_2Ecardinal_2EHAS__SIZE@A_27a)@V0s)@(inj__ty_2Enum_2Enum @ V1n))) <=> ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s)) & ((surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27a)@V0s)) = V1n)))))))).
thf(conj_thm_2Ecardinal_2EHAS__SIZE__CARD,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@(c_2Ecardinal_2EHAS__SIZE@A_27a)@V0s)@(inj__ty_2Enum_2Enum @ V1n))) => ((surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27a)@V0s)) = V1n))))))).
thf(conj_thm_2Ecardinal_2EHAS__SIZE__0,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Ecardinal_2EHAS__SIZE@A_27a)@V0s)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) <=> (V0s = (c_2Epred__set_2EEMPTY@A_27a))))))).
thf(conj_thm_2Ecardinal_2EHAS__SIZE__SUC,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@(c_2Ecardinal_2EHAS__SIZE@A_27a)@V0s)@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V1n)))) <=> ((~~ (V0s = (c_2Epred__set_2EEMPTY@A_27a))) & ( ! [V2a:$i] : ((mem@V2a@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2a)@V0s)) => (p@(ap@(ap@(c_2Ecardinal_2EHAS__SIZE@A_27a)@(ap@(ap@(c_2Epred__set_2EDELETE@A_27a)@V0s)@V2a))@(inj__ty_2Enum_2Enum @ V1n))))))))))))).
thf(conj_thm_2Ecardinal_2EFINITE__HAS__SIZE,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s)) <=> (p@(ap@(ap@(c_2Ecardinal_2EHAS__SIZE@A_27a)@V0s)@(ap@(c_2Epred__set_2ECARD@A_27a)@V0s)))))))).
thf(conj_thm_2Ecardinal_2EHAS__SIZE__CLAUSES,lemma,( ! [A_27a:del]: ( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => (((p@(ap@(ap@(c_2Ecardinal_2EHAS__SIZE@A_27a)@V1s)@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) <=> (V1s = (c_2Epred__set_2EEMPTY@A_27a))) & ((p@(ap@(ap@(c_2Ecardinal_2EHAS__SIZE@A_27a)@V1s)@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V0n)))) <=> (? [V2a:$i] : ((mem@V2a@A_27a) & (? [V3t:$i] : ((mem@V3t@(arr@A_27a@bool)) & ((p@(ap@(ap@(c_2Ecardinal_2EHAS__SIZE@A_27a)@V3t)@(inj__ty_2Enum_2Enum @ V0n))) & ((~~ (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2a)@V3t))) & (V1s = (ap@(ap@(c_2Epred__set_2EINSERT@A_27a)@V2a)@V3t))))))))))))))).
thf(conj_thm_2Ecardinal_2ECARD__SUBSET__EQ,lemma,( ! [A_27a:del]: ( ! [V0a:$i] : ((mem@V0a@(arr@A_27a@bool)) => ( ! [V1b:$i] : ((mem@V1b@(arr@A_27a@bool)) => (((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1b)) & ((p@(ap@(ap@(c_2Epred__set_2ESUBSET@A_27a)@V0a)@V1b)) & ((surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27a)@V0a)) = (surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27a)@V1b))))) => (V0a = V1b)))))))).
thf(conj_thm_2Ecardinal_2EHAS__SIZE__INDEX,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@(c_2Ecardinal_2EHAS__SIZE@A_27a)@V0s)@(inj__ty_2Enum_2Enum @ V1n))) => (? [V2f:$i] : ((mem@V2f@(arr@ty_2Enum_2Enum@A_27a)) & (( ! [V3m:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V3m))@(inj__ty_2Enum_2Enum @ V1n))) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@(ap@V2f@(inj__ty_2Enum_2Enum @ V3m)))@V0s)))) & ( ! [V4x:$i] : ((mem@V4x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V4x)@V0s)) => (p@(ap@(c_2Ebool_2E_3F_21@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V5m:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@c_2Eprim__rec_2E_3C@V5m)@(inj__ty_2Enum_2Enum @ V1n)))@(ap@(ap@(c_2Emin_2E_3D@A_27a)@(ap@V2f@V5m))@V4x)))))))))))))))))).
thf(conj_thm_2Ecardinal_2ECARD__BIGUNION__LE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@(arr@A_27b@bool))) => ( ! [V2m:tp__ty_2Enum_2Enum] : ( ! [V3n:tp__ty_2Enum_2Enum] : (((p@(ap@(ap@(c_2Ecardinal_2EHAS__SIZE@A_27a)@V0s)@(inj__ty_2Enum_2Enum @ V2m))) & ( ! [V4x:$i] : ((mem@V4x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V4x)@V0s)) => ((p@(ap@(c_2Epred__set_2EFINITE@A_27b)@(ap@V1t@V4x))) & (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(c_2Epred__set_2ECARD@A_27b)@(ap@V1t@V4x)))@(inj__ty_2Enum_2Enum @ V3n)))))))) => (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@(c_2Epred__set_2ECARD@A_27b)@(ap@(c_2Epred__set_2EBIGUNION@A_27b)@(ap@(c_2Epred__set_2EGSPEC@(arr@A_27b@bool)@A_27a)@(lam@A_27a@(^ [V5x:$i] : (ap@(ap@(c_2Epair_2E_2C@(arr@A_27b@bool)@bool)@(ap@V1t@V5x))@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V5x)@V0s))))))))@(ap@(ap@c_2Earithmetic_2E_2A@(inj__ty_2Enum_2Enum @ V2m))@(inj__ty_2Enum_2Enum @ V3n)))))))))))))).
thf(conj_thm_2Ecardinal_2EHAS__SIZE__BOOL,lemma,(p@(ap@(ap@(c_2Ecardinal_2EHAS__SIZE@bool)@(c_2Epred__set_2EUNIV@bool))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))).
thf(conj_thm_2Ecardinal_2ECARD__BOOL,lemma,((surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@bool)@(c_2Epred__set_2EUNIV@bool))) = (surj__ty_2Enum_2Enum @ (ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT2@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))).
thf(conj_thm_2Ecardinal_2EFINITE__BOOL,lemma,(p@(ap@(c_2Epred__set_2EFINITE@bool)@(c_2Epred__set_2EUNIV@bool)))).
thf(conj_thm_2Ecardinal_2EHAS__SIZE__CART__UNIV,lemma,( ! [A_27a:del]: ( ! [V0m:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@(c_2Ecardinal_2EHAS__SIZE@A_27a)@(c_2Epred__set_2EUNIV@A_27a))@(inj__ty_2Enum_2Enum @ V0m))) => (p@(ap@(ap@(c_2Ecardinal_2EHAS__SIZE@A_27a)@(c_2Epred__set_2EUNIV@A_27a))@(ap@(ap@c_2Earithmetic_2EEXP@(inj__ty_2Enum_2Enum @ V0m))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))))).
thf(conj_thm_2Ecardinal_2ECARD__CART__UNIV,lemma,( ! [A_27a:del]: ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@(c_2Epred__set_2EUNIV@A_27a))) => ((surj__ty_2Enum_2Enum @ (ap@(c_2Epred__set_2ECARD@A_27a)@(c_2Epred__set_2EUNIV@A_27a))) = (surj__ty_2Enum_2Enum @ (ap@(ap@c_2Earithmetic_2EEXP@(ap@(c_2Epred__set_2ECARD@A_27a)@(c_2Epred__set_2EUNIV@A_27a)))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))))))).
thf(conj_thm_2Ecardinal_2EFINITE__CART__UNIV,lemma,( ! [A_27a:del]: ((p@(ap@(c_2Epred__set_2EFINITE@A_27a)@(c_2Epred__set_2EUNIV@A_27a))) => (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@(c_2Epred__set_2EUNIV@A_27a)))))).
thf(conj_thm_2Ecardinal_2EHAS__SIZE__NUMSEG__LT,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@(c_2Ecardinal_2EHAS__SIZE@ty_2Enum_2Enum)@(ap@(c_2Epred__set_2EGSPEC@ty_2Enum_2Enum@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V1m:$i] : (ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@bool)@V1m)@(ap@(ap@c_2Eprim__rec_2E_3C@V1m)@(inj__ty_2Enum_2Enum @ V0n)))))))@(inj__ty_2Enum_2Enum @ V0n))))).
thf(conj_thm_2Ecardinal_2EFINITE__NUMSEG__LT,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : (p@(ap@(c_2Epred__set_2EFINITE@ty_2Enum_2Enum)@(ap@(c_2Epred__set_2EGSPEC@ty_2Enum_2Enum@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V1m:$i] : (ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@bool)@V1m)@(ap@(ap@c_2Eprim__rec_2E_3C@V1m)@(inj__ty_2Enum_2Enum @ V0n)))))))))).
thf(conj_thm_2Ecardinal_2EHAS__SIZE__NUMSEG__LE,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : (p@(ap@(ap@(c_2Ecardinal_2EHAS__SIZE@ty_2Enum_2Enum)@(ap@(c_2Epred__set_2EGSPEC@ty_2Enum_2Enum@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V1m:$i] : (ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@bool)@V1m)@(ap@(ap@c_2Earithmetic_2E_3C_3D@V1m)@(inj__ty_2Enum_2Enum @ V0n)))))))@(ap@(ap@c_2Earithmetic_2E_2B@(inj__ty_2Enum_2Enum @ V0n))@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO)))))))).
thf(conj_thm_2Ecardinal_2EFINITE__NUMSEG__LE,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : (p@(ap@(c_2Epred__set_2EFINITE@ty_2Enum_2Enum)@(ap@(c_2Epred__set_2EGSPEC@ty_2Enum_2Enum@ty_2Enum_2Enum)@(lam@ty_2Enum_2Enum@(^ [V1m:$i] : (ap@(ap@(c_2Epair_2E_2C@ty_2Enum_2Enum@bool)@V1m)@(ap@(ap@c_2Earithmetic_2E_3C_3D@V1m)@(inj__ty_2Enum_2Enum @ V0n)))))))))).
thf(conj_thm_2Ecardinal_2EINFINITE__DIFF__FINITE,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27a@bool)) => (((~~ (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V0s))) & (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@V1t))) => (~~ (p@(ap@(c_2Epred__set_2EFINITE@A_27a)@(ap@(ap@(c_2Epred__set_2EDIFF@A_27a)@V0s)@V1t))))))))))).
thf(conj_thm_2Ecardinal_2ELE__CASES,lemma,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V1n))) | (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V1n))@(inj__ty_2Enum_2Enum @ V0m))))))).
thf(conj_thm_2Ecardinal_2ELT__CASES,lemma,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V1n))) | ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V1n))@(inj__ty_2Enum_2Enum @ V0m))) | (V0m = V1n)))))).
thf(conj_thm_2Ecardinal_2ELT,lemma,(( ! [V0m:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))) <=> $false)) & ( ! [V1m:tp__ty_2Enum_2Enum] : ( ! [V2n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V1m))@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V2n)))) <=> ((V1m = V2n) | (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V1m))@(inj__ty_2Enum_2Enum @ V2n))))))))).
thf(conj_thm_2Ecardinal_2ELT__LE,lemma,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V1n))) <=> ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V1n))) & (~~ (V0m = V1n))))))).
thf(conj_thm_2Ecardinal_2EGE,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ( ! [V1m:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3E_3D@(inj__ty_2Enum_2Enum @ V1m))@(inj__ty_2Enum_2Enum @ V0n))) <=> (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(inj__ty_2Enum_2Enum @ V0n))@(inj__ty_2Enum_2Enum @ V1m))))))).
thf(conj_thm_2Ecardinal_2ELE__SUC__LT,lemma,( ! [V0m:tp__ty_2Enum_2Enum] : ( ! [V1n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@c_2Enum_2ESUC@(inj__ty_2Enum_2Enum @ V0m)))@(inj__ty_2Enum_2Enum @ V1n))) <=> (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ V0m))@(inj__ty_2Enum_2Enum @ V1n))))))).
thf(conj_thm_2Ecardinal_2EINJECTIVE__ON__LEFT__INVERSE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => (( ! [V2x:$i] : ((mem@V2x@A_27a) => ( ! [V3y:$i] : ((mem@V3y@A_27a) => (((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V1s)) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3y)@V1s)) & ((ap@V0f@V2x) = (ap@V0f@V3y)))) => (V2x = V3y)))))) <=> (? [V4g:$i] : ((mem@V4g@(arr@A_27b@A_27a)) & ( ! [V5x:$i] : ((mem@V5x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V5x)@V1s)) => ((ap@V4g@(ap@V0f@V5x)) = V5x)))))))))))))).
thf(conj_thm_2Ecardinal_2EINJECTIVE__LEFT__INVERSE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => (( ! [V1x:$i] : ((mem@V1x@A_27a) => ( ! [V2y:$i] : ((mem@V2y@A_27a) => (((ap@V0f@V1x) = (ap@V0f@V2y)) => (V1x = V2y)))))) <=> (? [V3g:$i] : ((mem@V3g@(arr@A_27b@A_27a)) & ( ! [V4x:$i] : ((mem@V4x@A_27a) => ((ap@V3g@(ap@V0f@V4x)) = V4x))))))))))).
thf(conj_thm_2Ecardinal_2EINTER__ACI,lemma,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(arr@A_27a@bool)) => ( ! [V1p:$i] : ((mem@V1p@(arr@A_27a@bool)) => ( ! [V2q:$i] : ((mem@V2q@(arr@A_27a@bool)) => (((ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V1p)@V2q) = (ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V2q)@V1p)) & (((ap@(ap@(c_2Epred__set_2EINTER@A_27a)@(ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V1p)@V2q))@V0r) = (ap@(ap@(c_2Epred__set_2EINTER@A_27a)@(ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V1p)@V2q))@V0r)) & (((ap@(ap@(c_2Epred__set_2EINTER@A_27a)@(ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V1p)@V2q))@V0r) = (ap@(ap@(c_2Epred__set_2EINTER@A_27a)@(ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V2q)@V1p))@V0r)) & (((ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V1p)@V1p) = V1p) & ((ap@(ap@(c_2Epred__set_2EINTER@A_27a)@(ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V1p)@V1p))@V2q) = (ap@(ap@(c_2Epred__set_2EINTER@A_27a)@V1p)@V2q)))))))))))))).
thf(conj_thm_2Ecardinal_2ECONJ__ACI,lemma,( ! [V0r:$i] : ((mem@V0r@bool) => ( ! [V1p:$i] : ((mem@V1p@bool) => ( ! [V2q:$i] : ((mem@V2q@bool) => ((((p@V1p) & (p@V2q)) <=> ((p@V2q) & (p@V1p))) & (((((p@V1p) & (p@V2q)) & (p@V0r)) <=> ((p@V1p) & ((p@V2q) & (p@V0r)))) & ((((p@V1p) & ((p@V2q) & (p@V0r))) <=> ((p@V2q) & ((p@V1p) & (p@V0r)))) & ((((p@V1p) & (p@V1p)) <=> (p@V1p)) & (((p@V1p) & ((p@V1p) & (p@V2q))) <=> ((p@V1p) & (p@V2q)))))))))))))).
thf(conj_thm_2Ecardinal_2EUNION__ACI,lemma,( ! [A_27a:del]: ( ! [V0r:$i] : ((mem@V0r@(arr@A_27a@bool)) => ( ! [V1p:$i] : ((mem@V1p@(arr@A_27a@bool)) => ( ! [V2q:$i] : ((mem@V2q@(arr@A_27a@bool)) => (((ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V1p)@V2q) = (ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V2q)@V1p)) & (((ap@(ap@(c_2Epred__set_2EUNION@A_27a)@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V1p)@V2q))@V0r) = (ap@(ap@(c_2Epred__set_2EUNION@A_27a)@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V1p)@V2q))@V0r)) & (((ap@(ap@(c_2Epred__set_2EUNION@A_27a)@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V1p)@V2q))@V0r) = (ap@(ap@(c_2Epred__set_2EUNION@A_27a)@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V2q)@V1p))@V0r)) & (((ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V1p)@V1p) = V1p) & ((ap@(ap@(c_2Epred__set_2EUNION@A_27a)@(ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V1p)@V1p))@V2q) = (ap@(ap@(c_2Epred__set_2EUNION@A_27a)@V1p)@V2q)))))))))))))).
thf(conj_thm_2Ecardinal_2ELT__NZ,lemma,( ! [V0n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V0n))) <=> (~~ (V0n = fo__c_2Enum_2E0))))).
thf(conj_thm_2Ecardinal_2ELE__1,lemma,(( ! [V0n:tp__ty_2Enum_2Enum] : ((~~ (V0n = fo__c_2Enum_2E0)) => (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V0n))))) & (( ! [V1n:tp__ty_2Enum_2Enum] : ((~~ (V1n = fo__c_2Enum_2E0)) => (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V1n))))) & (( ! [V2n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V2n))) => (~~ (V2n = fo__c_2Enum_2E0)))) & (( ! [V3n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V3n))) => (p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V3n))))) & (( ! [V4n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V4n))) => (p@(ap@(ap@c_2Eprim__rec_2E_3C@(inj__ty_2Enum_2Enum @ fo__c_2Enum_2E0))@(inj__ty_2Enum_2Enum @ V4n))))) & ( ! [V5n:tp__ty_2Enum_2Enum] : ((p@(ap@(ap@c_2Earithmetic_2E_3C_3D@(ap@c_2Earithmetic_2ENUMERAL@(ap@c_2Earithmetic_2EBIT1@(inj__ty_2Enum_2Enum @ fo__c_2Earithmetic_2EZERO))))@(inj__ty_2Enum_2Enum @ V5n))) => (~~ (V5n = fo__c_2Enum_2E0)))))))))).
thf(conj_thm_2Ecardinal_2EOR__EXISTS__THM,lemma,( ! [A_27a:del]: ( ! [V0P:$i] : ((mem@V0P@(arr@A_27a@bool)) => ( ! [V1Q:$i] : ((mem@V1Q@(arr@A_27a@bool)) => (((? [V2x:$i] : ((mem@V2x@A_27a) & (p@(ap@V0P@V2x)))) | (? [V3x:$i] : ((mem@V3x@A_27a) & (p@(ap@V1Q@V3x))))) <=> (? [V4x:$i] : ((mem@V4x@A_27a) & ((p@(ap@V0P@V4x)) | (p@(ap@V1Q@V4x)))))))))))).
thf(conj_thm_2Ecardinal_2EBIJECTIVE__INJECTIVE__SURJECTIVE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27b@bool)) => ((( ! [V3x:$i] : ((mem@V3x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@V1s)) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@(ap@V0f@V3x))@V2t))))) & ( ! [V4y:$i] : ((mem@V4y@A_27b) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V4y)@V2t)) => (p@(ap@(c_2Ebool_2E_3F_21@A_27a)@(lam@A_27a@(^ [V5x:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V5x)@V1s))@(ap@(ap@(c_2Emin_2E_3D@A_27b)@(ap@V0f@V5x))@V4y)))))))))) <=> (( ! [V6x:$i] : ((mem@V6x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V6x)@V1s)) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@(ap@V0f@V6x))@V2t))))) & (( ! [V7x:$i] : ((mem@V7x@A_27a) => ( ! [V8y:$i] : ((mem@V8y@A_27a) => (((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V7x)@V1s)) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V8y)@V1s)) & ((ap@V0f@V7x) = (ap@V0f@V8y)))) => (V7x = V8y)))))) & ( ! [V9y:$i] : ((mem@V9y@A_27b) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V9y)@V2t)) => (? [V10x:$i] : ((mem@V10x@A_27a) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V10x)@V1s)) & ((ap@V0f@V10x) = V9y))))))))))))))))))).
thf(conj_thm_2Ecardinal_2EBIJECTIVE__INVERSES,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0f:$i] : ((mem@V0f@(arr@A_27a@A_27b)) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => ( ! [V2t:$i] : ((mem@V2t@(arr@A_27b@bool)) => ((( ! [V3x:$i] : ((mem@V3x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@V1s)) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@(ap@V0f@V3x))@V2t))))) & ( ! [V4y:$i] : ((mem@V4y@A_27b) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V4y)@V2t)) => (p@(ap@(c_2Ebool_2E_3F_21@A_27a)@(lam@A_27a@(^ [V5x:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V5x)@V1s))@(ap@(ap@(c_2Emin_2E_3D@A_27b)@(ap@V0f@V5x))@V4y)))))))))) <=> (( ! [V6x:$i] : ((mem@V6x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V6x)@V1s)) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@(ap@V0f@V6x))@V2t))))) & (? [V7g:$i] : ((mem@V7g@(arr@A_27b@A_27a)) & (( ! [V8y:$i] : ((mem@V8y@A_27b) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V8y)@V2t)) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@(ap@V7g@V8y))@V1s))))) & (( ! [V9y:$i] : ((mem@V9y@A_27b) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V9y)@V2t)) => ((ap@V0f@(ap@V7g@V9y)) = V9y)))) & ( ! [V10x:$i] : ((mem@V10x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V10x)@V1s)) => ((ap@V7g@(ap@V0f@V10x)) = V10x))))))))))))))))))).
thf(conj_thm_2Ecardinal_2Ele__c,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => ((p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27a@A_27b)@V0s)@V1t)) <=> (? [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27b)) & (( ! [V3x:$i] : ((mem@V3x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@V0s)) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@(ap@V2f@V3x))@V1t))))) & ( ! [V4x:$i] : ((mem@V4x@A_27a) => ( ! [V5y:$i] : ((mem@V5y@A_27a) => (((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V4x)@V0s)) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V5y)@V0s)) & ((ap@V2f@V4x) = (ap@V2f@V5y)))) => (V4x = V5y))))))))))))))))).
thf(conj_thm_2Ecardinal_2Elt__c,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => ((~~ (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27b@A_27a)@V1t)@V0s))) <=> ((p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27a@A_27b)@V0s)@V1t)) & (~~ (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27b@A_27a)@V1t)@V0s)))))))))))).
thf(conj_thm_2Ecardinal_2Eeq__c,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => ((p@(ap@(ap@(c_2Ecardinal_2Ecardeq@A_27a@A_27b)@V0s)@V1t)) <=> (? [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27b)) & (( ! [V3x:$i] : ((mem@V3x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@V0s)) => (p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@(ap@V2f@V3x))@V1t))))) & ( ! [V4y:$i] : ((mem@V4y@A_27b) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V4y)@V1t)) => (p@(ap@(c_2Ebool_2E_3F_21@A_27a)@(lam@A_27a@(^ [V5x:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V5x)@V0s))@(ap@(ap@(c_2Emin_2E_3D@A_27b)@(ap@V2f@V5x))@V4y)))))))))))))))))))).
thf(ax_thm_2Ecardinal_2Ecardgeq__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => ((p@(ap@(ap@(c_2Ecardinal_2Ecardgeq@A_27a@A_27b)@V0s)@V1t)) <=> (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27b@A_27a)@V1t)@V0s)))))))))).
thf(conj_thm_2Ecardinal_2Ege__c,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => ((p@(ap@(ap@(c_2Ecardinal_2Ecardgeq@A_27a@A_27b)@V0s)@V1t)) <=> (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27b@A_27a)@V1t)@V0s)))))))))).
thf(ax_thm_2Ecardinal_2Ecardgt__def,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => ((p@(ap@(ap@(c_2Ecardinal_2Ecardgt@A_27a@A_27b)@V0s)@V1t)) <=> (~ (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27a@A_27b)@V0s)@V1t))))))))))).
thf(conj_thm_2Ecardinal_2Egt__c,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => ((p@(ap@(ap@(c_2Ecardinal_2Ecardgt@A_27a@A_27b)@V0s)@V1t)) <=> (~~ (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27a@A_27b)@V0s)@V1t))))))))))).
thf(conj_thm_2Ecardinal_2ELE__C,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => ((p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27a@A_27b)@V0s)@V1t)) <=> (? [V2g:$i] : ((mem@V2g@(arr@A_27b@A_27a)) & ( ! [V3x:$i] : ((mem@V3x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@V0s)) => (? [V4y:$i] : ((mem@V4y@A_27b) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V4y)@V1t)) & ((ap@V2g@V4y) = V3x))))))))))))))))).
thf(conj_thm_2Ecardinal_2EGE__C,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => ((p@(ap@(ap@(c_2Ecardinal_2Ecardgeq@A_27a@A_27b)@V0s)@V1t)) <=> (? [V2f:$i] : ((mem@V2f@(arr@A_27a@A_27b)) & ( ! [V3y:$i] : ((mem@V3y@A_27b) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V3y)@V1t)) => (? [V4x:$i] : ((mem@V4x@A_27a) & ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V4x)@V0s)) & (V3y = (ap@V2f@V4x)))))))))))))))))).
thf(conj_thm_2Ecardinal_2ECOUNTABLE,lemma,( ! [A_27a:del]: ( ! [V0t:$i] : ((mem@V0t@(arr@A_27a@bool)) => ((p@(ap@(c_2Epred__set_2Ecountable@A_27a)@V0t)) <=> (p@(ap@(ap@(c_2Ecardinal_2Ecardgeq@ty_2Enum_2Enum@A_27a)@(c_2Epred__set_2EUNIV@ty_2Enum_2Enum))@V0t))))))).
thf(conj_thm_2Ecardinal_2EEQ__C,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => ((p@(ap@(ap@(c_2Ecardinal_2Ecardeq@A_27a@A_27b)@V0s)@V1t)) <=> (? [V2R:$i] : ((mem@V2R@(arr@(ty_2Epair_2Eprod@A_27a@A_27b)@bool)) & (( ! [V3x:$i] : ((mem@V3x@A_27a) => ( ! [V4y:$i] : ((mem@V4y@A_27b) => ((p@(ap@V2R@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V3x)@V4y))) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V3x)@V0s)) & (p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V4y)@V1t)))))))) & (( ! [V5x:$i] : ((mem@V5x@A_27a) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V5x)@V0s)) => (p@(ap@(c_2Ebool_2E_3F_21@A_27b)@(lam@A_27b@(^ [V6y:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V6y)@V1t))@(ap@V2R@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V5x)@V6y)))))))))) & ( ! [V7y:$i] : ((mem@V7y@A_27b) => ((p@(ap@(ap@(c_2Ebool_2EIN@A_27b)@V7y)@V1t)) => (p@(ap@(c_2Ebool_2E_3F_21@A_27a)@(lam@A_27a@(^ [V8x:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V8x)@V0s))@(ap@V2R@(ap@(ap@(c_2Epair_2E_2C@A_27a@A_27b)@V8x)@V7y)))))))))))))))))))))).
thf(conj_thm_2Ecardinal_2ECARD__LE__REFL,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27a@A_27a)@V0s)@V0s)))))).
thf(conj_thm_2Ecardinal_2ECARD__LE__TRANS,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => ( ! [V2u:$i] : ((mem@V2u@(arr@A_27c@bool)) => (((p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27a@A_27b)@V0s)@V1t)) & (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27b@A_27c)@V1t)@V2u))) => (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27a@A_27c)@V0s)@V2u))))))))))))).
thf(conj_thm_2Ecardinal_2ECARD__LT__REFL,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => (~~ (~~ (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27a@A_27a)@V0s)@V0s)))))))).
thf(conj_thm_2Ecardinal_2ECARD__LET__TRANS,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => ( ! [V2u:$i] : ((mem@V2u@(arr@A_27c@bool)) => (((p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27a@A_27b)@V0s)@V1t)) & (~~ (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27c@A_27b)@V2u)@V1t)))) => (~~ (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27c@A_27a)@V2u)@V0s)))))))))))))).
thf(conj_thm_2Ecardinal_2ECARD__LTE__TRANS,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => ( ! [V2u:$i] : ((mem@V2u@(arr@A_27c@bool)) => (((~~ (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27b@A_27a)@V1t)@V0s))) & (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27b@A_27c)@V1t)@V2u))) => (~~ (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27c@A_27a)@V2u)@V0s)))))))))))))).
thf(conj_thm_2Ecardinal_2ECARD__LT__TRANS,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => ( ! [V2u:$i] : ((mem@V2u@(arr@A_27c@bool)) => (((~~ (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27b@A_27a)@V1t)@V0s))) & (~~ (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27c@A_27b)@V2u)@V1t)))) => (~~ (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27c@A_27a)@V2u)@V0s)))))))))))))).
thf(conj_thm_2Ecardinal_2ECARD__EQ__REFL,lemma,( ! [A_27a:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => (p@(ap@(ap@(c_2Ecardinal_2Ecardeq@A_27a@A_27a)@V0s)@V0s)))))).
thf(conj_thm_2Ecardinal_2ECARD__EQ__SYM,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => ((p@(ap@(ap@(c_2Ecardinal_2Ecardeq@A_27a@A_27b)@V0s)@V1t)) <=> (p@(ap@(ap@(c_2Ecardinal_2Ecardeq@A_27b@A_27a)@V1t)@V0s)))))))))).
thf(conj_thm_2Ecardinal_2ECARD__EQ__IMP__LE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => ((p@(ap@(ap@(c_2Ecardinal_2Ecardeq@A_27a@A_27b)@V0s)@V1t)) => (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27a@A_27b)@V0s)@V1t)))))))))).
thf(conj_thm_2Ecardinal_2ECARD__LT__IMP__LE,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ( ! [V1t:$i] : ((mem@V1t@(arr@A_27b@bool)) => ((~~ (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27b@A_27a)@V1t)@V0s))) => (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27a@A_27b)@V0s)@V1t)))))))))).
thf(conj_thm_2Ecardinal_2ECARD__LE__RELATIONAL,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0R:$i] : ((mem@V0R@(arr@A_27a@(arr@A_27b@bool))) => ( ! [V1s:$i] : ((mem@V1s@(arr@A_27a@bool)) => (( ! [V2x:$i] : ((mem@V2x@A_27a) => ( ! [V3y:$i] : ((mem@V3y@A_27b) => ( ! [V4y_27:$i] : ((mem@V4y_27@A_27b) => (((p@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V2x)@V1s)) & ((p@(ap@(ap@V0R@V2x)@V3y)) & (p@(ap@(ap@V0R@V2x)@V4y_27)))) => (V3y = V4y_27)))))))) => (p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27b@A_27a)@(ap@(c_2Epred__set_2EGSPEC@A_27b@A_27b)@(lam@A_27b@(^ [V5y:$i] : (ap@(ap@(c_2Epair_2E_2C@A_27b@bool)@V5y)@(ap@(c_2Ebool_2E_3F@A_27a)@(lam@A_27a@(^ [V6x:$i] : (ap@(ap@c_2Ebool_2E_2F_5C@(ap@(ap@(c_2Ebool_2EIN@A_27a)@V6x)@V1s))@(ap@(ap@V0R@V6x)@V5y))))))))))@V1s)))))))))).
thf(conj_thm_2Ecardinal_2ECARD__LE__EMPTY,lemma,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Ecardinal_2Ecardleq@A_27a@A_27b)@V0s)@(c_2Epred__set_2EEMPTY@A_27b))) <=> (V0s = (c_2Epred__set_2EEMPTY@A_27a)))))))).
thf(conj_thm_2Ecardinal_2ECARD__EQ__EMPTY,conjecture,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : ((mem@V0s@(arr@A_27a@bool)) => ((p@(ap@(ap@(c_2Ecardinal_2Ecardeq@A_27a@A_27b)@V0s)@(c_2Epred__set_2EEMPTY@A_27b))) <=> (V0s = (c_2Epred__set_2EEMPTY@A_27a)))))))).
