[STATEMENT]
lemma fresh_vsubstEnv_updEnv[simp]:
assumes rho: "goodEnv rho"
and *: "freshEnv ys y rho"
shows "(rho &[y1 // y]_ys) = (rho [y \<leftarrow> Var ys y1]_ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rho &[y1 // y]_ys = rho [y \<leftarrow> Var ys y1]_ys
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
goodEnv rho
freshEnv ys y rho

goal (1 subgoal):
 1. rho &[y1 // y]_ys = rho [y \<leftarrow> Var ys y1]_ys
[PROOF STEP]
unfolding vsubstEnv_def
[PROOF STATE]
proof (prove)
using this:
goodEnv rho
freshEnv ys y rho

goal (1 subgoal):
 1. rho &[Var ys y1 / y]_ys = rho [y \<leftarrow> Var ys y1]_ys
[PROOF STEP]
by simp