--- a/QuotScript.thy	Thu Oct 22 11:43:12 2009 +0200
+++ b/QuotScript.thy	Thu Oct 22 13:45:48 2009 +0200
@@ -473,5 +473,11 @@
   shows "Ex P \<Longrightarrow> Bex R Q"
   using a by (metis COMBC_def Collect_def Collect_mem_eq)
 
+lemma RES_FORALL_RSP:
+  assumes a: "QUOTIENT R abs rep"
+  shows "\<And>f g. (R ===> (op =)) f g ==>
+        (Ball (Respects R) f = Ball (Respects R) g)"
+  sorry
+
 end