case pred_const_ h1_X h1_xs h1_v h1_t | pred_var_ h1_X h1_xs h1_v h1_t =>
  simp only [Holds]
  congr! 1
  simp
  simp only [List.map_eq_map_iff]
  intro x _
  simp only [Function.updateITE]
  simp only [eq_comm]
  split_ifs
  case _ c1 =>
    simp
    simp only [if_pos c1]
  case _ c1 =>
    simp
    simp only [if_neg c1]
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
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E (pred_var_ h1_X h1_xs) ↔
    Holds D I V E (pred_var_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
no goals