simp only [Holds]
D : Type
I : Interpretation D
X : String
vs : List Var
V V' : VarAssignment D
h1 : ∀ v ∈ vs, V v = V' v
⊢ Holds D I V (pred_ X vs) ↔ Holds D I V' (pred_ X vs)
D : Type
I : Interpretation D
X : String
vs : List Var
V V' : VarAssignment D
h1 : ∀ v ∈ vs, V v = V' v
⊢ I.pred_ X (List.map V vs) ↔ I.pred_ X (List.map V' vs)