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