--- a/QuotMain.thy	Thu Oct 08 14:27:50 2009 +0200
+++ b/QuotMain.thy	Fri Oct 09 15:03:43 2009 +0200
@@ -542,11 +542,10 @@
   shows "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a memb Y) \<and> (X \<approx> a # Y)))"
   apply (induct X)
   apply (simp)
-  apply (erule disjE)
-  apply (metis QuotMain.m1 list_eq_refl)
-  apply (metis QUOT_TYPE_I_fset.R_sym QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons)
+  apply (metis QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons QuotMain.m1)
   done
 
+
 text {*
   Unabs_def converts a definition given as
 
@@ -1098,12 +1097,57 @@
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
 *}
 ML {* @{term "\<exists>x. P x"} *}
-ML {*  Thm.bicompose *}
-prove aaa: {* (Thm.term_of cgoal2) *}
+
+term "f ---> g"
+term "f ===> g"
+
+definition
+  "rfall p m = (\<forall>x. (p x \<longrightarrow> m x))"
+
+term "ABS_fset"
+term "I"
+
+term "(REP_fset ---> I) ---> I"
+lemma "rfall (Respects ((op \<approx>) ===> (op =)))
+         (((REP_fset ---> id) ---> id)
+             (((ABS_fset ---> id) ---> id)
+               (\<lambda>P.
+                  (ABS_fset ---> id) ((REP_fset ---> id) P)
+                    (REP_fset (ABS_fset [])) \<and>
+                  rfall (Respects (op \<approx>))
+                    ((ABS_fset ---> id)
+                       ((REP_fset ---> id)
+                          (\<lambda>t.
+                             ((ABS_fset ---> id)
+                               ((REP_fset ---> id) P)
+                               (REP_fset (ABS_fset t))) -->
+                             (!h.
+                               (ABS_fset ---> id)
+                                 ((REP_fset ---> id) P)
+                                 (REP_fset
+                                    (ABS_fset
+                                       (h #
+                                            REP_fset
+                                              (ABS_fset t)))))))) -->
+                  rfall (Respects (op \<approx>))
+                    ((ABS_fset ---> id)
+                       ((REP_fset ---> id)
+                          (\<lambda>l.
+                             (ABS_fset ---> id)
+                               ((REP_fset ---> id) P)
+                               (REP_fset (ABS_fset l))))))))"
+
+apply (unfold rfall_def)
+apply (unfold id_def)
+apply (simp add: FUN_MAP_I)
+apply (simp add: QUOT_TYPE_I_fset.thm10)
+.
+
+(*prove aaa: {* (Thm.term_of cgoal2) *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
   apply (atomize(full))
   apply (tactic {* foo_tac' @{context} 1 *})
-  done
+  done*)
 
 (*
 datatype obj1 =