simp only [Function.updateITE]
case s1.h1
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
⊢ Function.updateITE σ x x x = x

c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
s1 :
  Finset.image (Function.updateITE σ x x) phi.freeVarSet \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) \ {x}
⊢ Finset.image (Function.updateITE σ x x) phi.freeVarSet \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
case s1.h1
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
⊢ (if True then x else σ x) = x

c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
c1 : ∀ x_1 ∈ phi.freeVarSet, ¬x_1 = x → ¬σ x_1 = x
s1 :
  Finset.image (Function.updateITE σ x x) phi.freeVarSet \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x}) \ {x}
⊢ Finset.image (Function.updateITE σ x x) phi.freeVarSet \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})