diff -r e655ea5f0b5f -r 95324fb345e5 Nominal/Term5.thy
--- a/Nominal/Term5.thy	Thu Mar 11 14:05:36 2010 +0100
+++ b/Nominal/Term5.thy	Thu Mar 11 14:09:54 2010 +0100
@@ -54,9 +54,26 @@
 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