case _ c1 =>
  simp only [Function.updateITE]
  split_ifs
  case _ c2 c3 =>
    rfl
  case _ c2 c3 =>
    contradiction
  case _ c2 c3 =>
    obtain s1 := fresh_not_mem x c ((Finset.image (Function.updateITE σ x x) (freeVarSet phi)) ∪ (Finset.biUnion (predVarSet phi) (predVarFreeVarSet τ)))
    simp only [← c3] at s1
    simp only [Finset.mem_union] at s1
    simp only [isFreeIn_iff_mem_freeVarSet] at a1
    obtain s2 := Finset.mem_image_of_mem (Function.updateITE σ x x) a1
    simp only [Function.updateITE] at s2
    simp only [if_neg c2] at s2
    exfalso
    apply s1
    left
    exact s2
  case _ c2 c3 =>
    apply h1
    tauto
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), ¬x_1 = x ∧ isFreeIn x_1 phi → V' x_1 = V (σ x_1)
h2 : ∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
d : D
v : VarName
a1 : isFreeIn v phi
c1 : x ∈ Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ)
⊢ Function.updateITE V' x d v =
    Function.updateITE V
      (fresh x c
        (Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ)))
      d
      (Function.updateITE σ x
        (fresh x c
          (Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ)))
        v)
no goals