--- a/Quot/Nominal/Terms.thy	Tue Feb 09 17:05:07 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Tue Feb 09 17:24:08 2010 +0100
@@ -1023,6 +1023,11 @@
 as
   "rbv6"
 
+lemma [quot_respect]:
+  "(op = ===> alpha1 ===> alpha1) permute permute"
+apply auto (* eqvt *)
+sorry
+
 lemma [quot_respect]:"(alpha6 ===> op =) rbv6 rbv6"
 apply simp apply clarify
 apply (erule alpha6.induct)
@@ -1030,10 +1035,16 @@
 apply simp
 apply (erule exE)
 apply (simp add: alpha_gen)
-sorry
+oops
 
 lemma [quot_respect]:"(alpha6 ===> op =) rfv_trm6 rfv_trm6"
-sorry
+apply simp apply clarify
+apply (induct_tac x y rule: alpha6.induct)
+apply simp_all
+apply (erule exE)
+apply (simp add: alpha_gen)
+apply (erule conjE)+
+oops
 
 lemma [quot_respect]:
  "(op = ===> alpha6) rVr6 rVr6"
@@ -1045,7 +1056,7 @@
 apply (rule_tac x="0::perm" in exI)
 apply (simp add: alpha_gen)
 (* needs rbv6_rsp *)
-sorry
+oops
 
 instantiation trm6 :: pt begin
 
@@ -1055,9 +1066,22 @@
   "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6"
 
 instance
+apply default
 sorry
 end
 
+lemma 
+"\<lbrakk>x1 = x2; \<And>a b. a = b \<Longrightarrow> P (Vr6 a) (Vr6 b);
+  \<And>t1 t2 s1 s2. \<lbrakk>t1 = t2; P t1 t2; s1 = s2; P s1 s2\<rbrakk> \<Longrightarrow> P (Ap6 t1 s1) (Ap6 t2 s2);
+  \<And>l1 r1 l2 r2.
+     \<exists>pi. (bv6 l1, r1) \<approx>gen (\<lambda>x1 x2. x1 = x2 \<and> P x1 x2) fv_trm6 pi (bv6 l2, r2) \<Longrightarrow>
+     P (Fo6 l1 r1) (Fo6 l2 r2)\<rbrakk>
+ \<Longrightarrow> P x1 x2"
+unfolding alpha_gen
+apply (lifting alpha6.induct[unfolded alpha_gen])
+apply(injection)
+sorry
+
 lemma "\<lbrakk>\<exists>pi. ((bv6 l1, r1) \<approx>gen (op =) fv_trm6 pi (bv6 l2, r2))\<rbrakk>
         \<Longrightarrow> Fo6 l1 r1 = Fo6 l2 r2"
 apply (unfold alpha_gen)