simp only [Holds]
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
v✝ t✝ : VarName
V : VarAssignment D
⊢ Holds D I (Function.updateITE V v✝ (V t✝)) E false_ ↔ Holds D I V E false_
no goals