--- a/QuotScript.thy	Wed Oct 14 12:05:39 2009 +0200
+++ b/QuotScript.thy	Wed Oct 14 16:23:32 2009 +0200
@@ -98,6 +98,11 @@
 by metis
 
 fun
+  prod_rel
+where
+  "prod_rel r1 r2 = (\<lambda>(a,b) (c,d). r1 a c \<and> r2 b d)"
+
+fun
   fun_map 
 where
   "fun_map f g h x = g (h (f x))"
@@ -398,4 +403,16 @@
 using a1 a2 unfolding o_def expand_fun_eq
 by (auto)
 
-end
\ No newline at end of file
+lemma equiv_res_forall:
+  fixes P :: "'a \<Rightarrow> bool"
+  assumes a: "EQUIV E"
+  shows "Ball (Respects E) P = (All P)"
+  using a by (metis EQUIV_def IN_RESPECTS a)
+
+lemma equiv_res_exists:
+  fixes P :: "'a \<Rightarrow> bool"
+  assumes a: "EQUIV E"
+  shows "Bex (Respects E) P = (Ex P)"
+  using a by (metis EQUIV_def IN_RESPECTS a)
+
+end