--- a/LFex.thy	Sun Nov 29 02:51:42 2009 +0100
+++ b/LFex.thy	Sun Nov 29 03:59:18 2009 +0100
@@ -181,22 +181,36 @@
   "perm_trm \<equiv> (perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)"
 
 (* TODO/FIXME: Think whether these RSP theorems are true. *)
-lemma kpi_rsp: "(aty ===> op = ===> akind ===> akind) KPi KPi" sorry
-lemma tconst_rsp: "(op = ===> aty) TConst TConst" sorry
-lemma tapp_rsp: "(aty ===> atrm ===> aty) TApp TApp" sorry
-lemma tpi_rsp: "(aty ===> op = ===> aty ===> aty) TPi TPi" sorry
-lemma var_rsp: "(op = ===> atrm) Var Var" sorry
-lemma app_rsp: "(atrm ===> atrm ===> atrm) App App" sorry
-lemma const_rsp: "(op = ===> atrm) Const Const" sorry
-lemma lam_rsp: "(aty ===> op = ===> atrm ===> atrm) Lam Lam" sorry
+lemma kpi_rsp[quot_rsp]: 
+  "(aty ===> op = ===> akind ===> akind) KPi KPi" sorry
+lemma tconst_rsp[quot_rsp]: 
+  "(op = ===> aty) TConst TConst" sorry
+lemma tapp_rsp[quot_rsp]: 
+  "(aty ===> atrm ===> aty) TApp TApp" sorry
+lemma tpi_rsp[quot_rsp]: 
+  "(aty ===> op = ===> aty ===> aty) TPi TPi" sorry
+lemma var_rsp[quot_rsp]: 
+  "(op = ===> atrm) Var Var" sorry
+lemma app_rsp[quot_rsp]: 
+  "(atrm ===> atrm ===> atrm) App App" sorry
+lemma const_rsp[quot_rsp]: 
+  "(op = ===> atrm) Const Const" sorry
+lemma lam_rsp[quot_rsp]: 
+  "(aty ===> op = ===> atrm ===> atrm) Lam Lam" sorry
 
-lemma perm_kind_rsp: "(op = ===> akind ===> akind) op \<bullet> op \<bullet>" sorry
-lemma perm_ty_rsp: "(op = ===> aty ===> aty) op \<bullet> op \<bullet>" sorry
-lemma perm_trm_rsp: "(op = ===> atrm ===> atrm) op \<bullet> op \<bullet>" sorry
+lemma perm_kind_rsp[quot_rsp]: 
+  "(op = ===> akind ===> akind) op \<bullet> op \<bullet>" sorry
+lemma perm_ty_rsp[quot_rsp]: 
+  "(op = ===> aty ===> aty) op \<bullet> op \<bullet>" sorry
+lemma perm_trm_rsp[quot_rsp]: 
+  "(op = ===> atrm ===> atrm) op \<bullet> op \<bullet>" sorry
 
-lemma fv_ty_rsp: "(aty ===> op =) fv_ty fv_ty" sorry
-lemma fv_kind_rsp: "(akind ===> op =) fv_kind fv_kind" sorry
-lemma fv_trm_rsp: "(atrm ===> op =) fv_trm fv_trm" sorry
+lemma fv_ty_rsp[quot_rsp]: 
+  "(aty ===> op =) fv_ty fv_ty" sorry
+lemma fv_kind_rsp[quot_rsp]: 
+  "(akind ===> op =) fv_kind fv_kind" sorry
+lemma fv_trm_rsp[quot_rsp]: 
+  "(atrm ===> op =) fv_trm fv_trm" sorry
 
 
 thm akind_aty_atrm.induct
@@ -269,197 +283,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 {* 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 {* all_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 {* all_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 {* all_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 {* all_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 {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* all_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 {* all_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 {* all_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 {* all_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 {* all_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 {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp} 1*})
-apply(tactic {* all_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 {* all_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 {* all_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 {* all_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 {* all_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 {* all_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 {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp} 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tapp_rsp} 1*})
-apply(tactic {* all_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 {* all_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 {* all_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 {* all_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 {* all_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 {* all_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 {* all_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 {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* all_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 {* all_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 {* all_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 {* all_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 {* all_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 {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp} 1*})
-apply(tactic {* all_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 {* all_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 {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* all_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 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 {* all_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 {* all_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 {* all_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 {* all_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 {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
+apply(tactic {* all_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 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 {* all_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 {* all_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 {* all_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 {* all_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 {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
+apply(tactic {* all_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 {* all_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 {* 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 {* all_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 {* all_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 {* all_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 {* all_inj_repabs_tac @{context} @{typ trm} 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 {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
+apply(tactic {* all_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 {* all_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 {* all_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 {* all_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 {* all_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 {* all_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 {* 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 {* all_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 {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2  1*})
+apply(tactic {* all_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 {* 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 {* all_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 {* all_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 {* all_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 {* all_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 {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
+apply(tactic {* all_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 {* all_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 {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2  1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2  1*})
 done
 
 print_quotients