simp only [List.map_eq_map_iff]
case a.h.e'_4
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
X : PredName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
⊢ List.map V xs = List.map V' xs
case a.h.e'_4
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
X : PredName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
⊢ ∀ x ∈ xs, V x = V' x