case pred_3_ v phi ih =>
  intro D I V E _
  simp only [Holds]
  intro a2 d
  have s1 : Holds D I (Function.updateITE V v d) E phi ↔ Holds D I V E phi
  {
    apply Holds_coincide_Var
    intro v' a1
    simp only [Function.updateITE]
    split_ifs
    case _ c1 =>
      subst c1
      contradiction
    case _ c1 =>
      rfl
  }
  simp only [s1]
  exact a2
Δ : List Formula
F : Formula
v : VarName
phi : Formula
ih : ¬isFreeIn v phi
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env),
    (∀ H ∈ [], Holds D I V E H) → Holds D I V E (phi.imp_ (forall_ v phi))
no goals