--- a/FSet.thy	Fri Nov 06 19:26:08 2009 +0100
+++ b/FSet.thy	Fri Nov 06 19:26:32 2009 +0100
@@ -148,7 +148,7 @@
   apply (metis QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons m1)
   done
 
-quotient_def 
+quotient_def
   IN :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool"
 where
   "IN \<equiv> membship"
@@ -326,9 +326,12 @@
 where
   "fset_case \<equiv> list_case"
 
+(* Probably not true without additional assumptions about the function *)
 lemma list_rec_rsp:
   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec"
   apply (auto simp add: FUN_REL_EQ)
+  apply (erule_tac list_eq.induct)
+  apply (simp_all)
   sorry
 
 lemma list_case_rsp:
@@ -359,7 +362,7 @@
 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset" *}
 
-
+thm list.recs(2)
 ML {* val t_a = atomize_thm @{thm list.recs(2)} *}
 (* prove {* build_regularize_goal t_a rty rel @{context}  *}
  ML_prf {*  fun tac ctxt = FIRST' [
@@ -405,14 +408,22 @@
 ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *}
 ML {* val lam_prs_thms = map Thm.varifyT lam_prs_thms *}
 ML {* t_t *}
-ML {* val t_l0 = repeat_eqsubst_thm @{context} (lam_prs_thms) t_t *}
-ML {* val t_l = repeat_eqsubst_thm @{context} (app_prs_thms) t_l0 *}
 ML {* val (alls, exs) = findallex @{context} rty qty (prop_of t_a); *}
 ML {* val allthms = map (make_allex_prs_thm @{context} quot @{thm FORALL_PRS}) alls *}
-ML {* val t_a = MetaSimplifier.rewrite_rule (allthms) t_l *}
+ML {* val t_a = MetaSimplifier.rewrite_rule (allthms) t_t *}
+ML {* val t_l0 = repeat_eqsubst_thm @{context} (app_prs_thms) t_a *}
+ML {* val iitt = Drule.eta_contraction_rule (hd (tl lam_prs_thms)) *}
+ML {* val iitt = (hd (lam_prs_thms)) *}
+
+ML {* val t_l0 = repeat_eqsubst_thm @{context} [iitt] t_a *}
+ML {* val t_l0 = repeat_eqsubst_thm @{context} ([hd (tl lam_prs_thms)]) t_a *}
+ML {* val t_l = repeat_eqsubst_thm @{context} (lam_prs_thms) t_l0 *}
 ML {* val defs_sym = flat (map (add_lower_defs @{context}) defs) *}
-ML {* val t_id = simp_ids @{context} t_a *}
+ML t_l0
+ML {* val t_id = simp_ids @{context} t_l0 *}
 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_id *}
+ML {* val t_l = repeat_eqsubst_thm @{context} (lam_prs_thms) t_d *}
+
 ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_d *}
 ML {* ObjectLogic.rulify t_s *}