--- a/FSet.thy	Wed Dec 02 09:23:48 2009 +0100
+++ b/FSet.thy	Wed Dec 02 10:30:20 2009 +0100
@@ -309,6 +309,9 @@
 apply(tactic {* clean_tac @{context} [quot] defs 1*})
 done
 
+lemma QUOT_TRUE_imp: "QUOT_TRUE a \<equiv> QUOT_TRUE b"
+by (simp add: QUOT_TRUE_def)
+
 ML {*
 fun quot_true_tac' ctxt fnctn =
   CSUBGOAL (fn (cgl, i) =>
@@ -378,12 +381,56 @@
 
 ML {* fun inj_repabs_tac_fset' lthy = inj_repabs_tac' lthy rty [quot] [rel_refl] [trans2] *}
 
+ML {*
+fun quot_true_conv1 ctxt fnctn ctrm =
+  case (term_of ctrm) of
+    (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ x)) =>
+    let
+      val _ = tracing "A";
+      val fx = fnctn x;
+      val thy = ProofContext.theory_of ctxt;
+      val cx = cterm_of thy x;
+      val cfx = cterm_of thy fx;
+      val cxt = ctyp_of thy (fastype_of x);
+      val cfxt = ctyp_of thy (fastype_of fx);
+      val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QUOT_TRUE_imp}
+      val _ = tracing (Syntax.string_of_term @{context} (prop_of thm));
+    in
+      Conv.rewr_conv thm ctrm
+    end
+*}
+
+ML {*
+fun quot_true_conv ctxt fnctn ctrm =
+  case (term_of ctrm) of
+    (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) =>
+      quot_true_conv1 ctxt fnctn ctrm
+  | _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm
+  | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm
+  | _ => Conv.all_conv ctrm
+*}
+
+ML CONVERSION
+ML {*
+fun quot_true_tac ctxt fnctn = CONVERSION (
+  fn ctrm => 
+    let
+      val _ = tracing "B";
+      val t = quot_true_conv ctxt fnctn ctrm;
+      val _ = tracing "C";
+    in
+      t
+    end)
+*}
+
 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})
 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 prefer 2
 apply(tactic {* clean_tac @{context} [quot] defs 1 *})
+apply (tactic {* quot_true_tac @{context} (fst o dest_comb) 1 *}) apply(assumption)
+
 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 = (===>) *)