case
  forall_not_free_in h1_x h1_phi h1_v h1_t h1_1
| exists_not_free_in h1_x h1_phi h1_v h1_t h1_1 =>
  simp only [isFreeIn] at h1_1
  simp at h1_1
  split_ifs
  case pos c1 =>
    rfl
  case neg c1 =>
    congr!
    apply Rec.not_free_in_fastReplaceFree_self
    exact h1_1 c1
F F' : Formula
v u h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_1 : ¬isFreeIn h1_v (exists_ h1_x h1_phi)
⊢ (if h1_v = h1_x then exists_ h1_x h1_phi else exists_ h1_x (Rec.fastReplaceFree h1_v h1_t h1_phi)) =
    exists_ h1_x h1_phi
no goals