--- a/QuotScript.thy	Sat Oct 24 08:34:14 2009 +0200
+++ b/QuotScript.thy	Sat Oct 24 10:16:53 2009 +0200
@@ -480,6 +480,12 @@
   apply (simp add: FUN_REL.simps Ball_def IN_RESPECTS)
   done
 
+lemma RES_EXISTS_RSP:
+  shows "\<And>f g. (R ===> (op =)) f g ==>
+        (Bex (Respects R) f = Bex (Respects R) g)"
+  apply (simp add: FUN_REL.simps Bex_def IN_RESPECTS)
+  done
+
 (* TODO: 
 - [FORALL_PRS, EXISTS_PRS, COND_PRS];
 > val it =
@@ -498,9 +504,18 @@
   shows "!f. All f = Ball (Respects R) ((absf ---> id) f)"
   sorry
 
+lemma EXISTS_PRS:
+  assumes a: "QUOTIENT R absf repf"
+  shows "!f. Ex f = Bex (Respects R) ((absf ---> id) f)"
+  sorry
+
 lemma ho_all_prs: "op = ===> op = ===> op = All All"
   apply (auto)
   done
 
+lemma ho_ex_prs: "op = ===> op = ===> op = Ex Ex"
+  apply (auto)
+  done
+
 end