676 lemma alpha_gen_compose_eqvt:

   677   fixes  pia

   678   assumes b: "(g d, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2)) f pia (g e, s)"

   679   and     c: "\<And>y. pi \<bullet> (g y) = g (pi \<bullet> y)"

   680   and     a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)"

   681   shows  "(g (pi \<bullet> d), pi \<bullet> t) \<approx>gen R f (pi \<bullet> pia) (g (pi \<bullet> e), pi \<bullet> s)"

   682   using b

   683   apply -

   684   apply(simp add: alpha_gen.simps)

   685   apply(erule conjE)+

   686   apply(rule conjI)

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

   688   apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt c[symmetric])

   689   apply(rule conjI)

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

   691   apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt c[symmetric])

   692   apply(subst permute_eqvt[symmetric])

   693   apply(simp)

   694   sorry

   695