--- a/Nominal/Term5.thy	Wed Mar 10 14:24:27 2010 +0100
+++ b/Nominal/Term5.thy	Wed Mar 10 14:47:04 2010 +0100
@@ -50,15 +50,18 @@
 lemma alpha5_eqvt:
   "xa \<approx>5 y \<Longrightarrow> (x \<bullet> xa) \<approx>5 (x \<bullet> y)"
   "xb \<approx>l ya \<Longrightarrow> (x \<bullet> xb) \<approx>l (x \<bullet> ya)"
-  "alpha_rbv5 a b c \<Longrightarrow> True"
+  "alpha_rbv5 a b c \<Longrightarrow> alpha_rbv5 (x \<bullet> a) (x \<bullet> b) (x \<bullet> c)"
 apply (induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts)
-apply (simp_all add: alpha5_inj)
+apply (simp_all add: alpha5_inj permute_eqvt[symmetric])
 apply (erule exE)
 apply (rule_tac x="pi" in exI)
+apply (simp add: alpha_gen)
 apply clarify
-apply (simp add: alpha_gen fv_rtrm5_rlts_eqvt[symmetric] rbv5_eqvt[symmetric])
+apply (simp add: fv_rtrm5_rlts_eqvt[symmetric] rbv5_eqvt[symmetric])
 apply (subst eqvts[symmetric])
 apply (subst eqvts[symmetric])
+apply (subst permute_eqvt)
+apply simp
 sorry
 
 lemma alpha5_equivp: