--- a/Nominal/Term5.thy	Wed Mar 10 16:50:42 2010 +0100
+++ b/Nominal/Term5.thy	Wed Mar 10 16:51:15 2010 +0100
@@ -50,16 +50,19 @@
 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 clarify
-apply (simp add: alpha_gen fv_rtrm5_rlts_eqvt[symmetric] rbv5_eqvt[symmetric])
+apply (rule_tac x="x \<bullet> pi" in exI)
+apply (erule conjE)+
+apply (rule conjI)
+apply (erule alpha_gen_compose_eqvt)
+apply (simp_all add: eqvts)
+apply (simp add: permute_eqvt[symmetric])
 apply (subst eqvts[symmetric])
-apply (subst eqvts[symmetric])
-sorry
+apply (simp add: eqvts)
+done
 
 lemma alpha5_equivp:
   "equivp alpha_rtrm5"