apply exists_congr
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
V : VarAssignment D
h2 : all_def_in_env E phi
⊢ (∃ d, Holds D I (Function.updateITE V x d) E' phi) ↔ ∃ d, Holds D I (Function.updateITE V x d) E phi
case h
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
V : VarAssignment D
h2 : all_def_in_env E phi
⊢ ∀ (a : D), Holds D I (Function.updateITE V x a) E' phi ↔ Holds D I (Function.updateITE V x a) E phi