--- a/QuotMain.thy	Sat Oct 17 11:54:50 2009 +0200
+++ b/QuotMain.thy	Sat Oct 17 12:20:56 2009 +0200
@@ -1317,9 +1317,26 @@
 ML_prf {* man_inst_norm *}
 apply (tactic {* compose_tac (false, man_inst_norm, 4) 1 *})
 
-
+(* MINE *)
+apply (rule QUOTIENT_fset)
 
-
+prefer 3
+(* ABS_REP_RSP *)
+thm REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"]
+apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"])
+(* MINE *)
+apply (rule QUOTIENT_fset)
+(* MINE *)
+apply (rule list_eq_refl )
+prefer 2
+(* ABS_REP_RSP *)
+apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"])
+prefer 2
+(* MINE *)
+apply (simp only: FUN_REL.simps)
+prefer 3
+(* APPLY_RSP *)
+thm APPLY_RSP
 sorry
 
 thm list.recs(2)