--- a/QuotScript.thy	Fri Dec 04 09:33:32 2009 +0100
+++ b/QuotScript.thy	Fri Dec 04 10:12:17 2009 +0100
@@ -329,9 +329,8 @@
 lemma REP_ABS_RSP_LEFT:
   assumes q: "QUOTIENT R Abs Rep"
   and     a: "R x1 x2"
-  and   "R (Rep (Abs x1)) x2"
   shows "R x1 (Rep (Abs x2))"
-using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q] QUOTIENT_SYM[of q])
+using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q])
 
 (* ----------------------------------------------------- *)
 (* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE,           *)
@@ -382,6 +381,11 @@
 using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] by auto
 
 (* ask peter: no use of q1 q2 *)
+(* Cez: I can answer,
+   In the following theorem R2 can be instantiated with anything,
+   but we know some of the types of the Rep and Abs functions;
+   so by solving QUOTIENT assumptions we can get a unique R2 that
+   will be provable; which is why we need to use APPLY_RSP1 *)
 lemma APPLY_RSP:
   assumes q1: "QUOTIENT R1 Abs1 Rep1"
   and     q2: "QUOTIENT R2 Abs2 Rep2"
@@ -389,6 +393,12 @@
   shows "R2 (f x) (g y)"
 using a by (rule FUN_REL_IMP)
 
+lemma APPLY_RSP1:
+  assumes q: "QUOTIENT R1 Abs1 Rep1"
+  and     a: "(R1 ===> R2) f g" "R1 x y"
+  shows "R2 ((f::'a\<Rightarrow>'c) x) ((g::'a\<Rightarrow>'c) y)"
+using a by (rule FUN_REL_IMP)
+
 lemma APPLY_RSP2:
   assumes a: "(R1 ===> R2) f g" "R1 x y"
   shows "R2 (f x) (g y)"