case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  simp only [admitsAux] at h1
  simp only [replace]
  simp only [Holds]
  first | apply forall_congr' | apply exists_congr
  intro d
  apply phi_ih (Function.updateITE V x d) (binders ∪ {x}) h1
  intro v a1
  simp only [Function.updateITE]
  simp at a1
  push_neg at a1
  cases a1
  case h.intro a1_left a1_right =>
    simp only [if_neg a1_right]
    exact h2 v a1_left
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                if ds.length = (τ X ds.length).1.length then
                  Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (exists_ x phi)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E (exists_ x phi) ↔
    Holds D I V E (replace τ (exists_ x phi))
no goals