--- a/LFex.thy	Fri Nov 27 08:22:46 2009 +0100
+++ b/LFex.thy	Fri Nov 27 09:16:32 2009 +0100
@@ -296,13 +296,27 @@
     \<Longrightarrow> P3 (LAM A x M) (LAM A' x' M')\<rbrakk>
 \<Longrightarrow> ((x1 :: KIND) = x2 \<longrightarrow> P1 x1 x2) \<and>
    ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)"
+apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})
+ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
+ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm akind_aty_atrm.induct})) (term_of qtm) *}
 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *})
 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
 prefer 2
-thm QUOTIENT_TY
-apply (tactic {* clean_tac @{context} @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM} defs [] 1 *})
+ML_prf {* val quot = @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM} *}
+apply (tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *})
+apply (tactic {* lambda_prs_tac @{context} quot 1 *})
+ML_prf {* val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot *}
+ML_prf {* val aps_thms = map (applic_prs @{context} absrep) aps *}
+apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] aps_thms) 1 *})
+ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *}
+apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] lower) 1 *})
+ML_prf {* val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot *}
+apply (tactic {* simp_tac (HOL_ss addsimps reps_same) 1 *})
+apply (tactic {* lambda_prs_tac @{context} quot 1 *})
 
 
+apply (tactic {* clean_tac @{context}  defs aps 1 *})
+ML_prf {*  *}
 print_quotients
 apply(tactic {* r_mk_comb_tac' @{context} rty [quot] rel_refl trans2 [] 1*})