simp only [List.map_eq_map_iff]
case a.h.e'_4
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (pred_const_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ List.map V' xs = List.map (V ∘ σ) xs
case a.h.e'_4
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 : ∀ x ∈ (pred_const_ X xs).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ ∀ x ∈ xs, V' x = (V ∘ σ) x