--- a/QuotScript.thy	Fri Nov 13 16:44:36 2009 +0100
+++ b/QuotScript.thy	Fri Nov 13 19:32:12 2009 +0100
@@ -390,6 +390,11 @@
   shows "R2 (f x) (g y)"
 using a by (rule FUN_REL_IMP)
 
+lemma APPLY_RSP2:
+  assumes a: "(R1 ===> R2) f g" "R1 x y"
+  shows "R2 (f x) (g y)"
+using a by (rule FUN_REL_IMP)
+
 
 (* combinators: I, K, o, C, W *)