--- a/QuotMain.thy	Sat Oct 17 14:16:57 2009 +0200
+++ b/QuotMain.thy	Sat Oct 17 15:42:57 2009 +0200
@@ -1282,8 +1282,6 @@
 apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"])
 prefer 2
 (* APPLY_RSP *)
-thm APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op \<approx>" "ABS_fset" "REP_fset" ]
-
 apply (rule_tac ?f="\<lambda>x. h # x" and ?g="\<lambda>x. h # x" in APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op \<approx>" "ABS_fset" "REP_fset"] )
 prefer 3
 apply (rule_tac ?f="op #" and ?g="op #" in APPLY_RSP[of "op =" "id" "id" "op \<approx> ===> op \<approx>" "REP_fset ---> ABS_fset" "ABS_fset ---> REP_fset"])
@@ -1302,6 +1300,15 @@
 apply (assumption)
 prefer 3
 apply (simp)
+(* Mine *)
+apply (simp only: id_def)
+apply (rule IDENTITY_QUOTIENT)
+prefer 2
+apply (rule QUOTIENT_fset)
+prefer 2
+apply (rule QUOTIENT_fset)
+prefer 3
+apply (rule QUOTIENT_fset)
 sorry
 
 thm list.recs(2)