case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  push_neg at h1
  cases h1
  case intro h1_left h1_right =>
    split_ifs
    case pos c1 =>
      simp only [fastReplaceFree]
      simp only [if_neg h1_left]
      congr!
      apply not_free_in_fastReplaceFree_self
      contrapose! h1_right
      exact isFreeIn_imp_occursIn t phi h1_right
    case neg c1 =>
      simp only [fastReplaceFree]
      simp only [if_neg h1_left]
      congr!
      exact phi_ih h1_right
v t x : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1 : ¬(t = x ∨ occursIn t phi)
⊢ fastReplaceFree t v (if v = x then exists_ x phi else exists_ x (fastReplaceFree v t phi)) = exists_ x phi
no goals