1.1 --- a/src/ZF/AC/AC7_AC9.ML	Fri Feb 16 13:25:08 2001 +0100
     1.2 +++ b/src/ZF/AC/AC7_AC9.ML	Fri Feb 16 13:27:56 2001 +0100
     1.3 @@ -149,16 +149,21 @@
     1.4          ((prod_commute_eqpoll RS eqpoll_imp_lepoll) RSN (2,lepoll_trans));
     1.5  
     1.6  
     1.7 +Goal "[|0 \\<notin> A; B \\<in> A|] ==> nat \\<lesssim> ((nat \\<rightarrow> Union(A)) \\<times> B) \\<times> nat";
     1.8 +by (blast_tac (claset() addDs [Sigma_fun_space_not0]
     1.9 +                        addIs [snd_lepoll_SigmaI]) 1);
    1.10 +qed "nat_lepoll_lemma";
    1.11 +
    1.12 +
    1.13  Goal "[| 0~:A;  A~=0;  \
    1.14  \        C = {((nat->Union(A))*B)*nat. B:A}  Un \
    1.15  \            {cons(0,((nat->Union(A))*B)*nat). B:A}; \
    1.16  \        B1: C;  B2: C |]  \
    1.17  \     ==> B1 eqpoll B2";
    1.18 -by (blast_tac (claset() addSIs [nat_cons_eqpoll RS eqpoll_trans]
    1.19 -                addDs [Sigma_fun_space_not0]
    1.20 -                addIs [eqpoll_trans, eqpoll_sym, snd_lepoll_SigmaI, 
    1.21 -                       eqpoll_refl RSN (2, prod_eqpoll_cong), 
    1.22 -                       Sigma_fun_space_eqpoll]) 1);
    1.23 +by (blast_tac
    1.24 +    (claset() addSIs [nat_lepoll_lemma, nat_cons_eqpoll RS eqpoll_trans, 
    1.25 +                      eqpoll_refl RSN (2, prod_eqpoll_cong)]
    1.26 +              addIs [eqpoll_trans, eqpoll_sym, Sigma_fun_space_eqpoll]) 1);
    1.27  val lemma1 = result();
    1.28  
    1.29  Goal "ALL B1:{(F*B)*N. B:A} Un {cons(0,(F*B)*N). B:A}.  \