simp
case pos.h1
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), ¬isFreeIn v phi → admitsAux v u binders phi
binders : Finset VarName
h1 : ¬(¬v = x ∧ isFreeIn v phi)
c1 : v = x
⊢ v ∈ binders ∪ {x}
case pos.h1
v u x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), ¬isFreeIn v phi → admitsAux v u binders phi
binders : Finset VarName
h1 : ¬(¬v = x ∧ isFreeIn v phi)
c1 : v = x
⊢ v ∈ binders ∨ v = x