case _ c1 =>
  obtain s1 := fresh_not_mem x c (Finset.image (Function.updateITE σ x x) (freeVarSet phi))
  generalize (
  fresh x c (Finset.image (Function.updateITE σ x x) (freeVarSet phi)) ) = x' at *
  have s2 : Finset.image (Function.updateITE σ x x) (freeVarSet phi \ {x}) ⊆ Finset.image (Function.updateITE σ x x) (freeVarSet phi)
  apply Finset.image_subset_image
  simp
  have s3 : x' ∉ Finset.image (Function.updateITE σ x x) (freeVarSet phi \ {x})
  apply Finset.not_mem_mono s2 s1
  calc
    Finset.image (Function.updateITE σ x x') (freeVarSet phi) \ {x'}
  = Finset.image (Function.updateITE σ x x') (freeVarSet phi \ {x}) \ {x'} :=
      by
      {
        apply Finset.image_sdiff_singleton phi.freeVarSet x x' (Function.updateITE σ x x')
        simp only [Function.updateITE]
        simp
      }
  _ = Finset.image (Function.updateITE σ x x) (freeVarSet phi \ {x}) \ {x'} :=
      by simp only [Finset.image_congr_update_ite phi.freeVarSet x x' x]
  _ = Finset.image (Function.updateITE σ x x) (freeVarSet phi \ {x}) :=
      by exact Finset.sdiff_singleton_eq_self s3
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 (fresh x c (Finset.image (Function.updateITE σ x x) phi.freeVarSet)))
        phi.freeVarSet \
      {fresh x c (Finset.image (Function.updateITE σ x x) phi.freeVarSet)} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
no goals