--- a/Quot/QuotScript.thy	Wed Dec 09 00:54:46 2009 +0100
+++ b/Quot/QuotScript.thy	Wed Dec 09 05:59:49 2009 +0100
@@ -389,6 +389,16 @@
 (******************************************)
 (* REST OF THE FILE IS UNUSED (until now) *)
 (******************************************)
+
+(* Always safe to apply, but not too helpful *)
+lemma app_prs2:
+  assumes q1: "Quotient R1 abs1 rep1"
+  and     q2: "Quotient R2 abs2 rep2"
+  shows  "((abs1 ---> rep2) ((rep1 ---> abs2) f) (rep1 x)) = rep2 (((rep1 ---> abs2) f) x)"
+unfolding expand_fun_eq
+using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
+by simp
+
 lemma Quotient_rel_abs:
   assumes a: "Quotient E Abs Rep"
   shows "E r s \<Longrightarrow> Abs r = Abs s"