case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  first | apply forall_congr' | apply exists_congr
  intro a
  have s1 : Function.updateITE V (σ x) a ∘ σ = Function.updateITE (V ∘ σ) x a
  apply Function.updateITE_comp_right_injective
  apply h1
  simp only [← s1]
  exact phi_ih (Function.updateITE V (σ x) a)
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
V : VarAssignment D
⊢ (∃ d, Holds D I (Function.updateITE (V ∘ σ) x d) E phi) ↔
    ∃ d, Holds D I (Function.updateITE V (σ x) d) E (replaceAll σ phi)
no goals