simp only [Var.close]
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
x : String
⊢ shift D V d (Var.close (j + 1) (free_ z) (free_ x)) = V (Var.close j (free_ z) (free_ x))
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
x : String
⊢ shift D V d (if free_ x = free_ z then bound_ (j + 1) else free_ x) =
    V (if free_ x = free_ z then bound_ j else free_ x)