tauto
v t : VarName
phi psi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∉ binders → replaceFreeAux v t binders phi = fastReplaceFree v t phi
psi_ih : ∀ (binders : Finset VarName), v ∉ binders → replaceFreeAux v t binders psi = fastReplaceFree v t psi
binders : Finset VarName
h1 : v ∉ binders
⊢ replaceFreeAux v t binders phi = fastReplaceFree v t phi ∧ replaceFreeAux v t binders psi = fastReplaceFree v t psi
no goals