--- a/QuotScript.thy	Fri Oct 23 11:24:43 2009 +0200
+++ b/QuotScript.thy	Fri Oct 23 16:01:13 2009 +0200
@@ -473,11 +473,31 @@
   shows "Ex P \<Longrightarrow> Bex R Q"
   using a by (metis COMBC_def Collect_def Collect_mem_eq)
 
+(* TODO: Add similar *)
 lemma RES_FORALL_RSP:
   shows "\<And>f g. (R ===> (op =)) f g ==>
         (Ball (Respects R) f = Ball (Respects R) g)"
   apply (simp add: FUN_REL.simps Ball_def IN_RESPECTS)
   done
 
+(* TODO: 
+- [FORALL_PRS, EXISTS_PRS, COND_PRS];
+> val it =
+    [|- !R abs rep.
+          QUOTIENT R abs rep ==>
+          !f. $! f <=> RES_FORALL (respects R) ((abs --> I) f),
+     |- !R abs rep.
+          QUOTIENT R abs rep ==>
+          !f. $? f <=> RES_EXISTS (respects R) ((abs --> I) f),
+     |- !R abs rep.
+          QUOTIENT R abs rep ==>
+          !a b c. (if a then b else c) = abs (if a then rep b else rep c)] :
+*)
+lemma FORALL_PRS:
+  assumes a: "QUOTIENT R absf repf"
+  shows "!f. All f = Ball (Respects R) ((absf ---> id) f)"
+  sorry
+
+
 end