tauto
case neg.h.h1
v x : VarName
phi : Formula
phi_ih : ∀ (binders : Finset VarName), v ∉ binders → fastAdmitsAux v v binders phi
binders : Finset VarName
h1 : v ∉ binders
c1 : ¬v = x
⊢ v ∉ binders ∧ ¬v = x
no goals