--- a/QuotMain.thy	Sat Dec 05 16:26:18 2009 +0100
+++ b/QuotMain.thy	Sat Dec 05 21:28:24 2009 +0100
@@ -964,12 +964,6 @@
     | _ => no_tac)
 *}
 
-lemma fun_rel_id:
-  assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
-  shows "(R1 ===> R2) f g"
-using a by simp
-
-
 ML {*
 fun inj_repabs_tac_match ctxt trans2 = SUBGOAL (fn (goal, i) =>
 (case (bare_concl goal) of