include('Axioms/ring_2.ax').
tff(tp_c_2Ecardinal_2E_2B__c,type,(c_2Ecardinal_2E_2B__c:(del * del) > $i)).
tff(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))))))).
tff(tp_c_2Ecardinal_2EHAS__SIZE,type,(c_2Ecardinal_2EHAS__SIZE:del > $i)).
tff(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))))).
tff(tp_c_2Ecardinal_2Ebijns,type,(c_2Ecardinal_2Ebijns:del > $i)).
tff(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))))).
tff(tp_c_2Ecardinal_2Ecardeq,type,(c_2Ecardinal_2Ecardeq:(del * del) > $i)).
tff(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)))))).
tff(tp_c_2Ecardinal_2Ecardgeq,type,(c_2Ecardinal_2Ecardgeq:(del * del) > $i)).
tff(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)))))).
tff(tp_c_2Ecardinal_2Ecardgt,type,(c_2Ecardinal_2Ecardgt:(del * del) > $i)).
tff(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)))))).
tff(tp_c_2Ecardinal_2Ecardleq,type,(c_2Ecardinal_2Ecardleq:(del * del) > $i)).
tff(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)))))).
tff(tp_c_2Ecardinal_2Elist,type,(c_2Ecardinal_2Elist:del > $i)).
tff(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))))).
tff(tp_c_2Ecardinal_2Eset__exp,type,(c_2Ecardinal_2Eset__exp:(del * del) > $i)).
tff(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))))))).
tff(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)))))))))))).
tff(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))))))).
tff(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))))))))))).
tff(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)))))))))))))).
tff(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)))))))))))).
tff(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))))))).
tff(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)))))))))))))).
tff(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))))))))))).
tff(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)))))))))))).
tff(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)))))))))))).
tff(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))))))))))).
tff(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)))))))))))).
tff(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)))))))))).
tff(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)))))))).
tff(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))))))))))).
tff(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)))))))))))))))))).
tff(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))))))))))).
tff(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))))))))))).
tff(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)))))))))))))))))).
tff(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))))))))))).
tff(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)))))))).
tff(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)))))))))).
tff(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)))))))))))))))))).
tff(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)))))))))).
tff(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)))))))))))))).
tff(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))))))))).
tff(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)))))))))))).
tff(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))))))))))).
tff(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)))))))))))).
tff(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))))))))).
tff(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))))))))))))).
tff(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))))))))))))))).
tff(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))))))))))))))).
tff(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))))))))))))))).
tff(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))))))))).
tff(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)))))))))).
tff(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)))))))).
tff(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),inj__o(fo__c_2Ebool_2ET)),ap(ap(c_2Epred__set_2EINSERT(bool),inj__o(fo__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))))))))))))))).
tff(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))))))))))).
tff(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))),f1851(A_27b,A_27a,V1B,V0A)))))))))).
tff(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))))))))))))))).
tff(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))))))))))).
tff(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))))))))))))).
tff(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))))))))))))).
tff(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)))))))))))))))).
tff(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)))))))))))).
tff(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))),f1852(A_27a,A_27b,V0x,V1B)),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),f1854(A_27b,A_27c,V0x,V2A))))))))))))))).
tff(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)))))))))))))).
tff(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)))))))).
tff(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)),f1856(A_27a,V0A,V1n)))))))))).
tff(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))))))))))))))))))).
tff(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))))))))))))))))))).
tff(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))))))))))))))).
tff(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))))))))).
tff(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)))))))).
tff(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)))))))))))).
tff(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)))))))))))))).
tff(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)),f1858(A_27a,V0A))))))).
tff(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))))))).
tff(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)))))))).
tff(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)))))).
tff(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)),f1859(A_27a,V0A)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)))))))))).
tff(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)))))))).
tff(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)),f1860(A_27a,V0A)))))))))).
tff(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)))))))))))).
tff(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))))))))))))))).
tff(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))))))))))))))))).
tff(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))))))))))).
tff(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)))))))).
tff(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))))))))))).
tff(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))))))))))))))).
tff(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))))).
tff(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))))))))).
tff(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))),f1863(A_27a,V0A))))))).
tff(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)))))))))))).
tff(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))))))))).
tff(conj_thm_2Ecardinal_2ELEFT__IMP__EXISTS__THM,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1Q:tp__o] : (((? [V2x:$i] : (mem(V2x,A_27a) & p(ap(V0P,V2x)))) => p(inj__o(V1Q))) <=> ( ! [V3x:$i] : (mem(V3x,A_27a) => (p(ap(V0P,V3x)) => p(inj__o(V1Q)))))))))))).
tff(conj_thm_2Ecardinal_2ELEFT__IMP__FORALL__THM,lemma,(( ! [A_27a:del]: ( ! [V0P:$i] : (mem(V0P,arr(A_27a,bool)) => ( ! [V1Q:tp__o] : ((( ! [V2x:$i] : (mem(V2x,A_27a) => p(ap(V0P,V2x)))) => p(inj__o(V1Q))) <=> (? [V3x:$i] : (mem(V3x,A_27a) & (p(ap(V0P,V3x)) => p(inj__o(V1Q)))))))))))).
tff(conj_thm_2Ecardinal_2ERIGHT__IMP__EXISTS__THM,lemma,(( ! [A_27a:del]: ( ! [V0P:tp__o] : ( ! [V1Q:$i] : (mem(V1Q,arr(A_27a,bool)) => ((p(inj__o(V0P)) => (? [V2x:$i] : (mem(V2x,A_27a) & p(ap(V1Q,V2x))))) <=> (? [V3x:$i] : (mem(V3x,A_27a) & (p(inj__o(V0P)) => p(ap(V1Q,V3x)))))))))))).
tff(conj_thm_2Ecardinal_2ERIGHT__IMP__FORALL__THM,lemma,(( ! [A_27a:del]: ( ! [V0P:tp__o] : ( ! [V1Q:$i] : (mem(V1Q,arr(A_27a,bool)) => ((p(inj__o(V0P)) => ( ! [V2x:$i] : (mem(V2x,A_27a) => p(ap(V1Q,V2x))))) <=> ( ! [V3x:$i] : (mem(V3x,A_27a) => (p(inj__o(V0P)) => p(ap(V1Q,V3x)))))))))))).
tff(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)))))))))))).
tff(conj_thm_2Ecardinal_2ECONJ__EQ__IMP,lemma,(( ! [V0r:tp__o] : ( ! [V1p:tp__o] : ( ! [V2q:tp__o] : (((p(inj__o(V1p)) & p(inj__o(V2q))) => p(inj__o(V0r))) <=> (p(inj__o(V1p)) => (p(inj__o(V2q)) => p(inj__o(V0r)))))))))).
tff(conj_thm_2Ecardinal_2EIMP__CONJ__ALT,lemma,(( ! [V0r:tp__o] : ( ! [V1p:tp__o] : ( ! [V2q:tp__o] : (((p(inj__o(V1p)) & p(inj__o(V2q))) => p(inj__o(V0r))) <=> (p(inj__o(V2q)) => (p(inj__o(V1p)) => p(inj__o(V0r)))))))))).
tff(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)))))))).
tff(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)))))))))))))))))).
tff(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)))))))))))).
tff(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),f1864(A_27b,A_27a,V2s,V0f,V1A))))))))))))))).
tff(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),f1865(A_27b,A_27a,V1A,V0f))))))))))))).
tff(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)))))))))))).
tff(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)))))))))))))).
tff(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))))))))).
tff(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)),f1867(A_27c,A_27b,A_27a,V1s,V2t,V0f))))))))))))))))).
tff(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)),f1869(A_27a,A_27b,V1t,V0s)))))))))))))).
tff(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),f1870(A_27b,A_27a,V3P,V0f))) = ap(c_2Epred__set_2EGSPEC(A_27b,A_27b),f1871(A_27b,V3P)))))))))))).
tff(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)))))))))))))))))).
tff(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)))))))))))).
tff(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)))))))))))))))))).
tff(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)))))))))))).
tff(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)))))))))))).
tff(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)))))))))))))))))).
tff(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))))))))))))))).
tff(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))))))))))))))))))).
tff(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))))))))))))))))))).
tff(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)))))))))).
tff(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))))))))))))))).
tff(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))))))))))))).
tff(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)))))))))))).
tff(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))))))))))).
tff(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))))))))).
tff(conj_thm_2Ecardinal_2Enum__INFINITE,lemma,((~~ p(ap(c_2Epred__set_2EFINITE(ty_2Enum_2Enum),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)))))).
tff(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)))))))).
tff(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)))))))).
tff(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)))))))).
tff(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)))))))))))))).
tff(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))))))))).
tff(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)))))))))))))))).
tff(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))))))))).
tff(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),f1872(A_27a,V4x,V2f,V1n)))))))))))))))).
tff(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),f1873(A_27b,A_27a,V1t,V0s))))),ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(V2m)),inj__ty_2Enum_2Enum(V3n))))))))))))))).
tff(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))))))).
tff(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))))))).
tff(conj_thm_2Ecardinal_2EFINITE__BOOL,lemma,(p(ap(c_2Epred__set_2EFINITE(bool),c_2Epred__set_2EUNIV(bool))))).
tff(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))))))))))).
tff(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)))))))))).
tff(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))))))).
tff(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),f275(V0n))),inj__ty_2Enum_2Enum(V0n)))))).
tff(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),f275(V0n))))))).
tff(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),f1874(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))))))))).
tff(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),f1874(V0n))))))).
tff(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)))))))))))).
tff(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)))))))).
tff(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))))))).
tff(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)))))))))).
tff(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)))))))).
tff(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)))))))).
tff(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)))))))).
tff(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))))))))))))))).
tff(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)))))))))))).
tff(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))))))))))))))).
tff(conj_thm_2Ecardinal_2ECONJ__ACI,lemma,(( ! [V0r:tp__o] : ( ! [V1p:tp__o] : ( ! [V2q:tp__o] : (((p(inj__o(V1p)) & p(inj__o(V2q))) <=> (p(inj__o(V2q)) & p(inj__o(V1p)))) & ((((p(inj__o(V1p)) & p(inj__o(V2q))) & p(inj__o(V0r))) <=> (p(inj__o(V1p)) & (p(inj__o(V2q)) & p(inj__o(V0r))))) & (((p(inj__o(V1p)) & (p(inj__o(V2q)) & p(inj__o(V0r)))) <=> (p(inj__o(V2q)) & (p(inj__o(V1p)) & p(inj__o(V0r))))) & (((p(inj__o(V1p)) & p(inj__o(V1p))) <=> p(inj__o(V1p))) & ((p(inj__o(V1p)) & (p(inj__o(V1p)) & p(inj__o(V2q)))) <=> (p(inj__o(V1p)) & p(inj__o(V2q))))))))))))).
tff(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))))))))))))))).
tff(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)))))).
tff(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))))))))))).
tff(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))))))))))))).
tff(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),f1875(A_27b,A_27a,V4y,V0f,V1s))))))) <=> (( ! [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)))))))))))))))))))).
tff(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),f1875(A_27b,A_27a,V4y,V0f,V1s))))))) <=> (( ! [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)))))))))))))))))))).
tff(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)))))))))))))))))).
tff(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))))))))))))).
tff(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),f1876(A_27b,A_27a,V4y,V2f,V0s)))))))))))))))))).
tff(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)))))))))).
tff(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))))))))))).
tff(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))))))))))).
tff(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)))))))))))).
tff(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)))))))))))))))))).
tff(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))))))))))))))))))).
tff(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)))))))).
tff(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),f1877(A_27a,A_27b,V2R,V5x,V1t)))))) & ( ! [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),f1878(A_27b,A_27a,V2R,V7y,V0s))))))))))))))))))).
tff(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))))))).
tff(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)))))))))))))).
tff(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))))))))).
tff(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))))))))))))))).
tff(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))))))))))))))).
tff(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))))))))))))))).
tff(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))))))).
tff(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))))))))))).
tff(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))))))))))).
tff(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))))))))))).
tff(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),f1880(A_27a,A_27b,V0R,V1s))),V1s))))))))))).
tff(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))))))))).
tff(conj_thm_2Ecardinal_2ECARD__EQ__EMPTY,lemma,(( ! [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))))))))).
tff(conj_thm_2Ecardinal_2ECARD__LE__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))))))))))).
tff(conj_thm_2Ecardinal_2ECARD__LE__TOTAL,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))))))))))).
tff(conj_thm_2Ecardinal_2ECARD__LET__TOTAL,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_27a,A_27b),V0s),V1t)))))))))))).
tff(conj_thm_2Ecardinal_2ECARD__LTE__TOTAL,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_27b,A_27a),V1t),V0s))))))))))).
tff(conj_thm_2Ecardinal_2ECARD__LT__TOTAL,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_27b,A_27a),V1t),V0s))) | (~~ p(ap(ap(c_2Ecardinal_2Ecardleq(A_27a,A_27b),V0s),V1t))))))))))))).
tff(conj_thm_2Ecardinal_2ECARD__NOT__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_27a,A_27b),V0s),V1t))) <=> (~~ p(ap(ap(c_2Ecardinal_2Ecardleq(A_27a,A_27b),V0s),V1t)))))))))))).
tff(conj_thm_2Ecardinal_2ECARD__NOT__LT,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_27b,A_27a),V1t),V0s))))))))))).
tff(conj_thm_2Ecardinal_2ECARD__LT__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)) & (~~ p(ap(ap(c_2Ecardinal_2Ecardeq(A_27a,A_27b),V0s),V1t))))))))))))).
tff(conj_thm_2Ecardinal_2ECARD__LE__LT,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)))))))))))).
tff(conj_thm_2Ecardinal_2ECARD__LE__CONG,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [V0s:$i] : (mem(V0s,arr(A_27a,bool)) => ( ! [V1s_27:$i] : (mem(V1s_27,arr(A_27b,bool)) => ( ! [V2t:$i] : (mem(V2t,arr(A_27c,bool)) => ( ! [V3t_27:$i] : (mem(V3t_27,arr(A_27d,bool)) => ((p(ap(ap(c_2Ecardinal_2Ecardeq(A_27a,A_27b),V0s),V1s_27)) & p(ap(ap(c_2Ecardinal_2Ecardeq(A_27c,A_27d),V2t),V3t_27))) => (p(ap(ap(c_2Ecardinal_2Ecardleq(A_27a,A_27c),V0s),V2t)) <=> p(ap(ap(c_2Ecardinal_2Ecardleq(A_27b,A_27d),V1s_27),V3t_27)))))))))))))))))).
tff(conj_thm_2Ecardinal_2ECARD__LT__CONG,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [V0s:$i] : (mem(V0s,arr(A_27a,bool)) => ( ! [V1s_27:$i] : (mem(V1s_27,arr(A_27b,bool)) => ( ! [V2t:$i] : (mem(V2t,arr(A_27c,bool)) => ( ! [V3t_27:$i] : (mem(V3t_27,arr(A_27d,bool)) => ((p(ap(ap(c_2Ecardinal_2Ecardeq(A_27a,A_27b),V0s),V1s_27)) & p(ap(ap(c_2Ecardinal_2Ecardeq(A_27c,A_27d),V2t),V3t_27))) => ((~~ p(ap(ap(c_2Ecardinal_2Ecardleq(A_27c,A_27a),V2t),V0s))) <=> (~~ p(ap(ap(c_2Ecardinal_2Ecardleq(A_27d,A_27b),V3t_27),V1s_27))))))))))))))))))).
tff(conj_thm_2Ecardinal_2ECARD__EQ__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)))))))))))))).
tff(conj_thm_2Ecardinal_2ECARD__EQ__CONG,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [V0s:$i] : (mem(V0s,arr(A_27a,bool)) => ( ! [V1s_27:$i] : (mem(V1s_27,arr(A_27b,bool)) => ( ! [V2t:$i] : (mem(V2t,arr(A_27c,bool)) => ( ! [V3t_27:$i] : (mem(V3t_27,arr(A_27d,bool)) => ((p(ap(ap(c_2Ecardinal_2Ecardeq(A_27a,A_27b),V0s),V1s_27)) & p(ap(ap(c_2Ecardinal_2Ecardeq(A_27c,A_27d),V2t),V3t_27))) => (p(ap(ap(c_2Ecardinal_2Ecardeq(A_27a,A_27c),V0s),V2t)) <=> p(ap(ap(c_2Ecardinal_2Ecardeq(A_27b,A_27d),V1s_27),V3t_27)))))))))))))))))).
tff(conj_thm_2Ecardinal_2EINFINITE__CARD__LE,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_2Ecardleq(ty_2Enum_2Enum,A_27a),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),V0s)))))))).
tff(conj_thm_2Ecardinal_2EFINITE__CARD__LT,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_2Ecardleq(ty_2Enum_2Enum,A_27a),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),V0s))))))))).
tff(conj_thm_2Ecardinal_2ECARD__LE__SUBSET,lemma,(( ! [A_27a:del]: ( ! [V0s:$i] : (mem(V0s,arr(A_27a,bool)) => ( ! [V1t:$i] : (mem(V1t,arr(A_27a,bool)) => (p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),V0s),V1t)) => p(ap(ap(c_2Ecardinal_2Ecardleq(A_27a,A_27a),V0s),V1t)))))))))).
tff(conj_thm_2Ecardinal_2ECARD__LE__UNIV,lemma,(( ! [A_27a:del]: ( ! [V0s:$i] : (mem(V0s,arr(A_27a,bool)) => p(ap(ap(c_2Ecardinal_2Ecardleq(A_27a,A_27a),V0s),c_2Epred__set_2EUNIV(A_27a)))))))).
tff(conj_thm_2Ecardinal_2ECARD__LE__EQ__SUBSET,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)) <=> (? [V2u:$i] : (mem(V2u,arr(A_27b,bool)) & (p(ap(ap(c_2Epred__set_2ESUBSET(A_27b),V2u),V1t)) & p(ap(ap(c_2Ecardinal_2Ecardeq(A_27a,A_27b),V0s),V2u)))))))))))))).
tff(conj_thm_2Ecardinal_2ECARD__INFINITE__CONG,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_2EFINITE(A_27a),V0s))) <=> (~~ p(ap(c_2Epred__set_2EFINITE(A_27b),V1t))))))))))))).
tff(conj_thm_2Ecardinal_2ECARD__FINITE__CONG,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_2EFINITE(A_27a),V0s)) <=> p(ap(c_2Epred__set_2EFINITE(A_27b),V1t)))))))))))).
tff(conj_thm_2Ecardinal_2ECARD__LE__FINITE,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_27b),V1t)) & p(ap(ap(c_2Ecardinal_2Ecardleq(A_27a,A_27b),V0s),V1t))) => p(ap(c_2Epred__set_2EFINITE(A_27a),V0s))))))))))).
tff(conj_thm_2Ecardinal_2ECARD__EQ__FINITE,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : (mem(V0s,arr(A_27b,bool)) => ( ! [V1t:$i] : (mem(V1t,arr(A_27a,bool)) => ((p(ap(c_2Epred__set_2EFINITE(A_27a),V1t)) & p(ap(ap(c_2Ecardinal_2Ecardeq(A_27b,A_27a),V0s),V1t))) => p(ap(c_2Epred__set_2EFINITE(A_27b),V0s))))))))))).
tff(conj_thm_2Ecardinal_2ECARD__LE__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(ap(c_2Ecardinal_2Ecardleq(A_27a,A_27b),V0s),V1t))) => (~~ p(ap(c_2Epred__set_2EFINITE(A_27b),V1t)))))))))))).
tff(conj_thm_2Ecardinal_2ECARD__LT__FINITE__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_27b,A_27a),V1t),V0s)))))))))))).
tff(conj_thm_2Ecardinal_2ECARD__LE__CARD__IMP,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_27b),V1t)) & p(ap(ap(c_2Ecardinal_2Ecardleq(A_27a,A_27b),V0s),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)))))))))))).
tff(conj_thm_2Ecardinal_2ECARD__EQ__CARD__IMP,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_27b),V1t)) & p(ap(ap(c_2Ecardinal_2Ecardeq(A_27a,A_27b),V0s),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)))))))))))).
tff(conj_thm_2Ecardinal_2ECARD__LE__CARD,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)) <=> p(ap(ap(c_2Earithmetic_2E_3C_3D,ap(c_2Epred__set_2ECARD(A_27a),V0s)),ap(c_2Epred__set_2ECARD(A_27b),V1t))))))))))))).
tff(conj_thm_2Ecardinal_2ECARD__EQ__CARD,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_2Ecardeq(A_27a,A_27b),V0s),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))))))))))))).
tff(conj_thm_2Ecardinal_2ECARD__LT__CARD,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_27b,A_27a),V1t),V0s))) <=> p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Epred__set_2ECARD(A_27a),V0s)),ap(c_2Epred__set_2ECARD(A_27b),V1t))))))))))))).
tff(conj_thm_2Ecardinal_2ECARD__HAS__SIZE__CONG,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : (mem(V0s,arr(A_27a,bool)) => ( ! [V1t:$i] : (mem(V1t,arr(A_27b,bool)) => ( ! [V2n:tp__ty_2Enum_2Enum] : ((p(ap(ap(c_2Ecardinal_2EHAS__SIZE(A_27a),V0s),inj__ty_2Enum_2Enum(V2n))) & p(ap(ap(c_2Ecardinal_2Ecardeq(A_27a,A_27b),V0s),V1t))) => p(ap(ap(c_2Ecardinal_2EHAS__SIZE(A_27b),V1t),inj__ty_2Enum_2Enum(V2n))))))))))))).
tff(conj_thm_2Ecardinal_2ECARD__LE__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)) => p(ap(ap(c_2Ecardinal_2Ecardleq(A_27b,A_27a),ap(ap(c_2Epred__set_2EIMAGE(A_27a,A_27b),V0f),V1s)),V1s)))))))))).
tff(conj_thm_2Ecardinal_2ECARD__LE__IMAGE__GEN,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)) => (p(ap(ap(c_2Epred__set_2ESUBSET(A_27b),V2t),ap(ap(c_2Epred__set_2EIMAGE(A_27a,A_27b),V0f),V1s))) => p(ap(ap(c_2Ecardinal_2Ecardleq(A_27b,A_27a),V2t),V1s))))))))))))).
tff(conj_thm_2Ecardinal_2ECARD__EQ__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)) => (( ! [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(ap(c_2Ecardinal_2Ecardeq(A_27b,A_27a),ap(ap(c_2Epred__set_2EIMAGE(A_27a,A_27b),V0f),V1s)),V1s))))))))))).
tff(ax_thm_2Ecardinal_2Eadd__c,axiom,( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : (mem(V0s,arr(A_27a,bool)) => ( ! [V1t:$i] : (mem(V1t,arr(A_27b,bool)) => (ap(ap(c_2Ecardinal_2E_2B__c(A_27a,A_27b),V0s),V1t) = ap(ap(c_2Epred__set_2EUNION(ty_2Esum_2Esum(A_27a,A_27b)),ap(c_2Epred__set_2EGSPEC(ty_2Esum_2Esum(A_27a,A_27b),A_27a),f1881(A_27b,A_27a,V0s))),ap(c_2Epred__set_2EGSPEC(ty_2Esum_2Esum(A_27a,A_27b),A_27b),f1882(A_27a,A_27b,V1t))))))))))).
tff(conj_thm_2Ecardinal_2Emul__c,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [V0s:$i] : (mem(V0s,arr(A_27a,bool)) => ( ! [V1t:$i] : (mem(V1t,arr(A_27b,bool)) => (ap(ap(c_2Epred__set_2ECROSS(A_27a,A_27b),V0s),V1t) = 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)),f1869(A_27a,A_27b,V1t,V0s)))))))))))).
tff(conj_thm_2Ecardinal_2ECARD__LE__ADD,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [V0s:$i] : (mem(V0s,arr(A_27a,bool)) => ( ! [V1s_27:$i] : (mem(V1s_27,arr(A_27b,bool)) => ( ! [V2t:$i] : (mem(V2t,arr(A_27c,bool)) => ( ! [V3t_27:$i] : (mem(V3t_27,arr(A_27d,bool)) => ((p(ap(ap(c_2Ecardinal_2Ecardleq(A_27a,A_27b),V0s),V1s_27)) & p(ap(ap(c_2Ecardinal_2Ecardleq(A_27c,A_27d),V2t),V3t_27))) => p(ap(ap(c_2Ecardinal_2Ecardleq(ty_2Esum_2Esum(A_27a,A_27c),ty_2Esum_2Esum(A_27b,A_27d)),ap(ap(c_2Ecardinal_2E_2B__c(A_27a,A_27c),V0s),V2t)),ap(ap(c_2Ecardinal_2E_2B__c(A_27b,A_27d),V1s_27),V3t_27)))))))))))))))))).
tff(conj_thm_2Ecardinal_2ECARD__LE__MUL,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [V0s:$i] : (mem(V0s,arr(A_27a,bool)) => ( ! [V1s_27:$i] : (mem(V1s_27,arr(A_27b,bool)) => ( ! [V2t:$i] : (mem(V2t,arr(A_27c,bool)) => ( ! [V3t_27:$i] : (mem(V3t_27,arr(A_27d,bool)) => ((p(ap(ap(c_2Ecardinal_2Ecardleq(A_27a,A_27b),V0s),V1s_27)) & p(ap(ap(c_2Ecardinal_2Ecardleq(A_27c,A_27d),V2t),V3t_27))) => 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),V0s),V2t)),ap(ap(c_2Epred__set_2ECROSS(A_27b,A_27d),V1s_27),V3t_27)))))))))))))))))).
tff(conj_thm_2Ecardinal_2ECARD__ADD__CONG,lemma,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [V0s:$i] : (mem(V0s,arr(A_27a,bool)) => ( ! [V1s_27:$i] : (mem(V1s_27,arr(A_27b,bool)) => ( ! [V2t:$i] : (mem(V2t,arr(A_27c,bool)) => ( ! [V3t_27:$i] : (mem(V3t_27,arr(A_27d,bool)) => ((p(ap(ap(c_2Ecardinal_2Ecardeq(A_27a,A_27b),V0s),V1s_27)) & p(ap(ap(c_2Ecardinal_2Ecardeq(A_27c,A_27d),V2t),V3t_27))) => p(ap(ap(c_2Ecardinal_2Ecardeq(ty_2Esum_2Esum(A_27a,A_27c),ty_2Esum_2Esum(A_27b,A_27d)),ap(ap(c_2Ecardinal_2E_2B__c(A_27a,A_27c),V0s),V2t)),ap(ap(c_2Ecardinal_2E_2B__c(A_27b,A_27d),V1s_27),V3t_27)))))))))))))))))).
tff(conj_thm_2Ecardinal_2ECARD__MUL__CONG,conjecture,(( ! [A_27a:del]: ( ! [A_27b:del]: ( ! [A_27c:del]: ( ! [A_27d:del]: ( ! [V0s:$i] : (mem(V0s,arr(A_27a,bool)) => ( ! [V1s_27:$i] : (mem(V1s_27,arr(A_27b,bool)) => ( ! [V2t:$i] : (mem(V2t,arr(A_27c,bool)) => ( ! [V3t_27:$i] : (mem(V3t_27,arr(A_27d,bool)) => ((p(ap(ap(c_2Ecardinal_2Ecardeq(A_27a,A_27b),V0s),V1s_27)) & p(ap(ap(c_2Ecardinal_2Ecardeq(A_27c,A_27d),V2t),V3t_27))) => 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),V0s),V2t)),ap(ap(c_2Epred__set_2ECROSS(A_27b,A_27d),V1s_27),V3t_27)))))))))))))))))).
