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
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
c1 : v = x
⊢ fastReplaceFree t v (exists_ x phi) = exists_ x phi
no goals