case compat_forall_ h1_phi h1_psi h1_x _ h1_ih | compat_exists_ h1_phi h1_psi h1_x _ h1_ih =>
  simp only [Holds]
  first | apply forall_congr' | apply exists_congr
  intro d
  exact h1_ih (Function.updateITE V h1_x d)
D : Type
I : Interpretation D
E : Env
F F' h1_phi h1_psi : Formula
h1_x : VarName
a✝ : AlphaEqv h1_phi h1_psi
h1_ih : ∀ (V : VarAssignment D), Holds D I V E h1_phi ↔ Holds D I V E h1_psi
V : VarAssignment D
⊢ Holds D I V E (exists_ h1_x h1_phi) ↔ Holds D I V E (exists_ h1_x h1_psi)
no goals