--- a/FSet.thy	Fri Nov 27 04:02:20 2009 +0100
+++ b/FSet.thy	Fri Nov 27 07:00:14 2009 +0100
@@ -345,58 +345,11 @@
 
 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *})
-apply(rule cheat)
+apply(tactic {* regularize_tac @{context} [rel_eqv] rel_refl 1 *})
 prefer 2
-apply(rule cheat)
+apply (tactic {* clean_tac @{context} quot defs reps_same absrep [(@{typ "('a list \<Rightarrow> bool)"},@{typ "('a fset \<Rightarrow> bool)"})] 1 *})
 apply(tactic {* r_mk_comb_tac' @{context} rty quot rel_refl trans2 rsp_thms 1*})
-thm RES_FORALL_RSP
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
-sorry
+done
 
 quotient_def
   fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"