simp
σ σ' : VarName → VarName
phi psi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    (∀ v ∉ binders, σ v = σ' v) → replaceFreeAux σ binders phi = replaceFreeAux σ' binders phi
psi_ih :
  ∀ (binders : Finset VarName),
    (∀ v ∉ binders, σ v = σ' v) → replaceFreeAux σ binders psi = replaceFreeAux σ' binders psi
binders : Finset VarName
h1 : ∀ v ∉ binders, σ v = σ' v
⊢ (replaceFreeAux σ binders phi).iff_ (replaceFreeAux σ binders psi) =
    (replaceFreeAux σ' binders phi).iff_ (replaceFreeAux σ' binders psi)
σ σ' : VarName → VarName
phi psi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    (∀ v ∉ binders, σ v = σ' v) → replaceFreeAux σ binders phi = replaceFreeAux σ' binders phi
psi_ih :
  ∀ (binders : Finset VarName),
    (∀ v ∉ binders, σ v = σ' v) → replaceFreeAux σ binders psi = replaceFreeAux σ' binders psi
binders : Finset VarName
h1 : ∀ v ∉ binders, σ v = σ' v
⊢ replaceFreeAux σ binders phi = replaceFreeAux σ' binders phi ∧
    replaceFreeAux σ binders psi = replaceFreeAux σ' binders psi