--- a/Quot/Examples/FSet3.thy	Sat Dec 12 04:25:47 2009 +0100
+++ b/Quot/Examples/FSet3.thy	Sat Dec 12 04:48:43 2009 +0100
@@ -54,10 +54,23 @@
 by auto
 
 lemma finite_set_raw_strong_cases:
-  "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a mem Y) \<and> (X \<approx> a # Y)))"
+  "(X = []) \<or> (\<exists>a Y. ((a \<notin> set Y) \<and> (X \<approx> a # Y)))"
   apply (induct X)
+  apply (simp)
+  apply (rule disjI2)
+  apply (erule disjE)
+  apply (rule_tac x="a" in exI)
+  apply (rule_tac x="[]" in exI)
+  apply (simp)
+  apply (erule exE)+
+  apply (case_tac "a = aa")
+  apply (rule_tac x="a" in exI)
+  apply (rule_tac x="Y" in exI)
+  apply (simp)
+  apply (rule_tac x="aa" in exI)
+  apply (rule_tac x="a # Y" in exI)
   apply (auto)
-  sorry
+  done
 
 fun
   delete_raw :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list"