--- a/Quot/Examples/FSet.thy	Tue Dec 08 23:30:47 2009 +0100
+++ b/Quot/Examples/FSet.thy	Tue Dec 08 23:32:54 2009 +0100
@@ -447,6 +447,15 @@
 (* apply (tactic {* procedure_tac @{context} @{thm ttt3} 1 *}) *)
 sorry
 
+(* Always safe to apply, but not too helpful *)
+lemma app_prs2:
+  assumes q1: "Quotient R1 abs1 rep1"
+  and     q2: "Quotient R2 abs2 rep2"
+  shows  "((abs1 ---> rep2) ((rep1 ---> abs2) f) (rep1 x)) = rep2 (((rep1 ---> abs2) f) x)"
+unfolding expand_fun_eq
+using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
+by simp
+
 lemma hard: "(\<lambda>P. \<lambda>Q. P (Q (x::'a list))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a list)))"
 sorry
 
@@ -455,17 +464,26 @@
 defer
 apply(injection)
 apply(subst babs_prs)
-defer defer
+apply(tactic {* quotient_tac @{context} 1 *})
+apply(tactic {* quotient_tac @{context} 1 *})
 apply(subst babs_prs)
-defer defer
+apply(tactic {* quotient_tac @{context} 1 *})
+apply(tactic {* quotient_tac @{context} 1 *})
+apply(subst babs_prs)
+apply(tactic {* quotient_tac @{context} 1 *})
+apply(tactic {* quotient_tac @{context} 1 *})
 apply(subst babs_prs)
-defer defer
-apply(subst babs_prs)
-defer defer
+apply(tactic {* quotient_tac @{context} 1 *})
+apply(tactic {* quotient_tac @{context} 1 *})
+apply(subst all_prs)
+apply(tactic {* quotient_tac @{context} 1 *})
 apply(tactic {* lambda_prs_tac @{context} 1 *})
-(* Until here is ok *)
+apply(subst fun_map.simps)
+apply(tactic {* lambda_prs_tac @{context} 1 *})
+apply(subst fun_map.simps)
+apply(subst fun_map.simps)
+apply(tactic {* lambda_prs_tac @{context} 1 *})
 apply(cleaning)
 sorry
 
-
 end