congr! 1
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
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
⊢ ¬Holds D I V E' phi ↔ ¬Holds D I V E phi
case a.h.e'_1.a
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
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
⊢ Holds D I V E' phi ↔ Holds D I V E phi