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
x' : VarName
s1 : x' ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
s2 :
  Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) ⊆
    Finset.image (Function.updateITE σ x x) phi.freeVarSet
s3 : x' ∉ Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
⊢ Finset.image (Function.updateITE σ x x') phi.freeVarSet \ {x'} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
no goals