--- a/QuotScript.thy	Fri Oct 23 18:20:06 2009 +0200
+++ b/QuotScript.thy	Sat Oct 24 08:09:09 2009 +0200
@@ -498,6 +498,9 @@
   shows "!f. All f = Ball (Respects R) ((absf ---> id) f)"
   sorry
 
+lemma ho_all_prs: "op = ===> op = ===> op = All All"
+  apply (auto)
+  done
 
 end