congr! 1
phi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi → σ v = σ' v
⊢ (fastReplaceFree σ phi).not_ = (fastReplaceFree σ' phi).not_
case h.e'_1
phi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi → σ v = σ' v
⊢ fastReplaceFree σ phi = fastReplaceFree σ' phi