--- a/Quot/Examples/FSet3.thy	Fri Dec 11 16:32:40 2009 +0100
+++ b/Quot/Examples/FSet3.thy	Fri Dec 11 17:19:38 2009 +0100
@@ -22,7 +22,8 @@
 quotient fset = "'a list" / "list_eq"
   by (rule list_eq_equivp)
 
-lemma not_nil_equiv_cons: "\<not>[] \<approx> a # A" sorry
+lemma not_nil_equiv_cons: "\<not>[] \<approx> a # A"
+unfolding list_eq_def by auto
 
 (* The 2 lemmas below are different from the ones in QuotList *)
 lemma nil_rsp[quot_respect]: