--- a/Nominal/Term5.thy	Wed Mar 10 15:34:13 2010 +0100
+++ b/Nominal/Term5.thy	Wed Mar 10 15:40:15 2010 +0100
@@ -54,15 +54,15 @@
 apply (induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts)
 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: 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])
-apply (subst permute_eqvt)
-apply simp
-sorry
+apply (simp add: eqvts)
+done
 
 lemma alpha5_equivp:
   "equivp alpha_rtrm5"