# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1267003559 -3600
# Node ID 38eb2bd9ad3a0771825a0f25bed824b65a1e054e
# Parent  ca3c69545a7819fb239ba599c30894349d6b63c9
LF renaming part 3 (proper names of alpha equvalences)

diff -r ca3c69545a78 -r 38eb2bd9ad3a Quot/Nominal/LFex.thy
--- a/Quot/Nominal/LFex.thy	Wed Feb 24 10:08:54 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Wed Feb 24 10:25:59 2010 +0100
@@ -69,7 +69,7 @@
    [ [[]], [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]]]] *}
 notation
     alpha_rkind  ("_ \<approx>ki _" [100, 100] 100)
-and alpha_rty    ("_ \<approx>rty _" [100, 100] 100)
+and alpha_rty    ("_ \<approx>ty _" [100, 100] 100)
 and alpha_rtrm   ("_ \<approx>tr _" [100, 100] 100)
 thm fv_rkind_fv_rty_fv_rtrm.simps alpha_rkind_alpha_rty_alpha_rtrm.intros
 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alphas_inj}, []), (build_alpha_inj @{thms alpha_rkind_alpha_rty_alpha_rtrm.intros} @{thms rkind.distinct rty.distinct rtrm.distinct rkind.inject rty.inject rtrm.inject} @{thms alpha_rkind.cases alpha_rty.cases alpha_rtrm.cases} ctxt)) ctxt)) *}
@@ -107,56 +107,56 @@
 | "fv_rtrm (Lam A x M) = (fv_rty A) \<union> ((fv_rtrm M) - {atom x})"
 
 inductive
-    arkind :: "rkind \<Rightarrow> rkind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100)
-and arty   :: "rty \<Rightarrow> rty \<Rightarrow> bool"     ("_ \<approx>rty _" [100, 100] 100)
-and artrm  :: "rtrm \<Rightarrow> rtrm \<Rightarrow> bool"   ("_ \<approx>tr _" [100, 100] 100)
+    alpha_rkind :: "rkind \<Rightarrow> rkind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100)
+and alpha_rty   :: "rty \<Rightarrow> rty \<Rightarrow> bool"     ("_ \<approx>ty _" [100, 100] 100)
+and alpha_rtrm  :: "rtrm \<Rightarrow> rtrm \<Rightarrow> bool"   ("_ \<approx>tr _" [100, 100] 100)
 where
   a1: "(Type) \<approx>ki (Type)"
-| a2: "\<lbrakk>A \<approx>rty A'; \<exists>pi. (({atom a}, K) \<approx>gen arkind fv_rkind pi ({atom b}, K'))\<rbrakk> \<Longrightarrow> (KPi A a K) \<approx>ki (KPi A' b K')"
-| a3: "i = j \<Longrightarrow> (TConst i) \<approx>rty (TConst j)"
-| a4: "\<lbrakk>A \<approx>rty A'; M \<approx>tr M'\<rbrakk> \<Longrightarrow> (TApp A M) \<approx>rty (TApp A' M')"
-| a5: "\<lbrakk>A \<approx>rty A'; \<exists>pi. (({atom a}, B) \<approx>gen arty fv_rty pi ({atom b}, B'))\<rbrakk> \<Longrightarrow> (TPi A a B) \<approx>rty (TPi A' b B')"
+| a2: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (({atom a}, K) \<approx>gen alpha_rkind fv_rkind pi ({atom b}, K'))\<rbrakk> \<Longrightarrow> (KPi A a K) \<approx>ki (KPi A' b K')"
+| a3: "i = j \<Longrightarrow> (TConst i) \<approx>ty (TConst j)"
+| a4: "\<lbrakk>A \<approx>ty A'; M \<approx>tr M'\<rbrakk> \<Longrightarrow> (TApp A M) \<approx>ty (TApp A' M')"
+| a5: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (({atom a}, B) \<approx>gen alpha_rty fv_rty pi ({atom b}, B'))\<rbrakk> \<Longrightarrow> (TPi A a B) \<approx>ty (TPi A' b B')"
 | a6: "i = j \<Longrightarrow> (Const i) \<approx>tr (Const j)"
 | a7: "x = y \<Longrightarrow> (Var x) \<approx>tr (Var y)"
 | a8: "\<lbrakk>M \<approx>tr M'; N \<approx>tr N'\<rbrakk> \<Longrightarrow> (App M N) \<approx>tr (App M' N')"
-| a9: "\<lbrakk>A \<approx>rty A'; \<exists>pi. (({atom a}, M) \<approx>gen artrm fv_rtrm pi ({atom b}, M'))\<rbrakk> \<Longrightarrow> (Lam A a M) \<approx>tr (Lam A' b M')"
+| a9: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (({atom a}, M) \<approx>gen alpha_rtrm fv_rtrm pi ({atom b}, M'))\<rbrakk> \<Longrightarrow> (Lam A a M) \<approx>tr (Lam A' b M')"
 
-lemma arkind_arty_artrm_inj:
+lemma alpha_rkind_alpha_rty_alpha_rtrm_inj:
   "(Type) \<approx>ki (Type) = True"
-  "((KPi A a K) \<approx>ki (KPi A' b K')) = ((A \<approx>rty A') \<and> (\<exists>pi. ({atom a}, K) \<approx>gen arkind fv_rkind pi ({atom b}, K')))"
-  "(TConst i) \<approx>rty (TConst j) = (i = j)"
-  "(TApp A M) \<approx>rty (TApp A' M') = (A \<approx>rty A' \<and> M \<approx>tr M')"
-  "((TPi A a B) \<approx>rty (TPi A' b B')) = ((A \<approx>rty A') \<and> (\<exists>pi. (({atom a}, B) \<approx>gen arty fv_rty pi ({atom b}, B'))))"
+  "((KPi A a K) \<approx>ki (KPi A' b K')) = ((A \<approx>ty A') \<and> (\<exists>pi. ({atom a}, K) \<approx>gen alpha_rkind fv_rkind pi ({atom b}, K')))"
+  "(TConst i) \<approx>ty (TConst j) = (i = j)"
+  "(TApp A M) \<approx>ty (TApp A' M') = (A \<approx>ty A' \<and> M \<approx>tr M')"
+  "((TPi A a B) \<approx>ty (TPi A' b B')) = ((A \<approx>ty A') \<and> (\<exists>pi. (({atom a}, B) \<approx>gen alpha_rty fv_rty pi ({atom b}, B'))))"
   "(Const i) \<approx>tr (Const j) = (i = j)"
   "(Var x) \<approx>tr (Var y) = (x = y)"
   "(App M N) \<approx>tr (App M' N') = (M \<approx>tr M' \<and> N \<approx>tr N')"
-  "((Lam A a M) \<approx>tr (Lam A' b M')) = ((A \<approx>rty A') \<and> (\<exists>pi. (({atom a}, M) \<approx>gen artrm fv_rtrm pi ({atom b}, M'))))"
+  "((Lam A a M) \<approx>tr (Lam A' b M')) = ((A \<approx>ty A') \<and> (\<exists>pi. (({atom a}, M) \<approx>gen alpha_rtrm fv_rtrm pi ({atom b}, M'))))"
 apply -
-apply (simp add: arkind_arty_artrm.intros)
+apply (simp add: alpha_rkind_alpha_rty_alpha_rtrm.intros)
 
-apply rule apply (erule arkind.cases) apply simp apply blast
-apply (simp only: arkind_arty_artrm.intros)
+apply rule apply (erule alpha_rkind.cases) apply simp apply blast
+apply (simp only: alpha_rkind_alpha_rty_alpha_rtrm.intros)
 
-apply rule apply (erule arty.cases) apply simp apply simp apply simp
-apply (simp only: arkind_arty_artrm.intros)
+apply rule apply (erule alpha_rty.cases) apply simp apply simp apply simp
+apply (simp only: alpha_rkind_alpha_rty_alpha_rtrm.intros)
 
-apply rule apply (erule arty.cases) apply simp apply simp apply simp
-apply (simp only: arkind_arty_artrm.intros)
+apply rule apply (erule alpha_rty.cases) apply simp apply simp apply simp
+apply (simp only: alpha_rkind_alpha_rty_alpha_rtrm.intros)
 
-apply rule apply (erule arty.cases) apply simp apply simp apply blast
-apply (simp only: arkind_arty_artrm.intros)
+apply rule apply (erule alpha_rty.cases) apply simp apply simp apply blast
+apply (simp only: alpha_rkind_alpha_rty_alpha_rtrm.intros)
 
-apply rule apply (erule artrm.cases) apply simp apply simp apply simp apply blast
-apply (simp only: arkind_arty_artrm.intros)
+apply rule apply (erule alpha_rtrm.cases) apply simp apply simp apply simp apply blast
+apply (simp only: alpha_rkind_alpha_rty_alpha_rtrm.intros)
 
-apply rule apply (erule artrm.cases) apply simp apply simp apply simp apply blast
-apply (simp only: arkind_arty_artrm.intros)
+apply rule apply (erule alpha_rtrm.cases) apply simp apply simp apply simp apply blast
+apply (simp only: alpha_rkind_alpha_rty_alpha_rtrm.intros)
 
-apply rule apply (erule artrm.cases) apply simp apply simp apply simp apply blast
-apply (simp only: arkind_arty_artrm.intros)
+apply rule apply (erule alpha_rtrm.cases) apply simp apply simp apply simp apply blast
+apply (simp only: alpha_rkind_alpha_rty_alpha_rtrm.intros)
 
-apply rule apply (erule artrm.cases) apply simp apply simp apply simp apply blast
-apply (simp only: arkind_arty_artrm.intros)
+apply rule apply (erule alpha_rtrm.cases) apply simp apply simp apply simp apply blast
+apply (simp only: alpha_rkind_alpha_rty_alpha_rtrm.intros)
 done
 
 lemma rfv_eqvt[eqvt]:
@@ -170,11 +170,11 @@
 
 lemma alpha_eqvt:
   "t1 \<approx>ki s1 \<Longrightarrow> (pi \<bullet> t1) \<approx>ki (pi \<bullet> s1)"
-  "t2 \<approx>rty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>rty (pi \<bullet> s2)"
+  "t2 \<approx>ty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>ty (pi \<bullet> s2)"
   "t3 \<approx>tr s3 \<Longrightarrow> (pi \<bullet> t3) \<approx>tr (pi \<bullet> s3)"
-apply(induct rule: arkind_arty_artrm.inducts)
-apply (simp_all add: arkind_arty_artrm.intros)
-apply (simp_all add: arkind_arty_artrm_inj)
+apply(induct rule: alpha_rkind_alpha_rty_alpha_rtrm.inducts)
+apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros)
+apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm_inj)
 apply (rule alpha_gen_atom_eqvt)
 apply (simp add: rfv_eqvt)
 apply assumption
@@ -191,19 +191,19 @@
   and   A::"rty"
   and   M::"rtrm"
   shows "K \<approx>ki K"
-  and   "A \<approx>rty A"
+  and   "A \<approx>ty A"
   and   "M \<approx>tr M"
   apply(induct K and A and M rule: rkind_rty_rtrm.inducts)
-  apply(auto intro: arkind_arty_artrm.intros)
-  apply (rule a2)
+  apply(auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros)
+  apply (rule alpha_rkind_alpha_rty_alpha_rtrm.intros(2))
   apply auto
   apply(rule_tac x="0" in exI)
   apply(simp_all add: fresh_star_def fresh_zero_perm alpha_gen)
-  apply (rule a5)
+  apply (rule alpha_rkind_alpha_rty_alpha_rtrm.intros(5))
   apply auto
   apply(rule_tac x="0" in exI)
   apply(simp_all add: fresh_star_def fresh_zero_perm alpha_gen)
-  apply (rule a9)
+  apply (rule alpha_rkind_alpha_rty_alpha_rtrm.intros(9))
   apply auto
   apply(rule_tac x="0" in exI)
   apply(simp_all add: fresh_star_def fresh_zero_perm alpha_gen)
@@ -212,11 +212,11 @@
 lemma al_sym:
   fixes K K'::"rkind" and A A'::"rty" and M M'::"rtrm"
   shows "K \<approx>ki K' \<Longrightarrow> K' \<approx>ki K"
-  and   "A \<approx>rty A' \<Longrightarrow> A' \<approx>rty A"
+  and   "A \<approx>ty A' \<Longrightarrow> A' \<approx>ty A"
   and   "M \<approx>tr M' \<Longrightarrow> M' \<approx>tr M"
-  apply(induct K K' and A A' and M M' rule: arkind_arty_artrm.inducts)
-  apply(simp_all add: arkind_arty_artrm.intros)
-  apply (simp_all add: arkind_arty_artrm_inj)
+  apply(induct K K' and A A' and M M' rule: alpha_rkind_alpha_rty_alpha_rtrm.inducts)
+  apply(simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros)
+  apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm_inj)
   apply(erule alpha_gen_compose_sym)
   apply(erule alpha_eqvt)
   apply(erule alpha_gen_compose_sym)
@@ -228,42 +228,42 @@
 lemma al_trans:
   fixes K K' K''::"rkind" and A A' A''::"rty" and M M' M''::"rtrm"
   shows "K \<approx>ki K' \<Longrightarrow> K' \<approx>ki K'' \<Longrightarrow> K \<approx>ki K''"
-  and   "A \<approx>rty A' \<Longrightarrow> A' \<approx>rty A'' \<Longrightarrow> A \<approx>rty A''"
+  and   "A \<approx>ty A' \<Longrightarrow> A' \<approx>ty A'' \<Longrightarrow> A \<approx>ty A''"
   and   "M \<approx>tr M' \<Longrightarrow> M' \<approx>tr M'' \<Longrightarrow> M \<approx>tr M''"
-  apply(induct K K' and A A' and M M' arbitrary: K'' and A'' and M'' rule: arkind_arty_artrm.inducts)
-  apply(simp_all add: arkind_arty_artrm.intros)
-  apply(erule arkind.cases)
-  apply(simp_all add: arkind_arty_artrm.intros)
-  apply(simp add: arkind_arty_artrm_inj)
+  apply(induct K K' and A A' and M M' arbitrary: K'' and A'' and M'' rule: alpha_rkind_alpha_rty_alpha_rtrm.inducts)
+  apply(simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros)
+  apply(erule alpha_rkind.cases)
+  apply(simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros)
+  apply(simp add: alpha_rkind_alpha_rty_alpha_rtrm_inj)
   apply(erule alpha_gen_compose_trans)
   apply(assumption)
   apply(erule alpha_eqvt)
   apply(rotate_tac 4)
-  apply(erule arty.cases)
-  apply(simp_all add: arkind_arty_artrm.intros)
+  apply(erule alpha_rty.cases)
+  apply(simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros)
   apply(rotate_tac 3)
-  apply(erule arty.cases)
-  apply(simp_all add: arkind_arty_artrm.intros)
-  apply(simp add: arkind_arty_artrm_inj)
+  apply(erule alpha_rty.cases)
+  apply(simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros)
+  apply(simp add: alpha_rkind_alpha_rty_alpha_rtrm_inj)
   apply(erule alpha_gen_compose_trans)
   apply(assumption)
   apply(erule alpha_eqvt)
   apply(rotate_tac 4)
-  apply(erule artrm.cases)
-  apply(simp_all add: arkind_arty_artrm.intros)
+  apply(erule alpha_rtrm.cases)
+  apply(simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros)
   apply(rotate_tac 3)
-  apply(erule artrm.cases)
-  apply(simp_all add: arkind_arty_artrm.intros)
-  apply(simp add: arkind_arty_artrm_inj)
+  apply(erule alpha_rtrm.cases)
+  apply(simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros)
+  apply(simp add: alpha_rkind_alpha_rty_alpha_rtrm_inj)
   apply(erule alpha_gen_compose_trans)
   apply(assumption)
   apply(erule alpha_eqvt)
   done
 
 lemma alpha_equivps:
-  shows "equivp arkind"
-  and   "equivp arty"
-  and   "equivp artrm"
+  shows "equivp alpha_rkind"
+  and   "equivp alpha_rty"
+  and   "equivp alpha_rtrm"
   apply(rule equivpI)
   unfolding reflp_def symp_def transp_def
   apply(auto intro: al_refl al_sym al_trans)
@@ -275,12 +275,12 @@
   apply(auto intro: al_refl al_sym al_trans)
   done
 
-quotient_type RKIND = rkind / arkind
+quotient_type RKIND = rkind / alpha_rkind
   by (rule alpha_equivps)
 
 quotient_type
-    RTY = rty / arty and
-    RTRM = rtrm / artrm
+    RTY = rty / alpha_rty and
+    RTRM = rtrm / alpha_rtrm
   by (auto intro: alpha_equivps)
 
 quotient_definition
@@ -347,65 +347,65 @@
 
 lemma alpha_rfv:
   shows "(t \<approx>ki s \<longrightarrow> fv_rkind t = fv_rkind s) \<and>
-     (t1 \<approx>rty s1 \<longrightarrow> fv_rty t1 = fv_rty s1) \<and>
+     (t1 \<approx>ty s1 \<longrightarrow> fv_rty t1 = fv_rty s1) \<and>
      (t2 \<approx>tr s2 \<longrightarrow> fv_rtrm t2 = fv_rtrm s2)"
-  apply(rule arkind_arty_artrm.induct)
+  apply(rule alpha_rkind_alpha_rty_alpha_rtrm.induct)
   apply(simp_all add: alpha_gen)
   done
 
 lemma perm_rsp[quot_respect]:
-  "(op = ===> arkind ===> arkind) permute permute"
-  "(op = ===> arty ===> arty) permute permute"
-  "(op = ===> artrm ===> artrm) permute permute"
+  "(op = ===> alpha_rkind ===> alpha_rkind) permute permute"
+  "(op = ===> alpha_rty ===> alpha_rty) permute permute"
+  "(op = ===> alpha_rtrm ===> alpha_rtrm) permute permute"
   by (simp_all add:alpha_eqvt)
 
 lemma tconst_rsp[quot_respect]: 
-  "(op = ===> arty) TConst TConst"
-  apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
+  "(op = ===> alpha_rty) TConst TConst"
+  apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros) done
 lemma tapp_rsp[quot_respect]: 
-  "(arty ===> artrm ===> arty) TApp TApp" 
-  apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
+  "(alpha_rty ===> alpha_rtrm ===> alpha_rty) TApp TApp" 
+  apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros) done
 lemma var_rsp[quot_respect]: 
-  "(op = ===> artrm) Var Var"
-  apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
+  "(op = ===> alpha_rtrm) Var Var"
+  apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros) done
 lemma app_rsp[quot_respect]: 
-  "(artrm ===> artrm ===> artrm) App App"
-  apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
+  "(alpha_rtrm ===> alpha_rtrm ===> alpha_rtrm) App App"
+  apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros) done
 lemma const_rsp[quot_respect]: 
-  "(op = ===> artrm) Const Const"
-  apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9) done
+  "(op = ===> alpha_rtrm) Const Const"
+  apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros) done
 
 lemma kpi_rsp[quot_respect]: 
-  "(arty ===> op = ===> arkind ===> arkind) KPi KPi"
-  apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9)
-  apply (rule a2) apply assumption
+  "(alpha_rty ===> op = ===> alpha_rkind ===> alpha_rkind) KPi KPi"
+  apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros)
+  apply (rule alpha_rkind_alpha_rty_alpha_rtrm.intros(2)) apply simp_all
   apply (rule_tac x="0" in exI)
   apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen)
   done
 
 lemma tpi_rsp[quot_respect]: 
-  "(arty ===> op = ===> arty ===> arty) TPi TPi"
-  apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9)
-  apply (rule a5) apply assumption
+  "(alpha_rty ===> op = ===> alpha_rty ===> alpha_rty) TPi TPi"
+  apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros)
+  apply (rule alpha_rkind_alpha_rty_alpha_rtrm.intros(5)) apply simp_all
   apply (rule_tac x="0" in exI)
   apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen)
   done
 lemma lam_rsp[quot_respect]: 
-  "(arty ===> op = ===> artrm ===> artrm) Lam Lam"
-  apply (auto intro: a1 a2 a3 a4 a5 a6 a7 a8 a9)
-  apply (rule a9) apply assumption
+  "(alpha_rty ===> op = ===> alpha_rtrm ===> alpha_rtrm) Lam Lam"
+  apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros)
+  apply (rule alpha_rkind_alpha_rty_alpha_rtrm.intros(9)) apply simp_all
   apply (rule_tac x="0" in exI)
   apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen)
   done
 
 lemma fv_rty_rsp[quot_respect]: 
-  "(arty ===> op =) fv_rty fv_rty"
+  "(alpha_rty ===> op =) fv_rty fv_rty"
   by (simp add: alpha_rfv)
 lemma fv_rkind_rsp[quot_respect]:
-  "(arkind ===> op =) fv_rkind fv_rkind"
+  "(alpha_rkind ===> op =) fv_rkind fv_rkind"
   by (simp add: alpha_rfv)
 lemma fv_rtrm_rsp[quot_respect]:
-  "(artrm ===> op =) fv_rtrm fv_rtrm"
+  "(alpha_rtrm ===> op =) fv_rtrm fv_rtrm"
   by (simp add: alpha_rfv)
 
 thm rkind_rty_rtrm.induct
@@ -454,9 +454,9 @@
 
 end
 
-lemmas ARKIND_ARTY_ARTRM_inducts = arkind_arty_artrm.inducts[unfolded alpha_gen, quot_lifted, folded alpha_gen]
+lemmas ALPHA_RKIND_ALPHA_RTY_ALPHA_RTRM_inducts = alpha_rkind_alpha_rty_alpha_rtrm.inducts[unfolded alpha_gen, quot_lifted, folded alpha_gen]
 
-lemmas RKIND_RTY_RTRM_INJECT = arkind_arty_artrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
+lemmas RKIND_RTY_RTRM_INJECT = alpha_rkind_alpha_rty_alpha_rtrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
 
 lemmas fv_kind_ty_trm = fv_rkind_fv_rty_fv_rtrm.simps[quot_lifted]