diff -r 5a3965aa4d80 -r 9c33c0809733 QuotScript.thy
--- a/QuotScript.thy	Sat Nov 28 04:02:54 2009 +0100
+++ b/QuotScript.thy	Sat Nov 28 05:29:30 2009 +0100
@@ -517,6 +517,13 @@
   shows "Bex R Q"
   using a b by (metis COMBC_def Collect_def Collect_mem_eq)
 
+lemma ball_all_comm:
+  "(\<And>y. (\<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>x. B x y)) \<Longrightarrow> ((\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y))"
+by auto
+
+lemma bex_ex_comm:
+  "((\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)) \<Longrightarrow> ((\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y))"
+by auto