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_left : t ≠ x
h1_right : ¬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