simp
v u : VarName
phi psi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      fastAdmitsAux v u binders phi → toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi)
psi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      fastAdmitsAux v u binders psi → toIsBoundAux binders psi = toIsBoundAux binders (fastReplaceFree v u psi)
binders : Finset VarName
h1 : v ∉ binders
h2 : fastAdmitsAux v u binders phi ∧ fastAdmitsAux v u binders psi
⊢ (toIsBoundAux binders phi).iff_ (toIsBoundAux binders psi) =
    (toIsBoundAux binders (fastReplaceFree v u phi)).iff_ (toIsBoundAux binders (fastReplaceFree v u psi))
v u : VarName
phi psi : Formula
phi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      fastAdmitsAux v u binders phi → toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi)
psi_ih :
  ∀ (binders : Finset VarName),
    v ∉ binders →
      fastAdmitsAux v u binders psi → toIsBoundAux binders psi = toIsBoundAux binders (fastReplaceFree v u psi)
binders : Finset VarName
h1 : v ∉ binders
h2 : fastAdmitsAux v u binders phi ∧ fastAdmitsAux v u binders psi
⊢ toIsBoundAux binders phi = toIsBoundAux binders (fastReplaceFree v u phi) ∧
    toIsBoundAux binders psi = toIsBoundAux binders (fastReplaceFree v u psi)