# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268232015 -3600
# Node ID 01aa049d441a63cd3b86fccfdabfb6410c359105
# Parent  6f346b649f8e400924829e9684b0dc469dd9483b
alpha_equivp for trm5

diff -r 6f346b649f8e -r 01aa049d441a Nominal/Term5.thy
--- 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"