--- a/Quot/Examples/AbsRepTest.thy	Thu Jan 07 10:13:15 2010 +0100
+++ b/Quot/Examples/AbsRepTest.thy	Thu Jan 07 10:55:20 2010 +0100
@@ -190,6 +190,16 @@
 apply (metis equivp_def fset_equivp)
 apply (subgoal_tac "map abs_fset r \<approx>1 map abs_fset s")
 apply (metis Quotient_rel[OF Quotient_fset])
+apply (auto)[1]
+apply (subgoal_tac "map abs_fset r = map abs_fset b")
+prefer 2
+apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]])
+apply (subgoal_tac "map abs_fset s = map abs_fset ba")
+prefer 2
+apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]])
+apply simp
+(* To solve first subgoal we just need: *)
+(* b \<approx> ba \<Longrightarrow> mapabs b \<approx> mapabs ba *)
 prefer 2
 apply rule
 apply (rule rep_abs_rsp[of "list_rel op \<approx>1" "map abs_fset"])
@@ -202,6 +212,12 @@
 apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})
 apply (rule list_rel_refl)
 apply (metis equivp_def fset_equivp)
+apply (erule conjE)+
+apply (subgoal_tac "map abs_fset r \<approx>1 map abs_fset s")
+prefer 2
+apply (metis Quotient_def Quotient_fset equivp_reflp fset_equivp)
+(* To solve this subgoal we just need: *)
+(* x \<approx> y \<Longrightarrow> maprep x \<approx> maprep y *)
 sorry
 
 lemma quotient_compose_list: