case _ c1 =>
  simp at c1
  have s1 : Finset.image (Function.updateITE σ x x) (freeVarSet phi) \ {x} = Finset.image (Function.updateITE σ x x) (freeVarSet phi \ {x}) \ {x}
  apply Finset.image_sdiff_singleton
  simp only [Function.updateITE]
  simp
  simp only [s1]
  clear s1
  have s2 : x ∉ Finset.image (Function.updateITE σ x x) (freeVarSet phi \ {x})
  simp only [Finset.mem_image]
  simp
  simp only [Function.updateITE]
  simp
  tauto
  simp only [Finset.sdiff_singleton_eq_self s2]
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
⊢ Finset.image (Function.updateITE σ x x) phi.freeVarSet \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
no goals