--- a/QuotScript.thy	Sat Dec 05 16:26:18 2009 +0100
+++ b/QuotScript.thy	Sat Dec 05 21:28:24 2009 +0100
@@ -335,6 +335,19 @@
   using a unfolding Quotient_def
   by (metis COMBC_def Collect_def Collect_mem_eq in_respects fun_map.simps id_apply)
 
+lemma fun_rel_id:
+  assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
+  shows "(R1 ===> R2) f g"
+using a by simp
+
+lemma quot_rel_rsp:
+  assumes a: "Quotient R Abs Rep"
+  shows "(R ===> R ===> op =) R R"
+  apply(rule fun_rel_id)+
+  apply(rule equals_rsp[OF a])
+  apply(assumption)+
+  done
+