diff -r 925a5e9aa832 -r 00680cea0dde Nominal/Abs.thy
--- a/Nominal/Abs.thy	Thu Apr 01 08:06:01 2010 +0200
+++ b/Nominal/Abs.thy	Thu Apr 01 08:48:33 2010 +0200
@@ -444,6 +444,12 @@
   \<and> pi \<bullet> bsl = csl)"
 by (simp_all add: alphas)
 
+lemma alphas3:
+  "(bsl, x1, x2, x3) \<approx>lst (\<lambda>(x1, y1, z1) (x2, y2, z2). R1 x1 x2 \<and> R2 y1 y2 \<and> R3 z1 z2) (\<lambda>(a, b, c). f1 a \<union> (f2 b \<union> f3 c)) pi (csl, y1, y2, y3) = (f1 x1 \<union> (f2 x2 \<union> f3 x3) - set bsl = f1 y1 \<union> (f2 y2 \<union> f3 y3) - set csl \<and>
+     (f1 x1 \<union> (f2 x2 \<union> f3 x3) - set bsl) \<sharp>* pi \<and>
+     R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2 \<and> R3 (pi \<bullet> x3) y3 \<and> pi \<bullet> bsl = csl)"
+by (simp add: alphas)
+
 lemma alpha_gen_compose_sym:
   fixes pi
   assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)"