congr! 1
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
⊢ I.pred_var_ h1_X (List.map (Function.updateITE V h1_v (V h1_t)) h1_xs) ↔
    I.pred_var_ h1_X (List.map V (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
case a.h.e'_4
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : PredName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
⊢ List.map (Function.updateITE V h1_v (V h1_t)) h1_xs =
    List.map V (List.map (fun x => if h1_v = x then h1_t else x) h1_xs)