case
  forall_free_in h1_x h1_phi h1_v h1_t h1_phi' h1_1 _ _ h1_ih
| exists_free_in h1_x h1_phi h1_v h1_t h1_phi' h1_1 _ _ h1_ih =>
  simp only [isFreeIn] at h1_1
  cases h1_1
  case intro h1_1_left h1_1_right =>
    simp only [if_neg h1_1_left]
    subst h1_ih
    rfl
F F' : Formula
v u h1_x : VarName
h1_phi : Formula
h1_v h1_t : VarName
h1_phi' : Formula
h1_1 : isFreeIn h1_v (exists_ h1_x h1_phi)
a✝¹ : ¬h1_x = h1_t
a✝ : IsSub h1_phi h1_v h1_t h1_phi'
h1_ih : Rec.fastReplaceFree h1_v h1_t h1_phi = 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