--- a/FSet.thy	Tue Dec 01 16:27:42 2009 +0100
+++ b/FSet.thy	Tue Dec 01 18:22:48 2009 +0100
@@ -360,6 +360,13 @@
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 prefer 2
 apply(tactic {* clean_tac @{context} [quot] defs 1 *})
+apply(rule_tac a="\<forall>(P\<Colon>'a fset \<Rightarrow> bool) l\<Colon>'a fset. P EMPTY \<longrightarrow> (\<forall>(a\<Colon>'a) x\<Colon>'a fset. P x \<longrightarrow> P (INSERT a x)) \<longrightarrow> P l" in QUOT_TRUE_i)
+
+apply (drule QT_all)
+apply (drule_tac x = "x" in QT_lam)
+apply (drule QT_all)
+apply (drule_tac x = "y" in QT_lam)
+apply (tactic {* quot_true_tac @{context} (fst o strip_comb) 1 *})
 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *)