simp
case s2.h
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
⊢ phi.freeVarSet \ {x} ⊆ phi.freeVarSet

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
⊢ Finset.image (Function.updateITE σ x x') phi.freeVarSet \ {x'} =
    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
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
⊢ Finset.image (Function.updateITE σ x x') phi.freeVarSet \ {x'} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})