simp only [fastAdmits]
case a.a.a
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ fastAdmits v t P.not_
case a.a.a
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ fastAdmitsAux v t ∅ P.not_