simp only [List.map_eq_map_iff]
case a.h.e'_4
D : Type
I : Interpretation D
X : String
vs : List Var
V V' : VarAssignment D
h1 : ∀ v ∈ vs, V v = V' v
⊢ List.map V vs = List.map V' vs
case a.h.e'_4
D : Type
I : Interpretation D
X : String
vs : List Var
V V' : VarAssignment D
h1 : ∀ v ∈ vs, V v = V' v
⊢ ∀ x ∈ vs, V x = V' x