simp only [Holds]
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x h1_y h1_v h1_t : VarName
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E (eq_ h1_x h1_y) ↔
    Holds D I V E (eq_ (if h1_v = h1_x then h1_t else h1_x) (if h1_v = h1_y then h1_t else h1_y))
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_x h1_y h1_v h1_t : VarName
V : VarAssignment D
⊢ Function.updateITE V h1_v (V h1_t) h1_x = Function.updateITE V h1_v (V h1_t) h1_y ↔
    V (if h1_v = h1_x then h1_t else h1_x) = V (if h1_v = h1_y then h1_t else h1_y)