cases h1
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), ¬isBoundIn u phi → u ∉ binders → fastAdmitsAux v u binders phi
binders : Finset VarName
h2 : u ∉ binders
h1 : u ≠ x ∧ ¬isBoundIn u phi
⊢ v = x ∨ fastAdmitsAux v u (binders ∪ {x}) phi
case intro
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), ¬isBoundIn u phi → u ∉ binders → fastAdmitsAux v u binders phi
binders : Finset VarName
h2 : u ∉ binders
left✝ : u ≠ x
right✝ : ¬isBoundIn u phi
⊢ v = x ∨ fastAdmitsAux v u (binders ∪ {x}) phi