case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  simp only [phi_ih]
  simp only [<- Finset.image_sdiff_singleton_updateITE phi.freeVarSet x x σ]
  split_ifs
  case _ c1 =>
    obtain s1 := fresh_not_mem x c (Finset.image (Function.updateITE σ x x) (freeVarSet phi))
    generalize (
    fresh x c (Finset.image (Function.updateITE σ x x) (freeVarSet phi)) ) = x' at *
    have s2 : Finset.image (Function.updateITE σ x x) (freeVarSet phi \ {x}) ⊆ Finset.image (Function.updateITE σ x x) (freeVarSet phi)
    apply Finset.image_subset_image
    simp
    have s3 : x' ∉ Finset.image (Function.updateITE σ x x) (freeVarSet phi \ {x})
    apply Finset.not_mem_mono s2 s1
    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
  case _ c1 =>
    simp at c1
    have s1 : Finset.image (Function.updateITE σ x x) (freeVarSet phi) \ {x} = Finset.image (Function.updateITE σ x x) (freeVarSet phi \ {x}) \ {x}
    apply Finset.image_sdiff_singleton
    simp only [Function.updateITE]
    simp
    simp only [s1]
    clear s1
    have s2 : x ∉ Finset.image (Function.updateITE σ x x) (freeVarSet phi \ {x})
    simp only [Finset.mem_image]
    simp
    simp only [Function.updateITE]
    simp
    tauto
    simp only [Finset.sdiff_singleton_eq_self s2]
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
⊢ (sub
          (Function.updateITE σ x
            (if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet
            else x))
          c phi).freeVarSet \
      {if ∃ y ∈ phi.freeVarSet \ {x}, σ y = x then fresh x c (sub (Function.updateITE σ x x) c phi).freeVarSet else x} =
    Finset.image σ (phi.freeVarSet \ {x})
no goals