--- a/Quot/Examples/FSet3.thy	Fri Dec 11 15:58:15 2009 +0100
+++ b/Quot/Examples/FSet3.thy	Fri Dec 11 16:32:40 2009 +0100
@@ -22,7 +22,7 @@
 quotient fset = "'a list" / "list_eq"
   by (rule list_eq_equivp)
 
-lemma not_nil_equiv_cons: "[] \<noteq> a # A" sorry
+lemma not_nil_equiv_cons: "\<not>[] \<approx> a # A" sorry
 
 (* The 2 lemmas below are different from the ones in QuotList *)
 lemma nil_rsp[quot_respect]:
@@ -276,4 +276,20 @@
 lemma "funion (funion x xa) xb = funion x (funion xa xb)"
 by (lifting append_assoc)
 
+quotient_def
+  "fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
+as
+  "list_case"
+
+(* NOT SURE IF TRUE *)
+lemma list_case_rsp[quot_respect]:
+  "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"
+  apply (auto)
+  sorry
+
+lemma "fset_case (f1::'t) f2 (Insert a xa) = f2 a xa"
+apply (lifting list.cases(2))
+done
+
+
 end