--- a/Quot/QuotScript.thy	Thu Dec 10 11:19:34 2009 +0100
+++ b/Quot/QuotScript.thy	Thu Dec 10 12:25:12 2009 +0100
@@ -386,6 +386,11 @@
   shows "(R1 ===> R2) f g"
 using a by simp
 
+lemma fun_rel_id_asm:
+  assumes a: "\<And>x y. R1 x y \<Longrightarrow> (A \<longrightarrow> R2 (f x) (g y))"
+  shows "A \<longrightarrow> (R1 ===> R2) f g"
+using a by auto
+
 lemma quot_rel_rsp:
   assumes a: "Quotient R Abs Rep"
   shows "(R ===> R ===> op =) R R"