congr! 1
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
psi_ih : ∀ (V : VarAssignment D), all_def_in_env E psi → (Holds D I V E' psi ↔ Holds D I V E psi)
V : VarAssignment D
h2_left : all_def_in_env E phi
h2_right : all_def_in_env E psi
⊢ (Holds D I V E' phi ↔ Holds D I V E' psi) ↔ (Holds D I V E phi ↔ Holds D I V E psi)
case a.h.e'_1.a
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
psi_ih : ∀ (V : VarAssignment D), all_def_in_env E psi → (Holds D I V E' psi ↔ Holds D I V E psi)
V : VarAssignment D
h2_left : all_def_in_env E phi
h2_right : all_def_in_env E psi
⊢ Holds D I V E' phi ↔ Holds D I V E phi

case a.h.e'_2.a
D : Type
I : Interpretation D
E E' : Env
h1 : ∃ E1, E' = E1 ++ E
h3 : E'.nodup_
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D), all_def_in_env E phi → (Holds D I V E' phi ↔ Holds D I V E phi)
psi_ih : ∀ (V : VarAssignment D), all_def_in_env E psi → (Holds D I V E' psi ↔ Holds D I V E psi)
V : VarAssignment D
h2_left : all_def_in_env E phi
h2_right : all_def_in_env E psi
⊢ Holds D I V E' psi ↔ Holds D I V E psi