51   "xa \<approx>5 y \<Longrightarrow> (x \<bullet> xa) \<approx>5 (x \<bullet> y)"

    51   "(xa \<approx>5 y \<longrightarrow> (p \<bullet> xa) \<approx>5 (p \<bullet> y)) \<and>

    52   "xb \<approx>l ya \<Longrightarrow> (x \<bullet> xb) \<approx>l (x \<bullet> ya)"

    52   (xb \<approx>l ya \<longrightarrow> (p \<bullet> xb) \<approx>l (p \<bullet> ya)) \<and>

    53   "alpha_rbv5 a b c \<Longrightarrow> alpha_rbv5 (x \<bullet> a) (x \<bullet> b) (x \<bullet> c)"

    53   (alpha_rbv5 a b c \<longrightarrow> alpha_rbv5 (p \<bullet> a) (p \<bullet> b) (p \<bullet> c))"

    54 apply (induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts)

    54 apply (tactic {* alpha_eqvt_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj permute_rtrm5_permute_rlts.simps} @{context} 1 *})

    55 apply (simp_all add: alpha5_inj permute_eqvt[symmetric])

    55 done

    56 apply (erule exE)

    56 

    57 apply (rule_tac x="x \<bullet> pi" in exI)

    57 lemma alpha5_reflp:

    58 apply (erule conjE)+

    58 "y \<approx>5 y \<and> (x \<approx>l x \<and> alpha_rbv5 0 x x)"

    59 apply (rule conjI)

    59 apply (rule rtrm5_rlts.induct)

    60 apply (erule alpha_gen_compose_eqvt)

    60 apply (simp_all add: alpha5_inj)

    61 apply (simp_all add: eqvts)

    61 apply (rule_tac x="0::perm" in exI)

    62 apply (simp add: permute_eqvt[symmetric])

    62 apply (simp add: eqvts alpha_gen fresh_star_def fresh_zero_perm)

    63 apply (subst eqvts[symmetric])

    63 done

    64 apply (simp add: eqvts)

    64 

    65 done

    65 lemma alpha5_symp:

    66 "(a \<approx>5 b \<longrightarrow> a \<approx>5 b) \<and>

    67 (x \<approx>l y \<longrightarrow> y \<approx>l x) \<and>

    68 (alpha_rbv5 p x y \<longrightarrow> alpha_rbv5 (-p) y x)"

    69 apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct)

    70 apply (simp_all add: alpha5_inj)

    71 sorry