--- a/Nominal/Term5.thy	Thu Mar 11 15:10:07 2010 +0100
+++ b/Nominal/Term5.thy	Thu Mar 11 16:12:15 2010 +0100
@@ -48,25 +48,32 @@
   done
 
 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> 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 permute_eqvt[symmetric])
-apply (erule exE)
-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 (simp add: eqvts)
+  "(xa \<approx>5 y \<longrightarrow> (p \<bullet> xa) \<approx>5 (p \<bullet> y)) \<and>
+  (xb \<approx>l ya \<longrightarrow> (p \<bullet> xb) \<approx>l (p \<bullet> ya)) \<and>
+  (alpha_rbv5 a b c \<longrightarrow> alpha_rbv5 (p \<bullet> a) (p \<bullet> b) (p \<bullet> c))"
+apply (tactic {* alpha_eqvt_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj permute_rtrm5_permute_rlts.simps} @{context} 1 *})
 done
 
+lemma alpha5_reflp:
+"y \<approx>5 y \<and> (x \<approx>l x \<and> alpha_rbv5 0 x x)"
+apply (rule rtrm5_rlts.induct)
+apply (simp_all add: alpha5_inj)
+apply (rule_tac x="0::perm" in exI)
+apply (simp add: eqvts alpha_gen fresh_star_def fresh_zero_perm)
+done
+
+lemma alpha5_symp:
+"(a \<approx>5 b \<longrightarrow> a \<approx>5 b) \<and>
+(x \<approx>l y \<longrightarrow> y \<approx>l x) \<and>
+(alpha_rbv5 p x y \<longrightarrow> alpha_rbv5 (-p) y x)"
+apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct)
+apply (simp_all add: alpha5_inj)
+sorry
+
 lemma alpha5_equivp:
   "equivp alpha_rtrm5"
   "equivp alpha_rlts"
+  "equivp (alpha_rbv5 p)"
   sorry
 
 quotient_type