simp only [Holds]
case exists_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (V : VarAssignment D), all_def_in_env E a✝ → (Holds D I V E' a✝ ↔ Holds D I V E a✝)
V : VarAssignment D
h2 : all_def_in_env E a✝
⊢ Holds D I V E' (exists_ a✝¹ a✝) ↔ Holds D I V E (exists_ a✝¹ a✝)
case exists_
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (V : VarAssignment D), all_def_in_env E a✝ → (Holds D I V E' a✝ ↔ Holds D I V E a✝)
V : VarAssignment D
h2 : all_def_in_env E a✝
⊢ (∃ d, Holds D I (Function.updateITE V a✝¹ d) E' a✝) ↔ ∃ d, Holds D I (Function.updateITE V a✝¹ d) E a✝