diff -r 75af61f32ece -r f1c0a66284d3 LFex.thy
--- a/LFex.thy	Sat Nov 28 14:15:05 2009 +0100
+++ b/LFex.thy	Sat Nov 28 14:33:04 2009 +0100
@@ -269,197 +269,197 @@
   val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) @{thms alpha_EQUIVs}
   val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) @{thms alpha_EQUIVs}
 *}
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 @{thms kpi_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 @{thms perm_kind_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 @{thms perm_kind_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 @{thms kpi_rsp fv_ty_rsp fv_kind_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tconst_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tapp_rsp}) 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tapp_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tpi_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms perm_ty_rsp tpi_rsp fv_ty_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 @{thms const_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 @{thms var_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 @{thms app_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 @{thms lam_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 @{thms perm_trm_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 @{thms perm_trm_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 @{thms fv_trm_rsp lam_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 []) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 @{thms kpi_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 @{thms perm_kind_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 @{thms perm_kind_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 @{thms kpi_rsp fv_ty_rsp fv_kind_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tconst_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tapp_rsp}) 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tapp_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tpi_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms perm_ty_rsp tpi_rsp fv_ty_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms const_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms var_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms app_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms lam_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms perm_trm_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms perm_trm_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms fv_trm_rsp lam_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 []) 1*})
 done
 
 print_quotients