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