132 lemma alpha_gen_atom_eqvt:

   133   assumes a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)"

   134   and     b: "\<exists>pia. ({atom a}, t) \<approx>gen \<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2) f pia ({atom b}, s)"

   135   shows  "\<exists>pia. ({atom (pi \<bullet> a)}, pi \<bullet> t) \<approx>gen R f pia ({atom (pi \<bullet> b)}, pi \<bullet> s)"

   136   using b apply -

   137   apply(erule exE)

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

   139   apply(simp add: alpha_gen.simps)

   140   apply(erule conjE)+

   141   apply(rule conjI)+

   142   apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])

   143   apply(simp add: a[symmetric] atom_eqvt eqvts)

   144   apply(rule conjI)

   145   apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])

   146   apply(simp add: a[symmetric] eqvts atom_eqvt)

   147   apply(subst permute_eqvt[symmetric])

   148   apply(simp)

   149   done

   150 

   151