--- a/FSet.thy	Tue Dec 01 14:08:56 2009 +0100
+++ b/FSet.thy	Tue Dec 01 16:27:42 2009 +0100
@@ -12,6 +12,12 @@
 | "xs \<approx> ys \<Longrightarrow> a#xs \<approx> a#ys"
 | "\<lbrakk>xs1 \<approx> xs2; xs2 \<approx> xs3\<rbrakk> \<Longrightarrow> xs1 \<approx> xs3"
 
+lemma
+  "(list_eq ===> (list_eq ===> (op =))) (list_eq) (list_eq)"
+apply(simp add: FUN_REL.simps)
+apply(rule allI | rule impI)+
+sorry
+
 lemma list_eq_refl:
   shows "xs \<approx> xs"
   by (induct xs) (auto intro: list_eq.intros)