--- a/QuotScript.thy	Mon Oct 26 02:06:01 2009 +0100
+++ b/QuotScript.thy	Mon Oct 26 10:02:50 2009 +0100
@@ -495,9 +495,6 @@
      |- !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"
@@ -512,8 +509,16 @@
   using a
   unfolding QUOTIENT_def
   by (metis COMBC_def Collect_def Collect_mem_eq IN_RESPECTS fun_map.simps id_apply mem_def)
-   
-lemma ho_all_prs: 
+
+lemma COND_PRS:
+  assumes a: "QUOTIENT R absf repf"
+  shows "(if a then b else c) = absf (if a then repf b else repf c)"
+  using a
+  unfolding QUOTIENT_def
+  sorry
+
+(* These are the fixed versions, general ones need to be proved. *)
+lemma ho_all_prs:
   shows "op = ===> op = ===> op = All All"
   by auto