# HG changeset patch
# User paulson
# Date 982326476 -3600
# Node ID 4042eb2fde2f1f65a5a70fcc5c80dbea1c38ba40
# Parent  67387142225eaf6e6b1a3ab091017167e17c1a46
Blast bug fix made old proof too slow

diff -r 67387142225e -r 4042eb2fde2f src/ZF/AC/AC7_AC9.ML
--- a/src/ZF/AC/AC7_AC9.ML	Fri Feb 16 13:25:08 2001 +0100
+++ b/src/ZF/AC/AC7_AC9.ML	Fri Feb 16 13:27:56 2001 +0100
@@ -149,16 +149,21 @@
         ((prod_commute_eqpoll RS eqpoll_imp_lepoll) RSN (2,lepoll_trans));
 
 
+Goal "[|0 \\<notin> A; B \\<in> A|] ==> nat \\<lesssim> ((nat \\<rightarrow> Union(A)) \\<times> B) \\<times> nat";
+by (blast_tac (claset() addDs [Sigma_fun_space_not0]
+                        addIs [snd_lepoll_SigmaI]) 1);
+qed "nat_lepoll_lemma";
+
+
 Goal "[| 0~:A;  A~=0;  \
 \        C = {((nat->Union(A))*B)*nat. B:A}  Un \
 \            {cons(0,((nat->Union(A))*B)*nat). B:A}; \
 \        B1: C;  B2: C |]  \
 \     ==> B1 eqpoll B2";
-by (blast_tac (claset() addSIs [nat_cons_eqpoll RS eqpoll_trans]
-                addDs [Sigma_fun_space_not0]
-                addIs [eqpoll_trans, eqpoll_sym, snd_lepoll_SigmaI, 
-                       eqpoll_refl RSN (2, prod_eqpoll_cong), 
-                       Sigma_fun_space_eqpoll]) 1);
+by (blast_tac
+    (claset() addSIs [nat_lepoll_lemma, nat_cons_eqpoll RS eqpoll_trans, 
+                      eqpoll_refl RSN (2, prod_eqpoll_cong)]
+              addIs [eqpoll_trans, eqpoll_sym, Sigma_fun_space_eqpoll]) 1);
 val lemma1 = result();
 
 Goal "ALL B1:{(F*B)*N. B:A} Un {cons(0,(F*B)*N). B:A}.  \