692 lemma alpha_gen_compose_eqvt:

   693   fixes  pia

   694   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)"

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

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

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

   698   using b

   699   apply -

   700   apply(simp add: alpha_gen.simps)

   701   apply(erule conjE)+

   702   apply(rule conjI)

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

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

   705   apply(rule conjI)

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

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

   708   apply(subst permute_eqvt[symmetric])

   709   apply(simp)

   710   sorry

   711