case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  congr! 1
  apply phi_ih
  intro v a1
  simp only [Function.updateITE]
  split_ifs
  case _ c1 =>
    rfl
  case _ c1 =>
    apply h1
    tauto
x : VarName
phi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), ¬v = x ∧ isFreeIn v phi → σ v = σ' v
⊢ exists_ x (fastReplaceFree (Function.updateITE σ x x) phi) =
    exists_ x (fastReplaceFree (Function.updateITE σ' x x) phi)
no goals