[STATEMENT]
lemma wls_freshAbs_swapAbs_compose_aux:
"\<lbrakk>wlsAbs (us,s) A; wlsPar P\<rbrakk> \<Longrightarrow>
 \<forall> x y z. {x,y,z} \<subseteq> varsOfS P xs \<and> freshAbs xs y A \<and> freshAbs xs z A \<longrightarrow>
           ((A $[y \<and> x]_xs) $[z \<and> y]_xs) = (A $[z \<and> x]_xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wlsAbs (us, s) A; wlsPar P\<rbrakk> \<Longrightarrow> \<forall>x y z. {x, y, z} \<subseteq> varsOfS P xs \<and> freshAbs xs y A \<and> freshAbs xs z A \<longrightarrow> A $[y \<and> x]_xs $[z \<and> y]_xs = A $[z \<and> x]_xs
[PROOF STEP]
apply(erule wlsAbs_fresh_cases)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. wlsPar P \<Longrightarrow> wlsPar P
 2. \<And>x X. \<lbrakk>wlsPar P; wls s X; \<And>ys. x \<notin> varsOfS P ys; \<And>s' Y. Y \<in> termsOfS P s' \<Longrightarrow> fresh us x Y; \<And>usa s' B. B \<in> absOfS P (usa, s') \<Longrightarrow> freshAbs us x B; \<And>rho. rho \<in> envsOfS P \<Longrightarrow> freshEnv us x rho\<rbrakk> \<Longrightarrow> \<forall>xa y z. {xa, y, z} \<subseteq> varsOfS P xs \<and> freshAbs xs y (Abs us x X) \<and> freshAbs xs z (Abs us x X) \<longrightarrow> Abs us x X $[y \<and> xa]_xs $[z \<and> y]_xs = Abs us x X $[z \<and> xa]_xs
[PROOF STEP]
by simp_all (metis fresh_swap_compose sw_def wls_imp_good)