--- a/QuotMain.thy	Thu Oct 01 16:10:14 2009 +0200
+++ b/QuotMain.thy	Fri Oct 02 11:10:21 2009 +0200
@@ -703,6 +703,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
@@ -1255,4 +1264,3 @@
 *)
 
 end
-