--- a/QuotScript.thy	Wed Oct 28 12:22:06 2009 +0100
+++ b/QuotScript.thy	Wed Oct 28 14:59:24 2009 +0100
@@ -19,6 +19,10 @@
 unfolding EQUIV_def REFL_def SYM_def TRANS_def expand_fun_eq
 by (blast)
 
+lemma EQUIV_REFL:
+  shows "EQUIV E ==> REFL E"
+  by (simp add: EQUIV_REFL_SYM_TRANS)
+
 definition
   "PART_EQUIV E \<equiv> (\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y)))"