--- a/QuotScript.thy	Mon Dec 07 04:41:42 2009 +0100
+++ b/QuotScript.thy	Mon Dec 07 08:45:04 2009 +0100
@@ -19,13 +19,17 @@
   unfolding equivp_def reflp_def symp_def transp_def expand_fun_eq
   by (blast)
 
-lemma equivp_refl:
-  shows "equivp R \<Longrightarrow> (\<And>x. R x x)"
-  by (simp add: equivp_reflp_symp_transp reflp_def)
-
 lemma equivp_reflp:
   shows "equivp E \<Longrightarrow> (\<And>x. E x x)"
-  by (simp add: equivp_reflp_symp_transp reflp_def)
+  by (simp only: equivp_reflp_symp_transp reflp_def)
+
+lemma equivp_symp:
+  shows "equivp E \<Longrightarrow> (\<And>x y. E x y \<Longrightarrow> E y x)"
+  by (metis equivp_reflp_symp_transp symp_def)
+
+lemma equivp_transp:
+  shows "equivp E \<Longrightarrow> (\<And>x y z. E x y \<Longrightarrow> E y z \<Longrightarrow> E x z)"
+by (metis equivp_reflp_symp_transp transp_def)
 
 definition
   "part_equivp 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)))"
@@ -95,11 +99,6 @@
   by metis
 
 fun
-  prod_rel
-where
-  "prod_rel r1 r2 = (\<lambda>(a,b) (c,d). r1 a c \<and> r2 b d)"
-
-fun
   fun_map
 where
   "fun_map f g h x = g (h (f x))"