--- a/Quot/QuotScript.thy	Thu Jan 21 09:55:05 2010 +0100
+++ b/Quot/QuotScript.thy	Thu Jan 21 10:55:09 2010 +0100
@@ -372,6 +372,46 @@
   using a 
 by (simp add: Ex1_def Bex1_def in_respects) auto
 
+(* TODO/FIXME: simplify the repetitions in this proof *)
+lemma bexeq_rsp:
+assumes a: "Quotient R absf repf"
+shows "((R ===> op =) ===> op =) (Bexeq R) (Bexeq R)"
+apply simp
+unfolding Bexeq_def
+apply rule
+apply rule
+apply rule
+apply rule
+apply (erule conjE)+
+apply (erule bexE)
+apply rule
+apply (rule_tac x="xa" in bexI)
+apply metis
+apply metis
+apply rule+
+apply (erule_tac x="xb" in ballE)
+prefer 2
+apply (metis in_respects)
+apply (erule_tac x="ya" in ballE)
+prefer 2
+apply (metis in_respects)
+apply (metis in_respects)
+apply (erule conjE)+
+apply (erule bexE)
+apply rule
+apply (rule_tac x="xa" in bexI)
+apply metis
+apply metis
+apply rule+
+apply (erule_tac x="xb" in ballE)
+prefer 2
+apply (metis in_respects)
+apply (erule_tac x="ya" in ballE)
+prefer 2
+apply (metis in_respects)
+apply (metis in_respects)
+done
+
 lemma babs_rsp:
   assumes q: "Quotient R1 Abs1 Rep1"
   and     a: "(R1 ===> R2) f g"