--- a/Quot/QuotScript.thy	Thu Dec 10 10:54:45 2009 +0100
+++ b/Quot/QuotScript.thy	Thu Dec 10 11:19:34 2009 +0100
@@ -350,6 +350,19 @@
   apply (simp add: in_respects Quotient_rel_rep[OF q1])
   done
 
+lemma babs_simp:
+  assumes q: "Quotient R1 Abs Rep"
+  shows "((R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)) = ((R1 ===> R2) f g)"
+apply(rule iffI)
+apply(simp_all only: babs_rsp[OF q])
+apply(auto simp add: Babs_def)
+apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
+apply(metis Babs_def)
+apply (simp add: in_respects)
+using Quotient_rel[OF q]
+by metis
+
+
 (* needed for regularising? *)
 lemma babs_reg_eqv:
   shows "equivp R \<Longrightarrow> Babs (Respects R) P = P"