obtain s1 := fresh_not_mem x c (Finset.image (Function.updateITE σ x x) (freeVarSet phi))
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})
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
s1 :
  fresh x c (Finset.image (Function.updateITE σ x x) phi.freeVarSet) ∉
    Finset.image (Function.updateITE σ x x) phi.freeVarSet
⊢ 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})