simp only [List.map_eq_map_iff]
case a.h.e'_4
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
h2 : ∀ v ∈ vs, Var.lc_at j v
⊢ List.map V vs = List.map ((V ∘ Var.close j (free_ z)) ∘ Var.openList j [free_ z]) vs
case a.h.e'_4
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
h2 : ∀ v ∈ vs, Var.lc_at j v
⊢ ∀ x ∈ vs, V x = ((V ∘ Var.close j (free_ z)) ∘ Var.openList j [free_ z]) x