--- a/Quot/QuotScript.thy	Fri Jan 08 10:08:01 2010 +0100
+++ b/Quot/QuotScript.thy	Fri Jan 08 10:39:08 2010 +0100
@@ -509,6 +509,12 @@
   apply(simp add: Quotient_abs_rep[OF a])
   done
 
+lemma eq_comp_r: "op = OO R OO op = \<equiv> R"
+  apply (rule eq_reflection)
+  apply (rule ext)+
+  apply auto
+  done
+
 lemma fun_rel_eq_rel:
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"