right
v t x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName), ¬occursIn t phi → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t phi)
binders : Finset VarName
h2 : v ∉ binders
h1_left : t ≠ x
h1_right : ¬occursIn t phi
c1 : ¬v = x
⊢ t = x ∨ fastAdmitsAux t v (binders ∪ {x}) (fastReplaceFree v t phi)
case h
v t x : VarName
phi : Formula
phi_ih :
  ∀ (binders : Finset VarName), ¬occursIn t phi → v ∉ binders → fastAdmitsAux t v binders (fastReplaceFree v t phi)
binders : Finset VarName
h2 : v ∉ binders
h1_left : t ≠ x
h1_right : ¬occursIn t phi
c1 : ¬v = x
⊢ fastAdmitsAux t v (binders ∪ {x}) (fastReplaceFree v t phi)