intro _
v x : VarName
phi : Formula
phi_ih : fastReplaceFree v v phi = phi
⊢ ¬v = x → fastReplaceFree v v phi = phi
v x : VarName
phi : Formula
phi_ih : fastReplaceFree v v phi = phi
a✝ : ¬v = x
⊢ fastReplaceFree v v phi = phi