--- a/QuotMain.thy	Wed Sep 30 16:57:09 2009 +0200
+++ b/QuotMain.thy	Fri Oct 02 11:09:33 2009 +0200
@@ -702,6 +702,15 @@
   shows "(z # xs) \<approx> (z # ys)"
   using a by (rule QuotMain.list_eq.intros(5))
 
+lemma fs1_strong_cases:
+  fixes X :: "'a list"
+  shows "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a memb Y) \<and> (X \<approx> a # Y)))"
+  apply (induct X)
+  apply (simp)
+  apply (erule disjE)
+  apply (metis QuotMain.m1 list_eq_refl)
+  apply (metis QUOT_TYPE_I_fset.R_sym QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons)
+  done
 
 text {*
   Unlam_def converts a definition given as
@@ -1254,4 +1263,3 @@
 *)
 
 end
-