diff -r c4001cda9da3 -r aaeb5a34d21a Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Fri Feb 12 16:04:10 2010 +0100
+++ b/Quot/Examples/FSet.thy	Fri Feb 12 16:06:09 2010 +0100
@@ -363,6 +363,11 @@
 lemma hard: "(\<lambda>P. \<lambda>Q. P (Q (x::'a list))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a list)))"
 sorry
 
+lemma eq_imp_rel:
+  shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"
+  by (simp add: equivp_reflp)
+
+
 lemma hard_lift: "(\<lambda>P. \<lambda>Q. P (Q (x::'a fset))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a fset)))"
 apply(lifting hard)
 apply(regularize)