[STATEMENT]
theorem wls_swapAbs_involutive2[simp]:
"wlsAbs (us,s) A \<Longrightarrow> ((A $[x \<and> y]_zs) $[y \<and> x]_zs) = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wlsAbs (us, s) A \<Longrightarrow> A $[x \<and> y]_zs $[y \<and> x]_zs = A
[PROOF STEP]
using wls_swapAbs_sym[of us s A zs x y]
[PROOF STATE]
proof (prove)
using this:
wlsAbs (us, s) A \<Longrightarrow> A $[x \<and> y]_zs = A $[y \<and> x]_zs

goal (1 subgoal):
 1. wlsAbs (us, s) A \<Longrightarrow> A $[x \<and> y]_zs $[y \<and> x]_zs = A
[PROOF STEP]
by auto