congr! 1
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)
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