[STATEMENT]
theorem wls_freshAbs_vsubstAbs:
assumes "wlsAbs (us,s) A"
shows "freshAbs zs z (A $[y1 // y]_ys) =
       (((zs = ys \<and> z = y) \<or> freshAbs zs z A) \<and>
        (freshAbs ys y A \<or> (zs \<noteq> ys \<or> z \<noteq> y1)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. freshAbs zs z (A $[y1 // y]_ys) = ((zs = ys \<and> z = y \<or> freshAbs zs z A) \<and> (freshAbs ys y A \<or> zs \<noteq> ys \<or> z \<noteq> y1))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wlsAbs (us, s) A

goal (1 subgoal):
 1. freshAbs zs z (A $[y1 // y]_ys) = ((zs = ys \<and> z = y \<or> freshAbs zs z A) \<and> (freshAbs ys y A \<or> zs \<noteq> ys \<or> z \<noteq> y1))
[PROOF STEP]
by(simp add: freshAbs_vsubstAbs)