--- a/FSet.thy	Thu Nov 05 16:43:57 2009 +0100
+++ b/FSet.thy	Fri Nov 06 11:01:22 2009 +0100
@@ -122,13 +122,17 @@
 apply (metis QUOT_TYPE_I_fset.R_trans card1_cons list_eq_refl mem_cons)
 done
 
+definition
+  rsp_fold
+where
+  "rsp_fold f = ((!u v. (f u v = f v u)) \<and> (!u v w. ((f u (f v w) = f (f u v) w))))"
+
 primrec
   fold1
 where
   "fold1 f (g :: 'a \<Rightarrow> 'b) (z :: 'b) [] = z"
 | "fold1 f g z (a # A) =
-     (if ((!u v. (f u v = f v u))
-      \<and> (!u v w. ((f u (f v w) = f (f u v) w))))
+     (if rsp_fold f
      then (
        if (a memb A) then (fold1 f g z A) else (f (g a) (fold1 f g z A))
      ) else z)"
@@ -271,18 +275,25 @@
   done
 
 lemma ho_map_rsp:
-  "((op = ===> op =) ===> op \<approx> ===> op \<approx>) map map"
-  by (simp add: FUN_REL_EQ map_rsp)
+  "(op = ===> op \<approx> ===> op \<approx>) map map"
+  by (simp add: map_rsp)
 
-lemma map_append :
+lemma map_append:
   "(map f (a @ b)) \<approx>
   (map f a) @ (map f b)"
  by simp (rule list_eq_refl)
 
 lemma ho_fold_rsp:
-  "((op = ===> op = ===> op =) ===> (op = ===> op =) ===> op = ===> op \<approx> ===> op =) fold1 fold1"
+  "(op = ===> op = ===> op = ===> op \<approx> ===> op =) fold1 fold1"
   apply (auto simp add: FUN_REL_EQ)
-sorry
+  apply (case_tac "rsp_fold x")
+  prefer 2
+  apply (erule_tac list_eq.induct)
+  apply (simp_all)
+  apply (erule_tac list_eq.induct)
+  apply (simp_all)
+  apply (auto simp add: memb_rsp rsp_fold_def)
+done
 
 print_quotients