split_ifs
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
⊢ Finset.image
        (Function.updateITE σ x
          (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then
            fresh x c (Finset.image (Function.updateITE σ x x) phi.freeVarSet)
          else x))
        phi.freeVarSet \
      {if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (Finset.image (Function.updateITE σ x x) phi.freeVarSet)
        else x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})
case pos
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
h✝ : ∃ 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})

case neg
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
h✝ : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
⊢ Finset.image (Function.updateITE σ x x) phi.freeVarSet \ {x} =
    Finset.image (Function.updateITE σ x x) (phi.freeVarSet \ {x})